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

git.iko.soy/Idris-dev

on master help sign in

Shrink IBCs dramatically

5d8f805Edwin Brady13 years ago

src/Idris/DataOpts.hs+8−2

compare with master

unifiedsplit

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

196

197 stripCollapsed t = return t

198

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

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

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

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

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

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

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

202 return (b { binderTy = t' })

208 return (b { binderTy = t' })

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

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

src/Idris/IBC.hs+8−11

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

23import Paths_idris

25ibcVersion :: Word8

26−ibcVersion = 50

26+ibcVersion = 51

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

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

357 put (CGInfo x1 x2 x3 x4 x5)

358 = do put x1

359 put x2

360− put x3

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

361 put x4

362 put x5

363 get

364 = do x1 <- get

365 x2 <- get

366− x3 <- get

367 x4 <- get

366 x4 <- get

368 x5 <- get

367 x5 <- get

369− return (CGInfo x1 x2 x3 x4 x5)

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

370

369

371instance Binary FC where

370instance Binary FC where

372 put (FC x1 x2 x3)

371 put (FC x1 x2 x3)

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

650 P x1 x2 x3 -> do putWord8 0

649 P x1 x2 x3 -> do putWord8 0

651 put x1

650 put x1

652 put x2

651 put x2

653− put x3

652+-- put x3

654 V x1 -> do putWord8 1

653 V x1 -> do putWord8 1

655 put x1

654 put x1

656 Bind x1 x2 x3 -> do putWord8 2

655 Bind x1 x2 x3 -> do putWord8 2

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

674 case i of

673 case i of

675 0 -> do x1 <- get

674 0 -> do x1 <- get

676 x2 <- get

675 x2 <- get

677− x3 <- get

676+-- x3 <- get

678− return (P x1 x2 x3)

677+ return (P x1 x2 Erased)

679 1 -> do x1 <- get

678 1 -> do x1 <- get

680 return (V x1)

679 return (V x1)

681 2 -> do x1 <- get

680 2 -> do x1 <- get

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

772

771

773instance Binary CaseDefs where

772instance Binary CaseDefs where

774 put (CaseDefs x1 x2 x3 x4)

773 put (CaseDefs x1 x2 x3 x4)

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

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

776 put x2

775 put x2

777− put x3

778 put x4

776 put x4

779 get

777 get

780 = do x2 <- get

778 = do x2 <- get

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

782 x4 <- get

779 x4 <- get

783− return (CaseDefs x3 x2 x3 x4)

780+ return (CaseDefs x2 x2 x2 x4)

784

781

785instance Binary CaseInfo where

782instance Binary CaseInfo where

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

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