From 5c30cf26474aa4f52d26005c797130a0d6d21ab5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 20 May 2017 18:23:05 +0200 Subject: Fixing a failure to interpret some local implicit arguments in Inductive. For instance, the following was failing to use the implicitness of n: Inductive A (P:forall m {n}, n=m -> Prop) := C : P 0 eq_refl -> A P. --- interp/constrintern.ml | 4 ++-- interp/constrintern.mli | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4dcf287efc..3dfc850410 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -190,10 +190,10 @@ let compute_internalization_data env ty typ impl = let expls_impl = compute_explicitable_implicit impl ty in (ty, expls_impl, impl, compute_arguments_scope typ) -let compute_internalization_env env ty = +let compute_internalization_env env ?(impls=empty_internalization_env) ty = List.fold_left3 (fun map id typ impl -> Id.Map.add id (compute_internalization_data env ty typ impl) map) - empty_internalization_env + impls (**********************************************************************) (* Contracting "{ _ }" in notations *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 644cafe575..f3306b5929 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -61,7 +61,7 @@ val empty_internalization_env : internalization_env val compute_internalization_data : env -> var_internalization_type -> types -> Impargs.manual_explicitation list -> var_internalization_data -val compute_internalization_env : env -> var_internalization_type -> +val compute_internalization_env : env -> ?impls:internalization_env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env -- cgit v1.2.3 From ca630605330828b9b6456477b0fd4f8a0c3f1831 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 21 May 2017 22:23:24 +0200 Subject: More precise on preventing clash between bound vars name and hidden impargs. We want to avoid capture in "Inductive I {A} := C : forall A, I". But in "Record I {A} := { C : forall A, A }.", non recursivity ensures that no clash will occur. This fixes previous commit, with which it could possibly be merged. --- interp/constrintern.ml | 8 ++++---- interp/constrintern.mli | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3dfc850410..ce51f21c7b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -46,7 +46,7 @@ open Context.Rel.Declaration types and recursive definitions and of projection names in records *) type var_internalization_type = - | Inductive of Id.t list (* list of params *) + | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *) | Recursive | Method | Variable @@ -176,7 +176,7 @@ let parsing_explicit = ref false let empty_internalization_env = Id.Map.empty let compute_explicitable_implicit imps = function - | Inductive params -> + | Inductive (params,_) -> (* In inductive types, the parameters are fixed implicit arguments *) let sub_impl,_ = List.chop (List.length params) imps in let sub_impl' = List.filter is_status_implicit sub_impl in @@ -358,12 +358,12 @@ let locate_if_hole ?loc na = function let reset_hidden_inductive_implicit_test env = { env with impls = Id.Map.map (function - | (Inductive _,b,c,d) -> (Inductive [],b,c,d) + | (Inductive (params,_),b,c,d) -> (Inductive (params,false),b,c,d) | x -> x) env.impls } let check_hidden_implicit_parameters id impls = if Id.Map.exists (fun _ -> function - | (Inductive indparams,_,_,_) -> Id.List.mem id indparams + | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams | _ -> false) impls then user_err (strbrk "A parameter of an inductive type " ++ diff --git a/interp/constrintern.mli b/interp/constrintern.mli index f3306b5929..8a759a8033 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -38,7 +38,7 @@ open Misctypes of [env] *) type var_internalization_type = - | Inductive of Id.t list (* list of params *) + | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *) | Recursive | Method | Variable -- cgit v1.2.3 From d9ea37641bc67ca269065a9489ec8e70b2f2d246 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 22 May 2017 10:01:09 +0200 Subject: Locating error about clash between a inductive parameter and a bound variable. Also trying to reformulate the message, distinguishing between a variable/parameter and its name. --- interp/constrintern.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ce51f21c7b..6f01f6a50a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -361,13 +361,14 @@ let reset_hidden_inductive_implicit_test env = | (Inductive (params,_),b,c,d) -> (Inductive (params,false),b,c,d) | x -> x) env.impls } -let check_hidden_implicit_parameters id impls = +let check_hidden_implicit_parameters ?loc id impls = if Id.Map.exists (fun _ -> function | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams | _ -> false) impls then - user_err (strbrk "A parameter of an inductive type " ++ - pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") + user_err ?loc (pr_id id ++ strbrk " is already used as name of " ++ + strbrk "a parameter of the inductive type; bound variables in " ++ + strbrk "the type of a constructor shall use a different name.") let push_name_env ?(global_level=false) ntnvars implargs env = function @@ -376,7 +377,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env = user_err ?loc (str "Anonymous variables not allowed"); env | loc,Name id -> - check_hidden_implicit_parameters id env.impls ; + check_hidden_implicit_parameters ?loc id env.impls ; if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc; set_var_scope ?loc id false env ntnvars; -- cgit v1.2.3