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

2 files changed, 21 insertions, 4 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index e31e2be68..660e39e63 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
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e19a4c43a..2f99e16ec 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -8,8 +8,11 @@
 
 (** Universes. *)
 
+type universe_level
 type universe
 
+module UniverseLSet : Set.S with type elt = universe_level
+
 (** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... 
    Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
 
@@ -17,12 +20,17 @@ val type0m_univ : universe  (** image of Prop in the universes hierarchy *)
 val type0_univ : universe  (** image of Set in the universes hierarchy *)
 val type1_univ : universe  (** the universe of the type of Prop/Set *)
 
+val make_universe_level : Names.dir_path * int -> universe_level
+val make_universe : universe_level -> universe
 val make_univ : Names.dir_path * int -> universe
 
 val is_type0_univ : universe -> bool
 val is_type0m_univ : universe -> bool
 val is_univ_variable : universe -> bool
 
+val universe_level : universe -> universe_level option
+val compare_levels : universe_level -> universe_level -> int
+
 (** The type of a universe *)
 val super : universe -> universe
 
@@ -82,6 +90,7 @@ val no_upper_constraints : universe -> constraints -> bool
 
 (** {6 Pretty-printing of universes. } *)
 
+val pr_uni_level : universe_level -> Pp.std_ppcmds
 val pr_uni : universe -> Pp.std_ppcmds
 val pr_universes : universes -> Pp.std_ppcmds
 val pr_constraints : constraints -> Pp.std_ppcmds