]> matita.cs.unibo.it Git - helm.git/commitdiff
New reduction strategy: the new reduction strategy behaves as the previous
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 10 Jul 2007 18:48:14 +0000 (18:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 10 Jul 2007 18:48:14 +0000 (18:48 +0000)
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.

helm/software/components/cic_proof_checking/cicReduction.ml

index 213aa2356bd1e3d9940efccdc4420f1e7dd05b2b..af5564d0754c32c39a594bdef0ad2ba6552dd298 100644 (file)
@@ -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;;