{-|
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 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'"
----- Generated by 'derive'

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)) -- 16-19 inclusive
                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
--                                  put x3
                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 -- drop the 'Inferred'
                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
--                            x3 <- 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"