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
1188 let prunable_for_size flags s m todo =
1189 let rec aux b = function
1190 | (S _)::tl -> aux b tl
1191 | (D (_,_,T))::tl -> aux b tl
1193 (match calculate_goal_ty g s m with
1195 | Some (canonical_ctx, gty) ->
1197 Utils.weight_of_term
1198 ~consider_metas:false ~count_metas_occurrences:true gty in
1199 let newb = b || gsize > flags.maxgoalsizefactor in
1206 let prunable ty todo =
1207 let rec aux b = function
1208 | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
1209 | (D (_,_,T))::tl -> aux b tl
1217 let prunable menv subst ty todo =
1218 let rec aux = function
1219 | (S(_,k,_,_))::tl ->
1220 (match Equality.meta_convertibility_subst k ty menv with
1223 no_progress variant tl (* || aux tl*))
1224 | (D (_,_,T))::tl -> aux tl
1226 and no_progress variant = function
1227 | [] -> prerr_endline "++++++++++++++++++++++++ no_progress"; true
1228 | D ((n,_,P) as g)::tl ->
1229 (match calculate_goal_ty g subst menv with
1230 | None -> no_progress variant tl
1232 (match calculate_goal_ty g variant menv with
1233 | None -> assert false
1236 no_progress variant tl
1238 | _::tl -> no_progress variant tl
1244 let auto_main tables maxm context flags universe cache elems =
1245 auto_context := context;
1246 let rec aux tables maxm flags cache (elems : status) =
1247 (* pp_status context elems; *)
1248 (* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
1249 auto_status := elems;
1253 | (m, s, size, don, todo, fl)::orlist as status when !hint <> None ->
1255 | Some i when condition_for_hint i todo ->
1256 aux tables maxm flags cache orlist
1259 aux tables maxm flags cache elems)
1261 (* complete failure *)
1262 Gaveup (tables, cache, maxm)
1263 | (m, s, _, _, [],_)::orlist ->
1264 (* complete success *)
1265 Proved (m, s, orlist, tables, cache, maxm)
1266 | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist ->
1267 (* skip since not Prop, don't even check if closed by side-effect *)
1268 aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1269 | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
1270 (* partial success, cache g and go on *)
1271 let cache, orlist, fl, sibling_pruned =
1272 add_to_cache_and_del_from_orlist_if_green_cut
1273 g s m cache key todo orlist fl context size minsize
1275 debug_print (lazy (AutoCache.cache_print context cache));
1276 let fl = remove_s_from_fl g fl in
1277 let don = if sibling_pruned then don else op::don in
1278 aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1279 | (m, s, size, don, todo, fl)::orlist
1280 when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1281 debug_print (lazy ("FAIL: WIDTH"));
1282 (* too many goals in and generated by last th *)
1283 let cache = close_failures fl cache in
1284 aux tables maxm flags cache orlist
1285 | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
1287 (lazy ("FAIL: SIZE: "^string_of_int size ^
1288 " > " ^ string_of_int flags.maxsize ));
1289 (* we already have a too large proof term *)
1290 let cache = close_failures fl cache in
1291 aux tables maxm flags cache orlist
1292 | _ when Unix.gettimeofday () > flags.timeout ->
1294 debug_print (lazy ("FAIL: TIMEOUT"));
1295 Gaveup (tables, cache, maxm)
1296 | (m, s, size, don, (D (gno,depth,P as g))::todo, fl)::orlist as status ->
1298 match calculate_goal_ty g s m with
1300 (* closed by side effect *)
1301 debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1302 aux tables maxm flags cache ((m,s,size,don,todo, fl)::orlist)
1303 | Some (canonical_ctx, gty) ->
1305 Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty
1307 if gsize > flags.maxgoalsizefactor then
1308 (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
1309 aux tables maxm flags cache orlist)
1310 else if prunable_for_size flags s m todo then
1311 (prerr_endline ("POTO at depth: "^(string_of_int depth));
1312 aux tables maxm flags cache orlist)
1314 (* still to be proved *)
1315 (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
1316 match cache_examine cache gty with
1317 | Failed_in d when d >= depth ->
1319 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1320 let cache = close_failures fl cache in
1321 aux tables maxm flags cache orlist
1322 | UnderInspection ->
1324 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1325 let cache = close_failures fl cache in
1326 aux tables maxm flags cache orlist
1328 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1329 let s, m = put_in_subst s m g canonical_ctx t gty in
1330 aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist)
1332 | Failed_in _ when depth > 0 ->
1333 ( (* more depth or is the first time we see the goal *)
1334 if prunable m s gty todo then
1336 "FAIL: LOOP: one father is equal"));
1337 aux tables maxm flags cache orlist)
1339 let cache = cache_add_underinspection cache gty depth in
1340 auto_status := status;
1343 (lazy ("INSPECTING: " ^
1344 string_of_int gno ^ "("^ string_of_int size ^ "): "^
1346 (* elems are possible computations for proving gty *)
1347 let elems, tables, cache, maxm, flags =
1348 equational_and_applicative_case
1349 universe flags m s g gty tables cache maxm context
1352 (* this goal has failed *)
1353 let cache = close_failures ((g,gty)::fl) cache in
1354 aux tables maxm flags cache orlist
1356 (* elems = (cand,m,s,gl) *)
1357 let size_gl l = List.length
1358 (List.filter (function (_,_,P) -> true | _ -> false) l)
1361 let inj_gl gl = List.map (fun g -> D g) gl in
1362 let rec map = function
1363 | [] -> assert false
1364 | (cand,m,s,gl)::[] ->
1365 (* in the last one we add the failure *)
1367 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1369 (* we are the last in OR, we fail on g and
1370 * also on all failures implied by g *)
1371 (m,s, size + size_gl gl, don, todo, (g,gty)::fl)
1373 | (cand,m,s,gl)::tl ->
1374 (* we add the S step after gl and before todo *)
1376 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1378 (* since we are not the last in OR, we do not
1380 (m,s, size + size_gl gl, don, todo, []) :: map tl
1384 aux tables maxm flags cache elems)
1387 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1388 let cache = close_failures fl cache in
1389 aux tables maxm flags cache orlist)
1391 (aux tables maxm flags cache elems : auto_result)
1396 auto_all_solutions maxm tables universe cache context metasenv gl flags
1398 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1401 (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1403 let elems = [metasenv,[],1,[],goals,[]] in
1404 let rec aux tables maxm solutions cache elems flags =
1405 match auto_main tables maxm context flags universe cache elems with
1406 | Gaveup (tables,cache,maxm) ->
1407 solutions,cache,maxm
1408 | Proved (metasenv,subst,others,tables,cache,maxm) ->
1409 if Unix.gettimeofday () > flags.timeout then
1410 ((subst,metasenv)::solutions), cache, maxm
1412 aux tables maxm ((subst,metasenv)::solutions) cache others flags
1414 let rc = aux tables maxm [] cache elems flags in
1416 | [],cache,maxm -> [],cache,maxm
1417 | solutions,cache,maxm ->
1420 (fun (subst,newmetasenv) ->
1422 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1424 if opened = [] then Some subst else None)
1427 solutions,cache,maxm
1430 (* }}} ****************** AUTO ***************)
1432 let auto flags metasenv tables universe cache context metasenv gl =
1433 let initial_time = Unix.gettimeofday() in
1434 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1435 let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1436 let elems = [metasenv,[],1,[],goals,[]] in
1437 match auto_main tables 0 context flags universe cache elems with
1438 | Proved (metasenv,subst,_, tables,cache,_) ->
1440 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1441 Some (subst,metasenv), cache
1442 | Gaveup (tables,cache,maxm) ->
1444 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1448 let bool params name default =
1450 let s = List.assoc name params in
1451 if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
1452 else if s = "0" || s = "false" || s = "no" || s= "off" then false
1454 let msg = "Unrecognized value for parameter "^name^"\n" in
1455 let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
1456 raise (ProofEngineTypes.Fail (lazy msg))
1457 with Not_found -> default
1460 let string params name default =
1461 try List.assoc name params with
1462 | Not_found -> default
1465 let int params name default =
1466 try int_of_string (List.assoc name params) with
1467 | Not_found -> default
1469 raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
1472 let flags_of_params params ?(for_applyS=false) () =
1473 let int = int params in
1474 let bool = bool params in
1475 let close_more = bool "close_more" false in
1476 let use_paramod = bool "use_paramod" true in
1477 let use_only_paramod =
1478 if for_applyS then true else bool "paramodulation" false in
1479 let use_library = bool "library"
1480 ((AutoTypes.default_flags()).AutoTypes.use_library) in
1481 let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
1482 let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
1483 let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
1484 let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
1485 let timeout = int "timeout" 0 in
1486 { AutoTypes.maxdepth =
1487 if use_only_paramod then 2 else depth;
1488 AutoTypes.maxwidth = width;
1489 AutoTypes.maxsize = size;
1492 if for_applyS then Unix.gettimeofday () +. 30.0
1496 Unix.gettimeofday() +. (float_of_int timeout);
1497 AutoTypes.use_library = use_library;
1498 AutoTypes.use_paramod = use_paramod;
1499 AutoTypes.use_only_paramod = use_only_paramod;
1500 AutoTypes.close_more = close_more;
1501 AutoTypes.dont_cache_failures = false;
1502 AutoTypes.maxgoalsizefactor = gsize;
1505 let applyS_tac ~dbd ~term ~params ~universe =
1506 ProofEngineTypes.mk_tactic
1510 apply_smart ~dbd ~term ~subst:[] ~universe
1511 (flags_of_params params ~for_applyS:true ()) status
1515 | CicUnification.UnificationFailure msg
1516 | CicTypeChecker.TypeCheckerFailure msg ->
1517 raise (ProofEngineTypes.Fail msg))
1522 * auto superposition target = NAME
1523 * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
1525 * - if table is omitted no superposition will be performed
1526 * - if demod_table is omitted no demodulation will be prformed
1527 * - subterms_only is passed to Indexing.superposition_right
1529 * lists are coded using _ (example: H_H1_H2)
1532 let eq_and_ty_of_goal = function
1533 | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
1535 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1538 let rec find_in_ctx i name = function
1539 | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
1540 | Some (Cic.Name name', _)::tl when name = name' -> i
1541 | _::tl -> find_in_ctx (i+1) name tl
1544 let rec position_of i x = function
1545 | [] -> assert false
1546 | j::tl when j <> x -> position_of (i+1) x tl
1551 let superposition_tac ~target ~table ~subterms_only ~demod_table status =
1552 Saturation.reset_refs();
1553 let proof,goalno = status in
1554 let curi,metasenv,_subst,pbo,pty, attrs = proof in
1555 let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
1556 let eq_uri,tty = eq_and_ty_of_goal ty in
1557 let env = (metasenv, context, CicUniv.empty_ugraph) in
1558 let names = Utils.names_of_context context in
1559 let bag = Equality.mk_equality_bag () in
1560 let eq_index, equalities, maxm,cache =
1561 find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty
1564 let what = find_in_ctx 1 target context in
1565 List.nth equalities (position_of 0 what eq_index)
1570 let others = Str.split (Str.regexp "_") table in
1571 List.map (fun other -> find_in_ctx 1 other context) others
1574 (fun other -> List.nth equalities (position_of 0 other eq_index))
1579 let index = List.fold_left Indexing.index Indexing.empty eq_other in
1581 if table = "" then maxm,[eq_what] else
1582 Indexing.superposition_right bag
1583 ~subterms_only eq_uri maxm env index eq_what
1585 debug_print (lazy ("Superposition right:"));
1586 debug_print (lazy ("\n eq: " ^ Equality.string_of_equality eq_what ~env));
1587 debug_print (lazy ("\n table: "));
1590 debug_print (lazy (" " ^ Equality.string_of_equality e ~env))) eq_other;
1591 debug_print (lazy ("\n result: "));
1592 List.iter (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1593 debug_print (lazy ("\n result (cut&paste): "));
1596 let t = Equality.term_of_equality eq_uri e in
1597 debug_print (lazy (CicPp.pp t names)))
1599 debug_print (lazy ("\n result proofs: "));
1601 debug_print (lazy (let _,p,_,_,_ = Equality.open_equality e in
1602 let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
1603 Subst.ppsubst s ^ "\n" ^
1604 CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names))) eql;
1605 if demod_table <> "" then
1608 if eql = [] then [eq_what] else eql
1611 let demod = Str.split (Str.regexp "_") demod_table in
1612 List.map (fun other -> find_in_ctx 1 other context) demod
1616 (fun demod -> List.nth equalities (position_of 0 demod eq_index))
1619 let table = List.fold_left Indexing.index Indexing.empty eq_demod in
1622 (fun (maxm,acc) e ->
1624 Indexing.demodulation_equality bag eq_uri maxm env table e
1629 let eql = List.rev eql in
1630 debug_print (lazy ("\n result [demod]: "));
1632 (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1633 debug_print (lazy ("\n result [demod] (cut&paste): "));
1636 let t = Equality.term_of_equality eq_uri e in
1637 debug_print (lazy (CicPp.pp t names)))
1643 let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) =
1644 (* argument parsing *)
1645 let string = string params in
1646 let bool = bool params in
1647 (* hacks to debug paramod *)
1648 let superposition = bool "superposition" false in
1649 let target = string "target" "" in
1650 let table = string "table" "" in
1651 let subterms_only = bool "subterms_only" false in
1652 let demod_table = string "demod_table" "" in
1653 match superposition with
1655 (* this is the ugly hack to debug paramod *)
1657 ~target ~table ~subterms_only ~demod_table (proof,goal)
1659 (* this is the real auto *)
1660 let _,metasenv,_subst,_,_, _ = proof in
1661 let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1662 let flags = flags_of_params params () in
1663 (* just for testing *)
1664 let use_library = flags.use_library in
1665 let tables,cache,newmeta =
1666 init_cache_and_tables dbd use_library flags.use_only_paramod
1667 universe (proof, goal) in
1668 let tables,cache,newmeta =
1669 if flags.close_more then
1671 tables newmeta context (proof, goal)
1672 auto_all_solutions universe cache
1673 else tables,cache,newmeta in
1674 let initial_time = Unix.gettimeofday() in
1675 let (_,oldmetasenv,_subst,_,_, _) = proof in
1678 metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[]
1680 match auto_main tables newmeta context flags universe cache [elem] with
1681 | Proved (metasenv,subst,_, tables,cache,_) ->
1683 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
1684 let proof,metasenv =
1685 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1686 proof goal subst metasenv
1689 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1690 ~newmetasenv:metasenv
1693 | Gaveup (tables,cache,maxm) ->
1696 string_of_float(Unix.gettimeofday()-.initial_time)));
1697 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1700 let auto_tac ~dbd ~params ~universe =
1701 ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
1703 let eq_of_goal = function
1704 | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1706 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1710 let demodulate_tac ~dbd ~universe (proof,goal)=
1711 let curi,metasenv,_subst,pbo,pty, attrs = proof in
1712 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1713 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1714 let initgoal = [], [], ty in
1715 let eq_uri = eq_of_goal ty in
1716 let (active,passive,bag), cache, maxm =
1717 init_cache_and_tables dbd false true universe (proof,goal) in
1718 let equalities = (Saturation.list_of_passive passive) in
1719 (* we demodulate using both actives passives *)
1722 (fun tbl eq -> Indexing.index tbl eq)
1723 (snd active) equalities
1725 let changed,(newproof,newmetasenv, newty) =
1726 Indexing.demodulation_goal bag
1727 (metasenv,context,CicUniv.empty_ugraph) table initgoal
1731 let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1733 Equality.build_goal_proof bag
1734 eq_uri newproof opengoal ty [] context metasenv
1736 let extended_metasenv = (maxm,context,newty)::metasenv in
1737 let extended_status =
1738 (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in
1739 let (status,newgoals) =
1740 ProofEngineTypes.apply_tactic
1741 (PrimitiveTactics.apply_tac ~term:proofterm)
1743 (status,maxm::newgoals)
1745 else (* if newty = ty then *)
1746 raise (ProofEngineTypes.Fail (lazy "no progress"))
1747 (*else ProofEngineTypes.apply_tactic
1748 (ReductionTactics.simpl_tac
1749 ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1752 let demodulate_tac ~dbd ~universe =
1753 ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
1755 let pp_proofterm = Equality.pp_proofterm;;
1757 let revision = "$Revision$";;