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
37 let find_library_theorems dbd proof gl =
38 let univ = MetadataQuery.universe_of_goals ~dbd proof gl in
39 let terms = List.map CicUtil.term_of_uri univ in
42 (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)))
45 let find_context_theorems context metasenv =
48 (fun (res,i) ctxentry ->
50 | Some (_,Cic.Decl t) ->
51 (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
52 | Some (_,Cic.Def (_,Some t)) ->
53 (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
54 | Some (_,Cic.Def (_,None)) ->
57 CicTypeChecker.type_of_aux'
58 metasenv context t CicUniv.empty_ugraph
65 let rec is_an_equality = function
66 | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _]
67 when (LibraryObjects.is_eq_URI uri) -> true
68 | Cic.Prod (_, _, t) -> is_an_equality t
72 let partition_equalities =
73 List.partition (fun (_,ty) -> is_an_equality ty)
76 let default_auto maxm _ cache _ _ _ _ = [],cache,maxm ;;
79 let is_unit_equation context metasenv oldnewmeta term =
80 let head, metasenv, args, newmeta =
81 ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
83 let propositional_args =
87 let _,_,mt = CicUtil.lookup_meta i metasenv in
89 CicTypeChecker.type_of_aux' metasenv context mt
93 CicReduction.are_convertible ~metasenv context
94 sort (Cic.Sort Cic.Prop) u
96 if b then Some i else None
100 if propositional_args = [] then
101 let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
102 Some (args,metasenv,newmetas,head,newmeta)
105 let retrieve_equations cache =
107 match LibraryObjects.eq_URI() with
108 | None ->assert false
109 | Some eq_uri -> eq_uri in
110 let fake= Cic.Meta(-1,[]) in
111 let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);Cic.Meta(-1,[]);
112 Cic.Meta(-2,[]); Cic.Meta(-3,[])] in
113 let candidates = get_candidates cache fake_eq in
115 (lazy ("candidates for " ^ (CicPp.ppterm fake_eq) ^ " = " ^
116 (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
117 debug_print debug_msg;
121 let proof, goalno = status in
122 let _, metasenv,_,_ = proof in
123 let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
124 let eq_uri = eq_of_goal type_of_goal in
125 let env = (metasenv, context, CicUniv.empty_ugraph) in
126 let eq_indexes, equalities, maxm, cache =
127 Equality_retrieval.find_context_equalities maxmeta bag auto context proof cache
129 prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
132 (fun e -> prerr_endline (Equality.string_of_equality ~env e))
134 prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
137 (fun e -> forward_simplify bag eq_uri env e active)
140 prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
142 (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities;
143 prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
144 bag, equalities, cache, maxm
147 let build_equality bag head args proof newmetas maxmeta =
149 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
151 if args = [] then proof else Cic.Appl (proof::args)
153 let o = !Utils.compare_terms t1 t2 in
154 let stat = (ty,t1,t2,o) in
155 (* let w = compute_equality_weight stat in *)
157 let proof = Equality.Exact p in
158 let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
159 (* to clean the local context of metas *)
160 Equality.fix_metas bag maxmeta e
164 let partition_unit_equalities context metasenv newmeta bag equations =
166 (fun (units,other,maxmeta)(t,ty) ->
167 match is_unit_equation context metasenv maxmeta ty with
168 | Some (args,metasenv,newmetas,head,newmeta') ->
169 let maxmeta,equality =
170 build_equality bag head args t newmetas newmeta' in
171 equality::units,other,maxmeta
173 units,(t,ty)::other,maxmeta)
174 ([],[],newmeta) equations
177 (Saturation.make_active [],
178 Saturation.make_passive [],
179 Equality.mk_equality_bag)
181 let init_cache_and_tables dbd use_library (proof, goal) =
182 let _, metasenv, _, _ = proof in
183 let newmeta = CicMkImplicit.new_meta metasenv [] in
184 let _,context,_ = CicUtil.lookup_meta goal metasenv in
186 match LibraryObjects.eq_URI() with
187 | None ->assert false
188 | Some eq_uri -> eq_uri in
189 let ct = find_context_theorems context metasenv in
192 find_library_theorems dbd metasenv [goal]
194 (* all equations are added to the cache *)
195 prerr_endline ("ho trovato " ^ (string_of_int (List.length lt)));
196 let cache = cache_add_list AutoCache.cache_empty context (ct@lt) in
197 let equations,others = partition_equalities (ct@lt) in
198 let bag = Equality.mk_equality_bag () in
199 let units, other_equalities, newmeta =
200 partition_unit_equalities context metasenv newmeta bag equations in
201 (* other equations are added to the cache; note that untis equalities
203 let env = (metasenv, context, CicUniv.empty_ugraph) in
205 Saturation.simplify_equalities bag eq_uri env units in *)
206 let passive = Saturation.make_passive units in
207 let no = List.length units in
208 prerr_endline ("No = " ^ (string_of_int no));
209 let active = Saturation.make_active [] in
210 let active,passive,newmeta =
211 Saturation.pump_actives context bag newmeta active passive (no+1) infinity
213 (active,passive,bag),cache,newmeta
215 let fill_hypothesis context metasenv oldnewmeta term tables cache auto fast =
216 let head, metasenv, args, newmeta =
217 ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
219 let propositional_args =
223 let _,_,mt = CicUtil.lookup_meta i metasenv in
225 CicTypeChecker.type_of_aux' metasenv context mt
229 CicReduction.are_convertible ~metasenv context
230 sort (Cic.Sort Cic.Prop) u
232 if b then Some i else None
236 let results,cache,newmeta =
237 if propositional_args = [] then
238 let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
239 [args,metasenv,newmetas,head,newmeta],cache,newmeta
242 None,metasenv,term,term (* term non e' significativo *)
246 {AutoTypes.default_flags() with
247 AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
248 maxwidth = 2;maxdepth = 2;
249 use_paramod=true;use_only_paramod=false}
251 {AutoTypes.default_flags() with
252 AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
253 maxwidth = 2;maxdepth = 4;
254 use_paramod=true;use_only_paramod=false}
256 match auto newmeta tables cache context metasenv propositional_args flags with
257 | [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
258 | substs,cache,newmeta ->
262 CicMetaSubst.apply_subst_metasenv subst metasenv
264 let head = CicMetaSubst.apply_subst subst head in
266 List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
268 let args = List.map (CicMetaSubst.apply_subst subst) args in
269 let newm = CicMkImplicit.new_meta metasenv subst in
270 args,metasenv,newmetas,head,max newm newmeta)
271 substs, cache, newmeta
273 results,cache,newmeta
275 let build_equalities auto context metasenv tables cache newmeta equations =
277 (fun (facts,cache,newmeta) (t,ty) ->
278 (* in any case we add the equation to the cache *)
279 let cache = AutoCache.cache_add_list cache context [(t,ty)] in
281 let saturated,cache,newmeta =
282 fill_hypothesis context metasenv newmeta ty tables cache auto true
284 let (active,passive,bag) = tables in
285 let eqs,bag,newmeta =
287 (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') ->
288 let maxmeta,equality =
289 build_equality bag head args t newmetas newmeta'
291 equality::acc,bag,maxmeta)
292 ([],bag,newmeta) saturated
294 (eqs@facts, cache, newmeta)
295 with FillingFailure (cache,newmeta) ->
296 (* if filling hypothesis fails we add the equation to
298 (facts,cache,newmeta)
300 ([],cache,newmeta) equations
302 let close_more tables maxmeta context status auto cache =
303 let (active,passive,bag) = tables in
304 let proof, goalno = status in
305 let _, metasenv,_,_ = proof in
306 let equations = retrieve_equations cache in
311 CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
312 (* retrieve_equations could also return flexible terms *)
313 if is_an_equality ty then Some(t,ty) else None)
315 let units, cache, maxm =
316 build_equalities auto context metasenv tables cache maxmeta eqs_and_types in
317 prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
320 (fun e -> prerr_endline (Equality.string_of_equality e))
322 prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
323 let passive = Saturation.add_to_passive units passive in
324 let no = List.length units in
325 prerr_endline ("No = " ^ (string_of_int no));
326 let active,passive,newmeta =
327 Saturation.pump_actives context bag maxm active passive (no+1) infinity
329 (active,passive,bag),cache,newmeta
331 let find_context_equalities
332 maxmeta bag context proof cache
334 prerr_endline "find_equalities";
335 let module C = Cic in
336 let module S = CicSubstitution in
337 let module T = CicTypeChecker in
338 let _,metasenv,_,_ = proof in
339 let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
340 (* if use_auto is true, we try to close the hypothesis of equational
341 statements using auto; a naif, and probably wrong approach *)
342 let rec aux cache index newmeta = function
343 | [] -> [], newmeta,cache
344 | (Some (_, C.Decl (term)))::tl ->
347 (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
348 let do_find context term =
350 | C.Prod (name, s, t) when is_an_equality t ->
353 let term = S.lift index term in
354 let saturated,cache,newmeta =
355 fill_hypothesis context metasenv newmeta term
356 empty_tables cache default_auto false
360 (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
361 let newmeta, equality =
363 bag head args (Cic.Rel index) newmetas (max newmeta newmeta')
365 equality::acc, newmeta + 1)
366 ([],newmeta) saturated
369 with FillingFailure (cache,newmeta) ->
371 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
372 when LibraryObjects.is_eq_URI uri ->
373 let term = S.lift index term in
375 build_equality bag term [] (Cic.Rel index) [] newmeta
377 [e], (newmeta+1),cache
378 | _ -> [], newmeta, cache
380 let eqs, newmeta, cache = do_find context term in
381 let rest, newmeta,cache = aux cache (index+1) newmeta tl in
382 List.map (fun x -> index,x) eqs @ rest, newmeta, cache
384 aux cache (index+1) newmeta tl
386 let il, maxm, cache =
387 aux cache 1 newmeta context
389 let indexes, equalities = List.split il in
390 indexes, equalities, maxm, cache
393 (***************** applyS *******************)
395 let new_metasenv_and_unify_and_t
396 dbd flags proof goal ?tables newmeta' metasenv' context term' ty termty
399 let (consthead,newmetasenv,arguments,_) =
400 ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
402 match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
404 let proof',oldmetasenv =
405 let (puri,metasenv,pbo,pty) = proof in
406 (puri,newmetasenv,pbo,pty),metasenv
408 let goal_for_paramod =
409 match LibraryObjects.eq_URI () with
411 Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
412 | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
414 let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
415 let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
416 let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in
417 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
419 ProofEngineTypes.apply_tactic
420 (EqualityTactics.rewrite_tac ~direction:`RightToLeft
421 ~pattern:(ProofEngineTypes.conclusion_pattern None)
422 (Cic.Meta(newmeta,irl)))
425 let goal = match goals with [g] -> g | _ -> assert false in
426 let subst, (proof'''', _), _ =
427 PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
430 let (active, passive,bag), cache, maxmeta =
431 init_cache_and_tables dbd true (proof'''',newmeta)
433 Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
434 max_int max_int flags.timeout
437 raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
438 | Some (_,proof''''',_), active,passive,_ ->
440 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
441 ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive
444 let rec count_prods context ty =
445 match CicReduction.whd context ty with
446 Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
449 let apply_smart ~dbd ~term ~subst ?tables flags (proof, goal) =
450 let module T = CicTypeChecker in
451 let module R = CicReduction in
452 let module C = Cic in
453 let (_,metasenv,_,_) = proof in
454 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
455 let newmeta = CicMkImplicit.new_meta metasenv subst in
456 let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
458 C.Var (uri,exp_named_subst) ->
459 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
460 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
463 exp_named_subst_diff,newmeta',newmetasenvfragment,
464 C.Var (uri,exp_named_subst')
465 | C.Const (uri,exp_named_subst) ->
466 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
467 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
470 exp_named_subst_diff,newmeta',newmetasenvfragment,
471 C.Const (uri,exp_named_subst')
472 | C.MutInd (uri,tyno,exp_named_subst) ->
473 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
474 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
477 exp_named_subst_diff,newmeta',newmetasenvfragment,
478 C.MutInd (uri,tyno,exp_named_subst')
479 | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
480 let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
481 PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
484 exp_named_subst_diff,newmeta',newmetasenvfragment,
485 C.MutConstruct (uri,tyno,consno,exp_named_subst')
486 | _ -> [],newmeta,[],term
488 let metasenv' = metasenv@newmetasenvfragment in
490 CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
492 let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
493 let goal_arity = count_prods context ty in
494 let subst, proof, gl, active, passive =
495 new_metasenv_and_unify_and_t dbd flags proof goal ?tables
496 newmeta' metasenv' context term' ty termty goal_arity
498 subst, proof, gl, active, passive
501 (****************** AUTO ********************)
503 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
504 let ugraph = CicUniv.empty_ugraph;;
505 let typeof = CicTypeChecker.type_of_aux';;
507 let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
510 let is_in_prop context subst metasenv ty =
511 let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
512 fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
514 let assert_proof_is_valid proof metasenv context goalty =
515 let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
516 let b,_ = CicReduction.are_convertible context ty goalty u in
520 List.map (function None -> None | Some (x,_) -> Some x) context
522 prerr_endline ("PROOF:" ^ CicPp.pp proof names);
523 prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
524 prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
525 prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
529 let assert_subst_are_disjoint subst subst' =
531 (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
535 List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2)
538 let split_goals_in_prop metasenv subst gl =
541 let _,context,ty = CicUtil.lookup_meta g metasenv in
543 let sort,u = typeof ~subst metasenv context ty ugraph in
545 CicReduction.are_convertible
546 ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
549 | CicTypeChecker.AssertFailure s
550 | CicTypeChecker.TypeCheckerFailure s ->
552 (lazy (ppterm context (CicMetaSubst.apply_subst subst ty)));
555 (* FIXME... they should type! *)
559 let split_goals_with_metas metasenv subst gl =
562 let _,context,ty = CicUtil.lookup_meta g metasenv in
563 let ty = CicMetaSubst.apply_subst subst ty in
564 CicUtil.is_meta_closed ty)
568 let order_new_goals metasenv subst open_goals ppterm =
569 let prop,rest = split_goals_in_prop metasenv subst open_goals in
570 let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
572 (List.map (fun x -> x,P) (closed_prop @ open_prop))
574 (List.map (fun x -> x,T) rest)
579 let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals
581 debug_print (lazy (" OPEN: "^
585 | (i,t,P) -> string_of_int i (* ":"^ppterm t^ "Prop" *)
586 | (i,t,T) -> string_of_int i ) (* ":"^ppterm t^ "Type")*)
591 let is_an_equational_goal = function
592 | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
597 tables maxm cache depth fake_proof goalno goalty subst context
600 let active,passive,bag = tables in
601 let ppterm = ppterm context in
602 let status = (fake_proof,goalno) in
603 if flags.use_only_paramod then
605 prerr_endline ("PARAMODULATION SU: " ^
606 string_of_int goalno ^ " " ^ ppterm goalty );
607 let goal_steps, saturation_steps, timeout = max_int,max_int,flags.timeout in
609 Saturation.given_clause bag maxm status active passive
610 goal_steps saturation_steps timeout
612 | None, active, passive, maxmeta ->
613 [], (active,passive,bag), cache, maxmeta, flags
614 | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta ->
615 assert_subst_are_disjoint subst subst';
616 let subst = subst@subst' in
617 let open_goals = order_new_goals metasenv subst open_goals ppterm in
618 let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
619 [metasenv,subst,open_goals], (active,passive,bag),
620 cache, maxmeta, flags
624 prerr_endline ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
625 let res, maxmeta = Saturation.all_subsumed bag maxm status active passive in
626 assert (maxmeta >= maxm);
629 (fun subst',(_,metasenv,proof,_),open_goals ->
630 assert_subst_are_disjoint subst subst';
631 let subst = subst@subst' in
632 let open_goals = order_new_goals metasenv subst open_goals ppterm in
633 let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
634 metasenv,subst,open_goals)
636 res', (active,passive,bag), cache, maxmeta, flags
640 let active,passive,bag,cache,maxmeta,flags,goal_steps,saturation_steps,timeout =
642 tables maxm auto cache subst flags context status in
644 Saturation.given_clause bag maxmeta status active passive
645 goal_steps saturation_steps timeout
647 | None, active, passive, maxmeta ->
648 None, (active,passive,bag), cache, maxmeta, flags
649 | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta ->
650 assert_subst_are_disjoint subst subst';
651 let subst = subst@subst' in
652 let open_goals = order_new_goals metasenv subst open_goals ppterm in
653 let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
654 Some [metasenv,subst,open_goals], (active,passive,bag), cache, maxmeta, flags
659 goalty tables maxm subst fake_proof goalno depth context cand
661 let ppterm = ppterm context in
663 let subst', ((_,metasenv,_,_), open_goals), maxmeta =
664 PrimitiveTactics.apply_with_subst
665 ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
667 debug_print (lazy (" OK: " ^ ppterm cand));
668 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
669 assert (maxmeta >= maxm);
670 (*FIXME:sicuro che posso @?*)
671 assert_subst_are_disjoint subst subst';
672 let subst = subst@subst' in
673 let open_goals = order_new_goals metasenv subst open_goals ppterm in
674 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
675 Some (metasenv,subst,open_goals), tables , maxmeta
676 with ProofEngineTypes.Fail s ->
677 (*debug_print(" KO: "^Lazy.force s);*)None,tables, maxm
681 tables maxm depth subst fake_proof goalno goalty metasenv context cache
683 let candidates = get_candidates cache goalty in
685 (lazy ("candidates for " ^ (CicPp.ppterm goalty) ^ " = " ^
686 (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
687 debug_print debug_msg;
688 let tables, elems, maxm =
690 (fun (tables,elems,maxm) cand ->
693 tables maxm subst fake_proof goalno depth context cand
695 | None, tables,maxm -> tables,elems, maxm
696 | Some x, tables, maxm -> tables,x::elems, maxm)
697 (tables,[],maxm) candidates
699 let elems = sort_new_elems elems in
700 elems, tables, cache, maxm
703 (* Works if there is no dependency over proofs *)
704 let is_a_green_cut goalty =
705 CicUtil.is_meta_closed goalty
708 let prop = function (_,_,P) -> true | _ -> false;;
709 let calculate_timeout flags =
710 if flags.timeout = 0. then
711 (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
715 let is_equational_case goalty flags =
716 let ensure_equational t =
717 if is_an_equational_goal t then true
720 let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
721 raise (ProofEngineTypes.Fail (lazy msg))
724 (flags.use_paramod && is_an_equational_goal goalty) ||
725 (flags.use_only_paramod && ensure_equational goalty)
727 let cache_add_success sort cache k v =
728 if sort = P then cache_add_success cache k v else cache_remove_underinspection
732 let rec auto_main tables maxm context flags elems cache =
733 let flags = calculate_timeout flags in
734 let ppterm = ppterm context in
735 let irl = mk_irl context in
736 let rec aux flags tables maxm cache = function (* elems in OR *)
737 | [] -> Fail "no more steps can be done", tables, cache, maxm
739 | (metasenv,subst,[])::tl ->
740 Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
741 | (metasenv,subst,goals)::tl when
742 List.length (List.filter prop goals) > flags.maxwidth ->
744 (lazy (" FAILURE(width): " ^ string_of_int (List.length goals)));
745 aux flags tables maxm cache tl (* FAILURE (width) *)
746 | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
747 if Unix.gettimeofday() > flags.timeout then
748 Fail "timeout",tables,cache,maxm
751 let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
753 (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty));
754 debug_print (lazy (AutoCache.cache_print context cache));
755 if sort = T && tl <> [] then (* FIXME!!!! *)
757 (lazy (" FAILURE(not in prop)"));
758 aux flags tables maxm cache tl (* FAILURE (not in prop) *))
760 match aux_single flags tables maxm cache metasenv subst elem goalty cc with
761 | Fail s, tables, cache, maxm' ->
762 assert(maxm' >= maxm);let maxm = maxm' in
765 (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
767 if flags.dont_cache_failures then
768 cache_remove_underinspection cache goalty
769 else cache_add_failure cache goalty depth
771 aux flags tables maxm cache tl
772 | Success (metasenv,subst,others), tables, cache, maxm' ->
773 assert(maxm' >= maxm);let maxm = maxm' in
774 (* others are alternatives in OR *)
776 let goal = Cic.Meta(goalno,irl) in
777 let proof = CicMetaSubst.apply_subst subst goal in
779 (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
780 if is_a_green_cut goalty then
781 (assert_proof_is_valid proof metasenv context goalty;
782 let cache = cache_add_success sort cache goalty proof in
783 aux flags tables maxm cache ((metasenv,subst,gl)::tl))
785 (let goalty = CicMetaSubst.apply_subst subst goalty in
786 assert_proof_is_valid proof metasenv context goalty;
788 if is_a_green_cut goalty then
789 cache_add_success sort cache goalty proof
795 (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
798 aux flags tables maxm cache ((metasenv,subst,gl)::others@tl))
799 with CicUtil.Meta_not_found i when i = goalno ->
801 with CicUtil.Meta_not_found i when i = goalno ->
802 (* goalno was closed by sideeffect *)
804 (lazy ("Goal "^string_of_int goalno^" closed by sideeffect"));
805 aux flags tables maxm cache ((metasenv,subst,gl)::tl)
807 and aux_single flags tables maxm cache metasenv subst (goalno, depth, _) goalty cc =
808 let goalty = CicMetaSubst.apply_subst subst goalty in
809 (* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
810 (* FAILURE (euristic cut) *)
811 prerr_endline ("DEPTH = +++++++= "^ (string_of_int depth));
812 match cache_examine cache goalty with
813 | Failed_in d when d >= depth ->
814 Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
815 tables,cache,maxm(*FAILURE(depth)*)
817 assert(List.for_all (fun (i,_) -> i <> goalno) subst);
818 let entry = goalno, (cc, t,goalty) in
819 assert_subst_are_disjoint subst [entry];
820 let subst = entry :: subst in
821 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
822 debug_print (lazy (" CACHE HIT!"));
823 Success (metasenv, subst, []), tables, cache, maxm
824 | UnderInspection -> Fail "looping",tables,cache, maxm
826 | Failed_in _ when depth > 0 -> (* we have more depth now *)
827 let cache = cache_add_underinspection cache goalty depth in
828 let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
829 let elems, tables, cache, maxm, flags =
830 if is_equational_case goalty flags then
831 let elems,tables,cache,maxm1, flags =
832 equational_case tables maxm cache
833 depth fake_proof goalno goalty subst context flags in
834 assert(maxm1 >= maxm);
836 let more_elems, tables, cache, maxm1 =
837 if flags.use_only_paramod then
838 [],tables, cache, maxm
841 tables maxm depth subst fake_proof goalno
842 goalty metasenv context cache in
843 assert(maxm1 >= maxm);
845 elems@more_elems, tables, cache, maxm, flags
847 let elems, tables, cache, maxm =
848 applicative_case tables maxm depth subst fake_proof goalno
849 goalty metasenv context cache in
850 elems, tables, cache, maxm, flags
852 aux flags tables maxm cache elems
853 | _ -> Fail "??",tables,cache,maxm
855 aux flags tables maxm cache elems
858 auto_all_solutions maxm tables cache context metasenv gl flags
860 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
861 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
862 let elems = [metasenv,[],goals] in
863 let rec aux tables maxm solutions cache elems flags =
864 match auto_main tables maxm context flags elems cache with
865 | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
866 | Success (metasenv,subst,others),tables,cache,maxm ->
867 if Unix.gettimeofday () > flags.timeout then
868 ((subst,metasenv)::solutions), cache, maxm
870 aux tables maxm ((subst,metasenv)::solutions) cache others flags
872 let rc = aux tables maxm [] cache elems flags in
874 | [],cache,maxm -> [],cache,maxm
875 | solutions,cache,maxm ->
878 (fun (subst,newmetasenv) ->
880 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
882 if opened = [] then Some subst else None)
888 (* }}} ****************** AUTO ***************)
890 let auto_all tables cache context metasenv gl flags =
891 let solutions, cache, _ =
892 auto_all_solutions 0 tables cache context metasenv gl flags
897 let auto flags metasenv tables cache context metasenv gl =
898 let initial_time = Unix.gettimeofday() in
899 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
900 let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
901 let elems = [metasenv,[],goals] in
902 match auto_main tables 0 context flags elems cache with
903 | Success (metasenv,subst,_), tables,cache,_ ->
904 prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
905 Some (subst,metasenv), cache
906 | Fail s,tables,cache,maxm -> None,cache
909 let bool params name default =
911 let s = List.assoc name params in
912 if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
913 else if s = "0" || s = "false" || s = "no" || s= "off" then false
915 let msg = "Unrecognized value for parameter "^name^"\n" in
916 let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
917 raise (ProofEngineTypes.Fail (lazy msg))
918 with Not_found -> default
921 let string params name default =
922 try List.assoc name params with
923 | Not_found -> default
926 let int params name default =
927 try int_of_string (List.assoc name params) with
928 | Not_found -> default
930 raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
933 let flags_of_params params ?(for_applyS=false) () =
934 let int = int params in
935 let bool = bool params in
936 let use_paramod = bool "use_paramod" true in
937 let use_only_paramod =
938 if for_applyS then true else bool "paramodulation" false in
939 let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
940 let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
941 let timeout = int "timeout" 0 in
942 { AutoTypes.maxdepth =
943 if use_only_paramod then 2 else depth;
944 AutoTypes.maxwidth = width;
947 if for_applyS then Unix.gettimeofday () +. 30.0
951 Unix.gettimeofday() +. (float_of_int timeout);
952 AutoTypes.use_paramod = use_paramod;
953 AutoTypes.use_only_paramod = use_only_paramod;
954 AutoTypes.dont_cache_failures = false;
957 let applyS_tac ~dbd ~term ~params =
958 ProofEngineTypes.mk_tactic
961 let _, proof, gl,_,_ =
962 apply_smart ~dbd ~term ~subst:[]
963 (flags_of_params params ~for_applyS:true ()) status
967 | CicUnification.UnificationFailure msg
968 | CicTypeChecker.TypeCheckerFailure msg ->
969 raise (ProofEngineTypes.Fail msg))
974 * auto superposition target = NAME
975 * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
977 * - if table is omitted no superposition will be performed
978 * - if demod_table is omitted no demodulation will be prformed
979 * - subterms_only is passed to Indexing.superposition_right
981 * lists are coded using _ (example: H_H1_H2)
984 let eq_and_ty_of_goal = function
985 | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
987 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
990 let rec find_in_ctx i name = function
991 | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
992 | Some (Cic.Name name', _)::tl when name = name' -> i
993 | _::tl -> find_in_ctx (i+1) name tl
996 let rec position_of i x = function
998 | j::tl when j <> x -> position_of (i+1) x tl
1002 let superposition_tac ~target ~table ~subterms_only ~demod_table status =
1003 Saturation.reset_refs();
1004 let proof,goalno = status in
1005 let curi,metasenv,pbo,pty = proof in
1006 let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
1007 let eq_uri,tty = eq_and_ty_of_goal ty in
1008 let env = (metasenv, context, CicUniv.empty_ugraph) in
1009 let names = Utils.names_of_context context in
1010 let bag = Equality.mk_equality_bag () in
1011 let eq_index, equalities, maxm,cache =
1012 find_context_equalities 0 bag context proof AutoCache.cache_empty
1015 let what = find_in_ctx 1 target context in
1016 List.nth equalities (position_of 0 what eq_index)
1021 let others = Str.split (Str.regexp "_") table in
1022 List.map (fun other -> find_in_ctx 1 other context) others
1025 (fun other -> List.nth equalities (position_of 0 other eq_index))
1030 let index = List.fold_left Indexing.index Indexing.empty eq_other in
1032 if table = "" then maxm,[eq_what] else
1033 Indexing.superposition_right bag
1034 ~subterms_only eq_uri maxm env index eq_what
1036 prerr_endline ("Superposition right:");
1037 prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
1038 prerr_endline ("\n table: ");
1039 List.iter (fun e -> prerr_endline (" " ^ Equality.string_of_equality e ~env)) eq_other;
1040 prerr_endline ("\n result: ");
1041 List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
1042 prerr_endline ("\n result (cut&paste): ");
1045 let t = Equality.term_of_equality eq_uri e in
1046 prerr_endline (CicPp.pp t names))
1048 prerr_endline ("\n result proofs: ");
1050 prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
1051 let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
1052 Subst.ppsubst s ^ "\n" ^
1053 CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql;
1054 if demod_table <> "" then
1057 if eql = [] then [eq_what] else eql
1060 let demod = Str.split (Str.regexp "_") demod_table in
1061 List.map (fun other -> find_in_ctx 1 other context) demod
1065 (fun demod -> List.nth equalities (position_of 0 demod eq_index))
1068 let table = List.fold_left Indexing.index Indexing.empty eq_demod in
1071 (fun (maxm,acc) e ->
1073 Indexing.demodulation_equality bag eq_uri maxm env table e
1078 let eql = List.rev eql in
1079 prerr_endline ("\n result [demod]: ");
1081 (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
1082 prerr_endline ("\n result [demod] (cut&paste): ");
1085 let t = Equality.term_of_equality eq_uri e in
1086 prerr_endline (CicPp.pp t names))
1093 let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
1094 (* argument parsing *)
1095 let string = string params in
1096 let bool = bool params in
1097 (* hacks to debug paramod *)
1098 let superposition = bool "superposition" false in
1099 let target = string "target" "" in
1100 let table = string "table" "" in
1101 let subterms_only = bool "subterms_only" false in
1102 let demod_table = string "demod_table" "" in
1103 match superposition with
1105 (* this is the ugly hack to debug paramod *)
1107 ~target ~table ~subterms_only ~demod_table (proof,goal)
1109 (* this is the real auto *)
1110 let _,metasenv,_,_ = proof in
1111 let _,context,_ = CicUtil.lookup_meta goal metasenv in
1112 let flags = flags_of_params params () in
1113 (* just for testing *)
1114 let use_library = not flags.use_only_paramod in
1115 let tables,cache,newmeta =
1116 init_cache_and_tables dbd use_library (proof, goal) in
1117 let tables,cache,newmeta =
1118 close_more tables newmeta context (proof, goal) auto_all_solutions cache in
1119 let initial_time = Unix.gettimeofday() in
1120 let (_,oldmetasenv,_,_) = proof in
1121 let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
1122 match auto_main tables newmeta context flags [elem] cache with
1123 | Success (metasenv,subst,_), tables,cache,_ ->
1124 prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
1125 let proof,metasenv =
1126 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1127 proof goal (CicMetaSubst.apply_subst subst) metasenv
1130 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1131 ~newmetasenv:metasenv
1134 | Fail s,tables,cache,maxm ->
1135 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1138 let auto_tac ~dbd ~params = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd);;
1140 let eq_of_goal = function
1141 | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1143 | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1147 let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
1148 let curi,metasenv,pbo,pty = proof in
1149 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1150 let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1151 let initgoal = [], [], ty in
1152 let eq_uri = eq_of_goal ty in
1153 let (active,passive,bag), cache, maxm =
1154 init_cache_and_tables dbd true (proof,goal) in
1155 let equalities = (Saturation.list_of_passive passive) in
1156 (* we demodulate using both actives passives *)
1159 (fun tbl eq -> Indexing.index tbl eq)
1160 (snd active) equalities
1162 let changed,(newproof,newmetasenv, newty) =
1163 Indexing.demodulation_goal bag
1164 (metasenv,context,CicUniv.empty_ugraph) table initgoal
1168 let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1170 Equality.build_goal_proof bag
1171 eq_uri newproof opengoal ty [] context metasenv
1173 let extended_metasenv = (maxm,context,newty)::metasenv in
1174 let extended_status =
1175 (curi,extended_metasenv,pbo,pty),goal in
1176 let (status,newgoals) =
1177 ProofEngineTypes.apply_tactic
1178 (PrimitiveTactics.apply_tac ~term:proofterm)
1180 (status,maxm::newgoals)
1182 else (* if newty = ty then *)
1183 raise (ProofEngineTypes.Fail (lazy "no progress"))
1184 (*else ProofEngineTypes.apply_tactic
1185 (ReductionTactics.simpl_tac
1186 ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1189 let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);;