improve efficiency of the reduction interpreter of the checker

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

1 files changed, 31 insertions, 88 deletions

diff --git a/checker/closure.ml b/checker/closure.ml
index 35c16d2ab..a8b2b30f8 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -279,11 +279,12 @@ and fterm =
   | FProj of constant * 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 * constr) list * constr * fconstr subs
   | FProd of name * fconstr * fconstr
   | FLetIn of name * fconstr * fconstr * constr * fconstr subs
-  | FEvar of existential_key * fconstr array
+  | FEvar of existential_key * fconstr array (* why diff from kernel/closure? *)
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
   | FLOCKED
@@ -306,6 +307,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
@@ -373,77 +375,7 @@ let zupdate m s =
     Zupdate(m)::s'
   else s
 
-(* Closure optimization: *)
-let rec compact_constr (lg, subs as s) c k =
-  match c with
-      Rel i ->
-        if i < k then c,s else
-          (try Rel (k + lg - List.index Int.equal (i-k+1) subs), (lg,subs)
-          with Not_found -> Rel (k+lg), (lg+1, (i-k+1)::subs))
-    | (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s
-    | Evar(ev,v) ->
-        let (v',s) = compact_vect s v k in
-        if v==v' then c,s else Evar(ev,v'),s
-    | Cast(a,ck,b) ->
-        let (a',s) = compact_constr s a k in
-        let (b',s) = compact_constr s b k in
-        if a==a' && b==b' then c,s else Cast(a', ck, b'), s
-    | App(f,v) ->
-        let (f',s) = compact_constr s f k in
-        let (v',s) = compact_vect s v k in
-        if f==f' && v==v' then c,s else App(f',v'), s
-    | Proj (p, t) -> 
-        let (t', s) = compact_constr s t k in
-	  if t' == t then c,s else Proj(p,t'), s
-    | Lambda(n,a,b) ->
-        let (a',s) = compact_constr s a k in
-        let (b',s) = compact_constr s b (k+1) in
-        if a==a' && b==b' then c,s else Lambda(n,a',b'), s
-    | Prod(n,a,b) ->
-        let (a',s) = compact_constr s a k in
-        let (b',s) = compact_constr s b (k+1) in
-        if a==a' && b==b' then c,s else Prod(n,a',b'), s
-    | LetIn(n,a,ty,b) ->
-        let (a',s) = compact_constr s a k in
-        let (ty',s) = compact_constr s ty k in
-        let (b',s) = compact_constr s b (k+1) in
-        if a==a' && ty==ty' && b==b' then c,s else LetIn(n,a',ty',b'), s
-    | Fix(fi,(na,ty,bd)) ->
-        let (ty',s) = compact_vect s ty k in
-        let (bd',s) = compact_vect s bd (k+Array.length ty) in
-        if ty==ty' && bd==bd' then c,s else Fix(fi,(na,ty',bd')), s
-    | CoFix(i,(na,ty,bd)) ->
-        let (ty',s) = compact_vect s ty k in
-        let (bd',s) = compact_vect s bd (k+Array.length ty) in
-        if ty==ty' && bd==bd' then c,s else CoFix(i,(na,ty',bd')), s
-    | Case(ci,p,a,br) ->
-        let (p',s) = compact_constr s p k in
-        let (a',s) = compact_constr s a k in
-        let (br',s) = compact_vect s br k in
-        if p==p' && a==a' && br==br' then c,s else Case(ci,p',a',br'),s
-and compact_vect s v k = compact_v [] s v k (Array.length v - 1)
-and compact_v acc s v k i =
-  if i < 0 then
-    let v' = Array.of_list acc in
-    if Array.for_all2 (==) v v' then v,s else v',s
-  else
-    let (a',s') = compact_constr s v.(i) k in
-    compact_v (a'::acc) s' v k (i-1)
-
-(* 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 (c',(_,s)) = compact_constr (0,[]) c 1 in
-    let env' =
-      Array.map (fun i -> clos_rel env i) (Array.of_list 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)
 
@@ -487,9 +419,7 @@ let mk_clos_deep clos_fun env t =
 	{ norm = Red;
 	  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,
-			 Array.map (clos_fun env) v) }
+        { norm = Red; term = FCaseT (ci, p, clos_fun env c, v, env) }
     | Fix fx ->
         { norm = Cstr; term = FFix (fx, env) }
     | CoFix cfx ->
@@ -520,10 +450,13 @@ let rec to_constr constr_fun lfts v =
     | FFlex (ConstKey op) -> Const op
     | FInd op -> Ind op
     | FConstruct op -> Construct op
-    | FCases (ci,p,c,ve) ->
+    | FCase (ci,p,c,ve) ->
 	Case (ci, constr_fun lfts p,
               constr_fun lfts c,
 	      Array.map (constr_fun lfts) ve)
+    | FCaseT (ci,p,c,ve,e) -> (* TODO: enable sharing, cf FCLOS below ? *)
+        to_constr constr_fun lfts
+	  {norm=Red;term=FCase(ci,mk_clos2 e p,c,mk_clos_vect e ve)}
     | FFix ((op,(lna,tys,bds)),e) ->
         let n = Array.length bds in
         let ftys = Array.map (mk_clos e) tys in
@@ -573,6 +506,8 @@ let term_of_fconstr =
       | FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t
       | FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts ->
           compose_lam (List.rev tys) f
+      | FCaseT(ci,p,c,b,env) when is_subs_id env && is_lift_id lfts ->
+          Case(ci,p,term_of_fconstr_lift lfts c,b)
       | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> Fix fx
       | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> CoFix cfx
       | _ -> to_constr term_of_fconstr_lift lfts v in
@@ -592,7 +527,10 @@ let rec zip m stk =
     | [] -> m
     | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s
     | Zcase(ci,p,br)::s ->
-        let t = FCases(ci, p, m, br) in
+        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 (cst,m)} s
@@ -672,7 +610,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}|]]
@@ -790,7 +729,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,env) -> knh info t (ZcaseT(ci,p,br,env)::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')
@@ -814,12 +754,11 @@ and knht info e t stk =
   match t with
     | 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)
-    | Fix _ -> knh info (mk_clos2 e t) stk
+    | Case(ci,p,t,br) -> knht info e t (ZcaseT(ci, p, br, e)::stk)
+    | Fix _ -> knh info (mk_clos2 e t) stk (* laziness *)
     | Cast(a,_,_) -> knht info  e a stk
     | Rel n -> knh info (clos_rel e n) stk
-    | Proj (p,c) -> knh info (mk_clos2 e t) stk
+    | Proj (p,c) -> knh info (mk_clos2 e t) stk (* laziness *)
     | (Lambda _|Prod _|Construct _|CoFix _|Ind _|
        LetIn _|Const _|Var _|Evar _|Meta _|Sort _) ->
         (mk_clos2 e t, stk)
@@ -852,19 +791,23 @@ 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)
-        | (_, cargs, Zfix(fx,par)::s) ->
+       | (depth, args, ZcaseT(ci,_,br,env)::s) ->
+            assert (ci.ci_npar>=0);
+            let rargs = drop_parameters depth ci.ci_npar args in
+            knit info env 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
             let (fxe,fxbd) = contract_fix_vect fx.term in
             knit info fxe fxbd stk'
-	| (depth, args, Zproj (n, m, cst)::s) ->
+       | (depth, args, Zproj (n, m, cst)::s) ->
 	    let rargs = drop_parameters depth n args in
 	    let rarg = project_nth_arg m rargs in
-	      kni info rarg s
-        | (_,args,s) -> (m,args@s))
+	    kni info rarg s
+       | (_,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))