From dc334ef9fb37894658bdc51b931a0a7784dbdaa3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Nov 2014 16:37:10 +0100
Subject: Evar normalization is now done eagerly.

As witnessed in the ProjectiveGeometry contrib, some evar normalization were
taking ages because of an exponential behaviour due to a call-by-name
substitution: when normalizing an evar, its arguments were substituted right
away and the resulting term was then normalized, leading to a potential
duplication of normalizations.

Now we normalize evar arguments before substituting them, in a call-by-value
fashion. It makes examples from ProjectiveGeometry compile instanteanously
when they were killing the machine due to excessive memory allocation before
the patch.

Note that there is a tension here: we may be normalizing evar arguments too
eagerly, and try a call-by-need approach instead. To choose which particular
strategy we use, we should do some benchmarks... On stdlib, call-by-value
and call-by-need seem indistinguishable. To be continued?
---
 pretyping/reductionops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3819a92233..3837ef0c8f 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1170,7 +1170,9 @@ let whd_zeta c = Stack.zip (local_whd_state_gen zeta Evd.empty (c,Stack.empty))
 let rec whd_evar sigma c =
   match kind_of_term c with
     | Evar ev ->
-        (match safe_evar_value sigma ev with
+        let (evk, args) = ev in
+        let args = Array.map (fun c -> whd_evar sigma c) args in
+        (match safe_evar_value sigma (evk, args) with
             Some c -> whd_evar sigma c
           | None -> c)
     | Sort (Type u) -> 
-- 
cgit v1.2.3