Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Universes.

Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.

1 files changed, 97 insertions, 45 deletions

diff --git a/library/universes.mli b/library/universes.mli
index e5d3ded58..4cc92543b 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -16,12 +16,64 @@ open Locus
 open Univ
 
 (** Universes *)
-val new_univ_level : Names.dir_path -> universe_level
+
+(** The global universe counter *)
 val set_remote_new_univ_level : universe_level RemoteCounter.installer
+
+(** Side-effecting functions creating new universe levels. *)
+
+val new_univ_level : Names.dir_path -> universe_level
 val new_univ : Names.dir_path -> universe
 val new_Type : Names.dir_path -> types
 val new_Type_sort : Names.dir_path -> sorts
 
+val new_global_univ : unit -> universe in_universe_context_set
+val new_sort_in_family : sorts_family -> sorts
+
+(** {6 Constraints for type inference}
+    
+    When doing conversion of universes, not only do we have =/<= constraints but
+    also Lub constraints which correspond to unification of two levels which might
+    not be necessary if unfolding is performed.
+*)
+
+type universe_constraint_type = ULe | UEq | ULub
+
+type universe_constraint = universe * universe_constraint_type * universe
+module Constraints : sig
+  include Set.S with type elt = universe_constraint
+		       
+  val pr : t -> Pp.std_ppcmds
+end
+
+type universe_constraints = Constraints.t
+type 'a universe_constrained = 'a * universe_constraints
+type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
+
+val subst_univs_universe_constraints : universe_subst_fn -> 
+  universe_constraints -> universe_constraints
+
+val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function
+
+val to_constraints : universes -> universe_constraints -> constraints
+
+(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts,
+   application grouping, the universe constraints in [u] and additional constraints [c]. *)
+val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
+
+(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
+    modulo alpha, casts, application grouping, the universe constraints
+    in [u] and additional constraints [c]. *)
+val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
+
+(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
+    application grouping and the universe constraints in [c]. *)
+val eq_constr_universes : constr -> constr -> bool universe_constrained
+
+(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo
+    alpha, casts, application grouping and the universe constraints in [c]. *)
+val leq_constr_universes : constr -> constr -> bool universe_constrained
+
 (** Build a fresh instance for a given context, its associated substitution and 
     the instantiated constraints. *)
 
@@ -31,9 +83,6 @@ val fresh_instance_from_context : universe_context ->
 val fresh_instance_from : universe_context -> universe_instance option ->
   (universe_instance * universe_level_subst) in_universe_context_set
 
-val new_global_univ : unit -> universe in_universe_context_set
-val new_sort_in_family : sorts_family -> sorts
-
 val fresh_sort_in_family : env -> sorts_family -> 
   sorts in_universe_context_set
 val fresh_constant_instance : env -> constant ->
@@ -49,6 +98,11 @@ val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_re
 val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> 
   constr in_universe_context_set
 
+(** Get fresh variables for the universe context.
+    Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
+val fresh_universe_context_set_instance : universe_context_set -> 
+  universe_level_subst * universe_context_set
+
 (** Raises [Not_found] if not a global reference. *)
 val global_of_constr : constr -> Globnames.global_reference puniverses
 
@@ -78,39 +132,6 @@ val make_opt_subst : universe_opt_subst -> universe_subst_fn
 
 val subst_opt_univs_constr : universe_opt_subst -> constr -> constr
 
-val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> universe_set -> universe_set -> 
-  universe_level * (universe_set * universe_set * universe_set)
-
-val instantiate_with_lbound : 
-  Univ.LMap.key ->
-  Univ.universe ->
-  bool ->
-  bool ->
-  Univ.LSet.t * Univ.universe option Univ.LMap.t *
-    Univ.LSet.t *
-    (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints ->
-  (Univ.LSet.t * Univ.universe option Univ.LMap.t *
-    Univ.LSet.t *
-     (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) *
-    (bool * bool * Univ.universe)
-    
-val compute_lbound : (constraint_type * Univ.universe) list -> universe option
-
-type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
-
-val pr_constraints_map : constraints_map -> Pp.std_ppcmds
-
-val minimize_univ_variables : 
-           Univ.LSet.t ->
-           Univ.universe option Univ.LMap.t ->
-           Univ.LSet.t ->
-  constraints_map -> constraints_map ->
-           Univ.constraints ->
-           Univ.LSet.t * Univ.universe option Univ.LMap.t *
-	     Univ.LSet.t *
-           (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints
-
-
 val normalize_context_set : universe_context_set -> 
   universe_opt_subst (* The defined and undefined variables *) ->
   universe_set (* univ variables that can be substituted by algebraics *) -> 
@@ -141,7 +162,6 @@ val normalize_universe_subst : universe_subst ref ->
     the constraints should be properly added to an evd. 
     See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
     the proper way to get a fresh copy of a global reference. *)
-
 val constr_of_global : Globnames.global_reference -> constr
 
 (** ** DEPRECATED ** synonym of [constr_of_global] *)
@@ -171,13 +191,6 @@ val nf_evars_and_universes_local : (existential -> constr option) -> universe_le
 val nf_evars_and_universes_opt_subst : (existential -> constr option) -> 
   universe_opt_subst -> constr -> constr
 
-(** Get fresh variables for the universe context.
-    Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
-val fresh_universe_context_set_instance : universe_context_set -> 
-  universe_level_subst * universe_context_set
-
-val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
-
 (** Shrink a universe context to a restricted set of variables *)
 
 val universes_of_constr : constr -> universe_set
@@ -189,3 +202,42 @@ val simplify_universe_context : universe_context_set ->
 val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes
 
 val remove_trivial_constraints : universe_context_set -> universe_context_set
+
+(** Pretty-printing *)
+
+val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
+
+(* For tracing *)
+
+type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
+
+val pr_constraints_map : constraints_map -> Pp.std_ppcmds
+
+val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> universe_set -> universe_set -> 
+  universe_level * (universe_set * universe_set * universe_set)
+    
+val compute_lbound : (constraint_type * Univ.universe) list -> universe option
+
+val instantiate_with_lbound : 
+  Univ.LMap.key ->
+  Univ.universe ->
+  bool ->
+  bool ->
+  Univ.LSet.t * Univ.universe option Univ.LMap.t *
+    Univ.LSet.t *
+    (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints ->
+  (Univ.LSet.t * Univ.universe option Univ.LMap.t *
+    Univ.LSet.t *
+     (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) *
+    (bool * bool * Univ.universe)
+
+val minimize_univ_variables : 
+           Univ.LSet.t ->
+           Univ.universe option Univ.LMap.t ->
+           Univ.LSet.t ->
+  constraints_map -> constraints_map ->
+           Univ.constraints ->
+           Univ.LSet.t * Univ.universe option Univ.LMap.t *
+	     Univ.LSet.t *
+           (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints
+