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 (******************************************************************************)
41 (* CIC term inspecting functions ********************************************)
43 let env = ref [] (* metasemv *)
44 let cont = ref [] (* context *)
46 let ie_out (r, b, v) =
47 let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
48 res (pos ^ str_uref r) ^ nl ()
49 (* FG: si puo' usare xp_str_uref se si vuole xpointer *)
51 let rec il_out = function
53 | head :: tail -> ie_out head ^ il_out tail
55 let rec il_max = function
57 | (_, _, v) :: tail ->
58 let v0 = il_max tail in
59 if v > v0 then v else v0
61 let ie_str_uri (u, b, v) = xp_str_uref u
63 let rec il_restrict level = function
65 | (u, b, v) :: tail ->
66 if v <= level then (u, b, v) :: il_restrict level tail
67 else il_restrict level tail
69 let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) =
70 UriManager.eq u1 u2 && f1 = f2 && b1 = b2
72 let rec ie_insert ie = function
75 head :: if ie_eq head ie then tail else ie_insert ie tail
78 let u0 = CicTypeChecker.type_of_aux' !env !cont t in
79 let u = CicReduction.whd !cont u0 in
80 let rec deg = function
82 | Cast (uu, _) -> deg uu
83 | Prod (_, _, tt) -> deg tt
87 let inspect_uri main l uri tc v term =
88 let d = degree term in
89 let fi = match tc with
90 | t0 :: c0 :: _ -> [t0 + 1; c0]
93 in ie_insert ((uri, fi), main, 2 * v + d - 1) l
95 let rec inspect_term main l v term =
101 | Var u -> inspect_uri main l u [] v term
102 | Const (u, _) -> inspect_uri main l u [] v term
103 | MutInd (u, _, t) -> inspect_uri main l u [t] v term
104 | MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term
106 inspect_term main l v uu
107 | Prod (_, uu, tt) ->
108 let luu = inspect_term false l (v + 1) uu in
109 inspect_term main luu (v + 1) tt
110 | Lambda (_, uu, tt) ->
111 let luu = inspect_term false l (v + 1) uu in
112 inspect_term false luu (v + 1) tt
113 | LetIn (_, uu, tt) ->
114 let luu = inspect_term false l (v + 1) uu in
115 inspect_term false luu (v + 1) tt
116 | Appl m -> inspect_list main l true v m
117 | MutCase (u, _, t, tt, uu, m) ->
118 let lu = inspect_uri main l u [t] (v + 1) term in
119 let ltt = inspect_term false lu (v + 1) tt in
120 let luu = inspect_term false ltt (v + 1) uu in
121 inspect_list main luu false (v + 1) m
122 | Fix (_, m) -> inspect_ind l (v + 1) m
123 | CoFix (_, m) -> inspect_coind l (v + 1) m
124 and inspect_list main l head v = function
127 let ltt = inspect_term main l (if head then v else v + 1) tt in
128 inspect_list false ltt false v m
129 and inspect_ind l v = function
131 | (_, _, tt, uu) :: m ->
132 let ltt = inspect_term false l v tt in
133 let luu = inspect_term false ltt v uu in
135 and inspect_coind l v = function
137 | (_, tt, uu) :: m ->
138 let ltt = inspect_term false l v tt in
139 let luu = inspect_term false ltt v uu in
140 inspect_coind luu v m
142 let rec inspect_backbone = function
143 | Cast (uu, _) -> inspect_backbone uu
144 | Prod (_, _, tt) -> inspect_backbone tt
145 | LetIn (_, uu, tt) -> inspect_backbone tt
146 | t -> inspect_term true [] 0 t
148 let inspect t = inspect_backbone t
150 (* query building functions *************************************************)
152 let issue = ref (fun _ -> true)
155 let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
156 (64 * 6 + 8 * 6 + 4) "MQGenLog.htm" in
157 output_string och s; flush och; s
159 let build_result query =
160 if ! issue query then
161 let html = par () ^ out_query query ^ nl () in
162 let result = Mqint.execute query in
163 result, save (html ^ out_result result)
166 let build_select (r, b, v) n =
167 let rvar = "ref" ^ string_of_int n in
168 let svar = "str" ^ string_of_int n in
169 let mqs = if b then MQMConclusion else MQConclusion in
171 MQUse (MQReference [xp_str_uref r], svar),
172 MQIs (MQStringSVar svar, mqs)
175 let rec build_inter n = function
176 | [] -> MQPattern (None, [MQBSS], [MQFSS])
177 | [ie] -> build_select ie n
178 | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il)
180 let restrict_universe query =
182 [] -> query (* no constraints ===> the universe is the library *)
185 MQReference (List.map ie_str_uri l)
188 "universe", universe,
194 MQUsedBy (MQListRVar "uri", "pos"),
196 MQIs (MQStringSVar "pos", MQConclusion),
197 MQIs (MQStringSVar "pos", MQMConclusion)
200 MQListLVar "universe"
205 let init = Mqint.init
207 let close = Mqint.close
210 (*CSC: next query to be fixed
211 1) I am exploiting the bug that does not quote '|'
212 2) I am searching only constants and mutual inductive definition blocks
213 (i.e. no fragment identifier at all)
215 MQList (MQSelect ("ref",
216 MQPattern (Some "cic", [MQBSS ; MQBC ".con|.ind"],[]),
217 MQIs (MQFunc (MQName, "ref"),
224 let MQRefs uris, html = build_result (locate_query s) in
225 (*CSC: here I am mapping .ind URIs to .ind#1/1, i.e. the first type of *)
226 (*CSC: the mutual inductive block. It must be removed once the query *)
227 (*CSC: works reasonably. *)
231 if String.sub uri (String.length uri - 4) 4 = ".ind" then
241 let il = inspect t in
242 par () ^ il_out il ^ nl ()
247 let backward e c t level =
248 let t0 = Sys.time () in
250 let il = inspect t in
251 let query = build_inter 0 (il_restrict level il) in
252 let query' = restrict_universe query il in
253 let query'' = MQList query' in
254 let res = build_result query'' in
258 print_endline ("GEN = " ^ string_of_int (List.length il) ^ ":" ^
259 string_of_float (Sys.time () -. t0) ^ "s");
260 r, par () ^ il_out il ^ html