From: Claudio Sacerdoti Coen Date: Mon, 9 Oct 2006 18:17:50 +0000 (+0000) Subject: 1. applyS now uses its ~params X-Git-Tag: make_still_working~6776 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=46834f1afe49d481045a40fb1bf6ddbddcfef9f5;p=helm.git 1. applyS now uses its ~params 2. autoTactic.ml* is going to be deprecated. auto.ml* has now the expected interface (that of a tactic) and it is almost ready to replace autoTactic.ml --- diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 117978d8c..305a42ab1 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -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,10 +109,7 @@ 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 + let cache = cache_empty in given_clause dbd ?tables 0 None cache [] flags true (proof'''',newmeta) with | None, active, passive, bag,_,_ -> @@ -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 @@ -533,14 +531,110 @@ let auto dbd cache context metasenv gl flags = | 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 ?(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);; diff --git a/helm/software/components/tactics/auto.mli b/helm/software/components/tactics/auto.mli index c9f3b9b09..301aa4b45 100644 --- a/helm/software/components/tactics/auto.mli +++ b/helm/software/components/tactics/auto.mli @@ -24,23 +24,8 @@ *) (* stops at the first solution *) -val auto: - HMysql.dbd -> - AutoCache.cache -> - Cic.context -> - Cic.metasenv -> - ProofEngineTypes.goal list -> (* goals in AND *) - AutoTypes.flags -> - (Cic.substitution * Cic.metasenv) option * AutoCache.cache - -val auto_all_solutions: - HMysql.dbd -> - AutoCache.cache -> - Cic.context -> - Cic.metasenv -> - ProofEngineTypes.goal list -> - AutoTypes.flags -> - (Cic.substitution * Cic.metasenv) list * AutoCache.cache +val auto_tac: + dbd:HMysql.dbd -> params:(string * string) list -> ProofEngineTypes.tactic val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> params:(string * string) list -> diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml index 050d5c643..25696d794 100644 --- a/helm/software/components/tactics/autoTactic.ml +++ b/helm/software/components/tactics/autoTactic.ml @@ -319,70 +319,15 @@ let int params name default = let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) = (* argument parsing *) - let int = int params - and string = string params - and bool = bool params in + let int = int params in + let bool = bool params in let newauto = bool "new" 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 - let use_paramod = bool "use_paramod" true 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 - let newauto = if use_only_paramod then true else newauto 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 -> - if not newauto then - auto_tac_old ~depth ~width ~dbd () (proof,goal) - else - (* 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 = { - AutoTypes.maxdepth = - if use_only_paramod then 2 else depth; - AutoTypes.maxwidth = width; - AutoTypes.timeout = - if timeout = 0 then float_of_int timeout - else Unix.gettimeofday() +. (float_of_int timeout); - AutoTypes.use_paramod = use_paramod; - AutoTypes.use_only_paramod = use_only_paramod; - AutoTypes.dont_cache_failures = false - } - in - match Auto.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 -;; + if not newauto then + auto_tac_old ~depth ~width ~dbd () (proof,goal) + else + ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params) (proof,goal) let auto_tac ~params ~dbd = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd) diff --git a/helm/software/components/tactics/autoTactic.mli b/helm/software/components/tactics/autoTactic.mli index fadb603eb..23f1b813f 100644 --- a/helm/software/components/tactics/autoTactic.mli +++ b/helm/software/components/tactics/autoTactic.mli @@ -25,8 +25,6 @@ *) val auto_tac: - params:(string * string) list -> - dbd:HMysql.dbd -> - ProofEngineTypes.tactic + params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic val pp_proofterm: Cic.term -> string