content: {-|
  Module      : Idris.Core.Binary
  Description : Binary instances for the core datatypes
  
  License     : BSD3
  Maintainer  : The Idris Community.
  -}
  {-# LANGUAGE FlexibleInstances #-}
  
  {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
  module Idris.Core.Binary where
  
  import Idris.Core.TT
  
  import Data.Binary
  import Data.Binary.Get
  import Data.Binary.Put
  
  instance Binary ErrorReportPart
  instance Binary Provenance
  instance Binary UConstraint
  instance Binary ConstraintFC
  instance Binary a => Binary (Err' a) where
    put (Msg str) = do putWord8 0
                       put str
    put (InternalMsg str) = do putWord8 1
                               put str
    put (CantUnify x y z e ctxt i) = do putWord8 2
                                        put x
                                        put y
                                        put z
                                        put e
                                        put ctxt
                                        put i
    put (InfiniteUnify n t ctxt) = do putWord8 3
                                      put n
                                      put t
                                      put ctxt
    put (CantConvert x y ctxt) = do putWord8 4
                                    put x
                                    put y
                                    put ctxt
    put (CantSolveGoal x ctxt) = do putWord8 5
                                    put x
                                    put ctxt
    put (UnifyScope n1 n2 x ctxt) = do putWord8 6
                                       put n1
                                       put n2
                                       put x
                                       put ctxt
    put (CantInferType str) = do putWord8 7
                                 put str
    put (NonFunctionType t1 t2) = do putWord8 8
                                     put t1
                                     put t2
    put (NotEquality t1 t2) = do putWord8 9
                                 put t1
                                 put t2
    put (TooManyArguments n) = do putWord8 10
                                  put n
    put (CantIntroduce t) = do putWord8 11
                               put t
    put (NoSuchVariable n) = do putWord8 12
                                put n
    put (NoTypeDecl n) = do putWord8 13
                            put n
    put (NotInjective x y z) = do putWord8 14
                                  put x
                                  put y
                                  put z
    put (CantResolve _ t u) = do putWord8 15
                                 put t
                                 put u
    put (CantResolveAlts ns) = do putWord8 16
                                  put ns
    put (IncompleteTerm t) = do putWord8 17
                                put t
    put (UniverseError x1 x2 x3 x4 x5) = do putWord8 18
                                            put x1
                                            put x2
                                            put x3
                                            put x4
                                            put x5
    put (UniqueError u n) = do putWord8 19
                               put u
                               put n
    put (UniqueKindError u n) = do putWord8 20
                                   put u
                                   put n
    put ProgramLineComment = putWord8 21
    put (Inaccessible n) = do putWord8 22
                              put n
    put (NonCollapsiblePostulate n) = do putWord8 23
                                         put n
    put (AlreadyDefined n) = do putWord8 24
                                put n
    put (ProofSearchFail e) = do putWord8 25
                                 put e
    put (NoRewriting l r t) = do putWord8 26
                                 put l
                                 put r
                                 put t
    put (At fc e) = do putWord8 27
                       put fc
                       put e
    put (Elaborating str n ty e) = do putWord8 28
                                      put str
                                      put n
                                      put ty
                                      put e
    put (ElaboratingArg n1 n2 ns e) = do putWord8 29
                                         put n1
                                         put n2
                                         put ns
                                         put e
    put (ProviderError str) = do putWord8 30
                                 put str
    put (LoadingFailed str e) = do putWord8 31
                                   put str
                                   put e
    put (ReflectionError parts e) = do putWord8 32
                                       put parts
                                       put e
    put (ReflectionFailed str e) = do putWord8 33
                                      put str
                                      put e
    put (WithFnType t) = do putWord8 34
                            put t
    put (CantMatch t) = do putWord8 35
                           put t
    put (ElabScriptDebug x1 x2 x3) = do putWord8 36
                                        put x1
                                        put x2
                                        put x3
    put (InvalidTCArg n t) = do putWord8 38
                                put n
                                put t
    put (ElabScriptStuck x1) = do putWord8 39
                                  put x1
    put (UnknownImplicit n f) = do putWord8 40
                                   put n
                                   put f
    put (NoValidAlts ns) = do putWord8 41
                              put ns
    put (RunningElabScript e) = do putWord8 42
                                   put e
    put (ElabScriptStaging n) = do putWord8 43
                                   put n
    put (FancyMsg xs) = do putWord8 44
                           put xs
    get = do i <- getWord8
             case i of
               0 -> fmap Msg get
               1 -> fmap InternalMsg get
               2 -> do x <- get ; y <- get ; z <- get ; e <- get ; ctxt <- get ; i <- get
                       return $ CantUnify x y z e ctxt i
               3 -> do x <- get ; y <- get ; z <- get
                       return $ InfiniteUnify x y z
               4 -> do x <- get ; y <- get ; z <- get
                       return $ CantConvert x y z
               5 -> do x <- get ; y <- get
                       return $ CantSolveGoal x y
               6 -> do w <- get ; x <- get ; y <- get ; z <- get
                       return $ UnifyScope w x y z
               7 -> fmap CantInferType get
               8 -> do x <- get ; y <- get
                       return $ NonFunctionType x y
               9 -> do x <- get ; y <- get
                       return $ NotEquality x y
               10 -> fmap TooManyArguments get
               11 -> fmap CantIntroduce get
               12 -> fmap NoSuchVariable get
               13 -> fmap NoTypeDecl get
               14 -> do x <- get ; y <- get ; z <- get
                        return $ NotInjective x y z
               15 -> CantResolve False <$> get <*> get
               16 -> fmap CantResolveAlts get
               17 -> fmap IncompleteTerm get
               18 -> UniverseError <$> get <*> get <*> get <*> get <*> get
               19 -> do x <- get ; y <- get
                        return $ UniqueError x y
               20 -> do x <- get ; y <- get
                        return $ UniqueKindError x y
               21 -> return ProgramLineComment
               22 -> fmap Inaccessible get
               23 -> fmap NonCollapsiblePostulate get
               24 -> fmap AlreadyDefined get
               25 -> fmap ProofSearchFail get
               26 -> do l <- get; r <- get; t <- get
                        return $ NoRewriting l r t
               27 -> do x <- get ; y <- get
                        return $ At x y
               28 -> do w <- get; x <- get ; y <- get ; z <- get
                        return $ Elaborating w x y z
               29 -> do w <- get ; x <- get ; y <- get ; z <- get
                        return $ ElaboratingArg w x y z
               30 -> fmap ProviderError get
               31 -> do x <- get ; y <- get
                        return $ LoadingFailed x y
               32 -> do x <- get ; y <- get
                        return $ ReflectionError x y
               33 -> do x <- get ; y <- get
                        return $ ReflectionFailed x y
               34 -> fmap WithFnType get
               35 -> fmap CantMatch get
               36 -> do x1 <- get
                        x2 <- get
                        x3 <- get
                        return (ElabScriptDebug x1 x2 x3)
               38 -> do x1 <- get
                        x2 <- get
                        return (InvalidTCArg x1 x2)
               39 -> do x1 <- get
                        return (ElabScriptStuck x1)
               40 -> do x <- get ; y <- get
                        return $ UnknownImplicit x y
               41 -> fmap NoValidAlts get
               42 -> fmap RunningElabScript get
               43 -> fmap ElabScriptStaging get
               44 -> fmap FancyMsg get
               _ -> error "Corrupted binary data for Err'"
  ----- Generated by 'derive'
  
  instance Binary FC
  instance Binary FC'
  instance Binary Name
  instance Binary 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
                              putDoublele 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
                  Forgot -> putWord8 15
                  (AType (ATInt (ITFixed ity))) -> putWord8 (fromIntegral (16 + fromEnum ity)) -- 16-19 inclusive
                  VoidType -> putWord8 27
                  WorldType -> putWord8 28
                  TheWorld -> putWord8 29
          get
            = do i <- getWord8
                 case i of
                     0 -> do x1 <- get
                             return (I x1)
                     1 -> do x1 <- get
                             return (BI x1)
                     2 -> do x1 <- getDoublele
                             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
                     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)))
  
                     27 -> return VoidType
                     28 -> return WorldType
                     29 -> return TheWorld
                     _ -> error "Corrupted binary data for Const"
  
  instance Binary Raw
  instance Binary RigCount
  instance Binary ImplicitInfo where
          put x
            = case x of
                  Impl x1 x2 x3 -> do put x1; put x2
          get
            = do x1 <- get
                 x2 <- get
                 return (Impl x1 x2 False)
  
  instance (Binary b) => Binary (Binder b)
  instance Binary Universe
  instance Binary NameType
  instance Binary UExp
  instance Binary (TT Name) where
          put x
            = {-# SCC "putTT" #-}
              case x of
                  P x1 x2 x3 -> do putWord8 0
                                   put x1
                                   put x2
  --                                  put x3
                  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
                  Inferred x1 -> put x1 -- drop the 'Inferred'
                  UType x1 -> do putWord8 10
                                 put x1
          get
            = do i <- getWord8
                 case i of
                     0 -> do x1 <- get
                             x2 <- get
  --                            x3 <- 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 Complete 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"
  