Add a non-cumulative impredicative universe SProp.

Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.

8 files changed, 24 insertions, 7 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index c7b092b114..521d6b707d 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -48,6 +48,7 @@ type 'a puniverses = 'a * EInstance.t
 
 let in_punivs a = (a, EInstance.empty)
 
+let mkSProp = of_kind (Sort (ESorts.make Sorts.sprop))
 let mkProp = of_kind (Sort (ESorts.make Sorts.prop))
 let mkSet = of_kind (Sort (ESorts.make Sorts.set))
 let mkType u = of_kind (Sort (ESorts.make (Sorts.sort_of_univ u)))
@@ -81,6 +82,8 @@ let mkRef (gr,u) = let open GlobRef in match gr with
   | ConstructRef c -> mkConstructU (c,u)
   | VarRef x -> mkVar x
 
+let type1 = mkSort Sorts.type1
+
 let applist (f, arg) = mkApp (f, Array.of_list arg)
 let applistc f arg = mkApp (f, Array.of_list arg)
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 2f4cf7d5d0..6a144be6b3 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -104,6 +104,7 @@ val mkVar : Id.t -> t
 val mkMeta : metavariable -> t
 val mkEvar : t pexistential -> t
 val mkSort : Sorts.t -> t
+val mkSProp : t
 val mkProp : t
 val mkSet  : t
 val mkType : Univ.Universe.t -> t
@@ -128,6 +129,8 @@ val mkInt : Uint63.t -> t
 
 val mkRef : GlobRef.t * EInstance.t -> t
 
+val type1 : t
+
 val applist : t * t list -> t
 val applistc : t -> t list -> t
 
diff --git a/engine/evd.ml b/engine/evd.ml
index b8c52b27df..b89222cf8e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -962,7 +962,7 @@ let normalize_universe_instance evd l =
 
 let normalize_sort evars s =
   match s with
-  | Prop | Set -> s
+  | SProp | Prop | Set -> s
   | Type u -> 
     let u' = normalize_universe evars u in
     if u' == u then s else Sorts.sort_of_univ u'
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 7ef4108c22..46fdf08e10 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -136,6 +136,7 @@ let lowercase_first_char id = (* First character of a constr *)
         s ^ Unicode.lowercase_first_char s'
 
 let sort_hdchar = function
+  | SProp -> "P"
   | Prop -> "P"
   | Set -> "S"
   | Type _ -> "T"
diff --git a/engine/termops.ml b/engine/termops.ml
index 2f766afaa6..9c4b64b60d 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1098,7 +1098,8 @@ let is_template_polymorphic_ind env sigma f =
 
 let base_sort_cmp pb s0 s1 =
   match (s0,s1) with
-  | Prop, Prop | Set, Set | Type _, Type _ -> true
+  | SProp, SProp | Prop, Prop | Set, Set | Type _, Type _ -> true
+  | SProp, _ | _, SProp -> false
   | Prop, Set | Prop, Type _ | Set, Type _ -> pb == Reduction.CUMUL
   | Set, Prop | Type _, Prop | Type _, Set -> false
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 77d1896683..6f4f40e2c5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -37,18 +37,25 @@ type t =
    uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
    uctx_weak_constraints : UPairSet.t
  }
-  
+
+let initial_sprop_cumulative = UGraph.make_sprop_cumulative UGraph.initial_universes
+
 let empty =
   { uctx_names = UNameMap.empty, LMap.empty;
     uctx_local = ContextSet.empty;
     uctx_seff_univs = LSet.empty;
     uctx_univ_variables = LMap.empty;
     uctx_univ_algebraic = LSet.empty;
-    uctx_universes = UGraph.initial_universes;
-    uctx_initial_universes = UGraph.initial_universes;
+    uctx_universes = initial_sprop_cumulative;
+    uctx_initial_universes = initial_sprop_cumulative;
     uctx_weak_constraints = UPairSet.empty; }
 
+let elaboration_sprop_cumul =
+  Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration"
+    ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true
+
 let make u =
+  let u = if elaboration_sprop_cumul () then UGraph.make_sprop_cumulative u else u in
     { empty with 
       uctx_universes = u; uctx_initial_universes = u}
 
@@ -710,7 +717,7 @@ let universe_of_name uctx s =
   UNameMap.find s (fst uctx.uctx_names)
 
 let update_sigma_env uctx env =
-  let univs = Environ.universes env in
+  let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
   let eunivs =
     { uctx with uctx_initial_universes = univs;
                          uctx_universes = univs }
diff --git a/engine/univGen.ml b/engine/univGen.ml
index 4ad7fccb3a..c310331b15 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -128,6 +128,7 @@ let type_of_reference env r =
 let type_of_global t = type_of_reference (Global.env ()) t
 
 let fresh_sort_in_family = function
+  | InSProp -> Sorts.sprop, ContextSet.empty
   | InProp -> Sorts.prop, ContextSet.empty
   | InSet -> Sorts.set, ContextSet.empty
   | InType ->
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 1619ac3d34..46ff6340b4 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -268,6 +268,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 module UPairs = OrderedType.UnorderedPair(Univ.Level)
 module UPairSet = Set.Make (UPairs)
 
+(* TODO check is_small/sprop *)
 let normalize_context_set g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   (* Keep the Prop/Set <= i constraints separate for minimization *)
@@ -275,7 +276,7 @@ let normalize_context_set g ctx us algs weak =
     Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts
   in
   let smallles = if get_set_minimization ()
-    then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles
+    then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles
     else Constraint.empty
   in
   let csts, partition =