@@ -11,6 +11,7 @@ import Idris.Imports
1111import Idris.Error
1212
1313import Data.Binary
14+import Data.Vector.Binary
1415import Data.List
1516import Data.ByteString.Lazy as B hiding (length, elem)
1617import Control.Monad
@@ -395,6 +396,11 @@ instance Binary Const where
395396 putWord8 20
396397 putWord8 (fromIntegral . fromEnum $ ity)
397398 putWord8 (fromIntegral count)
399+
400+ B8V x1 -> putWord8 21 >> put x1
401+ B16V x1 -> putWord8 22 >> put x1
402+ B32V x1 -> putWord8 23 >> put x1
403+ B64V x1 -> putWord8 24 >> put x1
398404 get
399405 = do i <- getWord8
400406 case i of
@@ -431,6 +437,11 @@ instance Binary Const where
431437 c <- getWord8
432438 return (AType (ATInt (ITVec (toEnum . fromIntegral $ e) (fromIntegral c))))
433439
440+ 21 -> fmap B8V get
441+ 22 -> fmap B16V get
442+ 23 -> fmap B32V get
443+ 24 -> fmap B64V get
444+
434445 _ -> error "Corrupted binary data for Const"
435446
436447