improve efficiency of the reduction interpreter of coqtop

Conflicts:
	kernel/closure.ml
	kernel/closure.mli
	kernel/reduction.ml

1 files changed, 11 insertions, 4 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0ed6fd359c..a6b05d6071 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -64,7 +64,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,_,_)::s1, Zcase(c2,_,_)::s2) ->
+    | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1,
+       (Zcase(c2,_,_)|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
@@ -97,6 +98,8 @@ let pure_stack lfts stk =
             | (Zfix(fx,a),(l,pstk)) ->
                 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
   snd (pure_rec lfts stk)
@@ -243,6 +246,7 @@ let rec no_arg_available = function
   | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk
   | Zproj _ :: _ -> true
   | Zcase _ :: _ -> true
+  | ZcaseT _ :: _ -> true
   | Zfix _ :: _ -> true
 
 let rec no_nth_arg_available n = function
@@ -255,6 +259,7 @@ let rec no_nth_arg_available n = function
       else false
   | Zproj _ :: _ -> true
   | Zcase _ :: _ -> true
+  | ZcaseT _ :: _ -> true
   | Zfix _ :: _ -> true
 
 let rec no_case_available = function
@@ -264,11 +269,13 @@ let rec no_case_available = function
   | 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 _ | FCases _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false
+    | (FLetIn _ | FCase _ | FCaseT _ | FApp _ 
+	  | FCLOS _ | FLIFT _ | FCast _) -> false
     | FLambda _ -> no_arg_available stk
     | FConstruct _ -> no_case_available stk
     | FCoFix _ -> no_case_available stk
@@ -533,8 +540,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 _, _) | (FCases _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
-       | (_, FLetIn _) | (_,FCases _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
+     | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
+       | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
        | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
 
      (* In all other cases, terms are not convertible *)