aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/environ.ml3
-rw-r--r--checker/reduction.ml6
-rw-r--r--checker/univ.ml67
-rw-r--r--checker/univ.mli3
-rw-r--r--engine/universes.ml4
-rw-r--r--kernel/environ.ml3
-rw-r--r--kernel/inductive.ml4
-rw-r--r--kernel/reduction.ml13
-rw-r--r--kernel/univ.ml76
-rw-r--r--kernel/univ.mli4
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/reductionops.ml6
12 files changed, 90 insertions, 103 deletions
diff --git a/checker/environ.ml b/checker/environ.ml
index 11b8ea67c..d3f393c65 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -122,8 +122,7 @@ type const_evaluation_result = NoBody | Opaque | IsProj
let constraints_of cb u =
match cb.const_universes with
| Monomorphic_const _ -> Univ.Constraint.empty
- | Polymorphic_const ctx ->
- Univ.UContext.constraints (Univ.subst_instance_context u ctx)
+ | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
let map_regular_arity f = function
| RegularArity a as ar ->
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 0b605820d..6d8783d7e 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -166,16 +166,14 @@ let convert_inductive_instances cv_pb cumi u u' univs =
else
let comp_cst =
let comp_subst = (Univ.Instance.append u u') in
- Univ.UContext.constraints
- (Univ.subst_instance_context comp_subst ind_subtypctx)
+ Univ.AUContext.instantiate comp_subst ind_subtypctx
in
let comp_cst =
match cv_pb with
CONV ->
let comp_cst' =
let comp_subst = (Univ.Instance.append u' u) in
- Univ.UContext.constraints
- (Univ.subst_instance_context comp_subst ind_subtypctx)
+ Univ.AUContext.instantiate comp_subst ind_subtypctx
in
Univ.Constraint.union comp_cst comp_cst'
| CUMUL -> comp_cst
diff --git a/checker/univ.ml b/checker/univ.ml
index 4eebcb25b..600af230c 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1160,6 +1160,33 @@ struct
end
+(** Substitute instance inst for ctx in csts *)
+
+let subst_instance_level s l =
+ match l.Level.data with
+ | Level.Var n -> s.(n)
+ | _ -> l
+
+let subst_instance_instance s i =
+ Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+ let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+ let u' = Universe.smartmap f u in
+ if u == u' then u
+ else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+ let u' = subst_instance_level s u in
+ let v' = subst_instance_level s v in
+ if u' == u && v' == v then c
+ else (u',d,v')
+
+let subst_instance_constraints s csts =
+ Constraint.fold
+ (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+ csts Constraint.empty
+
type universe_instance = Instance.t
type 'a puniverses = 'a * Instance.t
@@ -1185,7 +1212,15 @@ end
type universe_context = UContext.t
-module AUContext = UContext
+module AUContext =
+struct
+ include UContext
+
+ let instantiate inst (u, cst) =
+ assert (Array.length u = Array.length inst);
+ subst_instance_constraints inst cst
+
+end
type abstract_universe_context = AUContext.t
@@ -1264,36 +1299,6 @@ let subst_univs_level_universe subst u =
if u == u' then u
else Universe.sort u'
-(** Substitute instance inst for ctx in csts *)
-
-let subst_instance_level s l =
- match l.Level.data with
- | Level.Var n -> s.(n)
- | _ -> l
-
-let subst_instance_instance s i =
- Array.smartmap (fun l -> subst_instance_level s l) i
-
-let subst_instance_universe s u =
- let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
- let u' = Universe.smartmap f u in
- if u == u' then u
- else Universe.sort u'
-
-let subst_instance_constraint s (u,d,v as c) =
- let u' = subst_instance_level s u in
- let v' = subst_instance_level s v in
- if u' == u && v' == v then c
- else (u',d,v')
-
-let subst_instance_constraints s csts =
- Constraint.fold
- (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
- csts Constraint.empty
-
-let subst_instance_context inst (inner_inst, inner_constr) =
- (inner_inst, subst_instance_constraints inst inner_constr)
-
let make_abstract_instance (ctx, _) =
Array.mapi (fun i l -> Level.var i) ctx
diff --git a/checker/univ.mli b/checker/univ.mli
index faa682cbf..75c76cd12 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -211,6 +211,8 @@ sig
val instance : t -> Instance.t
val size : t -> int
+ val instantiate : Instance.t -> t -> Constraint.t
+
end
type abstract_universe_context = AUContext.t
@@ -277,7 +279,6 @@ val subst_univs_universe : universe_subst_fn -> universe -> universe
(** Substitution of instances *)
val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
val subst_instance_universe : universe_instance -> universe -> universe
-val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context
(* val make_instance_subst : universe_instance -> universe_level_subst *)
(* val make_inverse_instance_subst : universe_instance -> universe_level_subst *)
diff --git a/engine/universes.ml b/engine/universes.ml
index 5df02c8a9..fc441fd0b 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -287,7 +287,7 @@ let fresh_universe_instance ctx =
let fresh_instance_from_context ctx =
let inst = fresh_universe_instance ctx in
- let constraints = UContext.constraints (subst_instance_context inst ctx) in
+ let constraints = AUContext.instantiate inst ctx in
inst, constraints
let fresh_instance ctx =
@@ -316,7 +316,7 @@ let fresh_instance_from ctx inst =
| Some inst -> existing_instance ctx inst
| None -> fresh_instance ctx
in
- let constraints = UContext.constraints (subst_instance_context inst ctx) in
+ let constraints = AUContext.instantiate inst ctx in
inst, (ctx', constraints)
let unsafe_instance_from ctx =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index dd204c7d5..ca2c8e135 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -230,8 +230,7 @@ let add_constant kn cb env =
let constraints_of cb u =
match cb.const_universes with
| Monomorphic_const _ -> Univ.Constraint.empty
- | Polymorphic_const ctx ->
- Univ.UContext.constraints (Univ.subst_instance_context u ctx)
+ | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
let map_regular_arity f = function
| RegularArity a as ar ->
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e3fb472be..1eaba49aa 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -54,9 +54,7 @@ let inductive_paramdecls (mib,u) =
Vars.subst_instance_context u mib.mind_params_ctxt
let instantiate_inductive_constraints mib u =
- let process auctx =
- Univ.UContext.constraints (Univ.subst_instance_context u auctx)
- in
+ let process auctx = Univ.AUContext.instantiate u auctx in
match mib.mind_universes with
| Monomorphic_ind _ -> Univ.Constraint.empty
| Polymorphic_ind auctx -> process auctx
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 423e0d934..2bf9f43a5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -689,16 +689,14 @@ let check_inductive_instances cv_pb cumi u u' univs =
else
let comp_cst =
let comp_subst = (Univ.Instance.append u u') in
- Univ.UContext.constraints
- (Univ.subst_instance_context comp_subst ind_subtypctx)
+ Univ.AUContext.instantiate comp_subst ind_subtypctx
in
let comp_cst =
match cv_pb with
CONV ->
let comp_cst' =
let comp_subst = (Univ.Instance.append u' u) in
- Univ.UContext.constraints
- (Univ.subst_instance_context comp_subst ind_subtypctx)
+ Univ.AUContext.instantiate comp_subst ind_subtypctx
in
Univ.Constraint.union comp_cst comp_cst'
| CUMUL -> comp_cst
@@ -775,16 +773,15 @@ let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
else
let comp_cst =
let comp_subst = (Univ.Instance.append u u') in
- Univ.UContext.constraints
- (Univ.subst_instance_context comp_subst ind_subtypctx)
+ Univ.AUContext.instantiate comp_subst ind_subtypctx
in
let comp_cst =
match cv_pb with
CONV ->
let comp_cst' =
let comp_subst = (Univ.Instance.append u' u) in
- Univ.UContext.constraints
- (Univ.subst_instance_context comp_subst ind_subtypctx) in
+ Univ.AUContext.instantiate comp_subst ind_subtypctx
+ in
Univ.Constraint.union comp_cst comp_cst'
| CUMUL -> comp_cst
in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1c887e2a9..cb19761b3 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -988,6 +988,31 @@ let enforce_eq_instances x y =
(Pp.str " instances of different lengths."));
CArray.fold_right2 enforce_eq_level ax ay
+let subst_instance_level s l =
+ match l.Level.data with
+ | Level.Var n -> s.(n)
+ | _ -> l
+
+let subst_instance_instance s i =
+ Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+ let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+ let u' = Universe.smartmap f u in
+ if u == u' then u
+ else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+ let u' = subst_instance_level s u in
+ let v' = subst_instance_level s v in
+ if u' == u && v' == v then c
+ else (u',d,v')
+
+let subst_instance_constraints s csts =
+ Constraint.fold
+ (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+ csts Constraint.empty
+
type universe_instance = Instance.t
type 'a puniverses = 'a * Instance.t
@@ -1031,7 +1056,15 @@ end
type universe_context = UContext.t
let hcons_universe_context = UContext.hcons
-module AUContext = UContext
+module AUContext =
+struct
+ include UContext
+
+ let instantiate inst (u, cst) =
+ assert (Array.length u = Array.length inst);
+ subst_instance_constraints inst cst
+
+end
type abstract_universe_context = AUContext.t
let hcons_abstract_universe_context = AUContext.hcons
@@ -1256,31 +1289,6 @@ let subst_univs_constraints subst csts =
(fun c cstrs -> subst_univs_constraint subst c cstrs)
csts Constraint.empty
-let subst_instance_level s l =
- match l.Level.data with
- | Level.Var n -> s.(n)
- | _ -> l
-
-let subst_instance_instance s i =
- Array.smartmap (fun l -> subst_instance_level s l) i
-
-let subst_instance_universe s u =
- let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
- let u' = Universe.smartmap f u in
- if u == u' then u
- else Universe.sort u'
-
-let subst_instance_constraint s (u,d,v as c) =
- let u' = subst_instance_level s u in
- let v' = subst_instance_level s v in
- if u' == u && v' == v then c
- else (u',d,v')
-
-let subst_instance_constraints s csts =
- Constraint.fold
- (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
- csts Constraint.empty
-
(** Substitute instance inst for ctx in csts *)
let instantiate_univ_context (ctx, csts) =
(ctx, subst_instance_constraints ctx csts)
@@ -1378,19 +1386,3 @@ let explain_universe_inconsistency prl (o,u,v,p) =
let compare_levels = Level.compare
let eq_levels = Level.equal
let equal_universes = Universe.equal
-
-
-let subst_instance_constraints =
- if Flags.profile then
- let key = Profile.declare_profile "subst_instance_constraints" in
- Profile.profile2 key subst_instance_constraints
- else subst_instance_constraints
-
-let subst_instance_context =
- let subst_instance_context_body inst (inner_inst, inner_constr) =
- (inner_inst, subst_instance_constraints inst inner_constr)
- in
- if Flags.profile then
- let key = Profile.declare_profile "subst_instance_constraints" in
- Profile.profile2 key subst_instance_context_body
- else subst_instance_context_body
diff --git a/kernel/univ.mli b/kernel/univ.mli
index dc6fb85a0..3d0d2234d 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -329,6 +329,9 @@ sig
(** Keeps the order of the instances *)
val union : t -> t -> t
+ val instantiate : Instance.t -> t -> Constraint.t
+ (** Generate the set of instantiated constraints **)
+
end
type abstract_universe_context = AUContext.t
@@ -443,7 +446,6 @@ val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
(** Substitution of instances *)
val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
val subst_instance_universe : universe_instance -> universe -> universe
-val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context
val make_instance_subst : universe_instance -> universe_level_subst
val make_inverse_instance_subst : universe_instance -> universe_level_subst
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2acf6bfe6..87f29ba49 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -363,9 +363,7 @@ let check_leq_inductives evd cumi u u' =
else
begin
let comp_subst = (Univ.Instance.append u u') in
- let comp_cst =
- Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst)
- in
+ let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in
Evd.add_constraints evd comp_cst
end
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3acefa134..21ed8e0a2 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1372,15 +1372,13 @@ let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
else
let comp_cst =
let comp_subst = (Univ.Instance.append u u') in
- Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbctx)
+ Univ.AUContext.instantiate comp_subst ind_sbctx
in
let comp_cst =
match cv_pb with
Reduction.CONV ->
let comp_subst = (Univ.Instance.append u' u) in
- let comp_cst' =
- Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx)
- in
+ let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in
Univ.Constraint.union comp_cst comp_cst'
| Reduction.CUMUL -> comp_cst
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 19:50:56 +0000