{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.TypeChecking.Serialise.Instances () where
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Serialise.Base
import Agda.TypeChecking.Serialise.Instances.Highlighting ()
import Agda.TypeChecking.Serialise.Instances.Errors ()
instance EmbPrj Interface where
icod_ :: Interface -> S Int32
icod_ (Interface a :: Hash
a b :: Text
b c :: FileType
c d :: [(ModuleName, Hash)]
d e :: ModuleName
e f :: Map ModuleName Scope
f g :: ScopeInfo
g h :: Signature
h i :: DisplayForms
i j :: Map QName String
j k :: Maybe String
k l :: BuiltinThings (String, QName)
l m :: Map String [ForeignCode]
m n :: HighlightingInfo
n o :: [OptionsPragma]
o p :: PragmaOptions
p q :: PatternSynDefns
q r :: [TCWarning]
r s :: Set QName
s) =
(Hash
-> Text
-> FileType
-> [(ModuleName, Hash)]
-> ModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> DisplayForms
-> Map QName String
-> Maybe String
-> BuiltinThings (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Interface)
-> Hash
-> Text
-> FileType
-> [(ModuleName, Hash)]
-> ModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> DisplayForms
-> Map QName String
-> Maybe String
-> BuiltinThings (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Hash
-> Text
-> FileType
-> [(ModuleName, Hash)]
-> ModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> DisplayForms
-> Map QName String
-> Maybe String
-> BuiltinThings (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Interface
Interface Hash
a Text
b FileType
c [(ModuleName, Hash)]
d ModuleName
e Map ModuleName Scope
f ScopeInfo
g Signature
h DisplayForms
i Map QName String
j Maybe String
k BuiltinThings (String, QName)
l Map String [ForeignCode]
m HighlightingInfo
n [OptionsPragma]
o PragmaOptions
p PatternSynDefns
q [TCWarning]
r Set QName
s
value :: Int32 -> R Interface
value = (Node -> R Interface) -> Int32 -> R Interface
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Interface
valu where
valu :: Node -> R Interface
valu [a :: Int32
a, b :: Int32
b, c :: Int32
c, d :: Int32
d, e :: Int32
e, f :: Int32
f, g :: Int32
g, h :: Int32
h, i :: Int32
i, j :: Int32
j, k :: Int32
k, l :: Int32
l, m :: Int32
m, n :: Int32
n, o :: Int32
o, p :: Int32
p, q :: Int32
q, r :: Int32
r, s :: Int32
s] =
(Hash
-> Text
-> FileType
-> [(ModuleName, Hash)]
-> ModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> DisplayForms
-> Map QName String
-> Maybe String
-> BuiltinThings (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Interface)
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> Int32
-> R Interface
forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Hash
-> Text
-> FileType
-> [(ModuleName, Hash)]
-> ModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> DisplayForms
-> Map QName String
-> Maybe String
-> BuiltinThings (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Interface
Interface Int32
a Int32
b Int32
c Int32
d Int32
e Int32
f Int32
g Int32
h Int32
i Int32
j Int32
k Int32
l Int32
m Int32
n Int32
o Int32
p Int32
q Int32
r Int32
s
valu _ = R Interface
forall a. R a
malformed