X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=305a42ab1adfab718e77d1e4d8f33bd7b919045e;hb=5b8cff10c1c13376ec0f36ecc72ed8c6524b0310;hp=6b1bf82abd7598cbef245ee740fac09e26243d6b;hpb=041ad23b567b9844ec187ad436595868441802f4;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 6b1bf82ab..305a42ab1 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -24,16 +24,19 @@ *) 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 @@ -44,9 +47,11 @@ let given_clause dbd ?tables maxm ?auto cache subst flags status = 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 @@ -54,21 +59,24 @@ let given_clause dbd ?tables maxm ?auto cache subst flags status = 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 @@ -101,11 +109,8 @@ let new_metasenv_and_unify_and_t 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"))) @@ -120,7 +125,7 @@ let rec count_prods context ty = 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 @@ -166,7 +171,7 @@ let apply_smart ~dbd ~term ~subst ?tables (proof, goal) = 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 @@ -262,16 +267,18 @@ let is_an_equational_goal = function ;; 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 ""; prerr_endline (cache_print context cache); prerr_endline ""; +*) 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 @@ -307,9 +314,9 @@ let try_candidate ;; 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 -> @@ -322,7 +329,7 @@ let applicative_case (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 *) @@ -339,25 +346,28 @@ let calculate_timeout flags = 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 -> @@ -396,10 +406,15 @@ let rec auto_main dbd tables maxm context flags elems cache universe = 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 @@ -439,7 +454,8 @@ let rec auto_main dbd tables maxm context flags elems cache universe = (* 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 @@ -457,21 +473,17 @@ let rec auto_main dbd tables maxm context flags elems cache universe = 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 @@ -479,13 +491,13 @@ let rec auto_main dbd tables maxm context flags elems cache universe = 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 @@ -500,35 +512,129 @@ and (* }}} ****************** 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);;