{-# 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.Errors ()
import Agda.TypeChecking.Serialise.Instances.General ()
import Agda.TypeChecking.Serialise.Instances.Highlighting ()
import Agda.Utils.Hash

type RangedImportedModules =
  [(SerialisedRange, TopLevelModuleName, Hash)]

fromImportedModules ::
  [(TopLevelModuleName, Hash)] -> RangedImportedModules
fromImportedModules :: [(TopLevelModuleName' Range, Hash)] -> RangedImportedModules
fromImportedModules [(TopLevelModuleName' Range, Hash)]
ms = [(Range -> SerialisedRange
SerialisedRange (Range -> SerialisedRange) -> Range -> SerialisedRange
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName' Range -> Range
forall a. HasRange a => a -> Range
getRange TopLevelModuleName' Range
x, TopLevelModuleName' Range
x, Hash
hash) | (TopLevelModuleName' Range
x, Hash
hash) <- [(TopLevelModuleName' Range, Hash)]
ms]

toImportedModules ::
  RangedImportedModules -> [(TopLevelModuleName, Hash)]
toImportedModules :: RangedImportedModules -> [(TopLevelModuleName' Range, Hash)]
toImportedModules RangedImportedModules
ms = [(Range -> TopLevelModuleName' Range -> TopLevelModuleName' Range
forall a. SetRange a => Range -> a -> a
setRange (SerialisedRange -> Range
underlyingRange SerialisedRange
r) TopLevelModuleName' Range
x, Hash
hash) | (SerialisedRange
r, TopLevelModuleName' Range
x, Hash
hash) <- RangedImportedModules
ms]

instance EmbPrj Interface where
  icod_ :: Interface -> S Word32
icod_ (Interface Hash
a Text
b FileType
c [(TopLevelModuleName' Range, Hash)]
d ModuleName
e TopLevelModuleName' Range
f Map ModuleName Scope
g ScopeInfo
h Signature
i HashMap MetaId RemoteMetaVariable
j HashMap QName (List1 LocalDisplayForm)
k Map QName Text
l Maybe Text
m Map SomeBuiltin (Builtin (PrimitiveId, QName))
n Map Text ForeignCodeStack
o RangeMap Aspects
p [OptionsPragma]
q [OptionsPragma]
r PragmaOptions
s Map QName PatternSynDefn
t Set TCWarning
u Set QName
v Map OpaqueId OpaqueBlock
w Map QName OpaqueId
x) =
      (Hash
 -> Text
 -> FileType
 -> RangedImportedModules
 -> ModuleName
 -> TopLevelModuleName' Range
 -> Map ModuleName Scope
 -> ScopeInfo
 -> Signature
 -> HashMap MetaId RemoteMetaVariable
 -> HashMap QName (List1 LocalDisplayForm)
 -> Map QName Text
 -> Maybe Text
 -> Map SomeBuiltin (Builtin (PrimitiveId, QName))
 -> Map Text ForeignCodeStack
 -> RangeMap Aspects
 -> [OptionsPragma]
 -> [OptionsPragma]
 -> PragmaOptions
 -> Map QName PatternSynDefn
 -> Set TCWarning
 -> Set QName
 -> Map OpaqueId OpaqueBlock
 -> Map QName OpaqueId
 -> Interface)
-> Arrows
     (Domains
        (Hash
         -> Text
         -> FileType
         -> RangedImportedModules
         -> ModuleName
         -> TopLevelModuleName' Range
         -> Map ModuleName Scope
         -> ScopeInfo
         -> Signature
         -> HashMap MetaId RemoteMetaVariable
         -> HashMap QName (List1 LocalDisplayForm)
         -> Map QName Text
         -> Maybe Text
         -> Map SomeBuiltin (Builtin (PrimitiveId, QName))
         -> Map Text ForeignCodeStack
         -> RangeMap Aspects
         -> [OptionsPragma]
         -> [OptionsPragma]
         -> PragmaOptions
         -> Map QName PatternSynDefn
         -> Set TCWarning
         -> Set QName
         -> Map OpaqueId OpaqueBlock
         -> Map QName OpaqueId
         -> Interface))
     (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName' Range
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> HashMap MetaId RemoteMetaVariable
-> HashMap QName (List1 LocalDisplayForm)
-> Map QName Text
-> Maybe Text
-> Map SomeBuiltin (Builtin (PrimitiveId, QName))
-> Map Text ForeignCodeStack
-> RangeMap Aspects
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> Map QName PatternSynDefn
-> Set TCWarning
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
interface Hash
a Text
b FileType
c ([(TopLevelModuleName' Range, Hash)] -> RangedImportedModules
fromImportedModules [(TopLevelModuleName' Range, Hash)]
d) ModuleName
e TopLevelModuleName' Range
f Map ModuleName Scope
g ScopeInfo
h Signature
i HashMap MetaId RemoteMetaVariable
j HashMap QName (List1 LocalDisplayForm)
k Map QName Text
l Maybe Text
m Map SomeBuiltin (Builtin (PrimitiveId, QName))
n Map Text ForeignCodeStack
o RangeMap Aspects
p [OptionsPragma]
q [OptionsPragma]
r PragmaOptions
s Map QName PatternSynDefn
t Set TCWarning
u Set QName
v Map OpaqueId OpaqueBlock
w Map QName OpaqueId
x
    where interface :: Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName' Range
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> HashMap MetaId RemoteMetaVariable
-> HashMap QName (List1 LocalDisplayForm)
-> Map QName Text
-> Maybe Text
-> Map SomeBuiltin (Builtin (PrimitiveId, QName))
-> Map Text ForeignCodeStack
-> RangeMap Aspects
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> Map QName PatternSynDefn
-> Set TCWarning
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
interface Hash
a Text
b FileType
c = Hash
-> Text
-> FileType
-> [(TopLevelModuleName' Range, Hash)]
-> ModuleName
-> TopLevelModuleName' Range
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> HashMap MetaId RemoteMetaVariable
-> HashMap QName (List1 LocalDisplayForm)
-> Map QName Text
-> Maybe Text
-> Map SomeBuiltin (Builtin (PrimitiveId, QName))
-> Map Text ForeignCodeStack
-> RangeMap Aspects
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> Map QName PatternSynDefn
-> Set TCWarning
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
Interface Hash
a Text
b FileType
c ([(TopLevelModuleName' Range, Hash)]
 -> ModuleName
 -> TopLevelModuleName' Range
 -> Map ModuleName Scope
 -> ScopeInfo
 -> Signature
 -> HashMap MetaId RemoteMetaVariable
 -> HashMap QName (List1 LocalDisplayForm)
 -> Map QName Text
 -> Maybe Text
 -> Map SomeBuiltin (Builtin (PrimitiveId, QName))
 -> Map Text ForeignCodeStack
 -> RangeMap Aspects
 -> [OptionsPragma]
 -> [OptionsPragma]
 -> PragmaOptions
 -> Map QName PatternSynDefn
 -> Set TCWarning
 -> Set QName
 -> Map OpaqueId OpaqueBlock
 -> Map QName OpaqueId
 -> Interface)
-> (RangedImportedModules -> [(TopLevelModuleName' Range, Hash)])
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName' Range
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> HashMap MetaId RemoteMetaVariable
-> HashMap QName (List1 LocalDisplayForm)
-> Map QName Text
-> Maybe Text
-> Map SomeBuiltin (Builtin (PrimitiveId, QName))
-> Map Text ForeignCodeStack
-> RangeMap Aspects
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> Map QName PatternSynDefn
-> Set TCWarning
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangedImportedModules -> [(TopLevelModuleName' Range, Hash)]
toImportedModules

  value :: Word32 -> R Interface
value = (Hash
 -> Text
 -> FileType
 -> RangedImportedModules
 -> ModuleName
 -> TopLevelModuleName' Range
 -> Map ModuleName Scope
 -> ScopeInfo
 -> Signature
 -> HashMap MetaId RemoteMetaVariable
 -> HashMap QName (List1 LocalDisplayForm)
 -> Map QName Text
 -> Maybe Text
 -> Map SomeBuiltin (Builtin (PrimitiveId, QName))
 -> Map Text ForeignCodeStack
 -> RangeMap Aspects
 -> [OptionsPragma]
 -> [OptionsPragma]
 -> PragmaOptions
 -> Map QName PatternSynDefn
 -> Set TCWarning
 -> Set QName
 -> Map OpaqueId OpaqueBlock
 -> Map QName OpaqueId
 -> Interface)
-> Word32
-> R (CoDomain
        (Hash
         -> Text
         -> FileType
         -> RangedImportedModules
         -> ModuleName
         -> TopLevelModuleName' Range
         -> Map ModuleName Scope
         -> ScopeInfo
         -> Signature
         -> HashMap MetaId RemoteMetaVariable
         -> HashMap QName (List1 LocalDisplayForm)
         -> Map QName Text
         -> Maybe Text
         -> Map SomeBuiltin (Builtin (PrimitiveId, QName))
         -> Map Text ForeignCodeStack
         -> RangeMap Aspects
         -> [OptionsPragma]
         -> [OptionsPragma]
         -> PragmaOptions
         -> Map QName PatternSynDefn
         -> Set TCWarning
         -> Set QName
         -> Map OpaqueId OpaqueBlock
         -> Map QName OpaqueId
         -> Interface))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName' Range
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> HashMap MetaId RemoteMetaVariable
-> HashMap QName (List1 LocalDisplayForm)
-> Map QName Text
-> Maybe Text
-> Map SomeBuiltin (Builtin (PrimitiveId, QName))
-> Map Text ForeignCodeStack
-> RangeMap Aspects
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> Map QName PatternSynDefn
-> Set TCWarning
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
interface
    where interface :: Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName' Range
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> HashMap MetaId RemoteMetaVariable
-> HashMap QName (List1 LocalDisplayForm)
-> Map QName Text
-> Maybe Text
-> Map SomeBuiltin (Builtin (PrimitiveId, QName))
-> Map Text ForeignCodeStack
-> RangeMap Aspects
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> Map QName PatternSynDefn
-> Set TCWarning
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
interface Hash
a Text
b FileType
c = Hash
-> Text
-> FileType
-> [(TopLevelModuleName' Range, Hash)]
-> ModuleName
-> TopLevelModuleName' Range
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> HashMap MetaId RemoteMetaVariable
-> HashMap QName (List1 LocalDisplayForm)
-> Map QName Text
-> Maybe Text
-> Map SomeBuiltin (Builtin (PrimitiveId, QName))
-> Map Text ForeignCodeStack
-> RangeMap Aspects
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> Map QName PatternSynDefn
-> Set TCWarning
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
Interface Hash
a Text
b FileType
c ([(TopLevelModuleName' Range, Hash)]
 -> ModuleName
 -> TopLevelModuleName' Range
 -> Map ModuleName Scope
 -> ScopeInfo
 -> Signature
 -> HashMap MetaId RemoteMetaVariable
 -> HashMap QName (List1 LocalDisplayForm)
 -> Map QName Text
 -> Maybe Text
 -> Map SomeBuiltin (Builtin (PrimitiveId, QName))
 -> Map Text ForeignCodeStack
 -> RangeMap Aspects
 -> [OptionsPragma]
 -> [OptionsPragma]
 -> PragmaOptions
 -> Map QName PatternSynDefn
 -> Set TCWarning
 -> Set QName
 -> Map OpaqueId OpaqueBlock
 -> Map QName OpaqueId
 -> Interface)
-> (RangedImportedModules -> [(TopLevelModuleName' Range, Hash)])
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName' Range
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> HashMap MetaId RemoteMetaVariable
-> HashMap QName (List1 LocalDisplayForm)
-> Map QName Text
-> Maybe Text
-> Map SomeBuiltin (Builtin (PrimitiveId, QName))
-> Map Text ForeignCodeStack
-> RangeMap Aspects
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> Map QName PatternSynDefn
-> Set TCWarning
-> Set QName
-> Map OpaqueId OpaqueBlock
-> Map QName OpaqueId
-> Interface
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangedImportedModules -> [(TopLevelModuleName' Range, Hash)]
toImportedModules