X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FautoTactic.ml;h=79cf52e65fa7bfe791474ef02e08a52c6530e5c6;hb=78f2fb8fcf0bbd2521b67e4366b734ad88ebdc68;hp=050d5c64333d223a7dbe3a2702495256867233e9;hpb=94983be5804a0ecbd14b43fe3b7475443bc8c804;p=helm.git diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index 050d5c643..79cf52e65 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -56,7 +56,7 @@ let search_theorems_in_context status = let module S = CicSubstitution in let module PET = ProofEngineTypes in let module PT = PrimitiveTactics in - let _,metasenv,_,_ = proof in + let _,metasenv,_,_, _ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let rec find n = function | [] -> [] @@ -89,7 +89,7 @@ let search_theorems_in_context status = let compare_goals proof goal1 goal2 = - let _,metasenv,_,_ = proof in + let _,metasenv,_,_, _ = proof in let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1 @@ -129,7 +129,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals if List.mem ty already_seen_goals then [] else let already_seen_goals = ty::already_seen_goals in let facts = (depth = 1) in - let _,metasenv,p,_ = proof in + let _,metasenv,p,_, _ = proof in (* first of all we check if the goal has been already inspected *) assert (CicUtil.exists_meta goal metasenv); @@ -228,7 +228,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals and auto_new dbd width already_seen_goals universe = function | [] -> [] | (subst,(proof, goals, sign))::tl -> - let _,metasenv,_,_ = proof in + let _,metasenv,_,_, _ = proof in let goals'= List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals in @@ -244,7 +244,7 @@ and auto_new_aux dbd width already_seen_goals universe = function (List.length goals) > width -> auto_new dbd width already_seen_goals universe tl | (subst,(proof, (goal,depth)::gtl, sign))::tl -> - let _,metasenv,p,_ = proof in + let _,metasenv,p,_, _ = proof in let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in match (auto_single dbd proof goal ey ty depth (width - (List.length gtl)) sign already_seen_goals) universe @@ -284,9 +284,9 @@ let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) | (_,(proof,[],_))::_ -> let t2 = Unix.gettimeofday () in debug_print (lazy "AUTO_TAC HA FINITO"); - let _,_,p,_ = proof in + let _,_,p,_, _ = proof in debug_print (lazy (CicPp.ppterm p)); - Printf.printf "tempo: %.9f\n" (t2 -. t1); + debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1))); (proof,[]) | _ -> assert false in @@ -317,75 +317,22 @@ let int params name default = raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) ;; -let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) = +let auto_tac ~params ~(dbd:HMysql.dbd) ~universe (proof, goal) = (* argument parsing *) - let int = int params - and string = string params - and bool = bool params in - let newauto = bool "new" false in + let int = int params in + let bool = bool params in + let oldauto = bool "old" false in + let use_only_paramod = bool "paramodulation" false in + let oldauto = if use_only_paramod then false else oldauto 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 oldauto then + auto_tac_old ~depth ~width ~dbd () (proof,goal) + else + ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params ~universe) (proof,goal) -let auto_tac ~params ~dbd = - ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd) +let auto_tac ~params ~dbd ~universe= + ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe) ;; let pp_proofterm = Equality.pp_proofterm;;