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

1 files changed, 4 insertions, 15 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index ee93ec2911..7a7a12b08f 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