Tentative to make unification check types at every instanciation of an

evar, and simultaneously make type inference with universes work better.
This only exports more functions from kernel/univ, to be able to work
with a set of universe variables during type inference. Universe
constraints are gradually added during type checking, adding information
necessary e.g. to lower the level of unknown Type variables to Prop or
Set. There does not seem to be a disastrous performance hit on the
stdlib, but might have one on some contribs (hence the "Tentative").


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 4 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index e31e2be689..660e39e637 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -54,6 +54,11 @@ module UniverseLevel = struct
 end
 
 module UniverseLMap = Map.Make (UniverseLevel)
+module UniverseLSet = Set.Make (UniverseLevel)
+
+type universe_level = UniverseLevel.t
+
+let compare_levels = UniverseLevel.compare
 
 (* An algebraic universe [universe] is either a universe variable
    [UniverseLevel.t] or a formal universe known to be greater than some
@@ -71,7 +76,13 @@ type universe =
   | Atom of UniverseLevel.t
   | Max of UniverseLevel.t list * UniverseLevel.t list
 
-let make_univ (m,n) = Atom (UniverseLevel.Level (m,n))
+let make_universe_level (m,n) = UniverseLevel.Level (m,n)
+let make_universe l = Atom l
+let make_univ c = Atom (make_universe_level c)
+
+let universe_level = function
+  | Atom l -> Some l
+  | Max _ -> None
 
 let pr_uni_level u = str (UniverseLevel.to_string u)
 
@@ -500,9 +511,6 @@ let merge_constraints c g =
 
 (* Normalization *)
 
-module UniverseLSet =
- Set.Make (UniverseLevel)
-
 let lookup_level u g =
   try Some (UniverseLMap.find u g) with Not_found -> None