From 1e3d73abd90af8646222bc4d6ea42f7d7ed3ddd1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 23 Sep 2016 20:55:21 +0200 Subject: Fix bug #5096: [vm_compute] is exponentially slower than [native_compute]. The fix is essentially a revert of f22ad60 that introduced the use of the pretyper version of whd_all instead of the one from the kernel. The exact cause of slowness of the pretyper version is still to be investigated, but it is believed that it is due to a call-by-name strategy, to compare with call-by-need in the kernel. Note that there is still something fishy in presence of evars. Technically vm_compute does not handle them, but if this comes to be the case, it might be worthwile to use an evar-aware variant of whd_all. --- pretyping/vnorm.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'pretyping/vnorm.ml') diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c396f593b..e281f22df 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -46,7 +46,11 @@ let invert_tag cst tag reloc_tbl = with Find_at j -> (j+1) (* Argggg, ces constructeurs de ... qui commencent a 1*) -let find_rectype_a env c = Inductiveops.find_mrectype_vect env Evd.empty c +let find_rectype_a env c = + let (t, l) = decompose_appvect (whd_all env c) in + match kind_of_term t with + | Ind ind -> (ind, l) + | _ -> assert false (* Instantiate inductives and parameters in constructor type *) -- cgit v1.2.3