X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fauto.ml;h=b904d52cb055bcd22263eee84d67108da633e54b;hb=98fa2447804cf187f88af1fbd0fa64d5666ff5f2;hp=2db8cc0014ec1d468b60df2872caff898fba9c57;hpb=be87825f491f5eff5f02ee78dd23f34fc0e46e71;p=helm.git diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index 2db8cc001..b904d52cb 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -30,13 +30,13 @@ 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 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 smart_flag cache + Saturation.find_equalities dbd status smart_flag auto cache in let passive = Saturation.make_passive equalities in let active = Saturation.make_active [] in @@ -50,8 +50,8 @@ let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status = (* 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 smart_flag ?auto cache + Saturation.close_more + bag active maxm status smart_flag auto cache else bag, [], cache, maxm in @@ -59,7 +59,7 @@ let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag 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 80 minsteps, minsteps, infinity + else max 50 minsteps, minsteps, infinity in active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout in @@ -75,7 +75,8 @@ let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status = (* {{{ **************** 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 @@ -108,11 +109,8 @@ let new_metasenv_and_unify_and_t PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal) in match - let cache, flags = cache_empty, default_flags() in - let flags = - {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0} - in - given_clause dbd ?tables 0 cache [] flags true (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"))) @@ -127,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 @@ -173,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 @@ -269,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 false (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 @@ -356,7 +356,8 @@ let is_equational_case goalty flags = (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 = @@ -472,11 +473,11 @@ let rec auto_main dbd tables maxm context flags elems cache = 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 -> applicative_case dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache @@ -530,14 +531,112 @@ let auto dbd cache context metasenv gl flags = | 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 ?(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:[] status in - proof, gl + 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 + 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);;