aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-02-13 18:37:57 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-03-04 15:13:02 +0100
commitf3aa5579c36223c98968c82545500340d76b5378 (patch)
tree32e426f0eb3492dbb5e78548f7c000c756de712b
parent16c884413bbf2f0b5fb43bd0be7da0bf7c5e4e75 (diff)
Remove whd_both from the kernel.
Now that the cache is distinct, there should be no nasty side-effects changing the value of one side while reducing the other.
-rw-r--r--kernel/reduction.ml55
1 files changed, 6 insertions, 49 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index ea17b2559..aba2b5535 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -313,47 +313,6 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
else raise NotConvertible
-let rec no_arg_available = function
- | [] -> true
- | Zupdate _ :: stk -> no_arg_available stk
- | Zshift _ :: stk -> no_arg_available stk
- | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk
- | Zproj _ :: _ -> true
- | ZcaseT _ :: _ -> true
- | Zfix _ :: _ -> true
-
-let rec no_nth_arg_available n = function
- | [] -> true
- | Zupdate _ :: stk -> no_nth_arg_available n stk
- | Zshift _ :: stk -> no_nth_arg_available n stk
- | Zapp v :: stk ->
- let k = Array.length v in
- if n >= k then no_nth_arg_available (n-k) stk
- else false
- | Zproj _ :: _ -> true
- | ZcaseT _ :: _ -> true
- | Zfix _ :: _ -> true
-
-let rec no_case_available = function
- | [] -> true
- | Zupdate _ :: stk -> no_case_available stk
- | Zshift _ :: stk -> no_case_available stk
- | Zapp _ :: stk -> no_case_available stk
- | Zproj (_,_,p) :: _ -> false
- | ZcaseT _ :: _ -> false
- | Zfix _ :: _ -> true
-
-let in_whnf (t,stk) =
- match fterm_of t with
- | (FLetIn _ | FCaseT _ | FApp _
- | FCLOS _ | FLIFT _ | FCast _) -> false
- | FLambda _ -> no_arg_available stk
- | FConstruct _ -> no_case_available stk
- | FCoFix _ -> no_case_available stk
- | FFix(((ri,n),(_,_,_)),_) -> no_nth_arg_available ri.(n) stk
- | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true
- | FLOCKED -> assert false
-
type conv_tab = {
cnv_inf : clos_infos;
lft_tab : fconstr infos_tab;
@@ -362,6 +321,9 @@ type conv_tab = {
(** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory
location contained both in tl and in tr. *)
+(** The same heap separation invariant must hold for the fconstr arguments
+ passed to each respective side of the conversion function below. *)
+
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
@@ -371,14 +333,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
Control.check_for_interrupt ();
(* First head reduce both terms *)
let ninfos = infos_with_reds infos.cnv_inf betaiotazeta in
- let rec whd_both (t1,stk1) (t2,stk2) =
- let st1' = whd_stack ninfos infos.lft_tab t1 stk1 in
- let st2' = whd_stack ninfos infos.rgt_tab t2 stk2 in
- (* Now, whd_stack on term2 might have modified st1 (due to sharing),
- and st1 might not be in whnf anymore. If so, we iterate ccnv. *)
- if in_whnf st1' then (st1',st2') else whd_both st1' st2' in
- let ((hd1,v1),(hd2,v2)) = whd_both st1 st2 in
- let appr1 = (lft1,(hd1,v1)) and appr2 = (lft2,(hd2,v2)) in
+ let (hd1, v1 as appr1) = whd_stack ninfos infos.lft_tab (fst st1) (snd st1) in
+ let (hd2, v2 as appr2) = whd_stack ninfos infos.rgt_tab (fst st2) (snd st2) in
+ let appr1 = (lft1, appr1) and appr2 = (lft2, appr2) in
(** We delay the computation of the lifts that apply to the head of the term
with [el_stack] inside the branches where they are actually used. *)
match (fterm_of hd1, fterm_of hd2) with