4 (* string linearization of a reference *)
6 let str_uptoken = function
13 let rec str_up = function
15 | head :: tail -> str_uptoken head ^ str_up tail
19 | (Some t, None) -> "#1/" ^ string_of_int t
20 | (Some t, Some c) -> "#1/" ^ string_of_int t ^ "/" ^ string_of_int c
22 let str_tref (p, u, i) =
23 p ^ ":/" ^ str_up u ^ str_fi i
26 UriManager.string_of_uri u ^ str_fi i
28 (* raw HTML representation *)
30 let key s = "<font color=\"blue\">" ^ s ^ " </font>"
36 let con s = "<font color=\"red\">\"" ^ s ^ "\" </font>"
38 let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
44 (* HTML representation of a query *)
46 let out_rvar s = sym s
48 let out_svar s = sep "$" ^ sym s
50 let out_tref r = con (str_tref r)
52 let out_pat p = out_tref p
54 let out_func = function
55 | MQName -> key "name"
58 let out_str = function
60 | MQRVar s -> out_rvar s
61 | MQSVar s -> out_svar s
62 | MQFunc (f, r) -> out_func f ^ out_rvar r
63 | MQMConclusion -> key "mainconclusion"
64 | MQConclusion -> key "conclusion"
66 let rec out_bool = function
67 | MQTrue -> key "true"
68 | MQFalse -> key "false"
69 | MQIs (s, t) -> out_str s ^ key "is" ^ out_str t
70 | MQNot b -> key "not" ^ out_bool b
71 | MQAnd (b1, b2) -> sep "(" ^ out_bool b1 ^ key "and" ^ out_bool b2 ^ sep ")"
72 | MQOr (b1, b2) -> sep "(" ^ out_bool b1 ^ key "or" ^ out_bool b2 ^ sep ")"
73 | MQSetEqual (l1, l2) ->
74 sep "(" ^ out_list l1 ^ key "setequal" ^ out_list l2 ^ sep ")"
75 | MQSubset (l1, l2) ->
76 sep "(" ^ out_list l1 ^ key "subset" ^ out_list l2 ^ sep ")"
78 and out_list = function
79 | MQSelect (r, l, b) ->
80 key "select" ^ out_rvar r ^ key "in" ^ out_list l ^ key "where" ^ out_bool b
81 | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v
82 | MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ key "position" ^ out_svar v
83 | MQPattern p -> key "pattern" ^ out_pat p
84 | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
85 | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"
86 | MQRVarOccur v -> key "rvaroccur" ^ v
88 let out_query = function
89 | MQList l -> out_list l
91 (* HTML representation of a query result *)
93 let rec out_list = function
95 | u :: l -> res (str_tref u) ^ nl () ^ out_list l
98 par () ^ "Result:" ^ nl () ^
100 | MQRefs l -> out_list l
102 (* Converting functions *)
106 let i = Str.search_forward (Str.regexp_string ":/") s 0 in
107 let p = Str.string_before s i in
108 let q = Str.string_after s (i + 2) in
113 let encode = function
114 | Str.Text s -> MQString s
116 if s = "?" then MQAnyChr else
117 if s = "*" then MQAst else
118 if s = "**" then MQAstAst else
119 if s = "/" then MQSlash else MQString s
121 let tref_uref (u, i) =
122 let s = UriManager.string_of_uri u in
125 let rx = Str.regexp "\?\|\*\*\|\*\|/" in
126 let l = Str.full_split rx q in
127 (p, List.map encode l, i)
129 (* CIC term inspecting functions *)
131 let out_ie (r, b, v) =
132 let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
133 res (pos ^ str_uref r) ^ nl () ^
134 con (pos ^ str_tref (tref_uref r)) ^ nl ()
136 let rec out_il = function
138 | head :: tail -> out_ie head ^ out_il tail
140 let tie_uie (r, b, v) = (tref_uref r, b, v)
142 let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) =
143 UriManager.eq u1 u2 && f1 = f2 && b1 = b2
145 let rec ie_insert ie = function
148 head :: if ie_eq head ie then tail else ie_insert ie tail
152 (*CSC: che brutto il codice imperativo!!!*)
153 let universe = ref [];;
155 let inspect_uri main l uri t c v =
158 | (None, _) -> (None, None)
159 | (Some t0, c0) -> (Some (t0 + 1), c0)
161 (*CSC: sbagliato, credo. MQString non dovrebbe poter contenere slash *)
162 universe := (tref_uref (uri,fi))::!universe ;
166 ie_insert ((uri, fi), main, v) l
169 let rec inspect_term main l v = function
175 | Var u -> inspect_uri main l u None None v
176 | Const (u, i) -> inspect_uri main l u None None v
177 | MutInd (u, i, t) -> inspect_uri main l u (Some t) None v
178 | MutConstruct (u, i, t, c) -> inspect_uri main l u (Some t) (Some c) v
180 (*CSC: Cast modified so that it behaves exactly as if no Cast was there *)
181 inspect_term main l v uu
182 | Prod (n, uu, tt) ->
183 let luu = inspect_term false l (v + 1) uu in
184 inspect_term false luu (v + 1) tt
185 | Lambda (n, uu, tt) ->
186 let luu = inspect_term false l (v + 1) uu in
187 inspect_term false luu (v + 1) tt
188 | LetIn (n, uu, tt) ->
189 let luu = inspect_term false l (v + 1) uu in
190 inspect_term false luu (v + 1) tt
191 | Appl m -> inspect_list main l true v m
192 | MutCase (u, i, t, tt, uu, m) ->
193 let lu = inspect_uri main l u (Some t) None (v + 1) in
194 let ltt = inspect_term false lu (v + 1) tt in
195 let luu = inspect_term false ltt (v + 1) uu in
196 inspect_list main luu false (v + 1) m
197 | Fix (i, m) -> inspect_ind l (v + 1) m
198 | CoFix (i, m) -> inspect_coind l (v + 1) m
199 and inspect_list main l head v = function
202 let ltt = inspect_term main l (if head then v else v+1) tt in
203 inspect_list false ltt false v m
204 and inspect_ind l v = function
206 | (n, i, tt, uu) :: m ->
207 let ltt = inspect_term false l v tt in
208 let luu = inspect_term false ltt v uu in
210 and inspect_coind l v = function
212 | (n, tt, uu) :: m ->
213 let ltt = inspect_term false l v tt in
214 let luu = inspect_term false ltt v uu in
215 inspect_coind luu v m
217 let inspect t = inspect_term true [] 0 t
219 (* query building functions *)
222 let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
223 (64 * 6 + 8 * 6 + 4) "mquery.htm" in
224 output_string och s; flush och; s
226 let build_select (r, b, v) n =
227 let rvar = "ref" ^ string_of_int n in
228 let svar = "str" ^ string_of_int n in
229 let mqs = if b then MQMConclusion else MQConclusion in
231 MQUse (MQPattern r, svar),
232 MQIs (MQSVar svar, mqs)
235 let rec build_inter n = function
236 | [] -> MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None))
237 | [ie] -> build_select ie n
238 | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
240 let restrict_universe query =
242 [] -> query (* no constraints ===> the universe is the library *)
245 (*CSC: Usare tante Union e Pattern per fare un insieme di uri mi *)
246 (*CSC: sembra un poco penoso. Inoltre creo un albero completamente *)
247 (*CSC: sbilanciato, aumentando il costo della risoluzione della *)
249 let rec compose_universe =
252 | [uri] -> MQPattern uri
253 | uri::tl -> MQUnion(MQPattern uri, compose_universe tl)
255 compose_universe !universe
262 MQUsedBy (MQRVarOccur "uri", "pos"),
264 MQIs (MQSVar "pos", MQConclusion),
265 MQIs (MQSVar "pos", MQMConclusion)
273 let build_result query =
274 let html = par () ^ out_query query ^ nl () in
275 let result = Mqint.execute query in
276 save (html ^ out_result result)
278 let init = Mqint.init
280 let close = Mqint.close
284 MQList (MQSelect ("ref",
285 MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None)),
286 MQIs (MQFunc (MQName, "ref"),
297 let uil = inspect t in
298 let til = List.map tie_uie uil in
299 let query = build_inter 0 til in
300 let query' = restrict_universe query til in
301 let query'' = MQList query' in
302 par () ^ out_il uil ^ build_result query''