Merge PR #15837: Reduce Universe.t footprint

Reviewed-by: SkySkimmer
Ack-by: mattam82
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

checker/checkInductive.ml

@@ -55,7 +55,7 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
         | TemplateArity ar ->
           let ctx = ind.mind_arity_ctxt in
           let ctx = List.firstn (List.length ctx - nparams) ctx in
-          Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level)
+          Term.mkArity (ctx, ar.template_level)
       in
       {
         mind_entry_typename = ind.mind_typename;
@@ -86,7 +86,7 @@ let check_arity env ar1 ar2 = match ar1, ar2 with
     Constr.equal ar.mind_user_arity mind_user_arity &&
     Sorts.equal ar.mind_sort mind_sort
   | TemplateArity ar, TemplateArity {template_level} ->
-    UGraph.check_leq (universes env) template_level ar.template_level
+    Sorts.check_leq_sort (universes env) template_level ar.template_level
     (* template_level is inferred by indtypes, so functor application can produce a smaller one *)
   | (RegularArity _ | TemplateArity _), _ -> assert false
 

checker/values.ml

@@ -222,7 +222,7 @@ let v_oracle =
   |]
 
 let v_template_arity =
-  v_tuple "template_arity" [|v_univ|]
+  v_tuple "template_arity" [|v_sort|]
 
 let v_template_universes =
   v_tuple "template_universes" [|List(Opt v_level);v_context_set|]

dev/ci/user-overlays/15837-ppedrot-reduce-universe-footprint.sh

@@ -0,0 +1,7 @@
+overlay elpi https://github.com/ppedrot/coq-elpi reduce-universe-footprint 15837
+
+overlay metacoq https://github.com/ppedrot/metacoq reduce-universe-footprint 15837
+
+overlay mtac2 https://github.com/ppedrot/Mtac2 reduce-universe-footprint 15837
+
+overlay unicoq https://github.com/ppedrot/unicoq reduce-universe-footprint 15837

engine/eConstr.ml

@@ -480,21 +480,18 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
   let open UnivProblem in
   if not nargs_ok then enforce_eq_instances_univs false u u' cstrs
   else
