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

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