From: Claudio Sacerdoti Coen Date: Wed, 27 Nov 2002 17:25:51 +0000 (+0000) Subject: lazily ==> call_by_name (since it is really a call_by_name!) X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9d35b4005007408a49a76864302f03db8aa7789a;p=helm.git 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 3b769b5bc..55db97045 100644 --- 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 *)