fac49fc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some IBC compression

fac49fcEdwin Brady13 years ago

idris.cabal+1

compare with master

unifiedsplit

@@ -446,6 +446,7 @@ Library

446 , network

447 , xml

448 , deepseq

449+ , zlib

449 Extensions: MultiParamTypeClasses

450 Extensions: MultiParamTypeClasses

450 , FunctionalDependencies

451 , FunctionalDependencies

451 , FlexibleInstances

452 , FlexibleInstances

src/Idris/AbsSyntax.hs+13

@@ -234,6 +234,19 @@ addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }

234clearIBC :: Idris ()

235clearIBC = do i <- getIState; putIState $ i { ibc_write = [] }

236

237+resetNameIdx :: Idris ()

238+resetNameIdx = do i <- getIState

239+ put (i { idris_nameIdx = (0, emptyContext) })

240+

241+addNameIdx :: Name -> Idris Int

242+addNameIdx n = do i <- getIState

243+ let idxs = snd (idris_nameIdx i)

244+ case lookupCtxt n idxs of

245+ [x] -> return x

246+ _ -> do let i' = fst (idris_nameIdx i) + 1

247+ put (i { idris_nameIdx = (i', addDef n i' idxs) })

248+ return i'

249+

237getHdrs :: Codegen -> Idris [String]

250getHdrs :: Codegen -> Idris [String]

238getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

251getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

239

252

src/Idris/AbsSyntaxTree.hs+3−2

@@ -132,7 +132,8 @@ data IState = IState {

132 idris_colourRepl :: Bool,

133 idris_colourTheme :: ColourTheme,

134 idris_outh :: Handle,

135− idris_errorhandlers :: [Name]

135+ idris_errorhandlers :: [Name],

136+ idris_nameIdx :: (Int, Ctxt Int)

136 }

137 }

137

138

138data SizeChange = Smaller | Same | Bigger | Unknown

139data SizeChange = Smaller | Same | Bigger | Unknown

@@ -198,7 +199,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

198 emptyContext

199 emptyContext

199 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

200 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

200 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

201 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

201− True defaultTheme stdout []

202+ True defaultTheme stdout [] (0, emptyContext)

202

203

203-- | The monad for the main REPL - reading and processing files and updating

204-- | The monad for the main REPL - reading and processing files and updating

204-- global state (hence the IO inner monad).

205-- global state (hence the IO inner monad).

src/Idris/Core/TT.hs+1

@@ -245,6 +245,7 @@ data Name = UN String -- ^ User-provided name

245 | MN Int String -- ^ Machine chosen names

246 | NErased -- ^ Name of somethng which is never used in scope

247 | SN SpecialName -- ^ Decorated function names

248+ | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)

248 deriving (Eq, Ord)

249 deriving (Eq, Ord)

249

250

