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

git.iko.soy/Idris-dev

on master help sign in

Fix term size calculation for inlining

45272d9Edwin Brady13 years ago

src/Core/CaseTree.hs+1

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

65instance TermSize SC where

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

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

67 termsize n (STerm t) = termsize n t

68 termsize n (STerm t) = termsize n t

68 termsize n _ = 1

69 termsize n _ = 1

src/Core/TT.hs+4

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

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

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

488 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

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

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

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

490 termsize n _ = 1

494 termsize n _ = 1

491

495

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

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