45272d9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix term size calculation for inlining

Now counting binders other than Let, so lots of things previously inlined over-aggressively are now not inlined.

commit45272d90ae003f369ddb4e0bbd589c07b45c76a9 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 2 Jul 2013, 10:53 (13 years ago) parent4bebb72

2 files changed+5

unifiedsplit

src/Core/CaseTree.hs+1

@@ -64,6 +64,7 @@ type CS = ([Term], Int)

6464

6565instance TermSize SC where

6666 termsize n (Case n' as) = termsize n as

67+ termsize n (ProjCase n' as) = termsize n as

6768 termsize n (STerm t) = termsize n t

6869 termsize n _ = 1

6970

src/Core/TT.hs+4

@@ -486,7 +486,11 @@ instance TermSize (TT Name) where

486486 termsize n (Bind n' (Let t v) sc)

487487 = let rn = if n == n' then MN 0 "noname" else n in

488488 termsize rn v + termsize rn sc

489+ termsize n (Bind n' b sc)

490+ = let rn = if n == n' then MN 0 "noname" else n in

491+ termsize rn sc

489492 termsize n (App f a) = termsize n f + termsize n a

493+ termsize n (Proj t i) = termsize n t

490494 termsize n _ = 1

491495

492496instance Sized a => Sized (TT a) where