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
22 MQFC n -> string_of_int n
29 | (Some t, None) -> "#1/" ^ string_of_int t
30 | (Some t, Some c) -> "#1/" ^ string_of_int t ^ "/" ^ string_of_int c
32 let str_tref (p, u, i) =
38 p ^ ":/" ^ str_up u ^ str_fi i
41 UriManager.string_of_uri u ^ str_fi i
43 (* raw HTML representation *)
45 let key s = "<font color=\"blue\">" ^ s ^ " </font>"
51 let con s = "<font color=\"red\">\"" ^ s ^ "\" </font>"
53 let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
59 (* HTML representation of a query *)
61 let out_rvar s = sym s
63 let out_svar s = sep "$" ^ sym s
65 let out_tref r = con (str_tref r)
67 let out_pat p = out_tref p
69 let out_func = function
70 | MQName -> key "name"
73 let out_str = function
75 | MQRVar s -> out_rvar s
76 | MQSVar s -> out_svar s
77 | MQFunc (f, r) -> out_func f ^ out_rvar r
78 | MQMConclusion -> key "mainconclusion"
79 | MQConclusion -> key "conclusion"
81 let rec out_bool = function
82 | MQTrue -> key "true"
83 | MQFalse -> key "false"
84 | MQIs (s, t) -> out_str s ^ key "is" ^ out_str t
85 | MQNot b -> key "not" ^ out_bool b
86 | MQAnd (b1, b2) -> sep "(" ^ out_bool b1 ^ key "and" ^ out_bool b2 ^ sep ")"
87 | MQOr (b1, b2) -> sep "(" ^ out_bool b1 ^ key "or" ^ out_bool b2 ^ sep ")"
88 | MQSetEqual (l1, l2) ->
89 sep "(" ^ out_list l1 ^ key "setequal" ^ out_list l2 ^ sep ")"
90 | MQSubset (l1, l2) ->
91 sep "(" ^ out_list l1 ^ key "subset" ^ out_list l2 ^ sep ")"
93 and out_list = function
94 | MQSelect (r, l, b) ->
95 key "select" ^ out_rvar r ^ key "in" ^ out_list l ^ key "where" ^ out_bool b
96 | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v
97 | MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ key "position" ^ out_svar v
98 | MQPattern p -> key "pattern" ^ out_pat p
99 | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
100 | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"
101 | MQRVarOccur v -> key "rvaroccur" ^ v
103 let out_query = function
104 | MQList l -> out_list l
106 (* HTML representation of a query result *)
108 let rec out_list = function
110 | u :: l -> res u ^ nl () ^ out_list l
113 par () ^ "Result:" ^ nl () ^
115 | MQRefs l -> out_list l
117 (* Converting functions *)
121 let i = Str.search_forward (Str.regexp_string ":/") s 0 in
122 let p = Str.string_before s i in
123 let q = Str.string_after s (i + 2) in
128 let encode = function
129 | Str.Text s -> MQBC s
131 if s = "?" then MQBQ else
132 if s = "*" then MQBS else
133 if s = "**" then MQBSS else
134 if s = "/" then MQBD else MQBC s
136 let tref_uref (u, i) =
137 let s = UriManager.string_of_uri u in
140 let rx = Str.regexp "\?\|\*\*\|\*\|/" in
141 let l = Str.full_split rx q in
142 (Some p, List.map encode l, i)
144 (* CIC term inspecting functions *)
146 let out_ie (r, b, v) =
147 let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
148 res (pos ^ str_uref r) ^ nl () ^
149 con (pos ^ str_tref (tref_uref r)) ^ nl ()
151 let rec out_il = function
153 | head :: tail -> out_ie head ^ out_il tail
155 let tie_uie (r, b, v) = (tref_uref r, b, v)
157 let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) =
158 UriManager.eq u1 u2 && f1 = f2 && b1 = b2
160 let rec ie_insert ie = function
163 head :: if ie_eq head ie then tail else ie_insert ie tail
167 (*CSC: che brutto il codice imperativo!!!*)
168 let universe = ref [];;
170 let inspect_uri main l uri t c v =
174 | (Some t0, Some c0) -> [MQFC (t0 + 1); MQFC c0]
175 | (Some t0, None) -> [MQFC (t0 + 1)]
177 (*CSC: sbagliato, credo. MQString non dovrebbe poter contenere slash *)
178 universe := (tref_uref (uri,fi))::!universe ;
182 ie_insert ((uri, fi), main, v) l
185 let rec inspect_term main l v = function
190 | Var u -> inspect_uri main l u None None v
191 | Const (u, i) -> inspect_uri main l u None None v
192 | MutInd (u, i, t) -> inspect_uri main l u (Some t) None v
193 | MutConstruct (u, i, t, c) -> inspect_uri main l u (Some t) (Some c) v
195 (*CSC: Cast modified so that it behaves exactly as if no Cast was there *)
196 inspect_term main l v uu
197 | Prod (n, uu, tt) ->
198 let luu = inspect_term false l (v + 1) uu in
199 inspect_term false luu (v + 1) tt
200 | Lambda (n, uu, tt) ->
201 let luu = inspect_term false l (v + 1) uu in
202 inspect_term false luu (v + 1) tt
203 | LetIn (n, uu, tt) ->
204 let luu = inspect_term false l (v + 1) uu in
205 inspect_term false luu (v + 1) tt
206 | Appl m -> inspect_list main l true v m
207 | MutCase (u, i, t, tt, uu, m) ->
208 let lu = inspect_uri main l u (Some t) None (v + 1) in
209 let ltt = inspect_term false lu (v + 1) tt in
210 let luu = inspect_term false ltt (v + 1) uu in
211 inspect_list main luu false (v + 1) m
212 | Fix (i, m) -> inspect_ind l (v + 1) m
213 | CoFix (i, m) -> inspect_coind l (v + 1) m
214 and inspect_list main l head v = function
217 let ltt = inspect_term main l (if head then v else v+1) tt in
218 inspect_list false ltt false v m
219 and inspect_ind l v = function
221 | (n, i, tt, uu) :: m ->
222 let ltt = inspect_term false l v tt in
223 let luu = inspect_term false ltt v uu in
225 and inspect_coind l v = function
227 | (n, tt, uu) :: m ->
228 let ltt = inspect_term false l v tt in
229 let luu = inspect_term false ltt v uu in
230 inspect_coind luu v m
232 let inspect t = inspect_term true [] 0 t
234 (* query building functions *)
237 let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
238 (64 * 6 + 8 * 6 + 4) "mquery.htm" in
239 output_string och s; flush och; s
241 let build_select (r, b, v) n =
242 let rvar = "ref" ^ string_of_int n in
243 let svar = "str" ^ string_of_int n in
244 let mqs = if b then MQMConclusion else MQConclusion in
246 MQUse (MQPattern r, svar),
247 MQIs (MQSVar svar, mqs)
250 let rec build_inter n = function
251 | [] -> MQPattern (Some "cic", [MQBSS; MQBC ".con"], [])
252 | [ie] -> build_select ie n
253 | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
255 let restrict_universe query =
257 [] -> query (* no constraints ===> the universe is the library *)
260 (*CSC: Usare tante Union e Pattern per fare un insieme di uri mi *)
261 (*CSC: sembra un poco penoso. Inoltre creo un albero completamente *)
262 (*CSC: sbilanciato, aumentando il costo della risoluzione della *)
264 let rec compose_universe =
267 | [uri] -> MQPattern uri
268 | uri::tl -> MQUnion(MQPattern uri, compose_universe tl)
270 compose_universe !universe
277 MQUsedBy (MQRVarOccur "uri", "pos"),
279 MQIs (MQSVar "pos", MQConclusion),
280 MQIs (MQSVar "pos", MQMConclusion)
288 let build_result query =
289 let html = par () ^ out_query query ^ nl () in
290 let result = Mqint.execute query in
291 save (html ^ out_result result)
293 let init = Mqint.init
295 let close = Mqint.close
299 MQList (MQSelect ("ref",
300 MQPattern (Some "cic", [MQBSS ; MQBC ".con"], []),
301 MQIs (MQFunc (MQName, "ref"),
312 let uil = inspect t in
313 let til = List.map tie_uie uil in
314 let query = build_inter 0 til in
315 let query' = restrict_universe query til in
316 let query'' = MQList query' in
317 par () ^ out_il uil ^ build_result query''