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?

1 files changed, 3 insertions, 1 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3819a9223..3837ef0c8 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) ->