{-|
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 Word8
i <- Get Word8
getWord8
           case Word8
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 Bool
x <- Get Bool
forall t. Binary t => Get t
get ; (a, Maybe Provenance)
y <- Get (a, Maybe Provenance)
forall t. Binary t => Get t
get ; (a, Maybe Provenance)
z <- Get (a, Maybe Provenance)
forall t. Binary t => Get t
get ; Err' a
e <- Get (Err' a)
forall t. Binary t => Get t
get ; [(Name, a)]
ctxt <- Get [(Name, a)]
forall t. Binary t => Get t
get ; Int
i <- Get Int
forall t. Binary t => Get t
get
                     Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ Bool
-> (a, Maybe Provenance)
-> (a, Maybe Provenance)
-> Err' a
-> [(Name, a)]
-> Int
-> Err' a
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
x (a, Maybe Provenance)
y (a, Maybe Provenance)
z Err' a
e [(Name, a)]
ctxt Int
i
             Word8
3 -> do Name
x <- Get Name
forall t. Binary t => Get t
get ; a
y <- Get a
forall t. Binary t => Get t
get ; [(Name, a)]
z <- Get [(Name, a)]
forall t. Binary t => Get t
get
                     Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ Name -> a -> [(Name, a)] -> Err' a
forall t. Name -> t -> [(Name, t)] -> Err' t
InfiniteUnify Name
x a
y [(Name, a)]
z
             Word8
4 -> do a
x <- Get a
forall t. Binary t => Get t
get ; a
y <- Get a
forall t. Binary t => Get t
get ; [(Name, a)]
z <- Get [(Name, a)]
forall t. Binary t => Get t
get
                     Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ a -> a -> [(Name, a)] -> Err' a
forall t. t -> t -> [(Name, t)] -> Err' t
CantConvert a
x a
y [(Name, a)]
z
             Word8
5 -> do a
x <- Get a
forall t. Binary t => Get t
get ; [(Name, a)]
y <- Get [(Name, a)]
forall t. Binary t => Get t
get
                     Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ a -> [(Name, a)] -> Err' a
forall t. t -> [(Name, t)] -> Err' t
CantSolveGoal a
x [(Name, a)]
y
             Word8
6 -> do Name
w <- Get Name
forall t. Binary t => Get t
get ; Name
x <- Get Name
forall t. Binary t => Get t
get ; a
y <- Get a
forall t. Binary t => Get t
get ; [(Name, a)]
z <- Get [(Name, a)]
forall t. Binary t => Get t
get
                     Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ Name -> Name -> a -> [(Name, a)] -> Err' a
forall t. Name -> Name -> t -> [(Name, t)] -> Err' t
UnifyScope Name
w Name
x a
y [(Name, a)]
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 a
x <- Get a
forall t. Binary t => Get t
get ; a
y <- Get a
forall t. Binary t => Get t
get
                     Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ a -> a -> Err' a
forall t. t -> t -> Err' t
NonFunctionType a
x a
y
             Word8
9 -> do a
x <- Get a
forall t. Binary t => Get t
get ; a
y <- Get a
forall t. Binary t => Get t
get
                     Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ a -> a -> Err' a
forall t. t -> t -> Err' t
NotEquality a
x a
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 a
x <- Get a
forall t. Binary t => Get t
get ; a
y <- Get a
forall t. Binary t => Get t
get ; a
z <- Get a
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> Err' a
forall t. t -> t -> t -> Err' t
NotInjective a
x a
y a
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 Universe
x <- Get Universe
forall t. Binary t => Get t
get ; Name
y <- Get Name
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ Universe -> Name -> Err' a
forall t. Universe -> Name -> Err' t
UniqueError Universe
x Name
y
             Word8
20 -> do Universe
x <- Get Universe
forall t. Binary t => Get t
get ; Name
y <- Get Name
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ Universe -> Name -> Err' a
forall t. Universe -> Name -> Err' t
UniqueKindError Universe
x Name
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 a
l <- Get a
forall t. Binary t => Get t
get; a
r <- Get a
forall t. Binary t => Get t
get; a
t <- Get a
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> Err' a
forall t. t -> t -> t -> Err' t
NoRewriting a
l a
r a
t
             Word8
27 -> do FC
x <- Get FC
forall t. Binary t => Get t
get ; Err' a
y <- Get (Err' a)
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ FC -> Err' a -> Err' a
forall t. FC -> Err' t -> Err' t
At FC
x Err' a
y
             Word8
28 -> do String
w <- Get String
forall t. Binary t => Get t
get; Name
x <- Get Name
forall t. Binary t => Get t
get ; Maybe a
y <- Get (Maybe a)
forall t. Binary t => Get t
get ; Err' a
z <- Get (Err' a)
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ String -> Name -> Maybe a -> Err' a -> Err' a
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
w Name
x Maybe a
y Err' a
z
             Word8
29 -> do Name
w <- Get Name
forall t. Binary t => Get t
get ; Name
x <- Get Name
forall t. Binary t => Get t
get ; [(Name, Name)]
y <- Get [(Name, Name)]
forall t. Binary t => Get t
get ; Err' a
z <- Get (Err' a)
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ Name -> Name -> [(Name, Name)] -> Err' a -> Err' a
forall t. Name -> Name -> [(Name, Name)] -> Err' t -> Err' t
ElaboratingArg Name
w Name
x [(Name, Name)]
y Err' a
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 String
x <- Get String
forall t. Binary t => Get t
get ; Err' a
y <- Get (Err' a)
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ String -> Err' a -> Err' a
forall t. String -> Err' t -> Err' t
LoadingFailed String
x Err' a
y
             Word8
32 -> do [[ErrorReportPart]]
x <- Get [[ErrorReportPart]]
forall t. Binary t => Get t
get ; Err' a
y <- Get (Err' a)
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ [[ErrorReportPart]] -> Err' a -> Err' a
forall t. [[ErrorReportPart]] -> Err' t -> Err' t
ReflectionError [[ErrorReportPart]]
x Err' a
y
             Word8
33 -> do String
x <- Get String
forall t. Binary t => Get t
get ; Err' a
y <- Get (Err' a)
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ String -> Err' a -> Err' a
forall t. String -> Err' t -> Err' t
ReflectionFailed String
x Err' a
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 [ErrorReportPart]
x1 <- Get [ErrorReportPart]
forall t. Binary t => Get t
get
                      a
x2 <- Get a
forall t. Binary t => Get t
get
                      [(Name, a, [(Name, Binder a)])]
x3 <- Get [(Name, a, [(Name, Binder a)])]
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ErrorReportPart] -> a -> [(Name, a, [(Name, Binder a)])] -> Err' a
forall t.
[ErrorReportPart] -> t -> [(Name, t, [(Name, Binder t)])] -> Err' t
ElabScriptDebug [ErrorReportPart]
x1 a
x2 [(Name, a, [(Name, Binder a)])]
x3)
             Word8
38 -> do Name
x1 <- Get Name
forall t. Binary t => Get t
get
                      a
x2 <- Get a
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> a -> Err' a
forall t. Name -> t -> Err' t
InvalidTCArg Name
x1 a
x2)
             Word8
39 -> do a
x1 <- Get a
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Err' a
forall t. t -> Err' t
ElabScriptStuck a
x1)
             Word8
40 -> do Name
x <- Get Name
forall t. Binary t => Get t
get ; Name
y <- Get Name
forall t. Binary t => Get t
get
                      Err' a -> Get (Err' a)
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Err' a -> Get (Err' a)) -> Err' a -> Get (Err' a)
forall a b. (a -> b) -> a -> b
$ Name -> Name -> Err' a
forall t. Name -> Name -> Err' t
UnknownImplicit Name
x Name
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 Word8
i <- Get Word8
getWord8
               case Word8
