lazily ==> call_by_name (since it is really a call_by_name!)

The default is now false (i.e. call_by_value strategy) to make an example
of Fourier application type-check in 8s instead of 1h40m!!!

We also tried a call_by_need strategy (not committed).
The results obtained are so far equivalent to the call_by_value strategy
(that is why we did not commit the code).

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index 3b769b5bcec98db1a51ca07c7d7ea8c1a9bce386..55db97045845401538bd4a4557963c17ad32b858 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -50,7 +50,7 @@ type stack = Cic.term list;;
 type config =
  int * env * Cic.term Cic.explicit_named_substitution * Cic.term * stack;;
 
-let lazily = true;;
+let call_by_name = false;;   (* false means call_by_value *)
 
 (* k is the length of the environment e *)
 (* m is the current depth inside the term *)
@@ -282,14 +282,14 @@ let reduce context : config -> Cic.term =
    | (k, e, ens, C.Lambda (_,_,t), p::s) ->
        reduce (k+1, p::e, ens, t,s) 
    (* lazy *)
-   | (k, e, ens, (C.LetIn (_,m,t) as t'), s) when lazily ->
+   | (k, e, ens, (C.LetIn (_,m,t) as t'), s) when call_by_name ->
       let m' = unwind k e ens m in reduce (k+1, m'::e, ens, t, s)
    (* strict *)
    | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
       let m' = reduce (k,e,ens,m,[]) in reduce (k+1,m'::e,ens,t,s)
    | (_, _, _, C.Appl [], _) -> raise (Impossible 1)
    (* lazy *)
-   | (k, e, ens, C.Appl (he::tl), s) when lazily ->
+   | (k, e, ens, C.Appl (he::tl), s) when call_by_name ->
       let tl' = List.map (unwind k e ens) tl in
        reduce (k, e, ens, he, (List.append tl' s))
    (* strict, but constants are NOT unfolded *)