Changement de stratégie vis à vis du commit 10859 sur la gestion des

univers, suite à discussion avec Bruno : on franchit le cap et on
ajoute le sous-typage Prop <= Set. On n'a donc plus besoin d'utiliser
l'image de Prop dans la hiérarchie en dehors de la zone de calcul de
la sorte la plus basse d'un inductif polymorphe (au passage, nous
avons décidé de renommer Type -1 en Type 0-, pour bien indiquer qu'il
se trouve au même niveau que Type 0).

Coq se retrouve donc avec la hiérarchie Prop <= Set <= Type i et avec
une copie de Prop (Type 0-) et une copie de Set (Type 0) dans la
hiérarchie Type. En théorie, on pourrait donc supprimer "Prop Null" et
"Prop Pos" de l'implémentation et ne travailler qu'avec "Type".

L'ajout de Prop <= Set vaut à la fois dans le cas Set prédicatif et
dans le cas Set imprédicatif (Prop et Set étant en bas de la
hiérarchie, il n'y a pas d'incohérence connue). Dans le modéle
ensembliste, Prop et Type 0- sont interprétés par exemple comme
{{},{o}}, où "o" est un objet particulier interprétant les preuves, et
il n'y a pas de Set imprédicatif.  Dans un modèle de réalisabilité,
Set imprédicatif est interprétable et Prop peut au choix s'interpréter
comme Set ou comme booléen (cf la thèse de Miquel). Le sous-typage du
côté ensembliste s'obtient en mettant au moins l'ensemble {{},{o}}
dans l'interprétation de Set (ce qu'on fait de la même manière que
Prop <= Type 1, avec conversion typée), et du côté réalisabilité en
mettant l'ensemble {Typ(vide),Typ(unit)} dans l'interprétation de Set
("Typ" étant la coercion faisant d'un ensemble un terme), ce qui est
fait dans la section 6.2.4 de la thèse d'Alexandre Miquel (modèle du
CC implicite sans types inductifs).

Il reste un problème pratique. Lorsqu'on donne

  Inductive unit:Type := tt:unit.

Coq dit que unit est dans Prop. C'est correct parce qu'il n'y a pas de
contraintes d'univers mais un peu déroutant même si la coercion 
"unit : Set" reste valide. Une suggestion est de ne rendre polymorphe
que les inductifs dont on ne donne pas la sorte explicitement, comme dans 

  Inductive unit := tt:unit.

mais alors, comment indiquer l'absence de sorte explicite si le type a
des paramètres réels (comme "vect") ??

PS: modification de sort_cmp dans checker/inductive.ml faite.

--This line, and those below, will be ignored--

M    kernel/univ.ml
M    kernel/univ.mli
M    kernel/inductive.ml
M    kernel/reduction.ml
M    kernel/indtypes.ml
M    checker/inductive.ml
M    checker/reduction.ml
M    pretyping/reductionops.ml
M    pretyping/termops.ml


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10920 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 44 insertions, 51 deletions

diff --git a/checker/inductive.ml b/checker/inductive.ml
index febe312f2..05ab5a846 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -127,7 +127,7 @@ Remark: Set (predicative) is encoded as Type(0)
 
 let sort_as_univ = function
 | Type u -> u
-| Prop Null -> lower_univ
+| Prop Null -> type0m_univ
 | Prop Pos -> type0_univ
 
 let cons_subst u su subst =
@@ -182,7 +182,7 @@ 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_lower_univ level then Prop Null
+  if is_type0m_univ level then Prop Null
   else if is_type0_univ level then Prop Pos
   else Type level
 
@@ -208,7 +208,7 @@ let cumulate_constructor_univ u = function
   | Type u' -> sup u u'
 
 let max_inductive_sort =
-  Array.fold_left cumulate_constructor_univ lower_univ
+  Array.fold_left cumulate_constructor_univ type0m_univ
 
 (************************************************************************)
 (* Type of a constructor *)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 503a1b29a..45a376873 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -145,7 +145,7 @@ type conv_pb =
 
 let sort_cmp univ pb s0 s1 =
   match (s0,s1) with
