> {-# OPTIONS_GHC -fglasgow-exts #-}

Binary instances for idris data structures, and saving and loading 
typechecked forms to disk.

> module Idris.Serialise where

> import Idris.AbsSyntax
> import Idris.ConTrans
> import Ivor.ViewTerm
> import Ivor.TT

> import Data.Binary
> import Data.Typeable
> import Control.Monad

> instance Binary ViewTerm where
>     put (Name t x) = do put (0 :: Word8)
>                         put t; put x
>     put (App f a) = do put (1 :: Word8)
>                        put f; put a
>     put (Lambda v ty sc) = do put (2 :: Word8)
>                               put v; put ty; put sc
>     put (Forall v ty sc) = do put (3 :: Word8)
>                               put v; put ty; put sc
>     put (Let n v ty sc) = do put (4 :: Word8)
>                              put n; put v; put ty; put sc
>     put Star = put (5 :: Word8)
>     put Placeholder = put (6 :: Word8)
>     put (Annotation a t) = do put (7 :: Word8)
>                               put a; put t
>     put (Metavar m) = do put (8 :: Word8)
>                          put m
>     put (Constant c) = case cast c :: Maybe String of
>                          Just v -> do put (9 :: Word8)
>                                       put v
>                          Nothing -> case cast c :: Maybe Int of
>                            Just v -> do put (10 :: Word8)
>                                         put v
>                            Nothing -> fail "Unknown constant type"

>     get = do tag <- getWord8
>              case tag of
>                0 -> liftM2 Name get get
>                1 -> liftM2 App get get
>                2 -> liftM3 Lambda get get get
>                3 -> liftM3 Forall get get get
>                4 -> liftM4 Let get get get get
>                5 -> return Star
>                6 -> return Placeholder
>                7 -> liftM2 Annotation get get
>                8 -> liftM Metavar get
>                9 -> do s <- get
>                        return (Constant (s :: String))
>                10 -> do i <- get
>                         return (Constant (i :: Int))


> instance Binary RBinder where
>     put (Pi p l r) = do put (0 :: Word8)
>                         put p; put l; put r
>     put (Lam t) = do put (1 :: Word8); put t
>     put (RLet t ty) = do put (2 :: Word8); put t; put ty

>     get = do tag <- getWord8
>              case tag of
>                0 -> liftM3 Pi get get get
>                1 -> liftM Lam get
>                2 -> liftM2 RLet get get

> instance Binary Op where
>     put x = put (fromEnum x)
>     get = do t <- get
>              return (toEnum t)

> instance Binary Plicit where
>     put x = put (fromEnum x)
>     get = do t <- get
>              return (toEnum t)

> instance Binary Fixity where
>     put x = put (fromEnum x)
>     get = do t <- get
>              return (toEnum t)

> instance Binary Opt where
>     put x = put (fromEnum x)
>     get = do t <- get
>              return (toEnum t)

> instance Binary TyOpt where
>     put x = put (fromEnum x)
>     get = do t <- get
>              return (toEnum t)

> instance Binary Laziness where
>     put x = put (fromEnum x)
>     get = do t <- get
>              return (toEnum t)

> instance Binary Do where
>     put (DoBinding f l i t y) = do put (0 :: Word8)
>                                    put f; put l; put i; put t; put y
>     put (DoLet a b c d e) = do put (1 :: Word8)
>                                put a; put b; put c; put d; put e
>     put (DoExp a b c) = do put (2 :: Word8); put a; put b; put c

>     get = do tag <- getWord8
>              case tag of
>                0 -> liftM5 DoBinding get get get get get
>                1 -> liftM5 DoLet get get get get get
>                2 -> liftM3 DoExp get get get

> instance Binary RawTerm where
>     put (RVar a b c) = do put (0 :: Word8); put a; put b; put c
>     put (RExpVar a b c) = do put (1 :: Word8); put a; put b; put c
>     put (RApp a b c d) = do put (2 :: Word8); put a; put b; put c; put d
>     put (RAppImp a b c d e) 
>        = do put (3 :: Word8); put a; put b; put c; put d; put e
>     put (RBind a b c) = do put (4 :: Word8); put a; put b; put c
>     put (RConst a b c) = do put (5 :: Word8); put a; put b; put c
>     put RPlaceholder = put (6 :: Word8)
>     put (RMetavar i) = do put (7 :: Word8); put i
>     put (RInfix a b c d e) 
>        = do put (8 :: Word8); put a; put b; put c; put d; put e
>     put (RUserInfix a b c d e f) 
>        = do put (9 :: Word8); put a; put b; put c; put d; put e; put f
>     put (RDo xs) = do put (10 :: Word8); put xs
>     put (RReturn a b) = do put (11 :: Word8); put a; put b
>     put (RIdiom i) = do put (12 :: Word8); put i
>     put (RPure i) = do put (13 :: Word8); put i
>     put RRefl = do put (14 :: Word8)
>     put (RError f l i) = do put (15 :: Word8); put f; put l; put i

>     get = do tag <- getWord8
>              case tag of
>                0 -> liftM3 RVar get get get
>                1 -> liftM3 RExpVar get get get
>                2 -> liftM4 RApp get get get get
>                3 -> liftM5 RAppImp get get get get get
>                4 -> liftM3 RBind get get get
>                5 -> liftM3 RConst get get get
>                6 -> return RPlaceholder
>                7 -> liftM RMetavar get
>                8 -> liftM5 RInfix get get get get get
>                9 -> do a <- get; b <- get; c <- get; d <- get; e <- get;
>                        f <- get;
>                        return $ RUserInfix a b c d e f
>                10 -> liftM RDo get
>                11 -> liftM2 RReturn get get
>                12 -> liftM RIdiom get
>                13 -> liftM RPure get
>                14 -> return RRefl
>                15 -> liftM3 RError get get get

> instance Binary Constant where
>     put (Num i) = do put (0 :: Word8); put i
>     put (Str i) = do put (1 :: Word8); put i
>     put (Bo b) = do put (2 :: Word8); put b
>     put (Ch c) = do put (3 :: Word8); put c
>     put (Fl f) = do put (4 :: Word8); put f
>     put TYPE = put (5 :: Word8)
>     put StringType = put (6 :: Word8)
>     put IntType = put (7 :: Word8)
>     put FloatType = put (8 :: Word8)
>     put CharType = put (9 :: Word8)
>     put PtrType = put (10 :: Word8)
>     put (Builtin i) = do put (11 :: Word8); put i

>     get = do tag <- getWord8
>              case tag of
>                0 -> liftM Num get
>                1 -> liftM Str get
>                2 -> liftM Bo get
>                3 -> liftM Ch get
>                4 -> liftM Fl get
>                5 -> return TYPE
>                6 -> return StringType
>                7 -> return IntType
>                8 -> return FloatType
>                9 -> return CharType
>                10 -> return PtrType
>                11 -> liftM Builtin get

> instance Binary TransData where
>     put (Force a b c d e f) = do put (0 :: Word8)
>                                  put a; put b; put c; put d; put e; put f
>     put (Collapse a b c d) = do put (1 :: Word8)
>                                 put a; put b; put c; put d
>     put (Drop a b c d) = do put (2 :: Word8)
>                             put a; put b; put c; put d
>     get = do tag <- getWord8
>              case tag of
>                0 -> do a <- get; b <- get; c <- get; d <- get;
>                        e <- get; f <- get;
>                        return (Force a b c d e f)
>                1 -> liftM4 Collapse get get get get
>                2 -> liftM4 Drop get get get get

> instance Binary Transform where
>     put (Trans n _ a) = do put n; put a
>     get = do n <- get; a <- get
>              let trans = case a of
>                            Nothing -> Nothing
>                            Just a' -> Just (rebuildTrans a')
>              return (Trans n trans a)

