From ed936515481f5035fde443f4aee55b86e427cef4 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 10 Jul 2007 18:48:14 +0000
Subject: [PATCH] New reduction strategy: the new reduction strategy behaves as
 the previous one (performing both CVN and CBV in parallel), but it is much
 more lazy. In particular, unwinding is never performed twice on the same
 term. On assembly/assembly.ma this seems to solve every performance problem.
 Let's see what happens this night with the benchmarks.

---
 .../cic_proof_checking/cicReduction.ml        | 39 ++++++++++++++++---
 1 file changed, 34 insertions(+), 5 deletions(-)

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 213aa2356..af5564d07 100644
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -55,8 +55,14 @@ module type Strategy =
   type env_term
   type ens_term
   type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
-  val to_env : config -> env_term
-  val to_ens : config -> ens_term
+  val to_env :
+   reduce: (config -> config) ->
+   unwind: (config -> Cic.term) ->
+   config -> env_term
+  val to_ens :
+   reduce: (config -> config) ->
+   unwind: (config -> Cic.term) ->
+   config -> ens_term
   val from_stack : stack_term -> config
   val from_stack_list_for_unwind :
    unwind: (config -> Cic.term) ->
@@ -106,6 +112,28 @@ module CallByValueByNameForUnwind =
  end
 ;;
 
+module CallByValueByNameForUnwind' =
+ struct
+  type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
+  and stack_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *)
+  and env_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *)
+  and ens_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *)
+
+  let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
+  let to_ens ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
+  let from_stack (c,_) = Lazy.force c
+  let from_stack_list_for_unwind ~unwind l = List.map (function (_,c) -> Lazy.force c) l
+  let from_env (c,_) = Lazy.force c
+  let from_ens (c,_) = Lazy.force c
+  let from_env_for_unwind ~unwind (_,c) = Lazy.force c
+  let from_ens_for_unwind ~unwind (_,c) = Lazy.force c
+  let stack_to_env ~reduce ~unwind config = config
+  let compute_to_env ~reduce ~unwind k e ens t =
+   lazy (reduce (k,e,ens,t,[])), lazy (unwind (k,e,ens,t,[]))
+  let compute_to_stack ~reduce ~unwind config = lazy (reduce config), lazy (unwind config)
+ end
+;;
+
 
 (* Old Machine
 module CallByNameStrategy =
@@ -717,7 +745,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
                       else
                        (incr counter ;
                         build_env
-                         ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e'))
+                         ((RS.to_env ~reduce ~unwind (k,e,ens,C.Fix (!counter -1, fl),[]))::e'))
                      in
                       build_env e
                     in
@@ -738,7 +766,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
     function
        [] -> ens
      | (uri,t)::tl ->
-         push_exp_named_subst k e ((uri,RS.to_ens (k,e,ens,t,[]))::ens) tl
+         push_exp_named_subst k e ((uri,RS.to_ens ~reduce ~unwind (k,e,ens,t,[]))::ens) tl
    in
     reduce
   ;;
@@ -767,7 +795,8 @@ module R = Reduction
  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 *)
-module R = Reduction(CallByValueByNameForUnwind);;
+(*module R = Reduction(CallByValueByNameForUnwind);;*)
+module R = Reduction(CallByValueByNameForUnwind');;
 (*module R = Reduction(CallByNameStrategy);;*)
 (*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*)
 module U = UriManager;;
-- 
2.39.2