Merge PR #1033: Universe binder improvements

11 files changed, 67 insertions, 56 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index b95796fd8..d5312c500 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -63,7 +63,7 @@ type constant_def =
   | OpaqueDef of Opaqueproof.opaque       (** or an opaque global definition *)
 
 type constant_universes =
-  | Monomorphic_const of Univ.UContext.t
+  | Monomorphic_const of Univ.ContextSet.t
   | Polymorphic_const of Univ.AUContext.t
 
 (** The [typing_flags] are instructions to the type-checker which
@@ -168,9 +168,9 @@ type one_inductive_body = {
   }
 
 type abstract_inductive_universes =
-  | Monomorphic_ind of Univ.UContext.t
+  | Monomorphic_ind of Univ.ContextSet.t
   | Polymorphic_ind of Univ.AUContext.t
-  | Cumulative_ind  of Univ.ACumulativityInfo.t
+  | Cumulative_ind of Univ.ACumulativityInfo.t
 
 type mutual_inductive_body = {
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index f5c26b33d..d8768a0fc 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -126,7 +126,7 @@ let hcons_const_def = function
 let hcons_const_universes cbu =
   match cbu with
   | Monomorphic_const ctx -> 
-    Monomorphic_const (Univ.hcons_universe_context ctx)
+    Monomorphic_const (Univ.hcons_universe_context_set ctx)
   | Polymorphic_const ctx -> 
     Polymorphic_const (Univ.hcons_abstract_universe_context ctx)
 
@@ -274,7 +274,7 @@ let hcons_mind_packet oib =
 
 let hcons_mind_universes miu =
   match miu with
-  | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context ctx)
+  | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context_set ctx)
   | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx)
   | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui)
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 185dba409..c44a17df2 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -35,9 +35,9 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 *)
 
 type inductive_universes =
-  | Monomorphic_ind_entry of Univ.UContext.t
+  | Monomorphic_ind_entry of Univ.ContextSet.t
   | Polymorphic_ind_entry of Univ.UContext.t
-  | Cumulative_ind_entry  of Univ.CumulativityInfo.t
+  | Cumulative_ind_entry of Univ.CumulativityInfo.t
 
 type one_inductive_entry = {
   mind_entry_typename : Id.t;
@@ -65,9 +65,11 @@ type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
 type constant_universes_entry =
-  | Monomorphic_const_entry of Univ.UContext.t
+  | Monomorphic_const_entry of Univ.ContextSet.t
   | Polymorphic_const_entry of Univ.UContext.t
 
+type 'a in_constant_universes_entry = 'a * constant_universes_entry
+
 type 'a definition_entry = {
   const_entry_body   : 'a const_entry_body;
   (* List of section variables *)
@@ -82,7 +84,7 @@ type 'a definition_entry = {
 type inline = int option (* inlining level, None for no inlining *)
 
 type parameter_entry = 
-    Context.Named.t option * bool * types Univ.in_universe_context * inline 
+    Context.Named.t option * types in_constant_universes_entry * inline
 
 type projection_entry = {
   proj_entry_ind : MutInd.t;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 083b0ae40..8e9b606a5 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -265,13 +265,12 @@ let typecheck_inductive env mie =
   (* Check unicity of names *)
   mind_check_names mie;
   (* Params are typed-checked here *)
-  let univctx =
+  let env' =
     match mie.mind_entry_universes with
-    | Monomorphic_ind_entry ctx -> ctx
-    | Polymorphic_ind_entry ctx -> ctx
-    | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi
+    | Monomorphic_ind_entry ctx -> push_context_set ctx env
+    | Polymorphic_ind_entry ctx -> push_context ctx env
+    | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
   in
-  let env' = push_context univctx env in
   let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in
   (* We first type arity of each inductive definition *)
   (* This allows building the environment of arities and to share *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 8568bf14b..f7e755f00 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -79,18 +79,20 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
               environment, because they do not appear in the type of the
               definition. Any inconsistency will be raised at a later stage
               when joining the environment. *)
-	  let env' = Environ.push_context ~strict:true ctx env' in
-	  let c',cst = match cb.const_body with
-	    | Undef _ | OpaqueDef _ ->
-	      let j = Typeops.infer env' c in
-	      let typ = cb.const_type in
-	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
-						j.uj_type typ in
-	      j.uj_val, cst'
-	    | Def cs ->
-	       let c' = Mod_subst.force_constr cs in
-	         c, Reduction.infer_conv env' (Environ.universes env') c c'
-	  in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
+          let env' = Environ.push_context ~strict:true ctx env' in
+          let c',cst = match cb.const_body with
+            | Undef _ | OpaqueDef _ ->
+              let j = Typeops.infer env' c in
+              let typ = cb.const_type in
+              let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+                  j.uj_type typ in
+              j.uj_val, cst'
+            | Def cs ->
+              let c' = Mod_subst.force_constr cs in
+              c, Reduction.infer_conv env' (Environ.universes env') c c'
+          in
+          let ctx = Univ.ContextSet.of_context ctx in
+          c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx
         | Polymorphic_const uctx ->
           let subst, ctx = Univ.abstract_universes ctx in
           let c = Vars.subst_univs_level_constr subst c in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0e416b3e5..0e41bfc3c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -249,14 +249,14 @@ let universes_of_private eff =
               in
               match cb.const_universes with
               | Monomorphic_const ctx ->
