aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-10 18:05:23 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-11 14:50:47 +0200
commitb8a7222e670f69e024d50394afd88204e15d1b29 (patch)
tree90c3c75ca9c2647ad41c6a30954cdf8ce3f6b5d8 /kernel
parent1309723672def9bf322a23e9c789e4a8bc2a4ac3 (diff)
Less footguns in universe handling: remove subst_instance_context.
This function was lurking around, waiting to bite anybody willing to use it. We use instead a better API, correct and much less error-prone.
Diffstat (limited to 'kernel')
-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
5 files changed, 44 insertions, 56 deletions
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