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);;
34 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
35 let ugraph = CicUniv.oblivion_ugraph;;
36 let typeof = CicTypeChecker.type_of_aux';;
38 let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
41 let is_propositional context sort =
42 match CicReduction.whd context sort with
44 | Cic.Sort (Cic.CProp _) -> true
47 let is_in_prop context subst metasenv ty =
48 let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
49 is_propositional context sort
52 exception NotConvertible;;
54 let check_proof_is_valid proof metasenv context goalty =
58 let ty,u = typeof metasenv context proof CicUniv.oblivion_ugraph in
59 let b,_ = CicReduction.are_convertible context ty goalty u in
60 if not b then raise NotConvertible else b
63 List.map (function None -> None | Some (x,_) -> Some x) context
65 debug_print (lazy ("PROOF:" ^ CicPp.pp proof names));
66 (* debug_print (lazy ("PROOFTY:" ^ CicPp.pp ty names)); *)
67 debug_print (lazy ("GOAL:" ^ CicPp.pp goalty names));
68 debug_print (lazy ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv));
74 let assert_proof_is_valid proof metasenv context goalty =
75 assert (check_proof_is_valid proof metasenv context goalty)
78 let assert_subst_are_disjoint subst subst' =
81 (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
86 let split_goals_in_prop metasenv subst gl =
89 let _,context,ty = CicUtil.lookup_meta g metasenv in
91 let sort,u = typeof ~subst metasenv context ty ugraph in
92 is_propositional context sort
94 | CicTypeChecker.AssertFailure s
95 | CicTypeChecker.TypeCheckerFailure s ->
97 (lazy ("NON TIPA" ^ ppterm context (CicMetaSubst.apply_subst subst ty)));
100 (* FIXME... they should type! *)
104 let split_goals_with_metas metasenv subst gl =
107 let _,context,ty = CicUtil.lookup_meta g metasenv in
108 let ty = CicMetaSubst.apply_subst subst ty in
109 CicUtil.is_meta_closed ty)
113 let order_new_goals metasenv subst open_goals ppterm =
114 let prop,rest = split_goals_in_prop metasenv subst open_goals in
115 let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
116 let closed_type, open_type = split_goals_with_metas metasenv subst rest in
118 (List.map (fun x -> x,P) (open_prop @ closed_prop))
120 (List.map (fun x -> x,T) (open_type @ closed_type))
125 let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals
127 debug_print (lazy (" OPEN: "^
131 | (i,t,P) -> string_of_int i ^ ":"^ppterm t^ "Prop"
132 | (i,t,T) -> string_of_int i ^ ":"^ppterm t^ "Type")
137 let is_an_equational_goal = function
138 | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
142 type auto_params = Cic.term list * (string * string) list
144 let elems = ref [] ;;
146 (* closing a term w.r.t. its metavariables
147 very naif version: it does not take dependencies properly into account *)
149 let naif_closure ?(prefix_name="xxx_") t metasenv context =
150 let in_term t (i,_,_) =
151 List.exists (fun (j,_) -> j=i) (CicUtil.metas_of_term t)
153 let metasenv = List.filter (in_term t) metasenv in
154 let metasenv = ProofEngineHelpers.sort_metasenv metasenv in
155 let n = List.length metasenv in
156 let what = List.map (fun (i,cc,ty) -> Cic.Meta(i,[])) metasenv in
159 (fun (i,acc) (_,cc,ty) -> (i-1,Cic.Rel i::acc))
162 let t = CicSubstitution.lift n t in
164 ProofEngineReduction.replace_lifting
165 ~equality:(fun c t1 t2 ->
167 | Cic.Meta(i,_),Cic.Meta(j,_) -> i = j
169 ~context ~what ~with_what ~where:t
173 (fun (n,t) (_,cc,ty) ->
174 n-1, Cic.Lambda(Cic.Name (prefix_name^string_of_int n),
175 CicSubstitution.lift n ty,t))
178 t, List.length metasenv
181 let lambda_close ?prefix_name t menv ctx =
182 let t, num_lambdas = naif_closure ?prefix_name t menv ctx in
184 (fun (t,i) -> function
185 | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *)
186 | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1
187 | Some (name, Cic.Def (bo, ty)) -> Cic.LetIn (name, bo, ty, t),i+1)
191 (* functions for retrieving theorems *)
194 exception FillingFailure of AutoCache.cache * AutomationCache.tables
196 let rec unfold context = function
197 | Cic.Prod(name,s,t) ->
198 let t' = unfold ((Some (name,Cic.Decl s))::context) t in
200 | t -> ProofEngineReduction.unfold context t
202 let find_library_theorems dbd proof goal =
203 let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
204 let terms = List.map CicUtil.term_of_uri univ in
207 (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph)))
210 let find_context_theorems context metasenv =
213 (fun (res,i) ctxentry ->
215 | Some (_,Cic.Decl t) ->
216 (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
217 | Some (_,Cic.Def (_,t)) ->
218 (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
223 let rec is_an_equality = function
224 | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _]
225 when (LibraryObjects.is_eq_URI uri) -> true
226 | Cic.Prod (_, _, t) -> is_an_equality t
230 let partition_equalities =
231 List.partition (fun (_,ty) -> is_an_equality ty)
234 let default_auto tables _ cache _ _ _ _ = [],cache,tables ;;
236 (* giusto per provare che succede
237 let is_unit_equation context metasenv oldnewmeta term =
238 let head, metasenv, args, newmeta =
239 TermUtil.saturate_term oldnewmeta metasenv context term 0
242 List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv
244 Some (args,metasenv,newmetas,head,newmeta) *)
246 let is_unit_equation context metasenv oldnewmeta term =
247 let head, metasenv, args, newmeta =
248 TermUtil.saturate_term oldnewmeta metasenv context term 0
250 let propositional_args =
254 let _,_,mt = CicUtil.lookup_meta i metasenv in
256 CicTypeChecker.type_of_aux' metasenv context mt
257 CicUniv.oblivion_ugraph
259 if is_propositional context sort then Some i else None
263 if propositional_args = [] then
265 List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv
267 Some (args,metasenv,newmetas,head,newmeta)
271 let get_candidates skip_trie_filtering universe cache t =
272 let t = if skip_trie_filtering then Cic.Meta(0,[]) else t in
274 (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
277 (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^
278 (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
279 debug_print debug_msg;
283 let only signature context metasenv t =
286 CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph
288 let consts = MetadataConstraints.constants_of ty in
289 let b = MetadataConstraints.UriManagerSet.subset consts signature in
290 (* if b then (prerr_endline ("keeping " ^ (CicPp.ppterm t)); b) *)
293 let ty' = unfold context ty in
294 let consts' = MetadataConstraints.constants_of ty' in
295 let b = MetadataConstraints.UriManagerSet.subset consts' signature in
297 if not b then prerr_endline ("filtering " ^ (CicPp.ppterm t))
298 else prerr_endline ("keeping " ^ (CicPp.ppterm t));
302 | CicTypeChecker.TypeCheckerFailure _ -> assert false
303 | ProofEngineTypes.Fail _ -> false (* unfold may fail *)
306 let not_default_eq_term t =
308 let uri = CicUtil.uri_of_term t in
309 not (LibraryObjects.in_eq_URIs uri)
310 with Invalid_argument _ -> true
312 let retrieve_equations dont_filter signature universe cache context metasenv =
313 match LibraryObjects.eq_URI() with
316 let eq_uri = UriManager.strip_xpointer eq_uri in
317 let fake= Cic.Meta(-1,[]) in
318 let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
319 let candidates = get_candidates false universe cache fake_eq in
320 if dont_filter then candidates
321 else let eq_uri = UriManager.uri_of_uriref eq_uri 0 None in
322 (* let candidates = List.filter not_default_eq_term candidates in *)
324 (only (MetadataConstraints.UriManagerSet.add eq_uri signature)
325 context metasenv) candidates
327 let build_equality bag head args proof newmetas =
329 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
331 if args = [] then proof else Cic.Appl (proof::args)
333 let o = !Utils.compare_terms t1 t2 in
334 let stat = (ty,t1,t2,o) in
335 (* let w = compute_equality_weight stat in *)
337 let proof = Equality.Exact p in
338 let bag, e = Equality.mk_equality bag (w, proof, stat, newmetas) in
339 (* to clean the local context of metas *)
340 Equality.fix_metas bag e
344 let partition_unit_equalities context metasenv newmeta bag equations =
346 (fun (bag,units,other,maxmeta)(t,ty) ->
347 if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then
350 ("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context
351 ^ " since it is not meta closed")
353 bag, units,(t,ty)::other,maxmeta
355 match is_unit_equation context metasenv maxmeta ty with
356 | Some (args,metasenv,newmetas,head,newmeta') ->
358 build_equality bag head args t newmetas in
359 bag, equality::units,other,maxmeta
361 bag, units,(t,ty)::other,maxmeta)
362 (bag,[],[],newmeta) equations
365 let init_cache_and_tables
366 ?dbd ~use_library ~use_context
367 automation_cache restricted_univ (proof, goal)
369 let _, metasenv, _, _, _, _ = proof in
370 let _,context,_ = CicUtil.lookup_meta goal metasenv in
371 if restricted_univ = [] then
373 if use_context then find_context_theorems context metasenv else []
376 match use_library, dbd with
377 | true, Some dbd -> find_library_theorems dbd metasenv goal
380 let cache = AutoCache.cache_empty in
381 let cache = cache_add_list cache context (ct@lt) in
383 let env = metasenv, context, CicUniv.oblivion_ugraph in
385 (fun (a,p,b) (t,ty) ->
386 let mes = CicUtil.metas_of_term ty in
387 Saturation.add_to_active b a p env ty t
388 (List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv))
389 automation_cache.AutomationCache.tables ct
391 automation_cache.AutomationCache.univ, tables, cache
393 let metasenv, t_ty, s_t_ty, _ =
395 (fun (metasenv,acc, sacc, maxmeta) t ->
397 CicTypeChecker.type_of_aux'
398 metasenv ~subst:[] context t CicUniv.oblivion_ugraph
400 let head, metasenv, args, maxmeta =
401 TermUtil.saturate_term maxmeta metasenv context ty 0
403 let st = if args = [] then t else Cic.Appl (t::args) in
404 metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta)
405 (metasenv, [],[], CicMkImplicit.new_meta metasenv []) restricted_univ
407 let automation_cache = AutomationCache.empty () in
408 let automation_cache =
409 let universe = automation_cache.AutomationCache.univ in
411 Universe.index_list universe context t_ty
413 { automation_cache with AutomationCache.univ = universe }
415 let automation_cache =
418 AutomationCache.add_term_to_active c metasenv [] context t (Some ty))
419 automation_cache s_t_ty
421 (* AutomationCache.pp_cache automation_cache; *)
422 automation_cache.AutomationCache.univ,
423 automation_cache.AutomationCache.tables,
424 cache_add_list cache_empty context t_ty
427 (* let signature = MetadataQuery.signature_of metasenv goal in *)
428 (* let newmeta = CicMkImplicit.new_meta metasenv [] in *)
430 retrieve_equations dont_filter (* true *) signature universe cache context metasenv
433 (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
438 CicTypeChecker.type_of_aux'
439 metasenv context t CicUniv.oblivion_ugraph
441 (* retrieve_equations could also return flexible terms *)
442 if is_an_equality ty then Some(t,ty)
445 let ty' = unfold context ty in
446 if is_an_equality ty' then Some(t,ty') else None
447 with ProofEngineTypes.Fail _ -> None)
450 let bag = Equality.mk_equality_bag () in
451 let units, other_equalities, newmeta =
452 partition_unit_equalities context metasenv newmeta bag eqs_and_types
454 (* SIMPLIFICATION STEP
456 let env = (metasenv, context, CicUniv.oblivion_ugraph) in
457 let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in
458 Saturation.simplify_equalities bag eq_uri env units
461 let passive = Saturation.make_passive units in
462 let no = List.length units in
463 let active = Saturation.make_active [] in
464 let active,passive,newmeta =
465 if paramod then active,passive,newmeta
467 Saturation.pump_actives
468 context bag newmeta active passive (no+1) infinity
470 (active,passive,bag),cache,newmeta
473 let fill_hypothesis context metasenv term tables (universe:Universe.universe) cache auto fast =
474 let actives, passives, bag = tables in
475 let bag, head, metasenv, args =
476 Equality.saturate_term bag metasenv context term
478 let tables = actives, passives, bag in
479 let propositional_args =
483 let _,_,mt = CicUtil.lookup_meta i metasenv in
485 CicTypeChecker.type_of_aux' metasenv context mt
486 CicUniv.oblivion_ugraph
488 if is_propositional context sort then Some i else None
492 let results,cache,tables =
493 if propositional_args = [] then
494 let _,_,bag = tables in
495 let newmetas = Equality.filter_metasenv_gt_maxmeta bag metasenv in
496 [args,metasenv,newmetas,head],cache,tables
500 None,metasenv,term,term (* term non e' significativo *)
504 {AutoTypes.default_flags() with
505 AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
506 maxwidth = 2;maxdepth = 2;
507 use_paramod=true;use_only_paramod=false}
509 {AutoTypes.default_flags() with
510 AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
511 maxwidth = 2;maxdepth = 4;
512 use_paramod=true;use_only_paramod=false}
514 match auto tables universe cache context metasenv propositional_args flags with
515 | [],cache,tables -> raise (FillingFailure (cache,tables))
516 | substs,cache,tables ->
517 let actives, passaives, bag = tables in
520 (fun subst (bag,acc) ->
522 CicMetaSubst.apply_subst_metasenv subst metasenv
524 let head = CicMetaSubst.apply_subst subst head in
525 let newmetas = Equality.filter_metasenv_gt_maxmeta bag metasenv in
526 let args = List.map (CicMetaSubst.apply_subst subst) args in
527 let newm = CicMkImplicit.new_meta metasenv subst in
528 let bag = Equality.push_maxmeta bag newm in
529 bag, ((args,metasenv,newmetas,head) :: acc))
532 let tables = actives, passives, bag in
538 let build_equalities auto context metasenv tables universe cache equations =
540 (fun (tables,facts,cache) (t,ty) ->
541 (* in any case we add the equation to the cache *)
542 let cache = AutoCache.cache_add_list cache context [(t,ty)] in
544 let saturated, cache, tables =
545 fill_hypothesis context metasenv ty tables universe cache auto true
549 (fun (acc, tables) (args,metasenv,newmetas,head) ->
550 let actives, passives, bag = tables in
552 build_equality bag head args t newmetas
554 let tables = actives, passives, bag in
555 equality::acc,tables)
556 ([],tables) saturated
558 (tables, eqs@facts, cache)
559 with FillingFailure (cache,tables) ->
560 (* if filling hypothesis fails we add the equation to
564 (tables,[],cache) equations
566 let close_more tables context status auto universe cache =
567 let proof, goalno = status in
568 let _, metasenv,_subst,_,_, _ = proof in
569 let signature = MetadataQuery.signature_of metasenv goalno in
571 retrieve_equations false signature universe cache context metasenv
577 CicTypeChecker.type_of_aux' metasenv context t
578 CicUniv.oblivion_ugraph in
579 (* retrieve_equations could also return flexible terms *)
580 if is_an_equality ty then Some(t,ty) else None)
582 let tables, units, cache =
583 build_equalities auto context metasenv tables universe cache eqs_and_types
585 let active,passive,bag = tables in
586 let passive = Saturation.add_to_passive units passive in
587 let no = List.length units in
588 let active, passive, bag =
589 Saturation.pump_actives context bag active passive (no+1) infinity
591 (active,passive,bag), cache
594 let find_context_equalities tables context proof (universe:Universe.universe) cache
596 let module C = Cic in
597 let module S = CicSubstitution in
598 let module T = CicTypeChecker in
599 let _,metasenv,_subst,_,_, _ = proof in
600 (* if use_auto is true, we try to close the hypothesis of equational
601 statements using auto; a naif, and probably wrong approach *)
602 let rec aux tables cache index = function
603 | [] -> tables, [], cache
604 | (Some (_, C.Decl (term)))::tl ->
607 (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
608 let do_find tables context term =
610 | C.Prod (name, s, t) when is_an_equality t ->
612 let term = S.lift index term in
613 let saturated, cache, tables =
614 fill_hypothesis context metasenv term
615 tables universe cache default_auto false
617 let actives, passives, bag = tables in
620 (fun (bag,acc) (args,metasenv,newmetas,head) ->
622 build_equality bag head args (Cic.Rel index) newmetas
627 let tables = actives, passives, bag in
629 with FillingFailure (cache,tables) ->
631 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
632 when LibraryObjects.is_eq_URI uri ->
633 let term = S.lift index term in
634 let actives, passives, bag = tables in
636 build_equality bag term [] (Cic.Rel index) []
638 let tables = actives, passives, bag in
640 | _ -> tables, [], cache
642 let tables, eqs, cache = do_find tables context term in
643 let tables, rest, cache = aux tables cache (index+1) tl in
644 tables, List.map (fun x -> index,x) eqs @ rest, cache
646 aux tables cache (index+1) tl
648 let tables, il, cache = aux tables cache 1 context in
649 let indexes, equalities = List.split il in
650 tables, indexes, equalities, cache
653 (********** PARAMETERS PASSING ***************)
655 let bool params name default =
657 let s = List.assoc name params in
658 if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
659 else if s = "0" || s = "false" || s = "no" || s= "off" then false
661 let msg = "Unrecognized value for parameter "^name^"\n" in
662 let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
663 raise (ProofEngineTypes.Fail (lazy msg))
664 with Not_found -> default
667 let string params name default =
668 try List.assoc name params with
669 | Not_found -> default
672 let int params name default =
673 try int_of_string (List.assoc name params) with
674 | Not_found -> default
676 raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
679 let flags_of_params params ?(for_applyS=false) () =
680 let int = int params in
681 let bool = bool params in
682 let close_more = bool "close_more" false in
683 let use_paramod = bool "use_paramod" true in
684 let skip_trie_filtering = bool "skip_trie_filtering" false in
685 let skip_context = bool "skip_context" false in
686 let use_only_paramod =
687 if for_applyS then true else bool "paramodulation" false in
688 let use_library = bool "library"
689 ((AutoTypes.default_flags()).AutoTypes.use_library) in
690 let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
691 let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
692 let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
693 let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
694 let do_type = bool "type" false in
695 let timeout = int "timeout" 0 in
696 { AutoTypes.maxdepth =
697 if use_only_paramod then 2 else depth;
698 AutoTypes.maxwidth = width;
699 AutoTypes.maxsize = size;
702 if for_applyS then Unix.gettimeofday () +. 30.0
706 Unix.gettimeofday() +. (float_of_int timeout);
707 AutoTypes.use_library = use_library;
708 AutoTypes.use_paramod = use_paramod;
709 AutoTypes.use_only_paramod = use_only_paramod;
710 AutoTypes.close_more = close_more;
711 AutoTypes.dont_cache_failures = false;
712 AutoTypes.maxgoalsizefactor = gsize;
713 AutoTypes.do_types = do_type;
714 AutoTypes.skip_trie_filtering = skip_trie_filtering;
715 AutoTypes.skip_context = skip_context;
718 (***************** applyS *******************)
721 dbd flags automation_cache univ proof goal newmeta' metasenv'
722 context term' ty termty goal_arity
724 (* let ppterm = ppterm context in *)
725 let (consthead,newmetasenv,arguments,_) =
726 TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
728 match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
730 let proof',oldmetasenv =
731 let (puri,metasenv,_subst,pbo,pty, attrs) = proof in
732 (puri,newmetasenv,_subst,pbo,pty, attrs),metasenv
734 let goal_for_paramod =
735 match LibraryObjects.eq_URI () with
737 Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
738 | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
740 let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
741 let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
743 let uri,_,_subst,p,ty, attrs = proof' in
744 uri,metasenv_for_paramod,_subst,p,ty, attrs
746 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
748 ProofEngineTypes.apply_tactic
749 (EqualityTactics.rewrite_tac ~direction:`RightToLeft
750 ~pattern:(ProofEngineTypes.conclusion_pattern None)
751 (Cic.Meta(newmeta,irl)) [])
754 let goal = match goals with [g] -> g | _ -> assert false in
756 ProofEngineTypes.apply_tactic
757 (PrimitiveTactics.apply_tac term'')
760 let universe, tables, cache =
761 init_cache_and_tables ~dbd ~use_library:flags.use_library
762 ~use_context:true automation_cache univ (proof'''',newmeta)
764 let active, passive, bag = tables in
766 Saturation.given_clause bag (proof'''',newmeta) active passive
770 raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
771 | Some (_,proof''''',_), active,passive,bag ->
773 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
774 ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive
778 ("SUBSUMPTION SU: " ^ string_of_int newmeta ^ " " ^ ppterm goal_for_paramod));
780 Saturation.all_subsumed bag maxm (proof'''',newmeta) active passive
783 raise (ProofEngineTypes.Fail (lazy("BUM")))
784 else let (_,proof''''',_) = List.hd res in
785 proof''''',ProofEngineHelpers.compare_metasenvs ~oldmetasenv
786 ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive
790 let rec count_prods context ty =
791 match CicReduction.whd context ty with
792 Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
796 ~dbd ~term ~subst ~automation_cache ~params:(univ,params) (proof, goal)
798 let module T = CicTypeChecker in
799 let module R = CicReduction in
800 let module C = Cic in
801 let (_,metasenv,_subst,_,_, _) = proof in
802 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
803 let flags = flags_of_params params ~for_applyS:true () in
804 let newmeta = CicMkImplicit.new_meta metasenv subst in
805 let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
807 C.Var (uri,exp_named_subst) ->
808 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
809 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
812 exp_named_subst_diff,newmeta',newmetasenvfragment,
813 C.Var (uri,exp_named_subst')
814 | C.Const (uri,exp_named_subst) ->
815 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
816 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
819 exp_named_subst_diff,newmeta',newmetasenvfragment,
820 C.Const (uri,exp_named_subst')
821 | C.MutInd (uri,tyno,exp_named_subst) ->
822 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
823 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
826 exp_named_subst_diff,newmeta',newmetasenvfragment,
827 C.MutInd (uri,tyno,exp_named_subst')
828 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
829 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
830 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
833 exp_named_subst_diff,newmeta',newmetasenvfragment,
834 C.MutConstruct (uri,tyno,consno,exp_named_subst')
835 | _ -> [],newmeta,[],term
837 let metasenv' = metasenv@newmetasenvfragment in
839 CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph
841 let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
842 let goal_arity = count_prods context ty in
843 let proof, gl, active, passive =
844 apply_smart_aux dbd flags automation_cache univ proof goal
845 newmeta' metasenv' context term' ty termty goal_arity
847 proof, gl, active, passive
850 (****************** AUTO ********************)
855 let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
858 let calculate_timeout flags =
859 if flags.timeout = 0. then
860 (debug_print (lazy "AUTO WITH NO TIMEOUT");
861 {flags with timeout = infinity})
865 let is_equational_case goalty flags =
866 let ensure_equational t =
867 if is_an_equational_goal t then true
870 let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
871 raise (ProofEngineTypes.Fail (lazy msg))
874 (flags.use_paramod && is_an_equational_goal goalty) ||
875 (flags.use_only_paramod && ensure_equational goalty)
878 let cache_add_success sort cache k v =
879 if sort = P then cache_add_success cache k v else cache_remove_underinspection
884 type menv = Cic.metasenv
885 type subst = Cic.substitution
886 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
887 let candidate_no = ref 0;;
888 type candidate = int * Cic.term Lazy.t
889 type cache = AutoCache.cache
892 (* the goal (mainly for depth) and key of the goal *)
893 goal * AutoCache.cache_key
895 (* goal has to be proved *)
897 (* goal has to be cached as a success obtained using candidate as the first
899 | S of goal * AutoCache.cache_key * candidate * int
901 (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
902 menv * subst * int * op list * op list * fail list
904 (* list of computations that may lead to the solution: all op list will
905 * end with the same (S(g,_)) *)
908 (* menv, subst, alternatives, tables, cache *)
909 | Proved of menv * subst * elem list * AutomationCache.tables * cache
910 | Gaveup of AutomationCache.tables * cache
913 (* the status exported to the external observer *)
915 (* context, (goal,candidate) list, and_list, history *)
916 Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
917 (int * Cic.term * int) list * Cic.term Lazy.t list
920 let rec aux acc = function
921 | (D g)::tl -> aux (acc@[g]) tl
927 List.filter (function (_,_,P) -> true | _ -> false) l
931 let rec aux acc = function
932 | (D g)::tl -> aux (acc@[g]) tl
933 | (S _)::tl -> aux acc tl
939 let calculate_goal_ty (goalno,_,_) s m =
941 let _,cc,goalty = CicUtil.lookup_meta goalno m in
942 (* XXX applicare la subst al contesto? *)
943 Some (cc, CicMetaSubst.apply_subst s goalty)
944 with CicUtil.Meta_not_found i when i = goalno -> None
947 let calculate_closed_goal_ty (goalno,_,_) s =
949 let cc,_,goalty = List.assoc goalno s in
950 (* XXX applicare la subst al contesto? *)
951 Some (cc, CicMetaSubst.apply_subst s goalty)
952 with Not_found -> None
955 let pp_status ctx status =
957 let names = Utils.names_of_context ctx in
960 ProofEngineReduction.replace
961 ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
962 ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
966 let string_of_do m s (gi,_,_ as g) d =
967 match calculate_goal_ty g s m with
968 | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
969 | None -> Printf.sprintf "D(%d, _, %d)" gi d
971 let string_of_s m su k (ci,ct) gi =
972 Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
974 let string_of_ol m su l =
978 | D (g,d,s) -> string_of_do m su (g,d,s) d
979 | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
982 let string_of_fl m s fl =
984 (List.map (fun ((i,_,_),ty) ->
985 Printf.sprintf "(%d, %s)" i (pp ty)) fl)
987 let rec aux = function
989 | (m,s,_,_,ol,fl)::tl ->
990 Printf.eprintf "< [%s] ;;; [%s]>\n"
991 (string_of_ol m s ol) (string_of_fl m s fl);
994 Printf.eprintf "-------------------------- status -------------------\n";
996 Printf.eprintf "-----------------------------------------------------\n";
999 let auto_status = ref [] ;;
1000 let auto_context = ref [];;
1001 let in_pause = ref false;;
1002 let pause b = in_pause := b;;
1003 let cond = Condition.create ();;
1004 let mutex = Mutex.create ();;
1005 let hint = ref None;;
1006 let prune_hint = ref [];;
1008 let step _ = Condition.signal cond;;
1009 let give_hint n = hint := Some n;;
1010 let give_prune_hint hint =
1011 prune_hint := hint :: !prune_hint
1018 Condition.wait cond mutex;
1023 let get_auto_status _ =
1024 let status = !auto_status in
1025 let and_list,elems,last =
1028 | (m,s,_,don,gl,fail)::tl ->
1031 (fun (id,d,_ as g) ->
1032 match calculate_goal_ty g s m with
1033 | Some (_,x) -> Some (id,x,d) | None -> None)
1037 (* these are the S goalsin the or list *)
1040 (fun (m,s,_,don,gl,fail) ->
1042 (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
1043 (List.rev don @ gl))
1046 (* this function eats id from a list l::[id,x] returning x, l *)
1047 let eat_tail_if_eq id l =
1048 let rec aux (s, l) = function
1050 | ((id1,_,_),k1,c)::tl when id = id1 ->
1052 | None -> aux (Some c,l) tl
1053 | Some _ -> assert false)
1054 | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
1056 let c, l = aux (None, []) l in
1059 let eat_in_parallel id l =
1060 let rec aux (b,eaten, new_l as acc) l =
1064 match eat_tail_if_eq id l with
1065 | None, l -> aux (b@[false], eaten, new_l@[l]) tl
1066 | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
1070 let rec eat_all rows l =
1074 match List.rev elem with
1075 | ((to_eat,depth,_),k,_)::next_lunch ->
1076 let b, eaten, l = eat_in_parallel to_eat l in
1077 let eaten = HExtlib.list_uniq eaten in
1078 let eaten = List.rev eaten in
1079 let b = true (* List.hd (List.rev b) *) in
1080 let rows = rows @ [to_eat,k,b,depth,eaten] in
1082 | [] -> eat_all rows or_list
1084 eat_all [] (List.rev orlist)
1088 (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
1091 (* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
1092 and_list, rows, history
1094 !auto_context, elems, and_list, last
1097 (* Works if there is no dependency over proofs *)
1098 let is_a_green_cut goalty =
1099 CicUtil.is_meta_closed goalty
1101 let rec first_s = function
1102 | (D _)::tl -> first_s tl
1103 | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
1106 let list_union l1 l2 =
1107 (* TODO ottimizzare compare *)
1108 HExtlib.list_uniq (List.sort compare (l1 @ l1))
1110 let rec eq_todo l1 l2 =
1112 | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
1113 | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
1114 when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
1115 if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
1119 let eat_head todo id fl orlist =
1120 let rec aux acc = function
1122 | (m, s, _, _, todo1, fl1)::tl as orlist ->
1123 let rec aux1 todo1 =
1124 match first_s todo1 with
1125 | None -> orlist, acc
1126 | Some (((gno,_,_),_,_,_), todo11) ->
1127 (* TODO confronto tra todo da ottimizzare *)
1128 if gno = id && eq_todo todo11 todo then
1129 aux (list_union fl1 acc) tl
1137 let close_proof p ty menv context =
1139 List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
1141 let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
1142 naif_closure p menv context
1144 (* XXX capire bene quando aggiungere alla cache *)
1145 let add_to_cache_and_del_from_orlist_if_green_cut
1146 g s m cache key todo orlist fl ctx size minsize
1148 let cache = cache_remove_underinspection cache key in
1149 (* prima per fare la irl usavamo il contesto vero e proprio e non quello
1151 match calculate_closed_goal_ty g s with
1152 | None -> assert false
1153 | Some (canonical_ctx , gty) ->
1154 let goalno,depth,sort = g in
1155 let irl = mk_irl canonical_ctx in
1156 let goal = Cic.Meta(goalno, irl) in
1157 let proof = CicMetaSubst.apply_subst s goal in
1158 let green_proof, closed_proof =
1159 let b = is_a_green_cut proof in
1161 b, (* close_proof proof gty m ctx *) proof
1165 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
1166 if is_a_green_cut key then
1167 (* if the initia goal was closed, we cut alternatives *)
1168 let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
1169 let orlist, fl = eat_head todo goalno fl orlist in
1171 if size < minsize then
1172 (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
1174 (* if the proof is closed we cache it *)
1175 if green_proof then cache_add_success cache key proof
1176 else (* cache_add_success cache key closed_proof *)
1177 (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
1179 cache, orlist, fl, true
1182 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
1183 if size < minsize then
1184 (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
1185 (* if the substituted goal and the proof are closed we cache it *)
1186 if is_a_green_cut gty then
1187 if green_proof then cache_add_success cache gty proof
1188 else (* cache_add_success cache gty closed_proof *)
1189 (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
1193 CicTypeChecker.type_of_aux' ~subst:s
1194 m ctx closed_proof CicUniv.oblivion_ugraph
1196 if is_a_green_cut ty then
1197 cache_add_success cache ty closed_proof
1200 | CicTypeChecker.TypeCheckerFailure _ ->*)
1201 (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
1203 cache, orlist, fl, false
1205 let close_failures (fl : fail list) (cache : cache) =
1207 (fun cache ((gno,depth,_),gty) ->
1208 debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
1209 cache_add_failure cache gty depth)
1212 let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
1213 let entry = goalno, (canonical_ctx, t,ty) in
1214 assert_subst_are_disjoint subst [entry];
1215 let subst = entry :: subst in
1217 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1222 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
1223 None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
1226 tables cache depth fake_proof goalno goalty subst context
1229 let active,passive,bag = tables in
1230 let ppterm = ppterm context in
1231 let status = (fake_proof,goalno) in
1232 if flags.use_only_paramod then
1234 debug_print (lazy ("PARAMODULATION SU: " ^
1235 string_of_int goalno ^ " " ^ ppterm goalty ));
1236 let goal_steps, saturation_steps, timeout =
1237 max_int,max_int,flags.timeout
1241 Saturation.given_clause bag status active passive
1242 goal_steps saturation_steps timeout
1244 | None, active, passive, bag ->
1245 [], (active,passive,bag), cache, flags
1246 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
1248 assert_subst_are_disjoint subst subst';
1249 let subst = subst@subst' in
1251 order_new_goals metasenv subst open_goals ppterm
1254 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1257 [(!candidate_no,proof),metasenv,subst,open_goals],
1258 (active,passive,bag), cache, flags
1264 ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty));
1265 let res = Saturation.all_subsumed bag status active passive in
1268 (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
1269 assert_subst_are_disjoint subst subst';
1270 let subst = subst@subst' in
1272 order_new_goals metasenv subst open_goals ppterm
1275 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1278 (!candidate_no,proof),metasenv,subst,open_goals)
1281 res', (active,passive,bag), cache, flags
1286 goalty tables subst fake_proof goalno depth context cand
1288 let ppterm = ppterm context in
1290 let actives, passives, bag = tables in
1291 let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
1292 (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:(Equality.maxmeta bag) ~term:cand)
1295 let tables = actives, passives, Equality.push_maxmeta bag maxmeta in
1296 debug_print (lazy (" OK: " ^ ppterm cand));
1297 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
1298 let open_goals = order_new_goals metasenv subst open_goals ppterm in
1299 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
1301 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
1303 | ProofEngineTypes.Fail s -> None,tables
1304 | CicUnification.Uncertain s -> None,tables
1307 let sort_new_elems =
1308 List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
1309 List.length (prop_only l1) - List.length (prop_only l2))
1312 let applicative_case
1313 tables depth subst fake_proof goalno goalty metasenv context universe
1316 let candidates = get_candidates flags.skip_trie_filtering universe cache goalty in
1319 (fun (tables,elems) cand ->
1321 try_candidate goalty
1322 tables subst fake_proof goalno depth context cand
1324 | None, tables -> tables, elems
1325 | Some x, tables -> tables, x::elems)
1326 (tables,[]) candidates
1328 let elems = sort_new_elems elems in
1329 elems, tables, cache
1332 let equational_and_applicative_case
1333 universe flags m s g gty tables cache context
1335 let goalno, depth, sort = g in
1336 let fake_proof = mk_fake_proof m s g gty context in
1337 if is_equational_case gty flags then
1338 let elems,tables,cache, flags =
1339 equational_case tables cache
1340 depth fake_proof goalno gty s context flags
1342 let more_elems, tables, cache =
1343 if flags.use_only_paramod then
1347 tables depth s fake_proof goalno
1348 gty m context universe cache flags
1350 elems@more_elems, tables, cache, flags
1352 let elems, tables, cache =
1353 applicative_case tables depth s fake_proof goalno
1354 gty m context universe cache flags
1356 elems, tables, cache, flags
1358 let rec condition_for_hint i = function
1360 | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
1361 | _::tl -> condition_for_hint i tl
1363 let remove_s_from_fl (id,_,_) (fl : fail list) =
1364 let rec aux = function
1366 | ((id1,_,_),_)::tl when id = id1 -> tl
1367 | hd::tl -> hd :: aux tl
1372 let prunable_for_size flags s m todo =
1373 let rec aux b = function
1374 | (S _)::tl -> aux b tl
1375 | (D (_,_,T))::tl -> aux b tl
1377 (match calculate_goal_ty g s m with
1379 | Some (canonical_ctx, gty) ->
1381 Utils.weight_of_term
1382 ~consider_metas:false ~count_metas_occurrences:true gty in
1383 let newb = b || gsize > flags.maxgoalsizefactor in
1390 let prunable ty todo =
1391 let rec aux b = function
1392 | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
1393 | (D (_,_,T))::tl -> aux b tl
1401 let prunable menv subst ty todo =
1402 let rec aux = function
1403 | (S(_,k,_,_))::tl ->
1404 (match Equality.meta_convertibility_subst k ty menv with
1407 no_progress variant tl (* || aux tl*))
1408 | (D (_,_,T))::tl -> aux tl
1410 and no_progress variant = function
1411 | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
1412 | D ((n,_,P) as g)::tl ->
1413 (match calculate_goal_ty g subst menv with
1414 | None -> no_progress variant tl
1416 (match calculate_goal_ty g variant menv with
1417 | None -> assert false
1419 if gty = gty' then no_progress variant tl
1421 (prerr_endline (string_of_int n);
1422 prerr_endline (CicPp.ppterm gty);
1423 prerr_endline (CicPp.ppterm gty');
1424 prerr_endline "---------- subst";
1425 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
1426 prerr_endline "---------- variant";
1427 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
1428 prerr_endline "---------- menv";
1429 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
1430 no_progress variant tl) *)
1432 | _::tl -> no_progress variant tl
1437 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
1439 HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
1441 List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
1443 let filter_prune_hint l =
1444 let prune = !prune_hint in
1445 prune_hint := []; (* possible race... *)
1446 if prune = [] then l
1447 else List.filter (condition_for_prune_hint prune) l
1449 let auto_main tables context flags universe cache elems =
1450 auto_context := context;
1451 let rec aux tables flags cache (elems : status) =
1452 (* pp_status context elems; *)
1453 (* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
1454 auto_status := elems;
1457 let elems = filter_prune_hint elems in
1459 | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
1460 debug_print (lazy "skip");
1462 | Some i when condition_for_hint i todo ->
1463 aux tables flags cache orlist
1466 aux tables flags cache elems)
1468 (* complete failure *)
1469 debug_print (lazy "give up");
1470 Gaveup (tables, cache)
1471 | (m, s, _, _, [],_)::orlist ->
1472 (* complete success *)
1473 debug_print (lazy "success");
1474 Proved (m, s, orlist, tables, cache)
1475 | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist
1476 when not flags.AutoTypes.do_types ->
1477 (* skip since not Prop, don't even check if closed by side-effect *)
1478 debug_print (lazy "skip existential goal");
1479 aux tables flags cache ((m, s, size, don, todo, fl)::orlist)
1480 | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
1481 (* partial success, cache g and go on *)
1482 let cache, orlist, fl, sibling_pruned =
1483 add_to_cache_and_del_from_orlist_if_green_cut
1484 g s m cache key todo orlist fl context size minsize
1486 debug_print (lazy (AutoCache.cache_print context cache));
1487 let fl = remove_s_from_fl g fl in
1488 let don = if sibling_pruned then don else op::don in
1489 aux tables flags cache ((m, s, size, don, todo, fl)::orlist)
1490 | (m, s, size, don, todo, fl)::orlist
1491 when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1492 debug_print (lazy ("FAIL: WIDTH"));
1493 (* too many goals in and generated by last th *)
1494 let cache = close_failures fl cache in
1495 aux tables flags cache orlist
1496 | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
1498 (lazy ("FAIL: SIZE: "^string_of_int size ^
1499 " > " ^ string_of_int flags.maxsize ));
1500 (* we already have a too large proof term *)
1501 let cache = close_failures fl cache in
1502 aux tables flags cache orlist
1503 | _ when Unix.gettimeofday () > flags.timeout ->
1505 debug_print (lazy ("FAIL: TIMEOUT"));
1506 Gaveup (tables, cache)
1507 | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
1509 debug_print (lazy "attack goal");
1510 match calculate_goal_ty g s m with
1512 (* closed by side effect *)
1513 debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1514 aux tables flags cache ((m,s,size,don,todo, fl)::orlist)
1515 | Some (canonical_ctx, gty) ->
1517 Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty
1519 if gsize > flags.maxgoalsizefactor then
1520 (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
1521 aux tables flags cache orlist)
1522 else if prunable_for_size flags s m todo then
1523 (debug_print (lazy ("POTO at depth: "^(string_of_int depth)));
1524 aux tables flags cache orlist)
1526 (* still to be proved *)
1527 (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
1528 match cache_examine cache gty with
1529 | Failed_in d when d >= depth ->
1531 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1532 let cache = close_failures fl cache in
1533 aux tables flags cache orlist
1534 | UnderInspection ->
1536 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1537 let cache = close_failures fl cache in
1538 aux tables flags cache orlist
1540 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1541 let s, m = put_in_subst s m g canonical_ctx t gty in
1542 aux tables flags cache ((m, s, size, don,todo, fl)::orlist)
1544 | Failed_in _ when depth > 0 ->
1545 ( (* more depth or is the first time we see the goal *)
1546 if prunable m s gty todo then
1548 "FAIL: LOOP: one father is equal"));
1549 aux tables flags cache orlist)
1551 let cache = cache_add_underinspection cache gty depth in
1552 auto_status := status;
1555 (lazy ("INSPECTING: " ^
1556 string_of_int gno ^ "("^ string_of_int size ^ "): "^
1558 (* elems are possible computations for proving gty *)
1559 let elems, tables, cache, flags =
1560 equational_and_applicative_case
1561 universe flags m s g gty tables cache context
1564 (* this goal has failed *)
1565 let cache = close_failures ((g,gty)::fl) cache in
1566 aux tables flags cache orlist
1568 (* elems = (cand,m,s,gl) *)
1569 let size_gl l = List.length
1570 (List.filter (function (_,_,P) -> true | _ -> false) l)
1573 let inj_gl gl = List.map (fun g -> D g) gl in
1574 let rec map = function
1575 | [] -> assert false
1576 | (cand,m,s,gl)::[] ->
1577 (* in the last one we add the failure *)
1579 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1581 (* we are the last in OR, we fail on g and
1582 * also on all failures implied by g *)
1583 (m,s, size + size_gl gl, don, todo, (g,gty)::fl)
1585 | (cand,m,s,gl)::tl ->
1586 (* we add the S step after gl and before todo *)
1588 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1590 (* since we are not the last in OR, we do not
1592 (m,s, size + size_gl gl, don, todo, []) :: map tl
1596 aux tables flags cache elems)
1599 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1600 let cache = close_failures fl cache in
1601 aux tables flags cache orlist)
1603 (aux tables flags cache elems : auto_result)
1608 auto_all_solutions tables universe cache context metasenv gl flags
1610 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1613 (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1615 let elems = [metasenv,[],1,[],goals,[]] in
1616 let rec aux tables solutions cache elems flags =
1617 match auto_main tables context flags universe cache elems with
1618 | Gaveup (tables,cache) ->
1619 solutions,cache, tables
1620 | Proved (metasenv,subst,others,tables,cache) ->
1621 if Unix.gettimeofday () > flags.timeout then
1622 ((subst,metasenv)::solutions), cache, tables
1624 aux tables ((subst,metasenv)::solutions) cache others flags
1626 let rc = aux tables [] cache elems flags in
1628 | [],cache,tables -> [],cache,tables
1629 | solutions, cache,tables ->
1632 (fun (subst,newmetasenv) ->
1634 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1636 if opened = [] then Some subst else None)
1639 solutions,cache,tables
1642 (******************* AUTO ***************)
1644 let auto flags metasenv tables universe cache context metasenv gl =
1645 let initial_time = Unix.gettimeofday() in
1646 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1647 let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1648 let elems = [metasenv,[],1,[],goals,[]] in
1649 match auto_main tables context flags universe cache elems with
1650 | Proved (metasenv,subst,_, tables,cache) ->
1652 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1653 Some (subst,metasenv), cache
1654 | Gaveup (tables,cache) ->
1656 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1660 let applyS_tac ~dbd ~term ~params ~automation_cache =
1661 ProofEngineTypes.mk_tactic
1665 apply_smart ~dbd ~term ~subst:[] ~params ~automation_cache status
1669 | CicUnification.UnificationFailure msg
1670 | CicTypeChecker.TypeCheckerFailure msg ->
1671 raise (ProofEngineTypes.Fail msg))
1673 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
1674 let flags = flags_of_params params () in
1675 let use_library = flags.use_library in
1676 let universe, tables, cache =
1677 init_cache_and_tables
1678 ~dbd ~use_library ~use_context:(not flags.skip_context)
1679 automation_cache univ (proof, goal)
1681 let _,metasenv,_subst,_,_, _ = proof in
1682 let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1684 if flags.close_more then
1686 tables context (proof, goal)
1687 auto_all_solutions universe cache
1688 else tables,cache in
1689 let initial_time = Unix.gettimeofday() in
1690 let (_,oldmetasenv,_subst,_,_, _) = proof in
1693 metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[]
1695 match auto_main tables context flags universe cache [elem] with
1696 | Proved (metasenv,subst,_, tables,cache) ->
1698 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1699 let proof,metasenv =
1700 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1701 proof goal subst metasenv
1704 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1705 ~newmetasenv:metasenv
1708 | Gaveup (tables,cache) ->
1711 string_of_float(Unix.gettimeofday()-.initial_time)));
1712 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1715 let auto_tac ~dbd ~params ~automation_cache =
1716 ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~automation_cache);;
1718 let eq_of_goal = function
1719 | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1721 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1724 (* performs steps of rewrite with the universe, obtaining if possible
1726 let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal as status)=
1727 let steps = int_of_string (string params "steps" "1") in
1728 let universe, tables, cache =
1729 init_cache_and_tables ~use_library:false ~use_context:false
1730 automation_cache univ (proof,goal)
1732 let actives, passives, bag = tables in
1733 let _,metasenv,_subst,_,_,_ = proof in
1734 let _,context,ty = CicUtil.lookup_meta goal metasenv in
1735 let eq_uri = eq_of_goal ty in
1736 let initgoal = [], metasenv, ty in
1738 let equalities = (Saturation.list_of_passive passives) in
1739 List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd actives) equalities
1741 let env = metasenv,context,CicUniv.oblivion_ugraph in
1742 match Indexing.solve_demodulating bag env table initgoal steps with
1743 | Some (proof, metasenv, newty) ->
1746 | Cic.Appl[Cic.MutInd _;eq_ty;left;_] ->
1747 Equality.Exact (Equality.refl_proof eq_uri eq_ty left)
1751 Equality.build_goal_proof
1752 bag eq_uri proof refl newty [] context metasenv
1754 ProofEngineTypes.apply_tactic
1755 (PrimitiveTactics.apply_tac ~term:proofterm) status
1758 (ProofEngineTypes.Fail (lazy
1759 ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
1761 let solve_rewrite_tac ~params ~automation_cache () =
1762 ProofEngineTypes.mk_tactic (solve_rewrite_tac ~automation_cache ~params)
1765 (* Demodulate thorem *)
1766 let open_type ty bo =
1767 let rec open_type_aux context ty k args =
1769 | Cic.Prod (n,s,t) ->
1771 FreshNamesGenerator.mk_fresh_name [] context n ~typ:s ~subst:[] in
1772 let entry = match n' with
1773 | Cic.Name _ -> Some (n',(Cic.Decl s))
1774 | Cic.Anonymous -> None
1776 open_type_aux (entry::context) t (k+1) ((Cic.Rel k)::args)
1777 | Cic.LetIn (n,s,sty,t) ->
1778 let entry = Some (n,(Cic.Def (s,sty)))
1780 open_type_aux (entry::context) t (k+1) args
1781 | _ -> context, ty, args
1783 let context, ty, args = open_type_aux [] ty 1 [] in
1785 | [] -> context, ty, bo
1786 | _ -> context, ty, Cic.Appl (bo::args)
1789 let rec close_type bo ty context =
1791 | [] -> assert_proof_is_valid bo [] [] ty; (bo,ty)
1792 | Some (n,(Cic.Decl s))::tl ->
1793 close_type (Cic.Lambda (n,s,bo)) (Cic.Prod (n,s,ty)) tl
1794 | Some (n,(Cic.Def (s,sty)))::tl ->
1795 close_type (Cic.LetIn (n,s,sty,bo)) (Cic.LetIn (n,s,sty,ty)) tl
1799 let is_subsumed univ context ty =
1800 let candidates = Universe.get_candidates univ ty in
1804 | Some found -> Some found
1807 let mk_irl = CicMkImplicit.identity_relocation_list_for_metavariable in
1808 let metasenv = [(0,context,ty)] in
1809 let fake_proof = None,metasenv,[] , (lazy (Cic.Meta(0,mk_irl context))),ty,[] in
1810 let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
1811 (PrimitiveTactics.apply_with_subst ~subst:[] ~maxmeta:0 ~term:cand) (fake_proof,0)
1813 let prop_goals, other = split_goals_in_prop metasenv subst open_goals in
1814 if prop_goals = [] then Some cand else None
1816 | ProofEngineTypes.Fail s -> None
1817 | CicUnification.Uncertain s -> None
1821 let demodulate_theorem ~automation_cache uri =
1823 match LibraryObjects.eq_URI () with
1825 | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
1826 let obj,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
1830 | Cic.Constant(n, _, ty ,_, _) -> open_type ty (Cic.Const(uri,[]))
1831 | _ -> raise (ProofEngineTypes.Fail (lazy "not a theorem"))
1833 if CicUtil.is_closed ty then
1834 raise (ProofEngineTypes.Fail (lazy ("closed term: dangerous reduction")));
1835 let initgoal = [], [], ty in
1836 (* compute the signature *)
1838 let ty_set = MetadataConstraints.constants_of ty in
1839 let hyp_set = MetadataQuery.signature_of_hypothesis context [] in
1840 let set = MetadataConstraints.UriManagerSet.union ty_set hyp_set in
1841 MetadataQuery.close_with_types set [] context
1843 (* retrieve equations from the universe universe *)
1844 (* XXX automation_cache *)
1845 let universe = automation_cache.AutomationCache.univ in
1847 retrieve_equations true signature universe AutoCache.cache_empty context []
1850 (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
1855 CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph
1857 (* retrieve_equations could also return flexible terms *)
1858 if is_an_equality ty then Some(t,ty)
1861 let ty' = unfold context ty in
1862 if is_an_equality ty' then Some(t,ty') else None
1863 with ProofEngineTypes.Fail _ -> None)
1866 let bag = Equality.mk_equality_bag () in
1868 let bag, units, _, newmeta =
1869 partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types
1873 (fun tbl eq -> Indexing.index tbl eq)
1874 Indexing.empty units
1876 let changed,(newproof,newmetasenv, newty) =
1878 ([],context,CicUniv.oblivion_ugraph) table initgoal in
1881 let oldproof = Equality.Exact bo in
1883 Equality.build_goal_proof (~contextualize:false) (~forward:true) bag
1884 eq_uri newproof oldproof ty [] context newmetasenv
1886 if newmetasenv <> [] then
1887 raise (ProofEngineTypes.Fail (lazy ("metasenv not empty")))
1890 assert_proof_is_valid proofterm newmetasenv context newty;
1891 match is_subsumed universe context newty with
1893 (ProofEngineTypes.Fail (lazy ("subsumed by " ^ CicPp.ppterm t)))
1894 | None -> close_type proofterm newty context
1897 else (* if newty = ty then *)
1898 raise (ProofEngineTypes.Fail (lazy "no progress"))
1899 (*else ProofEngineTypes.apply_tactic
1900 (ReductionTactics.simpl_tac
1901 ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1905 (* NEW DEMODULATE *)
1906 let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)=
1907 let universe, tables, cache =
1908 init_cache_and_tables
1909 ~dbd ~use_library:false ~use_context:true
1910 automation_cache univ (proof,goal)
1913 match LibraryObjects.eq_URI () with
1915 | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
1916 let active, passive, bag = tables in
1917 let curi,metasenv,_subst,pbo,pty, attrs = proof in
1918 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1919 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1920 let initgoal = [], metasenv, ty in
1921 let equalities = (Saturation.list_of_passive passive) in
1922 (* we demodulate using both actives passives *)
1923 let env = metasenv,context,CicUniv.empty_ugraph in
1924 debug_print (lazy ("PASSIVES:" ^ string_of_int(List.length equalities)));
1925 List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))
1929 (fun tbl eq -> Indexing.index tbl eq)
1930 (snd active) equalities
1932 let changed,(newproof,newmetasenv, newty) =
1933 (* Indexing.demodulation_goal bag *)
1935 (metasenv,context,CicUniv.oblivion_ugraph) table initgoal
1939 let maxm = CicMkImplicit.new_meta metasenv [] in
1940 let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1942 Equality.build_goal_proof (~contextualize:false) bag
1943 eq_uri newproof opengoal ty [] context metasenv
1945 let extended_metasenv = (maxm,context,newty)::metasenv in
1946 let extended_status =
1947 (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in
1948 let (status,newgoals) =
1949 ProofEngineTypes.apply_tactic
1950 (PrimitiveTactics.apply_tac ~term:proofterm)
1952 (status,maxm::newgoals)
1954 else (* if newty = ty then *)
1955 raise (ProofEngineTypes.Fail (lazy "no progress"))
1956 (*else ProofEngineTypes.apply_tactic
1957 (ReductionTactics.simpl_tac
1958 ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1961 let demodulate_tac ~dbd ~params ~automation_cache =
1962 ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~automation_cache);;
1964 let pp_proofterm = Equality.pp_proofterm;;
1966 let revision = "$Revision$";;
1967 let size_and_depth context metasenv t = 100, 100