-                (Univ.ContextSet.of_context ctx) :: acc
+                ctx :: acc
               | Polymorphic_const _ -> acc
            )
            acc l
        | Entries.SEsubproof (c, cb, e) ->
          match cb.const_universes with
               | Monomorphic_const ctx ->
-                (Univ.ContextSet.of_context ctx) :: acc
+                ctx :: acc
               | Polymorphic_const _ -> acc
     )
     [] (Term_typing.uniq_seff eff)
@@ -389,7 +389,6 @@ let push_named_def (id,de) senv =
   | Monomorphic_const_entry _ -> false
   | Polymorphic_const_entry _ -> true
   in
-  let univs = Univ.ContextSet.of_context univs in
   let c, univs = match c with
     | Def c -> Mod_subst.force_constr c, univs
     | OpaqueDef o ->
@@ -425,9 +424,8 @@ let labels_of_mib mib =
 
 let globalize_constant_universes env cb =
   match cb.const_universes with
-  | Monomorphic_const ctx ->
-    let cstrs = Univ.ContextSet.of_context ctx in
-    Now (false, cstrs) ::  
+  | Monomorphic_const cstrs ->
+    Now (false, cstrs) ::
     (match cb.const_body with
      | (Undef _ | Def _) -> []
      | OpaqueDef lc ->
@@ -443,7 +441,7 @@ let globalize_constant_universes env cb =
 let globalize_mind_universes mb =
   match mb.mind_universes with
   | Monomorphic_ind ctx ->
-    [Now (false, Univ.ContextSet.of_context ctx)]
+    [Now (false, ctx)]
   | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)]
   | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)]
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 4617f2d5f..70dd6438d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -125,11 +125,10 @@ let inline_side_effects env body ctx side_eff =
       | _ -> assert false
       in
       match cb.const_universes with
-      | Monomorphic_const cnstctx ->
+      | Monomorphic_const univs ->
         (** Abstract over the term at the top of the proof *)
         let ty = cb.const_type in
         let subst = Cmap_env.add c (Inr var) subst in
-        let univs = Univ.ContextSet.of_context cnstctx in
         let ctx = Univ.ContextSet.union ctx univs in
         (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
       | Polymorphic_const auctx ->
@@ -228,19 +227,25 @@ let feedback_completion_typecheck =
   Option.iter (fun state_id ->
       feedback ~id:state_id Feedback.Complete)
 
-let abstract_constant_universes abstract uctx =
-  if not abstract then
+let abstract_constant_universes abstract = function
+  | Monomorphic_const_entry uctx ->
     Univ.empty_level_subst, Monomorphic_const uctx
-  else
-    let sbst, auctx = Univ.abstract_universes uctx in
-    sbst, Polymorphic_const auctx
+  | Polymorphic_const_entry uctx ->
+    if not abstract then
+      Univ.empty_level_subst, Monomorphic_const (Univ.ContextSet.of_context uctx)
+    else
+      let sbst, auctx = Univ.abstract_universes uctx in
+      sbst, Polymorphic_const auctx
 
 let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) =
   match dcl with
