aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--interp/constrintern.ml38
-rw-r--r--interp/constrintern.mli14
2 files changed, 32 insertions, 20 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 268aacd40..66851e70e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -22,10 +22,12 @@ open Topconstr
open Nametab
open Symbols
-type implicits_env = (* For interpretation of inductive type with implicits *)
- identifier list *
+type implicits_env = (* To interpret inductive type with implicits *)
(identifier * (identifier list * Impargs.implicits_list)) list
+type full_implicits_env =
+ identifier list * implicits_env
+
let interning_grammar = ref false
let for_grammar f x =
@@ -161,17 +163,17 @@ let set_var_scope loc id (_,scopt,scopes) (_,_,varscopes,_,_) =
abstracted until this point *)
let intern_var (env,_,_) ((vars1,unbndltacvars),vars2,_,_,impls) loc id =
+ (* Is [id] an inductive type potentially with implicit *)
+ try
+ let l,impl = List.assoc id impls in
+ let l = List.map
+ (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
+ RVar (loc,id), impl, [],
+ (if !Options.v7 & !interning_grammar then [] else l)
+ with Not_found ->
(* Is [id] bound in current env or ltac vars bound to constr *)
if Idset.mem id env or List.mem id vars1
then
- (* Is [id] an inductive type with implicit *)
- try
- let l,impl = List.assoc id impls in
- let l = List.map
- (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
- RVar (loc,id), impl, [],
- (if !Options.v7 & !interning_grammar then [] else l)
- with Not_found ->
RVar (loc,id), [], [], []
else
(* Is [id] bound to a free name in ltac (this is an ltac error message) *)
@@ -412,10 +414,10 @@ let locate_if_isevar loc na = function
with Not_found -> RHole (loc, BinderType na))
| x -> x
-let check_hidden_implicit_parameters id (_,_,_,indparams,_) =
- if List.mem id indparams then
- errorlabstrm "" (str "A parameter of inductive type " ++ pr_id id
- ++ str " must not be used as a bound variable in the type \
+let check_hidden_implicit_parameters id (_,_,_,indnames,_) =
+ if List.mem id indnames then
+ errorlabstrm "" (str "A parameter or name of an inductive type " ++
+ pr_id id ++ str " must not be used as a bound variable in the type \
of its constructor")
let push_name_env lvar (ids,tmpsc,scopes as env) = function
@@ -795,6 +797,10 @@ let interp_rawtype sigma env c =
let interp_rawtype_with_implicits sigma env impls c =
interp_rawconstr_gen_with_implicits true sigma env impls false ([],[]) c
+let interp_rawconstr_with_implicits env vars impls c =
+ interp_rawconstr_gen_with_implicits false Evd.empty env ([],impls) false
+ (vars,[]) c
+
(*
(* The same as interp_rawconstr but with a list of variables which must not be
globalized *)
@@ -872,12 +878,12 @@ let interp_constrpattern_gen sigma env ltacvar c =
let interp_constrpattern sigma env c =
interp_constrpattern_gen sigma env [] c
-let interp_aconstr vars a =
+let interp_aconstr impls vars a =
let env = Global.env () in
(* [vl] is intended to remember the scope of the free variables of [a] *)
let vl = List.map (fun id -> (id,ref None)) vars in
let c = for_grammar (internalise Evd.empty (extract_ids env, None, [])
- false (([],[]),Environ.named_context env,vl,[],[])) a in
+ false (([],[]),Environ.named_context env,vl,[],impls)) a in
(* Translate and check that [c] has all its free variables bound in [vars] *)
let a = aconstr_of_rawconstr vars c in
(* Returns [a] and the ordered list of variables with their scopes *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index fa7162435..c1c9ede02 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -33,10 +33,12 @@ open Termops
- insert existential variables for implicit arguments
*)
-type implicits_env = (* For interpretation of inductive type with implicits *)
- identifier list *
+type implicits_env = (* To interpret inductive type with implicits *)
(identifier * (identifier list * Impargs.implicits_list)) list
+type full_implicits_env =
+ identifier list * implicits_env
+
type ltac_sign =
identifier list * (identifier * identifier option) list
@@ -62,7 +64,10 @@ val interp_casted_openconstr :
argument associates a list of implicit positions to identifiers
declared in the rel_context of [env] *)
val interp_type_with_implicits :
- evar_map -> env -> implicits_env -> constr_expr -> types
+ evar_map -> env -> full_implicits_env -> constr_expr -> types
+
+val interp_rawconstr_with_implicits :
+ env -> identifier list -> implicits_env -> constr_expr -> rawconstr
(*s Build a judgement from *)
val judgment_of_rawconstr : evar_map -> env -> constr_expr -> unsafe_judgment
@@ -91,7 +96,8 @@ val interp_constrpattern :
val interp_reference : ltac_sign -> reference -> rawconstr
(* Interprets into a abbreviatable constr *)
-val interp_aconstr : identifier list -> constr_expr -> interpretation
+val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
+ interpretation
(* Globalization leak for Grammar *)
val for_grammar : ('a -> 'b) -> 'a -> 'b