@@ -13,21 +13,24 @@ import Idris.Delaborate
1313import Data.Binary
1414import Data.Vector.Binary
1515import Data.List
16−import Data.ByteString.Lazy as B hiding (length, elem)
16+import Data.ByteString.Lazy as B hiding (length, elem, map)
1717import Control.Monad
1818import Control.Monad.State hiding (get, put)
19+import qualified Control.Monad.State as ST
1920import System.FilePath
2021import System.Directory
22+import Codec.Compression.Zlib
2123
2224import Debug.Trace
2325
2426import Paths_idris
2527
2628ibcVersion :: Word8
27−ibcVersion = 52
29+ibcVersion = 53
2830
2931data IBCFile = IBCFile { ver :: Word8,
3032 sourcefile :: FilePath,
33+ symbols :: [Name],
3134 ibc_imports :: [FilePath],
3235 ibc_implicits :: [(Name, [PArg])],
3336 ibc_fixes :: [FixDecl],
@@ -62,13 +65,17 @@ deriving instance Binary IBCFile
6265!-}
6366
6467initIBC :: IBCFile
65−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
68+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
6669
6770loadIBC :: FilePath -> Idris ()
6871loadIBC fp = do iLOG $ "Loading ibc " ++ fp
69− ibcf <- runIO $ (decodeFile fp :: IO IBCFile)
72+ ibcf <- runIO $ (bdecode fp :: IO IBCFile)
7073 process ibcf fp
7174
75+bencode f d = B.writeFile f (compress (encode d))
76+bdecode f = do d' <- B.readFile f
77+ return (decode (decompress d'))
78+
7279writeIBC :: FilePath -> FilePath -> Idris ()
7380writeIBC src f
7481 = do iLOG $ "Writing ibc " ++ show f
@@ -76,9 +83,10 @@ writeIBC src f
7683 case (Data.List.map fst (idris_metavars i)) \\ primDefs of
7784 (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"
7885 [] -> return ()
86+ resetNameIdx
7987 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })
8088 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)
81− runIO $ encodeFile f ibcf
89+ runIO $ bencode f ibcf
8290 iLOG "Written")
8391 (\c -> do iLOG $ "Failed " ++ pshow i c)
8492 return ()
@@ -125,8 +133,64 @@ ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }
125133ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }
126134ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }
127135ibc i (IBCDef n) f = case lookupDef n (tt_ctxt i) of
128− [v] -> return f { ibc_defs = (n,v) : ibc_defs f }
136+ [v] -> do (v', (f', _)) <- runStateT (updateDef v) (f, length (symbols f))
137+ return f' { ibc_defs = (n,v) : ibc_defs f' }
129138 _ -> 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+
130194ibc i (IBCDoc n) f = case lookupCtxt n (idris_docstrings i) of
131195 [v] -> return f { ibc_docstrings = (n,v) : ibc_docstrings f }
132196 _ -> ifail "IBC write failed"
@@ -170,7 +234,7 @@ process i fn
170234 pCGFlags (ibc_cgflags i)
171235 pDyLibs (ibc_dynamic_libs i)
172236 pHdrs (ibc_hdrs i)
173− pDefs (ibc_defs i)
237+ pDefs (symbols i) (ibc_defs i)
174238 pAccess (ibc_access i)
175239 pTotal (ibc_total i)
176240 pCG (ibc_cg i)
@@ -292,12 +356,32 @@ pDyLibs ls = do res <- mapM (addDyLib . return) ls
292356pHdrs :: [(Codegen, String)] -> Idris ()
293357pHdrs hs = mapM_ (uncurry addHdr) hs
294358
295−pDefs :: [(Name, Def)] -> Idris ()
296−pDefs ds = mapM_ (\ (n, d) ->
297− do i <- getIState
298− logLvl 5 $ "Added " ++ show (n, d)
299− putIState (i { tt_ctxt = addCtxtDef n d (tt_ctxt i) }))
300− ds
359+pDefs :: [Name] -> [(Name, Def)] -> Idris ()
360+pDefs syms ds
361+ = mapM_ (\ (n, d) ->
362+ do i <- getIState
363+ let d' = updateDef d
364+ logLvl 5 $ "Added " ++ show (n, d')
365+ putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) 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
301385
302386pDocs :: [(Name, String)] -> Idris ()
303387pDocs ds = mapM_ (\ (n, a) -> addDocStr n a) ds
@@ -394,6 +478,8 @@ instance Binary Name where
394478 NErased -> putWord8 3
395479 SN x1 -> do putWord8 4
396480 put x1
481+ SymRef x1 -> do putWord8 5
482+ put x1
397483 get
398484 = do i <- getWord8
399485 case i of
@@ -408,6 +494,8 @@ instance Binary Name where
408494 3 -> return NErased
409495 4 -> do x1 <- get
410496 return (SN x1)
497+ 5 -> do x1 <- get
498+ return (SymRef x1)
411499 _ -> error "Corrupted binary data for Name"
412500
413501instance Binary SpecialName where
@@ -647,8 +735,11 @@ instance {- (Binary n) => -} Binary (TT Name) where
647735 put x1
648736 put x2
649737-- put x3
650− V x1 -> do putWord8 1
651− put x1
738+ V x1 -> if (x1 >= 0 && x1 < 256)
739+ then do putWord8 1
740+ putWord8 (toEnum (x1 + 1))
741+ else do putWord8 9
742+ put x1
652743 Bind x1 x2 x3 -> do putWord8 2
653744 put x1
654745 put x2
@@ -660,7 +751,7 @@ instance {- (Binary n) => -} Binary (TT Name) where
660751 put x1
661752 Proj x1 x2 -> do putWord8 5
662753 put x1
663− put x2
754+ putWord8 (toEnum (x2 + 1))
664755 Erased -> putWord8 6
665756 TType x1 -> do putWord8 7
666757 put x1
@@ -672,8 +763,8 @@ instance {- (Binary n) => -} Binary (TT Name) where
672763 x2 <- get
673764-- x3 <- get
674765 return (P x1 x2 Erased)
675− 1 -> do x1 <- get
676− return (V x1)
766+ 1 -> do x1 <- getWord8
767+ return (V ((fromEnum x1) - 1))
677768 2 -> do x1 <- get
678769 x2 <- get
679770 x3 <- get
@@ -684,12 +775,14 @@ instance {- (Binary n) => -} Binary (TT Name) where
684775 4 -> do x1 <- get
685776 return (Constant x1)
686777 5 -> do x1 <- get
687− x2 <- get
688− return (Proj x1 x2)
778+ x2 <- getWord8
779+ return (Proj x1 ((fromEnum x2)-1))
689780 6 -> return Erased
690781 7 -> do x1 <- get
691782 return (TType x1)
692783 8 -> return Impossible
784+ 9 -> do x1 <- get
785+ return (V x1)
693786 _ -> error "Corrupted binary data for TT"
694787
695788instance Binary SC where
@@ -908,7 +1001,7 @@ instance Binary MetaInformation where
9081001 return (DataMI x1)
9091002
9101003instance 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)
9121005 = {-# SCC "putIBCFile" #-}
9131006 do put x1
9141007 put x2
@@ -939,6 +1032,7 @@ instance Binary IBCFile where
9391032 put x27
9401033 put x28
9411034 put x29
1035+ put x30
9421036 get
9431037 = do x1 <- get
9441038 if x1 == ibcVersion then
@@ -970,7 +1064,8 @@ instance Binary IBCFile where
9701064 x27 <- get
9711065 x28 <- get
9721066 x29 <- 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)
1067+ x30 <- get
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)
9741069 else return (initIBC { ver = x1 })
9751070
9761071instance Binary DataOpt where