{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.TypeChecking.Serialise.Instances () where
import Agda.Syntax.Position
import Agda.Syntax.TopLevelModuleName
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Serialise.Base
import Agda.TypeChecking.Serialise.Instances.Common (SerialisedRange(..))
import Agda.TypeChecking.Serialise.Instances.Highlighting ()
import Agda.TypeChecking.Serialise.Instances.Errors ()
import Agda.Utils.Hash
type RangedImportedModules =
[(SerialisedRange, TopLevelModuleName, Hash)]
fromImportedModules ::
[(TopLevelModuleName, Hash)] -> RangedImportedModules
fromImportedModules :: [(TopLevelModuleName, Hash)] -> RangedImportedModules
fromImportedModules [(TopLevelModuleName, Hash)]
ms = [(Range -> SerialisedRange
SerialisedRange (Range -> SerialisedRange) -> Range -> SerialisedRange
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> Range
forall a. HasRange a => a -> Range
getRange TopLevelModuleName
x, TopLevelModuleName
x, Hash
hash) | (TopLevelModuleName
x, Hash
hash) <- [(TopLevelModuleName, Hash)]
ms]
toImportedModules ::
RangedImportedModules -> [(TopLevelModuleName, Hash)]
toImportedModules :: RangedImportedModules -> [(TopLevelModuleName, Hash)]
toImportedModules RangedImportedModules
ms = [(Range -> TopLevelModuleName -> TopLevelModuleName
forall a. SetRange a => Range -> a -> a
setRange (SerialisedRange -> Range
underlyingRange SerialisedRange
r) TopLevelModuleName
x, Hash
hash) | (SerialisedRange
r, TopLevelModuleName
x, Hash
hash) <- RangedImportedModules
ms]
instance EmbPrj Interface where
icod_ :: Interface -> S Int32
icod_ (Interface Hash
a Text
b FileType
c [(TopLevelModuleName, Hash)]
d ModuleName
e TopLevelModuleName
f Map ModuleName Scope
g ScopeInfo
h Signature
i RemoteMetaStore
j DisplayForms
k Map QName Text
l Maybe Text
m BuiltinThings (PrimitiveId, QName)
n Map BackendName ForeignCodeStack
o HighlightingInfo
p [OptionsPragma]
q [OptionsPragma]
r PragmaOptions
s PatternSynDefns
t [TCWarning]
u Set QName
v Map OpaqueId OpaqueBlock
w Map QName OpaqueId
x) =
(Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface)
-> Arrows
(Domains
(Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface))
(S Int32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
interface Hash
a Text
b FileType
c ([(TopLevelModuleName, Hash)] -> RangedImportedModules
fromImportedModules [(TopLevelModuleName, Hash)]
d) ModuleName
e TopLevelModuleName
f Map ModuleName Scope
g ScopeInfo
h Signature
i RemoteMetaStore
j DisplayForms
k Map QName Text
l Maybe Text
m BuiltinThings (PrimitiveId, QName)
n Map BackendName ForeignCodeStack
o HighlightingInfo
p [OptionsPragma]
q [OptionsPragma]
r PragmaOptions
s PatternSynDefns
t [TCWarning]
u Set QName
v Map OpaqueId OpaqueBlock
w Map QName OpaqueId
x
where interface :: Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
interface Hash
a Text
b FileType
c = Hash
-> Text
-> FileType
-> [(TopLevelModuleName, Hash)]
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
Interface Hash
a Text
b FileType
c ([(TopLevelModuleName, Hash)]
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface)
-> (RangedImportedModules -> [(TopLevelModuleName, Hash)])
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangedImportedModules -> [(TopLevelModuleName, Hash)]
toImportedModules
value :: Int32 -> R Interface
value = (Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface)
-> Int32
-> R (CoDomain
(Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
interface
where interface :: Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
interface Hash
a Text
b FileType
c = Hash
-> Text
-> FileType
-> [(TopLevelModuleName, Hash)]
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
Interface Hash
a Text
b FileType
c ([(TopLevelModuleName, Hash)]
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface)
-> (RangedImportedModules -> [(TopLevelModuleName, Hash)])
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (PrimitiveId, QName)
-> Map BackendName ForeignCodeStack
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangedImportedModules -> [(TopLevelModuleName, Hash)]
toImportedModules