*)
open AutoTypes;;
+open AutoCache;;
-let debug_print s = () (* prerr_endline s;; *)
+let debug_print s = () (*prerr_endline s;;*)
-let given_clause dbd ?tables maxm ?auto cache subst flags status =
- prerr_endline ("given_clause " ^ string_of_int maxm);
- let active, passive, bag, cache, maxmeta, goal_steps, saturation_steps, timeout =
+(* {{{ *********** 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 ?auto true cache
+ Saturation.find_equalities dbd status smart_flag auto cache
in
let passive = Saturation.make_passive equalities in
let active = Saturation.make_active [] 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.saturate_more bag active maxm status true ?auto cache
+ Saturation.close_more
+ bag active maxm status smart_flag auto cache
else
bag, [], cache, maxm
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 30 minsteps, minsteps, infinity
+ else max 50 minsteps, minsteps, infinity
in
active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
in
- let res,a,p, maxmeta =
+ let res,actives,passives,maxmeta =
Saturation.given_clause bag maxmeta status active passive
goal_steps saturation_steps timeout
in
- res,a,p,bag,cache,maxmeta
+ res,actives,passives,bag,cache,maxmeta
;;
+(* }}} ****************************************************************)
+
(* {{{ **************** applyS *******************)
let new_metasenv_and_unify_and_t
- dbd proof goal ?tables newmeta' metasenv' context term' ty termty goal_arity
+ 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
PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
in
match
- let cache, flags = AutoTypes.cache_empty, AutoTypes.default_flags() in
- let flags =
- {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0}
- in
- given_clause dbd ?tables 0 cache [] flags (proof'''',newmeta)
+ 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")))
Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
| _ -> 0
-let apply_smart ~dbd ~term ~subst ?tables (proof, goal) =
+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 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 proof goal ?tables
+ 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
;;
let equational_case
- dbd tables maxm ?auto cache depth fake_proof goalno goalty subst context
+ 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 (fake_proof,goalno)
+ 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
;;
let applicative_case
- dbd tables maxm depth subst fake_proof goalno goalty metasenv context universe
+ dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache
=
- let candidates = get_candidates universe goalty in
+ let candidates = get_candidates cache goalty in
let tables, elems, maxm =
List.fold_left
(fun (tables,elems,maxm) cand ->
(tables,[],maxm) candidates
in
let elems = sort_new_elems elems in
- elems, tables, maxm
+ elems, tables, cache, maxm
;;
(* Works if there is no dependency over proofs *)
let is_equational_case goalty flags =
let ensure_equational t =
if is_an_equational_goal t then true
- else
+ 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
+ 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 universe =
+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} in
+ 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 universe cache commonctx metasenv l flags
+ dbd tables maxm cache commonctx metasenv l flags
with
| [],cache,maxm -> [],cache,maxm
| solutions,cache,maxm ->
aux tables maxm cache tl (* FAILURE (not in prop) *))
else
match aux_single tables maxm cache metasenv subst elem goalty cc with
- | Fail _, tables, cache, maxm' ->
+ | Fail s, tables, cache, maxm' ->
assert(maxm' >= maxm);let maxm = maxm' in
- debug_print (" FAIL: " ^string_of_int goalno^ ":"^ppterm goalty);
- let cache = cache_add_failure cache goalty depth 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
(* FAILURE (euristic cut) *)
match cache_examine cache goalty with
| Failed_in d when d >= depth ->
- Fail "depth",tables,cache,maxm(*FAILURE(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
if is_equational_case goalty flags then
match
equational_case dbd tables maxm
- ~auto:callback_for_paramod cache
+ (Some callback_for_paramod) cache
depth fake_proof goalno goalty subst context flags
with
| Some elems, tables, cache, maxm ->
- elems, tables, cache, maxm (* manca cache *)
+ elems, tables, cache, maxm
| None, tables,cache,maxm ->
- let elems, tables, maxm =
applicative_case dbd tables maxm depth subst fake_proof goalno
- goalty metasenv context universe
- in elems, tables, cache, maxm
+ goalty metasenv context cache
else
- let elems, tables, maxm =
applicative_case dbd tables maxm depth subst fake_proof goalno
- goalty metasenv context universe
- in elems, tables, cache, maxm
+ goalty metasenv context cache
in
aux tables maxm cache elems
| _ -> Fail "??",tables,cache,maxm
aux tables maxm cache elems
and
- auto_all_solutions dbd tables maxm universe cache context metasenv gl flags
+ 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
let rec aux tables maxm solutions cache elems flags =
- match auto_main dbd tables maxm context flags elems cache universe with
+ 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
(* }}} ****************** AUTO ***************)
-let auto_all_solutions dbd universe cache context metasenv gl flags =
+let auto_all_solutions dbd cache context metasenv gl flags =
let solutions, cache, _ =
- auto_all_solutions dbd None 0 universe cache context metasenv gl flags
+ auto_all_solutions dbd None 0 cache context metasenv gl flags
in
solutions, cache
;;
-let auto dbd universe cache context metasenv gl flags =
+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
- match auto_main dbd None 0 context flags elems cache universe with
- | Success (metasenv,subst,_), tables,cache,_ -> Some (subst,metasenv), cache
- | Fail s,tables,cache,maxm ->
- let cache = cache_clean cache in
- match auto_main dbd tables maxm context flags elems cache universe with
- | Success (metasenv,subst,_), tables,cache,_ ->
- Some (subst,metasenv), cache
- | Fail s,tables,cache,maxm -> prerr_endline s;None,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 applyS_tac ~dbd ~term =
+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 ?(use_only_paramod = bool params "paramodulation" false) () =
+ let int = int params in
+ let bool = bool params in
+ let use_paramod = bool "use_paramod" true 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 use_only_paramod then Unix.gettimeofday () +. 30.0
+ else
+ 0.0
+ 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:[] status in
- proof, gl
+ let _, proof, gl,_,_ =
+ apply_smart ~dbd ~term ~subst:[]
+ (flags_of_params params ~use_only_paramod: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
+ 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