diff options
| -rw-r--r-- | checker/cic.mli | 9 | ||||
| -rw-r--r-- | checker/declarations.ml | 33 | ||||
| -rw-r--r-- | checker/values.ml | 6 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 40 |
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 |