{-# 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 (String, QName)
n Map String [ForeignCode]
o HighlightingInfo
p [OptionsPragma]
q [OptionsPragma]
r PragmaOptions
s PatternSynDefns
t [TCWarning]
u Set QName
v) =
      (Hash
 -> Text
 -> FileType
 -> RangedImportedModules
 -> ModuleName
 -> TopLevelModuleName
 -> Map ModuleName Scope
 -> ScopeInfo
 -> Signature
 -> RemoteMetaStore
 -> DisplayForms
 -> Map QName Text
 -> Maybe Text
 -> BuiltinThings (String, QName)
 -> Map String [ForeignCode]
 -> HighlightingInfo
 -> [OptionsPragma]
 -> [OptionsPragma]
 -> PragmaOptions
 -> PatternSynDefns
 -> [TCWarning]
 -> Set QName
 -> Interface)
-> Arrows
     (Domains
        (Hash
         -> Text
         -> FileType
         -> RangedImportedModules
         -> ModuleName
         -> TopLevelModuleName
         -> Map ModuleName Scope
         -> ScopeInfo
         -> Signature
         -> RemoteMetaStore
         -> DisplayForms
         -> Map QName Text
         -> Maybe Text
         -> BuiltinThings (String, QName)
         -> Map String [ForeignCode]
         -> HighlightingInfo
         -> [OptionsPragma]
         -> [OptionsPragma]
         -> PragmaOptions
         -> PatternSynDefns
         -> [TCWarning]
         -> Set QName
         -> 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 (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> 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 (String, QName)
n Map String [ForeignCode]
o HighlightingInfo
p [OptionsPragma]
q [OptionsPragma]
r PragmaOptions
s PatternSynDefns
t [TCWarning]
u Set QName
v
    where interface :: Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> 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 (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> 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 (String, QName)
 -> Map String [ForeignCode]
 -> HighlightingInfo
 -> [OptionsPragma]
 -> [OptionsPragma]
 -> PragmaOptions
 -> PatternSynDefns
 -> [TCWarning]
 -> Set QName
 -> Interface)
-> (RangedImportedModules -> [(TopLevelModuleName, Hash)])
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Interface
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangedImportedModules -> [(TopLevelModuleName, Hash)]
toImportedModules

  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 [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, Int32
t, Int32
u, Int32
v] =
        (Hash
 -> Text
 -> FileType
 -> RangedImportedModules
 -> ModuleName
 -> TopLevelModuleName
 -> Map ModuleName Scope
 -> ScopeInfo
 -> Signature
 -> RemoteMetaStore
 -> DisplayForms
 -> Map QName Text
 -> Maybe Text
 -> BuiltinThings (String, QName)
 -> Map String [ForeignCode]
 -> HighlightingInfo
 -> [OptionsPragma]
 -> [OptionsPragma]
 -> PragmaOptions
 -> PatternSynDefns
 -> [TCWarning]
 -> Set QName
 -> Interface)
-> Arrows
     (Constant
        Int32
        (Domains
           (Hash
            -> Text
            -> FileType
            -> RangedImportedModules
            -> ModuleName
            -> TopLevelModuleName
            -> Map ModuleName Scope
            -> ScopeInfo
            -> Signature
            -> RemoteMetaStore
            -> DisplayForms
            -> Map QName Text
            -> Maybe Text
            -> BuiltinThings (String, QName)
            -> Map String [ForeignCode]
            -> HighlightingInfo
            -> [OptionsPragma]
            -> [OptionsPragma]
            -> PragmaOptions
            -> PatternSynDefns
            -> [TCWarning]
            -> Set QName
            -> Interface)))
     (R (CoDomain
           (Hash
            -> Text
            -> FileType
            -> RangedImportedModules
            -> ModuleName
            -> TopLevelModuleName
            -> Map ModuleName Scope
            -> ScopeInfo
            -> Signature
            -> RemoteMetaStore
            -> DisplayForms
            -> Map QName Text
            -> Maybe Text
            -> BuiltinThings (String, QName)
            -> Map String [ForeignCode]
            -> HighlightingInfo
            -> [OptionsPragma]
            -> [OptionsPragma]
            -> PragmaOptions
            -> PatternSynDefns
            -> [TCWarning]
            -> Set QName
            -> 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
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> [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 Int32
t Int32
u Int32
v
      where interface :: Hash
-> Text
-> FileType
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> 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 (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> 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 (String, QName)
 -> Map String [ForeignCode]
 -> HighlightingInfo
 -> [OptionsPragma]
 -> [OptionsPragma]
 -> PragmaOptions
 -> PatternSynDefns
 -> [TCWarning]
 -> Set QName
 -> Interface)
-> (RangedImportedModules -> [(TopLevelModuleName, Hash)])
-> RangedImportedModules
-> ModuleName
-> TopLevelModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> RemoteMetaStore
-> DisplayForms
-> Map QName Text
-> Maybe Text
-> BuiltinThings (String, QName)
-> Map String [ForeignCode]
-> HighlightingInfo
-> [OptionsPragma]
-> [OptionsPragma]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Interface
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangedImportedModules -> [(TopLevelModuleName, Hash)]
toImportedModules
    valu Node
_ = R Interface
forall a. R a
malformed