{-# 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'"
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))
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
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
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
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"