{-# LANGUAGE FlexibleInstances #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module Idris.Core.Binary where
import Idris.Core.TT
import Control.Applicative ((<$>), (<*>))
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 str :: String
str) = do Word8 -> Put
putWord8 0
String -> Put
forall t. Binary t => t -> Put
put String
str
put (InternalMsg str :: String
str) = do Word8 -> Put
putWord8 1
String -> Put
forall t. Binary t => t -> Put
put String
str
put (CantUnify x :: Bool
x y :: (a, Maybe Provenance)
y z :: (a, Maybe Provenance)
z e :: Err' a
e ctxt :: [(Name, a)]
ctxt i :: Int
i) = do Word8 -> Put
putWord8 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 n :: Name
n t :: a
t ctxt :: [(Name, a)]
ctxt) = do Word8 -> Put
putWord8 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 x :: a
x y :: a
y ctxt :: [(Name, a)]
ctxt) = do Word8 -> Put
putWord8 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 x :: a
x ctxt :: [(Name, a)]
ctxt) = do Word8 -> Put
putWord8 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 n1 :: Name
n1 n2 :: Name
n2 x :: a
x ctxt :: [(Name, a)]
ctxt) = do Word8 -> Put
putWord8 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 str :: String
str) = do Word8 -> Put
putWord8 7
String -> Put
forall t. Binary t => t -> Put
put String
str
put (NonFunctionType t1 :: a
t1 t2 :: a
t2) = do Word8 -> Put
putWord8 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 t1 :: a
t1 t2 :: a
t2) = do Word8 -> Put
putWord8 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 n :: Name
n) = do Word8 -> Put
putWord8 10
Name -> Put
forall t. Binary t => t -> Put
put Name
n
put (CantIntroduce t :: a
t) = do Word8 -> Put
putWord8 11
a -> Put
forall t. Binary t => t -> Put
put a
t
put (NoSuchVariable n :: Name
n) = do Word8 -> Put
putWord8 12
Name -> Put
forall t. Binary t => t -> Put
put Name
n
put (NoTypeDecl n :: Name
n) = do Word8 -> Put
putWord8 13
Name -> Put
forall t. Binary t => t -> Put
put Name
n
put (NotInjective x :: a
x y :: a
y z :: a
z) = do Word8 -> Put
putWord8 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 _ t :: a
t u :: Err' a
u) = do Word8 -> Put
putWord8 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 ns :: [Name]
ns) = do Word8 -> Put
putWord8 16
[Name] -> Put
forall t. Binary t => t -> Put
put [Name]
ns
put (IncompleteTerm t :: a
t) = do Word8 -> Put
putWord8 17
a -> Put
forall t. Binary t => t -> Put
put a
t
put (UniverseError x1 :: FC
x1 x2 :: UExp
x2 x3 :: (Int, Int)
x3 x4 :: (Int, Int)
x4 x5 :: [ConstraintFC]
x5) = do Word8 -> Put
putWord8 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 u :: Universe
u n :: Name
n) = do Word8 -> Put
putWord8 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 u :: Universe
u n :: Name
n) = do Word8 -> Put
putWord8 20
Universe -> Put
forall t. Binary t => t -> Put
put Universe
u
Name -> Put
forall t. Binary t => t -> Put
put Name
n
put ProgramLineComment = Word8 -> Put
putWord8 21
put (Inaccessible n :: Name
n) = do Word8 -> Put
putWord8 22
Name -> Put
forall t. Binary t => t -> Put
put Name
n
put (NonCollapsiblePostulate n :: Name
n) = do Word8 -> Put
putWord8 23
Name -> Put
forall t. Binary t => t -> Put
put Name
n
put (AlreadyDefined n :: Name
n) = do Word8 -> Put
putWord8 24
Name -> Put
forall t. Binary t => t -> Put
put Name
n
put (ProofSearchFail e :: Err' a
e) = do Word8 -> Put
putWord8 25
Err' a -> Put
forall t. Binary t => t -> Put
put Err' a
e
put (NoRewriting l :: a
l r :: a
r t :: a
t) = do Word8 -> Put
putWord8 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
fc e :: Err' a
e) = do Word8 -> Put
putWord8 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 str :: String
str n :: Name
n ty :: Maybe a
ty e :: Err' a
e) = do Word8 -> Put
putWord8 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 n1 :: Name
n1 n2 :: Name
n2 ns :: [(Name, Name)]
ns e :: Err' a
e) = do Word8 -> Put
putWord8 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 str :: String
str) = do Word8 -> Put
putWord8 30
String -> Put
forall t. Binary t => t -> Put
put String
str
put (LoadingFailed str :: String
str e :: Err' a
e) = do Word8 -> Put
putWord8 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 parts :: [[ErrorReportPart]]
parts e :: Err' a
e) = do Word8 -> Put
putWord8 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 str :: String
str e :: Err' a
e) = do Word8 -> Put
putWord8 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 t :: a
t) = do Word8 -> Put
putWord8 34
a -> Put
forall t. Binary t => t -> Put
put a
t
put (CantMatch t :: a
t) = do Word8 -> Put
putWord8 35
a -> Put
forall t. Binary t => t -> Put
put a
t
put (ElabScriptDebug x1 :: [ErrorReportPart]
x1 x2 :: a
x2 x3 :: [(Name, a, [(Name, Binder a)])]
x3) = do Word8 -> Put
putWord8 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 n :: Name
n t :: a
t) = do Word8 -> Put
putWord8 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 x1 :: a
x1) = do Word8 -> Put
putWord8 39
a -> Put
forall t. Binary t => t -> Put
put a
x1
put (UnknownImplicit n :: Name
n f :: Name
f) = do Word8 -> Put
putWord8 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 ns :: [Name]
ns) = do Word8 -> Put
putWord8 41
[Name] -> Put
forall t. Binary t => t -> Put
put [Name]
ns
put (RunningElabScript e :: Err' a
e) = do Word8 -> Put
putWord8 42
Err' a -> Put
forall t. Binary t => t -> Put
put Err' a
e
put (ElabScriptStaging n :: Name
n) = do Word8 -> Put
putWord8 43
Name -> Put
forall t. Binary t => t -> Put
put Name
n
put (FancyMsg xs :: [ErrorReportPart]
xs) = do Word8 -> Put
putWord8 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
0 -> (String -> Err' a) -> Get String -> Get (Err' a)
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
1 -> (String -> Err' a) -> Get String -> Get (Err' a)
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
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 (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
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 (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
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 (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
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 (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
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 (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
7 -> (String -> Err' a) -> Get String -> Get (Err' a)
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
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 (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
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 (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
10 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
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
11 -> (a -> Err' a) -> Get a -> Get (Err' a)
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
12 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
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
13 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
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
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 (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
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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get (Err' a)
forall t. Binary t => Get t
get
16 -> ([Name] -> Err' a) -> Get [Name] -> Get (Err' a)
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
17 -> (a -> Err' a) -> Get a -> Get (Err' a)
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
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 (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 (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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Get [ConstraintFC]
forall t. Binary t => Get t
get
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 (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
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 (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
21 -> Err' a -> Get (Err' a)
forall (m :: * -> *) a. Monad m => a -> m a
return Err' a
forall t. Err' t
ProgramLineComment
22 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
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
23 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
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
24 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
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
25 -> (Err' a -> Err' a) -> Get (Err' a) -> Get (Err' a)
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
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 (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
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 (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
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 (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
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 (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
30 -> (String -> Err' a) -> Get String -> Get (Err' a)
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
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 (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
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 (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
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 (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
34 -> (a -> Err' a) -> Get a -> Get (Err' a)
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
35 -> (a -> Err' a) -> Get a -> Get (Err' a)
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
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 (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)
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 (m :: * -> *) a. Monad m => a -> m a
return (Name -> a -> Err' a
forall t. Name -> t -> Err' t
InvalidTCArg Name
x1 a
x2)
39 -> do a
x1 <- Get a
forall t. Binary t => Get t
get
Err' a -> Get (Err' a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Err' a
forall t. t -> Err' t
ElabScriptStuck a
x1)
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 (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
41 -> ([Name] -> Err' a) -> Get [Name] -> Get (Err' a)
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
42 -> (Err' a -> Err' a) -> Get (Err' a) -> Get (Err' a)
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
43 -> (Name -> Err' a) -> Get Name -> Get (Err' a)
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
44 -> ([ErrorReportPart] -> Err' a)
-> Get [ErrorReportPart] -> Get (Err' a)
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
_ -> String -> Get (Err' a)
forall a. HasCallStack => String -> a
error "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 x :: Const
x
= case Const
x of
I x1 :: Int
x1 -> do Word8 -> Put
putWord8 0
Int -> Put
forall t. Binary t => t -> Put
put Int
x1
BI x1 :: Integer
x1 -> do Word8 -> Put
putWord8 1
Integer -> Put
forall t. Binary t => t -> Put
put Integer
x1
Fl x1 :: Double
x1 -> do Word8 -> Put
putWord8 2
Double -> Put
putDoublele Double
x1
Ch x1 :: Char
x1 -> do Word8 -> Put
putWord8 3
Char -> Put
forall t. Binary t => t -> Put
put Char
x1
Str x1 :: String
x1 -> do Word8 -> Put
putWord8 4
String -> Put
forall t. Binary t => t -> Put
put String
x1
B8 x1 :: Word8
x1 -> Word8 -> Put
putWord8 5 Put -> Put -> Put
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Word8 -> Put
forall t. Binary t => t -> Put
put Word8
x1
B16 x1 :: Word16
x1 -> Word8 -> Put
putWord8 6 Put -> Put -> Put
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Word16 -> Put
forall t. Binary t => t -> Put
put Word16
x1
B32 x1 :: Word32
x1 -> Word8 -> Put
putWord8 7 Put -> Put -> Put
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Word32 -> Put
forall t. Binary t => t -> Put
put Word32
x1
B64 x1 :: Word64
x1 -> Word8 -> Put
putWord8 8 Put -> Put -> Put
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 ITNative)) -> Word8 -> Put
putWord8 9
(AType (ATInt ITBig)) -> Word8 -> Put
putWord8 10
(AType ATFloat) -> Word8 -> Put
putWord8 11
(AType (ATInt ITChar)) -> Word8 -> Put
putWord8 12
StrType -> Word8 -> Put
putWord8 13
Forgot -> Word8 -> Put
putWord8 15
(AType (ATInt (ITFixed ity :: NativeTy
ity))) -> Word8 -> Put
putWord8 (Int -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (16 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ NativeTy -> Int
forall a. Enum a => a -> Int
fromEnum NativeTy
ity))
VoidType -> Word8 -> Put
putWord8 27
WorldType -> Word8 -> Put
putWord8 28
TheWorld -> Word8 -> Put
putWord8 29
get :: Get Const
get
= do Word8
i <- Get Word8
getWord8
case Word8
i of
0 -> do Int
x1 <- Get Int
forall t. Binary t => Get t
get
Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Const
I Int
x1)
1 -> do Integer
x1 <- Get Integer
forall t. Binary t => Get t
get
Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Const
BI Integer
x1)
2 -> do Double
x1 <- Get Double
getDoublele
Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (Double -> Const
Fl Double
x1)
3 -> do Char
x1 <- Get Char
forall t. Binary t => Get t
get
Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (Char -> Const
Ch Char
x1)
4 -> do String
x1 <- Get String
forall t. Binary t => Get t
get
Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Const
Str String
x1)
5 -> (Word8 -> Const) -> Get Word8 -> Get Const
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
6 -> (Word16 -> Const) -> Get Word16 -> Get Const
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
7 -> (Word32 -> Const) -> Get Word32 -> Get Const
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
8 -> (Word64 -> Const) -> Get Word64 -> Get Const
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
9 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITNative))
10 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITBig))
11 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType ArithTy
ATFloat)
12 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITChar))
13 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return Const
StrType
15 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return Const
Forgot
16 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT8)))
17 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT16)))
18 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT32)))
19 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT64)))
27 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return Const
VoidType
28 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return Const
WorldType
29 -> Const -> Get Const
forall (m :: * -> *) a. Monad m => a -> m a
return Const
TheWorld
_ -> String -> Get Const
forall a. HasCallStack => String -> a
error "Corrupted binary data for Const"
instance Binary Raw
instance Binary RigCount
instance Binary ImplicitInfo where
put :: ImplicitInfo -> Put
put x :: ImplicitInfo
x
= case ImplicitInfo
x of
Impl x1 :: Bool
x1 x2 :: Bool
x2 x3 :: 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 (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 :: TT Name -> Put
put x :: TT Name
x
= {-# SCC "putTT" #-}
case TT Name
x of
P x1 :: NameType
x1 x2 :: Name
x2 x3 :: TT Name
x3 -> do Word8 -> Put
putWord8 0
NameType -> Put
forall t. Binary t => t -> Put
put NameType
x1
Name -> Put
forall t. Binary t => t -> Put
put Name
x2
V x1 :: Int
x1 -> if (Int
x1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 Bool -> Bool -> Bool
&& Int
x1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 256)
then do Word8 -> Put
putWord8 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
+ 1))
else do Word8 -> Put
putWord8 9
Int -> Put
forall t. Binary t => t -> Put
put Int
x1
Bind x1 :: Name
x1 x2 :: Binder (TT Name)
x2 x3 :: TT Name
x3 -> do Word8 -> Put
putWord8 2
Name -> Put
forall t. Binary t => t -> Put
put Name
x1
Binder (TT Name) -> Put
forall t. Binary t => t -> Put
put Binder (TT Name)
x2
TT Name -> Put
forall t. Binary t => t -> Put
put TT Name
x3
App _ x1 :: TT Name
x1 x2 :: TT Name
x2 -> do Word8 -> Put
putWord8 3
TT Name -> Put
forall t. Binary t => t -> Put
put TT Name
x1
TT Name -> Put
forall t. Binary t => t -> Put
put TT Name
x2
Constant x1 :: Const
x1 -> do Word8 -> Put
putWord8 4
Const -> Put
forall t. Binary t => t -> Put
put Const
x1
Proj x1 :: TT Name
x1 x2 :: Int
x2 -> do Word8 -> Put
putWord8 5
TT Name -> Put
forall t. Binary t => t -> Put
put TT Name
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
+ 1))
Erased -> Word8 -> Put
putWord8 6
TType x1 :: UExp
x1 -> do Word8 -> Put
putWord8 7
UExp -> Put
forall t. Binary t => t -> Put
put UExp
x1
Impossible -> Word8 -> Put
putWord8 8
Inferred x1 :: TT Name
x1 -> TT Name -> Put
forall t. Binary t => t -> Put
put TT Name
x1
UType x1 :: Universe
x1 -> do Word8 -> Put
putWord8 10
Universe -> Put
forall t. Binary t => t -> Put
put Universe
x1
get :: Get (TT Name)
get
= do Word8
i <- Get Word8
getWord8
case Word8
i of
0 -> do NameType
x1 <- Get NameType
forall t. Binary t => Get t
get
Name
x2 <- Get Name
forall t. Binary t => Get t
get
TT Name -> Get (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
x1 Name
x2 TT Name
forall n. TT n
Erased)
1 -> do Word8
x1 <- Get Word8
getWord8
TT Name -> Get (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> TT Name
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
- 1))
2 -> do Name
x1 <- Get Name
forall t. Binary t => Get t
get
Binder (TT Name)
x2 <- Get (Binder (TT Name))
forall t. Binary t => Get t
get
TT Name
x3 <- Get (TT Name)
forall t. Binary t => Get t
get
TT Name -> Get (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
x1 Binder (TT Name)
x2 TT Name
x3)
3 -> do TT Name
x1 <- Get (TT Name)
forall t. Binary t => Get t
get
TT Name
x2 <- Get (TT Name)
forall t. Binary t => Get t
get
TT Name -> Get (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete TT Name
x1 TT Name
x2)
4 -> do Const
x1 <- Get Const
forall t. Binary t => Get t
get
TT Name -> Get (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> TT Name
forall n. Const -> TT n
Constant Const
x1)
5 -> do TT Name
x1 <- Get (TT Name)
forall t. Binary t => Get t
get
Word8
x2 <- Get Word8
getWord8
TT Name -> Get (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Int -> TT Name
forall n. TT n -> Int -> TT n
Proj TT Name
x1 ((Word8 -> Int
forall a. Enum a => a -> Int
fromEnum Word8
x2)Int -> Int -> Int
forall a. Num a => a -> a -> a
-1))
6 -> TT Name -> Get (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
forall n. TT n
Erased
7 -> do UExp
x1 <- Get UExp
forall t. Binary t => Get t
get
TT Name -> Get (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> TT Name
forall n. UExp -> TT n
TType UExp
x1)
8 -> TT Name -> Get (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
forall n. TT n
Impossible
9 -> do Int
x1 <- Get Int
forall t. Binary t => Get t
get
TT Name -> Get (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> TT Name
forall n. Int -> TT n
V Int
x1)
10 -> do Universe
x1 <- Get Universe
forall t. Binary t => Get t
get
TT Name -> Get (TT Name)
forall (m :: * -> *) a. Monad m => a -> m a
return (Universe -> TT Name
forall n. Universe -> TT n
UType Universe
x1)
_ -> String -> Get (TT Name)
forall a. HasCallStack => String -> a
error "Corrupted binary data for TT"