From 273005ac85e9ae0c23328e243edeadfc8dcaf8bb Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Oct 2015 22:25:35 +0200 Subject: Fixing a bug in reporting ill-formed inductive. Was introduced in b06d3badb (15 Jul 2015). --- kernel/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5d7a0bbf00..8b03df64c6 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -390,7 +390,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = | _::hyps -> match kind_of_term (whd_betadeltaiota env lpar.(k)) with | Rel w when Int.equal w index -> check (k-1) (index+1) hyps - | _ -> raise (IllFormedInd (LocalNonPar (k+1, index, l))) + | _ -> raise (IllFormedInd (LocalNonPar (k+1, index-n+nhyps+1, l))) in check (nparams-1) (n-nhyps) hyps; if not (Array.for_all (noccur_between n ntypes) largs') then failwith_non_pos_vect n ntypes largs' -- cgit v1.2.3 From c2de48c3f59415eaf0f2cbb5cfe78f23e908a459 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 25 Oct 2015 12:14:12 +0100 Subject: Minor module cleanup : error HigherOrderInclude was never happening When F is a Functor, doing an 'Include F' triggers the 'Include Self' mechanism: the current context is used as an pseudo-argument to F. This may fail with a subtype error if the current context isn't adequate. --- kernel/mod_typing.ml | 2 +- kernel/mod_typing.mli | 3 +++ kernel/modops.ml | 4 ---- kernel/modops.mli | 3 --- kernel/safe_typing.ml | 8 ++------ 5 files changed, 6 insertions(+), 14 deletions(-) (limited to 'kernel') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 922652287b..eef83ce743 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -359,4 +359,4 @@ let rec translate_mse_incl env mp inl = function |MEapply (fe,arg) -> let ftrans = translate_mse_incl env mp inl fe in translate_apply env inl ftrans arg (fun _ _ -> None) - |_ -> Modops.error_higher_order_include () + |MEwith _ -> assert false (* No 'with' syntax for modules *) diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 80db12b0d3..0c3fb2ba79 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -36,6 +36,9 @@ val translate_mse : env -> module_path option -> inline -> module_struct_entry -> module_alg_expr translation +(** [translate_mse_incl] translate the mse of a real module (no + module type here) given to an Include *) + val translate_mse_incl : env -> module_path -> inline -> module_struct_entry -> module_alg_expr translation diff --git a/kernel/modops.ml b/kernel/modops.ml index 8733ca8c2f..f0cb65c967 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -67,7 +67,6 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string - | HigherOrderInclude exception ModuleTypingError of module_typing_error @@ -113,9 +112,6 @@ let error_generative_module_expected l = let error_no_such_label_sub l l1 = raise (ModuleTypingError (LabelMissing (l,l1))) -let error_higher_order_include () = - raise (ModuleTypingError HigherOrderInclude) - (** {6 Operations on functors } *) let is_functor = function diff --git a/kernel/modops.mli b/kernel/modops.mli index 6fbcd81d03..a335ad9b4a 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -126,7 +126,6 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string - | HigherOrderInclude exception ModuleTypingError of module_typing_error @@ -153,5 +152,3 @@ val error_incorrect_with_constraint : Label.t -> 'a val error_generative_module_expected : Label.t -> 'a val error_no_such_label_sub : Label.t->string->'a - -val error_higher_order_include : unit -> 'a diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9329b16861..fdacbb365c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -706,17 +706,13 @@ let add_include me is_module inl senv = let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in compute_sign (Modops.subst_signature subst str) mb resolver senv - | str -> resolver,str,senv + | NoFunctor str -> resolver,str,senv in - let resolver,sign,senv = + let resolver,str,senv = let struc = NoFunctor (List.rev senv.revstruct) in let mtb = build_mtb mp_sup struc Univ.ContextSet.empty senv.modresolver in compute_sign sign mtb resolver senv in - let str = match sign with - | NoFunctor struc -> struc - | MoreFunctor _ -> Modops.error_higher_order_include () - in let senv = update_resolver (Mod_subst.add_delta_resolver resolver) senv in let add senv ((l,elem) as field) = -- cgit v1.2.3 From 83e82ef7b42f47d63d3b40b2698695a0e7b2d685 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 25 Oct 2015 14:58:39 +0100 Subject: Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331) --- kernel/mod_typing.ml | 12 ++++++++++-- kernel/mod_typing.mli | 14 +++++++------- kernel/safe_typing.ml | 9 ++------- 3 files changed, 19 insertions(+), 16 deletions(-) (limited to 'kernel') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index eef83ce743..c03c5175fd 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -351,12 +351,20 @@ let translate_module env mp inl = function let restype = Option.map (fun ty -> ((params,ty),inl)) oty in finalize_module env mp t restype -let rec translate_mse_incl env mp inl = function +let rec translate_mse_inclmod env mp inl = function |MEident mp1 -> let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in let sign = clean_bounded_mod_expr mb.mod_type in sign,None,mb.mod_delta,Univ.ContextSet.empty |MEapply (fe,arg) -> - let ftrans = translate_mse_incl env mp inl fe in + let ftrans = translate_mse_inclmod env mp inl fe in translate_apply env inl ftrans arg (fun _ _ -> None) |MEwith _ -> assert false (* No 'with' syntax for modules *) + +let translate_mse_incl is_mod env mp inl me = + if is_mod then + translate_mse_inclmod env mp inl me + else + let mtb = translate_modtype env mp inl ([],me) in + let sign = clean_bounded_mod_expr mtb.mod_type in + sign,None,mtb.mod_delta,mtb.mod_constraints diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 0c3fb2ba79..bc0e20205a 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -36,14 +36,14 @@ val translate_mse : env -> module_path option -> inline -> module_struct_entry -> module_alg_expr translation -(** [translate_mse_incl] translate the mse of a real module (no - module type here) given to an Include *) - -val translate_mse_incl : - env -> module_path -> inline -> module_struct_entry -> - module_alg_expr translation - val finalize_module : env -> module_path -> module_expression translation -> (module_type_entry * inline) option -> module_body + +(** [translate_mse_incl] translate the mse of a module or + module type given to an Include *) + +val translate_mse_incl : + bool -> env -> module_path -> inline -> module_struct_entry -> + module_alg_expr translation diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index fdacbb365c..ec245b0648 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -682,13 +682,8 @@ let end_modtype l senv = let add_include me is_module inl senv = let open Mod_typing in let mp_sup = senv.modpath in - let sign,cst,resolver = - if is_module then - let sign,_,reso,cst = translate_mse_incl senv.env mp_sup inl me in - sign,cst,reso - else - let mtb = translate_modtype senv.env mp_sup inl ([],me) in - mtb.mod_type,mtb.mod_constraints,mtb.mod_delta + let sign,_,resolver,cst = + translate_mse_incl is_module senv.env mp_sup inl me in let senv = add_constraints (Now (false, cst)) senv in (* Include Self support *) -- cgit v1.2.3