diff options
| -rw-r--r-- | kernel/reduction.ml | 55 |
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 |