aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-12-13 13:57:10 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-12-30 19:19:03 +0100
commit441bea723c511ed9e18ef005678bd01242b45c49 (patch)
treebbe502a899b3b1fa16cb91a7372a2bf2c601ec83 /library
parent6e49d0bee79cd68495955deb115b495fb01f01fd (diff)
Returning instance instead of substitution in universe context abstraction.
This datatype enforces stronger invariants, e.g. that we only have in the substitution codomain a connex interval of variables from 0 to n - 1.
Diffstat (limited to 'library')
-rw-r--r--library/lib.ml15
-rw-r--r--library/lib.mli4
2 files changed, 7 insertions, 12 deletions
diff --git a/library/lib.ml b/library/lib.ml
index 16dd7fdd0..971089c17 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -419,7 +419,7 @@ type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
type variable_context = variable_info list
type abstr_info = {
abstr_ctx : variable_context;
- abstr_subst : Univ.universe_level_subst;
+ abstr_subst : Univ.Instance.t;
abstr_uctx : Univ.AUContext.t;
}
type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
@@ -511,7 +511,7 @@ let section_segment_of_mutual_inductive kn =
let empty_segment = {
abstr_ctx = [];
- abstr_subst = Univ.LMap.empty;
+ abstr_subst = Univ.Instance.empty;
abstr_uctx = Univ.AUContext.empty;
}
@@ -672,13 +672,8 @@ let discharge_inductive (kn,i) =
let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx =
let open Univ in
- let len = LMap.cardinal subst in
- let rec gen_subst i acc =
- if i < 0 then acc
- else
- let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in
- gen_subst (pred i) acc
- in
- let subst = gen_subst (AUContext.size auctx - 1) subst in
+ let ainst = make_abstract_instance auctx in
+ let subst = Instance.append subst ainst in
+ let subst = make_instance_subst subst in
let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in
subst, AUContext.union abs_ctx auctx
diff --git a/library/lib.mli b/library/lib.mli
index 2f4d0d56f..cf75d5f8c 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -156,8 +156,8 @@ type variable_context = variable_info list
type abstr_info = private {
abstr_ctx : variable_context;
(** Section variables of this prefix *)
- abstr_subst : Univ.universe_level_subst;
- (** Abstract substitution: named universes are mapped to De Bruijn indices *)
+ abstr_subst : Univ.Instance.t;
+ (** Actual names of the abstracted variables *)
abstr_uctx : Univ.AUContext.t;
(** Universe quantification, same length as the substitution *)
}