Remove dead code in lazy reduction machine.

3 files changed, 8 insertions, 32 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index ea9b2755f2..bc414d9715 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -346,7 +346,6 @@ and fterm =
   | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
-  | FCase of case_info * fconstr * fconstr * fconstr array
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
   | FLambda of int * (Name.t * constr) list * constr * fconstr subs
   | FProd of Name.t * fconstr * fconstr
@@ -376,7 +375,6 @@ let update v1 no t =
 
 type stack_member =
   | Zapp of fconstr array
-  | Zcase of case_info * fconstr * fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
   | Zproj of int * int * constant
   | Zfix of fconstr * stack
@@ -569,10 +567,6 @@ let rec to_constr constr_fun lfts v =
     | FFlex (ConstKey op) -> mkConstU op
     | FInd op -> mkIndU op
     | FConstruct op -> mkConstructU op
-    | FCase (ci,p,c,ve) ->
-	mkCase (ci, constr_fun lfts p,
-                constr_fun lfts c,
-		CArray.Fun1.map constr_fun lfts ve)
     | FCaseT (ci,p,c,ve,env) ->
 	mkCase (ci, constr_fun lfts (mk_clos env p),
                 constr_fun lfts c,
@@ -646,9 +640,6 @@ let rec zip m stk =
   match stk with
     | [] -> m
     | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s
-    | Zcase(ci,p,br)::s ->
-        let t = FCase(ci, p, m, br) in
-        zip {norm=neutr m.norm; term=t} s
     | ZcaseT(ci,p,br,e)::s ->
         let t = FCaseT(ci, p, m, br, e) in
         zip {norm=neutr m.norm; term=t} s
@@ -731,7 +722,7 @@ let rec get_args n tys f e stk =
 
 (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
 let rec eta_expand_stack = function
-  | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _ 
+  | (Zapp _ | Zfix _ | ZcaseT _ | Zproj _
 	| Zshift _ | Zupdate _ as e) :: s ->
       e :: eta_expand_stack s
   | [] ->
@@ -842,7 +833,6 @@ let rec knh info m stk =
     | FCLOS(t,e) -> knht info e t (zupdate m stk)
     | FLOCKED -> assert false
     | FApp(a,b) -> knh info a (append_stack b (zupdate m stk))
-    | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk)
     | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate m stk)
     | FFix(((ri,n),(_,_,_)),_) ->
         (match get_nth_arg m ri.(n) stk with
@@ -904,10 +894,6 @@ let rec knr info m stk =
         | None -> (set_norm m; (m,stk)))
   | FConstruct((ind,c),u) when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
-          (depth, args, Zcase(ci,_,br)::s) ->
-            assert (ci.ci_npar>=0);
-            let rargs = drop_parameters depth ci.ci_npar args in
-            kni info br.(c-1) (rargs@s)
         | (depth, args, ZcaseT(ci,_,br,e)::s) ->
             assert (ci.ci_npar>=0);
             let rargs = drop_parameters depth ci.ci_npar args in
@@ -924,7 +910,7 @@ let rec knr info m stk =
         | (_,args,s) -> (m,args@s))
   | FCoFix _ when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
-          (_, args, (((Zcase _|ZcaseT _|Zproj _)::_) as stk')) ->
+          (_, args, (((ZcaseT _|Zproj _)::_) as stk')) ->
             let (fxe,fxbd) = contract_fix_vect m.term in
             knit info fxe fxbd (args@stk')
         | (_,args,s) -> (m,args@s))
@@ -953,9 +939,6 @@ let rec zip_term zfun m stk =
     | [] -> m
     | Zapp args :: s ->
         zip_term zfun (mkApp(m, Array.map zfun args)) s
-    | Zcase(ci,p,br)::s ->
-        let t = mkCase(ci, zfun p, m, Array.map zfun br) in
-        zip_term zfun t s
     | ZcaseT(ci,p,br,e)::s ->
         let t = mkCase(ci, zfun (mk_clos e p), m,
 		       Array.map (fun b -> zfun (mk_clos e b)) br) in
diff --git a/kernel/closure.mli b/kernel/closure.mli
index a3b0e0f301..c6f212aa55 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -119,7 +119,6 @@ type fterm =
   | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
-  | FCase of case_info * fconstr * fconstr * fconstr array
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
   | FLambda of int * (Name.t * constr) list * constr * fconstr subs
   | FProd of Name.t * fconstr * fconstr
@@ -136,7 +135,6 @@ type fterm =
 
 type stack_member =
   | Zapp of fconstr array
-  | Zcase of case_info * fconstr * fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
   | Zproj of int * int * constant
   | Zfix of fconstr * stack
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 3253cddf7c..2cf3f88735 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -56,8 +56,7 @@ 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) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
     | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -91,9 +90,8 @@ let pure_stack lfts stk =
                 let (lfx,pa) = pure_rec l a in
                 (l, Zlfix((lfx,fx),pa)::pstk)
             | (ZcaseT(ci,p,br,e),(l,pstk)) ->
-                (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk)
-            | (Zcase(ci,p,br),(l,pstk)) ->
-                (l,Zlcase(ci,l,p,br)::pstk)) in
+                (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk))
+  in
   snd (pure_rec lfts stk)
 
 (****************************************************************************)
@@ -237,7 +235,6 @@ let rec no_arg_available = function
   | Zshift _ :: stk -> no_arg_available stk
   | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk
   | Zproj _ :: _ -> true
-  | Zcase _ :: _ -> true
   | ZcaseT _ :: _ -> true
   | Zfix _ :: _ -> true
 
@@ -250,7 +247,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
 
@@ -260,13 +256,12 @@ let rec no_case_available = function
   | Zshift _ :: stk -> no_case_available stk
   | Zapp _ :: stk -> no_case_available stk
   | Zproj (_,_,p) :: _ -> false
-  | Zcase _ :: _ -> false
   | ZcaseT _ :: _ -> false
   | Zfix _ :: _ -> true
 
 let in_whnf (t,stk) =
   match fterm_of t with
-    | (FLetIn _ | FCase _ | FCaseT _ | FApp _ 
+    | (FLetIn _ | FCaseT _ | FApp _ 
 	  | FCLOS _ | FLIFT _ | FCast _) -> false
     | FLambda _ -> no_arg_available stk
     | FConstruct _ -> no_case_available stk
@@ -532,8 +527,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         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 *)