From ca3812d7804f3936bb420e96fad034983ede271a Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 27 Apr 2008 16:46:15 +0000 Subject: Correction du bug des types singletons pas sous-type de Set (i.e. "Inductive unit := tt." conduisait à "t:Prop" alors que le principe de la hiérarchie d'univers est d'être cumulative -- et que Set en soit le niveau 0). Une solution aurait été de poser Prop <= Set mais on adopte une autre solution. Pour éviter le côté contre-intuitif d'avoir unit dans Type et Prop <= Set, on garde la représentation de Prop au sein de la hiérarchie prédicative sous la forme "Type (max ([],[])" (le niveau sans aucune contrainte inférieure, appelons Type -1) et on adapte les fonctions de sous-typage et de typage pour qu'elle prenne en compte la règle Type -1 <= Prop (cf reduction.ml, reductionops.ml, et effets incidents dans Termops.refresh_universes et Univ.super). Petite uniformisation des noms d'univers et de sortes au passage (univ.ml, univ.mli, term.ml, term.mli et les autres fichiers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10859 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/inductive.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'checker/inductive.ml') diff --git a/checker/inductive.ml b/checker/inductive.ml index c2301777d2..febe312f27 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -127,8 +127,8 @@ Remark: Set (predicative) is encoded as Type(0) let sort_as_univ = function | Type u -> u -| Prop Null -> neutral_univ -| Prop Pos -> base_univ +| Prop Null -> lower_univ +| Prop Pos -> type0_univ let cons_subst u su subst = try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst @@ -182,8 +182,8 @@ let instantiate_universes env ctx ar argsorts = let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in let level = subst_large_constraints subst ar.poly_level in ctx, - if is_empty_univ level then Prop Null - else if is_base_univ level then Prop Pos + if is_lower_univ level then Prop Null + else if is_type0_univ level then Prop Pos else Type level let type_of_inductive_knowing_parameters env mip paramtyps = @@ -204,11 +204,11 @@ let type_of_inductive env (_,mip) = let cumulate_constructor_univ u = function | Prop Null -> u - | Prop Pos -> sup base_univ u + | Prop Pos -> sup type0_univ u | Type u' -> sup u u' let max_inductive_sort = - Array.fold_left cumulate_constructor_univ neutral_univ + Array.fold_left cumulate_constructor_univ lower_univ (************************************************************************) (* Type of a constructor *) -- cgit v1.2.3