Clarifying and documenting the UState API.

4 files changed, 74 insertions, 47 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index cfe9a3da40..52bfc2d1d1 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -263,7 +263,6 @@ type evar_universe_context = UState.t
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
 let empty_evar_universe_context = UState.empty
-let evar_universe_context_from = UState.from
 let is_empty_evar_universe_context = UState.is_empty
 let union_evar_universe_context = UState.union
 let evar_universe_context_set = UState.context_set
@@ -273,6 +272,7 @@ let evar_universe_context_of = UState.of_context_set
 let evar_universe_context_subst = UState.subst
 let add_constraints_context = UState.add_constraints
 let add_universe_constraints_context = UState.add_universe_constraints
+let constrain_variables = UState.constrain_variables 
 
 (* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *)
 (* let add_universe_constraints_context =  *)
@@ -587,7 +587,7 @@ let empty = {
 }
 
 let from_env e = 
-  { empty with universes = evar_universe_context_from e }
+  { empty with universes = UState.make (Environ.universes e) }
 
 let from_ctx ctx = { empty with universes = ctx }
 
@@ -746,7 +746,7 @@ let univ_flexible_alg = UnivFlexible true
 
 let evar_universe_context d = d.universes
 
-let universe_context_set d = UState.context_set Univ.UContext.empty d.universes
+let universe_context_set d = UState.context_set d.universes
 
 let pr_uctx_level = UState.pr_uctx_level
 let universe_context ?names evd = UState.universe_context ?names evd.universes
@@ -784,8 +784,16 @@ let add_global_univ d u =
 let make_flexible_variable evd b u =
   { evd with universes = UState.make_flexible_variable evd.universes b u }
 
-let make_evar_universe_context = UState.make
-    
+let make_evar_universe_context e l =
+  let uctx = UState.make (Environ.universes e) in
+  match l with
+  | None -> uctx
+  | Some us ->
+      List.fold_left
+        (fun uctx (loc,id) ->
+        fst (UState.new_univ_variable univ_rigid (Some (Id.to_string id)) uctx))
+        uctx us
+
 (****************************************)
 (* Operations on constants              *)
 (****************************************)
@@ -1338,9 +1346,9 @@ let pr_evar_universe_context ctx =
   if is_empty_evar_universe_context ctx then mt ()
   else
     (str"UNIVERSES:"++brk(0,1)++ 
-       h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set Univ.UContext.empty ctx)) ++ fnl () ++
+       h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
-     h 0 (Univ.LSet.pr prl (UState.variables ctx)) ++ fnl() ++
+     h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
      str"UNDEFINED UNIVERSES:"++brk(0,1)++
        h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 796f503746..dc498ed42e 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -474,7 +474,7 @@ val univ_flexible_alg : rigid
 
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
-val evar_universe_context_set : Univ.universe_context -> evar_universe_context -> Univ.universe_context_set
+val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set
 val evar_universe_context_constraints : evar_universe_context -> Univ.constraints
 val evar_context_universe_context : evar_universe_context -> Univ.universe_context
 val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context
@@ -482,6 +482,8 @@ val empty_evar_universe_context : evar_universe_context
 val union_evar_universe_context : evar_universe_context -> evar_universe_context ->
   evar_universe_context
 val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst
+val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints
+
 
 val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context
 val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map							   
diff --git a/engine/uState.ml b/engine/uState.ml
index 2eb0519b78..227c4ad52b 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -47,8 +47,7 @@ let empty =
     uctx_universes = UGraph.initial_universes;
     uctx_initial_universes = UGraph.initial_universes }
 
-let from e =
-  let u = Environ.universes e in
+let make u =
     { empty with 
       uctx_universes = u; uctx_initial_universes = u}
 
@@ -82,20 +81,8 @@ let union ctx ctx' =
             let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
               UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
 
