aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/univ.ml8
-rw-r--r--checker/univ.mli12
2 files changed, 18 insertions, 2 deletions
diff --git a/checker/univ.ml b/checker/univ.ml
index fc0764077..7d285b6fe 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -142,7 +142,13 @@ end
(** Level sets and maps *)
module LMap = HMap.Make (Level)
-module LSet = LMap.Set
+module LSet = struct
+ include LMap.Set
+
+ let pr s =
+ str"{" ++ prlist_with_sep spc Level.pr (elements s) ++ str"}"
+
+end
type 'a universe_map = 'a LMap.t
diff --git a/checker/univ.mli b/checker/univ.mli
index 935f0a2b8..6cd3b3638 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -49,6 +49,7 @@ sig
val make : Level.t -> t
(** Create a universe representing the given level. *)
+ val pr : t -> Pp.t
end
type universe = Universe.t
@@ -140,7 +141,14 @@ val check_constraints : constraints -> universes -> bool
(** Polymorphic maps from universe levels to 'a *)
module LMap : CSig.MapS with type key = universe_level
-module LSet : CSig.SetS with type elt = universe_level
+module LSet :
+sig
+ include CSig.SetS with type elt = Level.t
+
+ val pr : t -> Pp.t
+ (** Pretty-printing *)
+end
+
type 'a universe_map = 'a LMap.t
(** {6 Substitution} *)
@@ -216,6 +224,8 @@ sig
val instantiate : Instance.t -> t -> Constraint.t
val repr : t -> UContext.t
+ val pr : (Level.t -> Pp.t) -> t -> Pp.t
+
end
type abstract_universe_context = AUContext.t