-    | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
+    | (Prop c1, Prop c2) -> if c1 = Pos & c2 = Null then raise NotConvertible
     | (Prop c1, Type u)  ->
         (match pb with
             CUMUL -> ()
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 764dfcc7b..e9f8f89ad 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -262,7 +262,7 @@ let typecheck_inductive env mie =
 	  Inl (info,full_arity,s), enforce_geq u lev cst
       | Prop Pos when engagement env <> Some ImpredicativeSet ->
 	  (* Predicative set: check that the content is indeed predicative *)
-	  if not (is_lower_univ lev) & not (is_type0_univ lev) then
+	  if not (is_type0m_univ lev) & not (is_type0_univ lev) then
 	    error "Large non-propositional inductive types must be in Type";
 	  Inl (info,full_arity,s), cst
       | Prop _ ->
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2059a1a40..3b64a2c09 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -124,7 +124,7 @@ Remark: Set (predicative) is encoded as Type(0)
 
 let sort_as_univ = function
 | Type u -> u
-| Prop Null -> lower_univ
+| Prop Null -> type0m_univ
 | Prop Pos -> type0_univ
 
 let cons_subst u su subst =
@@ -179,10 +179,12 @@ 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_type0_univ level then set_sort else Type level
-    (* Note: for singleton types, we keep a representative in Type so that
-       predicativity and subtyping in Set applies, even if the resulting type
-       is semantically equivalent to Prop (and indeed convertible to it) *)
+  (* Singleton type not containing types are interpretable in Prop *)
+  if is_type0m_univ level then prop_sort
+  (* Non singleton type not containing types are interpretable in Set *)
+  else if is_type0_univ level then set_sort
+  (* This is a Type with constraints *)
+ else Type level
 
 let type_of_inductive_knowing_parameters env mip paramtyps =
   match mip.mind_arity with
@@ -206,7 +208,7 @@ let cumulate_constructor_univ u = function
   | Type u' -> sup u u'
 
 let max_inductive_sort =
-  Array.fold_left cumulate_constructor_univ lower_univ
+  Array.fold_left cumulate_constructor_univ type0m_univ
 
 (************************************************************************)
 (* Type of a constructor *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index ee93ec291..7a7a12b08 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -153,21 +153,9 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
 
 (* The sort cumulativity is
 
-    Prop, Set <= Type 1 <= ... <= Type i <= ...
+    Prop <= Set <= Type 1 <= ... <= Type i <= ...
 
     and this holds whatever Set is predicative or impredicative
-
-    In addition, there are the following internal sorts:
-    - Type (-1) is semantically equivalent to Prop but with the
-      following syntactic restrictions: 
-      Type (-1) is syntactically predicative and subtype of all Type i
-      Prop is syntactically impredicative and subtype of Type i only for i>=1
-    - Type 0 is semantically equivalent to predicative Set
-    Both Type (-1) and Type 0 can only occur as types of polymorphic 
-    inductive types (in practice Type 0 is systematically converted to Set and
-    we do not see it outside the computation of polymorphic inductive but
-    Type (-1) is kept to avoid setting Prop <= predicative Set in the syntax;
-    this means that (*1*) below can happen).
 *)
 
 type conv_pb = 
@@ -176,14 +164,15 @@ type conv_pb =
 
 let sort_cmp pb s0 s1 cuniv =
   match (s0,s1) with
-    | (Prop c1, Prop c2) -> if c1 = c2 then cuniv else raise NotConvertible
+    | (Prop c1, Prop c2) ->
+        if c1 = Null or c2 = Pos then cuniv   (* Prop <= Set *)
+        else raise NotConvertible
     | (Prop c1, Type u) when pb = CUMUL -> assert (is_univ_variable u); cuniv
     | (Type u1, Type u2) ->
 	assert (is_univ_variable u2);
 	(match pb with
            | CONV -> enforce_eq u1 u2 cuniv
 	   | CUMUL -> enforce_geq u2 u1 cuniv)
-    | (Type u, Prop _) when u = lower_univ & pb = CUMUL -> cuniv    (*1*)
     | (_, _) -> raise NotConvertible
 
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index aa12f0a8b..89b4a2112 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -40,8 +40,8 @@ open Util
  *)
 
 type universe_level =
-  | PredicativeSet
-  | PredicativeLevel of Names.dir_path * int
+  | Set
+  | Level of Names.dir_path * int
 
 type universe =
   | Atom of universe_level
@@ -53,10 +53,10 @@ module UniverseOrdered = struct
 end
 
 let string_of_univ_level = function
-  | PredicativeSet -> "0"
-  | PredicativeLevel (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
+  | Set -> "0"
+  | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
 
-let make_univ (m,n) = Atom (PredicativeLevel (m,n))
+let make_univ (m,n) = Atom (Level (m,n))
 
 let pr_uni_level u = str (string_of_univ_level u)
 
@@ -78,8 +78,6 @@ let pr_uni = function
 let super = function
   | Atom u -> 
       Max ([],[u])
-  | Max ([],[]) -> (* Used for polym. inductive types at the lower level *)
-      Max ([],[PredicativeSet])
   | Max _ ->
       anomaly ("Cannot take the successor of a non variable universe:\n"^
                "(maybe a bugged tactic)")
@@ -128,28 +126,28 @@ let declare_univ u g =
 
 (* The lower predicative level of the hierarchy that contains (impredicative)
    Prop and singleton inductive types *)
-let lower_univ = Max ([],[])
+let type0m_univ = Max ([],[])
 
-let is_lower_univ = function
+let is_type0m_univ = function
   | Max ([],[]) -> true
   | _ -> false
 
 (* The level of predicative Set *)
-let type0_univ = Atom PredicativeSet
+let type0_univ = Atom Set
 
 let is_type0_univ = function
-  | Atom PredicativeSet -> true
-  | Max ([PredicativeSet],[]) -> warning "Non canonical Set"; true
+  | Atom Set -> true
+  | Max ([Set],[]) -> warning "Non canonical Set"; true
   | u -> false
 
 let is_univ_variable = function
-  | Atom a when a<>PredicativeSet -> true
+  | Atom a when a<>Set -> true
   | _ -> false
 
 (* When typing [Prop] and [Set], there is no constraint on the level,
    hence the definition of [type1_univ], the type of [Prop] *)
 
-let type1_univ = Max ([],[PredicativeSet])
+let type1_univ = Max ([],[Set])
 
 let initial_universes = UniverseMap.empty
 
@@ -297,7 +295,7 @@ let check_eq g u v =
 let compare_greater g strict u v =
   let g = declare_univ u g in
   let g = declare_univ v g in
-  if not strict && compare_eq g v PredicativeSet then true else
+  if not strict && compare_eq g v Set then true else
   match compare g v u with
     | (EQ|LE) -> not strict
     | LT -> true
@@ -461,7 +459,7 @@ type constraint_function =
     universe -> universe -> constraints -> constraints
 
 let constraint_add_leq v u c =
-  if v = PredicativeSet then c else Constraint.add (v,Leq,u) c
+  if v = Set then c else Constraint.add (v,Leq,u) c
 
 let enforce_geq u v c =
   match u, v with
@@ -485,7 +483,7 @@ let merge_constraints c g =
 (* Temporary inductive type levels *)
 
 let fresh_level =
-  let n = ref 0 in fun () -> incr n; PredicativeLevel (Names.make_dirpath [],!n)
+  let n = ref 0 in fun () -> incr n; Level (Names.make_dirpath [],!n)
 
 let fresh_local_univ () = Atom (fresh_level ())
 
@@ -612,8 +610,8 @@ module Huniv =
       type t = universe
       type u = Names.dir_path -> Names.dir_path
       let hash_aux hdir = function
-	| PredicativeSet -> PredicativeSet
-	| PredicativeLevel (d,n) -> PredicativeLevel (hdir d,n)
+	| Set -> Set
+	| Level (d,n) -> Level (hdir d,n)
       let hash_sub hdir = function
 	| Atom u -> Atom (hash_aux hdir u)
 	| Max (gel,gtl) ->
diff --git a/kernel/univ.mli b/kernel/univ.mli
index ce25afb26..e2594e217 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -12,13 +12,17 @@
 
 type universe
 
-val type0_univ : universe  (* predicative Set seen as a universe *)
+(* The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... *)
+(* Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
+
+val type0m_univ : universe  (* image of Prop in the universes hierarchy *)
+val type0_univ : universe  (* image of Set in the universes hierarchy *)
 val type1_univ : universe  (* the universe of the type of Prop/Set *)
-val lower_univ : universe  (* image of Prop in the predicative hierarchy *)
+
 val make_univ : Names.dir_path * int -> universe
 
 val is_type0_univ : universe -> bool
-val is_lower_univ : universe -> bool
+val is_type0m_univ : universe -> bool
 val is_univ_variable : universe -> bool
 
 (* The type of a universe *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index d6bc6eb71..55b82e214 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -615,10 +615,10 @@ let sort_cmp = sort_cmp
 
 let base_sort_cmp pb s0 s1 =
   match (s0,s1) with
-    | (Prop c1, Prop c2) -> c1 = c2
+    | (Prop c1, Prop c2) -> c1 = Null or c2 = Pos  (* Prop <= Set *)
     | (Prop c1, Type u)  -> pb = CUMUL
     | (Type u1, Type u2) -> true
-    | (Type u, Prop _) -> u = lower_univ & pb = CUMUL
+    | _ -> false
 
 
 let test_conversion f env sigma x y =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 227a4f9ed..cb6146338 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -163,7 +163,7 @@ let new_Type_sort () = Type (new_univ ())
 let refresh_universes_gen strict t =
   let modified = ref false in
   let rec refresh t = match kind_of_term t with
-    | Sort (Type u) when strict or u <> Univ.lower_univ ->
+    | Sort (Type u) when strict or u <> Univ.type0m_univ ->
 	modified := true; new_Type ()
     | Prod (na,u,v) -> mkProd (na,u,refresh v)
     | _ -> t in