Forcing i > Set for global universes (incomplete)

5 files changed, 49 insertions, 32 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 109e3830c2..c433c07898 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -181,26 +181,41 @@ let fold_named_context_reverse f ~init env =
 
 (* Universe constraints *)
 
-let add_constraints c env =
-  if Univ.Constraint.is_empty c then
-    env
-  else
-    let s = env.env_stratification in
+let map_universes f env =
+  let s = env.env_stratification in
     { env with env_stratification =
-      { s with env_universes = Univ.merge_constraints c s.env_universes } }
+	 { s with env_universes = f s.env_universes } }
+				     
+let add_constraints c env =
+  if Univ.Constraint.is_empty c then env
+  else map_universes (Univ.merge_constraints c) env
 
 let check_constraints c env =
   Univ.check_constraints c env.env_stratification.env_universes
 
-let set_engagement c env = (* Unsafe *)
-  { env with env_stratification =
-    { env.env_stratification with env_engagement = c } }
-
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
 
-let push_context ctx env = add_constraints (Univ.UContext.constraints ctx) env
-let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx) env
+let add_universes strict ctx g =
+  let g = Array.fold_left (fun g v -> Univ.add_universe v strict g)
+			  g (Univ.Instance.to_array (Univ.UContext.instance ctx))
+  in
+    Univ.merge_constraints (Univ.UContext.constraints ctx) g
+			   
+let push_context ?(strict=false) ctx env =
+  map_universes (add_universes strict ctx) env
+
+let add_universes_set strict ctx g =
+  let g = Univ.LSet.fold (fun v g -> Univ.add_universe v strict g)
+			 (Univ.ContextSet.levels ctx) g
+  in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g
+
+let push_context_set ?(strict=false) ctx env =
+  map_universes (add_universes_set strict ctx) env
+
+let set_engagement c env = (* Unsafe *)
+  { env with env_stratification =
+    { env.env_stratification with env_engagement = c } }
 
 (* Global constants *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4ad0327fc7..9f6ea522a7 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -208,8 +208,8 @@ val add_constraints : Univ.constraints -> env -> env
 
 (** Check constraints are satifiable in the environment. *)
 val check_constraints : Univ.constraints -> env -> bool
-val push_context : Univ.universe_context -> env -> env
-val push_context_set : Univ.universe_context_set -> env -> env
+val push_context : ?strict:bool -> Univ.universe_context -> env -> env
+val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
 val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
 val set_engagement : engagement -> env -> env
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 83e566041f..e89b6ef8f7 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -100,11 +100,11 @@ let hcons_j j =
 
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-
+	      
 let infer_declaration env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
-      let env = push_context uctx env in
+      let env = push_context ~strict:(not poly) uctx env in
       let j = infer env t in
       let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract uctx in
@@ -115,7 +115,7 @@ let infer_declaration env kn dcl =
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
 		       const_entry_polymorphic = false} as c) ->
-      let env = push_context c.const_entry_universes env in
+      let env = push_context ~strict:true c.const_entry_universes env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
@@ -135,7 +135,7 @@ let infer_declaration env kn dcl =
 	c.const_entry_inline_code, c.const_entry_secctx
 
   | DefinitionEntry c ->
-      let env = push_context c.const_entry_universes env in
+      let env = push_context ~strict:(not c.const_entry_polymorphic) c.const_entry_universes env in
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 040e9bc270..b61b441d2e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -750,17 +750,6 @@ let get_set_arc g = repr g Level.set
 let is_set_arc u = Level.is_set u.univ
 let is_prop_arc u = Level.is_prop u.univ
 
-let add_universe vlev ~predicative g = 
-  let v = terminal ~predicative vlev in
-  let arc =
-    let arc =
-      if predicative then get_set_arc g else get_prop_arc g
-    in
-      { arc with le=vlev::arc.le}
-  in
-  let g = enter_arc arc g in
-    enter_arc v g
-
 (* [safe_repr] also search for the canonical representative, but
    if the graph doesn't contain the searched universe, we add it. *)
 
@@ -777,6 +766,18 @@ let safe_repr g u =
     let g = enter_arc {setarc with le=u::setarc.le} g in
     enter_arc can g, can
 
+let add_universe vlev strict g = 
+  let v = terminal ~predicative:true vlev in
+  let arc =
+    let arc = get_set_arc g in
+      if strict then
+	{ arc with lt=vlev::arc.lt}
+      else 
+	{ arc with le=vlev::arc.le}
+  in
+  let g = enter_arc arc g in
+    enter_arc v g
+
 (* reprleq : canonical_arc -> canonical_arc list *)
 (* All canonical arcv such that arcu<=arcv with arcv#arcu *)
 let reprleq g arcu =
@@ -1145,7 +1146,8 @@ let merge g arcu arcv =
   (* we find the arc with the biggest rank, and we redirect all others to it *)
   let arcu, g, v =
     let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
-      if arc.rank >= max_rank && not (Level.is_small best_arc.univ)
+      if Level.is_small arc.univ ||
+	   (arc.rank >= max_rank && not (Level.is_small best_arc.univ))
       then (arc.rank, max_rank, arc, best_arc::rest)
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 76453cbb08..fe7fc1ab9f 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -163,8 +163,8 @@ val is_initial_universes : universes -> bool
 
 val sort_universes : universes -> universes
 
-(** Adds a universe to the graph, ensuring it is >= Prop or Set. *)
-val add_universe : universe_level -> predicative:bool -> universes -> universes
+(** Adds a universe to the graph, ensuring it is >= or > Set. *)
+val add_universe : universe_level -> bool -> universes -> universes
 
 (** {6 Constraints. } *)