From bba897d5fd964bef0aa10102ef41cee1ac5fc3bb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 12 May 2008 10:19:32 +0000
Subject: 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
---
 kernel/inductive.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2059a1a409..3b64a2c09c 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 *)
-- 
cgit v1.2.3