From f52826877059858fb3fcd4314c629ed63d90a042 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Sep 2015 19:50:41 +0200
Subject: Hardening the API of evarmaps.

The evar counter has been moved from Evarutil to Evd, and all functions in
Evarutil now go through a dedicated primitive to create a fresh evar from
an evarmap.
---
 engine/evd.ml | 45 +++++++++++++++++++++------------------------
 1 file changed, 21 insertions(+), 24 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index fc4f5e040e..1af8565bdb 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -632,14 +632,30 @@ let reassign_name_defined evk evk' (evtoid,idtoev) =
   (EvMap.add evk' id (EvMap.remove evk evtoid),
    Idmap.add id evk' (Idmap.remove id idtoev))
 
-let add d e i = match i.evar_body with
+let add_with_name ?(naming = Misctypes.IntroAnonymous) d e i = match i.evar_body with
 | Evar_empty ->
-  let evar_names = add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in
+  let evar_names = add_name_undefined naming e i d.evar_names in
   { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
 | Evar_defined _ ->
   let evar_names = remove_name_possibly_already_defined e d.evar_names in
   { d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
 
+let add d e i = add_with_name d e i
+
+(** New evars *)
+
+let evar_counter_summary_name = "evar counter"
+
+(* Generator of existential names *)
+let new_untyped_evar =
+  let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in
+  fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
+
+let new_evar evd ?naming evi =
+  let evk = new_untyped_evar () in
+  let evd = add_with_name evd ?naming evk evi in
+  (evd, evk)
+
 let remove d e =
   let undf_evars = EvMap.remove e d.undf_evars in
   let defn_evars = EvMap.remove e d.defn_evars in
@@ -831,27 +847,8 @@ let define evk body evd =
   let evar_names = remove_name_defined evk evd.evar_names in
   { evd with defn_evars; undf_evars; last_mods; evar_names }
 
-let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) 
-    ?(filter=Filter.identity) ?candidates ?(store=Store.empty)
-    ?(naming=Misctypes.IntroAnonymous) evd =
-  let () = match Filter.repr filter with
-  | None -> ()
-  | Some filter ->
-    assert (Int.equal (List.length filter) (List.length (named_context_of_val hyps)))
-  in
-  let evar_info = {
-    evar_hyps = hyps;
-    evar_concl = ty;
-    evar_body = Evar_empty;
-    evar_filter = filter;
-    evar_source = src;
-    evar_candidates = candidates;
-    evar_extra = store; }
-  in
-  let evar_names = add_name_newly_undefined naming evk evar_info evd.evar_names in
-  { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; evar_names }
-
-let restrict evk evk' filter ?candidates evd =
+let restrict evk filter ?candidates evd =
+  let evk' = new_untyped_evar () in
   let evar_info = EvMap.find evk evd.undf_evars in
   let evar_info' =
     { evar_info with evar_filter = filter;
@@ -863,7 +860,7 @@ let restrict evk evk' filter ?candidates evd =
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; evar_names }
+    defn_evars; evar_names }, evk'
 
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
-- 
cgit v1.2.3


From ca14b0bb67c9db000736333a056fc147c6f5199c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Sep 2015 14:16:54 +0200
Subject: Removing uselessly duplicated function in Evd.

---
 engine/evd.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 1af8565bdb..ae382cab45 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -766,10 +766,6 @@ let cmap f evd =
 (* spiwack: deprecated *)
 let create_evar_defs sigma = { sigma with
   conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty }
-(* spiwack: tentatively deprecated *)
-let create_goal_evar_defs sigma = { sigma with
-   (* conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } *)
-  metas=Metamap.empty } 
 
 let empty = {
   defn_evars = EvMap.empty;
-- 
cgit v1.2.3


From 9cadb903b7c3a3be8014152b293cd5ade3a7c8b7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Sep 2015 16:36:10 +0200
Subject: Removing subst_defined_metas_evars from Evd.

---
 engine/evd.ml | 12 ------------
 1 file changed, 12 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index ae382cab45..9c53006c13 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1504,18 +1504,6 @@ let retract_coercible_metas evd =
   let metas = Metamap.smartmapi map evd.metas in
   !mc, set_metas evd metas
 
-let subst_defined_metas_evars (bl,el) c =
-  let rec substrec c = match kind_of_term c with
-    | Meta i ->
-      let select (j,_,_) = Int.equal i j in
-      substrec (pi2 (List.find select bl))
-    | Evar (evk,args) ->
-      let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal Constr.equal args args' in
-      (try substrec (pi3 (List.find select el))
-       with Not_found -> map_constr substrec c)
-    | _ -> map_constr substrec c
-  in try Some (substrec c) with Not_found -> None
-
 let evar_source_of_meta mv evd =
   match meta_name evd mv with
   | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar)
-- 
cgit v1.2.3


From a3d7630d74b720b771e880dcf0fcad05de553a6e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Sep 2015 16:39:36 +0200
Subject: Removing meta_with_name from Evd.

---
 engine/evd.ml | 33 ---------------------------------
 1 file changed, 33 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 9c53006c13..12a04fcc22 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1451,39 +1451,6 @@ let meta_reassign mv (v, pb) evd =
 let meta_name evd mv =
   try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
 
-let explain_no_such_bound_variable evd id =
-  let mvl =
-    List.rev (Metamap.fold (fun n clb l ->
-      let na = fst (clb_name clb) in
-      if na != Anonymous then out_name na :: l else l)
-    evd.metas []) in
-  errorlabstrm "Evd.meta_with_name"
-    (str"No such bound variable " ++ pr_id id ++
-     (if mvl == [] then str " (no bound variables at all in the expression)."
-      else
-        (str" (possible name" ++
-         str (if List.length mvl == 1 then " is: " else "s are: ") ++
-         pr_enum pr_id mvl ++ str").")))
-
-let meta_with_name evd id =
-  let na = Name id in
-  let (mvl,mvnodef) =
-    Metamap.fold
-      (fun n clb (l1,l2 as l) ->
-        let (na',def) = clb_name clb in
-        if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2)
-        else l)
-      evd.metas ([],[]) in
-  match mvnodef, mvl with
-    | _,[]  ->
-      explain_no_such_bound_variable evd id
-    | ([n],_|_,[n]) ->
-	n
-    | _  ->
-	errorlabstrm "Evd.meta_with_name"
-          (str "Binder name \"" ++ pr_id id ++
-           strbrk "\" occurs more than once in clause.")
-
 let clear_metas evd = {evd with metas = Metamap.empty}
 
 let meta_merge evd1 evd2 =
-- 
cgit v1.2.3


From 84add29c036735ceacde73ea98a9a5a454a5e3a0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 6 Oct 2015 19:09:10 +0200
Subject: Splitting kernel universe code in two modules.