-let context_set diff ctx =
-  let initctx = ctx.uctx_local in
-  let cstrs =
-    Univ.LSet.fold
-      (fun l cstrs ->
-       try
-         match Univ.LMap.find l ctx.uctx_univ_variables with
-         | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
-         | None -> cstrs
-       with Not_found | Option.IsNone -> cstrs)
-      (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty
-  in
-    Univ.ContextSet.add_constraints cstrs initctx 
-                      
+let context_set ctx = ctx.uctx_local
+
 let constraints ctx = snd ctx.uctx_local
 
 let context ctx = Univ.ContextSet.to_context ctx.uctx_local
@@ -106,7 +93,17 @@ let subst ctx = ctx.uctx_univ_variables
 
 let ugraph ctx = ctx.uctx_universes
 
-let variables ctx = ctx.uctx_univ_algebraic
+let algebraics ctx = ctx.uctx_univ_algebraic
+
+let constrain_variables diff ctx =
+  Univ.LSet.fold
+    (fun l cstrs ->
+      try
+        match Univ.LMap.find l ctx.uctx_univ_variables with
+        | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs
+        | None -> cstrs
+      with Not_found | Option.IsNone -> cstrs)
+    diff Univ.Constraint.empty
 
 let instantiate_variable l b v =
   v := Univ.LMap.add l (Some b) !v
@@ -381,16 +378,6 @@ let make_flexible_variable ctx b u =
   {ctx with uctx_univ_variables = uvars'; 
       uctx_univ_algebraic = avars'}
 
-let make e l = 
-  let uctx = from e in
-    match l with
-    | None -> uctx
-    | Some us ->
-       List.fold_left
-         (fun uctx (loc,id) ->
-          fst (new_univ_variable univ_rigid (Some (Id.to_string id)) uctx))
-         uctx us
-    
 let is_sort_variable uctx s = 
   match s with 
   | Sorts.Type u -> 
diff --git a/engine/uState.mli b/engine/uState.mli
index c3b28d0a6a..56e0fe14e5 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -13,14 +13,14 @@ open Names
 exception UniversesDiffer
 
 type t
+(** Type of universe unification states. They allow the incremental building of
+    universe constraints during an interactive proof. *)
 
 (** {5 Constructors} *)
 
 val empty : t
 
-val from : Environ.env -> t
-
-val make : Environ.env -> Id.t Loc.located list option -> t
+val make : UGraph.t -> t
 
 val is_empty : t -> bool
 
@@ -30,23 +30,47 @@ val of_context_set : Univ.universe_context_set -> t
 
 (** {5 Projections} *)
 
-val context_set : Univ.universe_context -> t -> Univ.universe_context_set
-val constraints : t -> Univ.constraints
-val context : t -> Univ.universe_context
+val context_set : t -> Univ.universe_context_set
+(** The local context of the state, i.e. a set of bound variables together
+    with their associated constraints. *)
+
 val subst : t -> Universes.universe_opt_subst
+(** The local universes that are unification variables *)
+
 val ugraph : t -> UGraph.t
-val variables : t -> Univ.LSet.t
+(** The current graph extended with the local constraints *)
+
+val algebraics : t -> Univ.LSet.t
+(** The subset of unification variables that can be instantiated with algebraic
+    universes as they appear in types and universe instances only. *)
+
+val constraints : t -> Univ.constraints
+(** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *)
+
+val context : t -> Univ.universe_context
+(** Shorthand for {!context_set} with {!Context_set.to_context}. *)
 
 (** {5 Constraints handling} *)
 
 val add_constraints : t -> Univ.constraints -> t
+(**
+  @raise UniversesDiffer
+*)
+
 val add_universe_constraints : t -> Universes.universe_constraints -> t
+(**
+  @raise UniversesDiffer
+*)
 
-(** {5 TODO: Document me} *)
+(** {5 Names} *)
 
-val universe_context : ?names:(Id.t Loc.located) list -> t -> Univ.universe_context
+val add_universe_name : t -> string -> Univ.Level.t -> t
+(** Associate a human-readable name to a local variable. *)
 
-val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds
+val universe_of_name : t -> string -> Univ.Level.t
+(** Retrieve the universe associated to the name. *)
+
+(** {5 Unification} *)
 
 val restrict : t -> Univ.universe_set -> t
 
@@ -70,6 +94,8 @@ val is_sort_variable : t -> Sorts.t -> Univ.Level.t option
 
 val normalize_variables : t -> Univ.universe_subst * t
 
+val constrain_variables : Univ.LSet.t -> t -> Univ.constraints
+
 val abstract_undefined_variables : t -> t
 
 val fix_undefined_variables : t -> t
@@ -78,6 +104,10 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 
 val normalize : t -> t
 
-val universe_of_name : t -> string -> Univ.Level.t
+(** {5 TODO: Document me} *)
 
-val add_universe_name : t -> string -> Univ.Level.t -> t
+val universe_context : ?names:(Id.t Loc.located) list -> t -> Univ.universe_context
+
+(** {5 Pretty-printing} *)
+
+val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds