{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wunused-matches #-}
{-# OPTIONS_GHC -Wunused-binds #-}

module Agda.TypeChecking.Serialise.Instances.Common (SerialisedRange(..)) where

import qualified Control.Exception as E
import Control.Monad              ( (<$!>) )
import Control.Monad.IO.Class     ( MonadIO(..) )
import Control.Monad.State        ( runStateT )
import Control.Monad.Reader       ( asks )

import Agda.Syntax.Common
import Agda.Syntax.Builtin
import Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Concrete (RecordDirective(..))
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Position as P
import Agda.Syntax.Literal
import Agda.Syntax.TopLevelModuleName
import Agda.Interaction.FindFile
import Agda.Interaction.Library

import Agda.TypeChecking.Monad.Base.Types
import Agda.TypeChecking.Serialise.Base
import Agda.TypeChecking.Serialise.Instances.General ()

import Agda.Utils.FileId (getIdFile)
import Agda.Utils.Null

import Agda.Utils.IORef
import Agda.Utils.Impossible
import Agda.Utils.CallStack
import qualified Agda.Utils.HashTable as H
import qualified Agda.Utils.CompactRegion as Compact

instance EmbPrj ConstructorOrPatternSynonym

instance EmbPrj FileType where
  icod_ :: FileType -> S Word32
icod_ FileType
AgdaFileType  = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
0
  icod_ FileType
MdFileType    = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
1
  icod_ FileType
RstFileType   = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
2
  icod_ FileType
TexFileType   = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
3
  icod_ FileType
OrgFileType   = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
4
  icod_ FileType
TypstFileType = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
5
  icod_ FileType
TreeFileType  = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
6

  value :: Word32 -> R FileType
value = \case
    Word32
0 -> FileType -> R FileType
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FileType
AgdaFileType
    Word32
1 -> FileType -> R FileType
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FileType
MdFileType
    Word32
2 -> FileType -> R FileType
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FileType
RstFileType
    Word32
3 -> FileType -> R FileType
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FileType
TexFileType
    Word32
4 -> FileType -> R FileType
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FileType
OrgFileType
    Word32
5 -> FileType -> R FileType
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FileType
TypstFileType
    Word32
6 -> FileType -> R FileType
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FileType
TreeFileType
    Word32
_ -> R FileType
forall a. HasCallStack => R a
malformed

instance EmbPrj Cubical where
  icod_ :: Cubical -> S Word32
icod_ Cubical
CErased = Cubical -> Arrows (Domains Cubical) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN'  Cubical
CErased
  icod_ Cubical
CFull   = Word32 -> Cubical -> Arrows (Domains Cubical) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 Cubical
CFull

  value :: Word32 -> R Cubical
value = (Node -> R Cubical) -> Word32 -> R Cubical
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase ((Node -> R Cubical) -> Word32 -> R Cubical)
-> (Node -> R Cubical) -> Word32 -> R Cubical
forall a b. (a -> b) -> a -> b
$ \case
    Node
N0   -> Cubical
-> Arrows
     (Constant Word32 (Domains Cubical)) (R (CoDomain Cubical))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Cubical
CErased
    N1 Word32
0 -> Cubical
-> Arrows
     (Constant Word32 (Domains Cubical)) (R (CoDomain Cubical))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Cubical
CFull
    Node
_    -> R Cubical
forall a. HasCallStack => R a
malformed

instance EmbPrj Language where
  icod_ :: Language -> S Word32
icod_ Language
WithoutK    = Language -> Arrows (Domains Language) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN'  Language
WithoutK
  icod_ Language
WithK       = Word32 -> Language -> Arrows (Domains Language) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 Language
WithK
  icod_ (Cubical Cubical
a) = Word32
-> (Cubical -> Language)
-> Arrows (Domains (Cubical -> Language)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 Cubical -> Language
Cubical Cubical
a

  value :: Word32 -> R Language
value = (Node -> R Language) -> Word32 -> R Language
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase ((Node -> R Language) -> Word32 -> R Language)
-> (Node -> R Language) -> Word32 -> R Language
forall a b. (a -> b) -> a -> b
$ \case
    Node
N0     -> Language
-> Arrows
     (Constant Word32 (Domains Language)) (R (CoDomain Language))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Language
WithoutK
    N1 Word32
0   -> Language
-> Arrows
     (Constant Word32 (Domains Language)) (R (CoDomain Language))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Language
WithK
    N2 Word32
1 Word32
a -> (Cubical -> Language)
-> Arrows
     (Constant Word32 (Domains (Cubical -> Language)))
     (R (CoDomain (Cubical -> Language)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Cubical -> Language
Cubical Word32
a
    Node
_      -> R Language
forall a. HasCallStack => R a
malformed

instance EmbPrj a => EmbPrj (Position' a) where
  icod_ :: Position' a -> S Word32
icod_ (P.Pn a
file Word32
pos Word32
line Word32
col) = (a -> Word32 -> Word32 -> Word32 -> Position' a)
-> Arrows
     (Domains (a -> Word32 -> Word32 -> Word32 -> Position' a))
     (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' a -> Word32 -> Word32 -> Word32 -> Position' a
forall a. a -> Word32 -> Word32 -> Word32 -> Position' a
P.Pn a
file Word32
pos Word32
line Word32
col

  value :: Word32 -> R (Position' a)
value = (a -> Word32 -> Word32 -> Word32 -> Position' a)
-> Word32
-> R (CoDomain (a -> Word32 -> Word32 -> Word32 -> Position' a))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN a -> Word32 -> Word32 -> Word32 -> Position' a
forall a. a -> Word32 -> Word32 -> Word32 -> Position' a
P.Pn

instance EmbPrj TopLevelModuleName where
  icod_ :: TopLevelModuleName -> S Word32
icod_ (TopLevelModuleName Range
a ModuleNameHash
b TopLevelModuleNameParts
c Bool
d) = (Range
 -> ModuleNameHash
 -> TopLevelModuleNameParts
 -> Bool
 -> TopLevelModuleName)
-> Arrows
     (Domains
        (Range
         -> ModuleNameHash
         -> TopLevelModuleNameParts
         -> Bool
         -> TopLevelModuleName))
     (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Range
-> ModuleNameHash
-> TopLevelModuleNameParts
-> Bool
-> TopLevelModuleName
forall range.
range
-> ModuleNameHash
-> TopLevelModuleNameParts
-> Bool
-> TopLevelModuleName' range
TopLevelModuleName Range
a ModuleNameHash
b TopLevelModuleNameParts
c Bool
d

  value :: Word32 -> R TopLevelModuleName
value = (Range
 -> ModuleNameHash
 -> TopLevelModuleNameParts
 -> Bool
 -> TopLevelModuleName)
-> Word32
-> R (CoDomain
        (Range
         -> ModuleNameHash
         -> TopLevelModuleNameParts
         -> Bool
         -> TopLevelModuleName))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Range
-> ModuleNameHash
-> TopLevelModuleNameParts
-> Bool
-> TopLevelModuleName
forall range.
range
-> ModuleNameHash
-> TopLevelModuleNameParts
-> Bool
-> TopLevelModuleName' range
TopLevelModuleName

instance EmbPrj a => EmbPrj (P.Interval' a) where
  icod_ :: Interval' a -> S Word32
icod_ (P.Interval a
f PositionWithoutFile
p PositionWithoutFile
q) = (a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a)
-> Arrows
     (Domains
        (a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a))
     (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
forall a.
a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
P.Interval a
f PositionWithoutFile
p PositionWithoutFile
q

  value :: Word32 -> R (Interval' a)
value = (a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a)
-> Word32
-> R (CoDomain
        (a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
forall a.
a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
P.Interval

instance EmbPrj RangeFile where
  icod_ :: RangeFile -> S Word32
icod_ (RangeFile AbsolutePath
_ Maybe TopLevelModuleName
Nothing)  = S Word32
forall a. HasCallStack => a
__IMPOSSIBLE__
  icod_ (RangeFile AbsolutePath
_ (Just TopLevelModuleName
a)) = TopLevelModuleName -> S Word32
forall a. EmbPrj a => a -> S Word32
icode TopLevelModuleName
a

  value :: Word32 -> R RangeFile
value Word32
r = do
    !m :: TopLevelModuleName <- Word32 -> R TopLevelModuleName
forall a. EmbPrj a => Word32 -> R a
value Word32
r
    !mfref    <- asks modFile
    !mf       <- liftIO $ readIORef mfref
    !incs     <- asks includes
    (!r, !mf) <- liftIO $ runStateT (findFile'' incs m) mf
    liftIO $ writeIORef mfref mf
    case r of
      Left FindError
err ->
        IO RangeFile -> R RangeFile
forall a. IO a -> ReaderT Decode IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO RangeFile -> R RangeFile) -> IO RangeFile -> R RangeFile
forall a b. (a -> b) -> a -> b
$ ErrorCall -> IO RangeFile
forall e a. (HasCallStack, Exception e) => e -> IO a
E.throwIO (ErrorCall -> IO RangeFile) -> ErrorCall -> IO RangeFile
forall a b. (a -> b) -> a -> b
$ String -> ErrorCall
E.ErrorCall (String -> ErrorCall) -> String -> ErrorCall
forall a b. (a -> b) -> a -> b
$ String
"file not found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FindError -> String
forall a. Show a => a -> String
show FindError
err
      Right (SourceFile FileId
i) -> do
        let !fp :: AbsolutePath
fp = FileDictWithBuiltins -> FileId -> AbsolutePath
forall a. GetIdFile a => a -> FileId -> AbsolutePath
getIdFile (ModuleToSource -> FileDictWithBuiltins
fileDict ModuleToSource
mf) FileId
i
        !fpmemo <- (Decode -> HashTableLL AbsolutePath AbsolutePath)
-> ReaderT Decode IO (HashTableLL AbsolutePath AbsolutePath)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Decode -> HashTableLL AbsolutePath AbsolutePath
filePathMemo
        !arena  <- asks arena
        liftIO $ H.insertingIfAbsent fpmemo fp
          (\AbsolutePath
fp -> RangeFile -> IO RangeFile
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RangeFile -> IO RangeFile) -> RangeFile -> IO RangeFile
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
RangeFile AbsolutePath
fp (TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just TopLevelModuleName
m))
          (Compact.add arena fp)
          (\AbsolutePath
fp -> RangeFile -> IO RangeFile
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RangeFile -> IO RangeFile) -> RangeFile -> IO RangeFile
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
RangeFile AbsolutePath
fp (TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just TopLevelModuleName
m))

-- | Ranges are always deserialised as 'noRange'.

instance EmbPrj Range where
  icod_ :: Range -> S Word32
icod_ Range
_ = () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' ()
  value :: Word32 -> R Range
value Word32
_ = Range -> R Range
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Range
forall a. Range' a
noRange

instance EmbPrj KwRange where
  icod_ :: KwRange -> S Word32
icod_ KwRange
_ = () -> Arrows (Domains ()) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' ()
  value :: Word32 -> R KwRange
value Word32
_ = KwRange -> R KwRange
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return KwRange
forall a. Null a => a
empty

-- | Ranges that should be serialised properly.

newtype SerialisedRange = SerialisedRange { SerialisedRange -> Range
underlyingRange :: Range }

instance EmbPrj SerialisedRange where
  icod_ :: SerialisedRange -> S Word32
icod_ (SerialisedRange Range
r) = (SrcFile -> [IntervalWithoutFile] -> Range)
-> Arrows
     (Domains (SrcFile -> [IntervalWithoutFile] -> Range)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' SrcFile -> [IntervalWithoutFile] -> Range
forall a. a -> [IntervalWithoutFile] -> Range' a
P.intervalsToRange (Range -> SrcFile
P.rangeFile Range
r) (Range -> [IntervalWithoutFile]
forall a. Range' a -> [IntervalWithoutFile]
P.rangeIntervals Range
r)

  value :: Word32 -> R SerialisedRange
value Word32
i = Range -> SerialisedRange
SerialisedRange (Range -> SerialisedRange) -> R Range -> R SerialisedRange
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> (SrcFile -> [IntervalWithoutFile] -> Range)
-> Word32
-> R (CoDomain (SrcFile -> [IntervalWithoutFile] -> Range))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN SrcFile -> [IntervalWithoutFile] -> Range
forall a. a -> [IntervalWithoutFile] -> Range' a
P.intervalsToRange Word32
i

instance EmbPrj C.Name where
  icod_ :: Name -> S Word32
icod_ (C.NoName Range
a NameId
b)     = Word32
-> (Range -> NameId -> Name)
-> Arrows (Domains (Range -> NameId -> Name)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 Range -> NameId -> Name
C.NoName Range
a NameId
b
  icod_ (C.Name Range
r NameInScope
nis NameParts
xs)  = Word32
-> (Range -> NameInScope -> NameParts -> Name)
-> Arrows
     (Domains (Range -> NameInScope -> NameParts -> Name)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 Range -> NameInScope -> NameParts -> Name
C.Name Range
r NameInScope
nis NameParts
xs

  value :: Word32 -> R Name
value = (Node -> R Name) -> Word32 -> R Name
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R Name
valu where
    valu :: Node -> R Name
valu (N3 Word32
0 Word32
a Word32
b)      = (Range -> NameId -> Name)
-> Arrows
     (Constant Word32 (Domains (Range -> NameId -> Name)))
     (R (CoDomain (Range -> NameId -> Name)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Range -> NameId -> Name
C.NoName Word32
a Word32
b
    valu (N4 Word32
1 Word32
r Word32
nis Word32
xs) = (Range -> NameInScope -> NameParts -> Name)
-> Arrows
     (Constant
        Word32 (Domains (Range -> NameInScope -> NameParts -> Name)))
     (R (CoDomain (Range -> NameInScope -> NameParts -> Name)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Range -> NameInScope -> NameParts -> Name
C.Name   Word32
r Word32
nis Word32
xs
    valu Node
_               = R Name
forall a. HasCallStack => R a
malformed

instance EmbPrj NamePart where
  icod_ :: NamePart -> S Word32
icod_ NamePart
Hole   = NamePart -> Arrows (Domains NamePart) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' NamePart
Hole
  icod_ (Id String
a) = (String -> NamePart)
-> Arrows (Domains (String -> NamePart)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' String -> NamePart
Id String
a

  value :: Word32 -> R NamePart
value = (Node -> R NamePart) -> Word32 -> R NamePart
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R NamePart
valu where
    valu :: Node
-> Arrows
     (Constant Word32 (Domains NamePart)) (R (CoDomain NamePart))
valu Node
N0     = NamePart
-> Arrows
     (Constant Word32 (Domains NamePart)) (R (CoDomain NamePart))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NamePart
Hole
    valu (N1 Word32
a) = (String -> NamePart)
-> Arrows
     (Constant Word32 (Domains (String -> NamePart)))
     (R (CoDomain (String -> NamePart)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN String -> NamePart
Id Word32
a
    valu Node
_      = R NamePart
Arrows (Constant Word32 (Domains NamePart)) (R (CoDomain NamePart))
forall a. HasCallStack => R a
malformed

instance EmbPrj NameInScope where
  icod_ :: NameInScope -> S Word32
icod_ NameInScope
InScope    = NameInScope -> Arrows (Domains NameInScope) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' NameInScope
InScope
  icod_ NameInScope
NotInScope = Word32 -> NameInScope -> Arrows (Domains NameInScope) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 NameInScope
NotInScope

  value :: Word32 -> R NameInScope
value = (Node -> R NameInScope) -> Word32 -> R NameInScope
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R NameInScope
valu where
    valu :: Node
-> Arrows
     (Constant Word32 (Domains NameInScope)) (R (CoDomain NameInScope))
valu Node
N0     = NameInScope
-> Arrows
     (Constant Word32 (Domains NameInScope)) (R (CoDomain NameInScope))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameInScope
InScope
    valu (N1 Word32
0) = NameInScope
-> Arrows
     (Constant Word32 (Domains NameInScope)) (R (CoDomain NameInScope))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN NameInScope
NotInScope
    valu Node
_      = R NameInScope
Arrows
  (Constant Word32 (Domains NameInScope)) (R (CoDomain NameInScope))
forall a. HasCallStack => R a
malformed

instance EmbPrj C.QName where
  icod_ :: QName -> S Word32
icod_ (Qual    Name
a QName
b) = (Name -> QName -> QName)
-> Arrows (Domains (Name -> QName -> QName)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Name -> QName -> QName
Qual Name
a QName
b
  icod_ (C.QName Name
a  ) = (Name -> QName) -> Arrows (Domains (Name -> QName)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Name -> QName
C.QName Name
a

  value :: Word32 -> R QName
value = (Node -> R QName) -> Word32 -> R QName
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R QName
valu where
    valu :: Node -> R QName
valu (N2 Word32
a Word32
b) = (Name -> QName -> QName)
-> Arrows
     (Constant Word32 (Domains (Name -> QName -> QName)))
     (R (CoDomain (Name -> QName -> QName)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Name -> QName -> QName
Qual    Word32
a Word32
b
    valu (N1 Word32
a)   = (Name -> QName)
-> Arrows
     (Constant Word32 (Domains (Name -> QName)))
     (R (CoDomain (Name -> QName)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Name -> QName
C.QName Word32
a
    valu Node
_        = R QName
forall a. HasCallStack => R a
malformed

instance (EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) where
  icod_ :: ImportedName' a b -> S Word32
icod_ (ImportedModule b
a) = Word32
-> (b -> ImportedName' (ZonkAny 1) b)
-> Arrows (Domains (b -> ImportedName' (ZonkAny 1) b)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 b -> ImportedName' (ZonkAny 1) b
forall n m. m -> ImportedName' n m
ImportedModule b
a
  icod_ (ImportedName a
a)   = Word32
-> (a -> ImportedName' a (ZonkAny 2))
-> Arrows (Domains (a -> ImportedName' a (ZonkAny 2))) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
2 a -> ImportedName' a (ZonkAny 2)
forall n m. n -> ImportedName' n m
ImportedName a
a

  value :: Word32 -> R (ImportedName' a b)
value = (Node -> R (ImportedName' a b)) -> Word32 -> R (ImportedName' a b)
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R (ImportedName' a b)
forall {m} {n}.
(EmbPrj m, EmbPrj n) =>
Node -> R (ImportedName' n m)
valu where
    valu :: Node -> R (ImportedName' n m)
valu (N2 Word32
1 Word32
a) = (m -> ImportedName' n m)
-> Arrows
     (Constant Word32 (Domains (m -> ImportedName' n m)))
     (R (CoDomain (m -> ImportedName' n m)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN m -> ImportedName' n m
forall n m. m -> ImportedName' n m
ImportedModule Word32
a
    valu (N2 Word32
2 Word32
a) = (n -> ImportedName' n m)
-> Arrows
     (Constant Word32 (Domains (n -> ImportedName' n m)))
     (R (CoDomain (n -> ImportedName' n m)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN n -> ImportedName' n m
forall n m. n -> ImportedName' n m
ImportedName Word32
a
    valu Node
_ = R (ImportedName' n m)
forall a. HasCallStack => R a
malformed

instance EmbPrj Associativity where
  icod_ :: Associativity -> S Word32
icod_ Associativity
LeftAssoc  = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
0
  icod_ Associativity
RightAssoc = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
1
  icod_ Associativity
NonAssoc   = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
2

  value :: Word32 -> R Associativity
value = \case
    Word32
0 -> Associativity -> R Associativity
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Associativity
LeftAssoc
    Word32
1 -> Associativity -> R Associativity
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Associativity
RightAssoc
    Word32
2 -> Associativity -> R Associativity
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Associativity
NonAssoc
    Word32
_ -> R Associativity
forall a. HasCallStack => R a
malformed

instance EmbPrj FixityLevel where
  icod_ :: FixityLevel -> S Word32
icod_ FixityLevel
Unrelated   = FixityLevel -> Arrows (Domains FixityLevel) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' FixityLevel
Unrelated
  icod_ (Related PrecedenceLevel
a) = (PrecedenceLevel -> FixityLevel)
-> Arrows (Domains (PrecedenceLevel -> FixityLevel)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' PrecedenceLevel -> FixityLevel
Related PrecedenceLevel
a

  value :: Word32 -> R FixityLevel
value = (Node -> R FixityLevel) -> Word32 -> R FixityLevel
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R FixityLevel
valu where
    valu :: Node
-> Arrows
     (Constant Word32 (Domains FixityLevel)) (R (CoDomain FixityLevel))
valu Node
N0     = FixityLevel
-> Arrows
     (Constant Word32 (Domains FixityLevel)) (R (CoDomain FixityLevel))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN FixityLevel
Unrelated
    valu (N1 Word32
a) = (PrecedenceLevel -> FixityLevel)
-> Arrows
     (Constant Word32 (Domains (PrecedenceLevel -> FixityLevel)))
     (R (CoDomain (PrecedenceLevel -> FixityLevel)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN PrecedenceLevel -> FixityLevel
Related Word32
a
    valu Node
_      = R FixityLevel
Arrows
  (Constant Word32 (Domains FixityLevel)) (R (CoDomain FixityLevel))
forall a. HasCallStack => R a
malformed

instance EmbPrj Fixity where
  icod_ :: Fixity -> S Word32
icod_ (Fixity Range
a FixityLevel
b Associativity
c) = (Range -> FixityLevel -> Associativity -> Fixity)
-> Arrows
     (Domains (Range -> FixityLevel -> Associativity -> Fixity))
     (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Range -> FixityLevel -> Associativity -> Fixity
Fixity Range
a FixityLevel
b Associativity
c

  value :: Word32 -> R Fixity
value = (Range -> FixityLevel -> Associativity -> Fixity)
-> Word32
-> R (CoDomain (Range -> FixityLevel -> Associativity -> Fixity))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Range -> FixityLevel -> Associativity -> Fixity
Fixity

instance EmbPrj Fixity' where
  icod_ :: Fixity' -> S Word32
icod_ (Fixity' Fixity
a Notation
b Range
r) = (Fixity -> Notation -> Fixity')
-> Arrows (Domains (Fixity -> Notation -> Fixity')) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' (\ Fixity
a Notation
b -> Fixity -> Notation -> Range -> Fixity'
Fixity' Fixity
a Notation
b Range
r) Fixity
a Notation
b  -- discard theNameRange

  value :: Word32 -> R Fixity'
value = (Fixity -> Notation -> Fixity')
-> Word32 -> R (CoDomain (Fixity -> Notation -> Fixity'))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN (\ Fixity
f Notation
n -> Fixity -> Notation -> Range -> Fixity'
Fixity' Fixity
f Notation
n Range
forall a. Range' a
noRange)

instance EmbPrj BoundVariablePosition where
  icod_ :: BoundVariablePosition -> S Word32
icod_ (BoundVariablePosition Int
a Int
b) = (Int -> Int -> BoundVariablePosition)
-> Arrows
     (Domains (Int -> Int -> BoundVariablePosition)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Int -> Int -> BoundVariablePosition
BoundVariablePosition Int
a Int
b

  value :: Word32 -> R BoundVariablePosition
value = (Int -> Int -> BoundVariablePosition)
-> Word32 -> R (CoDomain (Int -> Int -> BoundVariablePosition))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Int -> Int -> BoundVariablePosition
BoundVariablePosition

instance EmbPrj NotationPart where
  icod_ :: NotationPart -> S Word32
icod_ (VarPart Range
a Ranged BoundVariablePosition
b)  = Word32
-> (Range -> Ranged BoundVariablePosition -> NotationPart)
-> Arrows
     (Domains (Range -> Ranged BoundVariablePosition -> NotationPart))
     (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 Range -> Ranged BoundVariablePosition -> NotationPart
VarPart Range
a Ranged BoundVariablePosition
b
  icod_ (HolePart Range
a NamedArg (Ranged Int)
b) = Word32
-> (Range -> NamedArg (Ranged Int) -> NotationPart)
-> Arrows
     (Domains (Range -> NamedArg (Ranged Int) -> NotationPart))
     (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 Range -> NamedArg (Ranged Int) -> NotationPart
HolePart Range
a NamedArg (Ranged Int)
b
  icod_ (WildPart Ranged BoundVariablePosition
a)   = Word32
-> (Ranged BoundVariablePosition -> NotationPart)
-> Arrows
     (Domains (Ranged BoundVariablePosition -> NotationPart)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
2 Ranged BoundVariablePosition -> NotationPart
WildPart Ranged BoundVariablePosition
a
  icod_ (IdPart RString
a)     = (RString -> NotationPart)
-> Arrows (Domains (RString -> NotationPart)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' RString -> NotationPart
IdPart RString
a

  value :: Word32 -> R NotationPart
value = (Node -> R NotationPart) -> Word32 -> R NotationPart
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R NotationPart
valu where
    valu :: Node -> R NotationPart
valu (N3 Word32
0 Word32
a Word32
b) = (Range -> Ranged BoundVariablePosition -> NotationPart)
-> Arrows
     (Constant
        Word32
        (Domains (Range -> Ranged BoundVariablePosition -> NotationPart)))
     (R (CoDomain
           (Range -> Ranged BoundVariablePosition -> NotationPart)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Range -> Ranged BoundVariablePosition -> NotationPart
VarPart Word32
a Word32
b
    valu (N3 Word32
1 Word32
a Word32
b) = (Range -> NamedArg (Ranged Int) -> NotationPart)
-> Arrows
     (Constant
        Word32 (Domains (Range -> NamedArg (Ranged Int) -> NotationPart)))
     (R (CoDomain (Range -> NamedArg (Ranged Int) -> NotationPart)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Range -> NamedArg (Ranged Int) -> NotationPart
HolePart Word32
a Word32
b
    valu (N2 Word32
2 Word32
a)   = (Ranged BoundVariablePosition -> NotationPart)
-> Arrows
     (Constant
        Word32 (Domains (Ranged BoundVariablePosition -> NotationPart)))
     (R (CoDomain (Ranged BoundVariablePosition -> NotationPart)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Ranged BoundVariablePosition -> NotationPart
WildPart Word32
a
    valu (N1 Word32
a)     = (RString -> NotationPart)
-> Arrows
     (Constant Word32 (Domains (RString -> NotationPart)))
     (R (CoDomain (RString -> NotationPart)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN RString -> NotationPart
IdPart Word32
a
    valu Node
_          = R NotationPart
forall a. HasCallStack => R a
malformed

instance EmbPrj MetaId where
  icod_ :: MetaId -> S Word32
icod_ (MetaId Word64
a ModuleNameHash
b) = (Word64, ModuleNameHash) -> S Word32
forall a. EmbPrj a => a -> S Word32
icode (Word64
a, ModuleNameHash
b)

  value :: Word32 -> R MetaId
value Word32
m = (Word64 -> ModuleNameHash -> MetaId)
-> (Word64, ModuleNameHash) -> MetaId
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Word64 -> ModuleNameHash -> MetaId
MetaId ((Word64, ModuleNameHash) -> MetaId)
-> ReaderT Decode IO (Word64, ModuleNameHash) -> R MetaId
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Word32 -> ReaderT Decode IO (Word64, ModuleNameHash)
forall a. EmbPrj a => Word32 -> R a
value Word32
m

instance EmbPrj ProblemId where
  icod_ :: ProblemId -> S Word32
icod_ (ProblemId Int
a) = Int -> S Word32
forall a. EmbPrj a => a -> S Word32
icode Int
a

  value :: Word32 -> R ProblemId
value Word32
m = Int -> ProblemId
ProblemId (Int -> ProblemId) -> ReaderT Decode IO Int -> R ProblemId
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Word32 -> ReaderT Decode IO Int
forall a. EmbPrj a => Word32 -> R a
value Word32
m

instance EmbPrj A.QName where
  icod_ :: QName -> S Word32
icod_ n :: QName
n@(A.QName ModuleName
a Name
b) = (Dict -> HashTableLU QNameId Word32)
-> (Dict -> FreshAndReuse) -> QNameId -> S Word32 -> S Word32
forall a.
(Ord a, Hashable a) =>
(Dict -> HashTableLU a Word32)
-> (Dict -> FreshAndReuse) -> a -> S Word32 -> S Word32
icodeMemo Dict -> HashTableLU QNameId Word32
qnameD Dict -> FreshAndReuse
qnameC (QName -> QNameId
qnameId QName
n) (S Word32 -> S Word32) -> S Word32 -> S Word32
forall a b. (a -> b) -> a -> b
$ (ModuleName -> Name -> QName)
-> Arrows (Domains (ModuleName -> Name -> QName)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' ModuleName -> Name -> QName
A.QName ModuleName
a Name
b

  value :: Word32 -> R QName
value = (ModuleName -> Name -> QName)
-> Word32 -> R (CoDomain (ModuleName -> Name -> QName))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN ModuleName -> Name -> QName
A.QName

instance EmbPrj A.AmbiguousQName where
  icod_ :: AmbiguousQName -> S Word32
icod_ (A.AmbQ List1 QName
a) = List1 QName -> S Word32
forall a. EmbPrj a => a -> S Word32
icode List1 QName
a
  value :: Word32 -> R AmbiguousQName
value Word32
n          = List1 QName -> AmbiguousQName
A.AmbQ (List1 QName -> AmbiguousQName)
-> ReaderT Decode IO (List1 QName) -> R AmbiguousQName
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Word32 -> ReaderT Decode IO (List1 QName)
forall a. EmbPrj a => Word32 -> R a
value Word32
n

instance EmbPrj A.ModuleName where
  icod_ :: ModuleName -> S Word32
icod_ (A.MName [Name]
a) = [Name] -> S Word32
forall a. EmbPrj a => a -> S Word32
icode [Name]
a
  value :: Word32 -> R ModuleName
value Word32
n           = [Name] -> ModuleName
A.MName ([Name] -> ModuleName) -> ReaderT Decode IO [Name] -> R ModuleName
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Word32 -> ReaderT Decode IO [Name]
forall a. EmbPrj a => Word32 -> R a
value Word32
n

instance EmbPrj A.Name where
  icod_ :: Name -> S Word32
icod_ (A.Name NameId
a Name
b Name
c Range
d Fixity'
e Bool
f) = (Dict -> HashTableLU NameId Word32)
-> (Dict -> FreshAndReuse) -> NameId -> S Word32 -> S Word32
forall a.
(Ord a, Hashable a) =>
(Dict -> HashTableLU a Word32)
-> (Dict -> FreshAndReuse) -> a -> S Word32 -> S Word32
icodeMemo Dict -> HashTableLU NameId Word32
nameD Dict -> FreshAndReuse
nameC NameId
a (S Word32 -> S Word32) -> S Word32 -> S Word32
forall a b. (a -> b) -> a -> b
$
    (NameId
 -> Name -> Name -> SerialisedRange -> Fixity' -> Bool -> Name)
-> Arrows
     (Domains
        (NameId
         -> Name -> Name -> SerialisedRange -> Fixity' -> Bool -> Name))
     (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' (\ NameId
a Name
b Name
c SerialisedRange
d Fixity'
e Bool
f -> NameId -> Name -> Name -> Range -> Fixity' -> Bool -> Name
A.Name NameId
a Name
b Name
c (SerialisedRange -> Range
underlyingRange SerialisedRange
d) Fixity'
e Bool
f) NameId
a Name
b Name
c (Range -> SerialisedRange
SerialisedRange Range
d) Fixity'
e Bool
f

  value :: Word32 -> R Name
value = (NameId
 -> Name -> Name -> SerialisedRange -> Fixity' -> Bool -> Name)
-> Word32
-> R (CoDomain
        (NameId
         -> Name -> Name -> SerialisedRange -> Fixity' -> Bool -> Name))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN (\NameId
a Name
b Name
c SerialisedRange
d Fixity'
e Bool
f -> NameId -> Name -> Name -> Range -> Fixity' -> Bool -> Name
A.Name NameId
a Name
b Name
c (SerialisedRange -> Range
underlyingRange SerialisedRange
d) Fixity'
e Bool
f)

instance EmbPrj a => EmbPrj (C.FieldAssignment' a) where
  icod_ :: FieldAssignment' a -> S Word32
icod_ (C.FieldAssignment Name
a a
b) = (Name -> a -> FieldAssignment' a)
-> Arrows (Domains (Name -> a -> FieldAssignment' a)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Name -> a -> FieldAssignment' a
forall a. Name -> a -> FieldAssignment' a
C.FieldAssignment Name
a a
b

  value :: Word32 -> R (FieldAssignment' a)
value = (Name -> a -> FieldAssignment' a)
-> Word32 -> R (CoDomain (Name -> a -> FieldAssignment' a))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Name -> a -> FieldAssignment' a
forall a. Name -> a -> FieldAssignment' a
C.FieldAssignment

instance (EmbPrj s, EmbPrj t) => EmbPrj (Named s t) where
  icod_ :: Named s t -> S Word32
icod_ (Named Maybe s
a t
b) = (Maybe s -> t -> Named s t)
-> Arrows (Domains (Maybe s -> t -> Named s t)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Maybe s -> t -> Named s t
forall name a. Maybe name -> a -> Named name a
Named Maybe s
a t
b

  value :: Word32 -> R (Named s t)
value = (Maybe s -> t -> Named s t)
-> Word32 -> R (CoDomain (Maybe s -> t -> Named s t))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Maybe s -> t -> Named s t
forall name a. Maybe name -> a -> Named name a
Named

instance EmbPrj a => EmbPrj (Ranged a) where
  icod_ :: Ranged a -> S Word32
icod_ (Ranged Range
r a
x) = (Range -> a -> Ranged a)
-> Arrows (Domains (Range -> a -> Ranged a)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Range -> a -> Ranged a
forall a. Range -> a -> Ranged a
Ranged Range
r a
x

  value :: Word32 -> R (Ranged a)
value = (Range -> a -> Ranged a)
-> Word32 -> R (CoDomain (Range -> a -> Ranged a))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Range -> a -> Ranged a
forall a. Range -> a -> Ranged a
Ranged

instance EmbPrj ArgInfo where
  icod_ :: ArgInfo -> S Word32
icod_ (ArgInfo Hiding
h Modality
r Origin
o FreeVariables
fv Annotation
ann) = (Hiding
 -> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo)
-> Arrows
     (Domains
        (Hiding
         -> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo))
     (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Hiding
-> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo
ArgInfo Hiding
h Modality
r Origin
o FreeVariables
fv Annotation
ann

  value :: Word32 -> R ArgInfo
value = (Hiding
 -> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo)
-> Word32
-> R (CoDomain
        (Hiding
         -> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Hiding
-> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo
ArgInfo

instance EmbPrj ModuleNameHash where
  icod_ :: ModuleNameHash -> S Word32
icod_ (ModuleNameHash Word64
a) = (Word64 -> ModuleNameHash)
-> Arrows (Domains (Word64 -> ModuleNameHash)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Word64 -> ModuleNameHash
ModuleNameHash Word64
a

  value :: Word32 -> R ModuleNameHash
value = (Word64 -> ModuleNameHash)
-> Word32 -> R (CoDomain (Word64 -> ModuleNameHash))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Word64 -> ModuleNameHash
ModuleNameHash

instance EmbPrj NameId where
  icod_ :: NameId -> S Word32
icod_ (NameId Word64
a ModuleNameHash
b) = (Word64 -> ModuleNameHash -> NameId)
-> Arrows (Domains (Word64 -> ModuleNameHash -> NameId)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Word64 -> ModuleNameHash -> NameId
NameId Word64
a ModuleNameHash
b

  value :: Word32 -> R NameId
value = (Word64 -> ModuleNameHash -> NameId)
-> Word32 -> R (CoDomain (Word64 -> ModuleNameHash -> NameId))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Word64 -> ModuleNameHash -> NameId
NameId

instance EmbPrj OpaqueId where
  icod_ :: OpaqueId -> S Word32
icod_ (OpaqueId Word64
a ModuleNameHash
b) = (Word64 -> ModuleNameHash -> OpaqueId)
-> Arrows
     (Domains (Word64 -> ModuleNameHash -> OpaqueId)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Word64 -> ModuleNameHash -> OpaqueId
OpaqueId Word64
a ModuleNameHash
b

  value :: Word32 -> R OpaqueId
value = (Word64 -> ModuleNameHash -> OpaqueId)
-> Word32 -> R (CoDomain (Word64 -> ModuleNameHash -> OpaqueId))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Word64 -> ModuleNameHash -> OpaqueId
OpaqueId

instance EmbPrj a => EmbPrj (WithHiding a) where
  icod_ :: WithHiding a -> S Word32
icod_ (WithHiding Hiding
a a
b) = (Hiding -> a -> WithHiding a)
-> Arrows (Domains (Hiding -> a -> WithHiding a)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Hiding -> a -> WithHiding a
forall a. Hiding -> a -> WithHiding a
WithHiding Hiding
a a
b

  value :: Word32 -> R (WithHiding a)
value = (Hiding -> a -> WithHiding a)
-> Word32 -> R (CoDomain (Hiding -> a -> WithHiding a))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Hiding -> a -> WithHiding a
forall a. Hiding -> a -> WithHiding a
WithHiding

instance EmbPrj a => EmbPrj (Arg a) where
  icod_ :: Arg a -> S Word32
icod_ (Arg ArgInfo
i a
e) = (ArgInfo -> a -> Arg a)
-> Arrows (Domains (ArgInfo -> a -> Arg a)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i a
e

  value :: Word32 -> R (Arg a)
value = (ArgInfo -> a -> Arg a)
-> Word32 -> R (CoDomain (ArgInfo -> a -> Arg a))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg

instance EmbPrj a => EmbPrj (HasEta' a) where
  icod_ :: HasEta' a -> S Word32
icod_ HasEta' a
YesEta    = HasEta' (ZonkAny 0)
-> Arrows (Domains (HasEta' (ZonkAny 0))) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' HasEta' (ZonkAny 0)
forall a. HasEta' a
YesEta
  icod_ (NoEta a
a) = (a -> HasEta' a) -> Arrows (Domains (a -> HasEta' a)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' a -> HasEta' a
forall a. a -> HasEta' a
NoEta a
a

  value :: Word32 -> R (HasEta' a)
value = (Node -> R (HasEta' a)) -> Word32 -> R (HasEta' a)
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R (HasEta' a)
forall {a}. EmbPrj a => Node -> ReaderT Decode IO (HasEta' a)
valu where
    valu :: Node
-> Arrows
     (Constant Word32 (Domains (HasEta' a))) (R (CoDomain (HasEta' a)))
valu Node
N0     = HasEta' a
-> Arrows
     (Constant Word32 (Domains (HasEta' a))) (R (CoDomain (HasEta' a)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN HasEta' a
forall a. HasEta' a
YesEta
    valu (N1 Word32
a) = (a -> HasEta' a)
-> Arrows
     (Constant Word32 (Domains (a -> HasEta' a)))
     (R (CoDomain (a -> HasEta' a)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN a -> HasEta' a
forall a. a -> HasEta' a
NoEta Word32
a
    valu Node
_      = ReaderT Decode IO (HasEta' a)
Arrows
  (Constant Word32 (Domains (HasEta' a))) (R (CoDomain (HasEta' a)))
forall a. HasCallStack => R a
malformed

instance EmbPrj PatternOrCopattern
instance EmbPrj OverlapMode

instance EmbPrj Induction where
  icod_ :: Induction -> S Word32
icod_ Induction
Inductive   = Induction -> Arrows (Domains Induction) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Induction
Inductive
  icod_ Induction
CoInductive = Word32 -> Induction -> Arrows (Domains Induction) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 Induction
CoInductive

  value :: Word32 -> R Induction
value = (Node -> R Induction) -> Word32 -> R Induction
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R Induction
valu where
    valu :: Node
-> Arrows
     (Constant Word32 (Domains Induction)) (R (CoDomain Induction))
valu Node
N0     = Induction
-> Arrows
     (Constant Word32 (Domains Induction)) (R (CoDomain Induction))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Induction
Inductive
    valu (N1 Word32
1) = Induction
-> Arrows
     (Constant Word32 (Domains Induction)) (R (CoDomain Induction))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Induction
CoInductive
    valu Node
_      = R Induction
Arrows
  (Constant Word32 (Domains Induction)) (R (CoDomain Induction))
forall a. HasCallStack => R a
malformed

instance EmbPrj Hiding where
  icod_ :: Hiding -> S Word32
icod_ Hiding
Hidden                = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
0
  icod_ Hiding
NotHidden             = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
1
  icod_ (Instance Overlappable
NoOverlap)  = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
2
  icod_ (Instance Overlappable
YesOverlap) = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
3

  value :: Word32 -> R Hiding
value Word32
0 = Hiding -> R Hiding
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Hiding
Hidden
  value Word32
1 = Hiding -> R Hiding
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Hiding
NotHidden
  value Word32
2 = Hiding -> R Hiding
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Overlappable -> Hiding
Instance Overlappable
NoOverlap)
  value Word32
3 = Hiding -> R Hiding
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Overlappable -> Hiding
Instance Overlappable
YesOverlap)
  value Word32
_ = R Hiding
forall a. HasCallStack => R a
malformed

instance EmbPrj Q0Origin where
  icod_ :: Q0Origin -> S Word32
icod_ = \case
    Q0Origin
Q0Inferred -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
0
    Q0 Range
_       -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
1
    Q0Erased Range
_ -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
2

  value :: Word32 -> R Q0Origin
value = \case
    Word32
0 -> Q0Origin -> R Q0Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Q0Origin -> R Q0Origin) -> Q0Origin -> R Q0Origin
forall a b. (a -> b) -> a -> b
$ Q0Origin
Q0Inferred
    Word32
1 -> Q0Origin -> R Q0Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Q0Origin -> R Q0Origin) -> Q0Origin -> R Q0Origin
forall a b. (a -> b) -> a -> b
$ Range -> Q0Origin
Q0       Range
forall a. Range' a
noRange
    Word32
2 -> Q0Origin -> R Q0Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Q0Origin -> R Q0Origin) -> Q0Origin -> R Q0Origin
forall a b. (a -> b) -> a -> b
$ Range -> Q0Origin
Q0Erased Range
forall a. Range' a
noRange
    Word32
_ -> R Q0Origin
forall a. HasCallStack => R a
malformed

instance EmbPrj Q1Origin where
  icod_ :: Q1Origin -> S Word32
icod_ = \case
    Q1Origin
Q1Inferred -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
0
    Q1 Range
_       -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
1
    Q1Linear Range
_ -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
2

  value :: Word32 -> R Q1Origin
value = \case
    Word32
0 -> Q1Origin -> R Q1Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Q1Origin -> R Q1Origin) -> Q1Origin -> R Q1Origin
forall a b. (a -> b) -> a -> b
$ Q1Origin
Q1Inferred
    Word32
1 -> Q1Origin -> R Q1Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Q1Origin -> R Q1Origin) -> Q1Origin -> R Q1Origin
forall a b. (a -> b) -> a -> b
$ Range -> Q1Origin
Q1       Range
forall a. Range' a
noRange
    Word32
2 -> Q1Origin -> R Q1Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Q1Origin -> R Q1Origin) -> Q1Origin -> R Q1Origin
forall a b. (a -> b) -> a -> b
$ Range -> Q1Origin
Q1Linear Range
forall a. Range' a
noRange
    Word32
_ -> R Q1Origin
forall a. HasCallStack => R a
malformed

instance EmbPrj QωOrigin where
  icod_ :: QωOrigin -> S Word32
icod_ = \case
    QωOrigin
QωInferred -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
0
    Qω Range
_       -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
1
    QωPlenty Range
_ -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
2

  value :: Word32 -> R QωOrigin
value = \case
    Word32
0 -> QωOrigin -> R QωOrigin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (QωOrigin -> R QωOrigin) -> QωOrigin -> R QωOrigin
forall a b. (a -> b) -> a -> b
$ QωOrigin
QωInferred
    Word32
1 -> QωOrigin -> R QωOrigin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (QωOrigin -> R QωOrigin) -> QωOrigin -> R QωOrigin
forall a b. (a -> b) -> a -> b
$ Range -> QωOrigin
Qω       Range
forall a. Range' a
noRange
    Word32
2 -> QωOrigin -> R QωOrigin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (QωOrigin -> R QωOrigin) -> QωOrigin -> R QωOrigin
forall a b. (a -> b) -> a -> b
$ Range -> QωOrigin
QωPlenty Range
forall a. Range' a
noRange
    Word32
_ -> R QωOrigin
forall a. HasCallStack => R a
malformed

instance EmbPrj Quantity where
  icod_ :: Quantity -> S Word32
icod_ = \case
    Quantity0 Q0Origin
a -> Word32
-> (Q0Origin -> Quantity)
-> Arrows (Domains (Q0Origin -> Quantity)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 Q0Origin -> Quantity
Quantity0 Q0Origin
a
    Quantity1 Q1Origin
a -> Word32
-> (Q1Origin -> Quantity)
-> Arrows (Domains (Q1Origin -> Quantity)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 Q1Origin -> Quantity
Quantity1 Q1Origin
a
    Quantityω QωOrigin
a -> (QωOrigin -> Quantity)
-> Arrows (Domains (QωOrigin -> Quantity)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN'  QωOrigin -> Quantity
Quantityω QωOrigin
a  -- default quantity, shorter code

  value :: Word32 -> R Quantity
value = (Node -> R Quantity) -> Word32 -> R Quantity
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase ((Node -> R Quantity) -> Word32 -> R Quantity)
-> (Node -> R Quantity) -> Word32 -> R Quantity
forall a b. (a -> b) -> a -> b
$ \case
    (N2 Word32
0 Word32
a) -> (Q0Origin -> Quantity)
-> Arrows
     (Constant Word32 (Domains (Q0Origin -> Quantity)))
     (R (CoDomain (Q0Origin -> Quantity)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Q0Origin -> Quantity
Quantity0 Word32
a
    (N2 Word32
1 Word32
a) -> (Q1Origin -> Quantity)
-> Arrows
     (Constant Word32 (Domains (Q1Origin -> Quantity)))
     (R (CoDomain (Q1Origin -> Quantity)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Q1Origin -> Quantity
Quantity1 Word32
a
    (N1 Word32
a)   -> (QωOrigin -> Quantity)
-> Arrows
     (Constant Word32 (Domains (QωOrigin -> Quantity)))
     (R (CoDomain (QωOrigin -> Quantity)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN QωOrigin -> Quantity
Quantityω Word32
a
    Node
_        -> R Quantity
forall a. HasCallStack => R a
malformed

-- -- ALT: forget quantity origin when serializing?
-- instance EmbPrj Quantity where
--   icod_ Quantity0 = return 0
--   icod_ Quantity1 = return 1
--   icod_ Quantityω = return 2

--   value 0 = return Quantity0
--   value 1 = return Quantity1
--   value 2 = return Quantityω
--   value _ = malformed

instance EmbPrj Cohesion where
  icod_ :: Cohesion -> S Word32
icod_ Cohesion
Flat       = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
0
  icod_ Cohesion
Continuous = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
1
  icod_ Cohesion
Squash     = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
2

  value :: Word32 -> R Cohesion
value Word32
0 = Cohesion -> R Cohesion
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Cohesion
Flat
  value Word32
1 = Cohesion -> R Cohesion
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Cohesion
Continuous
  value Word32
2 = Cohesion -> R Cohesion
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Cohesion
Squash
  value Word32
_ = R Cohesion
forall a. HasCallStack => R a
malformed

instance EmbPrj ModalPolarity where
  icod_ :: ModalPolarity -> S Word32
icod_ ModalPolarity
UnusedPolarity = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
0
  icod_ ModalPolarity
StrictlyPositive = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
1
  icod_ ModalPolarity
Positive = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
2
  icod_ ModalPolarity
Negative = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
3
  icod_ ModalPolarity
MixedPolarity = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
4

  value :: Word32 -> R ModalPolarity
value Word32
0 = ModalPolarity -> R ModalPolarity
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ModalPolarity
UnusedPolarity
  value Word32
1 = ModalPolarity -> R ModalPolarity
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ModalPolarity
StrictlyPositive
  value Word32
2 = ModalPolarity -> R ModalPolarity
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ModalPolarity
Positive
  value Word32
3 = ModalPolarity -> R ModalPolarity
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ModalPolarity
Negative
  value Word32
4 = ModalPolarity -> R ModalPolarity
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ModalPolarity
MixedPolarity
  value Word32
_ = R ModalPolarity
forall a. HasCallStack => R a
malformed

instance EmbPrj PolarityModality where
  icod_ :: PolarityModality -> S Word32
icod_ (PolarityModality ModalPolarity
p ModalPolarity
o ModalPolarity
l) = (ModalPolarity, ModalPolarity, ModalPolarity) -> S Word32
forall a. EmbPrj a => a -> S Word32
icod_ (ModalPolarity
p, ModalPolarity
o, ModalPolarity
l)

  value :: Word32 -> R PolarityModality
value Word32
n = do
    (p, o, l) <- R (ModalPolarity, ModalPolarity, ModalPolarity)
polPair
    return $ PolarityModality p o l
    where
      polPair :: R (ModalPolarity, ModalPolarity, ModalPolarity)
      polPair :: R (ModalPolarity, ModalPolarity, ModalPolarity)
polPair = Word32 -> R (ModalPolarity, ModalPolarity, ModalPolarity)
forall a. EmbPrj a => Word32 -> R a
value Word32
n

instance EmbPrj Modality where
  icod_ :: Modality -> S Word32
icod_ (Modality Relevance
a Quantity
b Cohesion
c PolarityModality
d) = (Relevance -> Quantity -> Cohesion -> PolarityModality -> Modality)
-> Arrows
     (Domains
        (Relevance
         -> Quantity -> Cohesion -> PolarityModality -> Modality))
     (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Relevance -> Quantity -> Cohesion -> PolarityModality -> Modality
Modality Relevance
a Quantity
b Cohesion
c PolarityModality
d

  value :: Word32 -> R Modality
value = (Node -> R Modality) -> Word32 -> R Modality
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase ((Node -> R Modality) -> Word32 -> R Modality)
-> (Node -> R Modality) -> Word32 -> R Modality
forall a b. (a -> b) -> a -> b
$ \case
    (N4 Word32
a Word32
b Word32
c Word32
d) -> (Relevance -> Quantity -> Cohesion -> PolarityModality -> Modality)
-> Arrows
     (Constant
        Word32
        (Domains
           (Relevance
            -> Quantity -> Cohesion -> PolarityModality -> Modality)))
     (R (CoDomain
           (Relevance
            -> Quantity -> Cohesion -> PolarityModality -> Modality)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Relevance -> Quantity -> Cohesion -> PolarityModality -> Modality
Modality Word32
a Word32
b Word32
c Word32
d
    Node
_ -> R Modality
forall a. HasCallStack => R a
malformed

instance EmbPrj OriginRelevant where
  icod_ :: OriginRelevant -> S Word32
icod_ = \case
    OriginRelevant
ORelInferred   -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
0
    ORelRelevant Range
_ -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
1

  value :: Word32 -> R OriginRelevant
value = \case
    Word32
0 -> OriginRelevant -> R OriginRelevant
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OriginRelevant -> R OriginRelevant)
-> OriginRelevant -> R OriginRelevant
forall a b. (a -> b) -> a -> b
$ OriginRelevant
ORelInferred
    Word32
1 -> OriginRelevant -> R OriginRelevant
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OriginRelevant -> R OriginRelevant)
-> OriginRelevant -> R OriginRelevant
forall a b. (a -> b) -> a -> b
$ Range -> OriginRelevant
ORelRelevant Range
forall a. Range' a
noRange
    Word32
_ -> R OriginRelevant
forall a. HasCallStack => R a
malformed

instance EmbPrj OriginIrrelevant where
  icod_ :: OriginIrrelevant -> S Word32
icod_ = \case
    OriginIrrelevant
OIrrInferred     -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
0
    OIrrDot Range
_        -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
1
    OIrrIrr Range
_        -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
2
    OIrrIrrelevant Range
_ -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
3

  value :: Word32 -> R OriginIrrelevant
value = \case
    Word32
0 -> OriginIrrelevant -> R OriginIrrelevant
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OriginIrrelevant -> R OriginIrrelevant)
-> OriginIrrelevant -> R OriginIrrelevant
forall a b. (a -> b) -> a -> b
$ OriginIrrelevant
OIrrInferred
    Word32
1 -> OriginIrrelevant -> R OriginIrrelevant
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OriginIrrelevant -> R OriginIrrelevant)
-> OriginIrrelevant -> R OriginIrrelevant
forall a b. (a -> b) -> a -> b
$ Range -> OriginIrrelevant
OIrrDot        Range
forall a. Range' a
noRange
    Word32
2 -> OriginIrrelevant -> R OriginIrrelevant
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OriginIrrelevant -> R OriginIrrelevant)
-> OriginIrrelevant -> R OriginIrrelevant
forall a b. (a -> b) -> a -> b
$ Range -> OriginIrrelevant
OIrrIrr        Range
forall a. Range' a
noRange
    Word32
3 -> OriginIrrelevant -> R OriginIrrelevant
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OriginIrrelevant -> R OriginIrrelevant)
-> OriginIrrelevant -> R OriginIrrelevant
forall a b. (a -> b) -> a -> b
$ Range -> OriginIrrelevant
OIrrIrrelevant Range
forall a. Range' a
noRange
    Word32
_ -> R OriginIrrelevant
forall a. HasCallStack => R a
malformed

instance EmbPrj OriginShapeIrrelevant where
  icod_ :: OriginShapeIrrelevant -> S Word32
icod_ = \case
    OriginShapeIrrelevant
OShIrrInferred          -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
0
    OShIrrDotDot Range
_          -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
1
    OShIrrShIrr Range
_           -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
2
    OShIrrShapeIrrelevant Range
_ -> Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
3

  value :: Word32 -> R OriginShapeIrrelevant
value = \case
    Word32
0 -> OriginShapeIrrelevant -> R OriginShapeIrrelevant
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OriginShapeIrrelevant -> R OriginShapeIrrelevant)
-> OriginShapeIrrelevant -> R OriginShapeIrrelevant
forall a b. (a -> b) -> a -> b
$ OriginShapeIrrelevant
OShIrrInferred
    Word32
1 -> OriginShapeIrrelevant -> R OriginShapeIrrelevant
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OriginShapeIrrelevant -> R OriginShapeIrrelevant)
-> OriginShapeIrrelevant -> R OriginShapeIrrelevant
forall a b. (a -> b) -> a -> b
$ Range -> OriginShapeIrrelevant
OShIrrDotDot          Range
forall a. Range' a
noRange
    Word32
2 -> OriginShapeIrrelevant -> R OriginShapeIrrelevant
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OriginShapeIrrelevant -> R OriginShapeIrrelevant)
-> OriginShapeIrrelevant -> R OriginShapeIrrelevant
forall a b. (a -> b) -> a -> b
$ Range -> OriginShapeIrrelevant
OShIrrShIrr           Range
forall a. Range' a
noRange
    Word32
3 -> OriginShapeIrrelevant -> R OriginShapeIrrelevant
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (OriginShapeIrrelevant -> R OriginShapeIrrelevant)
-> OriginShapeIrrelevant -> R OriginShapeIrrelevant
forall a b. (a -> b) -> a -> b
$ Range -> OriginShapeIrrelevant
OShIrrShapeIrrelevant Range
forall a. Range' a
noRange
    Word32
_ -> R OriginShapeIrrelevant
forall a. HasCallStack => R a
malformed

instance EmbPrj Relevance where
  icod_ :: Relevance -> S Word32
icod_ = \case
    Relevant   OriginRelevant
a      -> (OriginRelevant -> Relevance)
-> Arrows (Domains (OriginRelevant -> Relevance)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' OriginRelevant -> Relevance
Relevant OriginRelevant
a
    Irrelevant OriginIrrelevant
a      -> Word32
-> (OriginIrrelevant -> Relevance)
-> Arrows (Domains (OriginIrrelevant -> Relevance)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 OriginIrrelevant -> Relevance
Irrelevant OriginIrrelevant
a
    ShapeIrrelevant OriginShapeIrrelevant
a -> Word32
-> (OriginShapeIrrelevant -> Relevance)
-> Arrows (Domains (OriginShapeIrrelevant -> Relevance)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 OriginShapeIrrelevant -> Relevance
ShapeIrrelevant OriginShapeIrrelevant
a

  value :: Word32 -> R Relevance
value = (Node -> R Relevance) -> Word32 -> R Relevance
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase \case
    N1 Word32
a   -> (OriginRelevant -> Relevance)
-> Arrows
     (Constant Word32 (Domains (OriginRelevant -> Relevance)))
     (R (CoDomain (OriginRelevant -> Relevance)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN OriginRelevant -> Relevance
Relevant Word32
a
    N2 Word32
0 Word32
a -> (OriginIrrelevant -> Relevance)
-> Arrows
     (Constant Word32 (Domains (OriginIrrelevant -> Relevance)))
     (R (CoDomain (OriginIrrelevant -> Relevance)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN OriginIrrelevant -> Relevance
Irrelevant Word32
a
    N2 Word32
1 Word32
a -> (OriginShapeIrrelevant -> Relevance)
-> Arrows
     (Constant Word32 (Domains (OriginShapeIrrelevant -> Relevance)))
     (R (CoDomain (OriginShapeIrrelevant -> Relevance)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN OriginShapeIrrelevant -> Relevance
ShapeIrrelevant Word32
a
    Node
_      -> R Relevance
forall a. HasCallStack => R a
malformed

instance EmbPrj Annotation where
  icod_ :: Annotation -> S Word32
icod_ (Annotation Lock
l) = (Lock -> Annotation)
-> Arrows (Domains (Lock -> Annotation)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Lock -> Annotation
Annotation Lock
l

  value :: Word32 -> R Annotation
value = (Lock -> Annotation) -> Word32 -> R (CoDomain (Lock -> Annotation))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Lock -> Annotation
Annotation

instance EmbPrj Lock where
  icod_ :: Lock -> S Word32
icod_ Lock
IsNotLock          = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
0
  icod_ (IsLock LockOrigin
LockOTick) = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
1
  icod_ (IsLock LockOrigin
LockOLock) = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
2

  value :: Word32 -> R Lock
value Word32
0 = Lock -> R Lock
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Lock
IsNotLock
  value Word32
1 = Lock -> R Lock
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LockOrigin -> Lock
IsLock LockOrigin
LockOTick)
  value Word32
2 = Lock -> R Lock
forall a. a -> ReaderT Decode IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LockOrigin -> Lock
IsLock LockOrigin
LockOLock)
  value Word32
_ = R Lock
forall a. HasCallStack => R a
malformed

instance EmbPrj Origin where
  icod_ :: Origin -> S Word32
icod_ Origin
UserWritten = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
0
  icod_ Origin
Inserted    = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
1
  icod_ Origin
Reflected   = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
2
  icod_ Origin
CaseSplit   = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
3
  icod_ Origin
Substitution = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
4
  icod_ Origin
ExpandedPun = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
5
  icod_ Origin
Generalization = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
6

  value :: Word32 -> R Origin
value Word32
0 = Origin -> R Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Origin
UserWritten
  value Word32
1 = Origin -> R Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Origin
Inserted
  value Word32
2 = Origin -> R Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Origin
Reflected
  value Word32
3 = Origin -> R Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Origin
CaseSplit
  value Word32
4 = Origin -> R Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Origin
Substitution
  value Word32
5 = Origin -> R Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Origin
ExpandedPun
  value Word32
6 = Origin -> R Origin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Origin
Generalization
  value Word32
_ = R Origin
forall a. HasCallStack => R a
malformed

instance EmbPrj a => EmbPrj (WithOrigin a) where
  icod_ :: WithOrigin a -> S Word32
icod_ (WithOrigin Origin
a a
b) = (Origin -> a -> WithOrigin a)
-> Arrows (Domains (Origin -> a -> WithOrigin a)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Origin -> a -> WithOrigin a
forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
a a
b

  value :: Word32 -> R (WithOrigin a)
value = (Origin -> a -> WithOrigin a)
-> Word32 -> R (CoDomain (Origin -> a -> WithOrigin a))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Origin -> a -> WithOrigin a
forall a. Origin -> a -> WithOrigin a
WithOrigin

instance EmbPrj FreeVariables where
  icod_ :: FreeVariables -> S Word32
icod_ FreeVariables
UnknownFVs   = FreeVariables -> Arrows (Domains FreeVariables) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' FreeVariables
UnknownFVs
  icod_ (KnownFVs VarSet
a) = (VarSet -> FreeVariables)
-> Arrows (Domains (VarSet -> FreeVariables)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' VarSet -> FreeVariables
KnownFVs VarSet
a

  value :: Word32 -> R FreeVariables
value = (Node -> R FreeVariables) -> Word32 -> R FreeVariables
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R FreeVariables
valu where
    valu :: Node
-> Arrows
     (Constant Word32 (Domains FreeVariables))
     (R (CoDomain FreeVariables))
valu Node
N0     = FreeVariables
-> Arrows
     (Constant Word32 (Domains FreeVariables))
     (R (CoDomain FreeVariables))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN FreeVariables
UnknownFVs
    valu (N1 Word32
a) = (VarSet -> FreeVariables)
-> Arrows
     (Constant Word32 (Domains (VarSet -> FreeVariables)))
     (R (CoDomain (VarSet -> FreeVariables)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN VarSet -> FreeVariables
KnownFVs Word32
a
    valu Node
_      = R FreeVariables
Arrows
  (Constant Word32 (Domains FreeVariables))
  (R (CoDomain FreeVariables))
forall a. HasCallStack => R a
malformed

instance EmbPrj ConOrigin where
  icod_ :: ConOrigin -> S Word32
icod_ ConOrigin
ConOSystem   = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
0
  icod_ ConOrigin
ConOCon      = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
1
  icod_ ConOrigin
ConORec      = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
2
  icod_ ConOrigin
ConOSplit    = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
3
  icod_ ConOrigin
ConORecWhere = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
4

  value :: Word32 -> R ConOrigin
value Word32
0 = ConOrigin -> R ConOrigin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConOSystem
  value Word32
1 = ConOrigin -> R ConOrigin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConOCon
  value Word32
2 = ConOrigin -> R ConOrigin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConORec
  value Word32
3 = ConOrigin -> R ConOrigin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConOSplit
  value Word32
4 = ConOrigin -> R ConOrigin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConORecWhere
  value Word32
_ = R ConOrigin
forall a. HasCallStack => R a
malformed

instance EmbPrj ProjOrigin where
  icod_ :: ProjOrigin -> S Word32
icod_ ProjOrigin
ProjPrefix  = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
0
  icod_ ProjOrigin
ProjPostfix = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
1
  icod_ ProjOrigin
ProjSystem  = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
2

  value :: Word32 -> R ProjOrigin
value Word32
0 = ProjOrigin -> R ProjOrigin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ProjOrigin
ProjPrefix
  value Word32
1 = ProjOrigin -> R ProjOrigin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ProjOrigin
ProjPostfix
  value Word32
2 = ProjOrigin -> R ProjOrigin
forall a. a -> ReaderT Decode IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ProjOrigin
ProjSystem
  value Word32
_ = R ProjOrigin
forall a. HasCallStack => R a
malformed

instance EmbPrj Agda.Syntax.Literal.Literal where
  icod_ :: Literal -> S Word32
icod_ (LitNat    Integer
a)   = (Integer -> Literal)
-> Arrows (Domains (Integer -> Literal)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Integer -> Literal
LitNat Integer
a
  icod_ (LitFloat  PrecedenceLevel
a)   = Word32
-> (PrecedenceLevel -> Literal)
-> Arrows (Domains (PrecedenceLevel -> Literal)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 PrecedenceLevel -> Literal
LitFloat PrecedenceLevel
a
  icod_ (LitString Text
a)   = Word32
-> (Text -> Literal)
-> Arrows (Domains (Text -> Literal)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
2 Text -> Literal
LitString Text
a
  icod_ (LitChar   Char
a)   = Word32
-> (Char -> Literal)
-> Arrows (Domains (Char -> Literal)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
3 Char -> Literal
LitChar Char
a
  icod_ (LitQName  QName
a)   = Word32
-> (QName -> Literal)
-> Arrows (Domains (QName -> Literal)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
5 QName -> Literal
LitQName QName
a
  icod_ (LitMeta   TopLevelModuleName
a MetaId
b) = Word32
-> (TopLevelModuleName -> MetaId -> Literal)
-> Arrows
     (Domains (TopLevelModuleName -> MetaId -> Literal)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
6 TopLevelModuleName -> MetaId -> Literal
LitMeta TopLevelModuleName
a MetaId
b
  icod_ (LitWord64 Word64
a)   = Word32
-> (Word64 -> Literal)
-> Arrows (Domains (Word64 -> Literal)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
7 Word64 -> Literal
LitWord64 Word64
a

  value :: Word32 -> R Literal
value = (Node -> R Literal) -> Word32 -> R Literal
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R Literal
valu where
    valu :: Node -> R Literal
valu (N1 Word32
a)     = (Integer -> Literal)
-> Arrows
     (Constant Word32 (Domains (Integer -> Literal)))
     (R (CoDomain (Integer -> Literal)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Integer -> Literal
LitNat    Word32
a
    valu (N2 Word32
1 Word32
a)   = (PrecedenceLevel -> Literal)
-> Arrows
     (Constant Word32 (Domains (PrecedenceLevel -> Literal)))
     (R (CoDomain (PrecedenceLevel -> Literal)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN PrecedenceLevel -> Literal
LitFloat  Word32
a
    valu (N2 Word32
2 Word32
a)   = (Text -> Literal)
-> Arrows
     (Constant Word32 (Domains (Text -> Literal)))
     (R (CoDomain (Text -> Literal)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Text -> Literal
LitString Word32
a
    valu (N2 Word32
3 Word32
a)   = (Char -> Literal)
-> Arrows
     (Constant Word32 (Domains (Char -> Literal)))
     (R (CoDomain (Char -> Literal)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Char -> Literal
LitChar   Word32
a
    valu (N2 Word32
5 Word32
a)   = (QName -> Literal)
-> Arrows
     (Constant Word32 (Domains (QName -> Literal)))
     (R (CoDomain (QName -> Literal)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN QName -> Literal
LitQName  Word32
a
    valu (N3 Word32
6 Word32
a Word32
b) = (TopLevelModuleName -> MetaId -> Literal)
-> Arrows
     (Constant
        Word32 (Domains (TopLevelModuleName -> MetaId -> Literal)))
     (R (CoDomain (TopLevelModuleName -> MetaId -> Literal)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN TopLevelModuleName -> MetaId -> Literal
LitMeta   Word32
a Word32
b
    valu (N2 Word32
7 Word32
a)   = (Word64 -> Literal)
-> Arrows
     (Constant Word32 (Domains (Word64 -> Literal)))
     (R (CoDomain (Word64 -> Literal)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Word64 -> Literal
LitWord64 Word32
a
    valu Node
_          = R Literal
forall a. HasCallStack => R a
malformed

instance EmbPrj IsAbstract where
  icod_ :: IsAbstract -> S Word32
icod_ IsAbstract
AbstractDef = Word32 -> IsAbstract -> Arrows (Domains IsAbstract) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 IsAbstract
AbstractDef
  icod_ IsAbstract
ConcreteDef = IsAbstract -> Arrows (Domains IsAbstract) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' IsAbstract
ConcreteDef

  value :: Word32 -> R IsAbstract
value = (Node -> R IsAbstract) -> Word32 -> R IsAbstract
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R IsAbstract
valu where
    valu :: Node
-> Arrows
     (Constant Word32 (Domains IsAbstract)) (R (CoDomain IsAbstract))
valu (N1 Word32
0) = IsAbstract
-> Arrows
     (Constant Word32 (Domains IsAbstract)) (R (CoDomain IsAbstract))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN IsAbstract
AbstractDef
    valu Node
N0     = IsAbstract
-> Arrows
     (Constant Word32 (Domains IsAbstract)) (R (CoDomain IsAbstract))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN IsAbstract
ConcreteDef
    valu Node
_      = R IsAbstract
Arrows
  (Constant Word32 (Domains IsAbstract)) (R (CoDomain IsAbstract))
forall a. HasCallStack => R a
malformed

instance EmbPrj IsOpaque where
  icod_ :: IsOpaque -> S Word32
icod_ (OpaqueDef OpaqueId
a)  = (OpaqueId -> IsOpaque)
-> Arrows (Domains (OpaqueId -> IsOpaque)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' OpaqueId -> IsOpaque
OpaqueDef OpaqueId
a
  icod_ IsOpaque
TransparentDef = IsOpaque -> Arrows (Domains IsOpaque) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' IsOpaque
TransparentDef

  value :: Word32 -> R IsOpaque
value = (Node -> R IsOpaque) -> Word32 -> R IsOpaque
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R IsOpaque
valu where
    valu :: Node -> R IsOpaque
valu (N1 Word32
a) = (OpaqueId -> IsOpaque)
-> Arrows
     (Constant Word32 (Domains (OpaqueId -> IsOpaque)))
     (R (CoDomain (OpaqueId -> IsOpaque)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN OpaqueId -> IsOpaque
OpaqueDef Word32
a
    valu Node
N0     = IsOpaque
-> Arrows
     (Constant Word32 (Domains IsOpaque)) (R (CoDomain IsOpaque))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN IsOpaque
TransparentDef
    valu Node
_      = R IsOpaque
forall a. HasCallStack => R a
malformed

instance EmbPrj SrcLoc where
  icod_ :: SrcLoc -> S Word32
icod_ (SrcLoc String
p String
m String
f Int
sl Int
sc Int
el Int
ec) = (String -> String -> String -> Int -> Int -> Int -> Int -> SrcLoc)
-> Arrows
     (Domains
        (String -> String -> String -> Int -> Int -> Int -> Int -> SrcLoc))
     (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' String -> String -> String -> Int -> Int -> Int -> Int -> SrcLoc
SrcLoc String
p String
m String
f Int
sl Int
sc Int
el Int
ec
  value :: Word32 -> R SrcLoc
value = (String -> String -> String -> Int -> Int -> Int -> Int -> SrcLoc)
-> Word32
-> R (CoDomain
        (String -> String -> String -> Int -> Int -> Int -> Int -> SrcLoc))
forall t.
(VALU t (Arity t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN String -> String -> String -> Int -> Int -> Int -> Int -> SrcLoc
SrcLoc

instance EmbPrj CallStack where
  icod_ :: CallStack -> S Word32
icod_ = [(String, SrcLoc)] -> S Word32
forall a. EmbPrj a => a -> S Word32
icode ([(String, SrcLoc)] -> S Word32)
-> (CallStack -> [(String, SrcLoc)]) -> CallStack -> S Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> [(String, SrcLoc)]
getCallStack
  value :: Word32 -> R CallStack
value = ([(String, SrcLoc)] -> CallStack)
-> ReaderT Decode IO [(String, SrcLoc)] -> R CallStack
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
(<$!>) [(String, SrcLoc)] -> CallStack
fromCallSiteList (ReaderT Decode IO [(String, SrcLoc)] -> R CallStack)
-> (Word32 -> ReaderT Decode IO [(String, SrcLoc)])
-> Word32
-> R CallStack
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> ReaderT Decode IO [(String, SrcLoc)]
forall a. EmbPrj a => Word32 -> R a
value

instance EmbPrj Impossible where
  icod_ :: Impossible -> S Word32
icod_ (Impossible CallStack
a)              = Word32
-> (CallStack -> Impossible)
-> Arrows (Domains (CallStack -> Impossible)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 CallStack -> Impossible
Impossible CallStack
a
  icod_ (Unreachable CallStack
a)             = Word32
-> (CallStack -> Impossible)
-> Arrows (Domains (CallStack -> Impossible)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 CallStack -> Impossible
Unreachable CallStack
a
  icod_ (ImpMissingDefinitions [String]
a String
b) = Word32
-> ([String] -> String -> Impossible)
-> Arrows (Domains ([String] -> String -> Impossible)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
2 [String] -> String -> Impossible
ImpMissingDefinitions [String]
a String
b

  value :: Word32 -> R Impossible
value = (Node -> R Impossible) -> Word32 -> R Impossible
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R Impossible
valu where
    valu :: Node -> R Impossible
valu (N2 Word32
0 Word32
a)   = (CallStack -> Impossible)
-> Arrows
     (Constant Word32 (Domains (CallStack -> Impossible)))
     (R (CoDomain (CallStack -> Impossible)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN CallStack -> Impossible
Impossible  Word32
a
    valu (N2 Word32
1 Word32
a)   = (CallStack -> Impossible)
-> Arrows
     (Constant Word32 (Domains (CallStack -> Impossible)))
     (R (CoDomain (CallStack -> Impossible)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN CallStack -> Impossible
Unreachable Word32
a
    valu (N3 Word32
2 Word32
a Word32
b) = ([String] -> String -> Impossible)
-> Arrows
     (Constant Word32 (Domains ([String] -> String -> Impossible)))
     (R (CoDomain ([String] -> String -> Impossible)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN [String] -> String -> Impossible
ImpMissingDefinitions Word32
a Word32
b
    valu Node
_          = R Impossible
forall a. HasCallStack => R a
malformed

instance EmbPrj ExpandedEllipsis where
  icod_ :: ExpandedEllipsis -> S Word32
icod_ ExpandedEllipsis
NoEllipsis = ExpandedEllipsis -> Arrows (Domains ExpandedEllipsis) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' ExpandedEllipsis
NoEllipsis
  icod_ (ExpandedEllipsis Range
a Int
b) = Word32
-> (Range -> Int -> ExpandedEllipsis)
-> Arrows (Domains (Range -> Int -> ExpandedEllipsis)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 Range -> Int -> ExpandedEllipsis
ExpandedEllipsis Range
a Int
b

  value :: Word32 -> R ExpandedEllipsis
value = (Node -> R ExpandedEllipsis) -> Word32 -> R ExpandedEllipsis
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R ExpandedEllipsis
valu where
    valu :: Node
-> Arrows
     (Constant Word32 (Domains ExpandedEllipsis))
     (R (CoDomain ExpandedEllipsis))
valu Node
N0         = ExpandedEllipsis
-> Arrows
     (Constant Word32 (Domains ExpandedEllipsis))
     (R (CoDomain ExpandedEllipsis))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN ExpandedEllipsis
NoEllipsis
    valu (N3 Word32
1 Word32
a Word32
b) = (Range -> Int -> ExpandedEllipsis)
-> Arrows
     (Constant Word32 (Domains (Range -> Int -> ExpandedEllipsis)))
     (R (CoDomain (Range -> Int -> ExpandedEllipsis)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Range -> Int -> ExpandedEllipsis
ExpandedEllipsis Word32
a Word32
b
    valu Node
_          = R ExpandedEllipsis
Arrows
  (Constant Word32 (Domains ExpandedEllipsis))
  (R (CoDomain ExpandedEllipsis))
forall a. HasCallStack => R a
malformed

instance EmbPrj OptionsPragma where
  icod_ :: OptionsPragma -> S Word32
icod_ (OptionsPragma [String]
a Range
b) = ([String], Range) -> S Word32
forall a. EmbPrj a => a -> S Word32
icod_ ([String]
a, Range
b)

  value :: Word32 -> R OptionsPragma
value Word32
op = ([String] -> Range -> OptionsPragma)
-> ([String], Range) -> OptionsPragma
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [String] -> Range -> OptionsPragma
OptionsPragma (([String], Range) -> OptionsPragma)
-> ReaderT Decode IO ([String], Range) -> R OptionsPragma
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Word32 -> ReaderT Decode IO ([String], Range)
forall a. EmbPrj a => Word32 -> R a
value Word32
op

instance EmbPrj BuiltinId
instance EmbPrj PrimitiveId

instance EmbPrj SomeBuiltin where
  icod_ :: SomeBuiltin -> S Word32
icod_ (BuiltinName BuiltinId
x)   = Word32
-> (BuiltinId -> SomeBuiltin)
-> Arrows (Domains (BuiltinId -> SomeBuiltin)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 BuiltinId -> SomeBuiltin
BuiltinName BuiltinId
x
  icod_ (PrimitiveName PrimitiveId
x) = Word32
-> (PrimitiveId -> SomeBuiltin)
-> Arrows (Domains (PrimitiveId -> SomeBuiltin)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 PrimitiveId -> SomeBuiltin
PrimitiveName PrimitiveId
x

  value :: Word32 -> R SomeBuiltin
value = (Node -> R SomeBuiltin) -> Word32 -> R SomeBuiltin
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R SomeBuiltin
valu where
    valu :: Node -> R SomeBuiltin
valu (N2 Word32
0 Word32
x) = (BuiltinId -> SomeBuiltin)
-> Arrows
     (Constant Word32 (Domains (BuiltinId -> SomeBuiltin)))
     (R (CoDomain (BuiltinId -> SomeBuiltin)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN BuiltinId -> SomeBuiltin
BuiltinName Word32
x
    valu (N2 Word32
1 Word32
x) = (PrimitiveId -> SomeBuiltin)
-> Arrows
     (Constant Word32 (Domains (PrimitiveId -> SomeBuiltin)))
     (R (CoDomain (PrimitiveId -> SomeBuiltin)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN PrimitiveId -> SomeBuiltin
PrimitiveName Word32
x
    valu Node
_        = R SomeBuiltin
forall a. HasCallStack => R a
malformed

instance EmbPrj IsInstance where
  icod_ :: IsInstance -> S Word32
icod_ = \case
    InstanceDef KwRange
a  -> (KwRange -> IsInstance)
-> Arrows (Domains (KwRange -> IsInstance)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' KwRange -> IsInstance
InstanceDef KwRange
a
    IsInstance
NotInstanceDef -> IsInstance -> Arrows (Domains IsInstance) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' IsInstance
NotInstanceDef

  value :: Word32 -> R IsInstance
value = (Node -> R IsInstance) -> Word32 -> R IsInstance
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase \case
    N1 Word32
a -> (KwRange -> IsInstance)
-> Arrows
     (Constant Word32 (Domains (KwRange -> IsInstance)))
     (R (CoDomain (KwRange -> IsInstance)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN KwRange -> IsInstance
InstanceDef Word32
a
    Node
N0   -> IsInstance
-> Arrows
     (Constant Word32 (Domains IsInstance)) (R (CoDomain IsInstance))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN IsInstance
NotInstanceDef
    Node
_    -> R IsInstance
forall a. HasCallStack => R a
malformed

instance EmbPrj a => EmbPrj (RecordDirectives' a) where
  icod_ :: RecordDirectives' a -> S Word32
icod_ (RecordDirectives Maybe (Ranged Induction)
a Maybe (Ranged HasEta0)
b Maybe Range
c a
d) = (Maybe (Ranged Induction)
 -> Maybe (Ranged HasEta0)
 -> Maybe Range
 -> a
 -> RecordDirectives' a)
-> Arrows
     (Domains
        (Maybe (Ranged Induction)
         -> Maybe (Ranged HasEta0)
         -> Maybe Range
         -> a
         -> RecordDirectives' a))
     (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Maybe (Ranged Induction)
-> Maybe (Ranged HasEta0)
-> Maybe Range
-> a
-> RecordDirectives' a
forall a.
Maybe (Ranged Induction)
-> Maybe (Ranged HasEta0)
-> Maybe Range
-> a
-> RecordDirectives' a
RecordDirectives Maybe (Ranged Induction)
a Maybe (Ranged HasEta0)
b Maybe Range
c a
d

  value :: Word32 -> R (RecordDirectives' a)
value = (Node -> R (RecordDirectives' a))
-> Word32 -> R (RecordDirectives' a)
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase \case
    N4 Word32
a Word32
b Word32
c Word32
d -> (Maybe (Ranged Induction)
 -> Maybe (Ranged HasEta0)
 -> Maybe Range
 -> a
 -> RecordDirectives' a)
-> Arrows
     (Constant
        Word32
        (Domains
           (Maybe (Ranged Induction)
            -> Maybe (Ranged HasEta0)
            -> Maybe Range
            -> a
            -> RecordDirectives' a)))
     (R (CoDomain
           (Maybe (Ranged Induction)
            -> Maybe (Ranged HasEta0)
            -> Maybe Range
            -> a
            -> RecordDirectives' a)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Maybe (Ranged Induction)
-> Maybe (Ranged HasEta0)
-> Maybe Range
-> a
-> RecordDirectives' a
forall a.
Maybe (Ranged Induction)
-> Maybe (Ranged HasEta0)
-> Maybe Range
-> a
-> RecordDirectives' a
RecordDirectives Word32
a Word32
b Word32
c Word32
d
    Node
_ -> R (RecordDirectives' a)
forall a. HasCallStack => R a
malformed

instance EmbPrj RecordDirective where
  icod_ :: RecordDirective -> S Word32
icod_ = \case
    Constructor Name
a IsInstance
b      -> Word32
-> (Name -> IsInstance -> RecordDirective)
-> Arrows
     (Domains (Name -> IsInstance -> RecordDirective)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 Name -> IsInstance -> RecordDirective
Constructor Name
a IsInstance
b
    Eta Ranged HasEta0
a                -> Word32
-> (Ranged HasEta0 -> RecordDirective)
-> Arrows (Domains (Ranged HasEta0 -> RecordDirective)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 Ranged HasEta0 -> RecordDirective
Eta Ranged HasEta0
a
    Induction Ranged Induction
a          -> Word32
-> (Ranged Induction -> RecordDirective)
-> Arrows
     (Domains (Ranged Induction -> RecordDirective)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
2 Ranged Induction -> RecordDirective
Induction Ranged Induction
a
    PatternOrCopattern Range
a -> Word32
-> (Range -> RecordDirective)
-> Arrows (Domains (Range -> RecordDirective)) (S Word32)
forall t.
(ICODE (Word32 -> t) (Arity (Word32 -> t)),
 StrictCurrying (Domains (Word32 -> t)) (S Word32),
 All EmbPrj (Domains (Word32 -> t))) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
3 Range -> RecordDirective
PatternOrCopattern Range
a

  value :: Word32 -> R RecordDirective
value = (Node -> R RecordDirective) -> Word32 -> R RecordDirective
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase \case
    (N3 Word32
0 Word32
a Word32
b) -> (Name -> IsInstance -> RecordDirective)
-> Arrows
     (Constant Word32 (Domains (Name -> IsInstance -> RecordDirective)))
     (R (CoDomain (Name -> IsInstance -> RecordDirective)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Name -> IsInstance -> RecordDirective
Constructor Word32
a Word32
b
    (N2 Word32
1 Word32
a)   -> (Ranged HasEta0 -> RecordDirective)
-> Arrows
     (Constant Word32 (Domains (Ranged HasEta0 -> RecordDirective)))
     (R (CoDomain (Ranged HasEta0 -> RecordDirective)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Ranged HasEta0 -> RecordDirective
Eta Word32
a
    (N2 Word32
2 Word32
a)   -> (Ranged Induction -> RecordDirective)
-> Arrows
     (Constant Word32 (Domains (Ranged Induction -> RecordDirective)))
     (R (CoDomain (Ranged Induction -> RecordDirective)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Ranged Induction -> RecordDirective
Induction Word32
a
    (N2 Word32
3 Word32
a)   -> (Range -> RecordDirective)
-> Arrows
     (Constant Word32 (Domains (Range -> RecordDirective)))
     (R (CoDomain (Range -> RecordDirective)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Range -> RecordDirective
PatternOrCopattern Word32
a
    Node
_ -> R RecordDirective
forall a. HasCallStack => R a
malformed

instance EmbPrj Catchall where
  icod_ :: Catchall -> S Word32
icod_ Catchall
NoCatchall  = Catchall -> Arrows (Domains Catchall) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Catchall
NoCatchall
  icod_ (YesCatchall Range
x) = (Range -> Catchall)
-> Arrows (Domains (Range -> Catchall)) (S Word32)
forall t.
(ICODE t (Arity t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Range -> Catchall
YesCatchall Range
x

  value :: Word32 -> R Catchall
value = (Node -> R Catchall) -> Word32 -> R Catchall
forall a. EmbPrj a => (Node -> R a) -> Word32 -> R a
vcase Node -> R Catchall
valu where
    valu :: Node
-> Arrows
     (Constant Word32 (Domains Catchall)) (R (CoDomain Catchall))
valu Node
N0     = Catchall
-> Arrows
     (Constant Word32 (Domains Catchall)) (R (CoDomain Catchall))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Catchall
NoCatchall
    valu (N1 Word32
x) = (Range -> Catchall)
-> Arrows
     (Constant Word32 (Domains (Range -> Catchall)))
     (R (CoDomain (Range -> Catchall)))
forall t.
(VALU t (Arity t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Range -> Catchall
YesCatchall Word32
x
    valu Node
_      = R Catchall
Arrows (Constant Word32 (Domains Catchall)) (R (CoDomain Catchall))
forall a. HasCallStack => R a
malformed