Bug#587730: Include patch r1875, fixing an off-by-one bug causing sensible slowdowns
Package: ssreflect
Severity: wishlist
>From upstream VCS:
------------------------------------------------------------------------
r1875 | gonthier | 2010-03-17 12:22:08 +0100 (Wed, 17 Mar 2010) | 4 lines
off-by-1 bug that delayed short-circuit occurrence selection:
move: {1}(f x)
actually looked for two instances of f x, selecting only the first one,
insetad of interrupting the search after the first one
------------------------------------------------------------------------
The attached patch fixes the issue. Also note that it's preserving the
semantics of commands, just making them more efficient.
-- System Information:
Debian Release: squeeze/sid
APT prefers unstable
APT policy: (500, 'unstable'), (500, 'testing'), (1, 'experimental')
Architecture: amd64 (x86_64)
Kernel: Linux 2.6.34-1-amd64 (SMP w/2 CPU cores)
Index: ssreflect-1.2+dfsg/src/ssreflect.ml
===================================================================
--- ssreflect-1.2+dfsg.orig/src/ssreflect.ml 2010-06-21 14:04:33.000000000 +0200
+++ ssreflect-1.2+dfsg/src/ssreflect.ml 2010-06-21 14:04:57.000000000 +0200
@@ -2685,9 +2685,10 @@
let subst_occ =
let occ_set = Array.make max_occ (not use_occ) in
let _ = List.iter (fun i -> occ_set.(i - 1) <- use_occ) occ_list in
+ let _ = if max_occ = 0 then skip_occ := use_occ in
fun () -> incr nocc;
- if !nocc <= max_occ then occ_set.(!nocc - 1) else
- begin skip_occ := use_occ; not use_occ end in
+ if !nocc = max_occ then skip_occ := use_occ;
+ if !nocc <= max_occ then occ_set.(!nocc - 1) else not use_occ in
let rec subst_loop h c' =
if !skip_occ then c' else
let f, a = splay_app ise c' in
Reply to: