{-# OPTIONS_GHC -Wunused-imports #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

-- Only instances exported
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), Currying (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