X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTactic.ml;h=050d5c64333d223a7dbe3a2702495256867233e9;hb=8e7803e5a72ca67cf4d99794da20c1e066f738c5;hp=61d078c22140dce589be39211b1bc0289e48ed4c;hpb=beb4e1e9549d5b43e24907dc86c7ef899e487a3c;p=helm.git diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml index 61d078c22..050d5c643 100644 --- a/helm/software/components/tactics/autoTactic.ml +++ b/helm/software/components/tactics/autoTactic.ml @@ -269,8 +269,7 @@ and auto_new_aux dbd width already_seen_goals universe = function let default_depth = 5 let default_width = 3 -(* -let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) +let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) () = let auto_tac dbd (proof,goal) = @@ -281,7 +280,7 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) let t1 = Unix.gettimeofday () in match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with [] -> debug_print (lazy "Auto failed"); - raise (ProofEngineTypes.Fail "No Applicable theorem") + raise (ProofEngineTypes.Fail (lazy "No Applicable theorem")) | (_,(proof,[],_))::_ -> let t2 = Unix.gettimeofday () in debug_print (lazy "AUTO_TAC HA FINITO"); @@ -291,267 +290,102 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) (proof,[]) | _ -> assert false in - ProofEngineTypes.mk_tactic (auto_tac dbd) + auto_tac dbd ;; -*) -(* -let paramodulation_tactic = ref - (fun dbd ?full ?depth ?width status -> - raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));; - -let term_is_equality = ref - (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);; -*) - -let bool name params = - try let _ = List.assoc name params in true with - | Not_found -> false +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 name params = +let string params name default = try List.assoc name params with - | Not_found -> "" + | Not_found -> default ;; -let int name default params = +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 callback_for_paramodulation dbd width depth t l = - let _,y,x,xx = t in - let universe = MetadataQuery.universe_of_goals ~dbd t l in - let todo = List.map (fun g -> (g, depth)) l in - prerr_endline ("AUTO: " ^ CicPp.ppterm x ^ " : " ^ CicPp.ppterm xx); - prerr_endline ("MENV: " ^ CicMetaSubst.ppmetasenv [] y); - match auto_new dbd width [] universe [(fun x -> x), (t, todo, None)] with - | (_,(proof,[],_))::_ -> proof - | _ -> raise (Failure "xxx") -;; -*) - -let callback_for_paramodulation dbd flags proof commonctx ?universe cache l = - let _,metasenv,_,_ = proof in - let oldmetasenv = metasenv in - let universe = - match universe with - | Some u -> u - | None -> - let universe = - AutoTypes.universe_of_goals dbd proof l AutoTypes.empty_universe - in - AutoTypes.universe_of_context commonctx metasenv universe - in - match - Auto.auto_all_solutions universe cache commonctx metasenv l flags - with - | [],cache -> [],cache,universe - | solutions,cache -> - let solutions = - HExtlib.filter_map - (fun (subst,metasenv) -> - let opened = - ProofEngineHelpers.compare_metasenvs - ~oldmetasenv ~newmetasenv:metasenv - in - if opened = [] then - Some subst - else - None) - solutions - in - solutions,cache,universe -;; - let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) = (* argument parsing *) - let depth = int "depth" AutoTypes.default_flags.AutoTypes.maxdepth params in - let width = int "width" AutoTypes.default_flags.AutoTypes.maxwidth params in - let timeout = string "timeout" params in - let paramodulation = bool "paramodulation" params in - let full = bool "full" params in - let superposition = bool "superposition" params in - let target = string "target" params in - let table = string "table" params in - let subterms_only = bool "subterms_only" params in - let caso_strano = bool "caso_strano" params in - let demod_table = string "demod_table" params in - let timeout = - try Some (float_of_string timeout) with Failure _ -> None - in + let int = int params + and string = string params + and 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 use_paramodulation = - paramodulation && Equality.term_is_equality goalty + 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 - if use_paramodulation then - try - let rc = - Saturation.saturate - ~auto:(callback_for_paramodulation dbd) - caso_strano dbd ~depth ~width ~full - ?timeout (proof, goal) + 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 - prerr_endline (Saturation.get_stats ());rc - with exn -> - prerr_endline (Saturation.get_stats ());raise exn - else - let universe = - AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe - in - let universe = (* we should get back a menv too XXX *) - AutoTypes.universe_of_context context metasenv universe - in - let oldmetasenv = metasenv in - match - Auto.auto universe AutoTypes.cache_empty context metasenv [goal] - {AutoTypes.default_flags with - AutoTypes.maxdepth = depth; - AutoTypes.maxwidth = width; -(* AutoTypes.timeout = 0; *) - } - 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 opened = + ProofEngineHelpers.compare_metasenvs ~oldmetasenv + ~newmetasenv:metasenv + in + proof,opened ;; let auto_tac ~params ~dbd = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd) ;; -(* {{{ **************** applyS *******************) - -let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' ty termty goal_arity = - let (consthead,newmetasenv,arguments,_) = - ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in - let term'' = match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) in - let proof',metasenv = - let (puri,metasenv,pbo,pty) = proof in - (puri,newmetasenv,pbo,pty),metasenv - in - let proof'',goals = - match LibraryObjects.eq_URI () with - | Some uri -> - ProofEngineTypes.apply_tactic - (Tacticals.then_ - ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*)) - ~continuation: - (PrimitiveTactics.cut_tac - (CicSubstitution.lift 1 - (Cic.Appl - [Cic.MutInd (uri,0,[]); - Cic.Sort Cic.Prop; - consthead; - ty])))) (proof',goal) - | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined")) - in - match goals with - [g1;g2] -> - let proof'',goals = - ProofEngineTypes.apply_tactic - (auto_tac ~params:["caso_strano","on";"paramodulation","on"] ~dbd) (proof'',g2) - in - let proof'',goals = - ProofEngineTypes.apply_tactic - (Tacticals.then_ - ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft - ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1)) - ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2)) - ) (proof'',g1) - in - proof'', - (*CSC: Brrrr.... *) - ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv - ~newmetasenv:(let _,m,_,_ = proof'' in m) - | _ -> assert false - -let rec count_prods context ty = - match CicReduction.whd context ty with - Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t - | _ -> 0 - -let applyS_tac ~dbd ~term (proof, goal) = - let module T = CicTypeChecker in - let module R = CicReduction in - let module C = Cic in - let (_,metasenv,_,_) = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in - let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = - match term with - C.Var (uri,exp_named_subst) -> - let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = - PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri - exp_named_subst - in - exp_named_subst_diff,newmeta',newmetasenvfragment, - C.Var (uri,exp_named_subst') - | C.Const (uri,exp_named_subst) -> - let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = - PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri - exp_named_subst - in - exp_named_subst_diff,newmeta',newmetasenvfragment, - C.Const (uri,exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = - PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri - exp_named_subst - in - exp_named_subst_diff,newmeta',newmetasenvfragment, - C.MutInd (uri,tyno,exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff = - PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri - exp_named_subst - in - exp_named_subst_diff,newmeta',newmetasenvfragment, - C.MutConstruct (uri,tyno,consno,exp_named_subst') - | _ -> [],newmeta,[],term - in - let metasenv' = metasenv@newmetasenvfragment in - let termty,_ = - CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph - in - let termty = - CicSubstitution.subst_vars exp_named_subst_diff termty in - let goal_arity = count_prods context ty in - let res = - new_metasenv_and_unify_and_t dbd proof goal - newmeta' metasenv' context term' ty termty goal_arity - in - res - -let applyS_tac ~dbd ~term = - ProofEngineTypes.mk_tactic - (fun status -> - try applyS_tac ~dbd ~term status - with - | CicUnification.UnificationFailure msg - | CicTypeChecker.TypeCheckerFailure msg -> - raise (ProofEngineTypes.Fail msg)) - -(* }}} ********************************) - let pp_proofterm = Equality.pp_proofterm;;