> instance Binary UserOps where
>     put (UO ds ts f) = do put ds; put ts; put f
>     get = do ds <- get; ts <- get; f <- get;
>              return (UO ds ts f)

> instance Binary IvorFun where
>     put (IvorFun a b c d e f g) = 
>         do put a; put b; put c; put d; put e; put f; put g;
>     get = do a <- get; b <- get; c <- get; d <- get; e <- get; f <- get; g <- get
>              return (IvorFun a b c d e f g)

> instance Binary CGFlag where
>     put NoCG = put (0 :: Word8)
>     put CGEval = put (1 :: Word8)
>     put (CExport s) = do put (2 :: Word8); put s
>     put Inline = put (3 :: Word8)
>     put (CGSpec x) = do put (4 :: Word8); put x

>     get = do tag <- getWord8
>              case tag of
>                0 -> return NoCG
>                1 -> return CGEval
>                2 -> liftM CExport get
>                3 -> return Inline
>                4 -> liftM CGSpec get

> instance Binary Decl where
>     put (DataDecl d) = do put (0 :: Word8); put d
>     put (Fwd a b c) = do put (1 :: Word8); put a; put b; put c
>     put (Fun a b) = do put (2 :: Word8); put a; put b
>     put (TermDef a b c) = do put (3 :: Word8); put a; put b; put c
>     put Constructor = put (4 :: Word8)
>     put (Prf d) = do put (5 :: Word8); put d
>     put (LatexDefs d) = do put (6 :: Word8); put d
>     put (Using a b) = do put (7 :: Word8); put a; put b
>     put (Params a b) = do put (8 :: Word8); put a; put b
>     put (DoUsing a b c) = do put (9 :: Word8); put a; put b; put c
>     put (Idiom a b c) = do put (10 :: Word8); put a; put b; put c
>     put (CLib d) = do put (11 :: Word8); put d
>     put (CInclude d) = do put (12 :: Word8); put d
>     put (Fixity a b c) = do put (13 :: Word8); put a; put b; put c
>     put (Transform a b) = do put (14 :: Word8); put a; put b
>     put (Freeze a) = do put (15 :: Word8); put a

