aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-11-11 21:57:25 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-11 22:28:39 +0100
commitd81ea7705cd60b6bcb1de07282860228a23b68ac (patch)
tree6fe6feea61545c35bc80ad9ff8a9fe294f9419d1
parent6c2d10b93b819f0735a43453c78566795de8ba5a (diff)
Universe instance printer: add optional variance argument.
-rw-r--r--kernel/indtypes.ml2
-rw-r--r--kernel/reduction.ml6
-rw-r--r--kernel/univ.ml109
-rw-r--r--kernel/univ.mli42
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) ->