diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 30 | ||||
| -rw-r--r-- | kernel/univ.mli | 2 |
2 files changed, 17 insertions, 15 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 7f49e6e761..db5b071313 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -13,6 +13,9 @@ (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *) +open Pp +open Util + (* Universes are stratified by a partial ordering $\le$. Let $\~{}$ be the associated equivalence. We also have a strict ordering $<$ between equivalence classes, and we maintain that $<$ is acyclic, @@ -25,21 +28,6 @@ union-find algorithm. The assertions $<$ and $\le$ are represented by adjacency lists *) -open Pp -open Util - -(* An algebraic universe [universe] is either a universe variable - [universe_level] or a formal universe known to be greater than some - universe variables and strictly greater than some (other) universe - variables - - Universes variables denote universes initially present in the term - to type-check and non variable algebraic universes denote the - universes inferred while type-checking: it is either the successor - of a universe present in the initial term to type-check or the - maximum of two algebraic universes - *) - type universe_level = | Set | Level of Names.dir_path * int @@ -63,6 +51,18 @@ let string_of_univ_level = function module UniverseLMap = Map.Make (struct type t = universe_level let compare = cmp_univ_level end) +(* An algebraic universe [universe] is either a universe variable + [universe_level] or a formal universe known to be greater than some + universe variables and strictly greater than some (other) universe + variables + + Universes variables denote universes initially present in the term + to type-check and non variable algebraic universes denote the + universes inferred while type-checking: it is either the successor + of a universe present in the initial term to type-check or the + maximum of two algebraic universes + *) + type universe = | Atom of universe_level | Max of universe_level list * universe_level list diff --git a/kernel/univ.mli b/kernel/univ.mli index 268321ece4..83c69da99d 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -90,4 +90,6 @@ val dump_universes : (constraint_type -> string -> string -> unit) -> universes -> unit +(** {6 Hash-consing } *) + val hcons1_univ : universe -> universe |