+    let make u = Sorts.sort_of_univ @@ Univ.Universe.make u in
     CArray.fold_left3
       (fun cstrs v u u' ->
          let open Univ.Variance in
          match v with
          | Irrelevant -> Set.add (UWeak (u,u')) cstrs
          | Covariant ->
-           let u = Univ.Universe.make u in
-           let u' = Univ.Universe.make u' in
            (match cv_pb with
-            | Reduction.CONV -> Set.add (UEq (u,u')) cstrs
-            | Reduction.CUMUL -> Set.add (ULe (u,u')) cstrs)
+            | Reduction.CONV -> Set.add (UEq (make u, make u')) cstrs
+            | Reduction.CUMUL -> Set.add (ULe (make u, make u')) cstrs)
          | Invariant ->
-           let u = Univ.Universe.make u in
-           let u' = Univ.Universe.make u' in
-           Set.add (UEq (u,u')) cstrs)
+           Set.add (UEq (make u, make u')) cstrs)
       cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
 
 let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
@@ -554,7 +551,7 @@ let test_constr_universes env sigma leq ?(nargs=0) m n =
       let s2 = ESorts.kind sigma s2 in
       if Sorts.equal s1 s2 then true
       else (cstrs := Set.add
-              (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
+              (UEq (s1, s2)) !cstrs;
             true)
     in
     let leq_sorts s1 s2 =
@@ -563,7 +560,7 @@ let test_constr_universes env sigma leq ?(nargs=0) m n =
       if Sorts.equal s1 s2 then true
       else
         (cstrs := Set.add
-           (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
+           (ULe (s1, s2)) !cstrs;
          true)
     in
     let rec eq_constr' nargs m n = compare_gen kind eq_universes eq_sorts eq_constr' nargs m n in
@@ -610,7 +607,7 @@ let eq_constr_universes_proj env sigma m n =
       if Sorts.equal s1 s2 then true
       else
         (cstrs := Set.add
-           (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs;
+           (UEq (s1, s2)) !cstrs;
          true)
     in
     let rec eq_constr' nargs m n =
@@ -631,8 +628,7 @@ let universes_of_constr sigma c =
       let sort = ESorts.kind sigma u in
       if Sorts.is_small sort then s
       else
-        let u = Sorts.univ_of_sort sort in
-        Level.Set.fold Level.Set.add (Universe.levels u) s
+        Level.Set.fold Level.Set.add (Sorts.levels sort) s
     | Evar (k, args) ->
       let concl = Evd.evar_concl (Evd.find sigma k) in
       fold sigma aux (aux s concl) c

engine/evarutil.ml

@@ -832,8 +832,8 @@ let occur_evar_upto sigma n c =
 
 let judge_of_new_Type evd =
   let open EConstr in
-  let (evd', s) = new_univ_variable univ_rigid evd in
-  (evd', { uj_val = mkType s; uj_type = mkType (Univ.super s) })
+  let (evd', s) = new_sort_variable univ_rigid evd in
+  (evd', { uj_val = mkSort s; uj_type = mkSort (Sorts.super s) })
 
 let subterm_source evk ?where (loc,k) =
   let evk = match k with
@@ -888,8 +888,7 @@ let eq_constr_univs_test ~evd ~extended_evd t u =
   let eq_sorts s1 s2 =
     if Sorts.equal s1 s2 then true
     else
-      let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-      try sigma := add_universe_constraints !sigma UnivProblem.(Set.singleton (UEq (u1, u2))); true
+      try sigma := add_universe_constraints !sigma UnivProblem.(Set.singleton (UEq (s1, s2))); true
       with Univ.UniverseInconsistency _ | UniversesDiffer -> false
   in
   let kind1 = kind_of_term_upto evd in

engine/evd.ml

@@ -997,11 +997,7 @@ let is_flexible_level evd l =
 
 let is_eq_sort s1 s2 =
   if Sorts.equal s1 s2 then None
-  else
-    let u1 = univ_of_sort s1
-    and u2 = univ_of_sort s2 in
-      if Univ.Universe.equal u1 u2 then None
-      else Some (u1, u2)
+  else Some (s1, s2)
 
 (* Precondition: l is not defined in the substitution *)
 let universe_rigidity evd l =
@@ -1060,10 +1056,10 @@ let set_leq_sort env evd s1 s2 =
      else evd
 
 let check_eq evd s s' =
-  UGraph.check_eq (UState.ugraph evd.universes) s s'
+  Sorts.check_eq_sort (UState.ugraph evd.universes) s s'
 
 let check_leq evd s s' =
-  UGraph.check_leq (UState.ugraph evd.universes) s s'
+  Sorts.check_leq_sort (UState.ugraph evd.universes) s s'
 
 let check_constraints evd csts =
   UGraph.check_constraints csts (UState.ugraph evd.universes)

engine/evd.mli

@@ -619,7 +619,6 @@ val universe_of_name : evar_map -> Id.t -> Univ.Level.t
 val universe_binders : evar_map -> UnivNames.universe_binders
 
 val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t
-val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t
 val new_sort_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Sorts.t
 
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
@@ -637,8 +636,6 @@ val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option
 
 val is_flexible_level : evar_map -> Univ.Level.t -> bool
 
-(* val normalize_universe_level : evar_map -> Univ.Level.t -> Univ.Level.t *)
-val normalize_universe : evar_map -> Univ.Universe.t -> Univ.Universe.t
 val normalize_universe_instance : evar_map -> Univ.Instance.t -> Univ.Instance.t
 
 val set_leq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
@@ -648,8 +645,8 @@ val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
 val set_eq_instances : ?flex:bool ->
   evar_map -> Univ.Instance.t -> Univ.Instance.t -> evar_map
 
-val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
-val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool
+val check_eq : evar_map -> Sorts.t -> Sorts.t -> bool
+val check_leq : evar_map -> Sorts.t -> Sorts.t -> bool
 
 val check_constraints : evar_map -> Univ.Constraints.t -> bool
 

engine/uState.ml

@@ -175,7 +175,7 @@ let universe_binders uctx =
   named
 
 let instantiate_variable l b v =
-  try v := Level.Map.set l (Some b) !v
+  try v := Level.Map.set l (Some (Sorts.univ_of_sort b)) !v
   with Not_found -> assert false
 
 exception UniversesDiffer
@@ -186,6 +186,12 @@ let drop_weak_constraints =
     ~key:["Cumulativity";"Weak";"Constraints"]
     ~value:false
 
+let sort_inconsistency cst l r =
+  raise (UniverseInconsistency (cst, Sorts.univ_of_sort l, Sorts.univ_of_sort r, None))
+
+let subst_univs_sort normalize s =
+  Sorts.sort_of_univ (subst_univs_universe normalize (Sorts.univ_of_sort s))
+
 let process_universe_constraints uctx cstrs =
   let open UnivSubst in
   let open UnivProblem in
@@ -196,12 +202,12 @@ let process_universe_constraints uctx cstrs =
   let nf_constraint = function
     | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v)
     | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v)
-    | UEq (u, v) -> UEq (subst_univs_universe normalize u, subst_univs_universe normalize v)
-    | ULe (u, v) -> ULe (subst_univs_universe normalize u, subst_univs_universe normalize v)
+    | UEq (u, v) -> UEq (subst_univs_sort normalize u, subst_univs_sort normalize v)
+    | ULe (u, v) -> ULe (subst_univs_sort normalize u, subst_univs_sort normalize v)
   in
   let is_local l = Level.Map.mem l !vars in
   let varinfo x =
-    match Universe.level x with
+    match Universe.level (Sorts.univ_of_sort x) with
     | None -> Inl x
     | Some l -> Inr l
   in
@@ -216,7 +222,7 @@ let process_universe_constraints uctx cstrs =
         (* Two rigid/global levels, none of them being local,
             one of them being Prop/Set, disallow *)
         if Level.is_small l' || Level.is_small r' then
-          raise (UniverseInconsistency (Eq, l, r, None))
+          sort_inconsistency Eq l r
         else if fo then
           raise UniversesDiffer
     in
@@ -226,49 +232,50 @@ let process_universe_constraints uctx cstrs =
   | Inr l', Inr r' -> equalize_variables false l l' r r' local
   | Inr l, Inl r | Inl r, Inr l ->
     let alg = Level.Set.mem l uctx.univ_algebraic in
-    let inst = univ_level_rem l r r in
+    let ru = Sorts.univ_of_sort r in
+    let inst = univ_level_rem l ru ru in
       if alg && not (Level.Set.mem l (Universe.levels inst)) then
-        (instantiate_variable l inst vars; local)
+        (instantiate_variable l (Sorts.sort_of_univ inst) vars; local)
       else
         let lu = Universe.make l in
-        if univ_level_mem l r then
+        if univ_level_mem l ru then
           enforce_leq inst lu local
-        else raise (UniverseInconsistency (Eq, lu, r, None))
+        else sort_inconsistency Eq (Sorts.sort_of_univ lu) r
   | Inl _, Inl _ (* both are algebraic *) ->
-    if UGraph.check_eq univs l r then local
-    else raise (UniverseInconsistency (Eq, l, r, None))
+    if Sorts.check_eq_sort univs l r then local
+    else sort_inconsistency Eq l r
   in
   let unify_universes cst local =
     let cst = nf_constraint cst in
       if UnivProblem.is_trivial cst then local
       else
           match cst with
           | ULe (l, r) ->
-            begin match Univ.Universe.level r with
+            begin match Univ.Universe.level (Sorts.univ_of_sort r) with
             | None ->
-              if UGraph.check_leq univs l r then local
+              if Sorts.check_leq_sort univs l r then local
               else user_err Pp.(str "Algebraic universe on the right")
             | Some r' ->
               if Level.is_small r' then
-                  if not (Universe.is_levels l)
+                  if not (Universe.is_levels (Sorts.univ_of_sort l))
                   then (* l contains a +1 and r=r' small so l <= r impossible *)
-                    raise (UniverseInconsistency (Le, l, r, None))
+                    sort_inconsistency Le l r
                   else
-                    if UGraph.check_leq univs l r then match Univ.Universe.level l with
+                    if Sorts.check_leq_sort univs l r then match Univ.Universe.level (Sorts.univ_of_sort l) with
                     | Some l ->
                       Univ.Constraints.add (l, Le, r') local
                     | None -> local
                     else
-                    let levels = Universe.levels l in
+                    let levels = Sorts.levels l in
                     let fold l' local =
-                      let l = Universe.make l' in
+                      let l = Sorts.sort_of_univ @@ Universe.make l' in
                       if Level.is_small l' || is_local l' then
                         equalize_variables false l l' r r' local
-                      else raise (UniverseInconsistency (Le, l, r, None))
+                      else sort_inconsistency Le l r
                     in
                     Level.Set.fold fold levels local
               else
-                match Univ.Universe.level l with
+                match Univ.Universe.level (Sorts.univ_of_sort l) with
                 | Some l ->
                   Univ.Constraints.add (l, Le, r') local
                 | None ->
@@ -280,10 +287,10 @@ let process_universe_constraints uctx cstrs =
                      Hence, by doing this, we avoid a costly check here, and
                      make further checks of this constraint easier since it will
                      exist directly in the graph. *)
-                  enforce_leq l r local
+                  Sorts.enforce_leq_sort l r local
               end
           | ULub (l, r) ->
-              equalize_variables true (Universe.make l) l (Universe.make r) r local
+              equalize_variables true (Sorts.sort_of_univ (Universe.make l)) l (Sorts.sort_of_univ (Universe.make r)) r local
           | UWeak (l, r) ->
             if not (drop_weak_constraints ()) then weak := UPairSet.add (l,r) !weak; local
           | UEq (l, r) -> equalize_universes l r local
@@ -300,13 +307,13 @@ let process_universe_constraints uctx cstrs =
 let add_constraints uctx cstrs =
   let univs, old_cstrs = uctx.local in
   let cstrs' = Constraints.fold (fun (l,d,r) acc ->
-    let l = Universe.make l and r = Universe.make r in
+    let l = Universe.make l and r = Sorts.sort_of_univ @@ Universe.make r in
     let cstr' = let open UnivProblem in
       match d with
       | Lt ->
-        ULe (Universe.super l, r)
-      | Le -> ULe (l, r)
-      | Eq -> UEq (l, r)
+        ULe (Sorts.sort_of_univ @@ Universe.super l, r)
+      | Le -> ULe (Sorts.sort_of_univ l, r)
+      | Eq -> UEq (Sorts.sort_of_univ l, r)
     in UnivProblem.Set.add cstr' acc)
     cstrs UnivProblem.Set.empty
   in

engine/univProblem.ml

@@ -11,23 +11,23 @@
 open Univ
 
 type t =
-  | ULe of Universe.t * Universe.t
-  | UEq of Universe.t * Universe.t
+  | ULe of Sorts.t * Sorts.t
+  | UEq of Sorts.t * Sorts.t
   | ULub of Level.t * Level.t
   | UWeak of Level.t * Level.t
 
 
 let is_trivial = function
-  | ULe (u, v) | UEq (u, v) -> Universe.equal u v
+  | ULe (u, v) | UEq (u, v) -> Sorts.equal u v
   | ULub (u, v) | UWeak (u, v) -> Level.equal u v
 
 let force = function
   | ULe _ | UEq _ | UWeak _ as cst -> cst
-  | ULub (u,v) -> UEq (Universe.make u, Universe.make v)
+  | ULub (u,v) -> UEq (Sorts.sort_of_univ @@ Universe.make u, Sorts.sort_of_univ @@ Universe.make v)
 
 let check g = function
-  | ULe (u,v) -> UGraph.check_leq g u v
-  | UEq (u,v) -> UGraph.check_eq g u v
+  | ULe (u,v) -> Sorts.check_leq_sort g u v
+  | UEq (u,v) -> Sorts.check_eq_sort g u v
   | ULub (u,v) -> UGraph.check_eq_level g u v
   | UWeak _ -> true
 
@@ -39,13 +39,13 @@ module Set = struct
     let compare x y =
       match x, y with
       | ULe (u, v), ULe (u', v') ->
-        let i = Universe.compare u u' in
-        if Int.equal i 0 then Universe.compare v v'
+        let i = Sorts.compare u u' in
+        if Int.equal i 0 then Sorts.compare v v'
         else i
       | UEq (u, v), UEq (u', v') ->
-        let i = Universe.compare u u' in
-        if Int.equal i 0 then Universe.compare v v'
-        else if Universe.equal u v' && Universe.equal v u' then 0
+        let i = Sorts.compare u u' in
+        if Int.equal i 0 then Sorts.compare v v'
+        else if Sorts.equal u v' && Sorts.equal v u' then 0
         else i
       | ULub (u, v), ULub (u', v') | UWeak (u, v), UWeak (u', v') ->
         let i = Level.compare u u' in
@@ -67,8 +67,8 @@ module Set = struct
     else add cst s
 
   let pr_one = let open Pp in function
-    | ULe (u, v) -> Universe.pr u ++ str " <= " ++ Universe.pr v
-    | UEq (u, v) -> Universe.pr u ++ str " = " ++ Universe.pr v
+    | ULe (u, v) -> Sorts.debug_print u ++ str " <= " ++ Sorts.debug_print v
+    | UEq (u, v) -> Sorts.debug_print u ++ str " = " ++ Sorts.debug_print v
     | ULub (u, v) -> Level.pr u ++ str " /\\ " ++ Level.pr v
     | UWeak (u, v) -> Level.pr u ++ str " ~ " ++ Level.pr v
 
@@ -88,7 +88,8 @@ end
 type 'a constraint_function = 'a -> 'a -> Set.t -> Set.t
 
 let enforce_eq_instances_univs strict x y c =
-  let mk u v = if strict then ULub (u, v) else UEq (Universe.make u, Universe.make v) in
+  let mkU u = Sorts.sort_of_univ @@ Universe.make u in
+  let mk u v = if strict then ULub (u, v) else UEq (mkU u, mkU v) in
   let ax = Instance.to_array x and ay = Instance.to_array y in
     if Array.length ax != Array.length ay then
       CErrors.anomaly Pp.(str "Invalid argument: enforce_eq_instances_univs called with" ++

engine/univProblem.mli

@@ -20,8 +20,8 @@ open Univ
 *)
 
 type t =
-  | ULe of Universe.t * Universe.t
-  | UEq of Universe.t * Universe.t
+  | ULe of Sorts.t * Sorts.t
+  | UEq of Sorts.t * Sorts.t
   | ULub of Level.t * Level.t
   | UWeak of Level.t * Level.t