1 (* Copyright (C) 2004, 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://helm.cs.unibo.it/
28 let nonvar uri = not (UriManager.uri_is_var uri)
30 module Constr = MetadataConstraints
32 exception Goal_is_not_an_equation
35 let debug_print s = if debug then prerr_endline (Lazy.force s)
37 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
39 let signature_of_hypothesis context =
44 | Some (_, Cic.Decl t)
45 | Some (_, Cic.Def (t, _)) ->
46 Constr.UriManagerSet.union set (Constr.constants_of t))
47 Constr.UriManagerSet.empty context
49 let intersect uris siguris =
50 let set1 = List.fold_right Constr.UriManagerSet.add uris Constr.UriManagerSet.empty in
52 List.fold_right Constr.UriManagerSet.add siguris Constr.UriManagerSet.empty
54 let inter = Constr.UriManagerSet.inter set1 set2 in
55 List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
59 let profiler = CicUtil.profile "at_most" in
60 fun ~dbd ~where uri -> profiler.profile (Constr.at_most ~dbd ~where) uri
63 let profiler = CicUtil.profile "sigmatch" in
64 fun ~dbd ~facts ~where signature ->
65 profiler.profile (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
67 let at_most = Constr.at_most
68 let sigmatch = MetadataConstraints.sigmatch
70 let filter_uris_forward ~dbd (main, constants) uris =
74 | Some (main, types) -> main :: types
77 List.fold_right Constr.UriManagerSet.add main_uris constants
79 List.filter (at_most ~dbd ~where:`Statement full_signature) uris
81 let filter_uris_backward ~dbd ~facts signature uris =
84 (sigmatch ~dbd ~facts ~where:`Statement signature)
86 intersect uris siguris
88 let compare_goal_list proof goal1 goal2 =
89 let _,metasenv,_,_ = proof in
90 let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
91 let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
93 CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph
96 CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph
100 CicReduction.are_convertible
101 ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.empty_ugraph
108 CicReduction.are_convertible
109 ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.empty_ugraph
116 (* experimental_hint is a version of hint for experimental
117 purposes. It uses auto_tac_verbose instead of auto tac.
118 Auto_tac verbose also returns a substitution - for the moment
119 as a function from cic to cic, to be changed into an association
120 list in the future -. This substitution is used to build a
121 hash table of the inspected goals with their associated proofs.
122 The cose is a cut and paste of the previous one: at the end
123 of the experimentation we shall make a choice. *)
125 let close_with_types s metasenv context =
126 Constr.UriManagerSet.fold
128 let t = CicUtil.term_of_uri e in
130 CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph
132 Constr.UriManagerSet.union bag (Constr.constants_of ty))
135 let close_with_constructors s metasenv context =
136 Constr.UriManagerSet.fold
138 let t = CicUtil.term_of_uri e in
141 | Cic.MutConstruct (uri,_,_,_) ->
142 (match fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
143 Cic.InductiveDefinition(tl,_,_,_) ->
146 (fun (i,s) (_,_,_,cl) ->
150 let curi = UriManager.uri_of_uriref uri i (Some j) in
151 j+1,Constr.UriManagerSet.add curi s) (1,s) cl in
158 let apply_tac_verbose =
159 let profiler = CicUtil.profile "apply_tac_verbose" in
160 fun ~term status -> profiler.profile (PrimitiveTactics.apply_tac_verbose ~term) status
163 let profiler = CicUtil.profile "sigmatch" in
164 fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler.profile (Constr.sigmatch ~dbd ~facts ~where) signature
167 let profiler = CicUtil.profile "cmatch'" in
168 fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature
170 let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
171 let cmatch' = Constr.cmatch'
173 let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
174 let (_, metasenv, _, _) = proof in
175 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
176 let main, sig_constants = Constr.signature_of ty in
177 let set = signature_of_hypothesis context in
182 List.fold_right Constr.UriManagerSet.add (main::l) set in
183 let set = Constr.UriManagerSet.union set sig_constants in
184 let all_constants_closed = close_with_types set metasenv context in
186 sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) in
187 let uris = List.filter nonvar (List.map snd uris) in
188 let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
191 let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
192 (* let to_string set =
195 (Constr.UriManagerSet.fold
196 (fun u l -> (UriManager.string_of_uri u)::l) set []))
199 let (_, metasenv, _, _) = proof in
200 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
201 let main, sig_constants = Constr.signature_of ty in
202 (* Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *)
203 (* match main with *)
204 (* None -> raise Goal_is_not_an_equation *)
205 (* | Some (m,l) -> *)
208 let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
209 UriManager.uri_of_string (us ^ "#xpointer(1/1)")
213 | Some (m, l) when UriManager.eq m eq_URI -> m, l
214 | Some (m, l) -> eq_URI, []
216 Printf.printf "\nSome (m, l): %s, [%s]\n\n"
217 (UriManager.string_of_uri m)
218 (String.concat "; " (List.map UriManager.string_of_uri l));
219 (* if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
220 let set = signature_of_hypothesis context in
221 (* Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
222 let set = Constr.UriManagerSet.union set sig_constants in
223 let set = close_with_types set metasenv context in
224 (* Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
225 let set = close_with_constructors set metasenv context in
226 (* Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
227 let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in
229 sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
230 let uris = List.filter nonvar (List.map snd uris) in
231 let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
234 (* else raise Goal_is_not_an_equation *)
236 let experimental_hint
237 ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
238 let (_, metasenv, _, _) = proof in
239 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
240 let (uris, (main, sig_constants)) =
243 (sigmatch ~dbd ~facts signature, signature)
245 (cmatch' ~dbd ~facts ty, Constr.signature_of ty)
247 let uris = List.filter nonvar (List.map snd uris) in
248 let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
249 let types_constants =
251 | None -> Constr.UriManagerSet.empty
252 | Some (main, types) ->
253 List.fold_right Constr.UriManagerSet.add (main :: types)
254 Constr.UriManagerSet.empty
258 Constr.UriManagerSet.union
259 (signature_of_hypothesis context)
264 | None -> Constr.UriManagerSet.empty
267 CicTypeChecker.type_of_aux'
268 metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
270 Constr.constants_of ty
272 Constr.UriManagerSet.union main hyp_and_sug
274 (* Constr.UriManagerSet.iter debug_print hyp_constants; *)
275 let all_constants_closed = close_with_types all_constants metasenv context in
276 let other_constants =
277 Constr.UriManagerSet.diff all_constants_closed types_constants
279 debug_print (lazy "all_constants_closed");
280 if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) all_constants_closed;
281 debug_print (lazy "other_constants");
282 if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) other_constants;
284 let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in
285 if ((List.length uris < pow) or (pow <= 0))
287 debug_print (lazy "MetadataQuery: large sig, falling back to old method");
288 filter_uris_forward ~dbd (main, other_constants) uris
290 filter_uris_backward ~dbd ~facts (main, other_constants) uris
292 let rec aux = function
297 let (subst,(proof, goal_list)) =
298 (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
300 ~term:(CicUtil.term_of_uri uri)
304 List.stable_sort (compare_goal_list proof) goal_list
306 Some (uri, (subst,(proof, goal_list)))
307 with ProofEngineTypes.Fail _ -> None
311 | Some status' -> status' :: aux tl)
314 (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
315 Pervasives.compare (List.length goals1) (List.length goals2))
318 let new_experimental_hint
319 ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
320 ((proof, goal) as status)
322 let (_, metasenv, _, _) = proof in
323 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
324 let (uris, (main, sig_constants)) =
327 (sigmatch ~dbd ~facts signature, signature)
329 (cmatch' ~dbd ~facts ty, Constr.signature_of ty) in
332 (fun res u -> Constr.UriManagerSet.add u res)
333 Constr.UriManagerSet.empty universe in
336 (fun res (_,u) -> Constr.UriManagerSet.add u res)
337 Constr.UriManagerSet.empty uris in
338 let uris = Constr.UriManagerSet.inter uris universe in
339 let uris = Constr.UriManagerSet.elements uris in
340 let rec aux = function
345 let (subst,(proof, goal_list)) =
346 (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
348 ~term:(CicUtil.term_of_uri uri)
352 List.stable_sort (compare_goal_list proof) goal_list
354 Some (uri, (subst,(proof, goal_list)))
355 with ProofEngineTypes.Fail _ -> None
359 | Some status' -> status' :: aux tl)
362 (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
363 Pervasives.compare (List.length goals1) (List.length goals2))