{-|
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 :: Err' a -> Put
put (Msg String
str) = do Word8 -> Put
putWord8 Word8
0
                     String -> Put
forall t. Binary t => t -> Put
put String
str
  put (InternalMsg String
str) = do Word8 -> Put
putWord8 Word8
1
                             String -> Put
forall t. Binary t => t -> Put
put String
str
  put (CantUnify Bool
x (a, Maybe Provenance)
y (a, Maybe Provenance)
z Err' a
e [(Name, a)]
ctxt Int
i) = do Word8 -> Put
putWord8 Word8
2
                                      Bool -> Put
forall t. Binary t => t -> Put
put Bool
x
                                      (a, Maybe Provenance) -> Put
forall t. Binary t => t -> Put
put (a, Maybe Provenance)
y
                                      (a, Maybe Provenance) -> Put
forall t. Binary t => t -> Put
put (a, Maybe Provenance)
z
                                      Err' a -> Put
forall t. Binary t => t -> Put
put Err' a
e
                                      [(Name, a)] -> Put
forall t. Binary t => t -> Put
put [(Name, a)]
ctxt
                                      Int -> Put
forall t. Binary t => t -> Put
put Int
i
  put (InfiniteUnify Name
n a
t [(Name, a)]
ctxt) = do Word8 -> Put
putWord8 Word8
3
                                    Name -> Put
forall t. Binary t => t -> Put
put Name
n
                                    a -> Put
forall t. Binary t => t -> Put
put a
t
                                    [(Name, a)] -> Put
forall t. Binary t => t -> Put
put [(Name, a)]
ctxt
  put (CantConvert a
x a
y [(Name, a)]
ctxt) = do Word8 -> Put
putWord8 Word8
4
                                  a -> Put
forall t. Binary t => t -> Put
put a
x
                                  a -> Put
forall t. Binary t => t -> Put
put a
y
                                  [(Name, a)] -> Put
forall t. Binary t => t -> Put
put [(Name, a)]
ctxt
  put (CantSolveGoal a
x [(Name, a)]
ctxt) = do Word8 -> Put
putWord8 Word8
5
                                  a -> Put
forall t. Binary t => t -> Put
put a
x
                                  [(Name, a)] -> Put
forall t. Binary t => t -> Put
put [(Name, a)]
ctxt
  put (UnifyScope Name
n1 Name
n2 a
x [(Name, a)]
ctxt) = do Word8 -> Put
putWord8 Word8
6
                                     Name -> Put
forall t. Binary t => t -> Put
put Name
n1
                                     Name -> Put
forall t. Binary t => t -> Put
put Name
n2
                                     a -> Put
forall t. Binary t => t -> Put
put a
x
                                     [(Name, a)] -> Put
forall t. Binary t => t -> Put
put [(Name, a)]
ctxt
  put (CantInferType String
str) = do Word8 -> Put
putWord8 Word8
7
                               String -> Put
forall t. Binary t => t -> Put
put String
str
  put (NonFunctionType a
t1 a
t2) = do Word8 -> Put
putWord8 Word8
8
                                   a -> Put
forall t. Binary t => t -> Put
put a
t1
                                   a -> Put
forall t. Binary t => t -> Put
put a
t2
  put (NotEquality a
t1 a
t2) = do Word8 -> Put
putWord8 Word8
9
                               a -> Put
forall t. Binary t => t -> Put
put a
t1
                               a -> Put
forall t. Binary t => t -> Put
put a
t2
  put (TooManyArguments Name
n) = do Word8 -> Put
putWord8 Word8
10
                                Name -> Put
forall t. Binary t => t -> Put
put Name
n
  put (CantIntroduce a
t) = do Word8 -> Put
putWord8 Word8
11
                             a -> Put
forall t. Binary t => t -> Put
put a
t
  put (NoSuchVariable Name
n) = do Word8 -> Put
putWord8 Word8
12
                              Name -> Put
forall t. Binary t => t -> Put
put Name
n
  put (NoTypeDecl Name
n) = do Word8 -> Put
putWord8 Word8
13
                          Name -> Put
forall t. Binary t => t -> Put
put Name
n
  put (NotInjective a
x a
y a
z) = do Word8 -> Put
putWord8 Word8
14
                                a -> Put
forall t. Binary t => t -> Put
put a
x
                                a -> Put
forall t. Binary t => t -> Put
put a
y
                                a -> Put
forall t. Binary t => t -> Put
put a
z
  put (CantResolve Bool
_ a
t Err' a
u) = do Word8 -> Put
putWord8 Word8
15
                               a -> Put
forall t. Binary t => t -> Put
put a
t
                               Err' a -> Put
forall t. Binary t => t -> Put
put Err' a
u
  put (CantResolveAlts [Name]
ns) = do Word8 -> Put
putWord8 Word8
16
                                [Name] -> Put
forall t. Binary t => t -> Put
put [Name]
ns
  put (IncompleteTerm a
t) = do Word8 -> Put
putWord8 Word8
17
                              a -> Put
forall t. Binary t => t -> Put
put a
t
  put (UniverseError FC
x1 UExp
x2 (Int, Int)
x3 (Int, Int)
x4 [ConstraintFC]
x5) = do Word8 -> Put
putWord8 Word8
18
                                          FC -> Put
forall t. Binary t => t -> Put
put FC
x1
                                          UExp -> Put
forall t. Binary t => t -> Put
put UExp
x2
                                          (Int, Int) -> Put
forall t. Binary t => t -> Put
put (Int, Int)
x3
                                          (Int, Int) -> Put
forall t. Binary t => t -> Put
put (Int, Int)
x4
                                          [ConstraintFC] -> Put
forall t. Binary t => t -> Put
put [ConstraintFC]
x5
  put (UniqueError Universe
u Name
n) = do Word8 -> Put
putWord8 Word8
19
                             Universe -> Put
forall t. Binary t => t -> Put
put Universe
u
                             Name -> Put
forall t. Binary t => t -> Put
put Name
n
  put (UniqueKindError Universe
u Name
n) = do Word8 -> Put
putWord8 Word8
20
                                 Universe -> Put
forall t. Binary t => t -> Put
put Universe
u
                                 Name -> Put
forall t. Binary t => t -> Put
put Name
n
  put Err' a
ProgramLineComment = Word8 -> Put
putWord8 Word8
21
  put (Inaccessible Name
n) = do Word8 -> Put
putWord8 Word8
22
                            Name -> Put
forall t. Binary t => t -> Put
put Name
n
  put (NonCollapsiblePostulate Name
n) = do Word8 -> Put
putWord8 Word8
23
                                       Name -> Put
forall t. Binary t => t -> Put
put Name
n
  put (AlreadyDefined Name
n) = do Word8 -> Put
putWord8 Word8
24
                              Name -> Put
forall t. Binary t => t -> Put
put Name
n
  put (ProofSearchFail Err' a
e) = do Word8 -> Put
putWord8 Word8
25
                               Err' a -> Put
forall t. Binary t => t -> Put
put Err' a
e
  put (NoRewriting a
l a
r a
t) = do Word8 -> Put
putWord8 Word8
26
                               a -> Put
forall t. Binary t => t -> Put
put a
l
                               a -> Put
forall t. Binary t => t -> Put
put a
r
                               a -> Put
forall t. Binary t => t -> Put
put a
t
  put (At FC
fc Err' a
e) = do Word8 -> Put
putWord8 Word8
27
                     FC -> Put
forall t. Binary t => t -> Put
put FC
fc
                     Err' a -> Put
forall t. Binary t => t -> Put
put Err' a
e
  put (Elaborating String
str Name
n Maybe a
ty Err' a
e) = do Word8 -> Put
putWord8 Word8
28
                                    String -> Put
forall t. Binary t => t -> Put
put String
str
                                    Name -> Put
forall t. Binary t => t -> Put
put Name
n
                                    Maybe a -> Put
forall t. Binary t => t -> Put
put Maybe a
ty
                                    Err' a -> Put
forall t. Binary t => t -> Put
put Err' a
e
  put (ElaboratingArg Name
n1 Name
n2 [(Name, Name)]
ns Err' a
e) = do Word8 -> Put
putWord8 Word8
29
                                       Name -> Put
forall t. Binary t => t -> Put
put Name
n1
                                       Name -> Put
forall t. Binary t => t -> Put
put Name
n2
                                       [(Name, Name)] -> Put
forall t. Binary t => t -> Put
put [(Name, Name)]
ns
                                       Err' a -> Put
forall t. Binary t => t -> Put
put Err' a
e
  put (ProviderError String
str) = do Word8 -> Put
putWord8 Word8
30
                               String -> Put
forall t. Binary t => t -> Put
put String
str
  put (LoadingFailed String
str Err' a
e) = do Word8 -> Put
putWord8 Word8
31
                                 String -> Put
forall t. Binary t => t -> Put
put String
str
                                 Err' a -> Put
forall t. Binary t => t -> Put
put Err' a
e
  put (ReflectionError [[ErrorReportPart]]
parts Err' a
e) = do Word8 -> Put
putWord8 Word8
32
                                     [[ErrorReportPart]] -> Put
forall t. Binary t => t -> Put
put [[ErrorReportPart]]
parts
                                     Err' a -> Put
forall t. Binary t => t -> Put
put Err' a
e
  put (ReflectionFailed String
str Err' a
e) = do Word8 -> Put
putWord8 Word8
33
                                    String -> Put
forall t. Binary t => t -> Put
put String
str
                                    Err' a -> Put
forall t. Binary t => t -> Put
put Err' a
e
  put (WithFnType a
t) = do Word8 -> Put
putWord8 Word8
34
                          a -> Put
forall t. Binary t => t -> Put
put a
t
  put (CantMatch a
t) = do Word8 -> Put
putWord8 Word8
35
                         a -> Put
forall t. Binary t => t -> Put
put a
t
  put (ElabScriptDebug [ErrorReportPart]
x1 a
x2 [(Name, a, [(Name, Binder a)])]
x3) = do Word8 -> Put
putWord8 Word8
36
                                      [ErrorReportPart] -> Put
forall t. Binary t => t -> Put
put [ErrorReportPart]
x1
                                      a -> Put
forall t. Binary t => t -> Put
put a
x2
                                      [(Name, a, [(Name, Binder a)])] -> Put
forall t. Binary t => t -> Put
put [(Name, a, [(Name, Binder a)])]
x3
  put (InvalidTCArg Name
n a
t) = do Word8 -> Put
putWord8 Word8
38
                              Name -> Put
forall t. Binary t => t -> Put
put Name
n
                              a -> Put
forall t. Binary t => t -> Put
put a
t
  put (ElabScriptStuck a
x1) = do Word8 -> Put
putWord8 Word8
39
                                a -> Put
forall t. Binary t => t -> Put
put a
x1
  put (UnknownImplicit Name
n Name
f) = do Word8 -> Put
putWord8 Word8
40
                                 Name -> Put
forall t. Binary t => t -> Put
put Name
n
                                 Name -> Put
forall t. Binary t => t -> Put
put Name
f
  put (NoValidAlts [Name]
ns) = do Word8 -> Put
putWord8 Word8
41
                            [Name] -> Put
forall t. Binary t => t -> Put
put [Name]
ns
  put (RunningElabScript Err' a
e) = do Word8 -> Put
putWord8 Word8
42
                                 Err' a -> Put
forall t. Binary t => t -> Put
put Err' a
e
  put (ElabScriptStaging Name
n) = do Word8 -> Put
putWord8 Word8
43
                                 Name -> Put
forall t. Binary t => t -> Put
put Name
n
  put (FancyMsg [ErrorReportPart]
xs) = do Word8 -> Put
putWord8 Word8
44
                         [ErrorReportPart] -> Put
forall t. Binary t => t -> Put
put [ErrorReportPart]
xs
  get :: Get (Err' a)
get = do i <- Get Word8
getWord8
           case i of
             Word8
0 -> (String -> Err' a) -> Get String -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Err' a
forall t. String -> Err' t
Msg Get String
forall t. Binary t => Get t
get
             Word8
1 -> (String -> Err' a) -> Get String -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Err' a
forall t. String -> Err' t
InternalMsg Get String
forall t. Binary t => Get t
get
             Word8
2 -> do x <- Get Bool
forall t. Binary t => Get t
get ; y <- get ; z <- get ; e <- get ; ctxt <- get ; i <- get
                     return $ CantUnify x y z e ctxt i
             Word8
3 -> do x <- Get Name
forall t. Binary t => Get t
get ; y <- get ; z <- get
                     return $ InfiniteUnify x y z
             Word8
4 -> do x <- Get a
forall t. Binary t => Get t
get ; y <- get ; z <- get
                     return $ CantConvert x y z
             Word8
5 -> do x <- Get a
forall t. Binary t => Get t
get ; y <- get
                     return $ CantSolveGoal x y
             Word8
6 -> do w <- Get Name
forall t. Binary t => Get t
get ; x <- get ; y <- get ; z <- get
                     return $ UnifyScope w x y z
             Word8
7 -> (String -> Err' a) -> Get String -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Err' a
forall t. String -> Err' t
CantInferType Get String
forall t. Binary t => Get t
get
             Word8
8 -> do x <- Get a
forall t. Binary t => Get t
get ; y <- get
                     return $ NonFunctionType x y
             Word8
9 -> do x <- Get a
forall t. Binary t => Get t
get ; y <- get
                     return $ NotEquality x y
             Word8
10 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Err' a
forall t. Name -> Err' t
TooManyArguments Get Name
forall t. Binary t => Get t
get
             Word8
11 -> (a -> Err' a) -> Get a -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Err' a
forall t. t -> Err' t
CantIntroduce Get a
forall t. Binary t => Get t
get
             Word8
12 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Err' a
forall t. Name -> Err' t
NoSuchVariable Get Name
forall t. Binary t => Get t
get
             Word8
13 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Err' a
forall t. Name -> Err' t
NoTypeDecl Get Name
forall t. Binary t => Get t
get
             Word8
14 -> do x <- Get a
forall t. Binary t => Get t
get ; y <- get ; z <- get
                      return $ NotInjective x y z
             Word8
15 -> Bool -> a -> Err' a -> Err' a
forall t. Bool -> t -> Err' t -> Err' t
CantResolve Bool
False (a -> Err' a -> Err' a) -> Get a -> Get (Err' a -> Err' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get a
forall t. Binary t => Get t
get Get (Err' a -> Err' a) -> Get (Err' a) -> Get (Err' a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Err' a)
forall t. Binary t => Get t
get
             Word8
16 -> ([Name] -> Err' a) -> Get [Name] -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Name] -> Err' a
forall t. [Name] -> Err' t
CantResolveAlts Get [Name]
forall t. Binary t => Get t
get
             Word8
17 -> (a -> Err' a) -> Get a -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Err' a
forall t. t -> Err' t
IncompleteTerm Get a
forall t. Binary t => Get t
get
             Word8
18 -> FC -> UExp -> (Int, Int) -> (Int, Int) -> [ConstraintFC] -> Err' a
forall t.
FC -> UExp -> (Int, Int) -> (Int, Int) -> [ConstraintFC] -> Err' t
UniverseError (FC
 -> UExp -> (Int, Int) -> (Int, Int) -> [ConstraintFC] -> Err' a)
-> Get FC
-> Get
     (UExp -> (Int, Int) -> (Int, Int) -> [ConstraintFC] -> Err' a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get FC
forall t. Binary t => Get t
get Get (UExp -> (Int, Int) -> (Int, Int) -> [ConstraintFC] -> Err' a)
-> Get UExp
-> Get ((Int, Int) -> (Int, Int) -> [ConstraintFC] -> Err' a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get UExp
forall t. Binary t => Get t
get Get ((Int, Int) -> (Int, Int) -> [ConstraintFC] -> Err' a)
-> Get (Int, Int) -> Get ((Int, Int) -> [ConstraintFC] -> Err' a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Int, Int)
forall t. Binary t => Get t
get Get ((Int, Int) -> [ConstraintFC] -> Err' a)
-> Get (Int, Int) -> Get ([ConstraintFC] -> Err' a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Int, Int)
forall t. Binary t => Get t
get Get ([ConstraintFC] -> Err' a)
-> Get [ConstraintFC] -> Get (Err' a)
forall a b. Get (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get [ConstraintFC]
forall t. Binary t => Get t
get
             Word8
19 -> do x <- Get Universe
forall t. Binary t => Get t
get ; y <- get
                      return $ UniqueError x y
             Word8
20 -> do x <- Get Universe
forall t. Binary t => Get t
get ; y <- get
                      return $ UniqueKindError x y
             Word8
21 -> Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return Err' a
forall t. Err' t
ProgramLineComment
             Word8
22 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Err' a
forall t. Name -> Err' t
Inaccessible Get Name
forall t. Binary t => Get t
get
             Word8
23 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Err' a
forall t. Name -> Err' t
NonCollapsiblePostulate Get Name
forall t. Binary t => Get t
get
             Word8
24 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Err' a
forall t. Name -> Err' t
AlreadyDefined Get Name
forall t. Binary t => Get t
get
             Word8
25 -> (Err' a -> Err' a) -> Get (Err' a) -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Err' a -> Err' a
forall t. Err' t -> Err' t
ProofSearchFail Get (Err' a)
forall t. Binary t => Get t
get
             Word8
26 -> do l <- Get a
forall t. Binary t => Get t
get; r <- get; t <- get
                      return $ NoRewriting l r t
             Word8
27 -> do x <- Get FC
forall t. Binary t => Get t
get ; y <- get
                      return $ At x y
             Word8
28 -> do w <- Get String
forall t. Binary t => Get t
get; x <- get ; y <- get ; z <- get
                      return $ Elaborating w x y z
             Word8
29 -> do w <- Get Name
forall t. Binary t => Get t
get ; x <- get ; y <- get ; z <- get
                      return $ ElaboratingArg w x y z
             Word8
30 -> (String -> Err' a) -> Get String -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Err' a
forall t. String -> Err' t
ProviderError Get String
forall t. Binary t => Get t
get
             Word8
31 -> do x <- Get String
forall t. Binary t => Get t
get ; y <- get
                      return $ LoadingFailed x y
             Word8
32 -> do x <- Get [[ErrorReportPart]]
forall t. Binary t => Get t
get ; y <- get
                      return $ ReflectionError x y
             Word8
33 -> do x <- Get String
forall t. Binary t => Get t
get ; y <- get
                      return $ ReflectionFailed x y
             Word8
34 -> (a -> Err' a) -> Get a -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Err' a
forall t. t -> Err' t
WithFnType Get a
forall t. Binary t => Get t
get
             Word8
35 -> (a -> Err' a) -> Get a -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Err' a
forall t. t -> Err' t
CantMatch Get a
forall t. Binary t => Get t
get
             Word8
36 -> do x1 <- Get [ErrorReportPart]
forall t. Binary t => Get t
get
                      x2 <- get
                      x3 <- get
                      return (ElabScriptDebug x1 x2 x3)
             Word8
38 -> do x1 <- Get Name
forall t. Binary t => Get t
get
                      x2 <- get
                      return (InvalidTCArg x1 x2)
             Word8
39 -> do x1 <- Get a
forall t. Binary t => Get t
get
                      return (ElabScriptStuck x1)
             Word8
40 -> do x <- Get Name
forall t. Binary t => Get t
get ; y <- get
                      return $ UnknownImplicit x y
             Word8
41 -> ([Name] -> Err' a) -> Get [Name] -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Name] -> Err' a
forall t. [Name] -> Err' t
NoValidAlts Get [Name]
forall t. Binary t => Get t
get
             Word8
42 -> (Err' a -> Err' a) -> Get (Err' a) -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Err' a -> Err' a
forall t. Err' t -> Err' t
RunningElabScript Get (Err' a)
forall t. Binary t => Get t
get
             Word8
43 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Err' a
forall t. Name -> Err' t
ElabScriptStaging Get Name
forall t. Binary t => Get t
get
             Word8
44 -> ([ErrorReportPart] -> Err' a)
-> Get [ErrorReportPart] -> Get (Err' a)
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [ErrorReportPart] -> Err' a
forall t. [ErrorReportPart] -> Err' t
FancyMsg Get [ErrorReportPart]
forall t. Binary t => Get t
get
             Word8
_ -> String -> Get (Err' a)
forall a. HasCallStack => String -> a
error String
"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 :: Const -> Put
put Const
x
          = case Const
x of
                I Int
x1 -> do Word8 -> Put
putWord8 Word8
0
                           Int -> Put
forall t. Binary t => t -> Put
put Int
x1
                BI Integer
x1 -> do Word8 -> Put
putWord8 Word8
1
                            Integer -> Put
forall t. Binary t => t -> Put
put Integer
x1
                Fl Double
x1 -> do Word8 -> Put
putWord8 Word8
2
                            Double -> Put
putDoublele Double
x1
                Ch Char
x1 -> do Word8 -> Put
putWord8 Word8
3
                            Char -> Put
forall t. Binary t => t -> Put
put Char
x1
                Str String
x1 -> do Word8 -> Put
putWord8 Word8
4
                             String -> Put
forall t. Binary t => t -> Put
put String
x1
                B8 Word8
x1 -> Word8 -> Put
putWord8 Word8
5 Put -> Put -> Put
forall a b. PutM a -> PutM b -> PutM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Word8 -> Put
forall t. Binary t => t -> Put
put Word8
x1
                B16 Word16
x1 -> Word8 -> Put
putWord8 Word8
6 Put -> Put -> Put
forall a b. PutM a -> PutM b -> PutM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Word16 -> Put
forall t. Binary t => t -> Put
put Word16
x1
                B32 Word32
x1 -> Word8 -> Put
putWord8 Word8
7 Put -> Put -> Put
forall a b. PutM a -> PutM b -> PutM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Word32 -> Put
forall t. Binary t => t -> Put
put Word32
x1
                B64 Word64
x1 -> Word8 -> Put
putWord8 Word8
8 Put -> Put -> Put
forall a b. PutM a -> PutM b -> PutM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Word64 -> Put
forall t. Binary t => t -> Put
put Word64
x1

                (AType (ATInt IntTy
ITNative)) -> Word8 -> Put
putWord8 Word8
9
                (AType (ATInt IntTy
ITBig)) -> Word8 -> Put
putWord8 Word8
10
                (AType ArithTy
ATFloat) -> Word8 -> Put
putWord8 Word8
11
                (AType (ATInt IntTy
ITChar)) -> Word8 -> Put
putWord8 Word8
12
                Const
StrType -> Word8 -> Put
putWord8 Word8
13
                Const
Forgot -> Word8 -> Put
putWord8 Word8
15
                (AType (ATInt (ITFixed NativeTy
ity))) -> Word8 -> Put
putWord8 (Int -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
16 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ NativeTy -> Int
forall a. Enum a => a -> Int
fromEnum NativeTy
ity)) -- 16-19 inclusive
                Const
VoidType -> Word8 -> Put
putWord8 Word8
27
                Const
WorldType -> Word8 -> Put
putWord8 Word8
28
                Const
TheWorld -> Word8 -> Put
putWord8 Word8
29
        get :: Get Const
get
          = do i <- Get Word8
getWord8
               case i of
                   Word8
0 -> do x1 <- Get Int
forall t. Binary t => Get t
get
                           return (I x1)
                   Word8
1 -> do x1 <- Get Integer
forall t. Binary t => Get t
get
                           return (BI x1)
                   Word8
2 -> do x1 <- Get Double
getDoublele
                           return (Fl x1)
                   Word8
3 -> do x1 <- Get Char
forall t. Binary t => Get t
get
                           return (Ch x1)
                   Word8
4 -> do x1 <- Get String
forall t. Binary t => Get t
get
                           return (Str x1)
                   Word8
5 -> (Word8 -> Const) -> Get Word8 -> Get Const
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word8 -> Const
B8 Get Word8
forall t. Binary t => Get t
get
                   Word8
6 -> (Word16 -> Const) -> Get Word16 -> Get Const
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word16 -> Const
B16 Get Word16
forall t. Binary t => Get t
get
                   Word8
7 -> (Word32 -> Const) -> Get Word32 -> Get Const
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word32 -> Const
B32 Get Word32
forall t. Binary t => Get t
get
                   Word8
8 -> (Word64 -> Const) -> Get Word64 -> Get Const
forall a b. (a -> b) -> Get a -> Get b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word64 -> Const
B64 Get Word64
forall t. Binary t => Get t
get

                   Word8
9 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITNative))
                   Word8
10 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITBig))
                   Word8
11 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType ArithTy
ATFloat)
                   Word8
12 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITChar))
                   Word8
13 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return Const
StrType
                   Word8
15 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return Const
Forgot

                   Word8
16 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT8)))
                   Word8
17 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT16)))
                   Word8
18 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT32)))
                   Word8
19 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT64)))

                   Word8
27 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return Const
VoidType
                   Word8
28 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return Const
WorldType
                   Word8
29 -> Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return Const
TheWorld
                   Word8
_ -> String -> Get Const
forall a. HasCallStack => String -> a
error String
"Corrupted binary data for Const"

instance Binary Raw
instance Binary RigCount
instance Binary ImplicitInfo where
        put :: ImplicitInfo -> Put
put ImplicitInfo
x
          = case ImplicitInfo
x of
                Impl Bool
x1 Bool
x2 Bool
x3 -> do Bool -> Put
forall t. Binary t => t -> Put
put Bool
x1; Bool -> Put
forall t. Binary t => t -> Put
put Bool
x2
        get :: Get ImplicitInfo
get
          = do x1 <- Get Bool
forall t. Binary t => Get t
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 :: Term -> Put
put Term
x
          = {-# SCC "putTT" #-}
            case Term
x of
                P NameType
x1 Name
x2 Term
x3 -> do Word8 -> Put
putWord8 Word8
0
                                 NameType -> Put
forall t. Binary t => t -> Put
put NameType
x1
                                 Name -> Put
forall t. Binary t => t -> Put
put Name
x2
--                                  put x3
                V Int
x1 -> if (Int
x1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
x1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
256)
                           then do Word8 -> Put
putWord8 Word8
1
                                   Word8 -> Put
putWord8 (Int -> Word8
forall a. Enum a => Int -> a
toEnum (Int
x1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
                           else do Word8 -> Put
putWord8 Word8
9
                                   Int -> Put
forall t. Binary t => t -> Put
put Int
x1
                Bind Name
x1 Binder Term
x2 Term
x3 -> do Word8 -> Put
putWord8 Word8
2
                                    Name -> Put
forall t. Binary t => t -> Put
put Name
x1
                                    Binder Term -> Put
forall t. Binary t => t -> Put
put Binder Term
x2
                                    Term -> Put
forall t. Binary t => t -> Put
put Term
x3
                App AppStatus Name
_ Term
x1 Term
x2 -> do Word8 -> Put
putWord8 Word8
3
                                  Term -> Put
forall t. Binary t => t -> Put
put Term
x1
                                  Term -> Put
forall t. Binary t => t -> Put
put Term
x2
                Constant Const
x1 -> do Word8 -> Put
putWord8 Word8
4
                                  Const -> Put
forall t. Binary t => t -> Put
put Const
x1
                Proj Term
x1 Int
x2 -> do Word8 -> Put
putWord8 Word8
5
                                 Term -> Put
forall t. Binary t => t -> Put
put Term
x1
                                 Word8 -> Put
putWord8 (Int -> Word8
forall a. Enum a => Int -> a
toEnum (Int
x2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
                Term
Erased -> Word8 -> Put
putWord8 Word8
6
                TType UExp
x1 -> do Word8 -> Put
putWord8 Word8
7
                               UExp -> Put
forall t. Binary t => t -> Put
put UExp
x1
                Term
Impossible -> Word8 -> Put
putWord8 Word8
8
                Inferred Term
x1 -> Term -> Put
forall t. Binary t => t -> Put
put Term
x1 -- drop the 'Inferred'
                UType Universe
x1 -> do Word8 -> Put
putWord8 Word8
10
                               Universe -> Put
forall t. Binary t => t -> Put
put Universe
x1
        get :: Get Term
get
          = do i <- Get Word8
getWord8
               case i of
                   Word8
0 -> do x1 <- Get NameType
forall t. Binary t => Get t
get
                           x2 <- get
--                            x3 <- get
                           return (P x1 x2 Erased)
                   Word8
1 -> do x1 <- Get Word8
getWord8
                           return (V ((fromEnum x1) - 1))
                   Word8
2 -> do x1 <- Get Name
forall t. Binary t => Get t
get
                           x2 <- get
                           x3 <- get
                           return (Bind x1 x2 x3)
                   Word8
3 -> do x1 <- Get Term
forall t. Binary t => Get t
get
                           x2 <- get
                           return (App Complete x1 x2)
                   Word8
4 -> do x1 <- Get Const
forall t. Binary t => Get t
get
                           return (Constant x1)
                   Word8
5 -> do x1 <- Get Term
forall t. Binary t => Get t
get
                           x2 <- getWord8
                           return (Proj x1 ((fromEnum x2)-1))
                   Word8
6 -> Term -> Get Term
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
forall n. TT n
Erased
                   Word8
7 -> do x1 <- Get UExp
forall t. Binary t => Get t
get
                           return (TType x1)
                   Word8
8 -> Term -> Get Term
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
forall n. TT n
Impossible
                   Word8
9 -> do x1 <- Get Int
forall t. Binary t => Get t
get
                           return (V x1)
                   Word8
10 -> do x1 <- Get Universe
forall t. Binary t => Get t
get
                            return (UType x1)
                   Word8
_ -> String -> Get Term
forall a. HasCallStack => String -> a
error String
"Corrupted binary data for TT"