git.iko.soy/Idris-dev
on master help sign in
Fix boolElim optimisation

It made assumptions about the form of Delay which have changed with the new erasure, so wasn't being applied any more (it is a modest, but noticeable, performance gain).

commit92d7b511a29ca478e70b1e981400c23a8fe2b074 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 4 May 2014, 22:28 (12 years ago) parent8d02588
1 file changed+2−2
compare with master
unifiedsplit
src/IRTS/Compiler.hs+2−2
src/IRTS/Compiler.hs+2−2
@@ -249,8 +249,8 @@ irTerm vs env tm@(App f a) = case unApply tm of
249249
250250 -- This case is here until we get more general inlining. It's just
251251 -- a really common case, and the laziness hurts...
252− (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
253− (App (P _ (UN d') _) e)])
252+ (P _ (NS (UN be) [b,p]) _, [_,x,(App (App (App (P _ (UN d) _) _) _) t),
253+ (App (App (App (P _ (UN d') _) _) _) e)])
254254 | be == txt "boolElim"
255255 , d == txt "Delay"
256256 , d' == txt "Delay"