*)
open AutoTypes;;
+open AutoCache;;
-let debug_print s = ();;(*prerr_endline s;;*)
+let debug_print s = () (* prerr_endline s;; *)
+
+(* {{{ *********** local given_clause wrapper ***********)
+
+let given_clause dbd ?tables maxm auto cache subst flags smart_flag status =
+ let active,passive,bag,cache,maxmeta,goal_steps,saturation_steps,timeout =
+ match tables with
+ | None ->
+ (* first time, do a huge saturation *)
+ let bag, equalities, cache, maxmeta =
+ Saturation.find_equalities dbd status smart_flag auto cache
+ in
+ let passive = Saturation.make_passive equalities in
+ let active = Saturation.make_active [] in
+ let goal_steps, saturation_steps, timeout =
+ if flags.use_only_paramod then max_int,max_int,flags.timeout
+ else 82, 82, infinity
+ in
+ let maxm = max maxm maxmeta in
+ active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
+ | Some (active,passive,bag,oldcache) ->
+ (* saturate a bit more if cache cahnged *)
+ let bag, equalities, cache, maxm =
+ if cache_size oldcache <> cache_size cache then
+ Saturation.close_more
+ bag active maxm status smart_flag auto cache
+ else
+ bag, [], cache, maxm
+ in
+ let minsteps = List.length equalities in
+ let passive = Saturation.add_to_passive equalities passive in
+ let goal_steps, saturation_steps, timeout =
+ if flags.use_only_paramod then max_int,max_int,flags.timeout
+ else max 50 minsteps, minsteps, infinity
+ in
+ active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
+ in
+ let res,actives,passives,maxmeta =
+ Saturation.given_clause bag maxmeta status active passive
+ goal_steps saturation_steps timeout
+ in
+ res,actives,passives,bag,cache,maxmeta
+;;
+
+(* }}} ****************************************************************)
+
+(* {{{ **************** applyS *******************)
+
+let new_metasenv_and_unify_and_t
+ dbd flags proof goal ?tables newmeta' metasenv' context term' ty termty
+ goal_arity
+=
+ let (consthead,newmetasenv,arguments,_) =
+ ProofEngineHelpers.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
+ in
+ let goal_for_paramod =
+ match LibraryObjects.eq_URI () with
+ | Some uri ->
+ Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
+ | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
+ 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 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)))
+ (proof'',goal)
+ in
+ let goal = match goals with [g] -> g | _ -> assert false in
+ let subst, (proof'''', _), _ =
+ PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
+ in
+ match
+ let cache = cache_empty in
+ given_clause dbd ?tables 0 None cache [] flags true (proof'''',newmeta)
+ with
+ | None, active, passive, bag,_,_ ->
+ raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
+ | Some (_,proof''''',_), active, passive,bag,_,_ ->
+ subst,proof''''',
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+ ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive
+;;
+
+let rec count_prods context ty =
+ match CicReduction.whd context ty with
+ Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
+ | _ -> 0
+
+let apply_smart ~dbd ~term ~subst ?tables flags (proof, goal) =
+ let module T = CicTypeChecker in
+ let module R = CicReduction in
+ let module C = Cic 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' =
+ match term with
+ C.Var (uri,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.Var (uri,exp_named_subst')
+ | C.Const (uri,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.MutInd (uri,tyno,exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.MutConstruct (uri,tyno,consno,exp_named_subst')
+ | _ -> [],newmeta,[],term
+ in
+ let metasenv' = metasenv@newmetasenvfragment in
+ let termty,_ =
+ CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
+ in
+ let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
+ let goal_arity = count_prods context ty in
+ let subst, proof, gl, active, passive =
+ new_metasenv_and_unify_and_t dbd flags proof goal ?tables
+ newmeta' metasenv' context term' ty termty goal_arity
+ in
+ subst, proof, gl, active, passive
+;;
+
+(* }}} **************** applyS **************)
+
+(* {{{ ***************** AUTO ********************)
let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
let ugraph = CicUniv.empty_ugraph;;
let b,_ = CicReduction.are_convertible context ty goalty u in
if not b then
begin
- prerr_endline (CicPp.ppterm proof);
- prerr_endline (CicPp.ppterm ty);
- prerr_endline (CicPp.ppterm goalty);
+ let names =
+ List.map (function None -> None | Some (x,_) -> Some x) context
+ in
+ prerr_endline ("PROOF:" ^ CicPp.pp proof names);
+ prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
+ prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
+ prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
end;
assert b
;;
open_goals
;;
-let try_candidate subst fake_proof goalno depth context cand =
+let is_an_equational_goal = function
+ | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
+ | _ -> false
+;;
+
+let equational_case
+ dbd tables maxm auto cache depth fake_proof goalno goalty subst context
+ flags
+=
+ let ppterm = ppterm context in
+ prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
+(*
+ prerr_endline "<CACHE>";
+ prerr_endline (cache_print context cache);
+ prerr_endline "</CACHE>";
+*)
+ match
+ given_clause dbd ?tables maxm auto cache subst flags false (fake_proof,goalno)
+ with
+ | None, active,passive, bag, cache, maxmeta ->
+ let tables = Some (active,passive,bag,cache) in
+ None, tables, cache, maxmeta
+ | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,bag,cache,maxmeta ->
+ let tables = Some (active,passive,bag,cache) in
+ assert_subst_are_disjoint subst subst';
+ let subst = 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, cache, maxmeta
+;;
+
+let try_candidate
+ goalty dbd tables maxm subst fake_proof goalno depth context cand
+=
let ppterm = ppterm context in
try
- debug_print (" PROVO: " ^ ppterm cand);
- let subst', ((_,metasenv,_,_), open_goals) =
- PrimitiveTactics.apply_with_subst ~term:cand ~subst (fake_proof,goalno)
+ let subst', ((_,metasenv,_,_), open_goals), maxmeta =
+ PrimitiveTactics.apply_with_subst
+ ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
in
debug_print (" OK: " ^ ppterm cand);
+ assert (maxmeta >= maxm);
(*FIXME:sicuro che posso @?*)
assert_subst_are_disjoint subst subst';
let subst = 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)
- with ProofEngineTypes.Fail s -> (*debug_print(" KO: "^Lazy.force s);*)None
+ Some (metasenv,subst,open_goals), tables , maxmeta
+ with ProofEngineTypes.Fail s ->
+ (*debug_print(" KO: "^Lazy.force s);*)None,tables, maxm
+;;
+
+let applicative_case
+ dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache
+=
+ let candidates = get_candidates cache goalty in
+ let tables, elems, maxm =
+ List.fold_left
+ (fun (tables,elems,maxm) cand ->
+ match
+ try_candidate goalty
+ dbd tables maxm subst fake_proof goalno depth context cand
+ with
+ | None, tables,maxm -> tables,elems, maxm
+ | Some x, tables, maxm -> tables,x::elems, maxm)
+ (tables,[],maxm) candidates
+ in
+ let elems = sort_new_elems elems in
+ elems, tables, cache, maxm
;;
(* Works if there is no dependency over proofs *)
CicUtil.is_meta_closed goalty
;;
let prop = function (_,_,P) -> true | _ -> false;;
-
-let auto_main context flags elems cache universe =
- let timeout =
+let calculate_timeout flags =
if flags.timeout = 0. then
- infinity
+ (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
else
- Unix.gettimeofday () +. flags.timeout
+ flags
+;;
+let is_equational_case goalty flags =
+ let ensure_equational t =
+ if is_an_equational_goal t then true
+ else false
+ (*
+ let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
+ raise (ProofEngineTypes.Fail (lazy msg))
+ *)
in
+ (flags.use_paramod && is_an_equational_goal goalty) ||
+ (flags.use_only_paramod && ensure_equational goalty)
+;;
+let cache_add_success sort cache k v =
+ if sort = P then cache_add_success cache k v else cache_remove_underinspection
+ cache k
+;;
+
+let rec auto_main dbd tables maxm context flags elems cache =
+ let callback_for_paramod maxm flags proof commonctx cache l =
+ let flags = {flags with use_paramod = false;dont_cache_failures=true} in
+ let _,metasenv,_,_ = proof in
+ let oldmetasenv = metasenv in
+ match
+ auto_all_solutions
+ dbd tables maxm cache commonctx metasenv l flags
+ with
+ | [],cache,maxm -> [],cache,maxm
+ | solutions,cache,maxm ->
+ let solutions =
+ HExtlib.filter_map
+ (fun (subst,newmetasenv) ->
+ let opened =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv
+ in
+ if opened = [] then Some subst else None)
+ solutions
+ in
+ solutions,cache,maxm
+ in
+ let flags = calculate_timeout flags in
let ppterm = ppterm context in
let irl = mk_irl context in
- let rec aux cache = function (* elems in OR *)
- | [] -> Fail "no more steps can be done", cache (* COMPLETE FAILURE *)
+ let rec aux tables maxm cache = function (* elems in OR *)
+ | [] -> Fail "no more steps can be done", tables, cache, maxm
+ (*COMPLETE FAILURE*)
| (metasenv,subst,[])::tl ->
- Success (metasenv,subst,tl), cache (* solution::cont *)
+ Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
| (metasenv,subst,goals)::tl when
List.length (List.filter prop goals) > flags.maxwidth ->
debug_print (" FAILURE(width): " ^ string_of_int (List.length goals));
- aux cache tl (* FAILURE (width) *)
+ aux tables maxm cache tl (* FAILURE (width) *)
| (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
- if Unix.gettimeofday() > timeout then Fail "timeout",cache
+ if Unix.gettimeofday() > flags.timeout then
+ Fail "timeout",tables,cache,maxm
else
try
let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
- if sort = T then
+ if sort = T && tl <> [] then (* FIXME!!!! *)
(debug_print (" FAILURE(not in prop)");
- aux cache tl (* FAILURE (not in prop) *))
+ aux tables maxm cache tl (* FAILURE (not in prop) *))
else
- match aux_single cache metasenv subst elem goalty cc with
- | Fail _, cache ->
- debug_print (" FAIL: " ^string_of_int goalno^ ":"^ppterm goalty);
- let cache = cache_add_failure cache goalty depth in
- aux cache tl
- | Success (metasenv,subst,others), cache ->
+ match aux_single tables maxm cache metasenv subst elem goalty cc with
+ | Fail s, tables, cache, maxm' ->
+ assert(maxm' >= maxm);let maxm = maxm' in
+ debug_print
+ (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty);
+ let cache =
+ if flags.dont_cache_failures then
+ cache_remove_underinspection cache goalty
+ else cache_add_failure cache goalty depth
+ in
+ aux tables maxm cache tl
+ | Success (metasenv,subst,others), tables, cache, maxm' ->
+ assert(maxm' >= maxm);let maxm = maxm' in
(* others are alternatives in OR *)
try
let goal = Cic.Meta(goalno,irl) in
debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof);
if is_a_green_cut goalty then
(assert_proof_is_valid proof metasenv context goalty;
- let cache = cache_add_success cache goalty proof in
- aux cache ((metasenv,subst,gl)::tl))
+ let cache = cache_add_success sort cache goalty proof in
+ aux tables maxm cache ((metasenv,subst,gl)::tl))
else
(let goalty = CicMetaSubst.apply_subst subst goalty in
assert_proof_is_valid proof metasenv context goalty;
let cache =
if is_a_green_cut goalty then
- cache_add_success cache goalty proof
+ cache_add_success sort cache goalty proof
else
cache
in
(fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
others
in
- aux cache ((metasenv,subst,gl)::others@tl))
+ aux tables maxm cache ((metasenv,subst,gl)::others@tl))
with CicUtil.Meta_not_found i when i = goalno ->
assert false
with CicUtil.Meta_not_found i when i = goalno ->
(* goalno was closed by sideeffect *)
- aux cache ((metasenv,subst,gl)::tl)
- and aux_single cache metasenv subst (goalno, depth, _) goalty cc =
+ debug_print ("Goal "^string_of_int goalno^" closed by sideeffect");
+ aux tables maxm cache ((metasenv,subst,gl)::tl)
+ and aux_single tables maxm cache metasenv subst (goalno, depth, _) goalty cc =
let goalty = CicMetaSubst.apply_subst subst goalty in
(* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
(* FAILURE (euristic cut) *)
match cache_examine cache goalty with
- | Failed_in d when d >= depth -> Fail "depth",cache(*FAILURE(depth)*)
+ | Failed_in d when d >= depth ->
+ Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
+ tables,cache,maxm(*FAILURE(depth)*)
| Succeded t ->
assert(List.for_all (fun (i,_) -> i <> goalno) subst);
let entry = goalno, (cc, t,goalty) in
let subst = entry :: subst in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
debug_print (" CACHE HIT!");
- Success (metasenv, subst, []),cache
- | UnderInspection -> Fail "looping",cache
+ Success (metasenv, subst, []), tables, cache, maxm
+ | UnderInspection -> 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 candidates = get_candidates universe goalty in
let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
- let elems =
- HExtlib.filter_map
- (try_candidate subst fake_proof goalno depth context)
- candidates
+ let elems, tables, cache, maxm =
+ if is_equational_case goalty flags then
+ match
+ equational_case dbd tables maxm
+ (Some callback_for_paramod) cache
+ depth fake_proof goalno goalty subst context flags
+ with
+ | Some elems, tables, cache, maxm ->
+ elems, tables, cache, maxm
+ | None, tables,cache,maxm ->
+ applicative_case dbd tables maxm depth subst fake_proof goalno
+ goalty metasenv context cache
+ else
+ applicative_case dbd tables maxm depth subst fake_proof goalno
+ goalty metasenv context cache
in
- let elems = sort_new_elems elems in
- aux cache elems
- | _ -> Fail "??",cache
+ aux tables maxm cache elems
+ | _ -> Fail "??",tables,cache,maxm
in
- aux cache elems
-;;
-
-let auto universe cache context metasenv gl flags =
+ aux tables maxm cache elems
+
+and
+ auto_all_solutions dbd tables maxm cache context metasenv gl flags
+=
let goals = order_new_goals metasenv [] gl CicPp.ppterm in
let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
let elems = [metasenv,[],goals] in
- match auto_main context flags elems cache universe with
- | Fail s,cache -> prerr_endline s;None,cache
- | Success (metasenv,subst,_), cache -> Some (subst,metasenv), cache
+ let rec aux tables maxm solutions cache elems flags =
+ match auto_main dbd tables maxm context flags elems cache with
+ | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
+ | Success (metasenv,subst,others),tables,cache,maxm ->
+ if Unix.gettimeofday () > flags.timeout then
+ ((subst,metasenv)::solutions), cache, maxm
+ else
+ aux tables maxm ((subst,metasenv)::solutions) cache others flags
+ in
+ let rc = aux tables maxm [] cache elems flags in
+ prerr_endline "fine auto all solutions";
+ rc
;;
-let auto_all_solutions universe cache context metasenv gl flags =
+(* }}} ****************** AUTO ***************)
+
+let auto_all_solutions dbd cache context metasenv gl flags =
+ let solutions, cache, _ =
+ auto_all_solutions dbd None 0 cache context metasenv gl flags
+ in
+ solutions, cache
+;;
+
+let auto dbd cache context metasenv gl flags =
+ let initial_time = Unix.gettimeofday() in
let goals = order_new_goals metasenv [] gl CicPp.ppterm in
let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
let elems = [metasenv,[],goals] in
- let bigbang = Unix.gettimeofday () in
- let rec aux solutions cache elems flags =
- match auto_main context flags elems cache universe with
- | Fail s,cache ->prerr_endline s; solutions,cache
- | Success (metasenv,subst,others), cache ->
- let elapsed = Unix.gettimeofday () -. bigbang in
- if elapsed > flags.timeout then
- ((subst,metasenv)::solutions), cache
+ match auto_main dbd None 0 context flags elems cache with
+ | Success (metasenv,subst,_), tables,cache,_ ->
+ prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
+ Some (subst,metasenv), cache
+ | Fail s,tables,cache,maxm -> None,cache
+;;
+
+let bool params name default =
+ try
+ let s = List.assoc name params in
+ if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
+ else if s = "0" || s = "false" || s = "no" || s= "off" then false
+ else
+ let msg = "Unrecognized value for parameter "^name^"\n" in
+ let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
+ raise (ProofEngineTypes.Fail (lazy msg))
+ with Not_found -> default
+;;
+
+let string params name default =
+ try List.assoc name params with
+ | Not_found -> default
+;;
+
+let int params name default =
+ try int_of_string (List.assoc name params) with
+ | Not_found -> default
+ | Failure _ ->
+ raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
+;;
+
+let flags_of_params params ?(for_applyS=false) () =
+ let int = int params in
+ let bool = bool params in
+ let use_paramod = bool "use_paramod" true in
+ let use_only_paramod =
+ if for_applyS then true else bool "paramodulation" false in
+ let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
+ let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
+ let timeout = int "timeout" 0 in
+ { AutoTypes.maxdepth =
+ if use_only_paramod then 2 else depth;
+ AutoTypes.maxwidth = width;
+ AutoTypes.timeout =
+ if timeout = 0 then
+ if for_applyS then Unix.gettimeofday () +. 30.0
+ else
+ infinity
+ else
+ Unix.gettimeofday() +. (float_of_int timeout);
+ AutoTypes.use_paramod = use_paramod;
+ AutoTypes.use_only_paramod = use_only_paramod;
+ AutoTypes.dont_cache_failures = false
+ }
+
+let applyS_tac ~dbd ~term ~params =
+ ProofEngineTypes.mk_tactic
+ (fun status ->
+ try
+ let _, proof, gl,_,_ =
+ apply_smart ~dbd ~term ~subst:[]
+ (flags_of_params params ~for_applyS:true ()) status
+ in
+ proof, gl
+ with
+ | CicUnification.UnificationFailure msg
+ | CicTypeChecker.TypeCheckerFailure msg ->
+ raise (ProofEngineTypes.Fail msg))
+
+let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
+ (* argument parsing *)
+ let string = string params in
+ let bool = bool params in
+ let use_only_paramod = bool "paramodulation" false in
+ (* hacks to debug paramod *)
+ let superposition = bool "superposition" false in
+ let target = string "target" "" in
+ let table = string "table" "" in
+ let subterms_only = bool "subterms_only" false in
+ let demod_table = string "demod_table" "" in
+ match superposition with
+ | true ->
+ (* this is the ugly hack to debug paramod *)
+ Saturation.superposition_tac
+ ~target ~table ~subterms_only ~demod_table (proof,goal)
+ | false ->
+ (* this is the real auto *)
+ let _, metasenv, _, _ = proof in
+ let _, context, goalty = CicUtil.lookup_meta goal metasenv in
+ let cache =
+ let cache =
+ AutoCache.cache_add_context context metasenv AutoCache.cache_empty
+ in
+ if use_only_paramod then (* only paramod *)
+ cache
else
- aux ((subst,metasenv)::solutions) cache others
- {flags with timeout = flags.timeout -. elapsed}
- in
- aux [] cache elems flags
+ AutoCache.cache_add_library dbd proof [goal] cache
+ in
+ let oldmetasenv = metasenv in
+ let flags = flags_of_params params () in
+ match auto dbd cache context metasenv [goal] flags with
+ | None,cache ->
+ raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
+ | Some (subst,metasenv),cache ->
+ let proof,metasenv =
+ ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+ proof goal (CicMetaSubst.apply_subst subst) metasenv
+ in
+ let opened =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+ ~newmetasenv:metasenv
+ in
+ proof,opened
;;
+
+let auto_tac ~dbd ~params = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd);;
projects / helm.git / blobdiff