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.

1 files changed, 51 insertions, 24 deletions

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 8187dea41b..0d5b55ca1b 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -29,15 +29,22 @@ module G = AcyclicGraph.Make(struct
    code (eg add_universe with a constraint vs G.add with no
    constraint) *)
 
-type t = G.t
-type 'a check_function = 'a G.check_function
+type t = { graph: G.t; sprop_cumulative : bool }
+type 'a check_function = t -> 'a -> 'a -> bool
+
+let g_map f g =
+  let g' = f g.graph in
+  if g.graph == g' then g
+  else {g with graph=g'}
+
+let make_sprop_cumulative g = {g with sprop_cumulative=true}
 
 let check_smaller_expr g (u,n) (v,m) =
   let diff = n - m in
     match diff with
-    | 0 -> G.check_leq g u v
-    | 1 -> G.check_lt g u v
-    | x when x < 0 -> G.check_leq g u v
+    | 0 -> G.check_leq g.graph u v
+    | 1 -> G.check_lt g.graph u v
+    | x when x < 0 -> G.check_leq g.graph u v
     | _ -> false
 
 let exists_bigger g ul l =
@@ -48,24 +55,28 @@ let real_check_leq g u v =
   Universe.for_all (fun ul -> exists_bigger g ul v) u
 
 let check_leq g u v =
-  Universe.equal u v ||
-    is_type0m_univ u ||
-    real_check_leq g u v
+  Universe.equal u v || (g.sprop_cumulative && Universe.is_sprop u) ||
+  (not (Universe.is_sprop u) && not (Universe.is_sprop v) &&
+    (is_type0m_univ u ||
+     real_check_leq g u v))
 
 let check_eq g u v =
   Universe.equal u v ||
-  (real_check_leq g u v && real_check_leq g v u)
+  (not (Universe.is_sprop u || Universe.is_sprop v) &&
+   (real_check_leq g u v && real_check_leq g v u))
 
-let check_eq_level = G.check_eq
+let check_eq_level g u v =
+  u == v ||
+  (not (Level.is_sprop u || Level.is_sprop v) && G.check_eq g.graph u v)
 
-let empty_universes = G.empty
+let empty_universes = {graph=G.empty; sprop_cumulative=false}
 
 let initial_universes =
   let big_rank = 1000000 in
   let g = G.empty in
   let g = G.add ~rank:big_rank Level.prop g in
   let g = G.add ~rank:big_rank Level.set g in
-  G.enforce_lt Level.prop Level.set g
+  {graph=G.enforce_lt Level.prop Level.set g; sprop_cumulative=false}
 
 let enforce_constraint (u,d,v) g =
   match d with
@@ -73,6 +84,13 @@ let enforce_constraint (u,d,v) g =
   | Lt -> G.enforce_lt u v g
   | Eq -> G.enforce_eq u v g
 
+let enforce_constraint (u,d,v as cst) g =
+  match Level.is_sprop u, d, Level.is_sprop v with
+  | false, _, false -> g_map (enforce_constraint cst) g
+  | true, (Eq|Le), true -> g
+  | true, Le, false when g.sprop_cumulative -> g
+  | _ ->  raise (UniverseInconsistency (d,Universe.make u, Universe.make v, None))
+
 let merge_constraints csts g = Constraint.fold enforce_constraint csts g
 
 let check_constraint g (u,d,v) =
@@ -81,6 +99,13 @@ let check_constraint g (u,d,v) =
   | Lt -> G.check_lt g u v
   | Eq -> G.check_eq g u v
 
+let check_constraint g (u,d,v as cst) =
+  match Level.is_sprop u, d, Level.is_sprop v with
+  | false, _, false -> check_constraint g.graph cst
+  | true, (Eq|Le), true -> true
+  | true, Le, false -> g.sprop_cumulative
+  | _ -> false
+
 let check_constraints csts g = Constraint.for_all (check_constraint g) csts
 
 let leq_expr (u,m) (v,n) =
@@ -125,17 +150,17 @@ let enforce_leq_alg u v g =
 
 exception AlreadyDeclared = G.AlreadyDeclared
 let add_universe u strict g =
-  let g = G.add u g in
+  let graph = G.add u g.graph in
   let d = if strict then Lt else Le in
-  enforce_constraint (Level.set,d,u) g
+  enforce_constraint (Level.set,d,u) {g with graph}
 
-let add_universe_unconstrained u g = G.add u g
+let add_universe_unconstrained u g = {g with graph=G.add u g.graph}
 
 exception UndeclaredLevel = G.Undeclared
-let check_declared_universes = G.check_declared
+let check_declared_universes g l = G.check_declared g.graph (LSet.remove Level.sprop l)
 
-let constraints_of_universes = G.constraints_of
-let constraints_for = G.constraints_for
+let constraints_of_universes g = G.constraints_of g.graph
+let constraints_for ~kept g = G.constraints_for ~kept:(LSet.remove Level.sprop kept) g.graph
 
 (** Subtyping of polymorphic contexts *)
 
@@ -160,18 +185,20 @@ let check_eq_instances g t1 t2 =
           (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1))
         in aux 0)
 
-let domain = G.domain
-let choose = G.choose
+let domain g = LSet.add Level.sprop (G.domain g.graph)
+let choose p g u = if Level.is_sprop u
+  then if p u then Some u else None
+  else G.choose p g.graph u
 
-let dump_universes = G.dump
+let dump_universes f g = G.dump f g.graph
 
-let check_universes_invariants g = G.check_invariants ~required_canonical:Level.is_small g
+let check_universes_invariants g = G.check_invariants ~required_canonical:Level.is_small g.graph
 
-let pr_universes = G.pr
+let pr_universes prl g = G.pr prl g.graph
 
 let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"]
 let make_dummy i = Level.(make (UGlobal.make dummy_mp i))
-let sort_universes g = G.sort make_dummy [Level.prop;Level.set] g
+let sort_universes g = g_map (G.sort make_dummy [Level.prop;Level.set]) g
 
 (** Profiling *)