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 | MQPattern p -> key "pattern" ^ out_pat p
113 | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")"
114 | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")"
116 let out_query = function
117 | MQList l -> out_list l
119 (* Converting functions *)
123 let i = Str.search_forward (Str.regexp_string ":/") s 0 in
124 let p = Str.string_before s i in
125 let q = Str.string_after s (i + 2) in
127 let j = String.rindex q '.' in
128 (p, Str.string_before q j, Str.string_after q (j + 1))
130 Not_found -> (p, q, "")
132 Not_found -> (s, "", "")
134 let encode = function
135 | Str.Text s -> MQString s
137 if s = "?" then MQAnyChr else
138 if s = "*" then MQAst else
139 if s = "**" then MQAstAst else
140 if s = "/" then MQSlash else MQString s
142 let tref_uref (u, i) =
143 let s = UriManager.string_of_uri u in
146 let rx = Str.regexp "\?\|\*\*\|\*\|/" in
147 let l = Str.full_split rx q in
148 (p, List.map encode l, r, i)
150 (* CIC term inspecting functions *)
153 let pos = if b then "HEAD: " else "TAIL: " in
154 res (pos ^ str_uref r) ^ nl ^
155 con (pos ^ str_tref (tref_uref r)) ^ nl
157 let rec out_il = function
159 | head :: tail -> out_ie head ^ out_il tail
161 let tie_uie (r, b) = (tref_uref r, b)
163 let ie_eq ((u1, f1), b1) ((u2, f2), b2) =
164 UriManager.eq u1 u2 && f1 = f2 && b1 = b2
166 let rec ie_insert ie = function
169 head :: if ie_eq head ie then tail else ie_insert ie tail
171 let inspect_uri main l uri t c =
174 | (None, _) -> (None, None)
175 | (Some t0, c0) -> (Some (t0 + 1), c0)
177 ie_insert ((uri, fi), main) l
179 let rec inspect_term main l = function
185 | Var u -> inspect_uri main l u None None
186 | Const (u, i) -> inspect_uri main l u None None
187 | MutInd (u, i, t) -> inspect_uri main l u (Some t) None
188 | MutConstruct (u, i, t, c) -> inspect_uri main l u (Some t) (Some c)
190 let luu = inspect_term main l uu in
191 inspect_term false luu tt
192 | Prod (n, uu, tt) ->
193 let luu = inspect_term false l uu in
194 inspect_term false luu tt
195 | Lambda (n, uu, tt) ->
196 let luu = inspect_term false l uu in
197 inspect_term false luu tt
198 | LetIn (n, uu, tt) ->
199 let luu = inspect_term false l uu in
200 inspect_term false luu tt
201 | Appl m -> inspect_list main l m
202 | MutCase (u, i, t, tt, uu, m) ->
203 let lu = inspect_uri main l u (Some t) None in
204 let ltt = inspect_term false lu tt in
205 let luu = inspect_term false ltt uu in
206 inspect_list main luu m
207 | Fix (i, m) -> inspect_ind l m
208 | CoFix (i, m) -> inspect_coind l m
209 and inspect_list main l = function
212 let ltt = inspect_term main l tt in
213 inspect_list false ltt m
214 and inspect_ind l = function
216 | (n, i, tt, uu) :: m ->
217 let ltt = inspect_term false l tt in
218 let luu = inspect_term false ltt uu in
220 and inspect_coind l = function
222 | (n, tt, uu) :: m ->
223 let ltt = inspect_term false l tt in
224 let luu = inspect_term false ltt uu in
227 let inspect t = inspect_term true [] t
229 (* query building functions *)
231 let build_select (r, b) n =
232 let rvar = "uri" ^ string_of_int n in
233 let svar = "s" ^ string_of_int n in
234 let mqs = if b then MQMConclusion else MQConclusion in
236 MQUse (MQPattern r, svar),
237 MQIs (MQSVar svar, mqs)
240 let rec build_inter n = function
241 | [] -> MQPattern ("cic", [MQAstAst], "con", (None, None))
242 | [ie] -> build_select ie n
243 | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
248 MQList (MQSelect ("uri",
249 MQPattern ("cic", [MQAstAst], "con", (None, None)),
250 MQIs (MQFunc (MQName, "uri"),
256 match Mqint.execute query with
258 out_query query ^ nl ^ "Result: " ^ nl ^
259 String.concat nl l ^ nl
260 | MQRefs _ -> assert false (*CSC: ????????????????????????????? *)
262 match Str.split (Str.regexp "[ \t]+") s with
264 | head :: tail -> par ^ locate_aux head
268 let uil = inspect t in
269 let til = List.map tie_uie uil in
270 let query = MQList (build_inter 0 til) in
271 match Mqint.execute query with
273 par ^ out_query query ^ nl ^ (* ^ par ^ out_il uil ^ *)
274 "Result: " ^ nl ^ String.concat nl l ^ nl
275 | MQRefs _ -> assert false (*CSC: ????????????????????????????? *)
278 let init = Mqint.init;;
279 let close = Mqint.close;;