diff options
| -rw-r--r-- | interp/constrintern.ml | 38 | ||||
| -rw-r--r-- | interp/constrintern.mli | 14 |
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 |