diff options
Diffstat (limited to 'checker/reduction.ml')
| -rw-r--r-- | checker/reduction.ml | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index 6d8783d7e..9b8eac04c 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -42,8 +42,8 @@ let compare_stack_shape stk1 stk2 = | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1, - (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) -> + | ((ZcaseT(c1,_,_,_))::s1, + (ZcaseT(c2,_,_,_))::s2) -> bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -78,8 +78,7 @@ let pure_stack lfts stk = (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,env),(l,pstk)) -> (l,Zlcase(ci,l,mk_clos env p,mk_clos_vect env br)::pstk) - | (Zcase(ci,p,br),(l,pstk)) -> - (l,Zlcase(ci,l,p,br)::pstk)) in + ) in snd (pure_rec lfts stk) (****************************************************************************) @@ -243,7 +242,6 @@ let rec no_arg_available = function | Zshift _ :: stk -> no_arg_available stk | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -256,7 +254,6 @@ let rec no_nth_arg_available n = function if n >= k then no_nth_arg_available (n-k) stk else false | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -266,13 +263,12 @@ let rec no_case_available = function | Zshift _ :: stk -> no_case_available stk | Zapp _ :: stk -> no_case_available stk | Zproj (_,_,_) :: _ -> false - | Zcase _ :: _ -> false | ZcaseT _ :: _ -> false | Zfix _ :: _ -> true let in_whnf (t,stk) = match fterm_of t with - | (FLetIn _ | FCase _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false + | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false | FLambda _ -> no_arg_available stk | FConstruct _ -> no_case_available stk | FCoFix _ -> no_case_available stk @@ -504,8 +500,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = else raise NotConvertible (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) - | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) - | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) + | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) + | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false (* In all other cases, terms are not convertible *) |