module Idris.Core.Binary where
import Data.Binary
import Data.Vector.Binary
import qualified Data.Text as T
import Idris.Core.TT
instance Binary FC where
put (FC x1 (x2, x3) (x4, x5))
= do put x1
put (x2 * 65536 + x3)
put (x4 * 65536 + x5)
get
= do x1 <- get
x2x3 <- get
x4x5 <- get
return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))
instance Binary Name where
put x
= case x of
UN x1 -> do putWord8 0
put x1
NS x1 x2 -> do putWord8 1
put x1
put x2
MN x1 x2 -> do putWord8 2
put x1
put x2
NErased -> putWord8 3
SN x1 -> do putWord8 4
put x1
SymRef x1 -> do putWord8 5
put x1
get
= do i <- getWord8
case i of
0 -> do x1 <- get
return (UN x1)
1 -> do x1 <- get
x2 <- get
return (NS x1 x2)
2 -> do x1 <- get
x2 <- get
return (MN x1 x2)
3 -> return NErased
4 -> do x1 <- get
return (SN x1)
5 -> do x1 <- get
return (SymRef x1)
_ -> error "Corrupted binary data for Name"
instance Binary T.Text where
put x = put (str x)
get = do x <- get
return (txt x)
instance Binary SpecialName where
put x
= case x of
WhereN x1 x2 x3 -> do putWord8 0
put x1
put x2
put x3
InstanceN x1 x2 -> do putWord8 1
put x1
put x2
ParentN x1 x2 -> do putWord8 2
put x1
put x2
MethodN x1 -> do putWord8 3
put x1
CaseN x1 -> do putWord8 4; put x1
ElimN x1 -> do putWord8 5; put x1
InstanceCtorN x1 -> do putWord8 6; put x1
WithN x1 x2 -> do putWord8 7
put x1
put x2
get
= do i <- getWord8
case i of
0 -> do x1 <- get
x2 <- get
x3 <- get
return (WhereN x1 x2 x3)
1 -> do x1 <- get
x2 <- get
return (InstanceN x1 x2)
2 -> do x1 <- get
x2 <- get
return (ParentN x1 x2)
3 -> do x1 <- get
return (MethodN x1)
4 -> do x1 <- get
return (CaseN x1)
5 -> do x1 <- get
return (ElimN x1)
6 -> do x1 <- get
return (InstanceCtorN x1)
7 -> do x1 <- get
x2 <- get
return (WithN x1 x2)
_ -> error "Corrupted binary data for SpecialName"
instance Binary Const where
put x
= case x of
I x1 -> do putWord8 0
put x1
BI x1 -> do putWord8 1
put x1
Fl x1 -> do putWord8 2
put x1
Ch x1 -> do putWord8 3
put x1
Str x1 -> do putWord8 4
put x1
B8 x1 -> putWord8 5 >> put x1
B16 x1 -> putWord8 6 >> put x1
B32 x1 -> putWord8 7 >> put x1
B64 x1 -> putWord8 8 >> put x1
(AType (ATInt ITNative)) -> putWord8 9
(AType (ATInt ITBig)) -> putWord8 10
(AType ATFloat) -> putWord8 11
(AType (ATInt ITChar)) -> putWord8 12
StrType -> putWord8 13
PtrType -> putWord8 14
Forgot -> putWord8 15
(AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity))
(AType (ATInt (ITVec ity count))) -> do
putWord8 20
putWord8 (fromIntegral . fromEnum $ ity)
putWord8 (fromIntegral count)
B8V x1 -> putWord8 21 >> put x1
B16V x1 -> putWord8 22 >> put x1
B32V x1 -> putWord8 23 >> put x1
B64V x1 -> putWord8 24 >> put x1
BufferType -> putWord8 25
ManagedPtrType -> putWord8 26
get
= do i <- getWord8
case i of
0 -> do x1 <- get
return (I x1)
1 -> do x1 <- get
return (BI x1)
2 -> do x1 <- get
return (Fl x1)
3 -> do x1 <- get
return (Ch x1)
4 -> do x1 <- get
return (Str x1)
5 -> fmap B8 get
6 -> fmap B16 get
7 -> fmap B32 get
8 -> fmap B64 get
9 -> return (AType (ATInt ITNative))
10 -> return (AType (ATInt ITBig))
11 -> return (AType ATFloat)
12 -> return (AType (ATInt ITChar))
13 -> return StrType
14 -> return PtrType
15 -> return Forgot
16 -> return (AType (ATInt (ITFixed IT8)))
17 -> return (AType (ATInt (ITFixed IT16)))
18 -> return (AType (ATInt (ITFixed IT32)))
19 -> return (AType (ATInt (ITFixed IT64)))
20 -> do
e <- getWord8
c <- getWord8
return (AType (ATInt (ITVec (toEnum . fromIntegral $ e) (fromIntegral c))))
21 -> fmap B8V get
22 -> fmap B16V get
23 -> fmap B32V get
24 -> fmap B64V get
25 -> return BufferType
26 -> return ManagedPtrType
_ -> error "Corrupted binary data for Const"
instance Binary Raw where
put x
= case x of
Var x1 -> do putWord8 0
put x1
RBind x1 x2 x3 -> do putWord8 1
put x1
put x2
put x3
RApp x1 x2 -> do putWord8 2
put x1
put x2
RType -> putWord8 3
RConstant x1 -> do putWord8 4
put x1
RForce x1 -> do putWord8 5
put x1
get
= do i <- getWord8
case i of
0 -> do x1 <- get
return (Var x1)
1 -> do x1 <- get
x2 <- get
x3 <- get
return (RBind x1 x2 x3)
2 -> do x1 <- get
x2 <- get
return (RApp x1 x2)
3 -> return RType
4 -> do x1 <- get
return (RConstant x1)
5 -> do x1 <- get
return (RForce x1)
_ -> error "Corrupted binary data for Raw"
instance (Binary b) => Binary (Binder b) where
put x
= case x of
Lam x1 -> do putWord8 0
put x1
Pi x1 x2 -> do putWord8 1
put x1
put x2
Let x1 x2 -> do putWord8 2
put x1
put x2
NLet x1 x2 -> do putWord8 3
put x1
put x2
Hole x1 -> do putWord8 4
put x1
GHole x1 x2 -> do putWord8 5
put x1
put x2
Guess x1 x2 -> do putWord8 6
put x1
put x2
PVar x1 -> do putWord8 7
put x1
PVTy x1 -> do putWord8 8
put x1
get
= do i <- getWord8
case i of
0 -> do x1 <- get
return (Lam x1)
1 -> do x1 <- get
x2 <- get
return (Pi x1 x2)
2 -> do x1 <- get
x2 <- get
return (Let x1 x2)
3 -> do x1 <- get
x2 <- get
return (NLet x1 x2)
4 -> do x1 <- get
return (Hole x1)
5 -> do x1 <- get
x2 <- get
return (GHole x1 x2)
6 -> do x1 <- get
x2 <- get
return (Guess x1 x2)
7 -> do x1 <- get
return (PVar x1)
8 -> do x1 <- get
return (PVTy x1)
_ -> error "Corrupted binary data for Binder"
instance Binary Universe where
put x = case x of
UniqueType -> putWord8 0
AllTypes -> putWord8 1
NullType -> putWord8 2
get = do i <- getWord8
case i of
0 -> return UniqueType
1 -> return AllTypes
2 -> return NullType
_ -> error "Corrupted binary data for Universe"
instance Binary NameType where
put x
= case x of
Bound -> putWord8 0
Ref -> putWord8 1
DCon x1 x2 x3 -> do putWord8 2
put (x1 * 65536 + x2)
put x3
TCon x1 x2 -> do putWord8 3
put (x1 * 65536 + x2)
get
= do i <- getWord8
case i of
0 -> return Bound
1 -> return Ref
2 -> do x1x2 <- get
x3 <- get
return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536) x3)
3 -> do x1x2 <- get
return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))
_ -> error "Corrupted binary data for NameType"
instance Binary (TT Name) where
put x
=
case x of
P x1 x2 x3 -> do putWord8 0
put x1
put x2
V x1 -> if (x1 >= 0 && x1 < 256)
then do putWord8 1
putWord8 (toEnum (x1 + 1))
else do putWord8 9
put x1
Bind x1 x2 x3 -> do putWord8 2
put x1
put x2
put x3
App x1 x2 -> do putWord8 3
put x1
put x2
Constant x1 -> do putWord8 4
put x1
Proj x1 x2 -> do putWord8 5
put x1
putWord8 (toEnum (x2 + 1))
Erased -> putWord8 6
TType x1 -> do putWord8 7
put x1
Impossible -> putWord8 8
UType x1 -> do putWord8 10
put x1
get
= do i <- getWord8
case i of
0 -> do x1 <- get
x2 <- get
return (P x1 x2 Erased)
1 -> do x1 <- getWord8
return (V ((fromEnum x1) 1))
2 -> do x1 <- get
x2 <- get
x3 <- get
return (Bind x1 x2 x3)
3 -> do x1 <- get
x2 <- get
return (App x1 x2)
4 -> do x1 <- get
return (Constant x1)
5 -> do x1 <- get
x2 <- getWord8
return (Proj x1 ((fromEnum x2)1))
6 -> return Erased
7 -> do x1 <- get
return (TType x1)
8 -> return Impossible
9 -> do x1 <- get
return (V x1)
10 -> do x1 <- get
return (UType x1)
_ -> error "Corrupted binary data for TT"