5d8f805 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Shrink IBCs dramatically

By erasing types, and inlined definitions which are only used for totality checking so really don't need storing.

commit5d8f8050d998caee8c909ecd6fe04f864f33fb9d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 16 Jan 2014, 00:27 (13 years ago) parent8b7f8ad

2 files changed+16−13

compare with master

unifiedsplit

src/Idris/DataOpts.hs+8−2 src/Idris/IBC.hs+8−11

src/Idris/DataOpts.hs+8−2

@@ -196,8 +196,14 @@ instance Optimisable Raw where

196196

197197 stripCollapsed t = return t

198198

199−instance Optimisable t => Optimisable (Binder t) where

200− applyOpts (Let t v) = Let <$> applyOpts t <*> applyOpts v

199+-- Erase types (makes ibc smaller, and we don't need them)

200+instance Optimisable (Binder (TT Name)) where

201+ applyOpts (Let t v) = Let <$> return Erased <*> applyOpts v

202+ applyOpts b = return (b { binderTy = Erased })

203+ stripCollapsed (Let t v) = Let <$> return Erased <*> stripCollapsed v

204+ stripCollapsed b = return (b { binderTy = Erased })

205+

206+instance Optimisable (Binder Raw) where

201207 applyOpts b = do t' <- applyOpts (binderTy b)

202208 return (b { binderTy = t' })

203209 stripCollapsed (Let t v) = Let <$> stripCollapsed t <*> stripCollapsed v

src/Idris/IBC.hs+8−11

@@ -23,7 +23,7 @@ import Debug.Trace

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 50

26+ibcVersion = 51

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

@@ -357,16 +357,15 @@ instance Binary CGInfo where

357357 put (CGInfo x1 x2 x3 x4 x5)

358358 = do put x1

359359 put x2

360− put x3

360+-- put x3 -- Already used SCG info for totality check

361361 put x4

362362 put x5

363363 get

364364 = do x1 <- get

365365 x2 <- get

366− x3 <- get

367366 x4 <- get

368367 x5 <- get

369− return (CGInfo x1 x2 x3 x4 x5)

368+ return (CGInfo x1 x2 [] x4 x5)

370369

371370instance Binary FC where

372371 put (FC x1 x2 x3)

@@ -650,7 +649,7 @@ instance {- (Binary n) => -} Binary (TT Name) where

650649 P x1 x2 x3 -> do putWord8 0

651650 put x1

652651 put x2

653− put x3

652+-- put x3

654653 V x1 -> do putWord8 1

655654 put x1

656655 Bind x1 x2 x3 -> do putWord8 2

@@ -674,8 +673,8 @@ instance {- (Binary n) => -} Binary (TT Name) where

674673 case i of

675674 0 -> do x1 <- get

676675 x2 <- get

677− x3 <- get

678− return (P x1 x2 x3)

676+-- x3 <- get

677+ return (P x1 x2 Erased)

679678 1 -> do x1 <- get

680679 return (V x1)

681680 2 -> do x1 <- get

@@ -772,15 +771,13 @@ instance Binary CaseAlt where

772771

773772instance Binary CaseDefs where

774773 put (CaseDefs x1 x2 x3 x4)

775− = do -- don't need totality checked version

774+ = do -- don't need totality checked or inlined versions

776775 put x2

777− put x3

778776 put x4

779777 get

780778 = do x2 <- get

781− x3 <- get -- use for totality checked version

782779 x4 <- get

783− return (CaseDefs x3 x2 x3 x4)

780+ return (CaseDefs x2 x2 x2 x4)

784781

785782instance Binary CaseInfo where

786783 put x@(CaseInfo x1 x2) = do put x1