From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Sat, 1 Apr 2017 17:35:39 +0200
Subject: Using UInfoInd for universes in inductive types

It stores both universe constraints and subtyping information for
blocks of inductive declarations.

At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.
---
 kernel/safe_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f5e8e86530..1568fe0bf2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -429,7 +429,7 @@ let globalize_mind_universes mb =
   if mb.mind_polymorphic then
     [Now (true, Univ.ContextSet.empty)]
   else
-    [Now (false, Univ.ContextSet.of_context mb.mind_universes)]
+    [Now (false, Univ.ContextSet.of_context (Univ.UInfoInd.univ_context mb.mind_universes))]
 
 let constraints_of_sfb env sfb = 
   match sfb with
-- 
cgit v1.2.3


From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 kernel/safe_typing.ml | 79 ++++++++++++++++++++++++++++++---------------------
 1 file changed, 47 insertions(+), 32 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1568fe0bf2..946222ef2f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -237,20 +237,29 @@ let private_con_of_scheme ~kind env cl =
 
 let universes_of_private eff =
   let open Declarations in
-  List.fold_left (fun acc { Entries.eff } ->
-     match eff with
-     | Entries.SEscheme (l,s) ->
-        List.fold_left (fun acc (_,_,cb,c) ->
-          let acc = match c with
-            | `Nothing -> acc
-            | `Opaque (_, ctx) -> ctx :: acc in
-          if cb.const_polymorphic then acc
-          else (Univ.ContextSet.of_context cb.const_universes) :: acc)
-        acc l
-     | Entries.SEsubproof (c, cb, e) ->
-	if cb.const_polymorphic then acc
-	else Univ.ContextSet.of_context cb.const_universes :: acc)
-   [] (Term_typing.uniq_seff eff)
+  List.fold_left
+    (fun acc { Entries.eff } ->
+       match eff with
+       | Entries.SEscheme (l,s) ->
+         List.fold_left
+           (fun acc (_,_,cb,c) ->
+              let acc = match c with
+                | `Nothing -> acc
+                | `Opaque (_, ctx) -> ctx :: acc
+              in
+              match cb.const_universes with
+              | Monomorphic_const ctx ->
+                (Univ.ContextSet.of_context 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
+              | Polymorphic_const _ -> acc
+    )
+    [] (Term_typing.uniq_seff eff)
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
@@ -373,7 +382,11 @@ let safe_push_named d env =
 
 
 let push_named_def (id,de) senv =
-  let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
+  let c,typ,univs = 
+    match Term_typing.translate_local_def senv.revstruct senv.env id de with
+    | c, typ, Monomorphic_const ctx -> c, typ, ctx
+    | _, _, Polymorphic_const _ -> assert false
+  in
   let poly = de.Entries.const_entry_polymorphic in
   let univs = Univ.ContextSet.of_context univs in
   let c, univs = match c with
@@ -410,26 +423,28 @@ let labels_of_mib mib =
   get ()
 
 let globalize_constant_universes env cb =
-  if cb.const_polymorphic then
-    [Now (true, Univ.ContextSet.empty)]
-  else
-    let cstrs = Univ.ContextSet.of_context cb.const_universes in
-      Now (false, cstrs) ::  
-	(match cb.const_body with
-	| (Undef _ | Def _) -> []
-	| OpaqueDef lc ->
-	  match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with
-	  | None -> []
-	  | Some fc ->
+  match cb.const_universes with
+  | Monomorphic_const ctx ->
+    let cstrs = Univ.ContextSet.of_context ctx in
+    Now (false, cstrs) ::  
+    (match cb.const_body with
+     | (Undef _ | Def _) -> []
+     | OpaqueDef lc ->
+       match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with
+       | None -> []
+       | Some fc ->
             match Future.peek_val fc with
-            | None -> [Later fc]
-            | Some c -> [Now (false, c)])
+             | None -> [Later fc]
+             | Some c -> [Now (false, c)])
+  | Polymorphic_const _ ->
+    [Now (true, Univ.ContextSet.empty)]
       
 let globalize_mind_universes mb =
-  if mb.mind_polymorphic then
-    [Now (true, Univ.ContextSet.empty)]
-  else
-    [Now (false, Univ.ContextSet.of_context (Univ.UInfoInd.univ_context mb.mind_universes))]
+  match mb.mind_universes with
+  | Monomorphic_ind ctx ->
+    [Now (false, Univ.ContextSet.of_context ctx)]
+  | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)]
+  | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)]
 
 let constraints_of_sfb env sfb = 
   match sfb with
-- 
cgit v1.2.3