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 into account *)
38 let naif_closure 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 ("x_"^string_of_int n),
60 CicSubstitution.lift n ty,t))
66 (* functions for retrieving theorems *)
68 exception FillingFailure of AutoCache.cache * int
70 let rec unfold context = function
71 | Cic.Prod(name,s,t) ->
72 let t' = unfold ((Some (name,Cic.Decl s))::context) t in
74 | t -> ProofEngineReduction.unfold context t
76 let find_library_theorems dbd proof goal =
77 let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
78 let terms = List.map CicUtil.term_of_uri univ in
81 (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)))
84 let find_context_theorems context metasenv =
87 (fun (res,i) ctxentry ->
89 | Some (_,Cic.Decl t) ->
90 (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
91 | Some (_,Cic.Def (_,Some t)) ->
92 (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
93 | Some (_,Cic.Def (_,None)) ->
96 CicTypeChecker.type_of_aux'
97 metasenv context t CicUniv.empty_ugraph
104 let rec is_an_equality = function
105 | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _]
106 when (LibraryObjects.is_eq_URI uri) -> true
107 | Cic.Prod (_, _, t) -> is_an_equality t
111 let partition_equalities =
112 List.partition (fun (_,ty) -> is_an_equality ty)
115 let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;;
118 let is_unit_equation context metasenv oldnewmeta term =
119 let head, metasenv, args, newmeta =
120 TermUtil.saturate_term oldnewmeta metasenv context term 0
122 let propositional_args =
126 let _,_,mt = CicUtil.lookup_meta i metasenv in
128 CicTypeChecker.type_of_aux' metasenv context mt
132 CicReduction.are_convertible ~metasenv context
133 sort (Cic.Sort Cic.Prop) u
135 if b then Some i else None
139 if propositional_args = [] then
140 let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
141 Some (args,metasenv,newmetas,head,newmeta)
145 let get_candidates universe cache t =
147 (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
150 (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^
151 (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
152 debug_print debug_msg;
156 let only signature context t =
158 let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
159 let consts = MetadataConstraints.constants_of ty in
160 let b = MetadataConstraints.UriManagerSet.subset consts signature in
164 let ty' = unfold context ty in
165 let consts' = MetadataConstraints.constants_of ty' in
166 MetadataConstraints.UriManagerSet.subset consts' signature
171 let not_default_eq_term t =
173 let uri = CicUtil.uri_of_term t in
174 not (LibraryObjects.in_eq_URIs uri)
175 with Invalid_argument _ -> true
177 let retrieve_equations signature universe cache context=
178 match LibraryObjects.eq_URI() with
181 let eq_uri = UriManager.strip_xpointer eq_uri in
182 let fake= Cic.Meta(-1,[]) in
183 let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
184 let candidates = get_candidates universe cache fake_eq in
185 (* defaults eq uris are built-in in auto *)
186 let candidates = List.filter not_default_eq_term candidates in
187 let candidates = List.filter (only signature context) candidates in
188 List.iter (fun t -> debug_print (lazy (CicPp.ppterm t))) candidates;
191 let build_equality bag head args proof newmetas maxmeta =
193 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
195 if args = [] then proof else Cic.Appl (proof::args)
197 let o = !Utils.compare_terms t1 t2 in
198 let stat = (ty,t1,t2,o) in
199 (* let w = compute_equality_weight stat in *)
201 let proof = Equality.Exact p in
202 let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
203 (* to clean the local context of metas *)
204 Equality.fix_metas bag maxmeta e
208 let partition_unit_equalities context metasenv newmeta bag equations =
210 (fun (units,other,maxmeta)(t,ty) ->
211 match is_unit_equation context metasenv maxmeta ty with
212 | Some (args,metasenv,newmetas,head,newmeta') ->
213 let maxmeta,equality =
214 build_equality bag head args t newmetas newmeta' in
215 equality::units,other,maxmeta
217 units,(t,ty)::other,maxmeta)
218 ([],[],newmeta) equations
221 (Saturation.make_active [],
222 Saturation.make_passive [],
223 Equality.mk_equality_bag)
225 let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
226 (* the local cache in initially empty *)
227 let cache = AutoCache.cache_empty in
228 let _, metasenv, _, _, _ = proof in
229 let signature = MetadataQuery.signature_of metasenv goal in
230 let newmeta = CicMkImplicit.new_meta metasenv [] in
231 let _,context,_ = CicUtil.lookup_meta goal metasenv in
232 let ct = find_context_theorems context metasenv in
234 (lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct))));
237 find_library_theorems dbd metasenv goal
240 (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
241 let cache = cache_add_list cache context (ct@lt) in
243 retrieve_equations signature universe cache context in
245 (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
250 CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
251 (* retrieve_equations could also return flexible terms *)
252 if is_an_equality ty then Some(t,ty)
255 let ty' = unfold context ty in
256 if is_an_equality ty' then Some(t,ty') else None
257 with _ -> None) (* catturare l'eccezione giusta di unfold *)
259 let bag = Equality.mk_equality_bag () in
260 let units, other_equalities, newmeta =
261 partition_unit_equalities context metasenv newmeta bag eqs_and_types in
262 (* let env = (metasenv, context, CicUniv.empty_ugraph) in
265 match LibraryObjects.eq_URI() with
266 | None ->assert false
267 | Some eq_uri -> eq_uri in
268 Saturation.simplify_equalities bag eq_uri env units in *)
269 let passive = Saturation.make_passive units in
270 let no = List.length units in
271 let active = Saturation.make_active [] in
272 let active,passive,newmeta =
273 if paramod then active,passive,newmeta
275 Saturation.pump_actives
276 context bag newmeta active passive (no+1) infinity
278 (active,passive,bag),cache,newmeta
280 let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast =
281 let head, metasenv, args, newmeta =
282 TermUtil.saturate_term oldnewmeta metasenv context term 0
284 let propositional_args =
288 let _,_,mt = CicUtil.lookup_meta i metasenv in
290 CicTypeChecker.type_of_aux' metasenv context mt
294 CicReduction.are_convertible ~metasenv context
295 sort (Cic.Sort Cic.Prop) u
297 if b then Some i else None
301 let results,cache,newmeta =
302 if propositional_args = [] then
303 let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
304 [args,metasenv,newmetas,head,newmeta],cache,newmeta
308 None,metasenv,term,term (* term non e' significativo *)
312 {AutoTypes.default_flags() with
313 AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
314 maxwidth = 2;maxdepth = 2;
315 use_paramod=true;use_only_paramod=false}
317 {AutoTypes.default_flags() with
318 AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
319 maxwidth = 2;maxdepth = 4;
320 use_paramod=true;use_only_paramod=false}
322 match auto newmeta tables universe cache context metasenv propositional_args flags with
323 | [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
324 | substs,cache,newmeta ->
328 CicMetaSubst.apply_subst_metasenv subst metasenv
330 let head = CicMetaSubst.apply_subst subst head in
332 List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
334 let args = List.map (CicMetaSubst.apply_subst subst) args in
335 let newm = CicMkImplicit.new_meta metasenv subst in
336 args,metasenv,newmetas,head,max newm newmeta)
337 substs, cache, newmeta
339 results,cache,newmeta
341 let build_equalities auto context metasenv tables universe cache newmeta equations =
343 (fun (facts,cache,newmeta) (t,ty) ->
344 (* in any case we add the equation to the cache *)
345 let cache = AutoCache.cache_add_list cache context [(t,ty)] in
347 let saturated,cache,newmeta =
348 fill_hypothesis context metasenv newmeta ty tables universe cache auto true
350 let (active,passive,bag) = tables in
351 let eqs,bag,newmeta =
353 (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') ->
354 let maxmeta,equality =
355 build_equality bag head args t newmetas newmeta'
357 equality::acc,bag,maxmeta)
358 ([],bag,newmeta) saturated
360 (eqs@facts, cache, newmeta)
361 with FillingFailure (cache,newmeta) ->
362 (* if filling hypothesis fails we add the equation to
364 (facts,cache,newmeta)
366 ([],cache,newmeta) equations
368 let close_more tables maxmeta context status auto universe cache =
369 let (active,passive,bag) = tables in
370 let proof, goalno = status in
371 let _, metasenv,_,_, _ = proof in
372 let signature = MetadataQuery.signature_of metasenv goalno in
373 let equations = retrieve_equations signature universe cache context in
378 CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
379 (* retrieve_equations could also return flexible terms *)
380 if is_an_equality ty then Some(t,ty) else None)
382 let units, cache, maxm =
383 build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in
384 debug_print (lazy (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
385 string_of_int maxm));
387 (fun e -> debug_print (lazy (Equality.string_of_equality e)))
389 debug_print (lazy ">>>>>>>>>>>>>>>>>>>>>>");
390 let passive = Saturation.add_to_passive units passive in
391 let no = List.length units in
392 debug_print (lazy ("No = " ^ (string_of_int no)));
393 let active,passive,newmeta =
394 Saturation.pump_actives context bag maxm active passive (no+1) infinity
396 (active,passive,bag),cache,newmeta
398 let find_context_equalities
399 maxmeta bag context proof (universe:Universe.universe) cache
401 let module C = Cic in
402 let module S = CicSubstitution in
403 let module T = CicTypeChecker in
404 let _,metasenv,_,_, _ = proof in
405 let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
406 (* if use_auto is true, we try to close the hypothesis of equational
407 statements using auto; a naif, and probably wrong approach *)
408 let rec aux cache index newmeta = function
409 | [] -> [], newmeta,cache
410 | (Some (_, C.Decl (term)))::tl ->
413 (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
414 let do_find context term =
416 | C.Prod (name, s, t) when is_an_equality t ->
419 let term = S.lift index term in
420 let saturated,cache,newmeta =
421 fill_hypothesis context metasenv newmeta term
422 empty_tables universe cache default_auto false
426 (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
427 let newmeta, equality =
429 bag head args (Cic.Rel index) newmetas (max newmeta newmeta')
431 equality::acc, newmeta + 1)
432 ([],newmeta) saturated
435 with FillingFailure (cache,newmeta) ->
437 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
438 when LibraryObjects.is_eq_URI uri ->
439 let term = S.lift index term in
441 build_equality bag term [] (Cic.Rel index) [] newmeta
443 [e], (newmeta+1),cache
444 | _ -> [], newmeta, cache
446 let eqs, newmeta, cache = do_find context term in
447 let rest, newmeta,cache = aux cache (index+1) newmeta tl in
448 List.map (fun x -> index,x) eqs @ rest, newmeta, cache
450 aux cache (index+1) newmeta tl
452 let il, maxm, cache =
453 aux cache 1 newmeta context
455 let indexes, equalities = List.split il in
456 indexes, equalities, maxm, cache
459 (***************** applyS *******************)
461 let new_metasenv_and_unify_and_t
462 dbd flags universe proof goal ?tables newmeta' metasenv'
463 context term' ty termty goal_arity
465 let (consthead,newmetasenv,arguments,_) =
466 TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
468 match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
470 let proof',oldmetasenv =
471 let (puri,metasenv,pbo,pty, attrs) = proof in
472 (puri,newmetasenv,pbo,pty, attrs),metasenv
474 let goal_for_paramod =
475 match LibraryObjects.eq_URI () with
477 Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
478 | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
480 let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
481 let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
482 let proof'' = let uri,_,p,ty, attrs = proof' in uri,metasenv_for_paramod,p,ty, attrs in
483 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
485 ProofEngineTypes.apply_tactic
486 (EqualityTactics.rewrite_tac ~direction:`RightToLeft
487 ~pattern:(ProofEngineTypes.conclusion_pattern None)
488 (Cic.Meta(newmeta,irl)) [])
491 let goal = match goals with [g] -> g | _ -> assert false in
492 let subst, (proof'''', _), _ =
493 PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
496 let (active, passive,bag), cache, maxmeta =
497 init_cache_and_tables dbd flags.use_library true universe (proof'''',newmeta)
499 Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
500 max_int max_int flags.timeout
503 raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
504 | Some (_,proof''''',_), active,passive,_ ->
506 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
507 ~newmetasenv:(let _,m,_,_, _ = proof''''' in m), active, passive
510 let rec count_prods context ty =
511 match CicReduction.whd context ty with
512 Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
515 let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
516 let module T = CicTypeChecker in
517 let module R = CicReduction in
518 let module C = Cic in
519 let (_,metasenv,_,_, _) = proof in
520 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
521 let newmeta = CicMkImplicit.new_meta metasenv subst in
522 let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
524 C.Var (uri,exp_named_subst) ->
525 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
526 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
529 exp_named_subst_diff,newmeta',newmetasenvfragment,
530 C.Var (uri,exp_named_subst')
531 | C.Const (uri,exp_named_subst) ->
532 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
533 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
536 exp_named_subst_diff,newmeta',newmetasenvfragment,
537 C.Const (uri,exp_named_subst')
538 | C.MutInd (uri,tyno,exp_named_subst) ->
539 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
540 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
543 exp_named_subst_diff,newmeta',newmetasenvfragment,
544 C.MutInd (uri,tyno,exp_named_subst')
545 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
546 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
547 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
550 exp_named_subst_diff,newmeta',newmetasenvfragment,
551 C.MutConstruct (uri,tyno,consno,exp_named_subst')
552 | _ -> [],newmeta,[],term
554 let metasenv' = metasenv@newmetasenvfragment in
556 CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
558 let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
559 let goal_arity = count_prods context ty in
560 let subst, proof, gl, active, passive =
561 new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
562 newmeta' metasenv' context term' ty termty goal_arity
564 subst, proof, gl, active, passive
567 (****************** AUTO ********************)
569 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
570 let ugraph = CicUniv.empty_ugraph;;
571 let typeof = CicTypeChecker.type_of_aux';;
573 let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
576 let is_in_prop context subst metasenv ty =
577 let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
578 fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
581 let assert_proof_is_valid proof metasenv context goalty =
584 let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
585 let b,_ = CicReduction.are_convertible context ty goalty u in
589 List.map (function None -> None | Some (x,_) -> Some x) context
591 debug_print (lazy ("PROOF:" ^ CicPp.pp proof names));
592 debug_print (lazy ("PROOFTY:" ^ CicPp.pp ty names));
593 debug_print (lazy ("GOAL:" ^ CicPp.pp goalty names));
594 debug_print (lazy ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv));
601 let assert_subst_are_disjoint subst subst' =
604 (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
609 let split_goals_in_prop metasenv subst gl =
612 let _,context,ty = CicUtil.lookup_meta g metasenv in
614 let sort,u = typeof ~subst metasenv context ty ugraph in
616 CicReduction.are_convertible
617 ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
620 | CicTypeChecker.AssertFailure s
621 | CicTypeChecker.TypeCheckerFailure s ->
623 (lazy ("NON TIPA" ^ ppterm context (CicMetaSubst.apply_subst subst ty)));
626 (* FIXME... they should type! *)
630 let split_goals_with_metas metasenv subst gl =
633 let _,context,ty = CicUtil.lookup_meta g metasenv in
634 let ty = CicMetaSubst.apply_subst subst ty in
635 CicUtil.is_meta_closed ty)
639 let order_new_goals metasenv subst open_goals ppterm =
640 let prop,rest = split_goals_in_prop metasenv subst open_goals in
641 let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
643 (List.map (fun x -> x,P) (closed_prop @ open_prop))
645 (List.map (fun x -> x,T) rest)
650 let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals
652 debug_print (lazy (" OPEN: "^
656 | (i,t,P) -> string_of_int i ^ ":"^ppterm t^ "Prop"
657 | (i,t,T) -> string_of_int i ^ ":"^ppterm t^ "Type")
662 let is_an_equational_goal = function
663 | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
668 let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
671 let calculate_timeout flags =
672 if flags.timeout = 0. then
673 (debug_print (lazy "AUTO WITH NO TIMEOUT");
674 {flags with timeout = infinity})
678 let is_equational_case goalty flags =
679 let ensure_equational t =
680 if is_an_equational_goal t then true
683 let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
684 raise (ProofEngineTypes.Fail (lazy msg))
687 (flags.use_paramod && is_an_equational_goal goalty) ||
688 (flags.use_only_paramod && ensure_equational goalty)
691 let cache_add_success sort cache k v =
692 if sort = P then cache_add_success cache k v else cache_remove_underinspection
697 type menv = Cic.metasenv
698 type subst = Cic.substitution
699 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
700 let candidate_no = ref 0;;
701 type candidate = int * Cic.term
702 type cache = AutoCache.cache
704 Saturation.active_table * Saturation.passive_table * Equality.equality_bag
707 (* the goal (mainly for depth) and key of the goal *)
708 goal * AutoCache.cache_key
710 (* goal has to be proved *)
712 (* goal has to be cached as a success obtained using candidate as the first
714 | S of goal * AutoCache.cache_key * candidate * int
716 (* menv, subst, size, operations to do, failures to cache if any op fails *)
717 menv * subst * int * op list * fail list
719 (* list of computations that may lead to the solution: all op list will
720 * end with the same (S(g,_)) *)
723 (* menv, subst, alternatives, tables, cache, maxmeta *)
724 | Proved of menv * subst * elem list * tables * cache * int
725 | Gaveup of tables * cache * int
728 (* the status exported to the external observer *)
730 (* context, (goal,candidate) list, and_list, history *)
731 Cic.context * (Cic.term * (int * Cic.term) list) list *
732 Cic.term list * Cic.term list
735 let rec aux acc = function
736 | (D g)::tl -> aux (acc@[g]) tl
742 List.filter (function (_,_,P) -> true | _ -> false) l
746 let rec aux acc = function
747 | (D g)::tl -> aux (acc@[g]) tl
748 | (S _)::tl -> aux acc tl
753 let calculate_goal_ty (goalno,_,_) s m =
755 let _,cc,goalty = CicUtil.lookup_meta goalno m in
756 (* XXX applicare la subst al contesto? *)
757 Some (cc, CicMetaSubst.apply_subst s goalty)
758 with CicUtil.Meta_not_found i when i = goalno -> None
760 let calculate_closed_goal_ty (goalno,_,_) s =
762 let cc,_,goalty = List.assoc goalno s in
763 (* XXX applicare la subst al contesto? *)
764 Some (cc, CicMetaSubst.apply_subst s goalty)
765 with Not_found -> None
767 let pp_status ctx status =
769 let names = Utils.names_of_context ctx in
772 ProofEngineReduction.replace
773 ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
774 ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
778 let string_of_do m s (gi,_,_ as g) d =
779 match calculate_goal_ty g s m with
780 | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
781 | None -> Printf.sprintf "D(%d, _, %d)" gi d
783 let string_of_s m su k (ci,ct) gi =
784 Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp ct) ci
786 let string_of_ol m su l =
790 | D (g,d,s) -> string_of_do m su (g,d,s) d
791 | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
794 let string_of_fl m s fl =
796 (List.map (fun ((i,_,_),ty) ->
797 Printf.sprintf "(%d, %s)" i (pp ty)) fl)
799 let rec aux = function
802 Printf.eprintf "< [%s] ;;; [%s]>\n"
803 (string_of_ol m s ol) (string_of_fl m s fl);
806 Printf.eprintf "-------------------------- status -------------------\n";
808 Printf.eprintf "-----------------------------------------------------\n";
811 let auto_status = ref [] ;;
812 let auto_context = ref [];;
813 let in_pause = ref false;;
814 let pause b = in_pause := b;;
815 let cond = Condition.create ();;
816 let mutex = Mutex.create ();;
817 let hint = ref None;;
819 let step _ = Condition.signal cond;;
820 let give_hint n = hint := Some n;;
826 Condition.wait cond mutex;
831 let get_auto_status _ =
832 let status = !auto_status in
834 debug_print "status:";
835 List.iter (fun ((cand,ty),_,_,gl) ->
836 Printf.eprintf "cand: %s; ty: %s; gl: %d\n"
837 (CicPp.ppterm cand) (CicPp.ppterm ty) (List.length gl)) status;
839 let and_list,elems,last =
842 | (m,s,_,gl,fail)::tl ->
846 (fun g -> calculate_goal_ty g s m) (d_goals gl))
849 (* these are the S goalsin the or list *)
852 (fun (m,s,_,gl,fail) ->
854 (function S (g,k,c,_) -> Some (g,k,c) | _ -> None) gl)
857 (* this function eats id from a list l::[id,x] returning x, l *)
858 let eat_tail_if_eq id l =
859 match (List.rev l) with
860 | ((id1,_,_),k1,c)::tl when id = id1 -> Some c, List.rev tl
863 let eat_in_parallel id l =
864 let rec aux (eaten, new_l as acc) l =
868 match eat_tail_if_eq id l with
869 | None, l -> aux (eaten, new_l@[l]) tl
870 | Some t,l -> aux (eaten@[t], new_l@[l]) tl
874 let rec eat_all rows l =
878 match List.rev elem with
879 | ((to_eat,_,_),k,_)::next_lunch ->
880 let eaten, l = eat_in_parallel to_eat l in
881 let eaten = HExtlib.list_uniq eaten in
882 let rows = rows @ [k,eaten] in
884 | [] -> eat_all rows or_list
890 (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
893 (* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
894 and_list, rows, history
896 !auto_context, elems, and_list, last
899 (* Works if there is no dependency over proofs *)
900 let is_a_green_cut goalty =
901 CicUtil.is_meta_closed goalty
903 let rec first_s = function
904 | (D _)::tl -> first_s tl
905 | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
908 let list_union l1 l2 =
909 (* TODO ottimizzare compare *)
910 HExtlib.list_uniq (List.sort compare (l1 @ l1))
912 let eat_head todo id fl orlist =
913 let rec aux acc = function
915 | (m, s, _, todo1, fl1)::tl as orlist ->
917 match first_s todo1 with
918 | None -> orlist, acc
919 | Some (((gno,_,_),_,_,_), todo11) ->
920 (* TODO confronto tra todo da ottimizzare *)
921 if gno = id && todo11 = todo then
922 aux (list_union fl1 acc) tl
930 let close_proof p ty menv context =
932 List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
934 let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
935 naif_closure p menv context
937 (* XXX capire bene quando aggiungere alla cache *)
938 let add_to_cache_and_del_from_orlist_if_green_cut
939 g s m cache key todo orlist fl ctx size minsize
941 let cache = cache_remove_underinspection cache key in
942 (* prima per fare la irl usavamo il contesto vero e proprio e non quello
944 match calculate_closed_goal_ty g s with
945 | None -> assert false
946 | Some (canonical_ctx , gty) ->
947 let goalno,depth,sort = g in
949 let irl = mk_irl canonical_ctx in
950 let goal = Cic.Meta(goalno, irl) in
951 let proof = CicMetaSubst.apply_subst s goal in
952 let green_proof, closed_proof =
953 let b = is_a_green_cut proof in
955 b, (* close_proof proof gty m ctx *) proof
959 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
960 if is_a_green_cut key then
961 (* if the initia goal was closed, we cut alternatives *)
962 let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
963 let orlist, fl = eat_head todo goalno fl orlist in
965 if size < minsize then
966 (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
968 (* if the proof is closed we cache it *)
969 if green_proof then cache_add_success cache key proof
970 else (* cache_add_success cache key closed_proof *)
971 (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
976 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
977 if size < minsize then
978 (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
979 (* if the substituted goal and the proof are closed we cache it *)
980 if is_a_green_cut gty then
981 if green_proof then cache_add_success cache gty proof
982 else (* cache_add_success cache gty closed_proof *)
983 (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
987 CicTypeChecker.type_of_aux' ~subst:s
988 m ctx closed_proof CicUniv.oblivion_ugraph
990 if is_a_green_cut ty then
991 cache_add_success cache ty closed_proof
994 | CicTypeChecker.TypeCheckerFailure _ ->*)
995 (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
999 let close_failures (fl : fail list) (cache : cache) =
1001 (fun cache ((gno,depth,_),gty) ->
1002 debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
1003 cache_add_failure cache gty depth)
1006 let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
1007 let entry = goalno, (canonical_ctx, t,ty) in
1008 assert_subst_are_disjoint subst [entry];
1009 let subst = entry :: subst in
1010 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1013 let mk_fake_proof metasenv (goalno,_,_) goalty context =
1014 None,metasenv,Cic.Meta(goalno,mk_irl context),goalty, []
1017 tables maxm cache depth fake_proof goalno goalty subst context
1020 let active,passive,bag = tables in
1021 let ppterm = ppterm context in
1022 let status = (fake_proof,goalno) in
1023 if flags.use_only_paramod then
1025 debug_print (lazy ("PARAMODULATION SU: " ^
1026 string_of_int goalno ^ " " ^ ppterm goalty ));
1027 let goal_steps, saturation_steps, timeout =
1028 max_int,max_int,flags.timeout
1031 Saturation.given_clause bag maxm status active passive
1032 goal_steps saturation_steps timeout
1034 | None, active, passive, maxmeta ->
1035 [], (active,passive,bag), cache, maxmeta, flags
1036 | Some(subst',(_,metasenv,proof,_, _),open_goals),active,
1038 assert_subst_are_disjoint subst subst';
1039 let subst = subst@subst' in
1041 order_new_goals metasenv subst open_goals ppterm
1044 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1047 [(!candidate_no,proof),metasenv,subst,open_goals],
1048 (active,passive,bag),
1049 cache, maxmeta, flags
1055 ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty));
1057 Saturation.all_subsumed bag maxm status active passive
1059 assert (maxmeta >= maxm);
1062 (fun subst',(_,metasenv,proof,_, _),open_goals ->
1063 assert_subst_are_disjoint subst subst';
1064 let subst = subst@subst' in
1066 order_new_goals metasenv subst open_goals ppterm
1069 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1072 (!candidate_no,proof),metasenv,subst,open_goals)
1075 res', (active,passive,bag), cache, maxmeta, flags
1080 goalty tables maxm subst fake_proof goalno depth context cand
1082 let ppterm = ppterm context in
1084 let subst', ((_,metasenv,_,_, _), open_goals), maxmeta =
1085 PrimitiveTactics.apply_with_subst
1086 ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
1088 debug_print (lazy (" OK: " ^ ppterm cand));
1089 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
1090 let subst = subst' in
1091 let open_goals = order_new_goals metasenv subst open_goals ppterm in
1092 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
1094 Some ((!candidate_no,cand),metasenv,subst,open_goals), tables , maxmeta
1096 | ProofEngineTypes.Fail s -> None,tables, maxm
1097 | CicUnification.Uncertain s -> None,tables, maxm
1100 let sort_new_elems =
1101 List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2)
1104 let applicative_case
1105 tables maxm depth subst fake_proof goalno goalty metasenv context universe
1108 let candidates = get_candidates universe cache goalty in
1109 let tables, elems, maxm =
1111 (fun (tables,elems,maxm) cand ->
1113 try_candidate goalty
1114 tables maxm subst fake_proof goalno depth context cand
1116 | None, tables,maxm -> tables,elems, maxm
1117 | Some x, tables, maxm -> tables,x::elems, maxm)
1118 (tables,[],maxm) candidates
1120 let elems = sort_new_elems elems in
1121 elems, tables, cache, maxm
1124 let equational_and_applicative_case
1125 universe flags m s g gty tables cache maxm context
1127 let goalno, depth, sort = g in
1128 let fake_proof = mk_fake_proof m g gty context in
1129 if is_equational_case gty flags then
1130 let elems,tables,cache,maxm1, flags =
1131 equational_case tables maxm cache
1132 depth fake_proof goalno gty s context flags
1135 let more_elems, tables, cache, maxm1 =
1136 if flags.use_only_paramod then
1137 [],tables, cache, maxm
1140 tables maxm depth s fake_proof goalno
1141 gty m context universe cache
1144 elems@more_elems, tables, cache, maxm, flags
1146 let elems, tables, cache, maxm =
1147 applicative_case tables maxm depth s fake_proof goalno
1148 gty m context universe cache
1150 elems, tables, cache, maxm, flags
1152 let rec first_s_cand = function
1154 | S (_,_,(i,_),_):: _ -> i
1155 | _::tl -> first_s_cand tl
1157 let remove_s_from_fl (id,_,_) (fl : fail list) =
1158 let rec aux = function
1160 | ((id1,_,_),_)::tl when id = id1 -> tl
1161 | hd::tl -> hd :: aux tl
1165 let auto_main tables maxm context flags universe cache elems =
1166 auto_context := context;
1167 let rec aux tables maxm flags cache (elems : status) =
1168 (* pp_status context elems; *)
1171 (* complete failure *)
1172 Gaveup (tables, cache, maxm)
1173 | (m, s, _, [],_)::orlist ->
1174 (* complete success *)
1175 Proved (m, s, orlist, tables, cache, maxm)
1176 | (m, s, size, (D (_,_,T))::todo, fl)::orlist ->
1177 (* skip since not Prop, don't even check if closed by side-effect *)
1178 aux tables maxm flags cache ((m, s, size, todo, fl)::orlist)
1179 | (m, s, size, (S(g, key, c,minsize))::todo, fl)::orlist ->
1180 (* partial success, cache g and go on *)
1181 let cache, orlist, fl =
1182 add_to_cache_and_del_from_orlist_if_green_cut
1183 g s m cache key todo orlist fl context size minsize
1185 debug_print (lazy (AutoCache.cache_print context cache));
1186 let fl = remove_s_from_fl g fl in
1187 aux tables maxm flags cache ((m, s, size, todo, fl)::orlist)
1188 | (m, s, size, todo, fl)::orlist
1189 when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1190 debug_print (lazy ("FAIL: WIDTH"));
1191 (* too many goals in and generated by last th *)
1192 let cache = close_failures fl cache in
1193 aux tables maxm flags cache orlist
1194 | (m, s, size, todo, fl)::orlist
1195 when size > flags.maxsize ->
1196 debug_print (lazy ("FAIL: SIZE"));
1197 (* we already have a too large proof term *)
1198 let cache = close_failures fl cache in
1199 aux tables maxm flags cache orlist
1200 | _ when Unix.gettimeofday () > flags.timeout ->
1202 debug_print (lazy ("FAIL: SIZE"));
1203 Gaveup (tables, cache, maxm)
1204 | (m, s, size, (D (gno,depth,P as g))::todo, fl)::orlist as status ->
1206 match calculate_goal_ty g s m with
1208 (* closed by side effect *)
1209 debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1210 aux tables maxm flags cache ((m,s,size,todo, fl)::orlist)
1211 | Some (canonical_ctx, gty) ->
1212 (* still to be proved *)
1213 debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
1214 debug_print (lazy (AutoCache.cache_print context cache));
1215 match cache_examine cache gty with
1216 | Failed_in d when d >= depth ->
1218 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1219 let cache = close_failures fl cache in
1220 aux tables maxm flags cache orlist
1221 | UnderInspection ->
1223 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1224 let cache = close_failures fl cache in
1225 aux tables maxm flags cache orlist
1227 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1228 let s, m = put_in_subst s m g canonical_ctx t gty in
1229 aux tables maxm flags cache ((m, s, size, todo, fl)::orlist)
1231 | Failed_in _ when depth > 0 ->
1233 | Some i when first_s_cand todo <> i ->
1234 aux tables maxm flags cache orlist
1235 | _ -> hint := None;
1236 (* more depth or is the first time we see the goal *)
1237 let cache = cache_add_underinspection cache gty depth in
1238 auto_status := status;
1241 (lazy ("INSPECTING: " ^
1242 string_of_int gno ^ "("^ string_of_int size ^ "): "^CicPp.ppterm gty));
1243 (* elems are possible computations for proving gty *)
1244 let elems, tables, cache, maxm, flags =
1245 equational_and_applicative_case
1246 universe flags m s g gty tables cache maxm context
1249 (* this goal has failed *)
1250 let cache = close_failures ((g,gty)::fl) cache in
1251 aux tables maxm flags cache orlist
1253 (* elems = (cand,m,s,gl) *)
1254 let size_gl l = List.length
1255 (List.filter (function (_,_,P) -> true | _ -> false) l)
1258 let inj_gl gl = List.map (fun g -> D g) gl in
1259 let rec map = function
1260 | [] -> assert false
1261 | (cand,m,s,gl)::[] ->
1262 (* in the last one we add the failure *)
1263 let todo = inj_gl gl @ (S(g,gty,cand,size+1))::todo in
1264 (* we are the last in OR, we fail on g and
1265 * also on all failures implied by g *)
1266 (m,s, size + size_gl gl, todo, (g,gty)::fl) :: orlist
1267 | (cand,m,s,gl)::tl ->
1268 (* we add the S step after gl and before todo *)
1269 let todo = inj_gl gl @ (S(g,gty,cand,size+1))::todo in
1270 (* since we are not the last in OR, we do not
1272 (m,s, size + size_gl gl, todo, []) :: map tl
1276 aux tables maxm flags cache elems)
1279 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1280 let cache = close_failures fl cache in
1281 aux tables maxm flags cache orlist
1283 (aux tables maxm flags cache elems : auto_result)
1287 let rec auto_main tables maxm context flags elems universe cache =
1288 auto_context := context;
1289 let flags = calculate_timeout flags in
1290 let ppterm = ppterm context in
1291 let irl = mk_irl context in
1292 let rec aux flags tables maxm cache elems status =
1293 match elems with (* elems in OR *)
1294 | [] -> Fail "no more steps can be done", tables, cache, maxm
1295 (*COMPLETE FAILURE*)
1296 | (p ,metasenv,subst,[])::tl ->
1297 Success (p,metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
1298 | (_,metasenv,subst,goals)::tl when
1299 List.length (List.filter prop goals) > flags.maxwidth ->
1301 (lazy (" FAILURE(width): " ^ string_of_int (List.length goals)));
1302 aux flags tables maxm cache tl (List.tl status) (* FAILURE (width) *)
1303 | (p,metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
1304 let (_,_,_,_::gl_status)::tl_status = status in
1305 if Unix.gettimeofday() > flags.timeout then
1306 Fail "timeout",tables,cache,maxm
1309 let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
1312 (lazy ("INSPECTING " ^ string_of_int goalno^
1313 ":"^"(id="^string_of_int id^")"^ppterm goalty ^
1314 "with depth"^string_of_int depth));
1315 debug_print (lazy (AutoCache.cache_print context cache));
1316 if sort = T (* && tl <> []*) then
1318 (lazy (" FAILURE(not in prop)"));
1319 aux flags tables maxm cache ((p,metasenv,subst,gl)::tl)
1320 ((p,metasenv,subst,gl)::tl_status))
1322 match aux_single flags tables maxm universe cache metasenv subst elem
1323 goalty cc gl_status tl_status p with
1324 | Fail s, tables, cache, maxm' ->
1328 (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
1330 if flags.dont_cache_failures or s = "hint" then
1331 cache_remove_underinspection cache goalty
1333 cache_add_failure cache goalty depth
1335 aux flags tables maxm cache tl tl_status
1336 | Success (p1,metasenv,subst,others), tables, cache, maxm' ->
1338 (* others are alternatives in OR *)
1340 let goal = Cic.Meta(goalno,irl) in
1341 let proof = CicMetaSubst.apply_subst subst goal in
1343 (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
1344 if is_a_green_cut goalty then
1345 (* assert_proof_is_valid proof metasenv context goalty; *)
1346 let cache = cache_add_success sort cache goalty proof in
1347 aux flags tables maxm cache ((p,metasenv,subst,gl)::tl)
1348 ((p,metasenv,subst,gl)::tl_status)
1351 (let goalty = CicMetaSubst.apply_subst subst goalty in
1352 (* assert_proof_is_valid proof metasenv context goalty; *)
1354 if is_a_green_cut goalty then
1355 cache_add_success sort cache goalty proof
1361 (fun (p,metasenv,subst,goals) ->
1362 (p,metasenv,subst,goals@gl))
1365 aux flags tables maxm cache
1366 ((p,metasenv,subst,gl)::others@tl)
1367 ((p,metasenv,subst,gl)::others@tl_status)
1371 with CicUtil.Meta_not_found i when i = goalno ->
1373 with CicUtil.Meta_not_found i when i = goalno ->
1374 (* goalno was closed by sideeffect *)
1376 (lazy ("Goal "^string_of_int goalno^" closed by sideeffect"));
1377 aux flags tables maxm cache ((p,metasenv,subst,gl)::tl)
1378 ((p,metasenv,subst,gl)::tl_status)
1380 and aux_single flags tables maxm universe cache metasenv subst (goalno, depth,
1381 _) goalty cc e l (id,_,_) =
1383 | Some id' when id <> id' -> Fail "hint", tables,cache,maxm
1386 (* let flags = if depth < 10 then {flags with maxwidth=3} else flags in *)
1387 let goalty = CicMetaSubst.apply_subst subst goalty in
1388 (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
1389 (* FAILURE (euristic cut) *)
1390 match cache_examine cache goalty with
1391 | Failed_in d when d >= depth ->
1392 Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
1393 tables,cache,maxm(*FAILURE(depth)*)
1395 let entry = goalno, (cc, t,goalty) in
1396 assert_subst_are_disjoint subst [entry];
1397 let subst = entry :: subst in
1398 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1399 debug_print (lazy (" CACHE HIT!"));
1401 Success ((!candidate_no,t,goalty),metasenv, subst, []), tables, cache, maxm
1402 | UnderInspection ->
1403 (* assert (not (is_a_green_cut goalty)); *)
1404 Fail "looping",tables,cache, maxm
1406 | Failed_in _ when depth > 0 -> (* we have more depth now *)
1407 let cache = cache_add_underinspection cache goalty depth in
1408 let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty, [] in (* FG: attrs *)
1409 let elems, tables, cache, maxm, flags =
1410 if is_equational_case goalty flags then
1411 let elems,tables,cache,maxm1, flags =
1412 equational_case tables maxm cache
1413 depth fake_proof goalno goalty subst context flags in
1415 let more_elems, tables, cache, maxm1 =
1416 if flags.use_only_paramod then
1417 [],tables, cache, maxm
1420 tables maxm depth subst fake_proof goalno
1421 goalty metasenv context universe cache in
1423 elems@more_elems, tables, cache, maxm, flags
1425 let elems, tables, cache, maxm =
1426 applicative_case tables maxm depth subst fake_proof goalno
1427 goalty metasenv context universe cache in
1428 elems, tables, cache, maxm, flags
1431 List.map (fun (p,m,s,l) -> p,m,s,l@e) elems @ l
1433 auto_status := status;
1435 let rc = aux flags tables maxm cache elems status in
1436 debug_print "BACK!";
1438 | _ -> Fail "depth = 0",tables,cache,maxm
1440 aux flags tables maxm cache elems elems
1447 auto_all_solutions maxm tables universe cache context metasenv gl flags
1449 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1450 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
1451 let elems = [(0,Cic.Implicit None,Cic.Implicit None), metasenv,[],goals] in
1452 let rec aux tables maxm solutions cache elems flags =
1453 match auto_main tables maxm context flags elems universe cache with
1454 | Fail s,tables,cache,maxm ->debug_print s; solutions,cache,maxm
1455 | Success (_,metasenv,subst,others),tables,cache,maxm ->
1456 if Unix.gettimeofday () > flags.timeout then
1457 ((subst,metasenv)::solutions), cache, maxm
1459 aux tables maxm ((subst,metasenv)::solutions) cache others flags
1461 let rc = aux tables maxm [] cache elems flags in
1463 | [],cache,maxm -> [],cache,maxm
1464 | solutions,cache,maxm ->
1467 (fun (subst,newmetasenv) ->
1469 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1471 if opened = [] then Some subst else None)
1474 solutions,cache,maxm
1478 auto_all_solutions maxm tables universe cache context metasenv gl flags
1480 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1483 (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1485 let elems = [metasenv,[],1,goals,[]] in
1486 let rec aux tables maxm solutions cache elems flags =
1487 match auto_main tables maxm context flags universe cache elems with
1488 | Gaveup (tables,cache,maxm) ->
1489 solutions,cache,maxm
1490 | Proved (metasenv,subst,others,tables,cache,maxm) ->
1491 if Unix.gettimeofday () > flags.timeout then
1492 ((subst,metasenv)::solutions), cache, maxm
1494 aux tables maxm ((subst,metasenv)::solutions) cache others flags
1496 let rc = aux tables maxm [] cache elems flags in
1498 | [],cache,maxm -> [],cache,maxm
1499 | solutions,cache,maxm ->
1502 (fun (subst,newmetasenv) ->
1504 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1506 if opened = [] then Some subst else None)
1509 solutions,cache,maxm
1512 (* }}} ****************** AUTO ***************)
1514 (* script generation for applicative proofs
1515 let cic2grafite context menv t =
1516 let module PT = CicNotationPt in
1517 let module GA = GrafiteAst in
1518 let pp_t context t =
1519 let names = Utils.names_of_context context in
1522 let sort_of context t =
1524 CicTypeChecker.type_of_aux' menv context t
1525 CicUniv.oblivion_ugraph
1527 let sort,_ = CicTypeChecker.type_of_aux' menv context ty
1528 CicUniv.oblivion_ugraph
1531 | Cic.Sort Cic.Prop -> P
1534 let floc = HExtlib.dummy_floc in
1535 let rec print_term c = function
1537 | Cic.MutConstruct _
1539 | Cic.Const _ as t ->
1540 PT.Ident (pp_t c t, None)
1541 | Cic.Appl l -> PT.Appl (List.map (print_term c) l)
1542 | Cic.Implicit _ -> PT.Implicit
1543 | Cic.Lambda (Cic.Name n, s, t) ->
1544 PT.Binder (`Lambda, (PT.Ident (n,None), Some (print_term c s)),
1545 print_term (Some (Cic.Name n, Cic.Decl s)::c) t)
1546 | Cic.Prod (Cic.Name n, s, t) ->
1547 PT.Binder (`Forall, (PT.Ident (n,None), Some (print_term c s)),
1548 print_term (Some (Cic.Name n, Cic.Decl s)::c) t)
1549 | Cic.LetIn (Cic.Name n, s, t) ->
1550 PT.Binder (`Lambda, (PT.Ident (n,None), Some (print_term c s)),
1551 print_term (Some (Cic.Name n, Cic.Def (s,None))::c) t)
1552 | Cic.Meta _ -> PT.Implicit
1554 PT.Ident ("ERROR"^CicPp.ppterm t, None)
1556 debug_print (lazy (CicPp.ppterm t));
1560 let rec print_proof context = function
1562 | Cic.Const _ as t ->
1563 [GA.Executable (floc,
1565 Some (GA.Apply (floc, print_term context t)), GA.Dot floc))]
1566 | Cic.Appl (he::tl) ->
1567 let tl = List.map (fun t -> t, sort_of context t) tl in
1569 HExtlib.filter_map (function (t,P) -> Some t | _ -> None) tl
1574 | (t,P) -> Cic.Implicit None
1578 if List.length subgoals > 1 then
1580 [GA.Executable (floc,
1582 Some (GA.Apply (floc, print_term context (Cic.Appl (he::args)))),
1583 GA.Semicolon floc))] @
1584 [GA.Executable (floc, GA.Tactic (floc, None, GA.Branch floc))] @
1585 (HExtlib.list_concat
1586 ~sep:[GA.Executable (floc, GA.Tactic (floc, None,GA.Shift floc))]
1587 (List.map (print_proof context) subgoals)) @
1588 [GA.Executable (floc, GA.Tactic (floc, None,GA.Merge floc))]
1591 [GA.Executable (floc,
1594 (floc, print_term context (Cic.Appl (he::args)) )), GA.Dot floc))]
1596 (match subgoals with
1598 | [x] -> print_proof context x
1599 | _ -> assert false)
1602 debug_print (lazy (CicPp.ppterm t));
1606 let ast = print_proof context t in
1608 (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
1609 * which will show up using the following command line:
1610 * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
1611 let width = max_int in
1612 let term_pp content_term =
1613 let pres_term = TermContentPres.pp_ast content_term in
1614 let dummy_tbl = Hashtbl.create 1 in
1615 let markup = CicNotationPres.render dummy_tbl pres_term in
1616 let s = "(" ^ BoxPp.render_to_string List.hd width markup ^ ")" in
1618 ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s
1620 CicNotationPp.set_pp_term term_pp;
1621 let lazy_term_pp = fun x -> assert false in
1622 let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
1623 GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t
1625 String.concat "\n" (List.map pp ast)
1627 let auto_all tables universe cache context metasenv gl flags =
1628 let solutions, cache, _ =
1629 auto_all_solutions 0 tables universe cache context metasenv gl flags
1635 let auto flags metasenv tables universe cache context metasenv gl =
1636 let initial_time = Unix.gettimeofday() in
1637 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1638 let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1639 let elems = [metasenv,[],1,goals,[]] in
1640 match auto_main tables 0 context flags universe cache elems with
1641 | Proved (metasenv,subst,_, tables,cache,_) ->
1643 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1644 Some (subst,metasenv), cache
1645 | Gaveup (tables,cache,maxm) ->
1647 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1651 let bool params name default =
1653 let s = List.assoc name params in
1654 if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
1655 else if s = "0" || s = "false" || s = "no" || s= "off" then false
1657 let msg = "Unrecognized value for parameter "^name^"\n" in
1658 let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
1659 raise (ProofEngineTypes.Fail (lazy msg))
1660 with Not_found -> default
1663 let string params name default =
1664 try List.assoc name params with
1665 | Not_found -> default
1668 let int params name default =
1669 try int_of_string (List.assoc name params) with
1670 | Not_found -> default
1672 raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
1675 let flags_of_params params ?(for_applyS=false) () =
1676 let int = int params in
1677 let bool = bool params in
1678 let close_more = bool "close_more" false in
1679 let use_paramod = bool "use_paramod" true in
1680 let use_only_paramod =
1681 if for_applyS then true else bool "paramodulation" false in
1682 let use_library = bool "library"
1683 ((AutoTypes.default_flags()).AutoTypes.use_library) in
1684 let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
1685 let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
1686 let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
1687 let timeout = int "timeout" 0 in
1688 { AutoTypes.maxdepth =
1689 if use_only_paramod then 2 else depth;
1690 AutoTypes.maxwidth = width;
1691 AutoTypes.maxsize = size;
1694 if for_applyS then Unix.gettimeofday () +. 30.0
1698 Unix.gettimeofday() +. (float_of_int timeout);
1699 AutoTypes.use_library = use_library;
1700 AutoTypes.use_paramod = use_paramod;
1701 AutoTypes.use_only_paramod = use_only_paramod;
1702 AutoTypes.close_more = close_more;
1703 AutoTypes.dont_cache_failures = false;
1706 let applyS_tac ~dbd ~term ~params ~universe =
1707 ProofEngineTypes.mk_tactic
1710 let _, proof, gl,_,_ =
1711 apply_smart ~dbd ~term ~subst:[] ~universe
1712 (flags_of_params params ~for_applyS:true ()) status
1716 | CicUnification.UnificationFailure msg
1717 | CicTypeChecker.TypeCheckerFailure msg ->
1718 raise (ProofEngineTypes.Fail msg))
1723 * auto superposition target = NAME
1724 * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
1726 * - if table is omitted no superposition will be performed
1727 * - if demod_table is omitted no demodulation will be prformed
1728 * - subterms_only is passed to Indexing.superposition_right
1730 * lists are coded using _ (example: H_H1_H2)
1733 let eq_and_ty_of_goal = function
1734 | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
1736 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1739 let rec find_in_ctx i name = function
1740 | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
1741 | Some (Cic.Name name', _)::tl when name = name' -> i
1742 | _::tl -> find_in_ctx (i+1) name tl
1745 let rec position_of i x = function
1746 | [] -> assert false
1747 | j::tl when j <> x -> position_of (i+1) x tl
1752 let superposition_tac ~target ~table ~subterms_only ~demod_table status =
1753 Saturation.reset_refs();
1754 let proof,goalno = status in
1755 let curi,metasenv,pbo,pty, attrs = proof in
1756 let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
1757 let eq_uri,tty = eq_and_ty_of_goal ty in
1758 let env = (metasenv, context, CicUniv.empty_ugraph) in
1759 let names = Utils.names_of_context context in
1760 let bag = Equality.mk_equality_bag () in
1761 let eq_index, equalities, maxm,cache =
1762 find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty
1765 let what = find_in_ctx 1 target context in
1766 List.nth equalities (position_of 0 what eq_index)
1771 let others = Str.split (Str.regexp "_") table in
1772 List.map (fun other -> find_in_ctx 1 other context) others
1775 (fun other -> List.nth equalities (position_of 0 other eq_index))
1780 let index = List.fold_left Indexing.index Indexing.empty eq_other in
1782 if table = "" then maxm,[eq_what] else
1783 Indexing.superposition_right bag
1784 ~subterms_only eq_uri maxm env index eq_what
1786 debug_print (lazy ("Superposition right:"));
1787 debug_print (lazy ("\n eq: " ^ Equality.string_of_equality eq_what ~env));
1788 debug_print (lazy ("\n table: "));
1791 debug_print (lazy (" " ^ Equality.string_of_equality e ~env))) eq_other;
1792 debug_print (lazy ("\n result: "));
1793 List.iter (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1794 debug_print (lazy ("\n result (cut&paste): "));
1797 let t = Equality.term_of_equality eq_uri e in
1798 debug_print (lazy (CicPp.pp t names)))
1800 debug_print (lazy ("\n result proofs: "));
1802 debug_print (lazy (let _,p,_,_,_ = Equality.open_equality e in
1803 let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
1804 Subst.ppsubst s ^ "\n" ^
1805 CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names))) eql;
1806 if demod_table <> "" then
1809 if eql = [] then [eq_what] else eql
1812 let demod = Str.split (Str.regexp "_") demod_table in
1813 List.map (fun other -> find_in_ctx 1 other context) demod
1817 (fun demod -> List.nth equalities (position_of 0 demod eq_index))
1820 let table = List.fold_left Indexing.index Indexing.empty eq_demod in
1823 (fun (maxm,acc) e ->
1825 Indexing.demodulation_equality bag eq_uri maxm env table e
1830 let eql = List.rev eql in
1831 debug_print (lazy ("\n result [demod]: "));
1833 (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1834 debug_print (lazy ("\n result [demod] (cut&paste): "));
1837 let t = Equality.term_of_equality eq_uri e in
1838 debug_print (lazy (CicPp.pp t names)))
1844 let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
1845 (* argument parsing *)
1846 let string = string params in
1847 let bool = bool params in
1848 (* hacks to debug paramod *)
1849 let superposition = bool "superposition" false in
1850 let target = string "target" "" in
1851 let table = string "table" "" in
1852 let subterms_only = bool "subterms_only" false in
1853 let demod_table = string "demod_table" "" in
1854 match superposition with
1856 (* this is the ugly hack to debug paramod *)
1858 ~target ~table ~subterms_only ~demod_table (proof,goal)
1860 (* this is the real auto *)
1861 let _,metasenv,_,_, _ = proof in
1862 let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1863 let flags = flags_of_params params () in
1864 (* just for testing *)
1865 let use_library = flags.use_library in
1866 let tables,cache,newmeta =
1867 init_cache_and_tables dbd use_library flags.use_only_paramod
1868 universe (proof, goal) in
1869 let tables,cache,newmeta =
1870 if flags.close_more then
1872 tables newmeta context (proof, goal)
1873 auto_all_solutions universe cache
1874 else tables,cache,newmeta in
1875 let initial_time = Unix.gettimeofday() in
1876 let (_,oldmetasenv,_,_, _) = proof in
1879 metasenv,[],1,[D (goal,flags.maxdepth,P)],[]
1881 match auto_main tables newmeta context flags universe cache [elem] with
1882 | Proved (metasenv,subst,_, tables,cache,_) ->
1884 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
1885 (* script generation
1886 let irl = mk_irl context in
1887 let goal_term = Cic.Meta(goal, irl) in
1888 let proof_term = CicMetaSubst.apply_subst subst goal_term in
1889 HLog.debug (cic2grafite context metasenv proof_term);
1891 let proof,metasenv =
1892 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1893 proof goal (CicMetaSubst.apply_subst subst) metasenv
1896 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1897 ~newmetasenv:metasenv
1900 | Gaveup (tables,cache,maxm) ->
1903 string_of_float(Unix.gettimeofday()-.initial_time)));
1904 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1907 let auto_tac ~dbd ~params ~universe =
1908 ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
1910 let eq_of_goal = function
1911 | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1913 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1917 let demodulate_tac ~dbd ~universe (proof,goal)=
1918 let curi,metasenv,pbo,pty, attrs = proof in
1919 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1920 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1921 let initgoal = [], [], ty in
1922 let eq_uri = eq_of_goal ty in
1923 let (active,passive,bag), cache, maxm =
1924 init_cache_and_tables dbd false true universe (proof,goal) in
1925 let equalities = (Saturation.list_of_passive passive) in
1926 (* we demodulate using both actives passives *)
1929 (fun tbl eq -> Indexing.index tbl eq)
1930 (snd active) equalities
1932 let changed,(newproof,newmetasenv, newty) =
1933 Indexing.demodulation_goal bag
1934 (metasenv,context,CicUniv.empty_ugraph) table initgoal
1938 let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1940 Equality.build_goal_proof bag
1941 eq_uri newproof opengoal ty [] context metasenv
1943 let extended_metasenv = (maxm,context,newty)::metasenv in
1944 let extended_status =
1945 (curi,extended_metasenv,pbo,pty, attrs),goal in
1946 let (status,newgoals) =
1947 ProofEngineTypes.apply_tactic
1948 (PrimitiveTactics.apply_tac ~term:proofterm)
1950 (status,maxm::newgoals)
1952 else (* if newty = ty then *)
1953 raise (ProofEngineTypes.Fail (lazy "no progress"))
1954 (*else ProofEngineTypes.apply_tactic
1955 (ReductionTactics.simpl_tac
1956 ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1959 let demodulate_tac ~dbd ~universe =
1960 ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;