improve efficiency of the reduction interpreter of the checker

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

1 files changed, 19 insertions, 11 deletions

diff --git a/checker/reduction.ml b/checker/reduction.ml
index aa9639e55..e333b67c3 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -42,7 +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,_,_)::s1, Zcase(c2,_,_)::s2) ->
+    | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1,
+       (Zcase(c2,_,_)|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
@@ -75,6 +76,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,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
   snd (pure_rec lfts stk)
@@ -176,6 +179,7 @@ let rec no_arg_available = function
   | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk
   | Zproj _ :: _ -> true
   | Zcase _ :: _ -> true
+  | ZcaseT _ :: _ -> true
   | Zfix _ :: _ -> true
 
 let rec no_nth_arg_available n = function
@@ -188,6 +192,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
@@ -197,11 +202,12 @@ let rec no_case_available = function
   | 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 _ | 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
@@ -414,8 +420,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 _, _) | (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 *)
@@ -430,21 +436,23 @@ and convert_stacks univ infos lft1 lft2 stk1 stk2 =
 and convert_vect univ infos lft1 lft2 v1 v2 =
   Array.iter2 (fun t1 t2 -> ccnv univ CONV infos lft1 lft2 t1 t2) v1 v2
 
-let clos_fconv cv_pb env t1 t2 =
-  let infos = create_clos_infos betaiotazeta env in
+let clos_fconv cv_pb eager_delta env t1 t2 =
+  let infos =
+    create_clos_infos
+      (if eager_delta then betadeltaiota else betaiotazeta) env in
   let univ = universes env in
   ccnv univ cv_pb infos el_id el_id (inject t1) (inject t2)
 
-let fconv cv_pb env t1 t2 =
+let fconv cv_pb eager_delta env t1 t2 =
   if eq_constr t1 t2 then ()
-  else clos_fconv cv_pb env t1 t2
+  else clos_fconv cv_pb eager_delta env t1 t2
 
-let conv = fconv CONV
-let conv_leq = fconv CUMUL
+let conv = fconv CONV false
+let conv_leq = fconv CUMUL false
 
 (* option for conversion : no compilation for the checker *)
 
-let vm_conv = fconv
+let vm_conv cv_pb = fconv cv_pb true
 
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)