Clarifying and documenting the UState API.

9 files changed, 87 insertions, 55 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
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5c6ed33961..4af18ab2d5 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -298,6 +298,11 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
+let constrain_variables init uctx =
+  let levels = Univ.Instance.levels (Univ.UContext.instance init) in
+  let cstrs = UState.constrain_variables levels uctx in
+  Univ.ContextSet.add_constraints cstrs (UState.context_set uctx)
+
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
@@ -326,7 +331,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
         let used_univs_typ = Universes.universes_of_constr typ in
         if keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff) then
           let initunivs = Evd.evar_context_universe_context initial_euctx in
-          let ctx = Evd.evar_universe_context_set initunivs universes in
+          let ctx = constrain_variables initunivs universes in
           (* For vi2vo compilation proofs are computed now but we need to
            * complement the univ constraints of the typ with the ones of
            * the body.  So we keep the two sets distinct. *)
@@ -334,7 +339,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
           (initunivs, typ), ((body, ctx_body), eff)
         else
           let initunivs = Univ.UContext.empty in
-          let ctx = Evd.evar_universe_context_set initunivs universes in
+          let ctx = constrain_variables initunivs universes in
           (* Since the proof is computed now, we can simply have 1 set of
            * constraints in which we merge the ones for the body and the ones
            * for the typ *)
@@ -349,7 +354,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
         let initunivs = Evd.evar_context_universe_context initial_euctx in
         Future.from_val (initunivs, nf t),
         Future.chain ~pure:true p (fun (pt,eff) ->
-          (pt,Evd.evar_universe_context_set initunivs (Future.force univs)),eff)
+          (pt,constrain_variables initunivs (Future.force univs)),eff)
   in
   let entries =
     Future.map2 (fun p (_, t) ->
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index d26af04baa..5f034e361e 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -428,7 +428,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
             let body,opaq = retrieve_first_recthm ref in
             let subst = Evd.evar_universe_context_subst ctx in
             let norm c = Universes.subst_opt_univs_constr subst c in
-	    let ctx = Evd.evar_universe_context_set (*FIXME*) Univ.UContext.empty ctx in
+	    let ctx = UState.context_set (*FIXME*) ctx in
 	    let body = Option.map norm body in
             List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index cab74968d2..1a3f460399 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -268,7 +268,7 @@ let add_rewrite_hint bases ort t lcsr =
   let f ce = 
     let c, ctx = Constrintern.interp_constr env sigma ce in
     let ctx =
-      let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
+      let ctx = UState.context_set ctx in
         if poly then ctx
 	else (Global.push_context_set false ctx; Univ.ContextSet.empty)
     in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7c86d2d059..06e2be72d8 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1127,7 +1127,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
     let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
-    let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
+    let ctx = UState.context_set ctx in
     let ctx = Universes.restrict_universe_context ctx vars in
     let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
     let ctx = Univ.ContextSet.to_context ctx in
@@ -1160,7 +1160,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
     let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
-    let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
+    let ctx = UState.context_set ctx in
     let ctx = Univ.ContextSet.to_context ctx in
     ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx) 
 	      fixnames fixdecls fixtypes fiximps);
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fc0e5beaad..5344909b61 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1547,7 +1547,7 @@ let vernac_global_check c =
   let sigma = Evd.from_env env in
   let c,ctx = interp_constr env sigma c in
   let senv = Global.safe_env() in
-  let cstrs = snd (Evd.evar_universe_context_set Univ.UContext.empty ctx) in
+  let cstrs = snd (UState.context_set ctx) in
   let senv = Safe_typing.add_constraints cstrs senv in
   let j = Safe_typing.typing senv c in
   let env = Safe_typing.env_of_safe_env senv in