diff options
| -rw-r--r-- | tactics/taccoerce.ml | 38 | ||||
| -rw-r--r-- | tactics/taccoerce.mli | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 10 |
3 files changed, 47 insertions, 5 deletions
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index ab71f5f2e7..8ee52c96f3 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -85,7 +85,7 @@ let coerce_to_constr_context v = else raise (CannotCoerceTo "a term context") (* Interprets an identifier which must be fresh *) -let coerce_to_ident fresh env v = +let coerce_var_to_ident fresh env v = let v = Value.normalize v in let fail () = raise (CannotCoerceTo "a fresh identifier") in if has_type v (topwit wit_intro_pattern) then @@ -102,6 +102,42 @@ let coerce_to_ident fresh env v = destVar c else fail () +(* Interprets, if possible, a constr to an identifier which may not + be fresh but suitable to be given to the fresh tactic. Works for + vars, constants, inductive, constructors and sorts. *) +let coerce_to_ident_not_fresh env v = + let v = Value.normalize v in + let fail () = raise (CannotCoerceTo "an identifier") in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) -> id + | _ -> fail () + else if has_type v (topwit wit_var) then + out_gen (topwit wit_var) v + else + match Value.to_constr v with + | None -> fail () + | Some c -> + match Constr.kind c with + | Var id -> id + | Const (cst,_) -> Label.to_id (Constant.label cst) + | Construct (cstr,_) -> + let ref = Globnames.ConstructRef cstr in + let basename = Nametab.basename_of_global ref in + basename + | Ind (ind,_) -> + let ref = Globnames.IndRef ind in + let basename = Nametab.basename_of_global ref in + basename + | Sort s -> + begin + match s with + | Prop _ -> Label.to_id (Label.make "Prop") + | Type _ -> Label.to_id (Label.make "Type") + end + | _ -> fail() + + let coerce_to_intro_pattern env v = let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index 85bad364d7..bf522b6116 100644 --- a/tactics/taccoerce.mli +++ b/tactics/taccoerce.mli @@ -48,7 +48,9 @@ end val coerce_to_constr_context : Value.t -> constr -val coerce_to_ident : bool -> Environ.env -> Value.t -> Id.t +val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t + +val coerce_to_ident_not_fresh : Environ.env -> Value.t -> Id.t val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 593e46b05c..c2e3400835 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -319,7 +319,7 @@ let interp_ltac_var coerce ist env locid = with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time") let interp_ident ist env sigma id = - try try_interp_ltac_var (coerce_to_ident false env) ist (Some (env,sigma)) (dloc,id) + try try_interp_ltac_var (coerce_var_to_ident false env) ist (Some (env,sigma)) (dloc,id) with Not_found -> id let pf_interp_ident id gl = interp_ident id (pf_env gl) (project gl) @@ -478,6 +478,10 @@ let extract_ids ids lfun = let default_fresh_id = Id.of_string "H" let interp_fresh_id ist env sigma l = + let extract_ident ist env sigma id = + try try_interp_ltac_var (coerce_to_ident_not_fresh env) + ist (Some (env,sigma)) (dloc,id) + with Not_found -> id in let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in let avoid = match TacStore.get ist.extra f_avoid_ids with | None -> [] @@ -490,7 +494,7 @@ let interp_fresh_id ist env sigma l = let s = String.concat "" (List.map (function | ArgArg s -> s - | ArgVar (_,id) -> Id.to_string (interp_ident ist env sigma id)) l) in + | ArgVar (_,id) -> Id.to_string (extract_ident ist env sigma id)) l) in let s = if Lexer.is_keyword s then s^"0" else s in Id.of_string s in Tactics.fresh_id_in_env avoid id env @@ -507,7 +511,7 @@ let extract_ltac_constr_context ist env = with CannotCoerceTo _ -> map in let add_ident id env v map = - try Id.Map.add id (coerce_to_ident false env v) map + try Id.Map.add id (coerce_var_to_ident false env v) map with CannotCoerceTo _ -> map in let fold id v {idents;typed;untyped} = |