diff options
| -rw-r--r-- | tactics/auto.ml | 57 | ||||
| -rw-r--r-- | tactics/auto.mli | 7 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 2 |
4 files changed, 36 insertions, 32 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 30b2b3fc7..b5adc6664 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -204,40 +204,42 @@ let make_apply_entry env sigma (eapply,verbose) pri (c,cty) = let pat = Pattern.pattern_of_constr c' in let hd = (try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry") in - let nmiss = List.length (clenv_missing ce) - in - if eapply & (nmiss <> 0) then begin - if verbose then + let nmiss = List.length (clenv_missing ce) in + if nmiss = 0 then + (hd, + { pri = (match pri with None -> nb_hyp cty | Some p -> p); + pat = Some pat; + code = Res_pf(c,{ce with env=empty_env}) }) + else begin + if not eapply then failwith "make_apply_entry"; + if verbose then warn (str "the hint: eapply " ++ pr_lconstr c ++ - str " will only be used by eauto"); + str " will only be used by eauto"); (hd, - { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); - pat = Some pat; - code = ERes_pf(c,{ce with env=empty_env}) }) - end else - (hd, - { pri = (match pri with None -> nb_hyp cty | Some p -> p); - pat = Some pat; - code = Res_pf(c,{ce with env=empty_env}) }) + { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); + pat = Some pat; + code = ERes_pf(c,{ce with env=empty_env}) }) + end | _ -> failwith "make_apply_entry" -(* eap is (e,v) with e=true if eapply and v=true if verbose +(* flags is (e,v) with e=true if eapply and v=true if verbose c is a constr cty is the type of constr *) -let make_resolves env sigma eap pri c = +let make_resolves env sigma flags pri c = let cty = type_of env sigma c in let ents = map_succeed (fun f -> f (c,cty)) - [make_exact_entry pri; make_apply_entry env sigma (eap,Flags.is_verbose()) pri] + [make_exact_entry pri; make_apply_entry env sigma flags pri] in if ents = [] then errorlabstrm "Hint" - (pr_lconstr c ++ spc() ++ str"cannot be used as a hint"); + (pr_lconstr c ++ spc() ++ + (if fst flags then str"cannot be used as a hint" + else str "can be used as a hint only for eauto")); ents - (* used to add an hypothesis to the local hint database *) let make_resolve_hyp env sigma (hname,_,htyp) = try @@ -364,7 +366,8 @@ let add_resolves env sigma clist local dbnames = Lib.add_anonymous_leaf (inAutoHint (local,dbname, - List.flatten (List.map (fun (x, y) -> make_resolves env sigma true x y) clist)))) + List.flatten (List.map (fun (x, y) -> + make_resolves env sigma (true,Flags.is_verbose()) x y) clist)))) dbnames @@ -577,10 +580,10 @@ let unify_resolve (c,clenv) gls = (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *) -let make_local_hint_db lems g = +let make_local_hint_db eapply lems g = let sign = pf_hyps g in let hintlist = list_map_append (pf_apply make_resolve_hyp g) sign in - let hintlist' = list_map_append (pf_apply make_resolves g true None) lems in + let hintlist' = list_map_append (pf_apply make_resolves g (eapply,false) None) lems in Hint_db.add_list hintlist' (Hint_db.add_list hintlist Hint_db.empty) (* Serait-ce possible de compiler d'abord la tactique puis de faire la @@ -668,13 +671,13 @@ let trivial lems dbnames gl = error ("trivial: "^x^": No such Hint database")) ("core"::dbnames) in - tclTRY (trivial_fail_db db_list (make_local_hint_db lems gl)) gl + tclTRY (trivial_fail_db db_list (make_local_hint_db false lems gl)) gl let full_trivial lems gl = let dbnames = Hintdbmap.dom !searchtable in let dbnames = list_subtract dbnames ["v62"] in let db_list = List.map (fun x -> searchtable_map x) dbnames in - tclTRY (trivial_fail_db db_list (make_local_hint_db lems gl)) gl + tclTRY (trivial_fail_db db_list (make_local_hint_db false lems gl)) gl let gen_trivial lems = function | None -> full_trivial lems @@ -772,7 +775,7 @@ let auto n lems dbnames gl = ("core"::dbnames) in let hyps = pf_hyps gl in - tclTRY (search n db_list (make_local_hint_db lems gl) hyps) gl + tclTRY (search n db_list (make_local_hint_db false lems gl) hyps) gl let default_auto = auto !default_search_depth [] [] @@ -781,7 +784,7 @@ let full_auto n lems gl = let dbnames = list_subtract dbnames ["v62"] in let db_list = List.map (fun x -> searchtable_map x) dbnames in let hyps = pf_hyps gl in - tclTRY (search n db_list (make_local_hint_db lems gl) hyps) gl + tclTRY (search n db_list (make_local_hint_db false lems gl) hyps) gl let default_full_auto gl = full_auto !default_search_depth [] gl @@ -810,7 +813,7 @@ let default_search_decomp = ref 1 let destruct_auto des_opt lems n gl = let hyps = pf_hyps gl in search_gen des_opt n (List.map searchtable_map ["core";"extcore"]) - (make_local_hint_db lems gl) hyps gl + (make_local_hint_db false lems gl) hyps gl let dautomatic des_opt lems n = tclTRY (destruct_auto des_opt lems n) @@ -895,7 +898,7 @@ let search_superauto n to_add argl g = (fun (id,c) -> add_named_decl (id, None, pf_type_of g c)) to_add empty_named_context in let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in - let db = Hint_db.add_list db0 (make_local_hint_db [] g) in + let db = Hint_db.add_list db0 (make_local_hint_db false [] g) in super_search n [Hintdbmap.find "core" !searchtable] db argl g let superauto n to_add argl = diff --git a/tactics/auto.mli b/tactics/auto.mli index de3814630..4fe9f03a9 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -95,7 +95,7 @@ val make_apply_entry : has missing arguments. *) val make_resolves : - env -> evar_map -> bool -> int option -> constr -> + env -> evar_map -> bool * bool -> int option -> constr -> (global_reference * pri_auto_tactic) list (* [make_resolve_hyp hname htyp]. @@ -125,9 +125,10 @@ val set_extern_subst_tactic : -> unit (* Create a Hint database from the pairs (name, constr). - Useful to take the current goal hypotheses as hints *) + Useful to take the current goal hypotheses as hints; + Boolean tells if lemmas with evars are allowed *) -val make_local_hint_db : constr list -> goal sigma -> Hint_db.t +val make_local_hint_db : bool -> constr list -> goal sigma -> Hint_db.t val priority : (int * 'a) list -> 'a list diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 32103a058..c87baf25f 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -275,7 +275,7 @@ let e_breadth_search debug s = let e_search_auto debug (in_depth,p) lems db_list gls = let sigma = Evd.sig_sig (fst gls) and gls' = Evd.sig_it (fst gls) in - let local_dbs = List.map (fun gl -> make_local_hint_db lems ({it = gl; sigma = sigma})) gls' in + let local_dbs = List.map (fun gl -> make_local_hint_db true lems ({it = gl; sigma = sigma})) gls' in let state = make_initial_state p gls db_list local_dbs in if in_depth then e_depth_search debug state diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index ab62aa9cf..74d6f9ccc 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -357,7 +357,7 @@ let e_breadth_search debug n db_list local_db gl = with Not_found -> error "EAuto: breadth first search failed" let e_search_auto debug (in_depth,p) lems db_list gl = - let local_db = make_local_hint_db lems gl in + let local_db = make_local_hint_db true lems gl in if in_depth then e_depth_search debug p db_list local_db gl else |