-  | ParameterEntry (ctx,poly,(t,uctx),nl) ->
-      let env = push_context ~strict:(not poly) uctx env in
+    | ParameterEntry (ctx,(t,uctx),nl) ->
+      let env = match uctx with
+        | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env
+        | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env
+      in
       let j = infer env t in
-      let abstract = poly && not (Option.is_empty kn) in
+      let abstract = not (Option.is_empty kn) in
       let usubst, univs = 
         abstract_constant_universes abstract uctx
       in
@@ -262,7 +267,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
 		       const_entry_universes = Monomorphic_const_entry univs } as c) ->
-      let env = push_context ~strict:true univs env in
+      let env = push_context_set ~strict:true univs env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
@@ -301,21 +306,22 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       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
-      let poly, univs = match c.const_entry_universes with
+      let poly, univsctx = match c.const_entry_universes with
       | Monomorphic_const_entry univs -> false, univs
-      | Polymorphic_const_entry univs -> true, univs
+      | Polymorphic_const_entry univs -> true, Univ.ContextSet.of_context univs
       in
-      let univsctx = Univ.ContextSet.of_context univs in
       let ctx = Univ.ContextSet.union univsctx ctx in
       let body, ctx, _ = match trust with
       | Pure -> body, ctx, []
       | SideEffects _ -> inline_side_effects env body ctx side_eff
       in
       let env = push_context_set ~strict:(not poly) ctx env in
-      let abstract = poly && not (Option.is_empty kn) in
-      let usubst, univs =
-        abstract_constant_universes abstract (Univ.ContextSet.to_context ctx)
-      in      
+      let abstract = not (Option.is_empty kn) in
+      let ctx = if poly
+        then Polymorphic_const_entry (Univ.ContextSet.to_context ctx)
+        else Monomorphic_const_entry ctx
+      in
+      let usubst, univs = abstract_constant_universes abstract ctx in
       let j = infer env body in
       let typ = match typ with
         | None ->
@@ -556,7 +562,7 @@ let export_side_effects mb env ce =
             let env = Environ.add_constant kn cb env in
             match cb.const_universes with
             | Monomorphic_const ctx ->
-              Environ.push_context ~strict:true ctx env
+              Environ.push_context_set ~strict:true ctx env
             | Polymorphic_const _ -> env
           end
         | kn, cb, `Opaque(_, ctx), _ ->
@@ -564,7 +570,7 @@ let export_side_effects mb env ce =
             let env = Environ.add_constant kn cb env in
             match cb.const_universes with
             | Monomorphic_const cstctx ->
-              let env = Environ.push_context ~strict:true cstctx env in
+              let env = Environ.push_context_set ~strict:true cstctx env in
               Environ.push_context_set ~strict:true ctx env
             | Polymorphic_const _ -> env
           end
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 9b35bfc6e..55da4197e 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -19,7 +19,7 @@ type _ trust =
 | SideEffects : structure_body -> side_effects trust
 
 val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry ->
-  constant_def * types * Univ.UContext.t
+  constant_def * types * Univ.ContextSet.t
 
 val translate_local_assum : env -> types -> types
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7fe4f8274..64afb95d5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1053,6 +1053,7 @@ struct
   let constraints (univs, cst) = cst
   let levels (univs, cst) = univs
 
+  let size (univs,_) = LSet.cardinal univs
 end
 
 type universe_context_set = ContextSet.t
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 8d46a8bee..c06ce2446 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -310,7 +310,7 @@ sig
   (** Keeps the order of the instances *)
   val union : t -> t -> t
 
-  (* the number of universes in the context *)
+  (** the number of universes in the context *)
   val size : t -> int
 
 end
@@ -423,6 +423,9 @@ sig
 
   val constraints : t -> constraints
   val levels : t -> LSet.t
+
+  (** the number of universes in the context *)
+  val size : t -> int
 end
 
 (** A set of universes with universe constraints.
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 0e452621c..578a89371 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
         let mib = Environ.lookup_mind mi env in
 	let ulen = 
           match mib.Declarations.mind_universes with
-          | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx
+          | Declarations.Monomorphic_ind ctx -> Univ.ContextSet.size ctx
           | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx
           | Declarations.Cumulative_ind cumi -> 
             Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)