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 ")"
74 let rec out_list = function
75 | MQSelect (r, l, b) ->
76 key "select" ^ out_rvar r ^ key "in" ^ out_list l ^ key "where" ^ out_bool b
77 | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v
78 | MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ key "position" ^ out_svar v
79 | MQPattern p -> key "pattern" ^ out_pat p
80 | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
81 | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"
84 let out_query = function
85 | MQList l -> out_list l
87 (* HTML representation of a query result *)
89 let rec out_list = function
91 | u :: l -> res (str_tref u) ^ nl () ^ out_list l
94 par () ^ "Result:" ^ nl () ^
96 | MQRefs l -> out_list l
98 (* Converting functions *)
102 let i = Str.search_forward (Str.regexp_string ":/") s 0 in
103 let p = Str.string_before s i in
104 let q = Str.string_after s (i + 2) in
109 let encode = function
110 | Str.Text s -> MQString s
112 if s = "?" then MQAnyChr else
113 if s = "*" then MQAst else
114 if s = "**" then MQAstAst else
115 if s = "/" then MQSlash else MQString s
117 let tref_uref (u, i) =
118 let s = UriManager.string_of_uri u in
121 let rx = Str.regexp "\?\|\*\*\|\*\|/" in
122 let l = Str.full_split rx q in
123 (p, List.map encode l, i)
125 (* CIC term inspecting functions *)
127 let out_ie (r, b, v) =
128 let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
129 res (pos ^ str_uref r) ^ nl () ^
130 con (pos ^ str_tref (tref_uref r)) ^ nl ()
132 let rec out_il = function
134 | head :: tail -> out_ie head ^ out_il tail
136 let tie_uie (r, b, v) = (tref_uref r, b, v)
138 let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) =
139 UriManager.eq u1 u2 && f1 = f2 && b1 = b2
141 let rec ie_insert ie = function
144 head :: if ie_eq head ie then tail else ie_insert ie tail
148 let inspect_uri main l uri t c v =
149 if v > !level then l else
152 | (None, _) -> (None, None)
153 | (Some t0, c0) -> (Some (t0 + 1), c0)
155 ie_insert ((uri, fi), main, v) l
157 let rec inspect_term main l v = function
163 | Var u -> inspect_uri main l u None None v
164 | Const (u, i) -> inspect_uri main l u None None v
165 | MutInd (u, i, t) -> inspect_uri main l u (Some t) None v
166 | MutConstruct (u, i, t, c) -> inspect_uri main l u (Some t) (Some c) v
168 let luu = inspect_term main l (v + 1) uu in
169 inspect_term false luu (v + 1) tt
170 | Prod (n, uu, tt) ->
171 let luu = inspect_term false l (v + 1) uu in
172 inspect_term false luu (v + 1) tt
173 | Lambda (n, uu, tt) ->
174 let luu = inspect_term false l (v + 1) uu in
175 inspect_term false luu (v + 1) tt
176 | LetIn (n, uu, tt) ->
177 let luu = inspect_term false l (v + 1) uu in
178 inspect_term false luu (v + 1) tt
179 | Appl m -> inspect_list main l (v + 1) m
180 | MutCase (u, i, t, tt, uu, m) ->
181 let lu = inspect_uri main l u (Some t) None (v + 1) in
182 let ltt = inspect_term false lu (v + 1) tt in
183 let luu = inspect_term false ltt (v + 1) uu in
184 inspect_list main luu (v + 1) m
185 | Fix (i, m) -> inspect_ind l (v + 1) m
186 | CoFix (i, m) -> inspect_coind l (v + 1) m
187 and inspect_list main l v = function
190 let ltt = inspect_term main l v tt in
191 inspect_list false ltt v m
192 and inspect_ind l v = function
194 | (n, i, tt, uu) :: m ->
195 let ltt = inspect_term false l v tt in
196 let luu = inspect_term false ltt v uu in
198 and inspect_coind l v = function
200 | (n, tt, uu) :: m ->
201 let ltt = inspect_term false l v tt in
202 let luu = inspect_term false ltt v uu in
203 inspect_coind luu v m
205 let inspect t = inspect_term true [] 0 t
207 (* query building functions *)
210 let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
211 (64 * 6 + 8 * 6 + 4) "mquery.htm" in
212 output_string och s; flush och; s
214 let build_select (r, b, v) n =
215 let rvar = "ref" ^ string_of_int n in
216 let svar = "str" ^ string_of_int n in
217 let mqs = if b then MQMConclusion else MQConclusion in
219 MQUse (MQPattern r, svar),
220 MQIs (MQSVar svar, mqs)
223 let rec build_inter n = function
224 | [] -> MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None))
225 | [ie] -> build_select ie n
226 | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
228 let build_result query =
229 let html = par () ^ out_query query ^ nl () in
230 let result = Mqint.execute query in
231 save (html ^ out_result result)
233 let init = Mqint.init
235 let close = Mqint.close
239 MQList (MQSelect ("ref",
240 MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None)),
241 MQIs (MQFunc (MQName, "ref"),
251 let uil = inspect t in
252 let til = List.map tie_uie uil in
253 let query = MQList (build_inter 0 til) in
254 par () ^ out_il uil ^ build_result query