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;;
834 let prune_hint = ref [];;
836 let step _ = Condition.signal cond;;
837 let give_hint n = hint := Some n;;
838 let give_prune_hint hint =
839 prune_hint := hint :: !prune_hint
846 Condition.wait cond mutex;
851 let get_auto_status _ =
852 let status = !auto_status in
853 let and_list,elems,last =
856 | (m,s,_,don,gl,fail)::tl ->
859 (fun (id,d,_ as g) ->
860 match calculate_goal_ty g s m with
861 | Some (_,x) -> Some (id,x,d) | None -> None)
865 (* these are the S goalsin the or list *)
868 (fun (m,s,_,don,gl,fail) ->
870 (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
874 (* this function eats id from a list l::[id,x] returning x, l *)
875 let eat_tail_if_eq id l =
876 let rec aux (s, l) = function
878 | ((id1,_,_),k1,c)::tl when id = id1 ->
880 | None -> aux (Some c,l) tl
881 | Some _ -> assert false)
882 | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
884 let c, l = aux (None, []) l in
887 let eat_in_parallel id l =
888 let rec aux (b,eaten, new_l as acc) l =
892 match eat_tail_if_eq id l with
893 | None, l -> aux (b@[false], eaten, new_l@[l]) tl
894 | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
898 let rec eat_all rows l =
902 match List.rev elem with
903 | ((to_eat,depth,_),k,_)::next_lunch ->
904 let b, eaten, l = eat_in_parallel to_eat l in
905 let eaten = HExtlib.list_uniq eaten in
906 let eaten = List.rev eaten in
907 let b = true (* List.hd (List.rev b) *) in
908 let rows = rows @ [to_eat,k,b,depth,eaten] in
910 | [] -> eat_all rows or_list
912 eat_all [] (List.rev orlist)
916 (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
919 (* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
920 and_list, rows, history
922 !auto_context, elems, and_list, last
925 (* Works if there is no dependency over proofs *)
926 let is_a_green_cut goalty =
927 CicUtil.is_meta_closed goalty
929 let rec first_s = function
930 | (D _)::tl -> first_s tl
931 | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
934 let list_union l1 l2 =
935 (* TODO ottimizzare compare *)
936 HExtlib.list_uniq (List.sort compare (l1 @ l1))
938 let eat_head todo id fl orlist =
939 let rec aux acc = function
941 | (m, s, _, _, todo1, fl1)::tl as orlist ->
943 match first_s todo1 with
944 | None -> orlist, acc
945 | Some (((gno,_,_),_,_,_), todo11) ->
946 (* TODO confronto tra todo da ottimizzare *)
947 if gno = id && todo11 = todo then
948 aux (list_union fl1 acc) tl
956 let close_proof p ty menv context =
958 List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
960 let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
961 naif_closure p menv context
963 (* XXX capire bene quando aggiungere alla cache *)
964 let add_to_cache_and_del_from_orlist_if_green_cut
965 g s m cache key todo orlist fl ctx size minsize
967 let cache = cache_remove_underinspection cache key in
968 (* prima per fare la irl usavamo il contesto vero e proprio e non quello
970 match calculate_closed_goal_ty g s with
971 | None -> assert false
972 | Some (canonical_ctx , gty) ->
973 let goalno,depth,sort = g in
975 let irl = mk_irl canonical_ctx in
976 let goal = Cic.Meta(goalno, irl) in
977 let proof = CicMetaSubst.apply_subst s goal in
978 let green_proof, closed_proof =
979 let b = is_a_green_cut proof in
981 b, (* close_proof proof gty m ctx *) proof
985 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
986 if is_a_green_cut key then
987 (* if the initia goal was closed, we cut alternatives *)
988 let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
989 let orlist, fl = eat_head todo goalno fl orlist in
991 if size < minsize then
992 (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
994 (* if the proof is closed we cache it *)
995 if green_proof then cache_add_success cache key proof
996 else (* cache_add_success cache key closed_proof *)
997 (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
999 cache, orlist, fl, true
1002 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
1003 if size < minsize then
1004 (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
1005 (* if the substituted goal and the proof are closed we cache it *)
1006 if is_a_green_cut gty then
1007 if green_proof then cache_add_success cache gty proof
1008 else (* cache_add_success cache gty closed_proof *)
1009 (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
1013 CicTypeChecker.type_of_aux' ~subst:s
1014 m ctx closed_proof CicUniv.oblivion_ugraph
1016 if is_a_green_cut ty then
1017 cache_add_success cache ty closed_proof
1020 | CicTypeChecker.TypeCheckerFailure _ ->*)
1021 (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
1023 cache, orlist, fl, false
1025 let close_failures (fl : fail list) (cache : cache) =
1027 (fun cache ((gno,depth,_),gty) ->
1028 debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
1029 cache_add_failure cache gty depth)
1032 let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
1033 let entry = goalno, (canonical_ctx, t,ty) in
1034 assert_subst_are_disjoint subst [entry];
1035 let subst = entry :: subst in
1036 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1039 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
1040 None,metasenv,subst ,Cic.Meta(goalno,mk_irl context),goalty, []
1043 tables maxm cache depth fake_proof goalno goalty subst context
1046 let active,passive,bag = tables in
1047 let ppterm = ppterm context in
1048 let status = (fake_proof,goalno) in
1049 if flags.use_only_paramod then
1051 debug_print (lazy ("PARAMODULATION SU: " ^
1052 string_of_int goalno ^ " " ^ ppterm goalty ));
1053 let goal_steps, saturation_steps, timeout =
1054 max_int,max_int,flags.timeout
1057 Saturation.given_clause bag maxm status active passive
1058 goal_steps saturation_steps timeout
1060 | None, active, passive, maxmeta ->
1061 [], (active,passive,bag), cache, maxmeta, flags
1062 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
1064 assert_subst_are_disjoint subst subst';
1065 let subst = subst@subst' in
1067 order_new_goals metasenv subst open_goals ppterm
1070 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1073 [(!candidate_no,proof),metasenv,subst,open_goals],
1074 (active,passive,bag),
1075 cache, maxmeta, flags
1081 ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty));
1083 Saturation.all_subsumed bag maxm status active passive
1085 assert (maxmeta >= maxm);
1088 (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
1089 assert_subst_are_disjoint subst subst';
1090 let subst = subst@subst' in
1092 order_new_goals metasenv subst open_goals ppterm
1095 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1098 (!candidate_no,proof),metasenv,subst,open_goals)
1101 res', (active,passive,bag), cache, maxmeta, flags
1106 goalty tables maxm subst fake_proof goalno depth context cand
1108 let ppterm = ppterm context in
1110 let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
1111 (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:maxm ~term:cand)
1114 debug_print (lazy (" OK: " ^ ppterm cand));
1115 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
1116 let open_goals = order_new_goals metasenv subst open_goals ppterm in
1117 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
1119 Some ((!candidate_no,cand),metasenv,subst,open_goals), tables , maxmeta
1121 | ProofEngineTypes.Fail s -> None,tables, maxm
1122 | CicUnification.Uncertain s -> None,tables, maxm
1125 let sort_new_elems =
1126 List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2)
1127 (* List.sort (fun (_,_,_,l2) (_,_,_,l1) -> List.length l1 - List.length l2) *)
1130 let applicative_case
1131 tables maxm depth subst fake_proof goalno goalty metasenv context universe
1134 let candidates = get_candidates universe cache goalty in
1135 let tables, elems, maxm =
1137 (fun (tables,elems,maxm) cand ->
1139 try_candidate goalty
1140 tables maxm subst fake_proof goalno depth context cand
1142 | None, tables,maxm -> tables,elems, maxm
1143 | Some x, tables, maxm -> tables,x::elems, maxm)
1144 (tables,[],maxm) candidates
1146 let elems = sort_new_elems elems in
1147 elems, tables, cache, maxm
1150 let equational_and_applicative_case
1151 universe flags m s g gty tables cache maxm context
1153 let goalno, depth, sort = g in
1154 let fake_proof = mk_fake_proof m s g gty context in
1155 if is_equational_case gty flags then
1156 let elems,tables,cache,maxm1, flags =
1157 equational_case tables maxm cache
1158 depth fake_proof goalno gty s context flags
1161 let more_elems, tables, cache, maxm1 =
1162 if flags.use_only_paramod then
1163 [],tables, cache, maxm
1166 tables maxm depth s fake_proof goalno
1167 gty m context universe cache
1170 elems@more_elems, tables, cache, maxm, flags
1172 let elems, tables, cache, maxm =
1173 applicative_case tables maxm depth s fake_proof goalno
1174 gty m context universe cache
1176 elems, tables, cache, maxm, flags
1178 let rec condition_for_hint i = function
1180 | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
1181 | _::tl -> condition_for_hint i tl
1183 let remove_s_from_fl (id,_,_) (fl : fail list) =
1184 let rec aux = function
1186 | ((id1,_,_),_)::tl when id = id1 -> tl
1187 | hd::tl -> hd :: aux tl
1192 let prunable_for_size flags s m todo =
1193 let rec aux b = function
1194 | (S _)::tl -> aux b tl
1195 | (D (_,_,T))::tl -> aux b tl
1197 (match calculate_goal_ty g s m with
1199 | Some (canonical_ctx, gty) ->
1201 Utils.weight_of_term
1202 ~consider_metas:false ~count_metas_occurrences:true gty in
1203 let newb = b || gsize > flags.maxgoalsizefactor in
1210 let prunable ty todo =
1211 let rec aux b = function
1212 | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
1213 | (D (_,_,T))::tl -> aux b tl
1221 let prunable menv subst ty todo =
1222 let rec aux = function
1223 | (S(_,k,_,_))::tl ->
1224 (match Equality.meta_convertibility_subst k ty menv with
1227 no_progress variant tl (* || aux tl*))
1228 | (D (_,_,T))::tl -> aux tl
1230 and no_progress variant = function
1231 | [] -> prerr_endline "++++++++++++++++++++++++ no_progress"; true
1232 | D ((n,_,P) as g)::tl ->
1233 (match calculate_goal_ty g subst menv with
1234 | None -> no_progress variant tl
1236 (match calculate_goal_ty g variant menv with
1237 | None -> assert false
1240 no_progress variant tl
1242 | _::tl -> no_progress variant tl
1247 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
1249 HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
1251 List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
1253 let filter_prune_hint l =
1254 let prune = !prune_hint in
1255 prune_hint := []; (* possible race... *)
1256 if prune = [] then l
1257 else List.filter (condition_for_prune_hint prune) l
1259 let auto_main tables maxm context flags universe cache elems =
1260 auto_context := context;
1261 let rec aux tables maxm flags cache (elems : status) =
1262 (* pp_status context elems; *)
1263 (* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
1264 auto_status := elems;
1267 let elems = filter_prune_hint elems in
1269 | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
1271 | Some i when condition_for_hint i todo ->
1272 aux tables maxm flags cache orlist
1275 aux tables maxm flags cache elems)
1277 (* complete failure *)
1278 Gaveup (tables, cache, maxm)
1279 | (m, s, _, _, [],_)::orlist ->
1280 (* complete success *)
1281 Proved (m, s, orlist, tables, cache, maxm)
1282 | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist ->
1283 (* skip since not Prop, don't even check if closed by side-effect *)
1284 aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1285 | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
1286 (* partial success, cache g and go on *)
1287 let cache, orlist, fl, sibling_pruned =
1288 add_to_cache_and_del_from_orlist_if_green_cut
1289 g s m cache key todo orlist fl context size minsize
1291 debug_print (lazy (AutoCache.cache_print context cache));
1292 let fl = remove_s_from_fl g fl in
1293 let don = if sibling_pruned then don else op::don in
1294 aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1295 | (m, s, size, don, todo, fl)::orlist
1296 when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1297 debug_print (lazy ("FAIL: WIDTH"));
1298 (* too many goals in and generated by last th *)
1299 let cache = close_failures fl cache in
1300 aux tables maxm flags cache orlist
1301 | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
1303 (lazy ("FAIL: SIZE: "^string_of_int size ^
1304 " > " ^ string_of_int flags.maxsize ));
1305 (* we already have a too large proof term *)
1306 let cache = close_failures fl cache in
1307 aux tables maxm flags cache orlist
1308 | _ when Unix.gettimeofday () > flags.timeout ->
1310 debug_print (lazy ("FAIL: TIMEOUT"));
1311 Gaveup (tables, cache, maxm)
1312 | (m, s, size, don, (D (gno,depth,P as g))::todo, fl)::orlist as status ->
1314 match calculate_goal_ty g s m with
1316 (* closed by side effect *)
1317 debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1318 aux tables maxm flags cache ((m,s,size,don,todo, fl)::orlist)
1319 | Some (canonical_ctx, gty) ->
1321 Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty
1323 if gsize > flags.maxgoalsizefactor then
1324 (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
1325 aux tables maxm flags cache orlist)
1326 else if prunable_for_size flags s m todo then
1327 (prerr_endline ("POTO at depth: "^(string_of_int depth));
1328 aux tables maxm flags cache orlist)
1330 (* still to be proved *)
1331 (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
1332 match cache_examine cache gty with
1333 | Failed_in d when d >= depth ->
1335 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1336 let cache = close_failures fl cache in
1337 aux tables maxm flags cache orlist
1338 | UnderInspection ->
1340 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1341 let cache = close_failures fl cache in
1342 aux tables maxm flags cache orlist
1344 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1345 let s, m = put_in_subst s m g canonical_ctx t gty in
1346 aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist)
1348 | Failed_in _ when depth > 0 ->
1349 ( (* more depth or is the first time we see the goal *)
1350 if prunable m s gty todo then
1352 "FAIL: LOOP: one father is equal"));
1353 aux tables maxm flags cache orlist)
1355 let cache = cache_add_underinspection cache gty depth in
1356 auto_status := status;
1359 (lazy ("INSPECTING: " ^
1360 string_of_int gno ^ "("^ string_of_int size ^ "): "^
1362 (* elems are possible computations for proving gty *)
1363 let elems, tables, cache, maxm, flags =
1364 equational_and_applicative_case
1365 universe flags m s g gty tables cache maxm context
1368 (* this goal has failed *)
1369 let cache = close_failures ((g,gty)::fl) cache in
1370 aux tables maxm flags cache orlist
1372 (* elems = (cand,m,s,gl) *)
1373 let size_gl l = List.length
1374 (List.filter (function (_,_,P) -> true | _ -> false) l)
1377 let inj_gl gl = List.map (fun g -> D g) gl in
1378 let rec map = function
1379 | [] -> assert false
1380 | (cand,m,s,gl)::[] ->
1381 (* in the last one we add the failure *)
1383 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1385 (* we are the last in OR, we fail on g and
1386 * also on all failures implied by g *)
1387 (m,s, size + size_gl gl, don, todo, (g,gty)::fl)
1389 | (cand,m,s,gl)::tl ->
1390 (* we add the S step after gl and before todo *)
1392 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1394 (* since we are not the last in OR, we do not
1396 (m,s, size + size_gl gl, don, todo, []) :: map tl
1400 aux tables maxm flags cache elems)
1403 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1404 let cache = close_failures fl cache in
1405 aux tables maxm flags cache orlist)
1407 (aux tables maxm flags cache elems : auto_result)
1412 auto_all_solutions maxm tables universe cache context metasenv gl flags
1414 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1417 (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1419 let elems = [metasenv,[],1,[],goals,[]] in
1420 let rec aux tables maxm solutions cache elems flags =
1421 match auto_main tables maxm context flags universe cache elems with
1422 | Gaveup (tables,cache,maxm) ->
1423 solutions,cache,maxm
1424 | Proved (metasenv,subst,others,tables,cache,maxm) ->
1425 if Unix.gettimeofday () > flags.timeout then
1426 ((subst,metasenv)::solutions), cache, maxm
1428 aux tables maxm ((subst,metasenv)::solutions) cache others flags
1430 let rc = aux tables maxm [] cache elems flags in
1432 | [],cache,maxm -> [],cache,maxm
1433 | solutions,cache,maxm ->
1436 (fun (subst,newmetasenv) ->
1438 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1440 if opened = [] then Some subst else None)
1443 solutions,cache,maxm
1446 (* }}} ****************** AUTO ***************)
1448 let auto flags metasenv tables universe cache context metasenv gl =
1449 let initial_time = Unix.gettimeofday() in
1450 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1451 let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1452 let elems = [metasenv,[],1,[],goals,[]] in
1453 match auto_main tables 0 context flags universe cache elems with
1454 | Proved (metasenv,subst,_, tables,cache,_) ->
1456 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1457 Some (subst,metasenv), cache
1458 | Gaveup (tables,cache,maxm) ->
1460 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1464 let bool params name default =
1466 let s = List.assoc name params in
1467 if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
1468 else if s = "0" || s = "false" || s = "no" || s= "off" then false
1470 let msg = "Unrecognized value for parameter "^name^"\n" in
1471 let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
1472 raise (ProofEngineTypes.Fail (lazy msg))
1473 with Not_found -> default
1476 let string params name default =
1477 try List.assoc name params with
1478 | Not_found -> default
1481 let int params name default =
1482 try int_of_string (List.assoc name params) with
1483 | Not_found -> default
1485 raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
1488 let flags_of_params params ?(for_applyS=false) () =
1489 let int = int params in
1490 let bool = bool params in
1491 let close_more = bool "close_more" false in
1492 let use_paramod = bool "use_paramod" true in
1493 let use_only_paramod =
1494 if for_applyS then true else bool "paramodulation" false in
1495 let use_library = bool "library"
1496 ((AutoTypes.default_flags()).AutoTypes.use_library) in
1497 let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
1498 let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
1499 let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
1500 let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
1501 let timeout = int "timeout" 0 in
1502 { AutoTypes.maxdepth =
1503 if use_only_paramod then 2 else depth;
1504 AutoTypes.maxwidth = width;
1505 AutoTypes.maxsize = size;
1508 if for_applyS then Unix.gettimeofday () +. 30.0
1512 Unix.gettimeofday() +. (float_of_int timeout);
1513 AutoTypes.use_library = use_library;
1514 AutoTypes.use_paramod = use_paramod;
1515 AutoTypes.use_only_paramod = use_only_paramod;
1516 AutoTypes.close_more = close_more;
1517 AutoTypes.dont_cache_failures = false;
1518 AutoTypes.maxgoalsizefactor = gsize;
1521 let applyS_tac ~dbd ~term ~params ~universe =
1522 ProofEngineTypes.mk_tactic
1526 apply_smart ~dbd ~term ~subst:[] ~universe
1527 (flags_of_params params ~for_applyS:true ()) status
1531 | CicUnification.UnificationFailure msg
1532 | CicTypeChecker.TypeCheckerFailure msg ->
1533 raise (ProofEngineTypes.Fail msg))
1538 * auto superposition target = NAME
1539 * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
1541 * - if table is omitted no superposition will be performed
1542 * - if demod_table is omitted no demodulation will be prformed
1543 * - subterms_only is passed to Indexing.superposition_right
1545 * lists are coded using _ (example: H_H1_H2)
1548 let eq_and_ty_of_goal = function
1549 | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
1551 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1554 let rec find_in_ctx i name = function
1555 | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
1556 | Some (Cic.Name name', _)::tl when name = name' -> i
1557 | _::tl -> find_in_ctx (i+1) name tl
1560 let rec position_of i x = function
1561 | [] -> assert false
1562 | j::tl when j <> x -> position_of (i+1) x tl
1567 let superposition_tac ~target ~table ~subterms_only ~demod_table status =
1568 Saturation.reset_refs();
1569 let proof,goalno = status in
1570 let curi,metasenv,_subst,pbo,pty, attrs = proof in
1571 let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
1572 let eq_uri,tty = eq_and_ty_of_goal ty in
1573 let env = (metasenv, context, CicUniv.empty_ugraph) in
1574 let names = Utils.names_of_context context in
1575 let bag = Equality.mk_equality_bag () in
1576 let eq_index, equalities, maxm,cache =
1577 find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty
1580 let what = find_in_ctx 1 target context in
1581 List.nth equalities (position_of 0 what eq_index)
1586 let others = Str.split (Str.regexp "_") table in
1587 List.map (fun other -> find_in_ctx 1 other context) others
1590 (fun other -> List.nth equalities (position_of 0 other eq_index))
1595 let index = List.fold_left Indexing.index Indexing.empty eq_other in
1597 if table = "" then maxm,[eq_what] else
1598 Indexing.superposition_right bag
1599 ~subterms_only eq_uri maxm env index eq_what
1601 debug_print (lazy ("Superposition right:"));
1602 debug_print (lazy ("\n eq: " ^ Equality.string_of_equality eq_what ~env));
1603 debug_print (lazy ("\n table: "));
1606 debug_print (lazy (" " ^ Equality.string_of_equality e ~env))) eq_other;
1607 debug_print (lazy ("\n result: "));
1608 List.iter (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1609 debug_print (lazy ("\n result (cut&paste): "));
1612 let t = Equality.term_of_equality eq_uri e in
1613 debug_print (lazy (CicPp.pp t names)))
1615 debug_print (lazy ("\n result proofs: "));
1617 debug_print (lazy (let _,p,_,_,_ = Equality.open_equality e in
1618 let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
1619 Subst.ppsubst s ^ "\n" ^
1620 CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names))) eql;
1621 if demod_table <> "" then
1624 if eql = [] then [eq_what] else eql
1627 let demod = Str.split (Str.regexp "_") demod_table in
1628 List.map (fun other -> find_in_ctx 1 other context) demod
1632 (fun demod -> List.nth equalities (position_of 0 demod eq_index))
1635 let table = List.fold_left Indexing.index Indexing.empty eq_demod in
1638 (fun (maxm,acc) e ->
1640 Indexing.demodulation_equality bag eq_uri maxm env table e
1645 let eql = List.rev eql in
1646 debug_print (lazy ("\n result [demod]: "));
1648 (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1649 debug_print (lazy ("\n result [demod] (cut&paste): "));
1652 let t = Equality.term_of_equality eq_uri e in
1653 debug_print (lazy (CicPp.pp t names)))
1659 let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) =
1660 (* argument parsing *)
1661 let string = string params in
1662 let bool = bool params in
1663 (* hacks to debug paramod *)
1664 let superposition = bool "superposition" false in
1665 let target = string "target" "" in
1666 let table = string "table" "" in
1667 let subterms_only = bool "subterms_only" false in
1668 let demod_table = string "demod_table" "" in
1669 match superposition with
1671 (* this is the ugly hack to debug paramod *)
1673 ~target ~table ~subterms_only ~demod_table (proof,goal)
1675 (* this is the real auto *)
1676 let _,metasenv,_subst,_,_, _ = proof in
1677 let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1678 let flags = flags_of_params params () in
1679 (* just for testing *)
1680 let use_library = flags.use_library in
1681 let tables,cache,newmeta =
1682 init_cache_and_tables dbd use_library flags.use_only_paramod
1683 universe (proof, goal) in
1684 let tables,cache,newmeta =
1685 if flags.close_more then
1687 tables newmeta context (proof, goal)
1688 auto_all_solutions universe cache
1689 else tables,cache,newmeta in
1690 let initial_time = Unix.gettimeofday() in
1691 let (_,oldmetasenv,_subst,_,_, _) = proof in
1694 metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[]
1696 match auto_main tables newmeta context flags universe cache [elem] with
1697 | Proved (metasenv,subst,_, tables,cache,_) ->
1699 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
1700 let proof,metasenv =
1701 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1702 proof goal subst metasenv
1705 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1706 ~newmetasenv:metasenv
1709 | Gaveup (tables,cache,maxm) ->
1712 string_of_float(Unix.gettimeofday()-.initial_time)));
1713 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1716 let auto_tac ~dbd ~params ~universe =
1717 ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
1719 let eq_of_goal = function
1720 | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1722 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1726 let demodulate_tac ~dbd ~universe (proof,goal)=
1727 let curi,metasenv,_subst,pbo,pty, attrs = proof in
1728 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1729 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1730 let initgoal = [], [], ty in
1731 let eq_uri = eq_of_goal ty in
1732 let (active,passive,bag), cache, maxm =
1733 init_cache_and_tables dbd false true universe (proof,goal) in
1734 let equalities = (Saturation.list_of_passive passive) in
1735 (* we demodulate using both actives passives *)
1738 (fun tbl eq -> Indexing.index tbl eq)
1739 (snd active) equalities
1741 let changed,(newproof,newmetasenv, newty) =
1742 Indexing.demodulation_goal bag
1743 (metasenv,context,CicUniv.empty_ugraph) table initgoal
1747 let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1749 Equality.build_goal_proof bag
1750 eq_uri newproof opengoal ty [] context metasenv
1752 let extended_metasenv = (maxm,context,newty)::metasenv in
1753 let extended_status =
1754 (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in
1755 let (status,newgoals) =
1756 ProofEngineTypes.apply_tactic
1757 (PrimitiveTactics.apply_tac ~term:proofterm)
1759 (status,maxm::newgoals)
1761 else (* if newty = ty then *)
1762 raise (ProofEngineTypes.Fail (lazy "no progress"))
1763 (*else ProofEngineTypes.apply_tactic
1764 (ReductionTactics.simpl_tac
1765 ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1768 let demodulate_tac ~dbd ~universe =
1769 ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
1771 let pp_proofterm = Equality.pp_proofterm;;
1773 let revision = "$Revision$";;
1774 let size_and_depth context metasenv t = 100, 100