From 98f9fb6ea86529fc623c031933e88ae9a8354a02 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 25 Jul 2008 19:59:53 +0000 Subject: Correction d'une incohérence de typage des inductifs polymorphes: les contraintes bornant par le haut le type de l'inductif (ce qui peut arriver quand l'inductif est argument d'une constante) étaient oubliées : on pouvait se retrouver avec des inductifs dont le type des constructeurs, une fois instancié par des paramètres) n'était plus typable (seul leur réduit, après expansion des constantes, était typable). [kernel, test-suite] + Affichage des inductifs (via Print) en prenant la forme utilisateur des constructeurs. + Correction warning dans compilation gallina.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11266 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/indtypes.ml | 7 +++++-- kernel/inductive.ml | 4 +++- kernel/inductive.mli | 3 +++ kernel/univ.ml | 5 +++++ kernel/univ.mli | 2 ++ 5 files changed, 18 insertions(+), 3 deletions(-) (limited to 'kernel') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index cd9e2e81f4..5786e67d53 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -254,10 +254,13 @@ let typecheck_inductive env mie = array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst -> let sign, s = dest_arity env full_arity in let status,cst = match s with - | Type _ when ar_level <> None (* Explicitly polymorphic *) -> + | Type u when ar_level <> None (* Explicitly polymorphic *) + && no_upper_constraints u cst -> (* The polymorphic level is a function of the level of the *) (* conclusions of the parameters *) - Inr (param_ccls, lev), cst + (* We enforce [u >= lev] in case [lev] has a strict upper *) + (* constraints over [u] *) + Inr (param_ccls, lev), enforce_geq u lev cst | Type u (* Not an explicit occurrence of Type *) -> Inl (info,full_arity,s), enforce_geq u lev cst | Prop Pos when engagement env <> Some ImpredicativeSet -> diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 8ff8ddb85e..918a32c956 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -228,7 +228,9 @@ let arities_of_specif kn (mib,mip) = let arities_of_constructors ind specif = arities_of_specif (fst ind) specif - +let type_of_constructors ind (mib,mip) = + let specif = mip.mind_user_lc in + Array.map (constructor_instantiate (fst ind) mib) specif (************************************************************************) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index e63c7772c3..118d19830e 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -47,6 +47,9 @@ val type_of_constructor : constructor -> mind_specif -> types (* Return constructor types in normal form *) val arities_of_constructors : inductive -> mind_specif -> types array +(* Return constructor types in user form *) +val type_of_constructors : inductive -> mind_specif -> types array + (* Transforms inductive specification into types (in nf) *) val arities_of_specif : mutual_inductive -> mind_specif -> types array diff --git a/kernel/univ.ml b/kernel/univ.ml index 001ee3ea8a..a681210acf 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -550,6 +550,11 @@ let subst_large_constraint u u' v = let subst_large_constraints = List.fold_right (fun (u,u') -> subst_large_constraint u u') +let no_upper_constraints u cst = + match u with + | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst + | Max _ -> anomaly "no_upper_constraints" + (* Pretty-printing *) let num_universes g = diff --git a/kernel/univ.mli b/kernel/univ.mli index 1ce5329ab9..225dce9a6c 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -76,6 +76,8 @@ val subst_large_constraint : universe -> universe -> universe -> universe val subst_large_constraints : (universe * universe) list -> universe -> universe +val no_upper_constraints : universe -> constraints -> bool + (*s Pretty-printing of universes. *) val pr_uni : universe -> Pp.std_ppcmds -- cgit v1.2.3