>     get = do tag <- getWord8
>              case tag of
>                0 -> liftM DataDecl get
>                1 -> liftM3 Fwd get get get
>                2 -> liftM2 Fun get get
>                3 -> liftM3 TermDef get get get
>                4 -> return Constructor
>                5 -> liftM Prf get
>                6 -> liftM LatexDefs get
>                7 -> liftM2 Using get get
>                8 -> liftM2 Params get get
>                9 -> liftM3 DoUsing get get get
>                10 -> liftM3 Idiom get get get
>                11 -> liftM CLib get
>                12 -> liftM CInclude get
>                13 -> liftM3 Fixity get get get
>                14 -> liftM2 Transform get get
>                15 -> liftM Freeze get

> instance Binary Datatype where
>     put (Datatype a b c d e f g) = do put (0 :: Word8)
>                                       put a; put b; put c; put d; put e;
>                                       put f; put g;
>     put (Latatype a b c d) = do put (1 :: Word8)
>                                 put a; put b; put c; put d
>     get = do tag <- getWord8
>              case tag of
>                0 -> do a <- get; b <- get; c <- get; d <- get;
>                        e <- get; f <- get; g <- get;
>                        return (Datatype a b c d e f g)
>                1 -> liftM4 Latatype get get get get

> instance Binary Function where
>     put (Function a b c d e) = do put a; put b; put c; put d; put e
>     get = liftM5 Function get get get get get

> instance Binary Proof where
>     put (Proof a b c) = do put a; put b; put c
>     get = liftM3 Proof get get get

> instance Binary RawClause where
>     put (RawClause a b) = do put (0 :: Word8); put a; put b
>     put (RawWithClause a b c d) = do put (0 :: Word8); put a; put b; put c; put d
>     get = do tag <- getWord8
>              case tag of
>                0 -> liftM2 RawClause get get
>                1 -> liftM4 RawWithClause get get get get

> instance Binary Patterns where
>     put (Patterns p) = put p
>     get = liftM Patterns get

> instance Binary PClause where
>     put (PClause a b c) = do put (0 :: Word8); put a; put b; put c
>     put (PWithClause a b c d) = do put (0 :: Word8); put a; put b; put c; put d
>     get = do tag <- getWord8
>              case tag of
>                0 -> liftM3 PClause get get get
>                1 -> liftM4 PWithClause get get get get

> instance Binary Inductive where
>     put (Inductive a b c d e) = do put a; put b; put c; put d; put e
>     get = liftM5 Inductive get get get get get

> instance Binary ITactic where
>     put (Intro a) = do put (0 :: Word8); put a
>     put (Refine a) = do put (1 :: Word8); put a
>     put (Generalise a) = do put (2 :: Word8); put a
>     put ReflP = put (3 :: Word8)
>     put (Induction a) = do put (4 :: Word8); put a
>     put (Fill a) = do put (5 :: Word8); put a
>     put Trivial = put (6 :: Word8)
>     put (Idris.AbsSyntax.Case a) = do put (7 :: Word8); put a
>     put (Rewrite a b c) = do put (8 :: Word8); put a; put b; put c
>     put (Unfold a) = do put (9 :: Word8); put a
>     put Compute = put (10 :: Word8)
>     put (Equiv a) = do put (11 :: Word8); put a
>     put (Believe a) = do put (12 :: Word8); put a
>     put (Use a) = do put (13 :: Word8); put a
>     put (Decide a) = do put (14 :: Word8); put a
>     put (RunTactic a) = do put (15 :: Word8); put a
>     put Qed = put (16 :: Word8)

>     get = do tag <- getWord8
>              case tag of
>                0 -> liftM Intro get
>                1 -> liftM Refine get
>                2 -> liftM Generalise get
>                3 -> return ReflP
>                4 -> liftM Induction get
>                5 -> liftM Fill get
>                6 -> return Trivial
>                7 -> liftM Idris.AbsSyntax.Case get
>                8 -> liftM3 Rewrite get get get
>                9 -> liftM Unfold get
>                10 -> return Compute
>                11 -> liftM Equiv get
>                12 -> liftM Believe get
>                13 -> liftM Use get
>                14 -> liftM Decide get
>                15 -> liftM RunTactic get
>                16 -> return Qed

> instance Binary IvorDef where
>     put (PattDef ps) = do put (0 :: Word8); put ps
>     put ITyCon = put (1 :: Word8)
>     put IDataCon = put (2 :: Word8)
>     put (SimpleDef t) = do put (3 :: Word8); put t
>     put (DataDef a b) = do put (4 :: Word8); put a; put b
>     put (IProof ts) = do put (5 :: Word8); put ts
>     put Later = put (6 :: Word8)
>     put LataDef = put (7 :: Word8)

>     get = do tag <- getWord8
>              case tag of
>                0 -> liftM PattDef get
>                1 -> return ITyCon
>                2 -> return IDataCon
>                3 -> liftM SimpleDef get
>                4 -> liftM2 DataDef get get
>                5 -> liftM IProof get
>                6 -> return Later
>                7 -> return LataDef

> instance Binary IdrisState where
>     put (IState a b c d e f g) 
>        = do put a; put b; put c; put d; put e; put f; put g
>     get = do a <- get; b <- get; c <- get;
>              d <- get; e <- get; f <- get; g <- get
>              return (IState a b c d e f g)