aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/genintern.ml2
-rw-r--r--interp/genintern.mli2
-rw-r--r--plugins/decl_mode/decl_interp.ml3
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml2
-rw-r--r--tactics/taccoerce.ml20
-rw-r--r--tactics/tacintern.ml80
-rw-r--r--tactics/tacintern.mli2
-rw-r--r--tactics/tacinterp.ml70
8 files changed, 117 insertions, 64 deletions
diff --git a/interp/genintern.ml b/interp/genintern.ml
index 00ea3a71b..12d25c785 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -13,7 +13,7 @@ open Mod_subst
open Genarg
type glob_sign = {
- ltacvars : Id.t list * Id.t list;
+ ltacvars : Id.Set.t;
ltacrecvars : (Id.t * Nametab.ltac_constant) list;
gsigma : Evd.evar_map;
genv : Environ.env }
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 25050fe7c..9fe553cba 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -11,7 +11,7 @@ open Mod_subst
open Genarg
type glob_sign = {
- ltacvars : Id.t list * Id.t list;
+ ltacvars : Id.Set.t;
ltacrecvars : (Id.t * Nametab.ltac_constant) list;
gsigma : Evd.evar_map;
genv : Environ.env }
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index c4d6a7a30..04c8c3064 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -44,8 +44,7 @@ let intern_constr_or_thesis globs = function
| This c -> This (intern_constr globs c)
let add_var id globs=
- let l1,l2=globs.ltacvars in
- {globs with ltacvars= (id::l1),(id::l2)}
+ {globs with ltacvars = Id.Set.add id globs.ltacvars}
let add_name nam globs=
match nam with
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 70c7f8d1f..cabbd4755 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1459,7 +1459,7 @@ let do_instr raw_instr pts =
let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in
let gl = { it=List.hd gls ; sigma=sigma } in
let env= pf_env gl in
- let ist = {ltacvars = ([],[]); ltacrecvars = [];
+ let ist = {ltacvars = Id.Set.empty; ltacrecvars = [];
gsigma = sigma; genv = env} in
let glob_instr = intern_proof_instr ist raw_instr in
let instr =
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 0d1a48f50..9318955df 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -88,6 +88,8 @@ let coerce_to_ident fresh env v =
match out_gen (topwit wit_intro_pattern) v with
| _, 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 ->
@@ -100,6 +102,9 @@ let coerce_to_intro_pattern env v =
let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
snd (out_gen (topwit wit_intro_pattern) v)
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ IntroIdentifier id
else match Value.to_constr v with
| Some c when isVar c ->
(* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
@@ -134,6 +139,9 @@ let coerce_to_constr env v =
([], c)
else if has_type v (topwit wit_constr_under_binders) then
out_gen (topwit wit_constr_under_binders) v
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ (try [], constr_of_id env id with Not_found -> fail ())
else fail ()
let coerce_to_closed_constr env v =
@@ -146,8 +154,12 @@ let coerce_to_evaluable_ref env v =
let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
- | _, IntroIdentifier id when List.mem id (Termops.ids_of_context env) -> EvalVarRef id
+ | _, IntroIdentifier id when is_variable env id -> EvalVarRef id
| _ -> fail ()
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ if List.mem id (Termops.ids_of_context env) then EvalVarRef id
+ else fail ()
else
let ev = match Value.to_constr v with
| Some c when isConst c -> EvalConstRef (destConst c)
@@ -178,6 +190,9 @@ let coerce_to_hyp env v =
match out_gen (topwit wit_intro_pattern) v with
| _, IntroIdentifier id when is_variable env id -> id
| _ -> fail ()
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ if is_variable env id then id else fail ()
else match Value.to_constr v with
| Some c when isVar c -> destVar c
| _ -> fail ()
@@ -215,6 +230,9 @@ let coerce_to_quantified_hypothesis v =
match v with
| _, IntroIdentifier id -> NamedHyp id
| _ -> raise (CannotCoerceTo "a quantified hypothesis")
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ NamedHyp id
else if has_type v (topwit wit_int) then
AnonHyp (out_gen (topwit wit_int) v)
else raise (CannotCoerceTo "a quantified hypothesis")
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index c449cab8d..6f0d7525d 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -54,7 +54,7 @@ let skip_metaid = function
(** Generic arguments *)
type glob_sign = Genintern.glob_sign = {
- ltacvars : Id.t list * Id.t list;
+ ltacvars : Id.Set.t;
(* ltac variables and the subset of vars introduced by Intro/Let/... *)
ltacrecvars : (Id.t * ltac_constant) list;
(* ltac recursive names *)
@@ -62,7 +62,7 @@ type glob_sign = Genintern.glob_sign = {
genv : Environ.env }
let fully_empty_glob_sign =
- { ltacvars = ([],[]); ltacrecvars = [];
+ { ltacvars = Id.Set.empty; ltacrecvars = [];
gsigma = Evd.empty; genv = Environ.empty_env }
let make_empty_glob_sign () =
@@ -124,28 +124,28 @@ let lookup_ltacref r = KNmap.find r !mactab
(* We have identifier <| global_reference <| constr *)
let find_ident id ist =
- List.mem id (fst ist.ltacvars) or
+ Id.Set.mem id ist.ltacvars ||
List.mem id (ids_of_named_context (Environ.named_context ist.genv))
let find_recvar qid ist = List.assoc qid ist.ltacrecvars
(* a "var" is a ltac var or a var introduced by an intro tactic *)
-let find_var id ist = List.mem id (fst ist.ltacvars)
+let find_var id ist = Id.Set.mem id ist.ltacvars
(* a "ctxvar" is a var introduced by an intro tactic (Intro/LetTac/...) *)
-let find_ctxvar id ist = List.mem id (snd ist.ltacvars)
+let find_ctxvar id ist = Id.Set.mem id ist.ltacvars
(* a "ltacvar" is an ltac var (Let-In/Fun/...) *)
-let find_ltacvar id ist = find_var id ist & not (find_ctxvar id ist)
+let find_ltacvar id ist = Id.Set.mem id ist.ltacvars
let find_hyp id ist =
List.mem id (ids_of_named_context (Environ.named_context ist.genv))
(* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *)
(* be fresh in which case it is binding later on *)
-let intern_ident l ist id =
+let intern_ident s ist id =
(* We use identifier both for variables and new names; thus nothing to do *)
- if not (find_ident id ist) then l:=(id::fst !l,id::snd !l);
+ if not (find_ident id ist) then s := Id.Set.add id !s;
id
let intern_name l ist = function
@@ -304,7 +304,7 @@ let intern_binding_name ist x =
let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in
- let ltacvars = (fst lfun, Id.Set.empty) in
+ let ltacvars = (Id.Set.elements lfun, Id.Set.empty) in
let c' =
warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars sigma env) c
in
@@ -377,6 +377,7 @@ let intern_flag ist red =
let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
let intern_constr_pattern ist ~as_type ~ltacvars pc =
+ let ltacvars = Id.Set.elements ltacvars, Id.Set.empty in
let metas,pat = Constrintern.intern_constr_pattern
ist.gsigma ist.genv ~as_type ~ltacvars pc
in
@@ -442,13 +443,11 @@ let intern_hyp_location ist ((occs,id),hl) =
intern_hyp_or_metaid ist id), hl)
(* Reads a pattern *)
-let intern_pattern ist ?(as_type=false) lfun = function
+let intern_pattern ist ?(as_type=false) ltacvars = function
| Subterm (b,ido,pc) ->
- let ltacvars = (lfun, Id.Set.empty) in
let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
ido, metas, Subterm (b,ido,pc)
| Term pc ->
- let ltacvars = (lfun, Id.Set.empty) in
let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
None, metas, Term pc
@@ -459,31 +458,37 @@ let intern_constr_may_eval ist = function
| ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c)
| ConstrTerm c -> ConstrTerm (intern_constr ist c)
+let name_cons accu = function
+| Anonymous -> accu
+| Name id -> Id.Set.add id accu
+
+let opt_cons accu = function
+| None -> accu
+| Some id -> Id.Set.add id accu
(* Reads the hypotheses of a "match goal" rule *)
let rec intern_match_goal_hyps ist lfun = function
| (Hyp ((_,na) as locna,mp))::tl ->
let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
- let lfun' = name_cons na (Option.List.cons ido lfun) in
+ let lfun' = name_cons (opt_cons lfun ido) na in
lfun', metas1@metas2, Hyp (locna,pat)::hyps
| (Def ((_,na) as locna,mv,mp))::tl ->
let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in
- let lfun' = name_cons na (Option.List.cons ido' (Option.List.cons ido lfun)) in
+ let lfun' = name_cons (opt_cons (opt_cons lfun ido) ido') na in
lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
| [] -> lfun, [], []
(* Utilities *)
let extract_let_names lrc =
- List.fold_right
- (fun ((loc,name),_) l ->
- if List.mem name l then
- user_err_loc
- (loc, "glob_tactic", str "This variable is bound several times.");
- name::l)
- lrc []
+ let fold accu ((loc, name), _) =
+ if Id.Set.mem name accu then user_err_loc
+ (loc, "glob_tactic", str "This variable is bound several times.")
+ else Id.Set.add name accu
+ in
+ List.fold_left fold Id.Set.empty lrc
let clause_app f = function
{ onhyps=None; concl_occs=nl } ->
@@ -641,8 +646,8 @@ and intern_tactic_seq onlytac ist = function
!lf, TacAtom (adjust_loc loc, t)
| TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun)
| TacLetIn (isrec,l,u) ->
- let (l1,l2) = ist.ltacvars in
- let ist' = { ist with ltacvars = (extract_let_names l @ l1, l2) } in
+ let ltacvars = Id.Set.union (extract_let_names l) ist.ltacvars in
+ let ist' = { ist with ltacvars } in
let l = List.map (fun (n,b) ->
(n,intern_tacarg !strict_check false (if isrec then ist' else ist) b)) l in
ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u)
@@ -702,9 +707,8 @@ and intern_tactic_or_tacarg ist = intern_tactic false ist
and intern_pure_tactic ist = intern_tactic true ist
and intern_tactic_fun ist (var,body) =
- let (l1,l2) = ist.ltacvars in
- let lfun' = List.rev_append (Option.List.flatten var) l1 in
- (var,intern_tactic_or_tacarg { ist with ltacvars = (lfun',l2) } body)
+ let lfun = List.fold_left opt_cons ist.ltacvars var in
+ (var,intern_tactic_or_tacarg { ist with ltacvars = lfun } body)
and intern_tacarg strict onlytac ist = function
| Reference r -> intern_non_tactic_reference strict ist r
@@ -740,11 +744,13 @@ and intern_match_rule onlytac ist = function
| (All tc)::tl ->
All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl)
| (Pat (rl,mp,tc))::tl ->
- let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
+ let {ltacvars=lfun; gsigma=sigma; genv=env} = ist in
let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
let ido,metas2,pat = intern_pattern ist lfun mp in
- let metas = List.uniquize (metas1@metas2) in
- let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
+ let fold accu x = Id.Set.add x accu in
+ let ltacvars = List.fold_left fold (opt_cons lfun' ido) metas1 in
+ let ltacvars = List.fold_left fold ltacvars metas2 in
+ let ist' = { ist with ltacvars } in
Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
| [] -> []
@@ -754,7 +760,7 @@ and intern_genarg ist x =
in_gen (glbwit wit_int_or_var)
(intern_or_var ist (out_gen (rawwit wit_int_or_var) x))
| IdentArgType b ->
- let lf = ref ([],[]) in
+ let lf = ref Id.Set.empty in
in_gen (glbwit (wit_ident_gen b))
(intern_ident lf ist (out_gen (rawwit (wit_ident_gen b)) x))
| VarArgType ->
@@ -804,9 +810,11 @@ let glob_tactic x =
(intern_pure_tactic (make_empty_glob_sign ())) x
let glob_tactic_env l env x =
+ let ltacvars =
+ List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
Flags.with_option strict_check
(intern_pure_tactic
- { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env })
+ { ltacvars; ltacrecvars = []; gsigma = Evd.empty; genv = env })
x
(***************************************************************************)
@@ -939,7 +947,7 @@ let add_tacdef local isrec tacl =
let () =
let intern_intro_pattern ist pat =
- let lf = ref ([], []) in
+ let lf = ref Id.Set.empty in
let ans = intern_intro_pattern lf ist pat in
let ist = { ist with ltacvars = !lf } in
(ist, ans)
@@ -950,7 +958,11 @@ let () =
(* Backwarding recursive needs of tactic glob/interp/eval functions *)
let _ =
- let f l = Flags.with_option strict_check
- (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars=(l,[])})
+ let f l =
+ let ltacvars =
+ List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l
+ in
+ Flags.with_option strict_check
+ (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars })
in
Hook.set Auto.extern_intern_tac f
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 3fa59ed3b..53a04f700 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -24,7 +24,7 @@ open Nametab
Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
type glob_sign = Genintern.glob_sign = {
- ltacvars : Id.t list * Id.t list;
+ ltacvars : Id.Set.t;
ltacrecvars : (Id.t * ltac_constant) list;
gsigma : Evd.evar_map;
genv : Environ.env }
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 05a62e499..58c64a831 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -363,8 +363,13 @@ let interp_move_location ist gl = function
let interp_reference ist env = function
| ArgArg (_,r) -> r
- | ArgVar locid ->
- interp_ltac_var (coerce_to_reference env) ist (Some env) locid
+ | ArgVar (loc, id) ->
+ try try_interp_ltac_var (coerce_to_reference env) ist (Some env) (loc, id)
+ with Not_found ->
+ try
+ let (v, _, _) = Environ.lookup_named id env in
+ VarRef v
+ with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)
let pf_interp_reference ist gl = interp_reference ist (pf_env gl)
@@ -372,19 +377,28 @@ let interp_inductive ist = function
| ArgArg r -> r
| ArgVar locid -> interp_ltac_var coerce_to_inductive ist None locid
+let try_interp_evaluable env (loc, id) =
+ let v = Environ.lookup_named id env in
+ match v with
+ | (_, Some _, _) -> EvalVarRef id
+ | _ -> error_not_evaluable (VarRef id)
+
let interp_evaluable ist env = function
| ArgArg (r,Some (loc,id)) ->
- (* Maybe [id] has been introduced by Intro-like tactics *)
- (try match Environ.lookup_named id env with
- | (_,Some _,_) -> EvalVarRef id
- | _ -> error_not_evaluable (VarRef id)
- with Not_found ->
- match r with
- | EvalConstRef _ -> r
- | _ -> error_global_not_found_loc loc (qualid_of_ident id))
+ (* Maybe [id] has been introduced by Intro-like tactics *)
+ begin
+ try try_interp_evaluable env (loc, id)
+ with Not_found ->
+ match r with
+ | EvalConstRef _ -> r
+ | _ -> error_global_not_found_loc loc (qualid_of_ident id)
+ end
| ArgArg (r,None) -> r
- | ArgVar locid ->
- interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid
+ | ArgVar (loc, id) ->
+ try try_interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) (loc, id)
+ with Not_found ->
+ try try_interp_evaluable env (loc, id)
+ with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)
(* Interprets an hypothesis name *)
let interp_occurrences ist occs =
@@ -794,21 +808,27 @@ let interp_induction_arg ist gl arg =
strbrk "Cannot coerce " ++ pr_id id ++
strbrk " neither to a quantified hypothesis nor to a term.")
in
+ let try_cast_id id' =
+ if Tactics.is_quantified_hypothesis id' gl
+ then ElimOnIdent (loc,id')
+ else
+ (try ElimOnConstr (sigma,(constr_of_id env id',NoBindings))
+ with Not_found ->
+ user_err_loc (loc,"",
+ pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis."))
+ in
try
+ (** FIXME: should be moved to taccoerce *)
let v = Id.Map.find id ist.lfun in
let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
let v = out_gen (topwit wit_intro_pattern) v in
match v with
- | _, IntroIdentifier id' ->
- if Tactics.is_quantified_hypothesis id' gl
- then ElimOnIdent (loc,id')
- else
- (try ElimOnConstr (sigma,(constr_of_id env id',NoBindings))
- with Not_found ->
- user_err_loc (loc,"",
- pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis."))
+ | _, IntroIdentifier id -> try_cast_id id
| _ -> error ()
+ else if has_type v (topwit wit_var) then
+ let id = out_gen (topwit wit_var) v in
+ try_cast_id id
else if has_type v (topwit wit_int) then
ElimOnAnonHyp (out_gen (topwit wit_int) v)
else match Value.to_constr v with
@@ -1075,7 +1095,10 @@ and force_vrec ist gl v =
and interp_ltac_reference loc' mustbetac ist gl = function
| ArgVar (loc,id) ->
- let v = Id.Map.find id ist.lfun in
+ let v =
+ try Id.Map.find id ist.lfun
+ with Not_found -> in_gen (topwit wit_var) id
+ in
let (sigma,v) = force_vrec ist gl v in
let v = propagate_trace ist loc id v in
sigma , if mustbetac then coerce_to_tactic loc id v else v
@@ -1987,7 +2010,8 @@ let interp_tac_gen lfun avoid_ids debug t gl =
let extra = TacStore.set TacStore.empty f_debug debug in
let extra = TacStore.set extra f_avoid_ids avoid_ids in
let ist = { lfun = lfun; extra = extra } in
- let ltacvars = List.map fst (Id.Map.bindings lfun), [] in
+ let fold x _ accu = Id.Set.add x accu in
+ let ltacvars = Id.Map.fold fold lfun Id.Set.empty in
interp_tactic ist
(intern_pure_tactic {
ltacvars; ltacrecvars = [];
@@ -2001,7 +2025,7 @@ let eval_ltac_constr gl t =
(* Used to hide interpretation for pretty-print, now just launch tactics *)
let hide_interp t ot gl =
- let ist = { ltacvars = ([],[]); ltacrecvars = [];
+ let ist = { ltacvars = Id.Set.empty; ltacrecvars = [];
gsigma = project gl; genv = pf_env gl } in
let te = intern_pure_tactic ist t in
let t = eval_tactic te in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 06:26:52 +0000