1 (* Copyright (C) 2002, 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/.
31 if debug then prerr_endline (Lazy.force s);;
35 (* closing a term w.r.t. its metavariables
36 very naif version: it does not take dependencies properly into account *)
38 let naif_closure ?(prefix_name="xxx_") t metasenv context =
39 let metasenv = ProofEngineHelpers.sort_metasenv metasenv in
40 let n = List.length metasenv in
41 let what = List.map (fun (i,cc,ty) -> Cic.Meta(i,[])) metasenv in
44 (fun (i,acc) (_,cc,ty) -> (i-1,Cic.Rel i::acc))
47 let t = CicSubstitution.lift n t in
49 ProofEngineReduction.replace_lifting
50 ~equality:(fun c t1 t2 ->
52 | Cic.Meta(i,_),Cic.Meta(j,_) -> i = j
54 ~context ~what ~with_what ~where:t
58 (fun (n,t) (_,cc,ty) ->
59 n-1, Cic.Lambda(Cic.Name (prefix_name^string_of_int n),
60 CicSubstitution.lift n ty,t))
66 let lambda_close ?prefix_name t menv ctx =
67 let t = naif_closure ?prefix_name t menv ctx in
70 | None -> CicSubstitution.subst (Cic.Implicit None) t (* delift *)
71 | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t)
72 | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t))
76 (* functions for retrieving theorems *)
78 exception FillingFailure of AutoCache.cache * int
80 let rec unfold context = function
81 | Cic.Prod(name,s,t) ->
82 let t' = unfold ((Some (name,Cic.Decl s))::context) t in
84 | t -> ProofEngineReduction.unfold context t
86 let find_library_theorems dbd proof goal =
87 let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
88 let terms = List.map CicUtil.term_of_uri univ in
91 (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)))
94 let find_context_theorems context metasenv =
97 (fun (res,i) ctxentry ->
99 | Some (_,Cic.Decl t) ->
100 (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
101 | Some (_,Cic.Def (_,Some t)) ->
102 (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
103 | Some (_,Cic.Def (_,None)) ->
106 CicTypeChecker.type_of_aux'
107 metasenv context t CicUniv.empty_ugraph
114 let rec is_an_equality = function
115 | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _]
116 when (LibraryObjects.is_eq_URI uri) -> true
117 | Cic.Prod (_, _, t) -> is_an_equality t
121 let partition_equalities =
122 List.partition (fun (_,ty) -> is_an_equality ty)
125 let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;;
128 let is_unit_equation context metasenv oldnewmeta term =
129 let head, metasenv, args, newmeta =
130 TermUtil.saturate_term oldnewmeta metasenv context term 0
132 let propositional_args =
136 let _,_,mt = CicUtil.lookup_meta i metasenv in
138 CicTypeChecker.type_of_aux' metasenv context mt
142 CicReduction.are_convertible ~metasenv context
143 sort (Cic.Sort Cic.Prop) u
145 if b then Some i else None
149 if propositional_args = [] then
150 let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
151 Some (args,metasenv,newmetas,head,newmeta)
155 let get_candidates universe cache t =
157 (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
160 (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^
161 (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
162 debug_print debug_msg;
166 let only signature context t =
168 let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
169 let consts = MetadataConstraints.constants_of ty in
170 let b = MetadataConstraints.UriManagerSet.subset consts signature in
174 let ty' = unfold context ty in
175 let consts' = MetadataConstraints.constants_of ty' in
176 MetadataConstraints.UriManagerSet.subset consts' signature
181 let not_default_eq_term t =
183 let uri = CicUtil.uri_of_term t in
184 not (LibraryObjects.in_eq_URIs uri)
185 with Invalid_argument _ -> true
187 let retrieve_equations signature universe cache context=
188 match LibraryObjects.eq_URI() with
191 let eq_uri = UriManager.strip_xpointer eq_uri in
192 let fake= Cic.Meta(-1,[]) in
193 let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
194 let candidates = get_candidates universe cache fake_eq in
195 (* defaults eq uris are built-in in auto *)
196 let candidates = List.filter not_default_eq_term candidates in
197 let candidates = List.filter (only signature context) candidates in
198 List.iter (fun t -> debug_print (lazy (CicPp.ppterm t))) candidates;
201 let build_equality bag head args proof newmetas maxmeta =
203 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
205 if args = [] then proof else Cic.Appl (proof::args)
207 let o = !Utils.compare_terms t1 t2 in
208 let stat = (ty,t1,t2,o) in
209 (* let w = compute_equality_weight stat in *)
211 let proof = Equality.Exact p in
212 let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
213 (* to clean the local context of metas *)
214 Equality.fix_metas bag maxmeta e
218 let partition_unit_equalities context metasenv newmeta bag equations =
220 (fun (units,other,maxmeta)(t,ty) ->
221 match is_unit_equation context metasenv maxmeta ty with
222 | Some (args,metasenv,newmetas,head,newmeta') ->
223 let maxmeta,equality =
224 build_equality bag head args t newmetas newmeta' in
225 equality::units,other,maxmeta
227 units,(t,ty)::other,maxmeta)
228 ([],[],newmeta) equations
231 (Saturation.make_active [],
232 Saturation.make_passive [],
233 Equality.mk_equality_bag)
235 let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
236 (* the local cache in initially empty *)
237 let cache = AutoCache.cache_empty in
238 let _, metasenv, _subst,_, _, _ = proof in
239 let signature = MetadataQuery.signature_of metasenv goal in
240 let newmeta = CicMkImplicit.new_meta metasenv [] in
241 let _,context,_ = CicUtil.lookup_meta goal metasenv in
242 let ct = find_context_theorems context metasenv in
244 (lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct))));
247 find_library_theorems dbd metasenv goal
250 (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
251 let cache = cache_add_list cache context (ct@lt) in
253 retrieve_equations signature universe cache context in
255 (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
260 CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
261 (* retrieve_equations could also return flexible terms *)
262 if is_an_equality ty then Some(t,ty)
265 let ty' = unfold context ty in
266 if is_an_equality ty' then Some(t,ty') else None
267 with _ -> None) (* catturare l'eccezione giusta di unfold *)
269 let bag = Equality.mk_equality_bag () in
270 let units, other_equalities, newmeta =
271 partition_unit_equalities context metasenv newmeta bag eqs_and_types in
272 (* let env = (metasenv, context, CicUniv.empty_ugraph) in
275 match LibraryObjects.eq_URI() with
276 | None ->assert false
277 | Some eq_uri -> eq_uri in
278 Saturation.simplify_equalities bag eq_uri env units in *)
279 let passive = Saturation.make_passive units in
280 let no = List.length units in
281 let active = Saturation.make_active [] in
282 let active,passive,newmeta =
283 if paramod then active,passive,newmeta
285 Saturation.pump_actives
286 context bag newmeta active passive (no+1) infinity
288 (active,passive,bag),cache,newmeta
290 let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast =
291 let head, metasenv, args, newmeta =
292 TermUtil.saturate_term oldnewmeta metasenv context term 0
294 let propositional_args =
298 let _,_,mt = CicUtil.lookup_meta i metasenv in
300 CicTypeChecker.type_of_aux' metasenv context mt
304 CicReduction.are_convertible ~metasenv context
305 sort (Cic.Sort Cic.Prop) u
307 if b then Some i else None
311 let results,cache,newmeta =
312 if propositional_args = [] then
313 let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
314 [args,metasenv,newmetas,head,newmeta],cache,newmeta
318 None,metasenv,term,term (* term non e' significativo *)
322 {AutoTypes.default_flags() with
323 AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
324 maxwidth = 2;maxdepth = 2;
325 use_paramod=true;use_only_paramod=false}
327 {AutoTypes.default_flags() with
328 AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
329 maxwidth = 2;maxdepth = 4;
330 use_paramod=true;use_only_paramod=false}
332 match auto newmeta tables universe cache context metasenv propositional_args flags with
333 | [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
334 | substs,cache,newmeta ->
338 CicMetaSubst.apply_subst_metasenv subst metasenv
340 let head = CicMetaSubst.apply_subst subst head in
342 List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
344 let args = List.map (CicMetaSubst.apply_subst subst) args in
345 let newm = CicMkImplicit.new_meta metasenv subst in
346 args,metasenv,newmetas,head,max newm newmeta)
347 substs, cache, newmeta
349 results,cache,newmeta
351 let build_equalities auto context metasenv tables universe cache newmeta equations =
353 (fun (facts,cache,newmeta) (t,ty) ->
354 (* in any case we add the equation to the cache *)
355 let cache = AutoCache.cache_add_list cache context [(t,ty)] in
357 let saturated,cache,newmeta =
358 fill_hypothesis context metasenv newmeta ty tables universe cache auto true
360 let (active,passive,bag) = tables in
361 let eqs,bag,newmeta =
363 (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') ->
364 let maxmeta,equality =
365 build_equality bag head args t newmetas newmeta'
367 equality::acc,bag,maxmeta)
368 ([],bag,newmeta) saturated
370 (eqs@facts, cache, newmeta)
371 with FillingFailure (cache,newmeta) ->
372 (* if filling hypothesis fails we add the equation to
374 (facts,cache,newmeta)
376 ([],cache,newmeta) equations
378 let close_more tables maxmeta context status auto universe cache =
379 let (active,passive,bag) = tables in
380 let proof, goalno = status in
381 let _, metasenv,_subst,_,_, _ = proof in
382 let signature = MetadataQuery.signature_of metasenv goalno in
383 let equations = retrieve_equations signature universe cache context in
388 CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
389 (* retrieve_equations could also return flexible terms *)
390 if is_an_equality ty then Some(t,ty) else None)
392 let units, cache, maxm =
393 build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in
394 debug_print (lazy (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
395 string_of_int maxm));
397 (fun e -> debug_print (lazy (Equality.string_of_equality e)))
399 debug_print (lazy ">>>>>>>>>>>>>>>>>>>>>>");
400 let passive = Saturation.add_to_passive units passive in
401 let no = List.length units in
402 debug_print (lazy ("No = " ^ (string_of_int no)));
403 let active,passive,newmeta =
404 Saturation.pump_actives context bag maxm active passive (no+1) infinity
406 (active,passive,bag),cache,newmeta
408 let find_context_equalities
409 maxmeta bag context proof (universe:Universe.universe) cache
411 let module C = Cic in
412 let module S = CicSubstitution in
413 let module T = CicTypeChecker in
414 let _,metasenv,_subst,_,_, _ = proof in
415 let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
416 (* if use_auto is true, we try to close the hypothesis of equational
417 statements using auto; a naif, and probably wrong approach *)
418 let rec aux cache index newmeta = function
419 | [] -> [], newmeta,cache
420 | (Some (_, C.Decl (term)))::tl ->
423 (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
424 let do_find context term =
426 | C.Prod (name, s, t) when is_an_equality t ->
429 let term = S.lift index term in
430 let saturated,cache,newmeta =
431 fill_hypothesis context metasenv newmeta term
432 empty_tables universe cache default_auto false
436 (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
437 let newmeta, equality =
439 bag head args (Cic.Rel index) newmetas (max newmeta newmeta')
441 equality::acc, newmeta + 1)
442 ([],newmeta) saturated
445 with FillingFailure (cache,newmeta) ->
447 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
448 when LibraryObjects.is_eq_URI uri ->
449 let term = S.lift index term in
451 build_equality bag term [] (Cic.Rel index) [] newmeta
453 [e], (newmeta+1),cache
454 | _ -> [], newmeta, cache
456 let eqs, newmeta, cache = do_find context term in
457 let rest, newmeta,cache = aux cache (index+1) newmeta tl in
458 List.map (fun x -> index,x) eqs @ rest, newmeta, cache
460 aux cache (index+1) newmeta tl
462 let il, maxm, cache =
463 aux cache 1 newmeta context
465 let indexes, equalities = List.split il in
466 indexes, equalities, maxm, cache
469 (***************** applyS *******************)
471 let new_metasenv_and_unify_and_t
472 dbd flags universe proof goal ?tables newmeta' metasenv'
473 context term' ty termty goal_arity
475 let (consthead,newmetasenv,arguments,_) =
476 TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
478 match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
480 let proof',oldmetasenv =
481 let (puri,metasenv,_subst,pbo,pty, attrs) = proof in
482 (puri,newmetasenv,_subst,pbo,pty, attrs),metasenv
484 let goal_for_paramod =
485 match LibraryObjects.eq_URI () with
487 Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
488 | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
490 let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
491 let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
493 let uri,_,_subst,p,ty, attrs = proof' in
494 uri,metasenv_for_paramod,_subst,p,ty, attrs
496 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
498 ProofEngineTypes.apply_tactic
499 (EqualityTactics.rewrite_tac ~direction:`RightToLeft
500 ~pattern:(ProofEngineTypes.conclusion_pattern None)
501 (Cic.Meta(newmeta,irl)) [])
504 let goal = match goals with [g] -> g | _ -> assert false in
506 ProofEngineTypes.apply_tactic
507 (PrimitiveTactics.apply_tac term'')
511 let (active, passive,bag), cache, maxmeta =
512 init_cache_and_tables dbd flags.use_library true universe
515 Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
516 max_int max_int flags.timeout
519 raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
520 | Some (_,proof''''',_), active,passive,_ ->
522 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
523 ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive
526 let rec count_prods context ty =
527 match CicReduction.whd context ty with
528 Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
531 let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
532 let module T = CicTypeChecker in
533 let module R = CicReduction in
534 let module C = Cic in
535 let (_,metasenv,_subst,_,_, _) = proof in
536 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
537 let newmeta = CicMkImplicit.new_meta metasenv subst in
538 let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
540 C.Var (uri,exp_named_subst) ->
541 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
542 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
545 exp_named_subst_diff,newmeta',newmetasenvfragment,
546 C.Var (uri,exp_named_subst')
547 | C.Const (uri,exp_named_subst) ->
548 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
549 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
552 exp_named_subst_diff,newmeta',newmetasenvfragment,
553 C.Const (uri,exp_named_subst')
554 | C.MutInd (uri,tyno,exp_named_subst) ->
555 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
556 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
559 exp_named_subst_diff,newmeta',newmetasenvfragment,
560 C.MutInd (uri,tyno,exp_named_subst')
561 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
562 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
563 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
566 exp_named_subst_diff,newmeta',newmetasenvfragment,
567 C.MutConstruct (uri,tyno,consno,exp_named_subst')
568 | _ -> [],newmeta,[],term
570 let metasenv' = metasenv@newmetasenvfragment in
572 CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
574 let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
575 let goal_arity = count_prods context ty in
576 let proof, gl, active, passive =
577 new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
578 newmeta' metasenv' context term' ty termty goal_arity
580 proof, gl, active, passive
583 (****************** AUTO ********************)
585 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
586 let ugraph = CicUniv.empty_ugraph;;
587 let typeof = CicTypeChecker.type_of_aux';;
589 let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
592 let is_in_prop context subst metasenv ty =
593 let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
594 fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
597 let assert_proof_is_valid proof metasenv context goalty =
600 let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
601 let b,_ = CicReduction.are_convertible context ty goalty u in
605 List.map (function None -> None | Some (x,_) -> Some x) context
607 debug_print (lazy ("PROOF:" ^ CicPp.pp proof names));
608 debug_print (lazy ("PROOFTY:" ^ CicPp.pp ty names));
609 debug_print (lazy ("GOAL:" ^ CicPp.pp goalty names));
610 debug_print (lazy ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv));
617 let assert_subst_are_disjoint subst subst' =
620 (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
625 let split_goals_in_prop metasenv subst gl =
628 let _,context,ty = CicUtil.lookup_meta g metasenv in
630 let sort,u = typeof ~subst metasenv context ty ugraph in
632 CicReduction.are_convertible
633 ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
636 | CicTypeChecker.AssertFailure s
637 | CicTypeChecker.TypeCheckerFailure s ->
639 (lazy ("NON TIPA" ^ ppterm context (CicMetaSubst.apply_subst subst ty)));
642 (* FIXME... they should type! *)
646 let split_goals_with_metas metasenv subst gl =
649 let _,context,ty = CicUtil.lookup_meta g metasenv in
650 let ty = CicMetaSubst.apply_subst subst ty in
651 CicUtil.is_meta_closed ty)
655 let order_new_goals metasenv subst open_goals ppterm =
656 let prop,rest = split_goals_in_prop metasenv subst open_goals in
657 let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
659 (List.map (fun x -> x,P) (closed_prop @ open_prop))
661 (List.map (fun x -> x,T) rest)
666 let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals
668 debug_print (lazy (" OPEN: "^
672 | (i,t,P) -> string_of_int i ^ ":"^ppterm t^ "Prop"
673 | (i,t,T) -> string_of_int i ^ ":"^ppterm t^ "Type")
678 let is_an_equational_goal = function
679 | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
684 let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
687 let calculate_timeout flags =
688 if flags.timeout = 0. then
689 (debug_print (lazy "AUTO WITH NO TIMEOUT");
690 {flags with timeout = infinity})
694 let is_equational_case goalty flags =
695 let ensure_equational t =
696 if is_an_equational_goal t then true
699 let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
700 raise (ProofEngineTypes.Fail (lazy msg))
703 (flags.use_paramod && is_an_equational_goal goalty) ||
704 (flags.use_only_paramod && ensure_equational goalty)
707 let cache_add_success sort cache k v =
708 if sort = P then cache_add_success cache k v else cache_remove_underinspection
713 type menv = Cic.metasenv
714 type subst = Cic.substitution
715 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
716 let candidate_no = ref 0;;
717 type candidate = int * Cic.term
718 type cache = AutoCache.cache
720 Saturation.active_table * Saturation.passive_table * Equality.equality_bag
723 (* the goal (mainly for depth) and key of the goal *)
724 goal * AutoCache.cache_key
726 (* goal has to be proved *)
728 (* goal has to be cached as a success obtained using candidate as the first
730 | S of goal * AutoCache.cache_key * candidate * int
732 (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
733 menv * subst * int * op list * op list * fail list
735 (* list of computations that may lead to the solution: all op list will
736 * end with the same (S(g,_)) *)
739 (* menv, subst, alternatives, tables, cache, maxmeta *)
740 | Proved of menv * subst * elem list * tables * cache * int
741 | Gaveup of tables * cache * int
744 (* the status exported to the external observer *)
746 (* context, (goal,candidate) list, and_list, history *)
747 Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list *
748 (int * Cic.term * int) list * Cic.term list
751 let rec aux acc = function
752 | (D g)::tl -> aux (acc@[g]) tl
758 List.filter (function (_,_,P) -> true | _ -> false) l
762 let rec aux acc = function
763 | (D g)::tl -> aux (acc@[g]) tl
764 | (S _)::tl -> aux acc tl
769 let calculate_goal_ty (goalno,_,_) s m =
771 let _,cc,goalty = CicUtil.lookup_meta goalno m in
772 (* XXX applicare la subst al contesto? *)
773 Some (cc, CicMetaSubst.apply_subst s goalty)
774 with CicUtil.Meta_not_found i when i = goalno -> None
776 let calculate_closed_goal_ty (goalno,_,_) s =
778 let cc,_,goalty = List.assoc goalno s in
779 (* XXX applicare la subst al contesto? *)
780 Some (cc, CicMetaSubst.apply_subst s goalty)
781 with Not_found -> None
783 let pp_status ctx status =
785 let names = Utils.names_of_context ctx in
788 ProofEngineReduction.replace
789 ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
790 ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
794 let string_of_do m s (gi,_,_ as g) d =
795 match calculate_goal_ty g s m with
796 | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
797 | None -> Printf.sprintf "D(%d, _, %d)" gi d
799 let string_of_s m su k (ci,ct) gi =
800 Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp ct) ci
802 let string_of_ol m su l =
806 | D (g,d,s) -> string_of_do m su (g,d,s) d
807 | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
810 let string_of_fl m s fl =
812 (List.map (fun ((i,_,_),ty) ->
813 Printf.sprintf "(%d, %s)" i (pp ty)) fl)
815 let rec aux = function
817 | (m,s,_,_,ol,fl)::tl ->
818 Printf.eprintf "< [%s] ;;; [%s]>\n"
819 (string_of_ol m s ol) (string_of_fl m s fl);
822 Printf.eprintf "-------------------------- status -------------------\n";
824 Printf.eprintf "-----------------------------------------------------\n";
827 let auto_status = ref [] ;;
828 let auto_context = ref [];;
829 let in_pause = ref false;;
830 let pause b = in_pause := b;;
831 let cond = Condition.create ();;
832 let mutex = Mutex.create ();;
833 let hint = ref None;;
835 let step _ = Condition.signal cond;;
836 let give_hint n = hint := Some n;;
842 Condition.wait cond mutex;
847 let get_auto_status _ =
848 let status = !auto_status in
849 let and_list,elems,last =
852 | (m,s,_,don,gl,fail)::tl ->
855 (fun (id,d,_ as g) ->
856 match calculate_goal_ty g s m with
857 | Some (_,x) -> Some (id,x,d) | None -> None)
861 (* these are the S goalsin the or list *)
864 (fun (m,s,_,don,gl,fail) ->
866 (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
870 (* this function eats id from a list l::[id,x] returning x, l *)
871 let eat_tail_if_eq id l =
872 let rec aux (s, l) = function
874 | ((id1,_,_),k1,c)::tl when id = id1 ->
876 | None -> aux (Some c,l) tl
877 | Some _ -> assert false)
878 | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
880 let c, l = aux (None, []) l in
883 let eat_in_parallel id l =
884 let rec aux (b,eaten, new_l as acc) l =
888 match eat_tail_if_eq id l with
889 | None, l -> aux (b@[false], eaten, new_l@[l]) tl
890 | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
894 let rec eat_all rows l =
898 match List.rev elem with
899 | ((to_eat,depth,_),k,_)::next_lunch ->
900 let b, eaten, l = eat_in_parallel to_eat l in
901 let eaten = HExtlib.list_uniq eaten in
902 let eaten = List.rev eaten in
903 let b = true (* List.hd (List.rev b) *) in
904 let rows = rows @ [to_eat,k,b,depth,eaten] in
906 | [] -> eat_all rows or_list
908 eat_all [] (List.rev orlist)
912 (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
915 (* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
916 and_list, rows, history
918 !auto_context, elems, and_list, last
921 (* Works if there is no dependency over proofs *)
922 let is_a_green_cut goalty =
923 CicUtil.is_meta_closed goalty
925 let rec first_s = function
926 | (D _)::tl -> first_s tl
927 | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
930 let list_union l1 l2 =
931 (* TODO ottimizzare compare *)
932 HExtlib.list_uniq (List.sort compare (l1 @ l1))
934 let eat_head todo id fl orlist =
935 let rec aux acc = function
937 | (m, s, _, _, todo1, fl1)::tl as orlist ->
939 match first_s todo1 with
940 | None -> orlist, acc
941 | Some (((gno,_,_),_,_,_), todo11) ->
942 (* TODO confronto tra todo da ottimizzare *)
943 if gno = id && todo11 = todo then
944 aux (list_union fl1 acc) tl
952 let close_proof p ty menv context =
954 List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
956 let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
957 naif_closure p menv context
959 (* XXX capire bene quando aggiungere alla cache *)
960 let add_to_cache_and_del_from_orlist_if_green_cut
961 g s m cache key todo orlist fl ctx size minsize
963 let cache = cache_remove_underinspection cache key in
964 (* prima per fare la irl usavamo il contesto vero e proprio e non quello
966 match calculate_closed_goal_ty g s with
967 | None -> assert false
968 | Some (canonical_ctx , gty) ->
969 let goalno,depth,sort = g in
971 let irl = mk_irl canonical_ctx in
972 let goal = Cic.Meta(goalno, irl) in
973 let proof = CicMetaSubst.apply_subst s goal in
974 let green_proof, closed_proof =
975 let b = is_a_green_cut proof in
977 b, (* close_proof proof gty m ctx *) proof
981 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
982 if is_a_green_cut key then
983 (* if the initia goal was closed, we cut alternatives *)
984 let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
985 let orlist, fl = eat_head todo goalno fl orlist in
987 if size < minsize then
988 (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
990 (* if the proof is closed we cache it *)
991 if green_proof then cache_add_success cache key proof
992 else (* cache_add_success cache key closed_proof *)
993 (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
995 cache, orlist, fl, true
998 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
999 if size < minsize then
1000 (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
1001 (* if the substituted goal and the proof are closed we cache it *)
1002 if is_a_green_cut gty then
1003 if green_proof then cache_add_success cache gty proof
1004 else (* cache_add_success cache gty closed_proof *)
1005 (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
1009 CicTypeChecker.type_of_aux' ~subst:s
1010 m ctx closed_proof CicUniv.oblivion_ugraph
1012 if is_a_green_cut ty then
1013 cache_add_success cache ty closed_proof
1016 | CicTypeChecker.TypeCheckerFailure _ ->*)
1017 (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
1019 cache, orlist, fl, false
1021 let close_failures (fl : fail list) (cache : cache) =
1023 (fun cache ((gno,depth,_),gty) ->
1024 debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
1025 cache_add_failure cache gty depth)
1028 let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
1029 let entry = goalno, (canonical_ctx, t,ty) in
1030 assert_subst_are_disjoint subst [entry];
1031 let subst = entry :: subst in
1032 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1035 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
1036 None,metasenv,subst ,Cic.Meta(goalno,mk_irl context),goalty, []
1039 tables maxm cache depth fake_proof goalno goalty subst context
1042 let active,passive,bag = tables in
1043 let ppterm = ppterm context in
1044 let status = (fake_proof,goalno) in
1045 if flags.use_only_paramod then
1047 debug_print (lazy ("PARAMODULATION SU: " ^
1048 string_of_int goalno ^ " " ^ ppterm goalty ));
1049 let goal_steps, saturation_steps, timeout =
1050 max_int,max_int,flags.timeout
1053 Saturation.given_clause bag maxm status active passive
1054 goal_steps saturation_steps timeout
1056 | None, active, passive, maxmeta ->
1057 [], (active,passive,bag), cache, maxmeta, flags
1058 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
1060 assert_subst_are_disjoint subst subst';
1061 let subst = subst@subst' in
1063 order_new_goals metasenv subst open_goals ppterm
1066 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1069 [(!candidate_no,proof),metasenv,subst,open_goals],
1070 (active,passive,bag),
1071 cache, maxmeta, flags
1077 ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty));
1079 Saturation.all_subsumed bag maxm status active passive
1081 assert (maxmeta >= maxm);
1084 (fun subst',(_,metasenv,_subst,proof,_, _),open_goals ->
1085 assert_subst_are_disjoint subst subst';
1086 let subst = subst@subst' in
1088 order_new_goals metasenv subst open_goals ppterm
1091 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1094 (!candidate_no,proof),metasenv,subst,open_goals)
1097 res', (active,passive,bag), cache, maxmeta, flags
1102 goalty tables maxm subst fake_proof goalno depth context cand
1104 let ppterm = ppterm context in
1106 let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
1107 (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:maxm ~term:cand)
1110 debug_print (lazy (" OK: " ^ ppterm cand));
1111 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
1112 let open_goals = order_new_goals metasenv subst open_goals ppterm in
1113 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
1115 Some ((!candidate_no,cand),metasenv,subst,open_goals), tables , maxmeta
1117 | ProofEngineTypes.Fail s -> None,tables, maxm
1118 | CicUnification.Uncertain s -> None,tables, maxm
1121 let sort_new_elems =
1122 List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2)
1123 (* List.sort (fun (_,_,_,l2) (_,_,_,l1) -> List.length l1 - List.length l2) *)
1126 let applicative_case
1127 tables maxm depth subst fake_proof goalno goalty metasenv context universe
1130 let candidates = get_candidates universe cache goalty in
1131 let tables, elems, maxm =
1133 (fun (tables,elems,maxm) cand ->
1135 try_candidate goalty
1136 tables maxm subst fake_proof goalno depth context cand
1138 | None, tables,maxm -> tables,elems, maxm
1139 | Some x, tables, maxm -> tables,x::elems, maxm)
1140 (tables,[],maxm) candidates
1142 let elems = sort_new_elems elems in
1143 elems, tables, cache, maxm
1146 let equational_and_applicative_case
1147 universe flags m s g gty tables cache maxm context
1149 let goalno, depth, sort = g in
1150 let fake_proof = mk_fake_proof m s g gty context in
1151 if is_equational_case gty flags then
1152 let elems,tables,cache,maxm1, flags =
1153 equational_case tables maxm cache
1154 depth fake_proof goalno gty s context flags
1157 let more_elems, tables, cache, maxm1 =
1158 if flags.use_only_paramod then
1159 [],tables, cache, maxm
1162 tables maxm depth s fake_proof goalno
1163 gty m context universe cache
1166 elems@more_elems, tables, cache, maxm, flags
1168 let elems, tables, cache, maxm =
1169 applicative_case tables maxm depth s fake_proof goalno
1170 gty m context universe cache
1172 elems, tables, cache, maxm, flags
1174 let rec condition_for_hint i = function
1176 | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
1177 | _::tl -> condition_for_hint i tl
1179 let remove_s_from_fl (id,_,_) (fl : fail list) =
1180 let rec aux = function
1182 | ((id1,_,_),_)::tl when id = id1 -> tl
1183 | hd::tl -> hd :: aux tl
1187 let prunable ty todo =
1188 let rec aux b = function
1189 | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
1190 | (D (_,_,T))::tl -> aux b tl
1197 let auto_main tables maxm context flags universe cache elems =
1198 auto_context := context;
1199 let rec aux tables maxm flags cache (elems : status) =
1200 (* pp_status context elems; *)
1203 (* complete failure *)
1204 Gaveup (tables, cache, maxm)
1205 | (m, s, _, _, [],_)::orlist ->
1206 (* complete success *)
1207 Proved (m, s, orlist, tables, cache, maxm)
1208 | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist ->
1209 (* skip since not Prop, don't even check if closed by side-effect *)
1210 aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1211 | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
1212 (* partial success, cache g and go on *)
1213 let cache, orlist, fl, sibling_pruned =
1214 add_to_cache_and_del_from_orlist_if_green_cut
1215 g s m cache key todo orlist fl context size minsize
1217 debug_print (lazy (AutoCache.cache_print context cache));
1218 let fl = remove_s_from_fl g fl in
1219 let don = if sibling_pruned then don else op::don in
1220 aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1221 | (m, s, size, don, todo, fl)::orlist
1222 when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1223 debug_print (lazy ("FAIL: WIDTH"));
1224 (* too many goals in and generated by last th *)
1225 let cache = close_failures fl cache in
1226 aux tables maxm flags cache orlist
1227 | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
1229 (lazy ("FAIL: SIZE: "^string_of_int size ^
1230 " > " ^ string_of_int flags.maxsize ));
1231 (* we already have a too large proof term *)
1232 let cache = close_failures fl cache in
1233 aux tables maxm flags cache orlist
1234 | _ when Unix.gettimeofday () > flags.timeout ->
1236 debug_print (lazy ("FAIL: TIMEOUT"));
1237 Gaveup (tables, cache, maxm)
1238 | (m, s, size, don, (D (gno,depth,P as g))::todo, fl)::orlist as status ->
1240 match calculate_goal_ty g s m with
1242 (* closed by side effect *)
1243 debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1244 aux tables maxm flags cache ((m,s,size,don,todo, fl)::orlist)
1245 | Some (canonical_ctx, gty) ->
1247 Utils.weight_of_term ~count_metas_occurrences:true gty
1249 if gsize > flags.maxgoalsizefactor then
1250 (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int size));
1251 aux tables maxm flags cache orlist)
1253 (* still to be proved *)
1254 (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
1255 match cache_examine cache gty with
1256 | Failed_in d when d >= depth ->
1258 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1259 let cache = close_failures fl cache in
1260 aux tables maxm flags cache orlist
1261 | UnderInspection ->
1263 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1264 let cache = close_failures fl cache in
1265 aux tables maxm flags cache orlist
1267 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1268 let s, m = put_in_subst s m g canonical_ctx t gty in
1269 aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist)
1271 | Failed_in _ when depth > 0 ->
1273 | Some i when condition_for_hint i todo ->
1274 aux tables maxm flags cache orlist
1275 | _ -> hint := None;
1276 (* more depth or is the first time we see the goal *)
1277 if prunable gty todo then
1279 "FAIL: LOOP: one father is equal"));
1280 aux tables maxm flags cache orlist)
1282 let cache = cache_add_underinspection cache gty depth in
1283 auto_status := status;
1286 (lazy ("INSPECTING: " ^
1287 string_of_int gno ^ "("^ string_of_int size ^ "): "^
1289 (* elems are possible computations for proving gty *)
1290 let elems, tables, cache, maxm, flags =
1291 equational_and_applicative_case
1292 universe flags m s g gty tables cache maxm context
1295 (* this goal has failed *)
1296 let cache = close_failures ((g,gty)::fl) cache in
1297 aux tables maxm flags cache orlist
1299 (* elems = (cand,m,s,gl) *)
1300 let size_gl l = List.length
1301 (List.filter (function (_,_,P) -> true | _ -> false) l)
1304 let inj_gl gl = List.map (fun g -> D g) gl in
1305 let rec map = function
1306 | [] -> assert false
1307 | (cand,m,s,gl)::[] ->
1308 (* in the last one we add the failure *)
1310 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1312 (* we are the last in OR, we fail on g and
1313 * also on all failures implied by g *)
1314 (m,s, size + size_gl gl, don, todo, (g,gty)::fl)
1316 | (cand,m,s,gl)::tl ->
1317 (* we add the S step after gl and before todo *)
1319 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1321 (* since we are not the last in OR, we do not
1323 (m,s, size + size_gl gl, don, todo, []) :: map tl
1327 aux tables maxm flags cache elems)
1330 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1331 let cache = close_failures fl cache in
1332 aux tables maxm flags cache orlist)
1334 (aux tables maxm flags cache elems : auto_result)
1339 auto_all_solutions maxm tables universe cache context metasenv gl flags
1341 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1344 (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1346 let elems = [metasenv,[],1,[],goals,[]] in
1347 let rec aux tables maxm solutions cache elems flags =
1348 match auto_main tables maxm context flags universe cache elems with
1349 | Gaveup (tables,cache,maxm) ->
1350 solutions,cache,maxm
1351 | Proved (metasenv,subst,others,tables,cache,maxm) ->
1352 if Unix.gettimeofday () > flags.timeout then
1353 ((subst,metasenv)::solutions), cache, maxm
1355 aux tables maxm ((subst,metasenv)::solutions) cache others flags
1357 let rc = aux tables maxm [] cache elems flags in
1359 | [],cache,maxm -> [],cache,maxm
1360 | solutions,cache,maxm ->
1363 (fun (subst,newmetasenv) ->
1365 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1367 if opened = [] then Some subst else None)
1370 solutions,cache,maxm
1373 (* }}} ****************** AUTO ***************)
1375 let auto flags metasenv tables universe cache context metasenv gl =
1376 let initial_time = Unix.gettimeofday() in
1377 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1378 let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1379 let elems = [metasenv,[],1,[],goals,[]] in
1380 match auto_main tables 0 context flags universe cache elems with
1381 | Proved (metasenv,subst,_, tables,cache,_) ->
1383 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1384 Some (subst,metasenv), cache
1385 | Gaveup (tables,cache,maxm) ->
1387 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1391 let bool params name default =
1393 let s = List.assoc name params in
1394 if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
1395 else if s = "0" || s = "false" || s = "no" || s= "off" then false
1397 let msg = "Unrecognized value for parameter "^name^"\n" in
1398 let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
1399 raise (ProofEngineTypes.Fail (lazy msg))
1400 with Not_found -> default
1403 let string params name default =
1404 try List.assoc name params with
1405 | Not_found -> default
1408 let int params name default =
1409 try int_of_string (List.assoc name params) with
1410 | Not_found -> default
1412 raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
1415 let flags_of_params params ?(for_applyS=false) () =
1416 let int = int params in
1417 let bool = bool params in
1418 let close_more = bool "close_more" false in
1419 let use_paramod = bool "use_paramod" true in
1420 let use_only_paramod =
1421 if for_applyS then true else bool "paramodulation" false in
1422 let use_library = bool "library"
1423 ((AutoTypes.default_flags()).AutoTypes.use_library) in
1424 let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
1425 let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
1426 let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
1427 let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
1428 let timeout = int "timeout" 0 in
1429 { AutoTypes.maxdepth =
1430 if use_only_paramod then 2 else depth;
1431 AutoTypes.maxwidth = width;
1432 AutoTypes.maxsize = size;
1435 if for_applyS then Unix.gettimeofday () +. 30.0
1439 Unix.gettimeofday() +. (float_of_int timeout);
1440 AutoTypes.use_library = use_library;
1441 AutoTypes.use_paramod = use_paramod;
1442 AutoTypes.use_only_paramod = use_only_paramod;
1443 AutoTypes.close_more = close_more;
1444 AutoTypes.dont_cache_failures = false;
1445 AutoTypes.maxgoalsizefactor = gsize;
1448 let applyS_tac ~dbd ~term ~params ~universe =
1449 ProofEngineTypes.mk_tactic
1453 apply_smart ~dbd ~term ~subst:[] ~universe
1454 (flags_of_params params ~for_applyS:true ()) status
1458 | CicUnification.UnificationFailure msg
1459 | CicTypeChecker.TypeCheckerFailure msg ->
1460 raise (ProofEngineTypes.Fail msg))
1465 * auto superposition target = NAME
1466 * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
1468 * - if table is omitted no superposition will be performed
1469 * - if demod_table is omitted no demodulation will be prformed
1470 * - subterms_only is passed to Indexing.superposition_right
1472 * lists are coded using _ (example: H_H1_H2)
1475 let eq_and_ty_of_goal = function
1476 | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
1478 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1481 let rec find_in_ctx i name = function
1482 | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
1483 | Some (Cic.Name name', _)::tl when name = name' -> i
1484 | _::tl -> find_in_ctx (i+1) name tl
1487 let rec position_of i x = function
1488 | [] -> assert false
1489 | j::tl when j <> x -> position_of (i+1) x tl
1494 let superposition_tac ~target ~table ~subterms_only ~demod_table status =
1495 Saturation.reset_refs();
1496 let proof,goalno = status in
1497 let curi,metasenv,_subst,pbo,pty, attrs = proof in
1498 let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
1499 let eq_uri,tty = eq_and_ty_of_goal ty in
1500 let env = (metasenv, context, CicUniv.empty_ugraph) in
1501 let names = Utils.names_of_context context in
1502 let bag = Equality.mk_equality_bag () in
1503 let eq_index, equalities, maxm,cache =
1504 find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty
1507 let what = find_in_ctx 1 target context in
1508 List.nth equalities (position_of 0 what eq_index)
1513 let others = Str.split (Str.regexp "_") table in
1514 List.map (fun other -> find_in_ctx 1 other context) others
1517 (fun other -> List.nth equalities (position_of 0 other eq_index))
1522 let index = List.fold_left Indexing.index Indexing.empty eq_other in
1524 if table = "" then maxm,[eq_what] else
1525 Indexing.superposition_right bag
1526 ~subterms_only eq_uri maxm env index eq_what
1528 debug_print (lazy ("Superposition right:"));
1529 debug_print (lazy ("\n eq: " ^ Equality.string_of_equality eq_what ~env));
1530 debug_print (lazy ("\n table: "));
1533 debug_print (lazy (" " ^ Equality.string_of_equality e ~env))) eq_other;
1534 debug_print (lazy ("\n result: "));
1535 List.iter (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1536 debug_print (lazy ("\n result (cut&paste): "));
1539 let t = Equality.term_of_equality eq_uri e in
1540 debug_print (lazy (CicPp.pp t names)))
1542 debug_print (lazy ("\n result proofs: "));
1544 debug_print (lazy (let _,p,_,_,_ = Equality.open_equality e in
1545 let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
1546 Subst.ppsubst s ^ "\n" ^
1547 CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names))) eql;
1548 if demod_table <> "" then
1551 if eql = [] then [eq_what] else eql
1554 let demod = Str.split (Str.regexp "_") demod_table in
1555 List.map (fun other -> find_in_ctx 1 other context) demod
1559 (fun demod -> List.nth equalities (position_of 0 demod eq_index))
1562 let table = List.fold_left Indexing.index Indexing.empty eq_demod in
1565 (fun (maxm,acc) e ->
1567 Indexing.demodulation_equality bag eq_uri maxm env table e
1572 let eql = List.rev eql in
1573 debug_print (lazy ("\n result [demod]: "));
1575 (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1576 debug_print (lazy ("\n result [demod] (cut&paste): "));
1579 let t = Equality.term_of_equality eq_uri e in
1580 debug_print (lazy (CicPp.pp t names)))
1586 let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) =
1587 (* argument parsing *)
1588 let string = string params in
1589 let bool = bool params in
1590 (* hacks to debug paramod *)
1591 let superposition = bool "superposition" false in
1592 let target = string "target" "" in
1593 let table = string "table" "" in
1594 let subterms_only = bool "subterms_only" false in
1595 let demod_table = string "demod_table" "" in
1596 match superposition with
1598 (* this is the ugly hack to debug paramod *)
1600 ~target ~table ~subterms_only ~demod_table (proof,goal)
1602 (* this is the real auto *)
1603 let _,metasenv,_subst,_,_, _ = proof in
1604 let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1605 let flags = flags_of_params params () in
1606 (* just for testing *)
1607 let use_library = flags.use_library in
1608 let tables,cache,newmeta =
1609 init_cache_and_tables dbd use_library flags.use_only_paramod
1610 universe (proof, goal) in
1611 let tables,cache,newmeta =
1612 if flags.close_more then
1614 tables newmeta context (proof, goal)
1615 auto_all_solutions universe cache
1616 else tables,cache,newmeta in
1617 let initial_time = Unix.gettimeofday() in
1618 let (_,oldmetasenv,_subst,_,_, _) = proof in
1621 metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[]
1623 match auto_main tables newmeta context flags universe cache [elem] with
1624 | Proved (metasenv,subst,_, tables,cache,_) ->
1626 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
1627 let proof,metasenv =
1628 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1629 proof goal subst metasenv
1632 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1633 ~newmetasenv:metasenv
1636 | Gaveup (tables,cache,maxm) ->
1639 string_of_float(Unix.gettimeofday()-.initial_time)));
1640 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1643 let auto_tac ~dbd ~params ~universe =
1644 ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
1646 let eq_of_goal = function
1647 | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1649 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1653 let demodulate_tac ~dbd ~universe (proof,goal)=
1654 let curi,metasenv,_subst,pbo,pty, attrs = proof in
1655 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1656 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1657 let initgoal = [], [], ty in
1658 let eq_uri = eq_of_goal ty in
1659 let (active,passive,bag), cache, maxm =
1660 init_cache_and_tables dbd false true universe (proof,goal) in
1661 let equalities = (Saturation.list_of_passive passive) in
1662 (* we demodulate using both actives passives *)
1665 (fun tbl eq -> Indexing.index tbl eq)
1666 (snd active) equalities
1668 let changed,(newproof,newmetasenv, newty) =
1669 Indexing.demodulation_goal bag
1670 (metasenv,context,CicUniv.empty_ugraph) table initgoal
1674 let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1676 Equality.build_goal_proof bag
1677 eq_uri newproof opengoal ty [] context metasenv
1679 let extended_metasenv = (maxm,context,newty)::metasenv in
1680 let extended_status =
1681 (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in
1682 let (status,newgoals) =
1683 ProofEngineTypes.apply_tactic
1684 (PrimitiveTactics.apply_tac ~term:proofterm)
1686 (status,maxm::newgoals)
1688 else (* if newty = ty then *)
1689 raise (ProofEngineTypes.Fail (lazy "no progress"))
1690 (*else ProofEngineTypes.apply_tactic
1691 (ReductionTactics.simpl_tac
1692 ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1695 let demodulate_tac ~dbd ~universe =
1696 ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
1698 let pp_proofterm = Equality.pp_proofterm;;