aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml13
-rw-r--r--engine/eConstr.mli4
-rw-r--r--engine/engine.mllib2
-rw-r--r--engine/evarutil.ml2
-rw-r--r--engine/evd.ml2
-rw-r--r--engine/termops.ml19
-rw-r--r--engine/termops.mli2
-rw-r--r--engine/uState.ml15
-rw-r--r--engine/uState.mli11
-rw-r--r--engine/univGen.ml183
-rw-r--r--engine/univGen.mli14
-rw-r--r--engine/univNames.ml2
-rw-r--r--engine/univops.ml28
-rw-r--r--engine/univops.mli6
14 files changed, 118 insertions, 185 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 8ab3ce821e..3385b78958 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -74,6 +74,12 @@ let mkCoFix f = of_kind (CoFix f)
let mkProj (p, c) = of_kind (Proj (p, c))
let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2))
+let mkRef (gr,u) = let open GlobRef in match gr with
+ | ConstRef c -> mkConstU (c,u)
+ | IndRef ind -> mkIndU (ind,u)
+ | ConstructRef c -> mkConstructU (c,u)
+ | VarRef x -> mkVar x
+
let applist (f, arg) = mkApp (f, Array.of_list arg)
let isRel sigma c = match kind sigma c with Rel _ -> true | _ -> false
@@ -166,6 +172,13 @@ let destProj sigma c = match kind sigma c with
| Proj (p, c) -> (p, c)
| _ -> raise DestKO
+let destRef sigma c = let open GlobRef in match kind sigma c with
+ | Var x -> VarRef x, EInstance.empty
+ | Const (c,u) -> ConstRef c, u
+ | Ind (ind,u) -> IndRef ind, u
+ | Construct (c,u) -> ConstructRef c, u
+ | _ -> raise DestKO
+
let decompose_app sigma c =
match kind sigma c with
| App (f,cl) -> (f, Array.to_list cl)
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index f897448557..1edc0ee12b 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -122,6 +122,8 @@ val mkFix : (t, t) pfixpoint -> t
val mkCoFix : (t, t) pcofixpoint -> t
val mkArrow : t -> t -> t
+val mkRef : GlobRef.t * EInstance.t -> t
+
val applist : t * t list -> t
val mkProd_or_LetIn : rel_declaration -> t -> t
@@ -180,6 +182,8 @@ val destProj : Evd.evar_map -> t -> Projection.t * t
val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
+val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t
+
val decompose_app : Evd.evar_map -> t -> t * t list
(** Pops lambda abstractions until there are no more, skipping casts. *)
diff --git a/engine/engine.mllib b/engine/engine.mllib
index 37e83b6238..bb43808542 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -4,8 +4,8 @@ UnivSubst
UnivProblem
UnivMinim
Universes
-Univops
UState
+Univops
Nameops
Evar_kinds
Evd
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 13356627f0..f9d9ce3569 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -549,7 +549,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
if Id.Set.mem id' ids then
raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c)))
in
- Id.Set.iter check (Environ.vars_of_global env c)
+ Id.Set.iter check (Environ.vars_of_global env (fst @@ destRef c))
in
c
diff --git a/engine/evd.ml b/engine/evd.ml
index d7b03a84f1..eafdc4cb46 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -818,7 +818,7 @@ let fresh_constructor_instance ?loc env evd c =
with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
- with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
+ with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr)
let is_sort_variable evd s = UState.is_sort_variable evd.universes s
diff --git a/engine/termops.ml b/engine/termops.ml
index 1244074d50..ee0c3d210e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -912,9 +912,9 @@ let occur_in_global env id constr =
let occur_var env sigma id c =
let rec occur_rec c =
- match EConstr.kind sigma c with
- | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id (EConstr.to_constr sigma c)
- | _ -> EConstr.iter sigma occur_rec c
+ match EConstr.destRef sigma c with
+ | gr, _ -> occur_in_global env id gr
+ | exception DestKO -> EConstr.iter sigma occur_rec c
in
try occur_rec c; false with Occur -> true
@@ -961,9 +961,7 @@ let collect_vars sigma c =
| _ -> EConstr.fold sigma aux vars c in
aux Id.Set.empty c
-let vars_of_global_reference env gr =
- let c, _ = Global.constr_of_global_in_context env gr in
- vars_of_global env c
+let vars_of_global_reference = vars_of_global
(* Tests whether [m] is a subterm of [t]:
[m] is appropriately lifted through abstractions of [t] *)
@@ -1458,12 +1456,9 @@ let clear_named_body id env =
let global_vars_set env sigma constr =
let rec filtrec acc c =
- let acc = match EConstr.kind sigma c with
- | Var _ | Const _ | Ind _ | Construct _ ->
- Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) acc
- | _ -> acc
- in
- EConstr.fold sigma filtrec acc c
+ match EConstr.destRef sigma c with
+ | gr, _ -> Id.Set.union (vars_of_global env gr) acc
+ | exception DestKO -> EConstr.fold sigma filtrec acc c
in
filtrec Id.Set.empty constr
diff --git a/engine/termops.mli b/engine/termops.mli
index 64e3977d68..f7b9469ae8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -118,7 +118,9 @@ val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool
val count_occurrences : Evd.evar_map -> constr -> constr -> int
val collect_metas : Evd.evar_map -> constr -> int list
val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
+
val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
+[@@ocaml.deprecated "Use [Environ.vars_of_global]"]
(* Substitution of metavariables *)
type meta_value_map = (metavariable * Constr.constr) list
diff --git a/engine/uState.ml b/engine/uState.ml
index 29cb3c9bcc..aa7ec63a6f 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -406,12 +406,25 @@ let check_univ_decl ~poly uctx decl =
(Univ.ContextSet.constraints uctx.uctx_local);
ctx
+let restrict_universe_context (univs, csts) keep =
+ let open Univ in
+ let removed = LSet.diff univs keep in
+ if LSet.is_empty removed then univs, csts
+ else
+ let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
+ let g = UGraph.empty_universes in
+ let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
+ let g = UGraph.merge_constraints csts g in
+ let allkept = LSet.diff allunivs removed in
+ let csts = UGraph.constraints_for ~kept:allkept g in
+ (LSet.inter univs keep, csts)
+
let restrict ctx vars =
let vars = Univ.LSet.union vars ctx.uctx_seff_univs in
let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars)
(fst ctx.uctx_names) vars
in
- let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
+ let uctx' = restrict_universe_context ctx.uctx_local vars in
{ ctx with uctx_local = uctx' }
let demote_seff_univs entry uctx =
diff --git a/engine/uState.mli b/engine/uState.mli
index f833508ebf..8053a7bf83 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -13,6 +13,7 @@
primitives when needed. *)
open Names
+open Univ
exception UniversesDiffer
@@ -91,6 +92,16 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
(** {5 Unification} *)
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+ the universes in [keep]. The constraints [csts] are adjusted so
+ that transitive constraints between remaining universes (those in
+ [keep] and those not in [univs]) are preserved. *)
+val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+
+(** [restrict uctx ctx] restricts the local universes of [uctx] to
+ [ctx] extended by local named universes and side effect universes
+ (from [demote_seff_univs]). Transitive constraints between retained
+ universes are preserved. *)
val restrict : t -> Univ.LSet.t -> t
val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t
diff --git a/engine/univGen.ml b/engine/univGen.ml
index b07d4848ff..23ab30eb75 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -11,7 +11,6 @@
open Sorts
open Names
open Constr
-open Environ
open Univ
(* Generator of levels *)
@@ -32,103 +31,51 @@ let new_univ dp = Univ.Universe.make (new_univ_level dp)
let new_Type dp = mkType (new_univ dp)
let new_Type_sort dp = Type (new_univ dp)
-let fresh_universe_instance ctx =
- let init _ = new_univ_level () in
- Instance.of_array (Array.init (AUContext.size ctx) init)
+let fresh_instance auctx =
+ let inst = Array.init (AUContext.size auctx) (fun _ -> new_univ_level()) in
+ let ctx = Array.fold_right LSet.add inst LSet.empty in
+ let inst = Instance.of_array inst in
+ inst, (ctx, AUContext.instantiate inst auctx)
-let fresh_instance_from_context ctx =
- let inst = fresh_universe_instance ctx in
- let constraints = AUContext.instantiate inst ctx in
- inst, constraints
-
-let fresh_instance ctx =
- let ctx' = ref LSet.empty in
- let init _ =
- let u = new_univ_level () in
- ctx' := LSet.add u !ctx'; u
- in
- let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
- in !ctx', inst
-
-let existing_instance ctx inst =
+let existing_instance ?loc auctx inst =
let () =
let len1 = Array.length (Instance.to_array inst)
- and len2 = AUContext.size ctx in
+ and len2 = AUContext.size auctx in
if not (len1 == len2) then
- CErrors.user_err ~hdr:"Universes"
- Pp.(str "Polymorphic constant expected " ++ int len2 ++
- str" levels but was given " ++ int len1)
+ CErrors.user_err ?loc ~hdr:"Universes"
+ Pp.(str "Universe instance should have length " ++ int len2 ++ str ".")
else ()
- in LSet.empty, inst
-
-let fresh_instance_from ctx inst =
- let ctx', inst =
- match inst with
- | Some inst -> existing_instance ctx inst
- | None -> fresh_instance ctx
in
- let constraints = AUContext.instantiate inst ctx in
- inst, (ctx', constraints)
+ inst, (LSet.empty, AUContext.instantiate inst auctx)
-(** Fresh universe polymorphic construction *)
+let fresh_instance_from ?loc ctx = function
+ | Some inst -> existing_instance ?loc ctx inst
+ | None -> fresh_instance ctx
-let fresh_constant_instance env c inst =
- let cb = lookup_constant c env in
- match cb.Declarations.const_universes with
- | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
- | Declarations.Polymorphic_const auctx ->
- let inst, ctx =
- fresh_instance_from auctx inst
- in
- ((c, inst), ctx)
-
-let fresh_inductive_instance env ind inst =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- match mib.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- ((ind,Instance.empty), ContextSet.empty)
- | Declarations.Polymorphic_ind uactx ->
- let inst, ctx = (fresh_instance_from uactx) inst in
- ((ind,inst), ctx)
- | Declarations.Cumulative_ind acumi ->
- let inst, ctx =
- fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
- in ((ind,inst), ctx)
-
-let fresh_constructor_instance env (ind,i) inst =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- match mib.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
- | Declarations.Polymorphic_ind auctx ->
- let inst, ctx = fresh_instance_from auctx inst in
- (((ind,i),inst), ctx)
- | Declarations.Cumulative_ind acumi ->
- let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
- (((ind,i),inst), ctx)
+(** Fresh universe polymorphic construction *)
open Globnames
-let fresh_global_instance ?names env gr =
- match gr with
- | VarRef id -> mkVar id, ContextSet.empty
- | ConstRef sp ->
- let c, ctx = fresh_constant_instance env sp names in
- mkConstU c, ctx
- | ConstructRef sp ->
- let c, ctx = fresh_constructor_instance env sp names in
- mkConstructU c, ctx
- | IndRef sp ->
- let c, ctx = fresh_inductive_instance env sp names in
- mkIndU c, ctx
+let fresh_global_instance ?loc ?names env gr =
+ let auctx = Environ.universes_of_global env gr in
+ let u, ctx = fresh_instance_from ?loc auctx names in
+ u, ctx
+
+let fresh_constant_instance env c =
+ let u, ctx = fresh_global_instance env (ConstRef c) in
+ (c, u), ctx
-let fresh_constant_instance env sp =
- fresh_constant_instance env sp None
+let fresh_inductive_instance env ind =
+ let u, ctx = fresh_global_instance env (IndRef ind) in
+ (ind, u), ctx
-let fresh_inductive_instance env sp =
- fresh_inductive_instance env sp None
+let fresh_constructor_instance env c =
+ let u, ctx = fresh_global_instance env (ConstructRef c) in
+ (c, u), ctx
-let fresh_constructor_instance env sp =
- fresh_constructor_instance env sp None
+let fresh_global_instance ?loc ?names env gr =
+ let u, ctx = fresh_global_instance ?loc ?names env gr in
+ mkRef (gr, u), ctx
let constr_of_global gr =
let c, ctx = fresh_global_instance (Global.env ()) gr in
@@ -142,12 +89,7 @@ let constr_of_global gr =
str " would forget universes.")
else c
-let constr_of_global_univ (gr,u) =
- match gr with
- | VarRef id -> mkVar id
- | ConstRef sp -> mkConstU (sp,u)
- | ConstructRef sp -> mkConstructU (sp,u)
- | IndRef sp -> mkIndU (sp,u)
+let constr_of_global_univ = mkRef
let fresh_global_or_constr_instance env = function
| IsConstr c -> c, ContextSet.empty
@@ -166,52 +108,26 @@ open Declarations
let type_of_reference env r =
match r with
| VarRef id -> Environ.named_type id env, ContextSet.empty
+
| ConstRef c ->
let cb = Environ.lookup_constant c env in
let ty = cb.const_type in
- begin
- match cb.const_universes with
- | Monomorphic_const _ -> ty, ContextSet.empty
- | Polymorphic_const auctx ->
- let inst, ctx = fresh_instance_from auctx None in
- Vars.subst_instance_constr inst ty, ctx
- end
+ let auctx = Declareops.constant_polymorphic_context cb in
+ let inst, ctx = fresh_instance auctx in
+ Vars.subst_instance_constr inst ty, ctx
+
| IndRef ind ->
- let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
- begin
- match mib.mind_universes with
- | Monomorphic_ind _ ->
- let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
- ty, ContextSet.empty
- | Polymorphic_ind auctx ->
- let inst, ctx = fresh_instance_from auctx None in
- let ty = Inductive.type_of_inductive env (specif, inst) in
- ty, ctx
- | Cumulative_ind cumi ->
- let inst, ctx =
- fresh_instance_from (ACumulativityInfo.univ_context cumi) None
- in
- let ty = Inductive.type_of_inductive env (specif, inst) in
- ty, ctx
- end
-
- | ConstructRef cstr ->
- let (mib,oib as specif) =
- Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
- in
- begin
- match mib.mind_universes with
- | Monomorphic_ind _ ->
- Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
- | Polymorphic_ind auctx ->
- let inst, ctx = fresh_instance_from auctx None in
- Inductive.type_of_constructor (cstr,inst) specif, ctx
- | Cumulative_ind cumi ->
- let inst, ctx =
- fresh_instance_from (ACumulativityInfo.univ_context cumi) None
- in
- Inductive.type_of_constructor (cstr,inst) specif, ctx
- end
+ let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in
+ let auctx = Declareops.inductive_polymorphic_context mib in
+ let inst, ctx = fresh_instance auctx in
+ let ty = Inductive.type_of_inductive env (specif, inst) in
+ ty, ctx
+
+ | ConstructRef (ind,_ as cstr) ->
+ let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+ let auctx = Declareops.inductive_polymorphic_context mib in
+ let inst, ctx = fresh_instance auctx in
+ Inductive.type_of_constructor (cstr,inst) specif, ctx
let type_of_global t = type_of_reference (Global.env ()) t
@@ -225,8 +141,7 @@ let fresh_sort_in_family = function
let new_sort_in_family sf =
fst (fresh_sort_in_family sf)
-let extend_context (a, ctx) (ctx') =
- (a, ContextSet.union ctx ctx')
+let extend_context = Univ.extend_in_context_set
let new_global_univ () =
let u = fresh_level () in
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 439424934c..c2e9d0c696 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -23,20 +23,24 @@ val set_remote_new_univ_id : universe_id RemoteCounter.installer
val new_univ_id : unit -> universe_id
val new_univ_level : unit -> Level.t
+
val new_univ : unit -> Universe.t
+[@@ocaml.deprecated "Use [new_univ_level]"]
val new_Type : unit -> types
+[@@ocaml.deprecated "Use [new_univ_level]"]
val new_Type_sort : unit -> Sorts.t
+[@@ocaml.deprecated "Use [new_univ_level]"]
val new_global_univ : unit -> Universe.t in_universe_context_set
val new_sort_in_family : Sorts.family -> Sorts.t
+[@@ocaml.deprecated "Use [fresh_sort_in_family]"]
(** Build a fresh instance for a given context, its associated substitution and
the instantiated constraints. *)
-val fresh_instance_from_context : AUContext.t ->
- Instance.t constrained
+val fresh_instance : AUContext.t -> Instance.t in_universe_context_set
-val fresh_instance_from : AUContext.t -> Instance.t option ->
+val fresh_instance_from : ?loc:Loc.t -> AUContext.t -> Instance.t option ->
Instance.t in_universe_context_set
val fresh_sort_in_family : Sorts.family ->
@@ -48,7 +52,7 @@ val fresh_inductive_instance : env -> inductive ->
val fresh_constructor_instance : env -> constructor ->
pconstructor in_universe_context_set
-val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
+val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t ->
constr in_universe_context_set
val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
@@ -63,9 +67,11 @@ val fresh_universe_context_set_instance : ContextSet.t ->
val global_of_constr : constr -> GlobRef.t puniverses
val constr_of_global_univ : GlobRef.t puniverses -> constr
+[@@ocaml.deprecated "Use [Constr.mkRef]"]
val extend_context : 'a in_universe_context_set -> ContextSet.t ->
'a in_universe_context_set
+[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"]
(** Create a fresh global in the global environment, without side effects.
BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
diff --git a/engine/univNames.ml b/engine/univNames.ml
index e89dcedb9c..a71f9c5736 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -86,7 +86,7 @@ let register_universe_binders ref ubinders =
part of the code that depends on the internal representation of names in
abstract contexts, but removing it requires quite a rework of the
callers. *)
- let univs = AUContext.instance (Global.universes_of_global ref) in
+ let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in
let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
let map lvl =
try LMap.find lvl revmap
diff --git a/engine/univops.ml b/engine/univops.ml
index 7f9672f828..53c42023ad 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -8,30 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Univ
-open Constr
+let universes_of_constr = Vars.universes_of_constr
-let universes_of_constr c =
- let rec aux s c =
- match kind c with
- | Const (c, u) ->
- LSet.fold LSet.add (Instance.levels u) s
- | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
- LSet.fold LSet.add (Instance.levels u) s
- | Sort u when not (Sorts.is_small u) ->
- let u = Sorts.univ_of_sort u in
- LSet.fold LSet.add (Universe.levels u) s
- | _ -> Constr.fold aux s c
- in aux LSet.empty c
-
-let restrict_universe_context (univs, csts) keep =
- let removed = LSet.diff univs keep in
- if LSet.is_empty removed then univs, csts
- else
- let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
- let g = UGraph.empty_universes in
- let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
- let g = UGraph.merge_constraints csts g in
- let allkept = LSet.diff allunivs removed in
- let csts = UGraph.constraints_for ~kept:allkept g in
- (LSet.inter univs keep, csts)
+let restrict_universe_context = UState.restrict_universe_context
diff --git a/engine/univops.mli b/engine/univops.mli
index 57a53597b9..597d2d6785 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -13,9 +13,7 @@ open Univ
(** Return the set of all universes appearing in [constr]. *)
val universes_of_constr : constr -> LSet.t
+[@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
-(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
- the universes in [keep]. The constraints [csts] are adjusted so
- that transitive constraints between remaining universes (those in
- [keep] and those not in [univs]) are preserved. *)
val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
+[@@ocaml.deprecated "Use [UState.restrict_universe_context]"]
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:22:01 +0000