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/.
29 let debug_print s = prerr_endline (Lazy.force s);;
31 (* functions for retrieving theorems *)
33 exception FillingFailure of AutoCache.cache * int
35 let rec unfold context = function
36 | Cic.Prod(name,s,t) ->
37 let t' = unfold ((Some (name,Cic.Decl s))::context) t in
39 | t -> ProofEngineReduction.unfold context t
41 let find_library_theorems dbd proof goal =
42 let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
43 let terms = List.map CicUtil.term_of_uri univ in
46 (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)))
49 let find_context_theorems context metasenv =
52 (fun (res,i) ctxentry ->
54 | Some (_,Cic.Decl t) ->
55 (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
56 | Some (_,Cic.Def (_,Some t)) ->
57 (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
58 | Some (_,Cic.Def (_,None)) ->
61 CicTypeChecker.type_of_aux'
62 metasenv context t CicUniv.empty_ugraph
69 let rec is_an_equality = function
70 | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _]
71 when (LibraryObjects.is_eq_URI uri) -> true
72 | Cic.Prod (_, _, t) -> is_an_equality t
76 let partition_equalities =
77 List.partition (fun (_,ty) -> is_an_equality ty)
80 let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;;
83 let is_unit_equation context metasenv oldnewmeta term =
84 let head, metasenv, args, newmeta =
85 ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
87 let propositional_args =
91 let _,_,mt = CicUtil.lookup_meta i metasenv in
93 CicTypeChecker.type_of_aux' metasenv context mt
97 CicReduction.are_convertible ~metasenv context
98 sort (Cic.Sort Cic.Prop) u
100 if b then Some i else None
104 if propositional_args = [] then
105 let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
106 Some (args,metasenv,newmetas,head,newmeta)
110 let get_candidates universe cache t =
112 (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
115 (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^
116 (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
117 debug_print debug_msg;
121 let only singature context t =
123 let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
124 let consts = MetadataConstraints.constants_of ty in
125 MetadataConstraints.UriManagerSet.subset consts singature
129 let retrieve_equations signature universe cache context=
130 match LibraryObjects.eq_URI() with
133 let eq_uri = UriManager.strip_xpointer eq_uri in
134 let fake= Cic.Meta(-1,[]) in
135 let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
136 let candidates = get_candidates universe cache fake_eq in
137 List.filter (only signature context) candidates
139 let build_equality bag head args proof newmetas maxmeta =
141 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
143 if args = [] then proof else Cic.Appl (proof::args)
145 let o = !Utils.compare_terms t1 t2 in
146 let stat = (ty,t1,t2,o) in
147 (* let w = compute_equality_weight stat in *)
149 let proof = Equality.Exact p in
150 let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
151 (* to clean the local context of metas *)
152 Equality.fix_metas bag maxmeta e
156 let partition_unit_equalities context metasenv newmeta bag equations =
158 (fun (units,other,maxmeta)(t,ty) ->
159 match is_unit_equation context metasenv maxmeta ty with
160 | Some (args,metasenv,newmetas,head,newmeta') ->
161 let maxmeta,equality =
162 build_equality bag head args t newmetas newmeta' in
163 equality::units,other,maxmeta
165 units,(t,ty)::other,maxmeta)
166 ([],[],newmeta) equations
169 (Saturation.make_active [],
170 Saturation.make_passive [],
171 Equality.mk_equality_bag)
173 let init_cache_and_tables dbd use_library universe (proof, goal) =
174 (* the local cache in initially empty *)
175 let cache = AutoCache.cache_empty in
176 let _, metasenv, _, _ = proof in
177 let signature = MetadataQuery.signature_of metasenv goal in
178 let newmeta = CicMkImplicit.new_meta metasenv [] in
179 let _,context,_ = CicUtil.lookup_meta goal metasenv in
180 let ct = find_context_theorems context metasenv in
183 find_library_theorems dbd metasenv goal
185 (* all equations are added to the cache *)
187 ("ho trovato nella libreria " ^ (string_of_int (List.length lt)));
188 (* let cache = cache_add_list AutoCache.cache_empty context (ct@lt) in *)
189 let cache = cache_add_list cache context (ct@lt) in
190 let equations = retrieve_equations signature universe cache context in
192 ("ho trovato equazioni n. " ^ (string_of_int (List.length equations)));
197 CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
198 (* retrieve_equations could also return flexible terms *)
199 if is_an_equality ty then Some(t,ty)
202 let ty' = unfold context ty in
203 if is_an_equality ty' then Some(t,ty') else None
204 with _ -> None) (* catturare l'eccezione giusta di unfold *)
206 let bag = Equality.mk_equality_bag () in
207 let units, other_equalities, newmeta =
208 partition_unit_equalities context metasenv newmeta bag eqs_and_types in
209 (* let env = (metasenv, context, CicUniv.empty_ugraph) in
212 match LibraryObjects.eq_URI() with
213 | None ->assert false
214 | Some eq_uri -> eq_uri in
215 Saturation.simplify_equalities bag eq_uri env units in *)
216 let passive = Saturation.make_passive units in
217 let no = List.length units in
218 let active = Saturation.make_active [] in
219 let active,passive,newmeta =
220 Saturation.pump_actives context bag newmeta active passive (no+1) infinity
222 (active,passive,bag),cache,newmeta
224 let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast =
225 let head, metasenv, args, newmeta =
226 ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
228 let propositional_args =
232 let _,_,mt = CicUtil.lookup_meta i metasenv in
234 CicTypeChecker.type_of_aux' metasenv context mt
238 CicReduction.are_convertible ~metasenv context
239 sort (Cic.Sort Cic.Prop) u
241 if b then Some i else None
245 let results,cache,newmeta =
246 if propositional_args = [] then
247 let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
248 [args,metasenv,newmetas,head,newmeta],cache,newmeta
252 None,metasenv,term,term (* term non e' significativo *)
256 {AutoTypes.default_flags() with
257 AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
258 maxwidth = 2;maxdepth = 2;
259 use_paramod=true;use_only_paramod=false}
261 {AutoTypes.default_flags() with
262 AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
263 maxwidth = 2;maxdepth = 4;
264 use_paramod=true;use_only_paramod=false}
266 match auto newmeta tables universe cache context metasenv propositional_args flags with
267 | [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
268 | substs,cache,newmeta ->
272 CicMetaSubst.apply_subst_metasenv subst metasenv
274 let head = CicMetaSubst.apply_subst subst head in
276 List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
278 let args = List.map (CicMetaSubst.apply_subst subst) args in
279 let newm = CicMkImplicit.new_meta metasenv subst in
280 args,metasenv,newmetas,head,max newm newmeta)
281 substs, cache, newmeta
283 results,cache,newmeta
285 let build_equalities auto context metasenv tables universe cache newmeta equations =
287 (fun (facts,cache,newmeta) (t,ty) ->
288 (* in any case we add the equation to the cache *)
289 let cache = AutoCache.cache_add_list cache context [(t,ty)] in
291 let saturated,cache,newmeta =
292 fill_hypothesis context metasenv newmeta ty tables universe cache auto true
294 let (active,passive,bag) = tables in
295 let eqs,bag,newmeta =
297 (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') ->
298 let maxmeta,equality =
299 build_equality bag head args t newmetas newmeta'
301 equality::acc,bag,maxmeta)
302 ([],bag,newmeta) saturated
304 (eqs@facts, cache, newmeta)
305 with FillingFailure (cache,newmeta) ->
306 (* if filling hypothesis fails we add the equation to
308 (facts,cache,newmeta)
310 ([],cache,newmeta) equations
312 let close_more tables maxmeta context status auto universe cache =
313 let (active,passive,bag) = tables in
314 let proof, goalno = status in
315 let _, metasenv,_,_ = proof in
316 let signature = MetadataQuery.signature_of metasenv goalno in
317 let equations = retrieve_equations signature universe cache context in
322 CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
323 (* retrieve_equations could also return flexible terms *)
324 if is_an_equality ty then Some(t,ty) else None)
326 let units, cache, maxm =
327 build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in
328 prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
331 (fun e -> prerr_endline (Equality.string_of_equality e))
333 prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
334 let passive = Saturation.add_to_passive units passive in
335 let no = List.length units in
336 prerr_endline ("No = " ^ (string_of_int no));
337 let active,passive,newmeta =
338 Saturation.pump_actives context bag maxm active passive (no+1) infinity
340 (active,passive,bag),cache,newmeta
342 let find_context_equalities
343 maxmeta bag context proof (universe:Universe.universe) cache
345 let module C = Cic in
346 let module S = CicSubstitution in
347 let module T = CicTypeChecker in
348 let _,metasenv,_,_ = proof in
349 let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
350 (* if use_auto is true, we try to close the hypothesis of equational
351 statements using auto; a naif, and probably wrong approach *)
352 let rec aux cache index newmeta = function
353 | [] -> [], newmeta,cache
354 | (Some (_, C.Decl (term)))::tl ->
357 (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
358 let do_find context term =
360 | C.Prod (name, s, t) when is_an_equality t ->
363 let term = S.lift index term in
364 let saturated,cache,newmeta =
365 fill_hypothesis context metasenv newmeta term
366 empty_tables universe cache default_auto false
370 (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
371 let newmeta, equality =
373 bag head args (Cic.Rel index) newmetas (max newmeta newmeta')
375 equality::acc, newmeta + 1)
376 ([],newmeta) saturated
379 with FillingFailure (cache,newmeta) ->
381 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
382 when LibraryObjects.is_eq_URI uri ->
383 let term = S.lift index term in
385 build_equality bag term [] (Cic.Rel index) [] newmeta
387 [e], (newmeta+1),cache
388 | _ -> [], newmeta, cache
390 let eqs, newmeta, cache = do_find context term in
391 let rest, newmeta,cache = aux cache (index+1) newmeta tl in
392 List.map (fun x -> index,x) eqs @ rest, newmeta, cache
394 aux cache (index+1) newmeta tl
396 let il, maxm, cache =
397 aux cache 1 newmeta context
399 let indexes, equalities = List.split il in
400 indexes, equalities, maxm, cache
403 (***************** applyS *******************)
405 let new_metasenv_and_unify_and_t
406 dbd flags universe proof goal ?tables newmeta' metasenv'
407 context term' ty termty goal_arity
409 let (consthead,newmetasenv,arguments,_) =
410 ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
412 match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
414 let proof',oldmetasenv =
415 let (puri,metasenv,pbo,pty) = proof in
416 (puri,newmetasenv,pbo,pty),metasenv
418 let goal_for_paramod =
419 match LibraryObjects.eq_URI () with
421 Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
422 | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
424 let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
425 let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
426 let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in
427 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
429 ProofEngineTypes.apply_tactic
430 (EqualityTactics.rewrite_tac ~direction:`RightToLeft
431 ~pattern:(ProofEngineTypes.conclusion_pattern None)
432 (Cic.Meta(newmeta,irl)))
435 let goal = match goals with [g] -> g | _ -> assert false in
436 let subst, (proof'''', _), _ =
437 PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
440 let (active, passive,bag), cache, maxmeta =
441 init_cache_and_tables dbd flags.use_library universe (proof'''',newmeta)
443 Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
444 max_int max_int flags.timeout
447 raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
448 | Some (_,proof''''',_), active,passive,_ ->
450 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
451 ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive
454 let rec count_prods context ty =
455 match CicReduction.whd context ty with
456 Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
459 let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
460 let module T = CicTypeChecker in
461 let module R = CicReduction in
462 let module C = Cic in
463 let (_,metasenv,_,_) = proof in
464 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
465 let newmeta = CicMkImplicit.new_meta metasenv subst in
466 let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
468 C.Var (uri,exp_named_subst) ->
469 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
470 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
473 exp_named_subst_diff,newmeta',newmetasenvfragment,
474 C.Var (uri,exp_named_subst')
475 | C.Const (uri,exp_named_subst) ->
476 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
477 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
480 exp_named_subst_diff,newmeta',newmetasenvfragment,
481 C.Const (uri,exp_named_subst')
482 | C.MutInd (uri,tyno,exp_named_subst) ->
483 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
484 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
487 exp_named_subst_diff,newmeta',newmetasenvfragment,
488 C.MutInd (uri,tyno,exp_named_subst')
489 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
490 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
491 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
494 exp_named_subst_diff,newmeta',newmetasenvfragment,
495 C.MutConstruct (uri,tyno,consno,exp_named_subst')
496 | _ -> [],newmeta,[],term
498 let metasenv' = metasenv@newmetasenvfragment in
500 CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
502 let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
503 let goal_arity = count_prods context ty in
504 let subst, proof, gl, active, passive =
505 new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
506 newmeta' metasenv' context term' ty termty goal_arity
508 subst, proof, gl, active, passive
511 (****************** AUTO ********************)
513 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
514 let ugraph = CicUniv.empty_ugraph;;
515 let typeof = CicTypeChecker.type_of_aux';;
517 let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
520 let is_in_prop context subst metasenv ty =
521 let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
522 fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
524 let assert_proof_is_valid proof metasenv context goalty =
525 let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
526 let b,_ = CicReduction.are_convertible context ty goalty u in
530 List.map (function None -> None | Some (x,_) -> Some x) context
532 prerr_endline ("PROOF:" ^ CicPp.pp proof names);
533 prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
534 prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
535 prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
539 let assert_subst_are_disjoint subst subst' =
541 (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
545 List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2)
548 let split_goals_in_prop metasenv subst gl =
551 let _,context,ty = CicUtil.lookup_meta g metasenv in
553 let sort,u = typeof ~subst metasenv context ty ugraph in
555 CicReduction.are_convertible
556 ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
559 | CicTypeChecker.AssertFailure s
560 | CicTypeChecker.TypeCheckerFailure s ->
562 (lazy (ppterm context (CicMetaSubst.apply_subst subst ty)));
565 (* FIXME... they should type! *)
569 let split_goals_with_metas metasenv subst gl =
572 let _,context,ty = CicUtil.lookup_meta g metasenv in
573 let ty = CicMetaSubst.apply_subst subst ty in
574 CicUtil.is_meta_closed ty)
578 let order_new_goals metasenv subst open_goals ppterm =
579 let prop,rest = split_goals_in_prop metasenv subst open_goals in
580 let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
582 (List.map (fun x -> x,P) (closed_prop @ open_prop))
584 (List.map (fun x -> x,T) rest)
589 let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals
591 debug_print (lazy (" OPEN: "^
595 | (i,t,P) -> string_of_int i (* ":"^ppterm t^ "Prop" *)
596 | (i,t,T) -> string_of_int i ) (* ":"^ppterm t^ "Type")*)
601 let is_an_equational_goal = function
602 | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
607 tables maxm cache depth fake_proof goalno goalty subst context
610 let active,passive,bag = tables in
611 let ppterm = ppterm context in
612 let status = (fake_proof,goalno) in
613 if flags.use_only_paramod then
615 prerr_endline ("PARAMODULATION SU: " ^
616 string_of_int goalno ^ " " ^ ppterm goalty );
617 let goal_steps, saturation_steps, timeout = max_int,max_int,flags.timeout in
619 Saturation.given_clause bag maxm status active passive
620 goal_steps saturation_steps timeout
622 | None, active, passive, maxmeta ->
623 [], (active,passive,bag), cache, maxmeta, flags
624 | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta ->
625 assert_subst_are_disjoint subst subst';
626 let subst = subst@subst' in
627 let open_goals = order_new_goals metasenv subst open_goals ppterm in
628 let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
629 [metasenv,subst,open_goals], (active,passive,bag),
630 cache, maxmeta, flags
634 prerr_endline ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
635 let res, maxmeta = Saturation.all_subsumed bag maxm status active passive in
636 assert (maxmeta >= maxm);
639 (fun subst',(_,metasenv,proof,_),open_goals ->
640 assert_subst_are_disjoint subst subst';
641 let subst = subst@subst' in
642 let open_goals = order_new_goals metasenv subst open_goals ppterm in
643 let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
644 metasenv,subst,open_goals)
646 res', (active,passive,bag), cache, maxmeta, flags
650 let active,passive,bag,cache,maxmeta,flags,goal_steps,saturation_steps,timeout =
652 tables maxm auto cache subst flags context status in
654 Saturation.given_clause bag maxmeta status active passive
655 goal_steps saturation_steps timeout
657 | None, active, passive, maxmeta ->
658 None, (active,passive,bag), cache, maxmeta, flags
659 | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta ->
660 assert_subst_are_disjoint subst subst';
661 let subst = subst@subst' in
662 let open_goals = order_new_goals metasenv subst open_goals ppterm in
663 let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
664 Some [metasenv,subst,open_goals], (active,passive,bag), cache, maxmeta, flags
669 goalty tables maxm subst fake_proof goalno depth context cand
671 let ppterm = ppterm context in
673 let subst', ((_,metasenv,_,_), open_goals), maxmeta =
674 PrimitiveTactics.apply_with_subst
675 ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
677 debug_print (lazy (" OK: " ^ ppterm cand));
678 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
679 assert (maxmeta >= maxm);
680 (*FIXME:sicuro che posso @?*)
681 assert_subst_are_disjoint subst subst';
682 let subst = subst@subst' in
683 let open_goals = order_new_goals metasenv subst open_goals ppterm in
684 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
685 Some (metasenv,subst,open_goals), tables , maxmeta
687 | ProofEngineTypes.Fail s ->
688 (*debug_print(" KO: "^Lazy.force s);*)None,tables, maxm
689 | CicUnification.Uncertain s ->
690 (*debug_print(" BECCATO: "^Lazy.force s);*)None,tables, maxm
694 tables maxm depth subst fake_proof goalno goalty metasenv context universe
697 let candidates = get_candidates universe cache goalty in
698 let tables, elems, maxm =
700 (fun (tables,elems,maxm) cand ->
703 tables maxm subst fake_proof goalno depth context cand
705 | None, tables,maxm -> tables,elems, maxm
706 | Some x, tables, maxm -> tables,x::elems, maxm)
707 (tables,[],maxm) candidates
709 let elems = sort_new_elems elems in
710 elems, tables, cache, maxm
713 (* Works if there is no dependency over proofs *)
714 let is_a_green_cut goalty =
715 CicUtil.is_meta_closed goalty
718 let prop = function (_,_,P) -> true | _ -> false;;
719 let calculate_timeout flags =
720 if flags.timeout = 0. then
721 (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
725 let is_equational_case goalty flags =
726 let ensure_equational t =
727 if is_an_equational_goal t then true
730 let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
731 raise (ProofEngineTypes.Fail (lazy msg))
734 (flags.use_paramod && is_an_equational_goal goalty) ||
735 (flags.use_only_paramod && ensure_equational goalty)
737 let cache_add_success sort cache k v =
738 if sort = P then cache_add_success cache k v else cache_remove_underinspection
742 let rec auto_main tables maxm context flags elems universe cache =
743 let flags = calculate_timeout flags in
744 let ppterm = ppterm context in
745 let irl = mk_irl context in
746 let rec aux flags tables maxm cache = function (* elems in OR *)
747 | [] -> Fail "no more steps can be done", tables, cache, maxm
749 | (metasenv,subst,[])::tl ->
750 Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
751 | (metasenv,subst,goals)::tl when
752 List.length (List.filter prop goals) > flags.maxwidth ->
754 (lazy (" FAILURE(width): " ^ string_of_int (List.length goals)));
755 aux flags tables maxm cache tl (* FAILURE (width) *)
756 | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
757 if Unix.gettimeofday() > flags.timeout then
758 Fail "timeout",tables,cache,maxm
761 let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
763 (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty));
764 debug_print (lazy (AutoCache.cache_print context cache));
765 if sort = T && tl <> [] then (* FIXME!!!! *)
767 (lazy (" FAILURE(not in prop)"));
768 aux flags tables maxm cache tl (* FAILURE (not in prop) *))
770 match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
771 | Fail s, tables, cache, maxm' ->
772 assert(maxm' >= maxm);let maxm = maxm' in
775 (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
777 if flags.dont_cache_failures then
778 cache_remove_underinspection cache goalty
779 else cache_add_failure cache goalty depth
781 aux flags tables maxm cache tl
782 | Success (metasenv,subst,others), tables, cache, maxm' ->
783 assert(maxm' >= maxm);let maxm = maxm' in
784 (* others are alternatives in OR *)
786 let goal = Cic.Meta(goalno,irl) in
787 let proof = CicMetaSubst.apply_subst subst goal in
789 (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
790 if is_a_green_cut goalty then
791 (assert_proof_is_valid proof metasenv context goalty;
792 let cache = cache_add_success sort cache goalty proof in
793 aux flags tables maxm cache ((metasenv,subst,gl)::tl))
795 (let goalty = CicMetaSubst.apply_subst subst goalty in
796 assert_proof_is_valid proof metasenv context goalty;
798 if is_a_green_cut goalty then
799 cache_add_success sort cache goalty proof
805 (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
808 aux flags tables maxm cache ((metasenv,subst,gl)::others@tl))
809 with CicUtil.Meta_not_found i when i = goalno ->
811 with CicUtil.Meta_not_found i when i = goalno ->
812 (* goalno was closed by sideeffect *)
814 (lazy ("Goal "^string_of_int goalno^" closed by sideeffect"));
815 aux flags tables maxm cache ((metasenv,subst,gl)::tl)
817 and aux_single flags tables maxm universe cache metasenv subst (goalno, depth, _) goalty cc =
818 let goalty = CicMetaSubst.apply_subst subst goalty in
819 (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
820 (* FAILURE (euristic cut) *)
821 match cache_examine cache goalty with
822 | Failed_in d when d >= depth ->
823 Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
824 tables,cache,maxm(*FAILURE(depth)*)
826 assert(List.for_all (fun (i,_) -> i <> goalno) subst);
827 let entry = goalno, (cc, t,goalty) in
828 assert_subst_are_disjoint subst [entry];
829 let subst = entry :: subst in
830 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
831 debug_print (lazy (" CACHE HIT!"));
832 Success (metasenv, subst, []), tables, cache, maxm
833 | UnderInspection -> Fail "looping",tables,cache, maxm
835 | Failed_in _ when depth > 0 -> (* we have more depth now *)
836 let cache = cache_add_underinspection cache goalty depth in
837 let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
838 let elems, tables, cache, maxm, flags =
839 if is_equational_case goalty flags then
840 let elems,tables,cache,maxm1, flags =
841 equational_case tables maxm cache
842 depth fake_proof goalno goalty subst context flags in
843 assert(maxm1 >= maxm);
845 let more_elems, tables, cache, maxm1 =
846 if flags.use_only_paramod then
847 [],tables, cache, maxm
850 tables maxm depth subst fake_proof goalno
851 goalty metasenv context universe cache in
852 assert(maxm1 >= maxm);
854 elems@more_elems, tables, cache, maxm, flags
856 let elems, tables, cache, maxm =
857 applicative_case tables maxm depth subst fake_proof goalno
858 goalty metasenv context universe cache in
859 elems, tables, cache, maxm, flags
861 aux flags tables maxm cache elems
862 | _ -> Fail "??",tables,cache,maxm
864 aux flags tables maxm cache elems
867 auto_all_solutions maxm tables universe cache context metasenv gl flags
869 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
870 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
871 let elems = [metasenv,[],goals] in
872 let rec aux tables maxm solutions cache elems flags =
873 match auto_main tables maxm context flags elems universe cache with
874 | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
875 | Success (metasenv,subst,others),tables,cache,maxm ->
876 if Unix.gettimeofday () > flags.timeout then
877 ((subst,metasenv)::solutions), cache, maxm
879 aux tables maxm ((subst,metasenv)::solutions) cache others flags
881 let rc = aux tables maxm [] cache elems flags in
883 | [],cache,maxm -> [],cache,maxm
884 | solutions,cache,maxm ->
887 (fun (subst,newmetasenv) ->
889 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
891 if opened = [] then Some subst else None)
897 (* }}} ****************** AUTO ***************)
899 let auto_all tables universe cache context metasenv gl flags =
900 let solutions, cache, _ =
901 auto_all_solutions 0 tables universe cache context metasenv gl flags
906 let auto flags metasenv tables universe cache context metasenv gl =
907 let initial_time = Unix.gettimeofday() in
908 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
909 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
910 let elems = [metasenv,[],goals] in
911 match auto_main tables 0 context flags elems universe cache with
912 | Success (metasenv,subst,_), tables,cache,_ ->
913 prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
914 Some (subst,metasenv), cache
915 | Fail s,tables,cache,maxm -> None,cache
918 let bool params name default =
920 let s = List.assoc name params in
921 if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
922 else if s = "0" || s = "false" || s = "no" || s= "off" then false
924 let msg = "Unrecognized value for parameter "^name^"\n" in
925 let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
926 raise (ProofEngineTypes.Fail (lazy msg))
927 with Not_found -> default
930 let string params name default =
931 try List.assoc name params with
932 | Not_found -> default
935 let int params name default =
936 try int_of_string (List.assoc name params) with
937 | Not_found -> default
939 raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
942 let flags_of_params params ?(for_applyS=false) () =
943 let int = int params in
944 let bool = bool params in
945 let close_more = bool "close_more" false in
946 let use_paramod = bool "use_paramod" true in
947 let use_only_paramod =
948 if for_applyS then true else bool "paramodulation" false in
949 let use_library = bool "library"
950 ((AutoTypes.default_flags()).AutoTypes.use_library) in
951 let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
952 let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
953 let timeout = int "timeout" 0 in
954 { AutoTypes.maxdepth =
955 if use_only_paramod then 2 else depth;
956 AutoTypes.maxwidth = width;
959 if for_applyS then Unix.gettimeofday () +. 30.0
963 Unix.gettimeofday() +. (float_of_int timeout);
964 AutoTypes.use_library = use_library;
965 AutoTypes.use_paramod = use_paramod;
966 AutoTypes.use_only_paramod = use_only_paramod;
967 AutoTypes.close_more = close_more;
968 AutoTypes.dont_cache_failures = false;
971 let applyS_tac ~dbd ~term ~params ~universe =
972 ProofEngineTypes.mk_tactic
975 let _, proof, gl,_,_ =
976 apply_smart ~dbd ~term ~subst:[] ~universe
977 (flags_of_params params ~for_applyS:true ()) status
981 | CicUnification.UnificationFailure msg
982 | CicTypeChecker.TypeCheckerFailure msg ->
983 raise (ProofEngineTypes.Fail msg))
988 * auto superposition target = NAME
989 * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
991 * - if table is omitted no superposition will be performed
992 * - if demod_table is omitted no demodulation will be prformed
993 * - subterms_only is passed to Indexing.superposition_right
995 * lists are coded using _ (example: H_H1_H2)
998 let eq_and_ty_of_goal = function
999 | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
1001 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1004 let rec find_in_ctx i name = function
1005 | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
1006 | Some (Cic.Name name', _)::tl when name = name' -> i
1007 | _::tl -> find_in_ctx (i+1) name tl
1010 let rec position_of i x = function
1011 | [] -> assert false
1012 | j::tl when j <> x -> position_of (i+1) x tl
1017 let superposition_tac ~target ~table ~subterms_only ~demod_table status =
1018 Saturation.reset_refs();
1019 let proof,goalno = status in
1020 let curi,metasenv,pbo,pty = proof in
1021 let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
1022 let eq_uri,tty = eq_and_ty_of_goal ty in
1023 let env = (metasenv, context, CicUniv.empty_ugraph) in
1024 let names = Utils.names_of_context context in
1025 let bag = Equality.mk_equality_bag () in
1026 let eq_index, equalities, maxm,cache =
1027 find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty
1030 let what = find_in_ctx 1 target context in
1031 List.nth equalities (position_of 0 what eq_index)
1036 let others = Str.split (Str.regexp "_") table in
1037 List.map (fun other -> find_in_ctx 1 other context) others
1040 (fun other -> List.nth equalities (position_of 0 other eq_index))
1045 let index = List.fold_left Indexing.index Indexing.empty eq_other in
1047 if table = "" then maxm,[eq_what] else
1048 Indexing.superposition_right bag
1049 ~subterms_only eq_uri maxm env index eq_what
1051 prerr_endline ("Superposition right:");
1052 prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
1053 prerr_endline ("\n table: ");
1054 List.iter (fun e -> prerr_endline (" " ^ Equality.string_of_equality e ~env)) eq_other;
1055 prerr_endline ("\n result: ");
1056 List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
1057 prerr_endline ("\n result (cut&paste): ");
1060 let t = Equality.term_of_equality eq_uri e in
1061 prerr_endline (CicPp.pp t names))
1063 prerr_endline ("\n result proofs: ");
1065 prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
1066 let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
1067 Subst.ppsubst s ^ "\n" ^
1068 CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql;
1069 if demod_table <> "" then
1072 if eql = [] then [eq_what] else eql
1075 let demod = Str.split (Str.regexp "_") demod_table in
1076 List.map (fun other -> find_in_ctx 1 other context) demod
1080 (fun demod -> List.nth equalities (position_of 0 demod eq_index))
1083 let table = List.fold_left Indexing.index Indexing.empty eq_demod in
1086 (fun (maxm,acc) e ->
1088 Indexing.demodulation_equality bag eq_uri maxm env table e
1093 let eql = List.rev eql in
1094 prerr_endline ("\n result [demod]: ");
1096 (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
1097 prerr_endline ("\n result [demod] (cut&paste): ");
1100 let t = Equality.term_of_equality eq_uri e in
1101 prerr_endline (CicPp.pp t names))
1107 let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
1108 (* argument parsing *)
1109 let string = string params in
1110 let bool = bool params in
1111 (* hacks to debug paramod *)
1112 let superposition = bool "superposition" false in
1113 let target = string "target" "" in
1114 let table = string "table" "" in
1115 let subterms_only = bool "subterms_only" false in
1116 let demod_table = string "demod_table" "" in
1117 match superposition with
1119 (* this is the ugly hack to debug paramod *)
1121 ~target ~table ~subterms_only ~demod_table (proof,goal)
1123 (* this is the real auto *)
1124 let _,metasenv,_,_ = proof in
1125 let _,context,_ = CicUtil.lookup_meta goal metasenv in
1126 let flags = flags_of_params params () in
1127 (* just for testing *)
1128 let use_library = flags.use_library in
1129 let tables,cache,newmeta =
1130 init_cache_and_tables dbd use_library universe (proof, goal) in
1131 let tables,cache,newmeta =
1132 if flags.close_more then
1134 tables newmeta context (proof, goal) auto_all_solutions universe cache
1135 else tables,cache,newmeta in
1136 let initial_time = Unix.gettimeofday() in
1137 let (_,oldmetasenv,_,_) = proof in
1138 let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
1139 match auto_main tables newmeta context flags [elem] universe cache with
1140 | Success (metasenv,subst,_), tables,cache,_ ->
1141 prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
1142 let proof,metasenv =
1143 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1144 proof goal (CicMetaSubst.apply_subst subst) metasenv
1147 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1148 ~newmetasenv:metasenv
1151 | Fail s,tables,cache,maxm ->
1152 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1155 let auto_tac ~dbd ~params ~universe =
1156 ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
1158 let eq_of_goal = function
1159 | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1161 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1165 let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
1166 let curi,metasenv,pbo,pty = proof in
1167 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1168 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1169 let initgoal = [], [], ty in
1170 let eq_uri = eq_of_goal ty in
1171 let (active,passive,bag), cache, maxm =
1172 init_cache_and_tables dbd true Universe.empty (proof,goal) in
1173 let equalities = (Saturation.list_of_passive passive) in
1174 (* we demodulate using both actives passives *)
1177 (fun tbl eq -> Indexing.index tbl eq)
1178 (snd active) equalities
1180 let changed,(newproof,newmetasenv, newty) =
1181 Indexing.demodulation_goal bag
1182 (metasenv,context,CicUniv.empty_ugraph) table initgoal
1186 let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1188 Equality.build_goal_proof bag
1189 eq_uri newproof opengoal ty [] context metasenv
1191 let extended_metasenv = (maxm,context,newty)::metasenv in
1192 let extended_status =
1193 (curi,extended_metasenv,pbo,pty),goal in
1194 let (status,newgoals) =
1195 ProofEngineTypes.apply_tactic
1196 (PrimitiveTactics.apply_tac ~term:proofterm)
1198 (status,maxm::newgoals)
1200 else (* if newty = ty then *)
1201 raise (ProofEngineTypes.Fail (lazy "no progress"))
1202 (*else ProofEngineTypes.apply_tactic
1203 (ReductionTactics.simpl_tac
1204 ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1207 let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);;