X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_proof_checking%2FcicReduction.ml;h=af5564d0754c32c39a594bdef0ad2ba6552dd298;hb=4cf7ea219b305d196710d96014fc3e5e11a7facd;hp=213aa2356bd1e3d9940efccdc4420f1e7dd05b2b;hpb=37a375b59014cdfaa15f50e2a7bbed29871adb9b;p=helm.git

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index 213aa2356..af5564d07 100644
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/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;;