open AutoTypes;;
open AutoCache;;
-let debug = false;;
+let debug = true;;
let debug_print s =
- if debug then () else prerr_endline (Lazy.force s);;
+ if debug then prerr_endline (Lazy.force s);;
(* functions for retrieving theorems *)
let is_unit_equation context metasenv oldnewmeta term =
let head, metasenv, args, newmeta =
- ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
+ TermUtil.saturate_term oldnewmeta metasenv context term 0
in
let propositional_args =
HExtlib.filter_map
let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
(* the local cache in initially empty *)
let cache = AutoCache.cache_empty in
- let _, metasenv, _, _ = proof in
+ let _, metasenv, _, _, _ = proof in
let signature = MetadataQuery.signature_of metasenv goal in
let newmeta = CicMkImplicit.new_meta metasenv [] in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast =
let head, metasenv, args, newmeta =
- ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
+ TermUtil.saturate_term oldnewmeta metasenv context term 0
in
let propositional_args =
HExtlib.filter_map
let close_more tables maxmeta context status auto universe cache =
let (active,passive,bag) = tables in
let proof, goalno = status in
- let _, metasenv,_,_ = proof in
+ let _, metasenv,_,_, _ = proof in
let signature = MetadataQuery.signature_of metasenv goalno in
let equations = retrieve_equations signature universe cache context in
let eqs_and_types =
let module C = Cic in
let module S = CicSubstitution in
let module T = CicTypeChecker in
- let _,metasenv,_,_ = proof in
+ let _,metasenv,_,_, _ = proof in
let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
(* if use_auto is true, we try to close the hypothesis of equational
statements using auto; a naif, and probably wrong approach *)
context term' ty termty goal_arity
=
let (consthead,newmetasenv,arguments,_) =
- ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
+ TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
let term'' =
match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
in
let proof',oldmetasenv =
- let (puri,metasenv,pbo,pty) = proof in
- (puri,newmetasenv,pbo,pty),metasenv
+ let (puri,metasenv,pbo,pty, attrs) = proof in
+ (puri,newmetasenv,pbo,pty, attrs),metasenv
in
let goal_for_paramod =
match LibraryObjects.eq_URI () with
in
let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
- let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in
+ let proof'' = let uri,_,p,ty, attrs = proof' in uri,metasenv_for_paramod,p,ty, attrs in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let proof''',goals =
ProofEngineTypes.apply_tactic
(EqualityTactics.rewrite_tac ~direction:`RightToLeft
~pattern:(ProofEngineTypes.conclusion_pattern None)
- (Cic.Meta(newmeta,irl)))
+ (Cic.Meta(newmeta,irl)) [])
(proof'',goal)
in
let goal = match goals with [g] -> g | _ -> assert false in
| Some (_,proof''''',_), active,passive,_ ->
subst,proof''''',
ProofEngineHelpers.compare_metasenvs ~oldmetasenv
- ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive
+ ~newmetasenv:(let _,m,_,_, _ = proof''''' in m), active, passive
;;
let rec count_prods context ty =
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
- let (_,metasenv,_,_) = proof in
+ let (_,metasenv,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta = CicMkImplicit.new_meta metasenv subst in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
with
| None, active, passive, maxmeta ->
[], (active,passive,bag), cache, maxmeta, flags
- | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta ->
+ | Some(subst',(_,metasenv,proof,_, _),open_goals),active,passive,maxmeta ->
assert_subst_are_disjoint subst subst';
let subst = subst@subst' in
let open_goals = order_new_goals metasenv subst open_goals ppterm in
assert (maxmeta >= maxm);
let res' =
List.map
- (fun subst',(_,metasenv,proof,_),open_goals ->
+ (fun subst',(_,metasenv,proof,_, _),open_goals ->
assert_subst_are_disjoint subst subst';
let subst = subst@subst' in
let open_goals = order_new_goals metasenv subst open_goals ppterm in
=
let ppterm = ppterm context in
try
- let subst', ((_,metasenv,_,_), open_goals), maxmeta =
+ let subst', ((_,metasenv,_,_, _), open_goals), maxmeta =
PrimitiveTactics.apply_with_subst
~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
in
debug_print (lazy (" OK: " ^ ppterm cand));
let metasenv = CicRefine.pack_coercion_metasenv metasenv in
- assert_subst_are_disjoint subst subst';
- let subst = subst@subst' in
+ (* assert_subst_are_disjoint subst subst'; *)
+ let subst = subst' in
let open_goals = order_new_goals metasenv subst open_goals ppterm in
let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
Some (metasenv,subst,open_goals), tables , maxmeta
CicUtil.is_meta_closed goalty
;;
-let prop = function (_,_,P) -> true | _ -> false;;
+let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
+
let calculate_timeout flags =
if flags.timeout = 0. then
(prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
try
let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
debug_print
- (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty));
+ (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty ^
+ "with depth"^string_of_int depth));
debug_print (lazy (AutoCache.cache_print context cache));
- if sort = T && tl <> [] then (* FIXME!!!! *)
+ if sort = T (* && tl <> []*) then
+ aux flags tables maxm cache ((metasenv,subst,gl)::tl)
+ (* Success (metasenv,subst,tl), tables, cache,maxm *)
+ (*
(debug_print
(lazy (" FAILURE(not in prop)"));
- aux flags tables maxm cache tl (* FAILURE (not in prop) *))
+ aux flags tables maxm cache tl (* FAILURE (not in prop) *)) *)
else
match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
| Fail s, tables, cache, maxm' ->
debug_print
(lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
if is_a_green_cut goalty then
- (assert_proof_is_valid proof metasenv context goalty;
+ (* assert_proof_is_valid proof metasenv context goalty; *)
let cache = cache_add_success sort cache goalty proof in
- aux flags tables maxm cache ((metasenv,subst,gl)::tl))
+ aux flags tables maxm cache ((metasenv,subst,gl)::tl)
else
(let goalty = CicMetaSubst.apply_subst subst goalty in
- assert_proof_is_valid proof metasenv context goalty;
+ (* assert_proof_is_valid proof metasenv context goalty; *)
let cache =
if is_a_green_cut goalty then
cache_add_success sort cache goalty proof
aux flags tables maxm cache ((metasenv,subst,gl)::tl)
and aux_single flags tables maxm universe cache metasenv subst (goalno, depth, _) goalty cc =
+ (* let flags = if depth < 10 then {flags with maxwidth=3} else flags in *)
let goalty = CicMetaSubst.apply_subst subst goalty in
(* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
(* FAILURE (euristic cut) *)
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
debug_print (lazy (" CACHE HIT!"));
Success (metasenv, subst, []), tables, cache, maxm
- | UnderInspection -> Fail "looping",tables,cache, maxm
+ | UnderInspection ->
+ (* assert (not (is_a_green_cut goalty)); *)
+ Fail "looping",tables,cache, maxm
| Notfound
| Failed_in _ when depth > 0 -> (* we have more depth now *)
let cache = cache_add_underinspection cache goalty depth in
- let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
+ let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty, [] in (* FG: attrs *)
let elems, tables, cache, maxm, flags =
if is_equational_case goalty flags then
let elems,tables,cache,maxm1, flags =
elems, tables, cache, maxm, flags
in
aux flags tables maxm cache elems
- | _ -> Fail "??",tables,cache,maxm
+ | _ -> Fail "depth = 0",tables,cache,maxm
in
aux flags tables maxm cache elems
let superposition_tac ~target ~table ~subterms_only ~demod_table status =
Saturation.reset_refs();
let proof,goalno = status in
- let curi,metasenv,pbo,pty = proof in
+ let curi,metasenv,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
let eq_uri,tty = eq_and_ty_of_goal ty in
let env = (metasenv, context, CicUniv.empty_ugraph) in
~target ~table ~subterms_only ~demod_table (proof,goal)
| false ->
(* this is the real auto *)
- let _,metasenv,_,_ = proof in
+ let _,metasenv,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let flags = flags_of_params params () in
(* just for testing *)
tables newmeta context (proof, goal) auto_all_solutions universe cache
else tables,cache,newmeta in
let initial_time = Unix.gettimeofday() in
- let (_,oldmetasenv,_,_) = proof in
+ let (_,oldmetasenv,_,_, _) = proof in
let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
match auto_main tables newmeta context flags [elem] universe cache with
| Success (metasenv,subst,_), tables,cache,_ ->
;;
(* DEMODULATE *)
-let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
- let curi,metasenv,pbo,pty = proof in
+let demodulate_tac ~dbd ~universe (proof,goal)=
+ let curi,metasenv,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let initgoal = [], [], ty in
let eq_uri = eq_of_goal ty in
let (active,passive,bag), cache, maxm =
- init_cache_and_tables dbd true true Universe.empty (proof,goal) in
+ init_cache_and_tables dbd false true universe (proof,goal) in
let equalities = (Saturation.list_of_passive passive) in
(* we demodulate using both actives passives *)
let table =
in
let extended_metasenv = (maxm,context,newty)::metasenv in
let extended_status =
- (curi,extended_metasenv,pbo,pty),goal in
+ (curi,extended_metasenv,pbo,pty, attrs),goal in
let (status,newgoals) =
ProofEngineTypes.apply_tactic
(PrimitiveTactics.apply_tac ~term:proofterm)
~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
;;
-let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);;
+let demodulate_tac ~dbd ~universe =
+ ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
projects / helm.git / blobdiff