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/
30 let nonvar uri = not (UriManager.uri_is_var uri)
32 module Constr = MetadataConstraints
34 exception Goal_is_not_an_equation
37 let debug_print s = if debug then prerr_endline (Lazy.force s)
39 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
41 let signature_of_hypothesis context metasenv =
44 (fun hyp (set,current_ctx) ->
46 | None -> set, hyp::current_ctx
47 | Some (_, Cic.Decl t) ->
48 Constr.UriManagerSet.union set (Constr.constants_of t),
50 | Some (_, Cic.Def (t, _)) ->
53 CicTypeChecker.type_of_aux'
54 metasenv current_ctx t CicUniv.oblivion_ugraph
57 CicTypeChecker.type_of_aux'
58 metasenv current_ctx ty CicUniv.oblivion_ugraph
60 let set = Constr.UriManagerSet.union set(Constr.constants_of ty)in
62 | Cic.Sort Cic.Prop -> set, hyp::current_ctx
63 | _ -> Constr.UriManagerSet.union set (Constr.constants_of t),
66 | CicTypeChecker.TypeCheckerFailure _ -> set, hyp::current_ctx)
67 context (Constr.UriManagerSet.empty,[])
72 let intersect uris siguris =
73 let set1 = List.fold_right Constr.UriManagerSet.add uris Constr.UriManagerSet.empty in
75 List.fold_right Constr.UriManagerSet.add siguris Constr.UriManagerSet.empty
77 let inter = Constr.UriManagerSet.inter set1 set2 in
78 List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
82 let profiler = CicUtil.profile "at_most" in
83 fun ~dbd ~where uri -> profiler.profile (Constr.at_most ~dbd ~where) uri
86 let profiler = CicUtil.profile "sigmatch" in
87 fun ~dbd ~facts ~where signature ->
88 profiler.profile (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
90 let at_most = Constr.at_most
91 let sigmatch = MetadataConstraints.sigmatch
93 let filter_uris_forward ~dbd (main, constants) uris =
97 | Some (main, types) -> main :: types
100 List.fold_right Constr.UriManagerSet.add main_uris constants
102 List.filter (at_most ~dbd ~where:`Statement full_signature) uris
104 let filter_uris_backward ~dbd ~facts signature uris =
107 (sigmatch ~dbd ~facts ~where:`Statement signature)
109 intersect uris siguris
111 let compare_goal_list proof goal1 goal2 =
112 let _,metasenv, _subst, _,_, _ = proof in
113 let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
114 let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
116 CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph
119 CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.oblivion_ugraph
123 CicReduction.are_convertible
124 ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.oblivion_ugraph
131 CicReduction.are_convertible
132 ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.oblivion_ugraph
139 (* experimental_hint is a version of hint for experimental
140 purposes. It uses auto_tac_verbose instead of auto tac.
141 Auto_tac verbose also returns a substitution - for the moment
142 as a function from cic to cic, to be changed into an association
143 list in the future -. This substitution is used to build a
144 hash table of the inspected goals with their associated proofs.
145 The cose is a cut and paste of the previous one: at the end
146 of the experimentation we shall make a choice. *)
148 let close_with_types s metasenv context =
149 Constr.UriManagerSet.fold
151 let t = CicUtil.term_of_uri e in
153 CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph
155 Constr.UriManagerSet.union bag (Constr.constants_of ty))
158 let close_with_constructors s metasenv context =
159 Constr.UriManagerSet.fold
161 let t = CicUtil.term_of_uri e in
164 | Cic.MutConstruct (uri,_,_,_) ->
165 (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
166 Cic.InductiveDefinition(tl,_,_,_) ->
169 (fun (i,s) (_,_,_,cl) ->
173 let curi = UriManager.uri_of_uriref uri i (Some j) in
174 (* prerr_endline ("adding " ^
175 * (UriManager.string_of_uri curi)); *)
176 j+1,Constr.UriManagerSet.add curi s) (1,s) cl in
183 let apply_tac_verbose =
184 let profiler = CicUtil.profile "apply_tac_verbose" in
185 fun ~term status -> profiler.profile (PrimitiveTactics.apply_tac_verbose ~term) status
188 let profiler = CicUtil.profile "sigmatch" in
189 fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler.profile (Constr.sigmatch ~dbd ~facts ~where) signature
192 let profiler = CicUtil.profile "cmatch'" in
193 fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature
195 let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
196 let cmatch' = Constr.cmatch'
198 (* used only by te old auto *)
199 let signature_of_goal ~(dbd:HSql.dbd) ((proof, goal) as _status) =
200 let (_, metasenv, _subst, _, _, _) = proof in
201 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
202 let main, sig_constants = Constr.signature_of ty in
203 let set = signature_of_hypothesis context metasenv in
208 List.fold_right Constr.UriManagerSet.add (main::l) set in
209 let set = Constr.UriManagerSet.union set sig_constants in
210 let all_constants_closed = close_with_types set metasenv context in
212 sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) in
213 let uris = List.filter nonvar (List.map snd uris) in
214 let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
219 try CicTypeChecker.type_of_aux' [] []
220 (CicUtil.term_of_uri u) CicUniv.oblivion_ugraph
221 with CicTypeChecker.TypeCheckerFailure _ -> assert false
223 let rec check_last_pi = function
224 | Cic.Prod (_,_,tgt) -> check_last_pi tgt
225 | Cic.Sort Cic.Prop -> true
231 let only constants uri =
232 prerr_endline (UriManager.string_of_uri uri);
233 let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
234 let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in
235 let consts = Constr.constants_of ty in
237 prerr_endline ("XXX " ^ UriManager.string_of_uri uri);
238 Constr.UriManagerSet.iter (fun u -> prerr_endline (" - " ^
239 UriManager.string_of_uri u)) consts;
240 Constr.UriManagerSet.iter (fun u -> prerr_endline (" + " ^
241 UriManager.string_of_uri u)) constants;*)
242 Constr.UriManagerSet.subset consts constants
245 let rec types_of_equality = function
246 | Cic.Appl [Cic.MutInd (uri, _, _); ty; _; _]
247 when (LibraryObjects.is_eq_URI uri) ->
248 let uri_set = Constr.constants_of ty in
249 if Constr.UriManagerSet.equal uri_set Constr.UriManagerSet.empty then
251 else Constr.SetSet.singleton uri_set
252 | Cic.Prod (_, s, t) ->
253 Constr.SetSet.union (types_of_equality s) (types_of_equality t)
254 | _ -> Constr.SetSet.empty
257 let types_for_equality metasenv goal =
258 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
259 let all = types_of_equality ty in
264 CicTypeChecker.type_of_aux'
265 metasenv context (Cic.Rel i) CicUniv.oblivion_ugraph in
266 let newty = types_of_equality ty in
267 (i+1,Constr.SetSet.union newty acc))
272 let signature_of metasenv goal =
273 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
274 let ty_set = Constr.constants_of ty in
275 let hyp_set = signature_of_hypothesis context metasenv in
276 let set = Constr.UriManagerSet.union ty_set hyp_set in
278 (close_with_constructors (close_with_types set metasenv context)
283 let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =
284 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
285 let ty_set = Constr.constants_of ty in
286 let hyp_set = signature_of_hypothesis context metasenv in
287 let set = Constr.UriManagerSet.union ty_set hyp_set in
288 let all_constants_closed = close_with_types set metasenv context in
289 (* we split predicates from the rest *)
290 let predicates, rest =
291 Constr.UriManagerSet.partition is_predicate all_constants_closed
294 Constr.UriManagerSet.fold
296 debug_print (lazy ("processing "^(UriManager.string_of_uri u)));
297 let set_for_sigmatch =
298 Constr.UriManagerSet.remove u all_constants_closed in
299 if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
300 (* equality has a special treatment *)
301 (debug_print (lazy "special treatment");
303 Constr.SetSet.elements (types_for_equality metasenv goal)
307 let tyl = Constr.UriManagerSet.elements l in
308 debug_print (lazy ("tyl: "^(String.concat "\n"
309 (List.map UriManager.string_of_uri tyl))));
310 let set_for_sigmatch =
311 Constr.UriManagerSet.diff set_for_sigmatch l in
313 sigmatch ~dbd ~facts:false ~where:`Statement
314 (Some (u,tyl),set_for_sigmatch) in
318 (debug_print (lazy "normal treatment");
320 sigmatch ~dbd ~facts:false ~where:`Statement
321 (Some (u,[]),set_for_sigmatch)
328 sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed)
331 let uris = List.filter nonvar (List.map snd uris) in
332 let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
334 List.filter (only all_constants_closed) uris
338 let filter_out_predicate set ctx menv =
339 Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set
342 let equations_for_goal ~(dbd:HSql.dbd) ?signature ((proof, goal) as _status) =
347 (Constr.UriManagerSet.fold
348 (fun u l -> (" "^UriManager.string_of_uri u)::l) set []))
352 let (_, metasenv, _subst, _, _, _) = proof in
353 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
354 let main, sig_constants =
356 | None -> Constr.signature_of ty
359 (* Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *)
360 (* match main with *)
361 (* None -> raise Goal_is_not_an_equation *)
362 (* | Some (m,l) -> *)
365 match LibraryObjects.eq_URI () with
369 (UriManager.uri_of_string
370 (UriManager.string_of_uri s ^ "#xpointer(1/1)"))
372 match eq_URI,main with
373 | Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l
376 (*Printf.printf "\nSome (m, l): %s, [%s]\n\n"
377 (UriManager.string_of_uri (List.hd l))
378 (String.concat "; " (List.map UriManager.string_of_uri (List.tl l)));
380 (* if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
381 let set = signature_of_hypothesis context metasenv in
382 (* Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
383 let set = Constr.UriManagerSet.union set sig_constants in
384 let set = filter_out_predicate set context metasenv in
385 let set = close_with_types set metasenv context in
386 (* Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
387 let set = close_with_constructors set metasenv context in
388 (* Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
389 let set_for_sigmatch = List.fold_right Constr.UriManagerSet.remove l set in
391 sigmatch ~dbd ~facts:false ~where:`Statement (main,set_for_sigmatch) in
392 let uris = List.filter nonvar (List.map snd uris) in
393 let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
394 let set = List.fold_right Constr.UriManagerSet.add l set in
395 let uris = List.filter (only set) uris in
398 (* else raise Goal_is_not_an_equation *)
400 let experimental_hint
401 ~(dbd:HSql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
402 let (_, metasenv, _subst, _, _, _) = proof in
403 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
404 let (uris, (main, sig_constants)) =
407 (sigmatch ~dbd ~facts signature, signature)
409 (cmatch' ~dbd ~facts ty, Constr.signature_of ty)
411 let uris = List.filter nonvar (List.map snd uris) in
412 let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
413 let types_constants =
415 | None -> Constr.UriManagerSet.empty
416 | Some (main, types) ->
417 List.fold_right Constr.UriManagerSet.add (main :: types)
418 Constr.UriManagerSet.empty
422 Constr.UriManagerSet.union
423 (signature_of_hypothesis context metasenv)
428 | None -> Constr.UriManagerSet.empty
431 CicTypeChecker.type_of_aux'
432 metasenv context (CicUtil.term_of_uri main)
433 CicUniv.oblivion_ugraph
435 Constr.constants_of ty
437 Constr.UriManagerSet.union main hyp_and_sug
439 (* Constr.UriManagerSet.iter debug_print hyp_constants; *)
440 let all_constants_closed = close_with_types all_constants metasenv context in
441 let other_constants =
442 Constr.UriManagerSet.diff all_constants_closed types_constants
444 debug_print (lazy "all_constants_closed");
445 if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) all_constants_closed;
446 debug_print (lazy "other_constants");
447 if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) other_constants;
449 let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in
450 if ((List.length uris < pow) or (pow <= 0))
452 debug_print (lazy "MetadataQuery: large sig, falling back to old method");
453 filter_uris_forward ~dbd (main, other_constants) uris
455 filter_uris_backward ~dbd ~facts (main, other_constants) uris
457 let rec aux = function
462 let (subst,(proof, goal_list)) =
463 (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
465 ~term:(CicUtil.term_of_uri uri)
469 List.stable_sort (compare_goal_list proof) goal_list
471 Some (uri, (subst,(proof, goal_list)))
472 with ProofEngineTypes.Fail _ -> None
476 | Some status' -> status' :: aux tl)
479 (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
480 Pervasives.compare (List.length goals1) (List.length goals2))
483 let new_experimental_hint
484 ~(dbd:HSql.dbd) ?(facts=false) ?signature ~universe
485 ((proof, goal) as status)
487 let (_, metasenv, _subst, _, _, _) = proof in
488 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
489 let (uris, (main, sig_constants)) =
492 (sigmatch ~dbd ~facts signature, signature)
494 (cmatch' ~dbd ~facts ty, Constr.signature_of ty) in
497 (fun res u -> Constr.UriManagerSet.add u res)
498 Constr.UriManagerSet.empty universe in
501 (fun res (_,u) -> Constr.UriManagerSet.add u res)
502 Constr.UriManagerSet.empty uris in
503 let uris = Constr.UriManagerSet.inter uris universe in
504 let uris = Constr.UriManagerSet.elements uris in
505 let rec aux = function
510 let (subst,(proof, goal_list)) =
511 (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
513 ~term:(CicUtil.term_of_uri uri)
517 List.stable_sort (compare_goal_list proof) goal_list
519 Some (uri, (subst,(proof, goal_list)))
520 with ProofEngineTypes.Fail _ -> None
524 | Some status' -> status' :: aux tl)
527 (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
528 Pervasives.compare (List.length goals1) (List.length goals2))