1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
---
 engine/evd.ml | 44 ++++++++++++++++++++++----------------------
 1 file changed, 22 insertions(+), 22 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index cd0b52ecaa..3f4bfe7afe 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -283,8 +283,8 @@ type evar_universe_context =
    (** The subset of unification variables that
 	can be instantiated with algebraic universes as they appear in types 
 	and universe instances only. *)
-   uctx_universes : Univ.universes; (** The current graph extended with the local constraints *)
-   uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *)
+   uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
+   uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
  }
   
 let empty_evar_universe_context = 
@@ -292,8 +292,8 @@ let empty_evar_universe_context =
     uctx_local = Univ.ContextSet.empty;
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
-    uctx_universes = Univ.initial_universes;
-    uctx_initial_universes = Univ.initial_universes }
+    uctx_universes = UGraph.initial_universes;
+    uctx_initial_universes = UGraph.initial_universes }
 
 let evar_universe_context_from e = 
   let u = universes e in
@@ -314,7 +314,7 @@ let union_evar_universe_context ctx ctx' =
 			       (Univ.ContextSet.levels ctx.uctx_local) in
     let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
     let declarenew g =
-      Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g
+      Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
     in
     let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
@@ -328,7 +328,7 @@ let union_evar_universe_context ctx ctx' =
 	  if local == ctx.uctx_local then ctx.uctx_universes
 	  else
 	    let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
-	      Univ.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
+	      UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
 
 (* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *)
 (* let union_evar_universe_context =  *)
@@ -374,7 +374,7 @@ let process_universe_constraints univs vars alg cstrs =
 	  | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg)
 	in
 	  if d == Universes.ULe then
-	    if Univ.check_leq univs l r then
+	    if UGraph.check_leq univs l r then
 	      (** Keep Prop/Set <= var around if var might be instantiated by prop or set
 		  later. *)
 	      if Univ.Universe.is_level l then 
@@ -413,7 +413,7 @@ let process_universe_constraints univs vars alg cstrs =
 		  instantiate_variable l' r vars
 		else if rloc then 
 		  instantiate_variable r' l vars
-		else if not (Univ.check_eq univs l r) then
+		else if not (UGraph.check_eq univs l r) then
 		  (* Two rigid/global levels, none of them being local,
 		     one of them being Prop/Set, disallow *)
 		  if Univ.Level.is_small l' || Univ.Level.is_small r' then
@@ -433,7 +433,7 @@ let process_universe_constraints univs vars alg cstrs =
 		     Univ.enforce_leq inst lu local
 		   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
             | _, _ (* One of the two is algebraic or global *) -> 
-	     if Univ.check_eq univs l r then local
+	     if UGraph.check_eq univs l r then local
 	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
   in
   let local = 
