Universe instance printer: add optional variance argument.

4 files changed, 81 insertions, 78 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index f2677acd6..cfca335d3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -246,7 +246,7 @@ let check_subtyping cumi paramsctxt env_ar inds =
     let env = Environ.push_context uctx env_ar in
     let env = Environ.push_context uctx_other env in
     let subtyp_constraints =
-      Variance.leq_constraints (CumulativityInfo.variance cumi)
+      CumulativityInfo.leq_constraints cumi
         (UContext.instance uctx) instance_other
         Constraint.empty
     in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 208a62ced..124c03ce5 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 +
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7ae099246..080bb7ad4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -712,7 +712,48 @@ type universe_level_subst = universe_level universe_map
 (** A full substitution might involve algebraic universes *)
 type universe_subst = universe universe_map
 
-module Instance : sig 
+module Variance =
+struct
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  let sup x y =
+    match x, y with
+    | Irrelevant, s | s, Irrelevant -> s
+    | Invariant, _ | _, Invariant -> Invariant
+    | Covariant, Covariant -> Covariant
+
+  let pr = function
+    | Irrelevant -> str "*"
+    | Covariant -> str "+"
+    | Invariant -> str "="
+
+  let leq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant -> enforce_leq_level u u' csts
+    | Invariant -> enforce_eq_level u u' csts
+
+  let eq_constraint csts variance u u' =
+    match variance with
+    | Irrelevant -> csts
+    | Covariant | Invariant -> enforce_eq_level u u' csts
+
+  let leq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 leq_constraint csts variance u u'
+
+  let eq_constraints variance u u' csts =
+    let len = Array.length u in
+    assert (len = Array.length u' && len = Array.length variance);
+    Array.fold_left3 eq_constraint csts variance u u'
+end
+
+module Instance : sig
     type t = Level.t array
 
     val empty : t
@@ -732,7 +773,7 @@ module Instance : sig
 
     val subst_fn : universe_level_subst_fn -> t -> t
     
-    val pr : (Level.t -> Pp.t) -> t -> Pp.t
+    val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t
     val levels : t -> LSet.t
 end = 
 struct
@@ -808,8 +849,12 @@ struct
 
   let levels x = LSet.of_array x
 
-  let pr =
-    prvect_with_sep spc
+  let pr prl ?variance =
+    let ppu i u =
+      let v = Option.map (fun v -> v.(i)) variance in
+      pr_opt_no_spc Variance.pr v ++ prl u
+    in
+    prvecti_with_sep spc ppu
 
   let equal t u = 
     t == u ||
@@ -873,9 +918,9 @@ struct
   let empty = (Instance.empty, Constraint.empty)
   let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
 
-  let pr prl (univs, cst as ctx) =
+  let pr prl ?variance (univs, cst as ctx) =
     if is_empty ctx then mt() else
-      h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+      h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 
   let hcons (univs, cst) =
     (Instance.hcons univs, hcons_constraints cst)
@@ -911,47 +956,6 @@ end
 type abstract_universe_context = AUContext.t
 let hcons_abstract_universe_context = AUContext.hcons
 
-module Variance =
-struct
-  (** A universe position in the instance given to a cumulative
-     inductive can be the following. Note there is no Contravariant
-     case because [forall x : A, B <= forall x : A', B'] requires [A =
-     A'] as opposed to [A' <= A]. *)
-  type t = Irrelevant | Covariant | Invariant
-
-  let sup x y =
-    match x, y with
-    | Irrelevant, s | s, Irrelevant -> s
-    | Invariant, _ | _, Invariant -> Invariant
-    | Covariant, Covariant -> Covariant
-
-  let pr = function
-    | Irrelevant -> str "*"
-    | Covariant -> str "+"
-    | Invariant -> str "="
-
-  let leq_constraint csts variance u u' =
-    match variance with
-    | Irrelevant -> csts
-    | Covariant -> enforce_leq_level u u' csts
-    | Invariant -> enforce_eq_level u u' csts
-
-  let eq_constraint csts variance u u' =
-    match variance with
-    | Irrelevant -> csts
-    | Covariant | Invariant -> enforce_eq_level u u' csts
-
-  let leq_constraints variance u u' csts =
-    let len = Array.length u in
-    assert (len = Array.length u' && len = Array.length variance);
-    Array.fold_left3 leq_constraint csts variance u u'
-
-  let eq_constraints variance u u' csts =
-    let len = Array.length u in
-    assert (len = Array.length u' && len = Array.length variance);
-    Array.fold_left3 eq_constraint csts variance u u'
-end
-
 (** Universe info for cumulative inductive types: A context of
    universe levels with universe constraints, representing local
    universe variables and constraints, together with an array of
@@ -972,13 +976,7 @@ struct
   let is_empty (univs, variance) = UContext.is_empty univs && Array.is_empty variance
 
   let pr prl (univs, variance) =
-    if UContext.is_empty univs then mt() else
-      let ppu i u =
-        let v = variance.(i) in
-        Variance.pr v ++ prl u
-      in
-      h 0 (prvecti_with_sep spc ppu (UContext.instance univs) ++ str " |= ") ++
-      h 0 (v 0 (Constraint.pr prl (UContext.constraints univs)))
+    UContext.pr prl ~variance univs
 
   let hcons (univs, variance) = (* should variance be hconsed? *)
     (UContext.hcons univs, variance)
@@ -992,6 +990,9 @@ struct
   let from_universe_context univs =
     (univs, Array.init (UContext.size univs) (fun _ -> Variance.Invariant))
 
+  let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts
+  let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts
+
 end
 
 type cumulativity_info = CumulativityInfo.t
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e8f5ba568..77ebf5a11 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -238,6 +238,20 @@ type universe_level_subst_fn = Level.t -> Level.t
 type universe_subst = Universe.t universe_map
 type universe_level_subst = Level.t universe_map
 
+module Variance :
+sig
+  (** A universe position in the instance given to a cumulative
+     inductive can be the following. Note there is no Contravariant
+     case because [forall x : A, B <= forall x : A', B'] requires [A =
+     A'] as opposed to [A' <= A]. *)
+  type t = Irrelevant | Covariant | Invariant
+
+  val sup : t -> t -> t
+
+  val pr : t -> Pp.t
+
+end
+
 (** {6 Universe instances} *)
 
 module Instance :
@@ -273,7 +287,7 @@ sig
   val subst_fn : universe_level_subst_fn -> t -> t
   (** Substitution by a level-to-level function. *)
 
-  val pr : (Level.t -> Pp.t) -> t -> Pp.t
+  val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t
   (** Pretty-printing, no comments *)
 
   val levels : t -> LSet.t
@@ -347,22 +361,6 @@ end
 type abstract_universe_context = AUContext.t
 [@@ocaml.deprecated "Use AUContext.t"]
 
-module Variance :
-sig
-  (** A universe position in the instance given to a cumulative
-     inductive can be the following. Note there is no Contravariant
-     case because [forall x : A, B <= forall x : A', B'] requires [A =
-     A'] as opposed to [A' <= A]. *)
-  type t = Irrelevant | Covariant | Invariant
-
-  val sup : t -> t -> t
-
-  val pr : t -> Pp.t
-
-  val leq_constraints : t array -> Instance.t constraint_function
-  val eq_constraints : t array -> Instance.t constraint_function
-end
-
 (** Universe info for cumulative inductive types: A context of
    universe levels with universe constraints, representing local
    universe variables and constraints, together with an array of
@@ -387,6 +385,8 @@ sig
      trivial subtyping relation. *)
   val from_universe_context : UContext.t -> t
 
+  val leq_constraints : t -> Instance.t constraint_function
+  val eq_constraints : t -> Instance.t constraint_function
 end
 
 type cumulativity_info = CumulativityInfo.t
@@ -398,6 +398,8 @@ sig
 
   val univ_context : t -> AUContext.t
   val variance : t -> Variance.t array
+  val leq_constraints : t -> Instance.t constraint_function
+  val eq_constraints : t -> Instance.t constraint_function
 end
 
 type abstract_cumulativity_info = ACumulativityInfo.t
@@ -491,9 +493,11 @@ val make_abstract_instance : AUContext.t -> Instance.t
 
 val pr_constraint_type : constraint_type -> Pp.t
 val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t
-val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t
+val pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array ->
+  UContext.t -> Pp.t
 val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t
-val pr_abstract_universe_context : (Level.t -> Pp.t) -> AUContext.t -> Pp.t
+val pr_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array ->
+  AUContext.t -> Pp.t
 val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> ACumulativityInfo.t -> Pp.t
 val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
 val explain_universe_inconsistency : (Level.t -> Pp.t) ->