diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-23 20:55:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-23 21:02:18 +0200 |
| commit | 1e3d73abd90af8646222bc4d6ea42f7d7ed3ddd1 (patch) | |
| tree | 380eec492ad25568d8d3ef7661378253d13fd3da /pretyping/vnorm.ml | |
| parent | a321074cdd2f9375662c7c9f17be5c045328bd82 (diff) | |
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.
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 6 |
1 files changed, 5 insertions, 1 deletions
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 *) |