@@ -459,7 +459,7 @@ let add_constraints_context ctx cstrs =
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
-      uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
+      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
 
 (* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
 (* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
@@ -473,7 +473,7 @@ let add_universe_constraints_context ctx cstrs =
   in
     { ctx with uctx_local = (univs, Univ.Constraint.union local local');
       uctx_univ_variables = vars;
-      uctx_universes = Univ.merge_constraints local' ctx.uctx_universes }
+      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
 
 (* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *)
 (* let add_universe_constraints_context =  *)
@@ -1012,13 +1012,13 @@ let merge_uctx sideff rigid uctx ctx' =
   in
   let declare g =
     LSet.fold (fun u g ->
-	       try Univ.add_universe u false g
-	       with Univ.AlreadyDeclared when sideff -> g)
+	       try UGraph.add_universe u false g
+	       with UGraph.AlreadyDeclared when sideff -> g)
 	      levels g
   in
   let initial = declare uctx.uctx_initial_universes in
   let univs = declare uctx.uctx_universes in
-  let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in
+  let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
     { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial }
 
 let merge_context_set rigid evd ctx' = 
@@ -1079,11 +1079,11 @@ let uctx_new_univ_variable rigid name predicative
     | None -> uctx.uctx_names
   in
   let initial =
-    Univ.add_universe u false uctx.uctx_initial_universes
+    UGraph.add_universe u false uctx.uctx_initial_universes
   in						     
   let uctx' =
     {uctx' with uctx_names = names; uctx_local = ctx';
-		uctx_universes = Univ.add_universe u false uctx.uctx_universes;
+		uctx_universes = UGraph.add_universe u false uctx.uctx_universes;
 		uctx_initial_universes = initial}
   in uctx', u
 						     
@@ -1102,10 +1102,10 @@ let new_sort_variable ?name ?(predicative=true) rigid d =
 let add_global_univ d u =
   let uctx = d.universes in
   let initial =
-    Univ.add_universe u true uctx.uctx_initial_universes
+    UGraph.add_universe u true uctx.uctx_initial_universes
   in
   let univs = 
-    Univ.add_universe u true uctx.uctx_universes
+    UGraph.add_universe u true uctx.uctx_universes
   in
     { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local;
 				     uctx_initial_universes = initial;
@@ -1245,10 +1245,10 @@ let set_leq_sort env evd s1 s2 =
       else evd
 	    
 let check_eq evd s s' =
-  Univ.check_eq evd.universes.uctx_universes s s'
+  UGraph.check_eq evd.universes.uctx_universes s s'
 
 let check_leq evd s s' =
-  Univ.check_leq evd.universes.uctx_universes s s'
+  UGraph.check_leq evd.universes.uctx_universes s s'
 
 let subst_univs_context_with_def def usubst (ctx, cst) =
   (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
@@ -1301,10 +1301,10 @@ let refresh_undefined_univ_variables uctx =
           (Option.map (Univ.subst_univs_level_universe subst) v) acc)
       uctx.uctx_univ_variables Univ.LMap.empty
   in
-  let declare g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g)
+  let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g)
 				   (Univ.ContextSet.levels ctx') g in
   let initial = declare uctx.uctx_initial_universes in
-  let univs = declare Univ.initial_universes in
+  let univs = declare UGraph.initial_universes in
   let uctx' = {uctx_names = uctx.uctx_names;
 	       uctx_local = ctx'; 
 	       uctx_univ_variables = vars; uctx_univ_algebraic = alg;
-- 
cgit v1.2.3


From 68863acca9abf4490c651df889721ef7f6a4d375 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 17 Oct 2015 15:32:03 +0200
Subject: Dedicated file for universe unification context manipulation.

This allows to remove a lot of independent code from Evd which was put
into the UState module. The API is not perfect yet, but this is a first
pass. Names of data structures should be thought about too because they
are way too similar.
---
 engine/evd.ml | 528 ++++++----------------------------------------------------
 1 file changed, 53 insertions(+), 475 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 79e73bda57..cfe9a3da40 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -259,221 +259,20 @@ let instantiate_evar_array info c args =
   | [] -> c
   | _ -> replace_vars inst c
 
-module StringOrd = struct type t = string let compare = String.compare end
-module UNameMap = struct
-    
-  include Map.Make(StringOrd)
-    
-  let union s t = 
-    if s == t then s
-    else
-      merge (fun k l r -> 
-	match l, r with
-	| Some _, _ -> l
-	| _, _ -> r) s t
-end
-
-(* 2nd part used to check consistency on the fly. *)
-type evar_universe_context = 
- { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t;
-   uctx_local : Univ.universe_context_set; (** The local context of variables *)
-   uctx_univ_variables : Universes.universe_opt_subst;
-   (** The local universes that are unification variables *)
-   uctx_univ_algebraic : Univ.universe_set; 
-   (** The subset of unification variables that
-	can be instantiated with algebraic universes as they appear in types 
-	and universe instances only. *)
-   uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
-   uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
- }
-  
-let empty_evar_universe_context = 
-  { uctx_names = UNameMap.empty, Univ.LMap.empty;
-    uctx_local = Univ.ContextSet.empty;
-    uctx_univ_variables = Univ.LMap.empty;
-    uctx_univ_algebraic = Univ.LSet.empty;
-    uctx_universes = UGraph.initial_universes;
-    uctx_initial_universes = UGraph.initial_universes }
-
-let evar_universe_context_from e = 
-  let u = universes e in
-    {empty_evar_universe_context with 
-      uctx_universes = u; uctx_initial_universes = u}
-
-let is_empty_evar_universe_context ctx =
-  Univ.ContextSet.is_empty ctx.uctx_local && 
-    Univ.LMap.is_empty ctx.uctx_univ_variables
-
-let union_evar_universe_context ctx ctx' =
-  if ctx == ctx' then ctx
-  else if is_empty_evar_universe_context ctx' then ctx
-  else
-    let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
-    let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
-    let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
-			       (Univ.ContextSet.levels ctx.uctx_local) in
-    let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
-    let declarenew g =
-      Univ.LSet.fold (fun u g -> UGraph.add_universe u false g) newus g
-    in
-    let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
-      { uctx_names = (names, names_rev);
-	uctx_local = local;
-	uctx_univ_variables = 
-	  Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
-	uctx_univ_algebraic = 
-	  Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic;
-	uctx_initial_universes = declarenew ctx.uctx_initial_universes;
-	uctx_universes = 
-	  if local == ctx.uctx_local then ctx.uctx_universes
-	  else
-	    let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in
-	      UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) }
-
-(* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *)
-(* let union_evar_universe_context =  *)
-(*   Profile.profile2 union_evar_universe_context_key union_evar_universe_context;; *)
-
+type evar_universe_context = UState.t
 type 'a in_evar_universe_context = 'a * evar_universe_context
 
-let evar_universe_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 evar_universe_context_constraints ctx = snd ctx.uctx_local
-let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local
-    
-let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx }
-let evar_universe_context_subst ctx = ctx.uctx_univ_variables
-
-let instantiate_variable l b v =
-  v := Univ.LMap.add l (Some b) !v
-
-exception UniversesDiffer
-
-let process_universe_constraints univs vars alg cstrs =
-  let vars = ref vars in
-  let normalize = Universes.normalize_universe_opt_subst vars in
-  let rec unify_universes fo l d r local =
-    let l = normalize l and r = normalize r in
-      if Univ.Universe.equal l r then local
-      else 
-	let varinfo x = 
-	  match Univ.Universe.level x with
-	  | None -> Inl x
-	  | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg)
-	in
-	  if d == Universes.ULe then
-	    if UGraph.check_leq univs l r then
-	      (** Keep Prop/Set <= var around if var might be instantiated by prop or set
-		  later. *)
-	      if Univ.Universe.is_level l then 
-		match Univ.Universe.level r with
-		| Some r ->
-		  Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
-		| _ -> local
-	      else local
-	    else
-	      match Univ.Universe.level r with
-	      | None -> error ("Algebraic universe on the right")
-	      | Some rl ->
-		if Univ.Level.is_small rl then
-		  let levels = Univ.Universe.levels l in
-		    Univ.LSet.fold (fun l local ->
-		      if Univ.Level.is_small l || Univ.LMap.mem l !vars then
-			unify_universes fo (Univ.Universe.make l) Universes.UEq r local
-		      else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
-		      levels local
-		else
-		  Univ.enforce_leq l r local
-	  else if d == Universes.ULub then
-	    match varinfo l, varinfo r with
-	    | (Inr (l, true, _), Inr (r, _, _)) 
-	    | (Inr (r, _, _), Inr (l, true, _)) -> 
-	      instantiate_variable l (Univ.Universe.make r) vars; 
-	      Univ.enforce_eq_level l r local
-	    | Inr (_, _, _), Inr (_, _, _) ->
-	      unify_universes true l Universes.UEq r local
-	    | _, _ -> assert false
-	  else (* d = Universes.UEq *)
-	    match varinfo l, varinfo r with
-	    | Inr (l', lloc, _), Inr (r', rloc, _) ->
-	      let () = 
-		if lloc then
-		  instantiate_variable l' r vars
-		else if rloc then 
-		  instantiate_variable r' l vars
-		else if not (UGraph.check_eq univs l r) then
-		  (* Two rigid/global levels, none of them being local,
-		     one of them being Prop/Set, disallow *)
-		  if Univ.Level.is_small l' || Univ.Level.is_small r' then
-		    raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
-		  else
-		    if fo then 
-		      raise UniversesDiffer
-	      in
-	        Univ.enforce_eq_level l' r' local
-	    | Inr (l, loc, alg), Inl r
-	    | Inl r, Inr (l, loc, alg) ->
-	       let inst = Univ.univ_level_rem l r r in
-		 if alg then (instantiate_variable l inst vars; local)
-		 else
-		   let lu = Univ.Universe.make l in
-		   if Univ.univ_level_mem l r then
-		     Univ.enforce_leq inst lu local
-		   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
-            | _, _ (* One of the two is algebraic or global *) -> 
-	     if UGraph.check_eq univs l r then local
-	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
-  in
-  let local = 
-    Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
-      cstrs Univ.Constraint.empty
-  in
-    !vars, local
-
-let add_constraints_context ctx cstrs =
-  let univs, local = ctx.uctx_local in
-  let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> 
-    let l = Univ.Universe.make l and r = Univ.Universe.make r in
-    let cstr' = 
-      if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r)
-      else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r)
-    in Universes.Constraints.add cstr' acc)
-    cstrs Universes.Constraints.empty
-  in
-  let vars, local' =
-    process_universe_constraints ctx.uctx_universes
-      ctx.uctx_univ_variables ctx.uctx_univ_algebraic
-      cstrs'
-  in
-    { ctx with uctx_local = (univs, Univ.Constraint.union local local');
-      uctx_univ_variables = vars;
-      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
-
-(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
-(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
-
-let add_universe_constraints_context ctx cstrs =
-  let univs, local = ctx.uctx_local in
-  let vars, local' = 
-    process_universe_constraints ctx.uctx_universes 
-      ctx.uctx_univ_variables ctx.uctx_univ_algebraic 
-      cstrs 
-  in
-    { ctx with uctx_local = (univs, Univ.Constraint.union local local');
-      uctx_univ_variables = vars;
-      uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
+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
+let evar_universe_context_constraints = UState.constraints
+let evar_context_universe_context = UState.context
+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 addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *)
 (* let add_universe_constraints_context =  *)
@@ -937,7 +736,7 @@ let evars_of_filtered_evar_info evi =
 (**********************************************************)
 (* Sort variables *)
 
-type rigid = 
+type rigid = UState.rigid =
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
 
@@ -947,146 +746,32 @@ let univ_flexible_alg = UnivFlexible true
 
 let evar_universe_context d = d.universes
 
-let universe_context_set d = d.universes.uctx_local
-
-let pr_uctx_level uctx = 
-  let map, map_rev = uctx.uctx_names in 
-    fun l ->
-      try str(Univ.LMap.find l map_rev)
-      with Not_found -> 
-	Universes.pr_with_global_universes l
-
-let universe_context ?names evd =
-  match names with
-  | None -> Univ.ContextSet.to_context evd.universes.uctx_local
-  | Some pl ->
-     let levels = Univ.ContextSet.levels evd.universes.uctx_local in
-     let newinst, left =
-       List.fold_right
-         (fun (loc,id) (newinst, acc) ->
-	  let l =
-	    try UNameMap.find (Id.to_string id) (fst evd.universes.uctx_names)
-	    with Not_found ->
-	      user_err_loc (loc, "universe_context",
-			    str"Universe " ++ pr_id id ++ str" is not bound anymore.")
-	  in (l :: newinst, Univ.LSet.remove l acc))
-	 pl ([], levels)
-     in
-       if not (Univ.LSet.is_empty left) then
-         let n = Univ.LSet.cardinal left in
-           errorlabstrm "universe_context"
-			(str(CString.plural n "Universe") ++ spc () ++
-			     Univ.LSet.pr (pr_uctx_level evd.universes) left ++
-			     spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")
-       else Univ.UContext.make (Univ.Instance.of_array (Array.of_list newinst),
-				Univ.ContextSet.constraints evd.universes.uctx_local)
+let universe_context_set d = UState.context_set Univ.UContext.empty d.universes
+
+let pr_uctx_level = UState.pr_uctx_level
+let universe_context ?names evd = UState.universe_context ?names evd.universes
 
 let restrict_universe_context evd vars =
-  let uctx = evd.universes in
-  let uctx' = Universes.restrict_universe_context uctx.uctx_local vars in
-    { evd with universes = { uctx with uctx_local = uctx' } }
-						 
+  { evd with universes = UState.restrict evd.universes vars }
+
 let universe_subst evd =
-  evd.universes.uctx_univ_variables
-
-let merge_uctx sideff rigid uctx ctx' =
-  let open Univ in
-  let levels = ContextSet.levels ctx' in
-  let uctx = if sideff then uctx else
-    match rigid with
-    | UnivRigid -> uctx
-    | UnivFlexible b ->
-      let fold u accu =
-        if LMap.mem u accu then accu
-        else LMap.add u None accu
-      in
-      let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in
-	if b then
-	  { uctx with uctx_univ_variables = uvars';
-	  uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
-	else { uctx with uctx_univ_variables = uvars' }
-  in
-  let uctx_local =
-    if sideff then uctx.uctx_local
-    else ContextSet.append ctx' uctx.uctx_local
-  in
-  let declare g =
-    LSet.fold (fun u g ->
-	       try UGraph.add_universe u false g
-	       with UGraph.AlreadyDeclared when sideff -> g)
-	      levels g
-  in
-  let initial = declare uctx.uctx_initial_universes in
-  let univs = declare uctx.uctx_universes in
-  let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
-    { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial }
+  UState.subst evd.universes
 
 let merge_context_set ?(sideff=false) rigid evd ctx' = 
-  {evd with universes = merge_uctx sideff rigid evd.universes ctx'}
+  {evd with universes = UState.merge sideff rigid evd.universes ctx'}
 
-let merge_uctx_subst uctx s =
-  { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s }
-      
 let merge_universe_subst evd subst = 
-  {evd with universes = merge_uctx_subst evd.universes subst }
+  {evd with universes = UState.merge_subst evd.universes subst }
 
 let with_context_set rigid d (a, ctx) = 
   (merge_context_set rigid d ctx, a)
 
-let emit_universe_side_effects eff u =
-  Declareops.fold_side_effects
-    (fun acc eff ->
-     match eff with
-     | Declarations.SEscheme (l,s) ->
-	List.fold_left
-	  (fun acc (_,_,cb,c) ->
-	   let acc = match c with
-	     | `Nothing -> acc
-	     | `Opaque (s, ctx) -> merge_uctx true univ_rigid acc ctx
-	   in if cb.Declarations.const_polymorphic then acc
-	      else
-		merge_uctx true univ_rigid acc
-			   (Univ.ContextSet.of_context cb.Declarations.const_universes))
-	  acc l
-     | Declarations.SEsubproof _ -> acc)
-    u eff
-        
-let add_uctx_names s l (names, names_rev) =
-    (UNameMap.add s l names, Univ.LMap.add l s names_rev)
-
-let uctx_new_univ_variable rigid name predicative
-  ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
-  let u = Universes.new_univ_level (Global.current_dirpath ()) in
-  let ctx' = Univ.ContextSet.add_universe u ctx in
-  let uctx', pred =
-    match rigid with
-    | UnivRigid -> uctx, true
-    | UnivFlexible b -> 
-      let uvars' = Univ.LMap.add u None uvars in
-	if b then {uctx with uctx_univ_variables = uvars';
-	  uctx_univ_algebraic = Univ.LSet.add u avars}, false
-	else {uctx with uctx_univ_variables = uvars'}, false
-  in
-  let names = 
-    match name with
-    | Some n -> add_uctx_names n u uctx.uctx_names
-    | None -> uctx.uctx_names
-  in
-  let initial =
-    UGraph.add_universe u false uctx.uctx_initial_universes
-  in						     
-  let uctx' =
-    {uctx' with uctx_names = names; uctx_local = ctx';
-		uctx_universes = UGraph.add_universe u false uctx.uctx_universes;
-		uctx_initial_universes = initial}
-  in uctx', u
-						     
 let new_univ_level_variable ?name ?(predicative=true) rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in
+  let uctx', u = UState.new_univ_variable rigid name evd.universes in
     ({evd with universes = uctx'}, u)
 
 let new_univ_variable ?name ?(predicative=true) rigid evd =
-  let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in
+  let uctx', u = UState.new_univ_variable rigid name evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
 let new_sort_variable ?name ?(predicative=true) rigid d =
@@ -1094,42 +779,12 @@ let new_sort_variable ?name ?(predicative=true) rigid d =
     (d', Type u)
 
 let add_global_univ d u =
-  let uctx = d.universes in
-  let initial =
-    UGraph.add_universe u true uctx.uctx_initial_universes
-  in
-  let univs = 
-    UGraph.add_universe u true uctx.uctx_universes
-  in
-    { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local;
-				     uctx_initial_universes = initial;
-				     uctx_universes = univs } }
-      
+  { d with universes = UState.add_global_univ d.universes u }
+
 let make_flexible_variable evd b u =
-  let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as ctx = evd.universes in
-  let uvars' = Univ.LMap.add u None uvars in
-  let avars' = 
-    if b then
-      let uu = Univ.Universe.make u in
-      let substu_not_alg u' v =
-	Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v
-      in
-	if not (Univ.LMap.exists substu_not_alg uvars)
-	then Univ.LSet.add u avars else avars 
-    else avars 
-  in
-    {evd with universes = {ctx with uctx_univ_variables = uvars'; 
-      uctx_univ_algebraic = avars'}}
-
-let make_evar_universe_context e l = 
-  let uctx = evar_universe_context_from e in
-    match l with
-    | None -> uctx
-    | Some us ->
-       List.fold_left
-	 (fun uctx (loc,id) ->
-	  fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) true uctx))
-	 uctx us
+  { evd with universes = UState.make_flexible_variable evd.universes b u }
+
+let make_evar_universe_context = UState.make
     
 (****************************************)
 (* Operations on constants              *)
@@ -1152,20 +807,11 @@ let fresh_global ?(rigid=univ_flexible) ?names env evd gr =
 
 let whd_sort_variable evd t = t
 
-let is_sort_variable evd s = 
-  match s with 
-  | Type u -> 
-    (match Univ.universe_level u with
-    | Some l as x -> 
-      let uctx = evd.universes in
-	if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x
-	else None
-    | None -> None)
-  | _ -> None
+let is_sort_variable evd s = UState.is_sort_variable evd.universes s
 
 let is_flexible_level evd l = 
   let uctx = evd.universes in
-    Univ.LMap.mem l uctx.uctx_univ_variables
+    Univ.LMap.mem l (UState.subst uctx)
 
 let is_eq_sort s1 s2 =
   if Sorts.equal s1 s2 then None
@@ -1176,12 +822,12 @@ let is_eq_sort s1 s2 =
       else Some (u1, u2)
 
 let normalize_universe evd =
-  let vars = ref evd.universes.uctx_univ_variables in
+  let vars = ref (UState.subst evd.universes) in
   let normalize = Universes.normalize_universe_opt_subst vars in
     normalize
 
 let normalize_universe_instance evd l =
-  let vars = ref evd.universes.uctx_univ_variables in
+  let vars = ref (UState.subst evd.universes) in
   let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
     Univ.Instance.subst_fn normalize l
 
@@ -1239,96 +885,28 @@ let set_leq_sort env evd s1 s2 =
       else evd
 	    
 let check_eq evd s s' =
-  UGraph.check_eq evd.universes.uctx_universes s s'
+  UGraph.check_eq (UState.ugraph evd.universes) s s'
 
 let check_leq evd s s' =
-  UGraph.check_leq evd.universes.uctx_universes s s'
-
-let subst_univs_context_with_def def usubst (ctx, cst) =
-  (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
+  UGraph.check_leq (UState.ugraph evd.universes) s s'
 
-let normalize_evar_universe_context_variables uctx =
-  let normalized_variables, undef, def, subst = 
-    Universes.normalize_univ_variables uctx.uctx_univ_variables 
-  in
-  let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in
-  let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in
-    subst, { uctx with uctx_local = ctx_local';
-      uctx_univ_variables = normalized_variables;
-      uctx_universes = univs }
+let normalize_evar_universe_context_variables = UState.normalize_variables
 
 (* let normvarsconstrkey = Profile.declare_profile "normalize_evar_universe_context_variables";; *)
 (* let normalize_evar_universe_context_variables = *)
 (*   Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *)
     
-let abstract_undefined_variables uctx =
-  let vars' = 
-    Univ.LMap.fold (fun u v acc ->
-      if v == None then Univ.LSet.remove u acc
-      else acc)
-    uctx.uctx_univ_variables uctx.uctx_univ_algebraic
-  in { uctx with uctx_local = Univ.ContextSet.empty;
-      uctx_univ_algebraic = vars' }
-
-let fix_undefined_variables ({ universes = uctx } as evm) =
-  let algs', vars' = 
-    Univ.LMap.fold (fun u v (algs, vars as acc) ->
-      if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars)
-      else acc)
-      uctx.uctx_univ_variables 
-      (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables)
-  in
-    {evm with universes = 
-	{ uctx with uctx_univ_variables = vars';
-	  uctx_univ_algebraic = algs' } }
+let abstract_undefined_variables = UState.abstract_undefined_variables
 
-
-let refresh_undefined_univ_variables uctx =
-  let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
-  let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc) 
-    uctx.uctx_univ_algebraic Univ.LSet.empty 
-  in
-  let vars = 
-    Univ.LMap.fold
-      (fun u v acc ->
-	Univ.LMap.add (Univ.subst_univs_level_level subst u) 
-          (Option.map (Univ.subst_univs_level_universe subst) v) acc)
-      uctx.uctx_univ_variables Univ.LMap.empty
-  in
-  let declare g = Univ.LSet.fold (fun u g -> UGraph.add_universe u false g)
-				   (Univ.ContextSet.levels ctx') g in
-  let initial = declare uctx.uctx_initial_universes in
-  let univs = declare UGraph.initial_universes in
-  let uctx' = {uctx_names = uctx.uctx_names;
-	       uctx_local = ctx'; 
-	       uctx_univ_variables = vars; uctx_univ_algebraic = alg;
-	       uctx_universes = univs;
-	       uctx_initial_universes = initial } in
-    uctx', subst
+let fix_undefined_variables evd =
+  { evd with universes = UState.fix_undefined_variables evd.universes }
 
 let refresh_undefined_universes evd =
-  let uctx', subst = refresh_undefined_univ_variables evd.universes in
+  let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in
   let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in
     evd', subst
 
-let normalize_evar_universe_context uctx = 
-  let rec fixpoint uctx = 
-    let ((vars',algs'), us') = 
-      Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables
-        uctx.uctx_univ_algebraic
-    in
-      if Univ.ContextSet.equal us' uctx.uctx_local then uctx
-      else
-	let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in
-	let uctx' = 
-	  { uctx_names = uctx.uctx_names;
-	    uctx_local = us'; 
-	    uctx_univ_variables = vars'; 
-	    uctx_univ_algebraic = algs';
-	    uctx_universes = universes;
-	    uctx_initial_universes = uctx.uctx_initial_universes }
-	in fixpoint uctx'
-  in fixpoint uctx
+let normalize_evar_universe_context = UState.normalize
 
 let nf_univ_variables evd = 
   let subst, uctx' = normalize_evar_universe_context_variables evd.universes in
@@ -1346,14 +924,12 @@ let nf_constraints =
       Profile.profile1 nfconstrkey nf_constraints
   else nf_constraints
 
-let universe_of_name evd s = 
-  UNameMap.find s (fst evd.universes.uctx_names)
+let universe_of_name evd s = UState.universe_of_name evd.universes s
 
 let add_universe_name evd s l =
-  let names' = add_uctx_names s l evd.universes.uctx_names in
-    {evd with universes = {evd.universes with uctx_names = names'}}
+  { evd with universes = UState.add_universe_name evd.universes s l }
 
-let universes evd = evd.universes.uctx_universes
+let universes evd = UState.ugraph evd.universes
 
 (* Conversion w.r.t. an evar map and its local universes. *)
 
@@ -1362,10 +938,10 @@ let conversion_gen env evd pb t u =
   | Reduction.CONV -> 
     Reduction.trans_conv_universes 
       full_transparent_state ~evars:(existential_opt_value evd) env 
-      evd.universes.uctx_universes t u
+      (UState.ugraph evd.universes) t u
   | Reduction.CUMUL -> Reduction.trans_conv_leq_universes
      full_transparent_state ~evars:(existential_opt_value evd) env 
-    evd.universes.uctx_universes t u
+      (UState.ugraph evd.universes) t u
 
 (* let conversion_gen_key = Profile.declare_profile "conversion_gen" *)
 (* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *)
@@ -1377,8 +953,10 @@ let test_conversion env d pb t u =
   try conversion_gen env d pb t u; true
   with _ -> false
 
+exception UniversesDiffer = UState.UniversesDiffer
+
 let eq_constr_univs evd t u =
-  let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in
+  let b, c = Universes.eq_constr_univs_infer (UState.ugraph evd.universes) t u in
     if b then 
       try let evd' = add_universe_constraints evd c in evd', b
       with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false
@@ -1393,7 +971,7 @@ let e_eq_constr_univs evdref t u =
 
 let emit_side_effects eff evd =
   { evd with effects = Declareops.union_side_effects eff evd.effects;
-	     universes = emit_universe_side_effects eff evd.universes }
+	     universes = UState.emit_side_effects eff evd.universes }
 
 let drop_side_effects evd =
   { evd with effects = Declareops.no_seff; }
@@ -1760,11 +1338,11 @@ 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 ctx.uctx_local) ++ fnl () ++
+       h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set Univ.UContext.empty ctx)) ++ fnl () ++
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
-     h 0 (Univ.LSet.pr prl ctx.uctx_univ_algebraic) ++ fnl() ++
+     h 0 (Univ.LSet.pr prl (UState.variables ctx)) ++ fnl() ++
      str"UNDEFINED UNIVERSES:"++brk(0,1)++
-       h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables) ++ fnl())
+       h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl())
 
 let print_env_short env =
   let pr_body n = function
-- 
cgit v1.2.3


From d558bf5289e87899a850dda410a3a3c4de1ce979 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 17 Oct 2015 18:55:42 +0200
Subject: Clarifying and documenting the UState API.

---
 engine/evd.ml | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

(limited to 'engine/evd.ml')

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())
 
-- 
cgit v1.2.3


From 103ec7205d9038f1f3821f9287e3bb0907a1e3ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 19 Nov 2015 13:36:31 +0100
Subject: More efficient implementation of equality-up-to-universes in
 Universes.

Instead of accumulating constraints which are not present in the original
graph, we parametrize the equality function by a function actually merging
those constraints in the current graph. This prevents doing the work twice.
---
 engine/evd.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 069fcbfa6e..00a869fda8 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -962,11 +962,13 @@ let test_conversion env d pb t u =
 exception UniversesDiffer = UState.UniversesDiffer
 
 let eq_constr_univs evd t u =
-  let b, c = Universes.eq_constr_univs_infer (UState.ugraph evd.universes) t u in
-    if b then 
-      try let evd' = add_universe_constraints evd c in evd', b
-      with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false
-    else evd, b
+  let fold cstr sigma =
+    try Some (add_universe_constraints sigma cstr)
+    with Univ.UniverseInconsistency _ | UniversesDiffer -> None
+  in
+  match Universes.eq_constr_univs_infer (UState.ugraph evd.universes) fold t u evd with
+  | None -> evd, false
+  | Some evd -> evd, true
 
 let e_eq_constr_univs evdref t u =
   let evd, b = eq_constr_univs !evdref t u in
-- 
cgit v1.2.3


From f7030a3358dda9bbc6de8058ab3357be277c031a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 Nov 2015 14:19:37 +0100
Subject: Remove unneeded fixpoint in normalize_context_set. Note that it is no
 longer stable w.r.t. equality constraints as the universe graph will choose
 different canonical levels depending on the equalities given to it (l = r vs
 r = l).

---
 engine/evd.ml | 34 ++++++----------------------------
 1 file changed, 6 insertions(+), 28 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 00a869fda8..425b67e080 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -275,9 +275,6 @@ let add_universe_constraints_context = UState.add_universe_constraints
 let constrain_variables = UState.constrain_variables 
 let evar_universe_context_of_binders = UState.of_binders
 
-(* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *)
-(* let add_universe_constraints_context =  *)
-(*   Profile.profile2 addunivconstrkey add_universe_constraints_context;; *)
 (*******************************************************************)
 (* Metamaps *)
 
@@ -860,12 +857,9 @@ let set_eq_sort env d s1 s2 =
       d
 
 let has_lub evd u1 u2 =
-  (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *)
-  (* (\* let dref, norm = memo_normalize_universe d in *\) *)
-  (* let u1 = normalize u1 and u2 = normalize u2 in *)
-    if Univ.Universe.equal u1 u2 then evd
-    else add_universe_constraints evd
-      (Universes.Constraints.singleton (u1,Universes.ULub,u2))
+  if Univ.Universe.equal u1 u2 then evd
+  else add_universe_constraints evd
+    (Universes.Constraints.singleton (u1,Universes.ULub,u2))
 
 let set_eq_level d u1 u2 =
   add_constraints d (Univ.enforce_eq_level u1 u2 Univ.Constraint.empty)
@@ -883,15 +877,9 @@ let set_leq_sort env evd s1 s2 =
   match is_eq_sort s1 s2 with
   | None -> evd
   | Some (u1, u2) ->
-    (* if Univ.is_type0_univ u2 then *)
-    (*   if Univ.is_small_univ u1 then evd *)
-    (*   else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
-    (* else if Univ.is_type0m_univ u2 then  *)
-    (*   raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
-    (* else  *)
-      if not (type_in_type env) then
-      add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2))
-      else evd
+     if not (type_in_type env) then
+       add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2))
+     else evd
 	    
 let check_eq evd s s' =
   UGraph.check_eq (UState.ugraph evd.universes) s s'
@@ -901,10 +889,6 @@ let check_leq evd s s' =
 
 let normalize_evar_universe_context_variables = UState.normalize_variables
 
-(* let normvarsconstrkey = Profile.declare_profile "normalize_evar_universe_context_variables";; *)
-(* let normalize_evar_universe_context_variables = *)
-(*   Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *)
-    
 let abstract_undefined_variables = UState.abstract_undefined_variables
 
 let fix_undefined_variables evd =
@@ -927,12 +911,6 @@ let nf_constraints evd =
   let uctx' = normalize_evar_universe_context uctx' in
     {evd with universes = uctx'}
 
-let nf_constraints = 
-  if Flags.profile then
-    let nfconstrkey = Profile.declare_profile "nf_constraints" in
-      Profile.profile1 nfconstrkey nf_constraints
-  else nf_constraints
-
 let universe_of_name evd s = UState.universe_of_name evd.universes s
 
 let add_universe_name evd s l =
-- 
cgit v1.2.3


From 39b13903e7a6824f4405f61bb4b41a30cfbd0b3c Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 9 Dec 2015 12:30:32 +0100
Subject: CLEANUP: in the Reduction module

---
 engine/evd.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 425b67e080..2060141644 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -926,10 +926,10 @@ let update_sigma_env evd env =
 let test_conversion_gen env evd pb t u =
   match pb with 
   | Reduction.CONV -> 
-    Reduction.trans_conv_universes 
+    Reduction.conv_universes 
       full_transparent_state ~evars:(existential_opt_value evd) env 
       (UState.ugraph evd.universes) t u
-  | Reduction.CUMUL -> Reduction.trans_conv_leq_universes
+  | Reduction.CUMUL -> Reduction.conv_leq_universes
      full_transparent_state ~evars:(existential_opt_value evd) env 
       (UState.ugraph evd.universes) t u
 
-- 
cgit v1.2.3


From 672f8ee0c96584735294641bb4b8760e25197b80 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 14 Dec 2015 12:52:49 +0100
Subject: CLEANUP: in the Reduction module

---
 engine/evd.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 2060141644..6651ff5f63 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -926,12 +926,12 @@ let update_sigma_env evd env =
 let test_conversion_gen env evd pb t u =
   match pb with 
   | Reduction.CONV -> 
-    Reduction.conv_universes 
-      full_transparent_state ~evars:(existential_opt_value evd) env 
-      (UState.ugraph evd.universes) t u
-  | Reduction.CUMUL -> Reduction.conv_leq_universes
-     full_transparent_state ~evars:(existential_opt_value evd) env 
-      (UState.ugraph evd.universes) t u
+    Reduction.conv env
+      ~evars:((existential_opt_value evd), (UState.ugraph evd.universes))
+      t u
+  | Reduction.CUMUL -> Reduction.conv_leq env
+      ~evars:((existential_opt_value evd), (UState.ugraph evd.universes))
+      t u
 
 let test_conversion env d pb t u =
   try test_conversion_gen env d pb t u; true
-- 
cgit v1.2.3


From 2c8275ee3e0e5cd4eb8afd24047fda7f864e0e4e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sat, 2 Jan 2016 16:50:02 +0100
Subject: Remove useless rec flags.

---
 engine/evd.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index d91b90caa2..8476db6646 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1230,7 +1230,7 @@ let pr_decl ((id,b,_),ok) =
   | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
       print_constr c ++ str (if ok then ")" else "}")
 
-let rec pr_evar_source = function
+let pr_evar_source = function
   | Evar_kinds.QuestionMark _ -> str "underscore"
   | Evar_kinds.CasesType false -> str "pattern-matching return predicate"
   | Evar_kinds.CasesType true ->
-- 
cgit v1.2.3


From 34ef02fac1110673ae74c41c185c228ff7876de2 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 29 Jan 2016 10:13:12 +0100
Subject: CLEANUP: Context.{Rel,Named}.Declaration.t

  Originally, rel-context was represented as:

    Context.rel_context = Names.Name.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
                  | LocalDef of Names.Name.t * Constr.t * Constr.t

  Originally, named-context was represented as:

    Context.named_context = Names.Id.t * Constr.t option * Constr.t

  Now it is represented as:

    Context.Named.t = LocalAssum of Names.Id.t * Constr.t
                    | LocalDef of Names.Id.t * Constr.t * Constr.t

Motivation:

  (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
      function which looked like this:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      Suppose that you do not know about rel-context and named-context.
      (that is the case of people who just started to read the source code)
      Merlin would tell you that the type of the value you are destructing
      by "match" is:

        'a * 'b option * Constr.t                    (* worst-case scenario *)

      or

        Named.Name.t * Constr.t option * Constr.t    (* best-case scenario (?) *)

      To me, this is akin to wearing an opaque veil.
      It is hard to figure out the meaning of the values you are looking at.
      In particular, it is hard to discover the connection between the value
      we are destructing above and the datatypes and functions defined
      in the "kernel/context.ml" file.

      In this case, the connection is there, but it is not visible
      (between the function above and the "Context" module).

      ------------------------------------------------------------------------

      Now consider, what happens when the reader see the same function
      presented in the following form:

        let test_strict_disjunction n lc =
          Array.for_all_i (fun i c ->
            match (prod_assum (snd (decompose_prod_n_assum n c))) with
            | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
            | _ -> false) 0 lc

      If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
      to jump to the corresponding definition and learn more.

      In this case, the connection is there, and it is directly visible
      (between the function above and the "Context" module).

  (2) Also, if we already have the concepts such as:
      - local declaration
      - local assumption
      - local definition
      and we describe these notions meticulously in the Reference Manual,
      then it is a real pity not to reinforce the connection
      of the actual code with the abstract description we published.
---
 engine/evd.ml | 27 +++++++++++++++------------
 1 file changed, 15 insertions(+), 12 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 8f8b29d106..f1f65bd8af 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -16,6 +16,7 @@ open Vars
 open Termops
 open Environ
 open Globnames
+open Context.Named.Declaration
 
 (** Generic filters *)
 module Filter :
@@ -230,20 +231,20 @@ let evar_instance_array test_id info args =
     else instance_mismatch ()
   | false :: filter, _ :: ctxt ->
     instrec filter ctxt i
-  | true :: filter, (id,_,_ as d) :: ctxt ->
+  | true :: filter, d :: ctxt ->
     if i < len then
       let c = Array.unsafe_get args i in
       if test_id d c then instrec filter ctxt (succ i)
-      else (id, c) :: instrec filter ctxt (succ i)
+      else (get_id d, c) :: instrec filter ctxt (succ i)
     else instance_mismatch ()
   | _ -> instance_mismatch ()
   in
   match Filter.repr (evar_filter info) with
   | None ->
-    let map i (id,_,_ as d) =
+     let map i d =
       if (i < len) then
         let c = Array.unsafe_get args i in
-        if test_id d c then None else Some (id,c)
+        if test_id d c then None else Some (get_id d, c)
       else instance_mismatch ()
     in
     List.map_filter_i map (evar_context info)
@@ -251,7 +252,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array (fun (id,_,_) -> isVarId id) info args
+  evar_instance_array (isVarId % get_id) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
@@ -660,7 +661,7 @@ let restrict evk filter ?candidates evd =
       evar_extra = Store.empty } in
   let evar_names = reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
-  let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in
+  let id_inst = Array.map_of_list (mkVar % get_id) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
@@ -722,10 +723,10 @@ let evars_of_term c =
   evrec Evar.Set.empty c
 
 let evars_of_named_context nc =
-  List.fold_right (fun (_, b, t) s ->
+  List.fold_right (fun decl s ->
     Option.fold_left (fun s t ->
       Evar.Set.union s (evars_of_term t))
-      (Evar.Set.union s (evars_of_term t)) b)
+      (Evar.Set.union s (evars_of_term (get_type decl))) (get_value decl))
     nc Evar.Set.empty
 
 let evars_of_filtered_evar_info evi =
@@ -1228,8 +1229,9 @@ let pr_meta_map mmap =
   in
   prlist pr_meta_binding (metamap_to_list mmap)
 
-let pr_decl ((id,b,_),ok) =
-  match b with
+let pr_decl (decl,ok) =
+  let id = get_id decl in
+  match get_value decl with
   | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
   | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++
       print_constr c ++ str (if ok then ")" else "}")
@@ -1346,8 +1348,9 @@ let print_env_short env =
   let pr_body n = function
   | None -> pr_name n
   | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in
-  let pr_named_decl (n, b, _) = pr_body (Name n) b in
-  let pr_rel_decl (n, b, _) = pr_body n b in
+  let pr_named_decl decl = pr_body (Name (get_id decl)) (get_value decl) in
+  let pr_rel_decl decl = let open Context.Rel.Declaration in
+                         pr_body (get_name decl) (get_value decl) in
   let nc = List.rev (named_context env) in
   let rc = List.rev (rel_context env) in
     str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++
-- 
cgit v1.2.3


From 8d0ff142913fc6351ff7f0a6b8eacc6c21d36000 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 19 Feb 2016 15:12:53 +0100
Subject: Allowing to attach location to universes in UState.

---
 engine/evd.ml | 42 +++++++++++++++++++++---------------------
 1 file changed, 21 insertions(+), 21 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index f751f4d922..b6849f7ffb 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -781,25 +781,25 @@ let restrict_universe_context evd vars =
 let universe_subst evd =
   UState.subst evd.universes
 
-let merge_context_set ?(sideff=false) rigid evd ctx' = 
-  {evd with universes = UState.merge sideff rigid evd.universes ctx'}
+let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
+  {evd with universes = UState.merge ?loc sideff rigid evd.universes ctx'}
 
 let merge_universe_subst evd subst = 
   {evd with universes = UState.merge_subst evd.universes subst }
 
-let with_context_set rigid d (a, ctx) = 
-  (merge_context_set rigid d ctx, a)
+let with_context_set ?loc rigid d (a, ctx) =
+  (merge_context_set ?loc rigid d ctx, a)
 
-let new_univ_level_variable ?name ?(predicative=true) rigid evd =
-  let uctx', u = UState.new_univ_variable rigid name evd.universes in
+let new_univ_level_variable ?loc ?name ?(predicative=true) rigid evd =
+  let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in
     ({evd with universes = uctx'}, u)
 
-let new_univ_variable ?name ?(predicative=true) rigid evd =
-  let uctx', u = UState.new_univ_variable rigid name evd.universes in
+let new_univ_variable ?loc ?name ?(predicative=true) rigid evd =
+  let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in
     ({evd with universes = uctx'}, Univ.Universe.make u)
 
-let new_sort_variable ?name ?(predicative=true) rigid d =
-  let (d', u) = new_univ_variable rigid ?name ~predicative d in
+let new_sort_variable ?loc ?name ?(predicative=true) rigid d =
+  let (d', u) = new_univ_variable ?loc rigid ?name ~predicative d in
     (d', Type u)
 
 let add_global_univ d u =
@@ -815,27 +815,27 @@ let make_evar_universe_context e l =
   | Some us ->
       List.fold_left
         (fun uctx (loc,id) ->
-        fst (UState.new_univ_variable univ_rigid (Some (Id.to_string id)) uctx))
+        fst (UState.new_univ_variable ~loc univ_rigid (Some (Id.to_string id)) uctx))
         uctx us
 
 (****************************************)
 (* Operations on constants              *)
 (****************************************)
 
-let fresh_sort_in_family ?(rigid=univ_flexible) env evd s = 
-  with_context_set rigid evd (Universes.fresh_sort_in_family env s)
+let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = 
+  with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s)
 
-let fresh_constant_instance env evd c =
-  with_context_set univ_flexible evd (Universes.fresh_constant_instance env c)
+let fresh_constant_instance ?loc env evd c =
+  with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c)
 
-let fresh_inductive_instance env evd i =
-  with_context_set univ_flexible evd (Universes.fresh_inductive_instance env i)
+let fresh_inductive_instance ?loc env evd i =
+  with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i)
 
-let fresh_constructor_instance env evd c =
-  with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c)
+let fresh_constructor_instance ?loc env evd c =
+  with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env c)
 
-let fresh_global ?(rigid=univ_flexible) ?names env evd gr =
-  with_context_set rigid evd (Universes.fresh_global_instance ?names env gr)
+let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
+  with_context_set ?loc rigid evd (Universes.fresh_global_instance ?names env gr)
 
 let whd_sort_variable evd t = t
 
-- 
cgit v1.2.3