From 35fba70509d9fb219b2a88f8e7bd246b2671b39b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 9 Nov 2017 17:27:58 +0100
Subject: Simplification: cumulativity information is variance information.

Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.

As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).

Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie

         Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
         Print Foo.

gives

        Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
          { foo : Type@{i} -> Type@{j} }
          (* =i +j *k |=  *)
---
 interp/discharge.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/discharge.ml b/interp/discharge.ml
index 75bfca3078..710f88c3ff 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -92,7 +92,7 @@ let process_inductive info modlist mib =
       let auctx = Univ.ACumulativityInfo.univ_context cumi in
       let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
       let auctx = Univ.AUContext.repr auctx in
-      subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx)
+      subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx)
   in
   let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
   let inds =
-- 
cgit v1.2.3


From 1ed0836a7e0c8e05b0288f85e344ef5249d5d228 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 10 Nov 2017 13:23:32 +0100
Subject: Inference of inductive subtyping does not need an evar map.

---
 interp/declare.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index 55f825c251..0bfc9060b8 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -364,13 +364,8 @@ let infer_inductive_subtyping (pth, mind_ent) =
   | Cumulative_ind_entry cumi ->
     begin
       let env = Global.env () in
-      let env' =
-        Environ.push_context
-          (Univ.CumulativityInfo.univ_context cumi) env
-      in
       (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
-      let evd = Evd.from_env env' in
-        (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent)
+        (pth, Inductiveops.infer_inductive_subtyping env mind_ent)
     end
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
-- 
cgit v1.2.3


From 6c2d10b93b819f0735a43453c78566795de8ba5a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 10 Nov 2017 15:05:21 +0100
Subject: Use specialized function for inductive subtyping inference.

This ensures by construction that we never infer constraints outside
the variance model.
---
 interp/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index 0bfc9060b8..72cdabfd20 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -365,7 +365,7 @@ let infer_inductive_subtyping (pth, mind_ent) =
     begin
       let env = Global.env () in
       (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
-        (pth, Inductiveops.infer_inductive_subtyping env mind_ent)
+        (pth, InferCumulativity.infer_inductive env mind_ent)
     end
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
-- 
cgit v1.2.3