X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=41ea1e5e44386f35ec74959a6784bdfb0a095deb;hb=5649890273cf8e660bba744e84ce5fee1e5efe69;hp=9be698dcf286e48f4966e9bfb27f7473a2a9f85c;hpb=b2a190e3c2d5b594d409db937e88f9f4f7d22b8c;p=helm.git diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 9be698dcf..41ea1e5e4 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -30,6 +30,8 @@ let debug = false;; let debug_print s = if debug then prerr_endline (Lazy.force s);; +type auto_params = Cic.term list * (string * string) list + let elems = ref [] ;; (* closing a term w.r.t. its metavariables @@ -480,6 +482,80 @@ let find_context_equalities indexes, equalities, maxm, cache ;; +(********** PARAMETERS PASSING ***************) + +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 close_more = bool "close_more" false in + let use_paramod = bool "use_paramod" true in + let use_only_paramod = + if for_applyS then true else bool "paramodulation" false in + let use_library = bool "library" + ((AutoTypes.default_flags()).AutoTypes.use_library) in + let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in + let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in + let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in + let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in + let do_type = bool "type" false in + let timeout = int "timeout" 0 in + { AutoTypes.maxdepth = + if use_only_paramod then 2 else depth; + AutoTypes.maxwidth = width; + AutoTypes.maxsize = size; + 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_library = use_library; + AutoTypes.use_paramod = use_paramod; + AutoTypes.use_only_paramod = use_only_paramod; + AutoTypes.close_more = close_more; + AutoTypes.dont_cache_failures = false; + AutoTypes.maxgoalsizefactor = gsize; + AutoTypes.do_types = do_type; + } + +let universe_of_params metasenv context universe tl = + if tl = [] then universe else + let tys = + List.map + (fun term -> + fst (CicTypeChecker.type_of_aux' metasenv context term + CicUniv.oblivion_ugraph)) + tl + in + Universe.index_list Universe.empty context (List.combine tl tys) +;; + + (***************** applyS *******************) let new_metasenv_and_unify_and_t @@ -542,12 +618,16 @@ 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 ~universe ?tables flags (proof, goal) = +let apply_smart + ~dbd ~term ~subst ~universe ?tables ~params:(univ,params) (proof, goal) += let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let flags = flags_of_params params ~for_applyS:true () in + let universe = universe_of_params metasenv context universe univ in let newmeta = CicMkImplicit.new_meta metasenv subst in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with @@ -1475,72 +1555,12 @@ let auto flags metasenv tables universe cache context metasenv gl = 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 ?(for_applyS=false) () = - let int = int params in - let bool = bool params in - let close_more = bool "close_more" false in - let use_paramod = bool "use_paramod" true in - let use_only_paramod = - if for_applyS then true else bool "paramodulation" false in - let use_library = bool "library" - ((AutoTypes.default_flags()).AutoTypes.use_library) in - let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in - let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in - let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in - let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in - let do_type = bool "type" false in - let timeout = int "timeout" 0 in - { AutoTypes.maxdepth = - if use_only_paramod then 2 else depth; - AutoTypes.maxwidth = width; - AutoTypes.maxsize = size; - 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_library = use_library; - AutoTypes.use_paramod = use_paramod; - AutoTypes.use_only_paramod = use_only_paramod; - AutoTypes.close_more = close_more; - AutoTypes.dont_cache_failures = false; - AutoTypes.maxgoalsizefactor = gsize; - AutoTypes.do_types = do_type; - } - let applyS_tac ~dbd ~term ~params ~universe = ProofEngineTypes.mk_tactic (fun status -> try let proof, gl,_,_ = - apply_smart ~dbd ~term ~subst:[] ~universe - (flags_of_params params ~for_applyS:true ()) status + apply_smart ~dbd ~term ~subst:[] ~params ~universe status in proof, gl with @@ -1548,185 +1568,45 @@ let applyS_tac ~dbd ~term ~params ~universe = | CicTypeChecker.TypeCheckerFailure msg -> raise (ProofEngineTypes.Fail msg)) -(* SUPERPOSITION *) - -(* Syntax: - * auto superposition target = NAME - * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only] - * - * - if table is omitted no superposition will be performed - * - if demod_table is omitted no demodulation will be prformed - * - subterms_only is passed to Indexing.superposition_right - * - * lists are coded using _ (example: H_H1_H2) - *) - -let eq_and_ty_of_goal = function - | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri -> - uri,t - | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality "))) -;; - -let rec find_in_ctx i name = function - | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name))) - | Some (Cic.Name name', _)::tl when name = name' -> i - | _::tl -> find_in_ctx (i+1) name tl -;; - -let rec position_of i x = function - | [] -> assert false - | j::tl when j <> x -> position_of (i+1) x tl - | _ -> i -;; - - -let superposition_tac ~target ~table ~subterms_only ~demod_table status = - Saturation.reset_refs(); - let proof,goalno = status in - let curi,metasenv,_subst,pbo,pty, attrs = proof in - let metano,context,ty = CicUtil.lookup_meta goalno metasenv in - let eq_uri,tty = eq_and_ty_of_goal ty in - let env = (metasenv, context, CicUniv.empty_ugraph) in - let names = Utils.names_of_context context in - let bag = Equality.mk_equality_bag () in - let eq_index, equalities, maxm,cache = - find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty - in - let eq_what = - let what = find_in_ctx 1 target context in - List.nth equalities (position_of 0 what eq_index) - in - let eq_other = - if table <> "" then - let other = - let others = Str.split (Str.regexp "_") table in - List.map (fun other -> find_in_ctx 1 other context) others - in - List.map - (fun other -> List.nth equalities (position_of 0 other eq_index)) - other - else - [] - in - let index = List.fold_left Indexing.index Indexing.empty eq_other in - let maxm, eql = - if table = "" then maxm,[eq_what] else - Indexing.superposition_right bag - ~subterms_only eq_uri maxm env index eq_what +let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) = + let _,metasenv,_subst,_,_, _ = proof in + let _,context,goalty = CicUtil.lookup_meta goal metasenv in + let universe = universe_of_params metasenv context universe univ in + let flags = flags_of_params params () in + let use_library = flags.use_library in + let tables,cache,newmeta = + init_cache_and_tables ~dbd use_library flags.use_only_paramod true + false universe (proof, goal) in + let tables,cache,newmeta = + if flags.close_more then + close_more + tables newmeta context (proof, goal) + auto_all_solutions universe cache + else tables,cache,newmeta in + let initial_time = Unix.gettimeofday() in + let (_,oldmetasenv,_subst,_,_, _) = proof in + hint := None; + let elem = + metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[] in - debug_print (lazy ("Superposition right:")); - debug_print (lazy ("\n eq: " ^ Equality.string_of_equality eq_what ~env)); - debug_print (lazy ("\n table: ")); - List.iter - (fun e -> - debug_print (lazy (" " ^ Equality.string_of_equality e ~env))) eq_other; - debug_print (lazy ("\n result: ")); - List.iter (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql; - debug_print (lazy ("\n result (cut&paste): ")); - List.iter - (fun e -> - let t = Equality.term_of_equality eq_uri e in - debug_print (lazy (CicPp.pp t names))) - eql; - debug_print (lazy ("\n result proofs: ")); - List.iter (fun e -> - debug_print (lazy (let _,p,_,_,_ = Equality.open_equality e in - let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in - Subst.ppsubst s ^ "\n" ^ - CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names))) eql; - if demod_table <> "" then - begin - let eql = - if eql = [] then [eq_what] else eql - in - let demod = - let demod = Str.split (Str.regexp "_") demod_table in - List.map (fun other -> find_in_ctx 1 other context) demod - in - let eq_demod = - List.map - (fun demod -> List.nth equalities (position_of 0 demod eq_index)) - demod - in - let table = List.fold_left Indexing.index Indexing.empty eq_demod in - let maxm,eql = - List.fold_left - (fun (maxm,acc) e -> - let maxm,eq = - Indexing.demodulation_equality bag eq_uri maxm env table e - in - maxm,eq::acc) - (maxm,[]) eql - in - let eql = List.rev eql in - debug_print (lazy ("\n result [demod]: ")); - List.iter - (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql; - debug_print (lazy ("\n result [demod] (cut&paste): ")); - List.iter - (fun e -> - let t = Equality.term_of_equality eq_uri e in - debug_print (lazy (CicPp.pp t names))) - eql; - end; - proof,[goalno] -;; - -let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) = - (* argument parsing *) - let string = string params in - let bool = bool params 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 *) - superposition_tac - ~target ~table ~subterms_only ~demod_table (proof,goal) - | false -> - (* this is the real auto *) - let _,metasenv,_subst,_,_, _ = proof in - let _,context,goalty = CicUtil.lookup_meta goal metasenv in - let flags = flags_of_params params () in - (* just for testing *) - let use_library = flags.use_library in - let tables,cache,newmeta = - init_cache_and_tables ~dbd use_library flags.use_only_paramod true - false universe (proof, goal) in - let tables,cache,newmeta = - if flags.close_more then - close_more - tables newmeta context (proof, goal) - auto_all_solutions universe cache - else tables,cache,newmeta in - let initial_time = Unix.gettimeofday() in - let (_,oldmetasenv,_subst,_,_, _) = proof in - hint := None; - let elem = - metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[] - in - match auto_main tables newmeta context flags universe cache [elem] with - | Proved (metasenv,subst,_, tables,cache,_) -> - (*prerr_endline - ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));*) - let proof,metasenv = - ProofEngineHelpers.subst_meta_and_metasenv_in_proof - proof goal subst metasenv - in - let opened = - ProofEngineHelpers.compare_metasenvs ~oldmetasenv - ~newmetasenv:metasenv - in - proof,opened - | Gaveup (tables,cache,maxm) -> - debug_print - (lazy ("TIME:"^ - string_of_float(Unix.gettimeofday()-.initial_time))); - raise (ProofEngineTypes.Fail (lazy "Auto gave up")) + match auto_main tables newmeta context flags universe cache [elem] with + | Proved (metasenv,subst,_, tables,cache,_) -> + (*prerr_endline + ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));*) + let proof,metasenv = + ProofEngineHelpers.subst_meta_and_metasenv_in_proof + proof goal subst metasenv + in + let opened = + ProofEngineHelpers.compare_metasenvs ~oldmetasenv + ~newmetasenv:metasenv + in + proof,opened + | Gaveup (tables,cache,maxm) -> + debug_print + (lazy ("TIME:"^ + string_of_float(Unix.gettimeofday()-.initial_time))); + raise (ProofEngineTypes.Fail (lazy "Auto gave up")) ;; let auto_tac ~dbd ~params ~universe = @@ -1740,9 +1620,11 @@ let eq_of_goal = function (* performs steps of rewrite with the universe, obtaining if possible * a trivial goal *) -let solve_rewrite_tac ~universe ?(steps=1) (proof,goal as status)= +let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)= let _,metasenv,_subst,_,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in + let steps = int_of_string (string params "steps" "1") in + let universe = universe_of_params metasenv context universe univ in let eq_uri = eq_of_goal ty in let (active,passive,bag), cache, maxm = (* we take the whole universe (no signature filtering) *) @@ -1774,14 +1656,15 @@ let solve_rewrite_tac ~universe ?(steps=1) (proof,goal as status)= (ProofEngineTypes.Fail (lazy ("Unable to solve with " ^ string_of_int steps ^ " demodulations"))) ;; -let solve_rewrite_tac ~universe ?steps () = - ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ?steps) +let solve_rewrite_tac ~params ~universe () = + ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ~params) ;; (* DEMODULATE *) -let demodulate_tac ~dbd ~universe (proof,goal)= +let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)= let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in + let universe = universe_of_params metasenv context universe univ in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let initgoal = [], metasenv, ty in let eq_uri = eq_of_goal ty in @@ -1823,8 +1706,8 @@ let demodulate_tac ~dbd ~universe (proof,goal)= ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*) ;; -let demodulate_tac ~dbd ~universe = - ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);; +let demodulate_tac ~dbd ~params ~universe = + ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~universe);; let pp_proofterm = Equality.pp_proofterm;;