250{-!

251{-!

src/Idris/IBC.hs+117−22

@@ -13,21 +13,24 @@ import Idris.Delaborate

13import Data.Binary

14import Data.Vector.Binary

15import Data.List

16−import Data.ByteString.Lazy as B hiding (length, elem)

16+import Data.ByteString.Lazy as B hiding (length, elem, map)

17import Control.Monad

18import Control.Monad.State hiding (get, put)

19+import qualified Control.Monad.State as ST

19import System.FilePath

20import System.FilePath

20import System.Directory

21import System.Directory

22+import Codec.Compression.Zlib

22import Debug.Trace

24import Debug.Trace

24import Paths_idris

26import Paths_idris

26ibcVersion :: Word8

28ibcVersion :: Word8

27−ibcVersion = 52

29+ibcVersion = 53

29data IBCFile = IBCFile { ver :: Word8,

31data IBCFile = IBCFile { ver :: Word8,

30 sourcefile :: FilePath,

32 sourcefile :: FilePath,

33+ symbols :: [Name],

31 ibc_imports :: [FilePath],

34 ibc_imports :: [FilePath],

32 ibc_implicits :: [(Name, [PArg])],

35 ibc_implicits :: [(Name, [PArg])],

33 ibc_fixes :: [FixDecl],

36 ibc_fixes :: [FixDecl],

@@ -62,13 +65,17 @@ deriving instance Binary IBCFile

62!-}

65!-}

64initIBC :: IBCFile

67initIBC :: IBCFile

65−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

68+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

67loadIBC :: FilePath -> Idris ()

70loadIBC :: FilePath -> Idris ()

68loadIBC fp = do iLOG $ "Loading ibc " ++ fp

71loadIBC fp = do iLOG $ "Loading ibc " ++ fp

69− ibcf <- runIO $ (decodeFile fp :: IO IBCFile)

72+ ibcf <- runIO $ (bdecode fp :: IO IBCFile)

70 process ibcf fp

73 process ibcf fp

75+bencode f d = B.writeFile f (compress (encode d))

76+bdecode f = do d' <- B.readFile f

77+ return (decode (decompress d'))

78+

72writeIBC :: FilePath -> FilePath -> Idris ()

79writeIBC :: FilePath -> FilePath -> Idris ()

73writeIBC src f

80writeIBC src f

74 = do iLOG $ "Writing ibc " ++ show f

81 = do iLOG $ "Writing ibc " ++ show f

@@ -76,9 +83,10 @@ writeIBC src f

76 case (Data.List.map fst (idris_metavars i)) \\ primDefs of

83 case (Data.List.map fst (idris_metavars i)) \\ primDefs of

77 (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

84 (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

78 [] -> return ()

85 [] -> return ()

86+ resetNameIdx

79 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

87 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

80 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

88 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

81− runIO $ encodeFile f ibcf

89+ runIO $ bencode f ibcf

82 iLOG "Written")

90 iLOG "Written")

83 (\c -> do iLOG $ "Failed " ++ pshow i c)

91 (\c -> do iLOG $ "Failed " ++ pshow i c)

84 return ()

92 return ()

@@ -125,8 +133,64 @@ ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }

125ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

133ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

126ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

134ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

127ibc i (IBCDef n) f = case lookupDef n (tt_ctxt i) of

135ibc i (IBCDef n) f = case lookupDef n (tt_ctxt i) of

136+ [v] -> do (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))

128− [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

137+ return f' { ibc_defs = (n,v) : ibc_defs f' }

129 _ -> ifail "IBC write failed"

138 _ -> ifail "IBC write failed"

139+ where

140+ updateDef :: Def -> StateT (IBCFile, Int) Idris Def

141+ updateDef (CaseOp c t args o s cd)

142+ = do o' <- mapM updateOrig o

143+ cd' <- updateCD cd

144+ return (CaseOp c t args o' s cd')

145+ updateDef t = return t

146+

147+ updateOrig (Left t) = do t' <- update t

148+ return (Left t')

149+ updateOrig (Right (l,r)) = do l' <- update l

150+ r' <- update r

151+ return (Right (l', r'))

152+

153+ updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

154+ = do c' <- updateSC c; r' <- updateSC r

155+ return (CaseDefs (ts, t) (cs, c') (is, i) (rs, r'))

156+

157+ updateSC (Case n alts) = do alts' <- mapM updateAlt alts

158+ return (Case n alts')

159+ updateSC (ProjCase t alts) = do t' <- update t

160+ alts' <- mapM updateAlt alts

161+ return (ProjCase t' alts')

162+ updateSC (STerm t) = do t' <- update t

163+ return (STerm t')

164+ updateSC t = return t

165+

166+ updateAlt (ConCase n i a sc) = do sc' <- updateSC sc

167+ return (ConCase n i a sc')

168+ updateAlt (FnCase n a sc) = do sc' <- updateSC sc

169+ return (FnCase n a sc')

170+ updateAlt (ConstCase i sc) = do sc' <- updateSC sc

171+ return (ConstCase i sc')

172+ updateAlt (SucCase n sc) = do sc' <- updateSC sc

173+ return (SucCase n sc')

174+ updateAlt (DefaultCase sc) = do sc' <- updateSC sc

175+ return (DefaultCase sc')

176+

177+ update (P t n@(MN _ _) ty) = return (P t n ty)

178+ update (P t n@(UN _) ty) = return (P t n ty)

179+ update (P t n ty) = do (f, len) <- ST.get

180+ i <- lift (addNameIdx n)

181+ when (i >= len) $

182+ ST.put (f { symbols = symbols f ++ [n] }, len+1)

183+ return (P t (SymRef i) ty)

184+ update (App f a) = do f' <- update f; a' <- update a

185+ return (App f' a')

186+ update (Bind n b sc) = do b' <- fmapMB update b

187+ sc' <- update sc

188+ return (Bind n b' sc')

189+ update (Proj t i) = do t' <- update t

190+ return (Proj t' i)

191+ update t = return t

192+

193+

130ibc i (IBCDoc n) f = case lookupCtxt n (idris_docstrings i) of

194ibc i (IBCDoc n) f = case lookupCtxt n (idris_docstrings i) of

131 [v] -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }

195 [v] -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }

132 _ -> ifail "IBC write failed"

196 _ -> ifail "IBC write failed"

@@ -170,7 +234,7 @@ process i fn

170 pCGFlags (ibc_cgflags i)

234 pCGFlags (ibc_cgflags i)

171 pDyLibs (ibc_dynamic_libs i)

235 pDyLibs (ibc_dynamic_libs i)

172 pHdrs (ibc_hdrs i)

236 pHdrs (ibc_hdrs i)

173− pDefs (ibc_defs i)

237+ pDefs (symbols i) (ibc_defs i)

174 pAccess (ibc_access i)

238 pAccess (ibc_access i)

175 pTotal (ibc_total i)

239 pTotal (ibc_total i)

176 pCG (ibc_cg i)

240 pCG (ibc_cg i)

@@ -292,12 +356,32 @@ pDyLibs ls = do res <- mapM (addDyLib . return) ls

292pHdrs :: [(Codegen, String)] -> Idris ()

356pHdrs :: [(Codegen, String)] -> Idris ()

293pHdrs hs = mapM_ (uncurry addHdr) hs

357pHdrs hs = mapM_ (uncurry addHdr) hs

294

358

295−pDefs :: [(Name, Def)] -> Idris ()

359+pDefs :: [Name] -> [(Name, Def)] -> Idris ()

360+pDefs syms ds

296−pDefs ds = mapM_ (\ (n, d) ->

361+ = mapM_ (\ (n, d) ->

297− do i <- getIState

362+ do i <- getIState

363+ let d' = updateDef d

298− logLvl 5 $ "Added " ++ show (n, d)

364+ logLvl 5 $ "Added " ++ show (n, d')

299− putIState (i { tt_ctxt = addCtxtDef n d (tt_ctxt i) }))

365+ putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds

300− ds

366+ where

367+ updateDef (CaseOp c t args o s cd)

368+ = CaseOp c t args (map updateOrig o) s (updateCD cd)

369+ updateDef t = t

370+

371+ updateOrig (Left t) = Left (update t)

372+ updateOrig (Right (l, r)) = Right (update l, update r)

373+

374+ updateCD (CaseDefs (ts, t) (cs, c) (is, i) (rs, r))

375+ = CaseDefs (ts, fmap update t)

376+ (cs, fmap update c)

377+ (is, fmap update i)

378+ (rs, fmap update r)

379+

380+ update (P t (SymRef i) ty) = P t (syms!!i) ty

381+ update (App f a) = App (update f) (update a)

382+ update (Bind n b sc) = Bind n (fmap update b) (update sc)

383+ update (Proj t i) = Proj (update t) i

384+ update t = t

301

385

302pDocs :: [(Name, String)] -> Idris ()

386pDocs :: [(Name, String)] -> Idris ()

303pDocs ds = mapM_ (\ (n, a) -> addDocStr n a) ds

387pDocs ds = mapM_ (\ (n, a) -> addDocStr n a) ds

@@ -394,6 +478,8 @@ instance Binary Name where

394 NErased -> putWord8 3

478 NErased -> putWord8 3

395 SN x1 -> do putWord8 4

479 SN x1 -> do putWord8 4

396 put x1

480 put x1

481+ SymRef x1 -> do putWord8 5

482+ put x1

397 get

483 get

398 = do i <- getWord8

484 = do i <- getWord8

399 case i of

485 case i of

@@ -408,6 +494,8 @@ instance Binary Name where

408 3 -> return NErased

494 3 -> return NErased

409 4 -> do x1 <- get

495 4 -> do x1 <- get

410 return (SN x1)

496 return (SN x1)

497+ 5 -> do x1 <- get

498+ return (SymRef x1)

411 _ -> error "Corrupted binary data for Name"

499 _ -> error "Corrupted binary data for Name"

412

500

413instance Binary SpecialName where

501instance Binary SpecialName where

@@ -647,8 +735,11 @@ instance {- (Binary n) => -} Binary (TT Name) where

647 put x1

735 put x1

648 put x2

736 put x2

649-- put x3

737-- put x3

738+ V x1 -> if (x1 >= 0 && x1 < 256)

650− V x1 -> do putWord8 1

739+ then do putWord8 1

740+ putWord8 (toEnum (x1 + 1))

741+ else do putWord8 9

651− put x1

742+ put x1

652 Bind x1 x2 x3 -> do putWord8 2

743 Bind x1 x2 x3 -> do putWord8 2

653 put x1

744 put x1

654 put x2

745 put x2

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

660 put x1

751 put x1

661 Proj x1 x2 -> do putWord8 5

752 Proj x1 x2 -> do putWord8 5

662 put x1

753 put x1

663− put x2

754+ putWord8 (toEnum (x2 + 1))

664 Erased -> putWord8 6

755 Erased -> putWord8 6

665 TType x1 -> do putWord8 7

756 TType x1 -> do putWord8 7

666 put x1

757 put x1

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

672 x2 <- get

763 x2 <- get

673-- x3 <- get

764-- x3 <- get

674 return (P x1 x2 Erased)

765 return (P x1 x2 Erased)

675− 1 -> do x1 <- get

766+ 1 -> do x1 <- getWord8

676− return (V x1)

767+ return (V ((fromEnum x1) - 1))

677 2 -> do x1 <- get

768 2 -> do x1 <- get

678 x2 <- get

769 x2 <- get

679 x3 <- get

770 x3 <- get

@@ -684,12 +775,14 @@ instance {- (Binary n) => -} Binary (TT Name) where

684 4 -> do x1 <- get

775 4 -> do x1 <- get

685 return (Constant x1)

776 return (Constant x1)

686 5 -> do x1 <- get

777 5 -> do x1 <- get

687− x2 <- get

778+ x2 <- getWord8

688− return (Proj x1 x2)

779+ return (Proj x1 ((fromEnum x2)-1))

689 6 -> return Erased

780 6 -> return Erased

690 7 -> do x1 <- get

781 7 -> do x1 <- get

691 return (TType x1)

782 return (TType x1)

692 8 -> return Impossible

783 8 -> return Impossible

784+ 9 -> do x1 <- get

785+ return (V x1)

693 _ -> error "Corrupted binary data for TT"

786 _ -> error "Corrupted binary data for TT"

694

787

695instance Binary SC where

788instance Binary SC where

@@ -908,7 +1001,7 @@ instance Binary MetaInformation where

908 return (DataMI x1)

1001 return (DataMI x1)

909

1002

910instance Binary IBCFile where

1003instance Binary IBCFile where

911− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29)

1004+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30)

912 = {-# SCC "putIBCFile" #-}

1005 = {-# SCC "putIBCFile" #-}

913 do put x1

1006 do put x1

914 put x2

1007 put x2

@@ -939,6 +1032,7 @@ instance Binary IBCFile where

939 put x27

1032 put x27

940 put x28

1033 put x28

941 put x29

1034 put x29

1035+ put x30

942 get

1036 get

943 = do x1 <- get

1037 = do x1 <- get

944 if x1 == ibcVersion then

1038 if x1 == ibcVersion then

@@ -970,7 +1064,8 @@ instance Binary IBCFile where

970 x27 <- get

1064 x27 <- get

971 x28 <- get

1065 x28 <- get

972 x29 <- get

1066 x29 <- get

1067+ x30 <- get

973− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29)

1068+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30)

974 else return (initIBC { ver = x1 })

1069 else return (initIBC { ver = x1 })

975

1070

976instance Binary DataOpt where

1071instance Binary DataOpt where