From b641379bb1ce569e46f39e16736640a4223a5758 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 6 Nov 2017 13:09:38 +0100
Subject: Factorize code for comparing maybe-cumulative inductives.

The part in Reduction should be semantics preserving, but Reductionops
only tried cumulativity if equality fails. This is probably wrong so I
changed it.
---
 kernel/reduction.ml | 143 +++++++++++++++++++---------------------------------
 1 file changed, 52 insertions(+), 91 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1724f210db..c77085067f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -200,13 +200,10 @@ let is_cumul = function CUMUL -> true | CONV -> false
 
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
-    compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
+    compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
-      Univ.Instance.t -> int -> 'a -> 'a;
-    conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
-      Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
-  } 
+    compare_cumul_instances : conv_pb -> Univ.abstract_cumulativity_info ->
+      Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a }
 
 type 'a universe_state = 'a * 'a universe_compare
 
@@ -215,18 +212,49 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
 
 let sort_cmp_universes env pb s0 s1 (u, check) =
-  (check.compare env pb s0 s1 u, check)
+  (check.compare_sorts env pb s0 s1 u, check)
 
 (* [flex] should be true for constants, false for inductive types and
    constructors. *)
 let convert_instances ~flex u u' (s, check) =
   (check.compare_instances ~flex u u' s, check)
   
-let convert_inductives cv_pb ind u1 sv1 u2 sv2 (s, check) =
-  (check.conv_inductives cv_pb ind u1 sv1 u2 sv2 s, check)
+let convert_inductives cv_pb (mind,ind) u1 sv1 u2 sv2 (s, check as univs) =
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ ->
+    assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
+    univs
+  | Declarations.Polymorphic_ind _ ->
+    check.compare_instances ~flex:false u1 u2 s, check
+  | Declarations.Cumulative_ind cumi ->
+    let num_param_arity =
+      mind.Declarations.mind_nparams +
+      mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+    in
+    if not (num_param_arity = sv1 && num_param_arity = sv2) then
+      check.compare_instances ~flex:false u1 u2 s, check
+    else
+      check.compare_cumul_instances cv_pb cumi u1 u2 s, check
 
-let convert_constructors cons u1 sv1 u2 sv2 (s, check) =
-  (check.conv_constructors cons u1 sv1 u2 sv2 s, check)
+let convert_constructors (mind, ind, cns) u1 sv1 u2 sv2 (s, check as univs) =
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ ->
+    assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
+    univs
+  | Declarations.Polymorphic_ind _ ->
+    check.compare_instances ~flex:false u1 u2 s, check
+  | Declarations.Cumulative_ind cumi ->
+    let num_cnstr_args =
+      let nparamsctxt =
+        mind.Declarations.mind_nparams +
+        mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+        (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
+      nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
+    in
+    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+      check.compare_instances ~flex:false u1 u2 s, check
+    else
+      check.compare_cumul_instances CONV cumi u1 u2 s, check
 
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
@@ -510,12 +538,10 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         else
           let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
           let cuniv =
-            match mind.Declarations.mind_universes with
-            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-              convert_instances ~flex:false u1 u2 cuniv
-            | Declarations.Cumulative_ind cumi ->
-              convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
-                u2 (CClosure.stack_args_size v2) cuniv
+            convert_inductives cv_pb (mind, snd ind1)
+              u1 (CClosure.stack_args_size v1)
+              u2 (CClosure.stack_args_size v2)
+              cuniv
           in
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
@@ -528,13 +554,10 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         else
           let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
           let cuniv =
-            match mind.Declarations.mind_universes with
-            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-              convert_instances ~flex:false u1 u2 cuniv
-            | Declarations.Cumulative_ind _ ->
-              convert_constructors
-                (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
-                u2 (CClosure.stack_args_size v2) cuniv
+            convert_constructors (mind, snd ind1, j1)
+              u1 (CClosure.stack_args_size v1)
+              u2 (CClosure.stack_args_size v2)
+              cuniv
           in
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
@@ -653,41 +676,6 @@ let check_convert_instances ~flex u u' univs =
   else raise NotConvertible
 
 (* general conversion and inference functions *)
-let infer_check_conv_inductives
-    infer_check_convert_instances
-    infer_check_inductive_instances
-    cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
-  match mind.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-    infer_check_convert_instances ~flex:false u1 u2 univs
-  | Declarations.Cumulative_ind cumi ->
-    let num_param_arity =
-      mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
-    in
-    if not (num_param_arity = sv1 && num_param_arity = sv2) then
-      infer_check_convert_instances ~flex:false u1 u2 univs
-    else
-      infer_check_inductive_instances cv_pb cumi u1 u2 univs
-
-let infer_check_conv_constructors
-    infer_check_convert_instances
-    infer_check_inductive_instances
-    (mind, ind, cns) u1 sv1 u2 sv2 univs =
-  match mind.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-    infer_check_convert_instances ~flex:false u1 u2 univs
-  | Declarations.Cumulative_ind cumi ->
-    let num_cnstr_args =
-      let nparamsctxt =
-        mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
-        (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
-      nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
-    in
-    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
-      infer_check_convert_instances ~flex:false u1 u2 univs
-    else
-      infer_check_inductive_instances CONV cumi u1 u2 univs
-
 let check_inductive_instances cv_pb cumi u u' univs =
   let length_ind_instance = 
     Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
@@ -714,23 +702,10 @@ let check_inductive_instances cv_pb cumi u u' univs =
     if (UGraph.check_constraints comp_cst univs) then univs
     else raise NotConvertible
 
-let check_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
-  infer_check_conv_inductives
-    check_convert_instances
-    check_inductive_instances
-    cv_pb ind u1 sv1 u2 sv2 univs
-
-let check_conv_constructors cns u1 sv1 u2 sv2 univs =
-  infer_check_conv_constructors
-    check_convert_instances
-    check_inductive_instances
-    cns u1 sv1 u2 sv2 univs
-
 let checked_universes =
-  { compare = checked_sort_cmp_universes;
+  { compare_sorts = checked_sort_cmp_universes;
     compare_instances = check_convert_instances;
-    conv_inductives = check_conv_inductives;
-    conv_constructors = check_conv_constructors}
+    compare_cumul_instances = check_inductive_instances; }
 
 let infer_eq (univs, cstrs as cuniv) u u' =
   if UGraph.check_eq univs u u' then cuniv
@@ -798,24 +773,10 @@ let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
     in
     (univs, Univ.Constraint.union cstrs comp_cst)
 
-
-let infer_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
-  infer_check_conv_inductives
-    infer_convert_instances
-    infer_inductive_instances
-    cv_pb ind u1 sv1 u2 sv2 univs
-
-let infer_conv_constructors cns u1 sv1 u2 sv2 univs =
-  infer_check_conv_constructors
-    infer_convert_instances
-    infer_inductive_instances
-    cns u1 sv1 u2 sv2 univs
-    
-let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
-  { compare = infer_cmp_universes;
+let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
+  { compare_sorts = infer_cmp_universes;
     compare_instances = infer_convert_instances;
-    conv_inductives = infer_conv_inductives;
-    conv_constructors = infer_conv_constructors}
+    compare_cumul_instances = infer_inductive_instances; }
 
 let gen_conv cv_pb l2r reds env evars univs t1 t2 =
   let b = 
-- 
cgit v1.2.3


From 10d3d803e6b57024dd15df7d61670ce42260948a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 7 Nov 2017 15:09:27 +0100
Subject: [get_cumulativity_constraints] allowing further code sharing.

---
 kernel/reduction.ml | 141 +++++++++++++++++++++++-----------------------------
 1 file changed, 63 insertions(+), 78 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c77085067f..dc46ac01b6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -202,8 +202,7 @@ type 'a universe_compare =
   { (* Might raise NotConvertible *)
     compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    compare_cumul_instances : conv_pb -> Univ.abstract_cumulativity_info ->
-      Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a }
+    compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a }
 
 type 'a universe_state = 'a * 'a universe_compare
 
@@ -218,31 +217,58 @@ let sort_cmp_universes env pb s0 s1 (u, check) =
    constructors. *)
 let convert_instances ~flex u u' (s, check) =
   (check.compare_instances ~flex u u' s, check)
-  
-let convert_inductives cv_pb (mind,ind) u1 sv1 u2 sv2 (s, check as univs) =
+
+let get_cumulativity_constraints cv_pb cumi u u' =
+  let length_ind_instance =
+    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
+  in
+  let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
+  if not ((length_ind_instance = Univ.Instance.length u) &&
+          (length_ind_instance = Univ.Instance.length u')) then
+     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  else
+    let comp_cst =
+      let comp_subst = (Univ.Instance.append u u') in
+      Univ.AUContext.instantiate comp_subst ind_subtypctx
+    in
+    match cv_pb with
+    | CONV ->
+      let comp_cst' =
+        let comp_subst = (Univ.Instance.append u' u) in
+        Univ.AUContext.instantiate comp_subst ind_subtypctx
+      in
+      Univ.Constraint.union comp_cst comp_cst'
+    | CUMUL -> comp_cst
+
+let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s =
   match mind.Declarations.mind_universes with
   | Declarations.Monomorphic_ind _ ->
     assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
-    univs
+    s
   | Declarations.Polymorphic_ind _ ->
-    check.compare_instances ~flex:false u1 u2 s, check
+    cmp_instances u1 u2 s
   | Declarations.Cumulative_ind cumi ->
     let num_param_arity =
       mind.Declarations.mind_nparams +
       mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
     in
-    if not (num_param_arity = sv1 && num_param_arity = sv2) then
-      check.compare_instances ~flex:false u1 u2 s, check
+    if not (Int.equal num_param_arity nargs) then
+      cmp_instances u1 u2 s
     else
-      check.compare_cumul_instances cv_pb cumi u1 u2 s, check
+      let csts = get_cumulativity_constraints cv_pb cumi u1 u2 in
+      cmp_cumul csts s
 
-let convert_constructors (mind, ind, cns) u1 sv1 u2 sv2 (s, check as univs) =
+let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
+  convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
+    cv_pb ind nargs u1 u2 s, check
+
+let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s =
   match mind.Declarations.mind_universes with
   | Declarations.Monomorphic_ind _ ->
     assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
-    univs
+    s
   | Declarations.Polymorphic_ind _ ->
-    check.compare_instances ~flex:false u1 u2 s, check
+    cmp_instances u1 u2 s
   | Declarations.Cumulative_ind cumi ->
     let num_cnstr_args =
       let nparamsctxt =
@@ -251,10 +277,15 @@ let convert_constructors (mind, ind, cns) u1 sv1 u2 sv2 (s, check as univs) =
         (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
       nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
     in
-    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
-      check.compare_instances ~flex:false u1 u2 s, check
+    if not (Int.equal num_cnstr_args nargs) then
+      cmp_instances u1 u2 s
     else
-      check.compare_cumul_instances CONV cumi u1 u2 s, check
+      let csts = get_cumulativity_constraints CONV cumi u1 u2 in
+      cmp_cumul csts s
+
+let convert_constructors ctor nargs u1 u2 (s, check) =
+  convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
+    ctor nargs u1 u2 s, check
 
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
@@ -537,13 +568,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
           let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
-          let cuniv =
-            convert_inductives cv_pb (mind, snd ind1)
-              u1 (CClosure.stack_args_size v1)
-              u2 (CClosure.stack_args_size v2)
-              cuniv
-          in
-          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          let nargs = CClosure.stack_args_size v1 in
+          if not (Int.equal nargs (CClosure.stack_args_size v2))
+          then raise NotConvertible
+          else
+            let cuniv = convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv in
+            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
@@ -553,13 +583,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
           let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
-          let cuniv =
-            convert_constructors (mind, snd ind1, j1)
-              u1 (CClosure.stack_args_size v1)
-              u2 (CClosure.stack_args_size v2)
-              cuniv
-          in
-          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          let nargs = CClosure.stack_args_size v1 in
+          if not (Int.equal nargs (CClosure.stack_args_size v2))
+          then raise NotConvertible
+          else
+            let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in
+            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 	  
     (* Eta expansion of records *)
@@ -676,31 +705,9 @@ let check_convert_instances ~flex u u' univs =
   else raise NotConvertible
 
 (* general conversion and inference functions *)
-let check_inductive_instances cv_pb cumi u u' univs =
-  let length_ind_instance = 
-    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
-  in
-  let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((length_ind_instance = Univ.Instance.length u) &&
-          (length_ind_instance = Univ.Instance.length u')) then
-     anomaly (Pp.str "Invalid inductive subtyping encountered!")
-  else
-    let comp_cst =
-      let comp_subst = (Univ.Instance.append u u') in
-      Univ.AUContext.instantiate comp_subst ind_subtypctx
-    in
-    let comp_cst =
-      match cv_pb with
-        CONV -> 
-        let comp_cst' = 
-          let comp_subst = (Univ.Instance.append u' u) in
-          Univ.AUContext.instantiate comp_subst ind_subtypctx
-        in
-        Univ.Constraint.union comp_cst comp_cst'
-      | CUMUL -> comp_cst
-    in
-    if (UGraph.check_constraints comp_cst univs) then univs
-    else raise NotConvertible
+let check_inductive_instances csts univs =
+  if (UGraph.check_constraints csts univs) then univs
+  else raise NotConvertible
 
 let checked_universes =
   { compare_sorts = checked_sort_cmp_universes;
@@ -748,30 +755,8 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
     else Univ.enforce_eq_instances u u' cstrs
   in (univs, cstrs')
 
-let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
-  let length_ind_instance = 
-    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
-  in
-  let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((length_ind_instance = Univ.Instance.length u) &&
-          (length_ind_instance = Univ.Instance.length u')) then
-    anomaly (Pp.str "Invalid inductive subtyping encountered!")
-  else
-    let comp_cst =
-      let comp_subst = (Univ.Instance.append u u') in
-      Univ.AUContext.instantiate comp_subst ind_subtypctx
-    in
-    let comp_cst =
-      match cv_pb with
-        CONV -> 
-        let comp_cst' = 
-          let comp_subst = (Univ.Instance.append u' u) in
-          Univ.AUContext.instantiate comp_subst ind_subtypctx
-        in
-        Univ.Constraint.union comp_cst comp_cst'
-      | CUMUL -> comp_cst
-    in
-    (univs, Univ.Constraint.union cstrs comp_cst)
+let infer_inductive_instances csts (univs,csts') =
+  (univs, Univ.Constraint.union csts csts')
 
 let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
   { compare_sorts = infer_cmp_universes;
-- 
cgit v1.2.3


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 |=  *)
---
 kernel/reduction.ml | 27 +++++++--------------------
 1 file changed, 7 insertions(+), 20 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index dc46ac01b6..083692e91d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -219,26 +219,13 @@ let convert_instances ~flex u u' (s, check) =
   (check.compare_instances ~flex u u' s, check)
 
 let get_cumulativity_constraints cv_pb cumi u u' =
-  let length_ind_instance =
-    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
-  in
-  let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((length_ind_instance = Univ.Instance.length u) &&
-          (length_ind_instance = Univ.Instance.length u')) then
-     anomaly (Pp.str "Invalid inductive subtyping encountered!")
-  else
-    let comp_cst =
-      let comp_subst = (Univ.Instance.append u u') in
-      Univ.AUContext.instantiate comp_subst ind_subtypctx
-    in
-    match cv_pb with
-    | CONV ->
-      let comp_cst' =
-        let comp_subst = (Univ.Instance.append u' u) in
-        Univ.AUContext.instantiate comp_subst ind_subtypctx
-      in
-      Univ.Constraint.union comp_cst comp_cst'
-    | CUMUL -> comp_cst
+  match cv_pb with
+  | CONV ->
+    Univ.Variance.eq_constraints (Univ.ACumulativityInfo.variance cumi)
+      u u' Univ.Constraint.empty
+  | CUMUL ->
+    Univ.Variance.leq_constraints (Univ.ACumulativityInfo.variance cumi)
+      u u' Univ.Constraint.empty
 
 let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s =
   match mind.Declarations.mind_universes with
-- 
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.
---
 kernel/reduction.ml | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 083692e91d..208a62cedc 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -227,6 +227,10 @@ let get_cumulativity_constraints cv_pb cumi u u' =
     Univ.Variance.leq_constraints (Univ.ACumulativityInfo.variance cumi)
       u u' Univ.Constraint.empty
 
+let inductive_cumulativity_arguments (mind,ind) =
+  mind.Declarations.mind_nparams +
+  mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+
 let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s =
   match mind.Declarations.mind_universes with
   | Declarations.Monomorphic_ind _ ->
@@ -235,10 +239,7 @@ let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2
   | Declarations.Polymorphic_ind _ ->
     cmp_instances u1 u2 s
   | Declarations.Cumulative_ind cumi ->
-    let num_param_arity =
-      mind.Declarations.mind_nparams +
-      mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
-    in
+    let num_param_arity = inductive_cumulativity_arguments (mind,ind) in
     if not (Int.equal num_param_arity nargs) then
       cmp_instances u1 u2 s
     else
@@ -249,6 +250,13 @@ let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
   convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
     cv_pb ind nargs u1 u2 s, check
 
+let constructor_cumulativity_arguments (mind, ind, ctor) =
+  let nparamsctxt =
+    mind.Declarations.mind_nparams +
+    mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+    (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
+  nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1)
+
 let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s =
   match mind.Declarations.mind_universes with
   | Declarations.Monomorphic_ind _ ->
@@ -257,13 +265,7 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u
   | Declarations.Polymorphic_ind _ ->
     cmp_instances u1 u2 s
   | Declarations.Cumulative_ind cumi ->
-    let num_cnstr_args =
-      let nparamsctxt =
-        mind.Declarations.mind_nparams +
-        mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
-        (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
-      nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
-    in
+    let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in
     if not (Int.equal num_cnstr_args nargs) then
       cmp_instances u1 u2 s
     else
-- 
cgit v1.2.3


From d81ea7705cd60b6bcb1de07282860228a23b68ac Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 11 Nov 2017 21:57:25 +0100
Subject: Universe instance printer: add optional variance argument.

---
 kernel/reduction.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 208a62cedc..124c03ce5b 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -221,11 +221,9 @@ let convert_instances ~flex u u' (s, check) =
 let get_cumulativity_constraints cv_pb cumi u u' =
   match cv_pb with
   | CONV ->
-    Univ.Variance.eq_constraints (Univ.ACumulativityInfo.variance cumi)
-      u u' Univ.Constraint.empty
+    Univ.ACumulativityInfo.eq_constraints cumi u u' Univ.Constraint.empty
   | CUMUL ->
-    Univ.Variance.leq_constraints (Univ.ACumulativityInfo.variance cumi)
-      u u' Univ.Constraint.empty
+    Univ.ACumulativityInfo.leq_constraints cumi u u' Univ.Constraint.empty
 
 let inductive_cumulativity_arguments (mind,ind) =
   mind.Declarations.mind_nparams +
-- 
cgit v1.2.3