aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-09-14 17:18:21 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-09-14 17:18:21 +0000
commitc9f07d9494bf7ba8630f8eb3006b56bf6d21b9f7 (patch)
treef6304b4e4760baa52d57bc541a2c315cc6dfb7c8
parentaeec3d3fa3c5014cbec45f3eefc0889cd1793a62 (diff)
Slightly more compact representation of 'a substituted type,
removing an unneeded indirection. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16781 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--checker/cic.mli9
-rw-r--r--checker/declarations.ml33
-rw-r--r--checker/values.ml6
-rw-r--r--kernel/mod_subst.ml40
4 files changed, 36 insertions, 52 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index 7e0cae20a..93dc84fa5 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -128,11 +128,12 @@ type substitution = (module_path * delta_resolver) umap_t
(** {6 Delayed constr} *)
-type 'a lazy_subst =
- | LSval of 'a
- | LSlazy of substitution list * 'a
+type 'a substituted = {
+ mutable subst_value : 'a;
+ mutable subst_subst : substitution list;
+}
-type constr_substituted = constr lazy_subst ref
+type constr_substituted = constr substituted
(** Nota : in coqtop, the [lazy_constr] type also have a [Direct]
constructor, but it shouldn't occur inside a .vo, so we ignore it *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index eec76ba39..a6a7f9405 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -271,8 +271,6 @@ let rec map_kn f f' c =
let subst_mps sub c =
if is_empty_subst sub then c
else map_kn (subst_ind sub) (subst_con0 sub) c
-
-let from_val a = ref (LSval a)
let rec replace_mp_in_mp mpfrom mpto mp =
match mp with
@@ -396,27 +394,20 @@ let join subst1 subst2 =
let subst = Umap.fold mp_apply_subst mbi_apply_subst subst1 empty_subst in
Umap.join subst2 subst
-let force fsubst r =
- match !r with
- | LSval a -> a
- | LSlazy(s,a) ->
- match List.rev s with
- | [] -> assert false
- | sub0::subs ->
- let subst = List.fold_left join sub0 subs in
- let a' = fsubst subst a in
- r := LSval a';
- a'
-
-let subst_substituted s r =
- match !r with
- | LSval a -> ref (LSlazy([s],a))
- | LSlazy(s',a) ->
- ref (LSlazy(s::s',a))
+let from_val x = { subst_value = x; subst_subst = []; }
-let force_constr = force subst_mps
+let force fsubst r = match r.subst_subst with
+| [] -> r.subst_value
+| s ->
+ let subst = List.fold_left join empty_subst (List.rev s) in
+ let x = fsubst subst r.subst_value in
+ let () = r.subst_subst <- [] in
+ let () = r.subst_value <- x in
+ x
-let from_val c = ref (LSval c)
+let subst_substituted s r = { r with subst_subst = s :: r.subst_subst; }
+
+let force_constr = force subst_mps
let subst_constr_subst = subst_substituted
diff --git a/checker/values.ml b/checker/values.ml
index 3d77339dc..55c6367a7 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 01def72abe22a5b53c7cbe4de4b9695b checker/cic.mli
+MD5 96dc15ee04e3baa6502b4d78c35d4b76 checker/cic.mli
*)
@@ -172,9 +172,7 @@ let v_subst =
(** kernel/lazyconstr *)
let v_substituted v_a =
- v_ref
- (v_sum "constr_substituted" 0
- [|[|v_a|];[|List v_subst;v_a|]|])
+ v_tuple "substituted" [|v_a; List v_subst|]
let v_cstr_subst = v_substituted v_constr
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 65d2b46d1..b79276750 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -531,31 +531,25 @@ let occur_mbid mbi sub =
false
with Exit -> true
-type 'a lazy_subst =
- | LSval of 'a
- | LSlazy of substitution list * 'a
+type 'a substituted = {
+ mutable subst_value : 'a;
+ mutable subst_subst : substitution list;
+}
-type 'a substituted = 'a lazy_subst ref
+let from_val x = { subst_value = x; subst_subst = []; }
-let from_val a = ref (LSval a)
+let force fsubst r = match r.subst_subst with
+| [] -> r.subst_value
+| s ->
+ let subst = List.fold_left join empty_subst (List.rev s) in
+ let x = fsubst subst r.subst_value in
+ let () = r.subst_subst <- [] in
+ let () = r.subst_value <- x in
+ x
-let force fsubst r =
- match !r with
- | LSval a -> a
- | LSlazy(s,a) ->
- let subst = List.fold_left join empty_subst (List.rev s) in
- let a' = fsubst subst a in
- r := LSval a';
- a'
-
-let subst_substituted s r =
- match !r with
- | LSval a -> ref (LSlazy([s],a))
- | LSlazy(s',a) ->
- ref (LSlazy(s::s',a))
+let subst_substituted s r = { r with subst_subst = s :: r.subst_subst; }
(* debug *)
-let repr_substituted r =
- match !r with
- | LSval a -> None, a
- | LSlazy(s,a) -> Some s, a
+let repr_substituted r = match r.subst_subst with
+| [] -> None, r.subst_value
+| s -> Some s, r.subst_value