i of
                   Word8
0 -> do Int
x1 <- Get Int
forall t. Binary t => Get t
get
                           Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Const
I Int
x1)
                   Word8
1 -> do Integer
x1 <- Get Integer
forall t. Binary t => Get t
get
                           Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Const
BI Integer
x1)
                   Word8
2 -> do Double
x1 <- Get Double
getDoublele
                           Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Double -> Const
Fl Double
x1)
                   Word8
3 -> do Char
x1 <- Get Char
forall t. Binary t => Get t
get
                           Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Char -> Const
Ch Char
x1)
                   Word8
4 -> do String
x1 <- Get String
forall t. Binary t => Get t
get
                           Const -> Get Const
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Const
Str String
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 Bool
x1 <- Get Bool
forall t. Binary t => Get t
get
               Bool
x2 <- Get Bool
forall t. Binary t => Get t
get
               ImplicitInfo -> Get ImplicitInfo
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Bool -> Bool -> ImplicitInfo
Impl Bool
x1 Bool
x2 Bool
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 Word8
i <- Get Word8
getWord8
               case Word8
i of
                   Word8
0 -> do NameType
x1 <- Get NameType
forall t. Binary t => Get t
get
                           Name
x2 <- Get Name
forall t. Binary t => Get t
get
--                            x3 <- get
                           Term -> Get Term
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
x1 Name
x2 Term
forall n. TT n
Erased)
                   Word8
1 -> do Word8
x1 <- Get Word8
getWord8
                           Term -> Get Term
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Term
forall n. Int -> TT n
V ((Word8 -> Int
forall a. Enum a => a -> Int
fromEnum Word8
x1) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
                   Word8
2 -> do Name
x1 <- Get Name
forall t. Binary t => Get t
get
                           Binder Term
x2 <- Get (Binder Term)
forall t. Binary t => Get t
get
                           Term
x3 <- Get Term
forall t. Binary t => Get t
get
                           Term -> Get Term
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x1 Binder Term
x2 Term
x3)
                   Word8
3 -> do Term
x1 <- Get Term
forall t. Binary t => Get t
get
                           Term
x2 <- Get Term
forall t. Binary t => Get t
get
                           Term -> Get Term
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete Term
x1 Term
x2)
                   Word8
4 -> do Const
x1 <- Get Const
forall t. Binary t => Get t
get
                           Term -> Get Term
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> Term
forall n. Const -> TT n
Constant Const
x1)
                   Word8
5 -> do Term
x1 <- Get Term
forall t. Binary t => Get t
get
                           Word8
x2 <- Get Word8
getWord8
                           Term -> Get Term
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Int -> Term
forall n. TT n -> Int -> TT n
Proj Term
x1 ((Word8 -> Int
forall a. Enum a => a -> Int
fromEnum Word8
x2)Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
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 UExp
x1 <- Get UExp
forall t. Binary t => Get t
get
                           Term -> Get Term
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> Term
forall n. UExp -> TT n
TType UExp
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 Int
x1 <- Get Int
forall t. Binary t => Get t
get
                           Term -> Get Term
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Term
forall n. Int -> TT n
V Int
x1)
                   Word8
10 -> do Universe
x1 <- Get Universe
forall t. Binary t => Get t
get
                            Term -> Get Term
forall a. a -> Get a
forall (m :: * -> *) a. Monad m => a -> m a
return (Universe -> Term
forall n. Universe -> TT n
UType Universe
x1)
                   Word8
_ -> String -> Get Term
forall a. HasCallStack => String -> a
error String
"Corrupted binary data for TT"