1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Ferruccio Guidi <fguidi@cs.unibo.it> *)
34 (******************************************************************************)
39 (* string linearization of a reference *)
41 let str_uptoken = function
48 let rec str_up = function
50 | head :: tail -> str_uptoken head ^ str_up tail
54 | (Some t, None) -> "#1/" ^ string_of_int t
55 | (Some t, Some c) -> "#1/" ^ string_of_int t ^ "/" ^ string_of_int c
57 let str_tref (p, u, x, i) =
58 p ^ ":/" ^ str_up u ^ "." ^ x ^ str_fi i
61 UriManager.string_of_uri u ^ str_fi i
63 (* raw HTML representation *)
65 let key s = "<font color=\"blue\">" ^ s ^ " </font>"
71 let con s = "<font color=\"red\">\"" ^ s ^ "\" </font>"
73 let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
79 (* HTML representation of a query *)
81 let out_rvar s = sym s
83 let out_svar s = sep "$" ^ sym s
85 let out_tref r = con (str_tref r)
87 let out_pat p = out_tref p
89 let out_func = function
90 | MQName -> key "name"
92 let out_str = function
94 | MQRVar s -> out_rvar s
95 | MQSVar s -> out_svar s
96 | MQFunc (f, r) -> out_func f ^ out_rvar r
97 | MQMConclusion -> key "mainconclusion"
98 | MQConclusion -> key "conclusion"
100 let rec out_bool = function
101 | MQTrue -> key "true"
102 | MQFalse -> key "false"
103 | MQIs (s, t) -> out_str s ^ key "is" ^ out_str t
104 | MQNot b -> key "not" ^ out_bool b
105 | MQAnd (b1, b2) -> sep "(" ^ out_bool b1 ^ key "and" ^ out_bool b2 ^ sep ")"
106 | MQOr (b1, b2) -> sep "(" ^ out_bool b1 ^ key "or" ^ out_bool b2 ^ sep ")"
108 let rec out_list = function
109 | MQSelect (r, l, b) ->
110 key "select" ^ out_rvar r ^ key "in" ^ out_list l ^ key "where" ^ out_bool b
111 | MQUse (l, v) -> key "use" ^ out_list l ^ key "position" ^ out_svar v
112 | MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ key "position" ^ out_svar v
113 | MQPattern p -> key "pattern" ^ out_pat p
114 | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
115 | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"
117 let out_query = function
118 | MQList l -> out_list l
120 (* HTML representation of a query result *)
122 let rec out_list = function
124 | u :: l -> res u ^ nl () ^ out_list l
127 par () ^ "Result:" ^ nl () ^
129 | MQRefs l -> out_list l
131 (* Converting functions *)
135 let i = Str.search_forward (Str.regexp_string ":/") s 0 in
136 let p = Str.string_before s i in
137 let q = Str.string_after s (i + 2) in
139 let j = String.rindex q '.' in
140 (p, Str.string_before q j, Str.string_after q (j + 1))
142 Not_found -> (p, q, "")
144 Not_found -> (s, "", "")
146 let encode = function
147 | Str.Text s -> MQString s
149 if s = "?" then MQAnyChr else
150 if s = "*" then MQAst else
151 if s = "**" then MQAstAst else
152 if s = "/" then MQSlash else MQString s
154 let tref_uref (u, i) =
155 let s = UriManager.string_of_uri u in
158 let rx = Str.regexp "\?\|\*\*\|\*\|/" in
159 let l = Str.full_split rx q in
160 (p, List.map encode l, r, i)
162 (* CIC term inspecting functions *)
164 let out_ie (r, b, v) =
165 let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
166 res (pos ^ str_uref r) ^ nl () ^
167 con (pos ^ str_tref (tref_uref r)) ^ nl ()
169 let rec out_il = function
171 | head :: tail -> out_ie head ^ out_il tail
173 let tie_uie (r, b, v) = (tref_uref r, b, v)
175 let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) =
176 UriManager.eq u1 u2 && f1 = f2 && b1 = b2
178 let rec ie_insert ie = function
181 head :: if ie_eq head ie then tail else ie_insert ie tail
185 let inspect_uri main l uri t c v =
186 if v > !level then l else
189 | (None, _) -> (None, None)
190 | (Some t0, c0) -> (Some (t0 + 1), c0)
192 ie_insert ((uri, fi), main, v) l
194 let rec inspect_term main l v = function
200 | Var u -> inspect_uri main l u None None v
201 | Const (u, i) -> inspect_uri main l u None None v
202 | MutInd (u, i, t) -> inspect_uri main l u (Some t) None v
203 | MutConstruct (u, i, t, c) -> inspect_uri main l u (Some t) (Some c) v
205 let luu = inspect_term main l (v + 1) uu in
206 inspect_term false luu (v + 1) tt
207 | Prod (n, uu, tt) ->
208 let luu = inspect_term false l (v + 1) uu in
209 inspect_term false luu (v + 1) tt
210 | Lambda (n, uu, tt) ->
211 let luu = inspect_term false l (v + 1) uu in
212 inspect_term false luu (v + 1) tt
213 | LetIn (n, uu, tt) ->
214 let luu = inspect_term false l (v + 1) uu in
215 inspect_term false luu (v + 1) tt
216 | Appl m -> inspect_list main l (v + 1) m
217 | MutCase (u, i, t, tt, uu, m) ->
218 let lu = inspect_uri main l u (Some t) None (v + 1) in
219 let ltt = inspect_term false lu (v + 1) tt in
220 let luu = inspect_term false ltt (v + 1) uu in
221 inspect_list main luu (v + 1) m
222 | Fix (i, m) -> inspect_ind l (v + 1) m
223 | CoFix (i, m) -> inspect_coind l (v + 1) m
224 and inspect_list main l v = function
227 let ltt = inspect_term main l v tt in
228 inspect_list false ltt v m
229 and inspect_ind l v = function
231 | (n, i, tt, uu) :: m ->
232 let ltt = inspect_term false l v tt in
233 let luu = inspect_term false ltt v uu in
235 and inspect_coind l v = function
237 | (n, tt, uu) :: m ->
238 let ltt = inspect_term false l v tt in
239 let luu = inspect_term false ltt v uu in
240 inspect_coind luu v m
242 let inspect t = inspect_term true [] 0 t
244 (* query building functions *)
247 let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
248 (64 * 6 + 8 * 6 + 4) "mquery.htm" in
249 output_string och s; flush och; s
251 let build_select (r, b, v) n =
252 let rvar = "ref" ^ string_of_int n in
253 let svar = "str" ^ string_of_int n in
254 let mqs = if b then MQMConclusion else MQConclusion in
256 MQUse (MQPattern r, svar),
257 MQIs (MQSVar svar, mqs)
260 let rec build_inter n = function
261 | [] -> MQPattern ("cic", [MQAstAst], "con", (None, None))
262 | [ie] -> build_select ie n
263 | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
265 let build_result query =
266 let html = par () ^ out_query query ^ nl () in
267 let result = Mqint.execute query in
268 save (html ^ out_result result)
270 let init = Mqint.init
272 let close = Mqint.close
276 MQList (MQSelect ("ref",
277 MQPattern ("cic", [MQAstAst], "con", (None, None)),
278 MQIs (MQFunc (MQName, "ref"),
288 let uil = inspect t in
289 let til = List.map tie_uie uil in
290 let query = MQList (build_inter 0 til) in
291 par () ^ out_il uil ^ build_result query