Expanding a definition used as a macro in CClosure.

While thought as a macro, the with_stats function was calling lazy + Lazy.force,
which has a remarkable cost in the implementation, as it allocates and breaches
the write barrier. We simply expand the definition twice, breaking the
abstraction but gaining in performance.

Author: ppedrot

kernel/cClosure.ml

@@ -1057,11 +1057,23 @@ and norm_head_array info env n (v : constr array) =
 
 (* weak reduction *)
 let whd_val info v =
-  with_stats (lazy (term_of_fconstr (kh info v [])))
+  if !stats then begin
+    reset();
+    let r = term_of_fconstr (kh info v []) in
+    stop();
+    r
+  end else
+    term_of_fconstr (kh info v [])
 
 (* strong reduction *)
 let norm_val info v =
-  with_stats (lazy (kl info v))
+  if !stats then begin
+    reset();
+    let r = kl info v in
+    stop();
+    r
+  end else
+    kl info v
 
 let inject c = mk_clos (subs_id 0) c