improve efficiency of the reduction interpreter of coqtop

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

Author: barras

kernel/closure.ml

@@ -346,7 +346,8 @@ and fterm =
   | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
-  | FCases of case_info * fconstr * fconstr * fconstr array
+  | 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
   | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
@@ -376,6 +377,7 @@ 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
   | Zshift of int
@@ -490,72 +492,7 @@ let zupdate m s =
     Zupdate(m)::s'
   else s
 
-(* Closure optimization: *)
-let rec compact_constr (lg, subs as s) c k =
-  match kind_of_term c with
-      Rel i ->
-        if i < k then s, c else
-          (try (lg,subs), mkRel (k + lg - List.index Int.equal (i-k+1) subs)
-          with Not_found -> (lg+1, (i-k+1)::subs), mkRel (k+lg))
-    | (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> s, c
-    | Evar(ev,v) ->
-        let (s, v') = compact_vect s v k in
-        if v==v' then s, c else s, mkEvar(ev, v')
-    | Cast(a,ck,b) ->
-        let (s, a') = compact_constr s a k in
-        let (s, b') = compact_constr s b k in
-        if a==a' && b==b' then s, c else s, mkCast(a', ck, b')
-    | App(f,v) ->
-        let (s, f') = compact_constr s f k in
-        let (s, v') = compact_vect s v k in
-        if f==f' && v==v' then s, c else s, mkApp(f',v')
-    | Proj (p,t) ->
-        let (s, t') = compact_constr s t k in
-	  if t'==t then s, c else s, mkProj (p,t')
-    | Lambda(n,a,b) ->
-        let (s, a') = compact_constr s a k in
-        let (s, b') = compact_constr s b (k+1) in
-        if a==a' && b==b' then s, c else s, mkLambda(n,a',b')
-    | Prod(n,a,b) ->
-        let (s, a') = compact_constr s a k in
-        let (s, b') = compact_constr s b (k+1) in
-        if a==a' && b==b' then s, c else s, mkProd(n,a',b')
-    | LetIn(n,a,ty,b) ->
-        let (s, a') = compact_constr s a k in
-        let (s, ty') = compact_constr s ty k in
-        let (s, b') = compact_constr s b (k+1) in
-        if a==a' && ty==ty' && b==b' then s, c else s, mkLetIn(n,a',ty',b')
-    | Fix(fi,(na,ty,bd)) ->
-        let (s, ty') = compact_vect s ty k in
-        let (s, bd') = compact_vect s bd (k+Array.length ty) in
-        if ty==ty' && bd==bd' then s, c else s, mkFix(fi,(na,ty',bd'))
-    | CoFix(i,(na,ty,bd)) ->
-        let (s, ty') = compact_vect s ty k in
-        let (s, bd') = compact_vect s bd (k+Array.length ty) in
-        if ty==ty' && bd==bd' then s, c else s, mkCoFix(i,(na,ty',bd'))
-    | Case(ci,p,a,br) ->
-        let (s, p') = compact_constr s p k in
-        let (s, a') = compact_constr s a k in
-        let (s, br') = compact_vect s br k in
-        if p==p' && a==a' && br==br' then s, c else s, mkCase(ci,p',a',br')
-
-and compact_vect s v k =
-  let fold s c = compact_constr s c k in
-  Array.smartfoldmap fold s v
-
-(* Computes the minimal environment of a closure.
-   Idea: if the subs is not identity, the term will have to be
-   reallocated entirely (to propagate the substitution). So,
-   computing the set of free variables does not change the
-   complexity. *)
-let optimise_closure env c =
-  if is_subs_id env then (env,c) else
-    let ((_,s), c') = compact_constr (0,[]) c 1 in
-    let env' = Array.map_of_list (fun i -> clos_rel env i) s in
-    (subs_cons (env', subs_id 0),c')
-
 let mk_lambda env t =
-  let (env,t) = optimise_closure env t in
   let (rvars,t') = decompose_lam t in
   FLambda(List.length rvars, List.rev rvars, t', env)
 
@@ -601,8 +538,7 @@ let mk_clos_deep clos_fun env t =
 	  term = FProj (p, clos_fun env c) }
     | Case (ci,p,c,v) ->
         { norm = Red;
-	  term = FCases (ci, clos_fun env p, clos_fun env c,
-			 CArray.Fun1.map clos_fun env v) }
+	  term = FCaseT (ci, p, clos_fun env c, v, env) }
     | Fix fx ->
         { norm = Cstr; term = FFix (fx, env) }
     | CoFix cfx ->
@@ -633,10 +569,14 @@ let rec to_constr constr_fun lfts v =
     | FFlex (ConstKey op) -> mkConstU op
     | FInd op -> mkIndU op
     | FConstruct op -> mkConstructU op
-    | FCases (ci,p,c,ve) ->
+    | 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,
+		Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve)
     | FFix ((op,(lna,tys,bds)),e) ->
         let n = Array.length bds in
         let ftys = CArray.Fun1.map mk_clos e tys in
@@ -702,35 +642,24 @@ let rec fstrong unfreeze_fun lfts v =
   to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v)
 *)
 
-let rec zip m stk rem = match stk with
-| [] ->
-  begin match rem with
-  | [] -> m
-  | stk :: rem -> zip m stk rem
-  end
-| Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s rem
-| Zcase(ci,p,br)::s ->
-  let t = FCases(ci, p, m, br) in
-  zip {norm=neutr m.norm; term=t} s rem
-| Zproj (i,j,cst) :: s -> 
-  zip {norm=neutr m.norm; term=FProj (Projection.make cst true,m)} s rem
-| Zfix(fx,par)::s ->
-  zip fx par ((Zapp [|m|] :: s) :: rem)
-| Zshift(n)::s ->
-  zip (lift_fconstr n m) s rem
-| Zupdate(rf)::s ->
-  zip_update m s rem rf
-
-and zip_update m stk rem rf = match stk with
-| [] ->
-  begin match rem with
-  | [] -> update rf m.norm m.term
-  | stk :: rem -> zip_update m stk rem rf
-  end
-| Zupdate rf :: s -> zip_update m s rem rf
-| s -> zip (update rf m.norm m.term) s rem
-
-let zip m stk = zip m stk []
+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
+    | Zproj (i,j,cst) :: s -> 
+        zip {norm=neutr m.norm; term=FProj(Projection.make cst true,m)} s
+    | Zfix(fx,par)::s ->
+        zip fx (par @ append_stack [|m|] s)
+    | Zshift(n)::s ->
+        zip (lift_fconstr n m) s
+    | Zupdate(rf)::s ->
+        zip (update rf m.norm m.term) s
 
 let fapp_stack (m,stk) = zip m stk
 
@@ -802,7 +731,8 @@ 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 _ | Zshift _ | Zupdate _ | Zproj _ as e) :: s ->
+  | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _ 
+	| Zshift _ | Zupdate _ as e) :: s ->
       e :: eta_expand_stack s
   | [] ->
       [Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]]
@@ -930,7 +860,8 @@ 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))
-    | FCases(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::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
              (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
@@ -958,7 +889,7 @@ and knht info e t stk =
     | App(a,b) ->
         knht info e a (append_stack (mk_clos_vect e b) stk)
     | Case(ci,p,t,br) ->
-        knht info e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk)
+        knht info e t (ZcaseT(ci, p, br, e)::stk)
     | Fix _ -> knh info (mk_clos2 e t) stk
     | Cast(a,_,_) -> knht info e a stk
     | Rel n -> knh info (clos_rel e n) stk
@@ -995,6 +926,10 @@ let rec knr info m stk =
             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
+            knit info e br.(c-1) (rargs@s)
         | (_, cargs, Zfix(fx,par)::s) ->
             let rarg = fapp_stack(m,cargs) in
             let stk' = par @ append_stack [|rarg|] s in
@@ -1007,7 +942,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 _::_) as stk')) ->
+          (_, args, (((Zcase _|ZcaseT _)::_) as stk')) ->
             let (fxe,fxbd) = contract_fix_vect m.term in
             knit info fxe fxbd (args@stk')
         | (_,args,s) -> (m,args@s))
@@ -1039,6 +974,10 @@ let rec zip_term zfun m stk =
     | 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
+        zip_term zfun t s
     | Zproj(_,_,p)::s -> 
         let t = mkProj (Projection.make p true, m) in 
 	zip_term zfun t s

kernel/closure.mli

@@ -119,7 +119,8 @@ type fterm =
   | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
-  | FCases of case_info * fconstr * fconstr * fconstr array
+  | 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
   | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
@@ -136,6 +137,7 @@ 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
   | Zshift of int
@@ -228,6 +230,5 @@ val knr: clos_infos -> fconstr -> stack -> fconstr * stack
 val kl : clos_infos -> fconstr -> constr
 
 val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
-val optimise_closure : fconstr subs -> constr -> fconstr subs * constr
 
 (** End of cbn debug section i*)

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 *)