{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE UndecidableInstances #-}
module Agda.TypeChecking.Serialise.Instances.Common (SerialisedRange(..)) where
import Control.Monad ( (<=<) )
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.Except ( MonadError(..) )
import Control.Monad.Reader ( MonadReader(..), asks )
import Control.Monad.State.Strict ( gets, modify )
import Data.Array.IArray
import Data.Word
import qualified Data.Foldable as Fold
import Data.Hashable
import Data.Int (Int32)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.IntSet as IntSet
import Data.IntSet (IntSet)
import qualified Data.Set as Set
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.Strict.Tuple (Pair(..))
import qualified Data.Text as T
import qualified Data.Text.Lazy as TL
import Data.Typeable
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HMap
import Data.Void
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name as C
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.TypeChecking.Serialise.Base
import Agda.Utils.BiMap (BiMap)
import qualified Agda.Utils.BiMap as BiMap
import qualified Agda.Utils.Empty as Empty
import Agda.Utils.FileName
import qualified Agda.Utils.HashTable as H
import Agda.Utils.List1 (List1)
import qualified Agda.Utils.List1 as List1
import Agda.Utils.List2 (List2(List2))
import qualified Agda.Utils.List2 as List2
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Trie (Trie(..))
import Agda.Utils.WithDefault
import Agda.Utils.Impossible
import Agda.Utils.CallStack
instance {-# OVERLAPPING #-} EmbPrj String where
icod_ :: String -> S Int32
icod_ = String -> S Int32
icodeString
value :: Int32 -> R String
value Int32
i = (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int32
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Int32 String
stringE
instance EmbPrj TL.Text where
icod_ :: Text -> S Int32
icod_ = forall k.
(Eq k, Hashable k) =>
(Dict -> HashTable k Int32)
-> (Dict -> IORef FreshAndReuse) -> k -> S Int32
icodeX Dict -> HashTable Text Int32
lTextD Dict -> IORef FreshAndReuse
lTextC
value :: Int32 -> R Text
value Int32
i = (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int32
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Int32 Text
lTextE
instance EmbPrj T.Text where
icod_ :: Text -> S Int32
icod_ = forall k.
(Eq k, Hashable k) =>
(Dict -> HashTable k Int32)
-> (Dict -> IORef FreshAndReuse) -> k -> S Int32
icodeX Dict -> HashTable Text Int32
sTextD Dict -> IORef FreshAndReuse
sTextC
value :: Int32 -> R Text
value Int32
i = (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int32
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Int32 Text
sTextE
instance EmbPrj Integer where
icod_ :: Integer -> S Int32
icod_ = Integer -> S Int32
icodeInteger
value :: Int32 -> R Integer
value Int32
i = (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int32
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Int32 Integer
integerE
instance EmbPrj Word64 where
icod_ :: Word64 -> S Int32
icod_ Word64
i = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (forall a. HasCallStack => a
undefined :: Int32 -> Int32 -> Int32) (Word64 -> Int32
int32 Word64
q) (Word64 -> Int32
int32 Word64
r)
where (Word64
q, Word64
r) = forall a. Integral a => a -> a -> (a, a)
quotRem Word64
i (Word64
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
32)
int32 :: Word64 -> Int32
int32 :: Word64 -> Int32
int32 = forall a b. (Integral a, Num b) => a -> b
fromIntegral
value :: Int32 -> R Word64
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Word64
valu where
valu :: Node -> R Word64
valu [Int32
a, Int32
b] = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Word64
n forall a. Num a => a -> a -> a
* forall a. Integral a => a -> a -> a
mod (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
a) Word64
n forall a. Num a => a -> a -> a
+ forall a. Integral a => a -> a -> a
mod (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
b) Word64
n
valu Node
_ = forall a. R a
malformed
n :: Word64
n = Word64
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
32
instance EmbPrj Int32 where
icod_ :: Int32 -> S Int32
icod_ Int32
i = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i
value :: Int32 -> R Int32
value Int32
i = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i
instance EmbPrj Int where
icod_ :: Int -> S Int32
icod_ Int
i = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)
value :: Int32 -> R Int
value Int32
i = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
i)
instance EmbPrj Char where
icod_ :: Char -> S Int32
icod_ Char
c = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> Int
fromEnum Char
c)
value :: Int32 -> R Char
value Int32
i = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Enum a => Int -> a
toEnum forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Integer
toInteger Int32
i)
instance EmbPrj Double where
icod_ :: Double -> S Int32
icod_ = Double -> S Int32
icodeDouble
value :: Int32 -> R Double
value Int32
i = (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int32
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Int32 Double
doubleE
instance EmbPrj Void where
icod_ :: Void -> S Int32
icod_ = forall a. Void -> a
absurd
value :: Int32 -> R Void
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {p} {a}. p -> R a
valu where valu :: p -> R a
valu p
_ = forall a. R a
malformed
instance EmbPrj () where
icod_ :: () -> S Int32
icod_ () = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ()
value :: Int32 -> R ()
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {a}. [a] -> R ()
valu where
valu :: [a] -> Arrows (Constant Int32 (Domains ())) (R (CoDomain ()))
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ()
valu [a]
_ = forall a. R a
malformed
instance (EmbPrj a, EmbPrj b) => EmbPrj (a, b) where
icod_ :: (a, b) -> S Int32
icod_ (a
a, b
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (,) a
a b
b
value :: Int32 -> R (a, b)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN (,)
instance (EmbPrj a, EmbPrj b) => EmbPrj (Pair a b) where
icod_ :: Pair a b -> S Int32
icod_ (a
a :!: b
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a b. a -> b -> Pair a b
(:!:) a
a b
b
value :: Int32 -> R (Pair a b)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall a b. a -> b -> Pair a b
(:!:)
instance (EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c) where
icod_ :: (a, b, c) -> S Int32
icod_ (a
a, b
b, c
c) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (,,) a
a b
b c
c
value :: Int32 -> R (a, b, c)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN (,,)
instance (EmbPrj a, EmbPrj b) => EmbPrj (Either a b) where
icod_ :: Either a b -> S Int32
icod_ (Left a
x) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 forall a b. a -> Either a b
Left a
x
icod_ (Right b
x) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 forall a b. b -> Either a b
Right b
x
value :: Int32 -> R (Either a b)
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {a} {b}. (EmbPrj a, EmbPrj b) => Node -> R (Either a b)
valu where
valu :: Node -> R (Either a b)
valu [Int32
0, Int32
x] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a b. a -> Either a b
Left Int32
x
valu [Int32
1, Int32
x] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a b. b -> Either a b
Right Int32
x
valu Node
_ = forall a. R a
malformed
instance EmbPrj a => EmbPrj (Maybe a) where
icod_ :: Maybe a -> S Int32
icod_ Maybe a
Nothing = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Maybe a
Nothing
icod_ (Just a
x) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. a -> Maybe a
Just a
x
value :: Int32 -> R (Maybe a)
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {a}.
EmbPrj a =>
Node -> ExceptT TypeError (StateT St IO) (Maybe a)
valu where
valu :: Node
-> Arrows
(Constant Int32 (Domains (Maybe a))) (R (CoDomain (Maybe a)))
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. Maybe a
Nothing
valu [Int32
x] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> Maybe a
Just Int32
x
valu Node
_ = forall a. R a
malformed
instance EmbPrj a => EmbPrj (Strict.Maybe a) where
icod_ :: Maybe a -> S Int32
icod_ Maybe a
m = forall a. EmbPrj a => a -> S Int32
icode (forall lazy strict. Strict lazy strict => strict -> lazy
Strict.toLazy Maybe a
m)
value :: Int32 -> R (Maybe a)
value Int32
m = forall lazy strict. Strict lazy strict => lazy -> strict
Strict.toStrict forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. EmbPrj a => Int32 -> R a
value Int32
m
instance EmbPrj Bool where
icod_ :: Bool -> S Int32
icod_ Bool
True = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Bool
True
icod_ Bool
False = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Bool
False
value :: Int32 -> R Bool
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {a}. (Eq a, Num a) => [a] -> R Bool
valu where
valu :: [a] -> Arrows (Constant Int32 (Domains Bool)) (R (CoDomain Bool))
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Bool
True
valu [a
0] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Bool
False
valu [a]
_ = forall a. R a
malformed
instance EmbPrj FileType where
icod_ :: FileType -> S Int32
icod_ FileType
AgdaFileType = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' FileType
AgdaFileType
icod_ FileType
MdFileType = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 FileType
MdFileType
icod_ FileType
RstFileType = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 FileType
RstFileType
icod_ FileType
TexFileType = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 FileType
TexFileType
icod_ FileType
OrgFileType = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 FileType
OrgFileType
value :: Int32 -> R FileType
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall a b. (a -> b) -> a -> b
$ \case
[] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN FileType
AgdaFileType
[Int32
0] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN FileType
MdFileType
[Int32
1] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN FileType
RstFileType
[Int32
2] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN FileType
TexFileType
[Int32
3] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN FileType
OrgFileType
Node
_ -> forall a. R a
malformed
instance EmbPrj Cubical where
icod_ :: Cubical -> S Int32
icod_ Cubical
CErased = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Cubical
CErased
icod_ Cubical
CFull = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Cubical
CFull
value :: Int32 -> R Cubical
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall a b. (a -> b) -> a -> b
$ \case
[] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Cubical
CErased
[Int32
0] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Cubical
CFull
Node
_ -> forall a. R a
malformed
instance EmbPrj Language where
icod_ :: Language -> S Int32
icod_ Language
WithoutK = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Language
WithoutK
icod_ Language
WithK = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Language
WithK
icod_ (Cubical Cubical
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Cubical -> Language
Cubical Cubical
a
value :: Int32 -> R Language
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall a b. (a -> b) -> a -> b
$ \case
[] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Language
WithoutK
[Int32
0] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Language
WithK
[Int32
1, Int32
a] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Cubical -> Language
Cubical Int32
a
Node
_ -> forall a. R a
malformed
instance EmbPrj a => EmbPrj (Position' a) where
icod_ :: Position' a -> S Int32
icod_ (P.Pn a
file Int32
pos Int32
line Int32
col) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. a -> Int32 -> Int32 -> Int32 -> Position' a
P.Pn a
file Int32
pos Int32
line Int32
col
value :: Int32 -> R (Position' a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall a. a -> Int32 -> Int32 -> Int32 -> Position' a
P.Pn
instance Typeable b => EmbPrj (WithDefault b) where
icod_ :: WithDefault b -> S Int32
icod_ = \case
WithDefault b
Default -> forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall (b :: Bool). WithDefault b
Default
Value Bool
b -> forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall (b :: Bool). Bool -> WithDefault b
Value Bool
b
value :: Int32 -> R (WithDefault b)
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall a b. (a -> b) -> a -> b
$ \case
[] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall (b :: Bool). WithDefault b
Default
[Int32
a] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall (b :: Bool). Bool -> WithDefault b
Value Int32
a
Node
_ -> forall a. R a
malformed
instance EmbPrj TopLevelModuleName where
icod_ :: TopLevelModuleName -> S Int32
icod_ (TopLevelModuleName Range
a ModuleNameHash
b TopLevelModuleNameParts
c) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Range
-> ModuleNameHash -> TopLevelModuleNameParts -> TopLevelModuleName
TopLevelModuleName Range
a ModuleNameHash
b TopLevelModuleNameParts
c
value :: Int32 -> R TopLevelModuleName
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Range
-> ModuleNameHash -> TopLevelModuleNameParts -> TopLevelModuleName
TopLevelModuleName
instance {-# OVERLAPPABLE #-} EmbPrj a => EmbPrj [a] where
icod_ :: [a] -> S Int32
icod_ [a]
xs = Node -> S Int32
icodeNode forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. EmbPrj a => a -> S Int32
icode [a]
xs
value :: Int32 -> R [a]
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. EmbPrj a => Int32 -> R a
value)
instance EmbPrj a => EmbPrj (List1 a) where
icod_ :: List1 a -> S Int32
icod_ = forall a. EmbPrj a => a -> S Int32
icod_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. IsList l => l -> [Item l]
List1.toList
value :: Int32 -> R (List1 a)
value = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. R a
malformed forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Maybe (NonEmpty a)
List1.nonEmpty forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. EmbPrj a => Int32 -> R a
value
instance EmbPrj a => EmbPrj (List2 a) where
icod_ :: List2 a -> S Int32
icod_ = forall a. EmbPrj a => a -> S Int32
icod_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. IsList l => l -> [Item l]
List2.toList
value :: Int32 -> R (List2 a)
value = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. R a
malformed forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Maybe (List2 a)
List2.fromListMaybe forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< forall a. EmbPrj a => Int32 -> R a
value
instance (EmbPrj k, EmbPrj v, EmbPrj (BiMap.Tag v)) =>
EmbPrj (BiMap k v) where
icod_ :: BiMap k v -> S Int32
icod_ BiMap k v
m = forall a. EmbPrj a => a -> S Int32
icode (forall k v. BiMap k v -> ([(k, v)], [(Tag v, k)])
BiMap.toDistinctAscendingLists BiMap k v
m)
value :: Int32 -> R (BiMap k v)
value Int32
m = forall k v. ([(k, v)], [(Tag v, k)]) -> BiMap k v
BiMap.fromDistinctAscendingLists forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. EmbPrj a => Int32 -> R a
value Int32
m
mapPairsIcode :: (EmbPrj k, EmbPrj v) => [(k, v)] -> S Int32
mapPairsIcode :: forall k v. (EmbPrj k, EmbPrj v) => [(k, v)] -> S Int32
mapPairsIcode [(k, v)]
xs = Node -> S Int32
icodeNode forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall {a} {a}.
(EmbPrj a, EmbPrj a) =>
Node -> [(a, a)] -> ReaderT Dict IO Node
convert [] [(k, v)]
xs where
convert :: Node -> [(a, a)] -> ReaderT Dict IO Node
convert Node
ys [] = forall (m :: * -> *) a. Monad m => a -> m a
return Node
ys
convert Node
ys ((a
start, a
entry):[(a, a)]
xs) = do
Int32
start <- forall a. EmbPrj a => a -> S Int32
icode a
start
Int32
entry <- forall a. EmbPrj a => a -> S Int32
icode a
entry
Node -> [(a, a)] -> ReaderT Dict IO Node
convert (Int32
startforall a. a -> [a] -> [a]
:Int32
entryforall a. a -> [a] -> [a]
:Node
ys) [(a, a)]
xs
mapPairsValue :: (EmbPrj k, EmbPrj v) => [Int32] -> R [(k, v)]
mapPairsValue :: forall k v. (EmbPrj k, EmbPrj v) => Node -> R [(k, v)]
mapPairsValue = forall {a} {b}.
(EmbPrj a, EmbPrj b) =>
[(a, b)] -> Node -> ExceptT TypeError (StateT St IO) [(a, b)]
convert [] where
convert :: [(a, b)] -> Node -> ExceptT TypeError (StateT St IO) [(a, b)]
convert [(a, b)]
ys [] = forall (m :: * -> *) a. Monad m => a -> m a
return [(a, b)]
ys
convert [(a, b)]
ys (Int32
start:Int32
entry:Node
xs) = do
a
start <- forall a. EmbPrj a => Int32 -> R a
value Int32
start
b
entry <- forall a. EmbPrj a => Int32 -> R a
value Int32
entry
[(a, b)] -> Node -> ExceptT TypeError (StateT St IO) [(a, b)]
convert ((a
start, b
entry)forall a. a -> [a] -> [a]
:[(a, b)]
ys) Node
xs
convert [(a, b)]
_ Node
_ = forall a. R a
malformed
instance (Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) where
icod_ :: Map a b -> S Int32
icod_ Map a b
m = forall k v. (EmbPrj k, EmbPrj v) => [(k, v)] -> S Int32
mapPairsIcode (forall k a. Map k a -> [(k, a)]
Map.toAscList Map a b
m)
value :: Int32 -> R (Map a b)
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (EmbPrj k, EmbPrj v) => Node -> R [(k, v)]
mapPairsValue)
instance (Ord a, EmbPrj a) => EmbPrj (Set a) where
icod_ :: Set a -> S Int32
icod_ Set a
s = forall a. EmbPrj a => a -> S Int32
icode (forall a. Set a -> [a]
Set.toAscList Set a
s)
value :: Int32 -> R (Set a)
value Int32
s = forall a. [a] -> Set a
Set.fromDistinctAscList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. EmbPrj a => Int32 -> R a
value Int32
s
instance EmbPrj IntSet where
icod_ :: IntSet -> S Int32
icod_ IntSet
s = forall a. EmbPrj a => a -> S Int32
icode (IntSet -> [Int]
IntSet.toAscList IntSet
s)
value :: Int32 -> R IntSet
value Int32
s = [Int] -> IntSet
IntSet.fromDistinctAscList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. EmbPrj a => Int32 -> R a
value Int32
s
instance (Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Trie a b) where
icod_ :: Trie a b -> S Int32
icod_ (Trie Maybe b
a Map a (Trie a b)
b)= forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall k v. Maybe v -> Map k (Trie k v) -> Trie k v
Trie Maybe b
a Map a (Trie a b)
b
value :: Int32 -> R (Trie a b)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall k v. Maybe v -> Map k (Trie k v) -> Trie k v
Trie
instance EmbPrj a => EmbPrj (Seq a) where
icod_ :: Seq a -> S Int32
icod_ Seq a
s = forall a. EmbPrj a => a -> S Int32
icode (forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq a
s)
value :: Int32 -> R (Seq a)
value Int32
s = forall a. [a] -> Seq a
Seq.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. EmbPrj a => Int32 -> R a
value Int32
s
instance EmbPrj a => EmbPrj (P.Interval' a) where
icod_ :: Interval' a -> S Int32
icod_ (P.Interval Position' a
p Position' a
q) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Position' a -> Position' a -> Interval' a
P.Interval Position' a
p Position' a
q
value :: Int32 -> R (Interval' a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall a. Position' a -> Position' a -> Interval' a
P.Interval
instance EmbPrj RangeFile where
icod_ :: RangeFile -> S Int32
icod_ (RangeFile AbsolutePath
_ Maybe TopLevelModuleName
Nothing) = forall a. HasCallStack => a
__IMPOSSIBLE__
icod_ (RangeFile AbsolutePath
_ (Just TopLevelModuleName
a)) = forall a. EmbPrj a => a -> S Int32
icode TopLevelModuleName
a
value :: Int32 -> R RangeFile
value Int32
r = do
TopLevelModuleName
m :: TopLevelModuleName
<- forall a. EmbPrj a => Int32 -> R a
value Int32
r
ModuleToSource
mf <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> ModuleToSource
modFile
[AbsolutePath]
incs <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> [AbsolutePath]
includes
(Either FindError SourceFile
r, ModuleToSource
mf) <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [AbsolutePath]
-> TopLevelModuleName
-> ModuleToSource
-> IO (Either FindError SourceFile, ModuleToSource)
findFile'' [AbsolutePath]
incs TopLevelModuleName
m ModuleToSource
mf
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \St
s -> St
s { modFile :: ModuleToSource
modFile = ModuleToSource
mf }
case Either FindError SourceFile
r of
Left FindError
err -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> FindError -> TypeError
findErrorToTypeError TopLevelModuleName
m FindError
err
Right SourceFile
f -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
RangeFile (SourceFile -> AbsolutePath
srcFilePath SourceFile
f) (forall a. a -> Maybe a
Just TopLevelModuleName
m)
instance EmbPrj Range where
icod_ :: Range -> S Int32
icod_ Range
_ = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ()
value :: Int32 -> R Range
value Int32
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Range' a
noRange
newtype SerialisedRange = SerialisedRange { SerialisedRange -> Range
underlyingRange :: Range }
instance EmbPrj SerialisedRange where
icod_ :: SerialisedRange -> S Int32
icod_ (SerialisedRange Range
r) =
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (forall a. HasCallStack => a
undefined :: SrcFile -> [IntervalWithoutFile] -> SerialisedRange)
(Range -> SrcFile
P.rangeFile Range
r) (forall a. Range' a -> [IntervalWithoutFile]
P.rangeIntervals Range
r)
value :: Int32 -> R SerialisedRange
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R SerialisedRange
valu where
valu :: Node -> R SerialisedRange
valu [Int32
a, Int32
b] = Range -> SerialisedRange
SerialisedRange forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> [IntervalWithoutFile] -> Range' a
P.intervalsToRange Int32
a Int32
b
valu Node
_ = forall a. R a
malformed
instance EmbPrj C.Name where
icod_ :: Name -> S Int32
icod_ (C.NoName Range
a NameId
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Range -> NameId -> Name
C.NoName Range
a NameId
b
icod_ (C.Name Range
r NameInScope
nis NameParts
xs) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Range -> NameInScope -> NameParts -> Name
C.Name Range
r NameInScope
nis NameParts
xs
value :: Int32 -> R Name
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Name
valu where
valu :: Node -> R Name
valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Range -> NameId -> Name
C.NoName Int32
a Int32
b
valu [Int32
1, Int32
r, Int32
nis, Int32
xs] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Range -> NameInScope -> NameParts -> Name
C.Name Int32
r Int32
nis Int32
xs
valu Node
_ = forall a. R a
malformed
instance EmbPrj NamePart where
icod_ :: NamePart -> S Int32
icod_ NamePart
Hole = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' NamePart
Hole
icod_ (Id String
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' String -> NamePart
Id String
a
value :: Int32 -> R NamePart
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R NamePart
valu where
valu :: Node
-> Arrows
(Constant Int32 (Domains NamePart)) (R (CoDomain NamePart))
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NamePart
Hole
valu [Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN String -> NamePart
Id Int32
a
valu Node
_ = forall a. R a
malformed
instance EmbPrj NameInScope where
icod_ :: NameInScope -> S Int32
icod_ NameInScope
InScope = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' NameInScope
InScope
icod_ NameInScope
NotInScope = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 NameInScope
NotInScope
value :: Int32 -> R NameInScope
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {a}. (Eq a, Num a) => [a] -> R NameInScope
valu where
valu :: [a]
-> Arrows
(Constant Int32 (Domains NameInScope)) (R (CoDomain NameInScope))
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NameInScope
InScope
valu [a
0] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN NameInScope
NotInScope
valu [a]
_ = forall a. R a
malformed
instance EmbPrj C.QName where
icod_ :: QName -> S Int32
icod_ (Qual Name
a QName
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Name -> QName -> QName
Qual Name
a QName
b
icod_ (C.QName Name
a ) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Name -> QName
C.QName Name
a
value :: Int32 -> R QName
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R QName
valu where
valu :: Node -> R QName
valu [Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Name -> QName -> QName
Qual Int32
a Int32
b
valu [Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Name -> QName
C.QName Int32
a
valu Node
_ = forall a. R a
malformed
instance (EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) where
icod_ :: ImportedName' a b -> S Int32
icod_ (ImportedModule b
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 forall n m. m -> ImportedName' n m
ImportedModule b
a
icod_ (ImportedName a
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 forall n m. n -> ImportedName' n m
ImportedName a
a
value :: Int32 -> R (ImportedName' a b)
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {m} {n}.
(EmbPrj m, EmbPrj n) =>
Node -> R (ImportedName' n m)
valu where
valu :: Node -> R (ImportedName' n m)
valu [Int32
1, Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall n m. m -> ImportedName' n m
ImportedModule Int32
a
valu [Int32
2, Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall n m. n -> ImportedName' n m
ImportedName Int32
a
valu Node
_ = forall a. R a
malformed
instance EmbPrj Associativity where
icod_ :: Associativity -> S Int32
icod_ Associativity
LeftAssoc = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Associativity
LeftAssoc
icod_ Associativity
RightAssoc = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Associativity
RightAssoc
icod_ Associativity
NonAssoc = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Associativity
NonAssoc
value :: Int32 -> R Associativity
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {a}. (Eq a, Num a) => [a] -> R Associativity
valu where
valu :: [a]
-> Arrows
(Constant Int32 (Domains Associativity))
(R (CoDomain Associativity))
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Associativity
LeftAssoc
valu [a
1] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Associativity
RightAssoc
valu [a
2] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Associativity
NonAssoc
valu [a]
_ = forall a. R a
malformed
instance EmbPrj FixityLevel where
icod_ :: FixityLevel -> S Int32
icod_ FixityLevel
Unrelated = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' FixityLevel
Unrelated
icod_ (Related Double
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Double -> FixityLevel
Related Double
a
value :: Int32 -> R FixityLevel
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R FixityLevel
valu where
valu :: Node
-> Arrows
(Constant Int32 (Domains FixityLevel)) (R (CoDomain FixityLevel))
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN FixityLevel
Unrelated
valu [Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Double -> FixityLevel
Related Int32
a
valu Node
_ = forall a. R a
malformed
instance EmbPrj Fixity where
icod_ :: Fixity -> S Int32
icod_ (Fixity Range
a FixityLevel
b Associativity
c) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Range -> FixityLevel -> Associativity -> Fixity
Fixity Range
a FixityLevel
b Associativity
c
value :: Int32 -> R Fixity
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Range -> FixityLevel -> Associativity -> Fixity
Fixity
instance EmbPrj Fixity' where
icod_ :: Fixity' -> S Int32
icod_ (Fixity' Fixity
a Notation
b Range
r) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (\ Fixity
a Notation
b -> Fixity -> Notation -> Range -> Fixity'
Fixity' Fixity
a Notation
b Range
r) Fixity
a Notation
b
value :: Int32 -> R Fixity'
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN (\ Fixity
f Notation
n -> Fixity -> Notation -> Range -> Fixity'
Fixity' Fixity
f Notation
n forall a. Range' a
noRange)
instance EmbPrj BoundVariablePosition where
icod_ :: BoundVariablePosition -> S Int32
icod_ (BoundVariablePosition Int
a Int
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Int -> Int -> BoundVariablePosition
BoundVariablePosition Int
a Int
b
value :: Int32 -> R BoundVariablePosition
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Int -> Int -> BoundVariablePosition
BoundVariablePosition
instance EmbPrj NotationPart where
icod_ :: NotationPart -> S Int32
icod_ (VarPart Range
a Ranged BoundVariablePosition
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Range -> Ranged BoundVariablePosition -> NotationPart
VarPart Range
a Ranged BoundVariablePosition
b
icod_ (HolePart Range
a NamedArg (Ranged Int)
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Range -> NamedArg (Ranged Int) -> NotationPart
HolePart Range
a NamedArg (Ranged Int)
b
icod_ (WildPart Ranged BoundVariablePosition
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Ranged BoundVariablePosition -> NotationPart
WildPart Ranged BoundVariablePosition
a
icod_ (IdPart RString
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' RString -> NotationPart
IdPart RString
a
value :: Int32 -> R NotationPart
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R NotationPart
valu where
valu :: Node -> R NotationPart
valu [Int32
0, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Range -> Ranged BoundVariablePosition -> NotationPart
VarPart Int32
a Int32
b
valu [Int32
1, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Range -> NamedArg (Ranged Int) -> NotationPart
HolePart Int32
a Int32
b
valu [Int32
2, Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Ranged BoundVariablePosition -> NotationPart
WildPart Int32
a
valu [Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN RString -> NotationPart
IdPart Int32
a
valu Node
_ = forall a. R a
malformed
instance EmbPrj MetaId where
icod_ :: MetaId -> S Int32
icod_ (MetaId Word64
a ModuleNameHash
b) = forall a. EmbPrj a => a -> S Int32
icode (Word64
a, ModuleNameHash
b)
value :: Int32 -> R MetaId
value Int32
m = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Word64 -> ModuleNameHash -> MetaId
MetaId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. EmbPrj a => Int32 -> R a
value Int32
m
instance EmbPrj A.QName where
icod_ :: QName -> S Int32
icod_ n :: QName
n@(A.QName ModuleName
a Name
b) = forall a.
(Ord a, Hashable a) =>
(Dict -> HashTable a Int32)
-> (Dict -> IORef FreshAndReuse) -> a -> S Int32 -> S Int32
icodeMemo Dict -> HashTable QNameId Int32
qnameD Dict -> IORef FreshAndReuse
qnameC (QName -> QNameId
qnameId QName
n) forall a b. (a -> b) -> a -> b
$ forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ModuleName -> Name -> QName
A.QName ModuleName
a Name
b
value :: Int32 -> R QName
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN ModuleName -> Name -> QName
A.QName
instance EmbPrj A.AmbiguousQName where
icod_ :: AmbiguousQName -> S Int32
icod_ (A.AmbQ List1 QName
a) = forall a. EmbPrj a => a -> S Int32
icode List1 QName
a
value :: Int32 -> R AmbiguousQName
value Int32
n = List1 QName -> AmbiguousQName
A.AmbQ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. EmbPrj a => Int32 -> R a
value Int32
n
instance EmbPrj A.ModuleName where
icod_ :: ModuleName -> S Int32
icod_ (A.MName [Name]
a) = forall a. EmbPrj a => a -> S Int32
icode [Name]
a
value :: Int32 -> R ModuleName
value Int32
n = [Name] -> ModuleName
A.MName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall a. EmbPrj a => Int32 -> R a
value Int32
n
instance EmbPrj A.Name where
icod_ :: Name -> S Int32
icod_ (A.Name NameId
a Name
b Name
c Range
d Fixity'
e Bool
f) = forall a.
(Ord a, Hashable a) =>
(Dict -> HashTable a Int32)
-> (Dict -> IORef FreshAndReuse) -> a -> S Int32 -> S Int32
icodeMemo Dict -> HashTable NameId Int32
nameD Dict -> IORef FreshAndReuse
nameC NameId
a forall a b. (a -> b) -> a -> b
$
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (\ NameId
a Name
b Name
c -> NameId -> Name -> Name -> Range -> Fixity' -> Bool -> Name
A.Name NameId
a Name
b Name
c forall b c a. (b -> c) -> (a -> b) -> a -> c
. SerialisedRange -> Range
underlyingRange) NameId
a Name
b Name
c (Range -> SerialisedRange
SerialisedRange Range
d) Fixity'
e Bool
f
value :: Int32 -> R Name
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN (\NameId
a Name
b Name
c SerialisedRange
d -> NameId -> Name -> Name -> Range -> Fixity' -> Bool -> Name
A.Name NameId
a Name
b Name
c (SerialisedRange -> Range
underlyingRange SerialisedRange
d))
instance EmbPrj a => EmbPrj (C.FieldAssignment' a) where
icod_ :: FieldAssignment' a -> S Int32
icod_ (C.FieldAssignment Name
a a
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Name -> a -> FieldAssignment' a
C.FieldAssignment Name
a a
b
value :: Int32 -> R (FieldAssignment' a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall a. Name -> a -> FieldAssignment' a
C.FieldAssignment
instance (EmbPrj s, EmbPrj t) => EmbPrj (Named s t) where
icod_ :: Named s t -> S Int32
icod_ (Named Maybe s
a t
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall name a. Maybe name -> a -> Named name a
Named Maybe s
a t
b
value :: Int32 -> R (Named s t)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall name a. Maybe name -> a -> Named name a
Named
instance EmbPrj a => EmbPrj (Ranged a) where
icod_ :: Ranged a -> S Int32
icod_ (Ranged Range
r a
x) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Range -> a -> Ranged a
Ranged Range
r a
x
value :: Int32 -> R (Ranged a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall a. Range -> a -> Ranged a
Ranged
instance EmbPrj ArgInfo where
icod_ :: ArgInfo -> S Int32
icod_ (ArgInfo Hiding
h Modality
r Origin
o FreeVariables
fv Annotation
ann) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Hiding
-> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo
ArgInfo Hiding
h Modality
r Origin
o FreeVariables
fv Annotation
ann
value :: Int32 -> R ArgInfo
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Hiding
-> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo
ArgInfo
instance EmbPrj ModuleNameHash where
icod_ :: ModuleNameHash -> S Int32
icod_ (ModuleNameHash Word64
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Word64 -> ModuleNameHash
ModuleNameHash Word64
a
value :: Int32 -> R ModuleNameHash
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Word64 -> ModuleNameHash
ModuleNameHash
instance EmbPrj NameId where
icod_ :: NameId -> S Int32
icod_ (NameId Word64
a ModuleNameHash
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Word64 -> ModuleNameHash -> NameId
NameId Word64
a ModuleNameHash
b
value :: Int32 -> R NameId
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Word64 -> ModuleNameHash -> NameId
NameId
instance (Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v) where
icod_ :: HashMap k v -> S Int32
icod_ HashMap k v
m = forall k v. (EmbPrj k, EmbPrj v) => [(k, v)] -> S Int32
mapPairsIcode (forall k v. HashMap k v -> [(k, v)]
HMap.toList HashMap k v
m)
value :: Int32 -> R (HashMap k v)
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HMap.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (EmbPrj k, EmbPrj v) => Node -> R [(k, v)]
mapPairsValue)
instance EmbPrj a => EmbPrj (WithHiding a) where
icod_ :: WithHiding a -> S Int32
icod_ (WithHiding Hiding
a a
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Hiding -> a -> WithHiding a
WithHiding Hiding
a a
b
value :: Int32 -> R (WithHiding a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall a. Hiding -> a -> WithHiding a
WithHiding
instance EmbPrj a => EmbPrj (Arg a) where
icod_ :: Arg a -> S Int32
icod_ (Arg ArgInfo
i a
e) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i a
e
value :: Int32 -> R (Arg a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall e. ArgInfo -> e -> Arg e
Arg
instance EmbPrj a => EmbPrj (HasEta' a) where
icod_ :: HasEta' a -> S Int32
icod_ HasEta' a
YesEta = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. HasEta' a
YesEta
icod_ (NoEta a
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. a -> HasEta' a
NoEta a
a
value :: Int32 -> R (HasEta' a)
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {a}.
EmbPrj a =>
Node -> ExceptT TypeError (StateT St IO) (HasEta' a)
valu where
valu :: Node
-> Arrows
(Constant Int32 (Domains (HasEta' a))) (R (CoDomain (HasEta' a)))
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. HasEta' a
YesEta
valu [Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN forall a. a -> HasEta' a
NoEta Int32
a
valu Node
_ = forall a. R a
malformed
instance EmbPrj PatternOrCopattern
instance EmbPrj Induction where
icod_ :: Induction -> S Int32
icod_ Induction
Inductive = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Induction
Inductive
icod_ Induction
CoInductive = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Induction
CoInductive
value :: Int32 -> R Induction
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {a}. (Eq a, Num a) => [a] -> R Induction
valu where
valu :: [a]
-> Arrows
(Constant Int32 (Domains Induction)) (R (CoDomain Induction))
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Induction
Inductive
valu [a
1] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Induction
CoInductive
valu [a]
_ = forall a. R a
malformed
instance EmbPrj Hiding where
icod_ :: Hiding -> S Int32
icod_ Hiding
Hidden = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
icod_ Hiding
NotHidden = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
icod_ (Instance Overlappable
NoOverlap) = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
icod_ (Instance Overlappable
YesOverlap) = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
3
value :: Int32 -> R Hiding
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return Hiding
Hidden
value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return Hiding
NotHidden
value Int32
2 = forall (m :: * -> *) a. Monad m => a -> m a
return (Overlappable -> Hiding
Instance Overlappable
NoOverlap)
value Int32
3 = forall (m :: * -> *) a. Monad m => a -> m a
return (Overlappable -> Hiding
Instance Overlappable
YesOverlap)
value Int32
_ = forall a. R a
malformed
instance EmbPrj Q0Origin where
icod_ :: Q0Origin -> S Int32
icod_ = \case
Q0Origin
Q0Inferred -> forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
Q0 Range
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
Q0Erased Range
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
value :: Int32 -> R Q0Origin
value = \case
Int32
0 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Q0Origin
Q0Inferred
Int32
1 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Q0Origin
Q0 forall a. Range' a
noRange
Int32
2 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Q0Origin
Q0Erased forall a. Range' a
noRange
Int32
_ -> forall a. R a
malformed
instance EmbPrj Q1Origin where
icod_ :: Q1Origin -> S Int32
icod_ = \case
Q1Origin
Q1Inferred -> forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
Q1 Range
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
Q1Linear Range
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
value :: Int32 -> R Q1Origin
value = \case
Int32
0 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Q1Origin
Q1Inferred
Int32
1 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Q1Origin
Q1 forall a. Range' a
noRange
Int32
2 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> Q1Origin
Q1Linear forall a. Range' a
noRange
Int32
_ -> forall a. R a
malformed
instance EmbPrj QωOrigin where
icod_ :: QωOrigin -> S Int32
icod_ = \case
QωOrigin
QωInferred -> forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
Qω Range
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
QωPlenty Range
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
value :: Int32 -> R QωOrigin
value = \case
Int32
0 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QωOrigin
QωInferred
Int32
1 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> QωOrigin
Qω forall a. Range' a
noRange
Int32
2 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Range -> QωOrigin
QωPlenty forall a. Range' a
noRange
Int32
_ -> forall a. R a
malformed
instance EmbPrj Quantity where
icod_ :: Quantity -> S Int32
icod_ = \case
Quantity0 Q0Origin
a -> forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Q0Origin -> Quantity
Quantity0 Q0Origin
a
Quantity1 Q1Origin
a -> forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Q1Origin -> Quantity
Quantity1 Q1Origin
a
Quantityω QωOrigin
a -> forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' QωOrigin -> Quantity
Quantityω QωOrigin
a
value :: Int32 -> R Quantity
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall a b. (a -> b) -> a -> b
$ \case
[Int32
0, Int32
a] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Q0Origin -> Quantity
Quantity0 Int32
a
[Int32
1, Int32
a] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Q1Origin -> Quantity
Quantity1 Int32
a
[Int32
a] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QωOrigin -> Quantity
Quantityω Int32
a
Node
_ -> forall a. R a
malformed
instance EmbPrj Cohesion where
icod_ :: Cohesion -> S Int32
icod_ Cohesion
Flat = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
icod_ Cohesion
Continuous = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
icod_ Cohesion
Squash = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
value :: Int32 -> R Cohesion
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return Cohesion
Flat
value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return Cohesion
Continuous
value Int32
2 = forall (m :: * -> *) a. Monad m => a -> m a
return Cohesion
Squash
value Int32
_ = forall a. R a
malformed
instance EmbPrj Modality where
icod_ :: Modality -> S Int32
icod_ (Modality Relevance
a Quantity
b Cohesion
c) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Relevance -> Quantity -> Cohesion -> Modality
Modality Relevance
a Quantity
b Cohesion
c
value :: Int32 -> R Modality
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall a b. (a -> b) -> a -> b
$ \case
[Int32
a, Int32
b, Int32
c] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Relevance -> Quantity -> Cohesion -> Modality
Modality Int32
a Int32
b Int32
c
Node
_ -> forall a. R a
malformed
instance EmbPrj Relevance where
icod_ :: Relevance -> S Int32
icod_ Relevance
Relevant = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
icod_ Relevance
Irrelevant = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
icod_ Relevance
NonStrict = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
value :: Int32 -> R Relevance
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return Relevance
Relevant
value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return Relevance
Irrelevant
value Int32
2 = forall (m :: * -> *) a. Monad m => a -> m a
return Relevance
NonStrict
value Int32
_ = forall a. R a
malformed
instance EmbPrj Annotation where
icod_ :: Annotation -> S Int32
icod_ (Annotation Lock
l) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Lock -> Annotation
Annotation Lock
l
value :: Int32 -> R Annotation
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall a b. (a -> b) -> a -> b
$ \case
[Int32
l] -> forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Lock -> Annotation
Annotation Int32
l
Node
_ -> forall a. R a
malformed
instance EmbPrj Lock where
icod_ :: Lock -> S Int32
icod_ Lock
IsNotLock = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
icod_ Lock
IsLock = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
value :: Int32 -> R Lock
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return Lock
IsNotLock
value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return Lock
IsLock
value Int32
_ = forall a. R a
malformed
instance EmbPrj Origin where
icod_ :: Origin -> S Int32
icod_ Origin
UserWritten = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
icod_ Origin
Inserted = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
icod_ Origin
Reflected = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
icod_ Origin
CaseSplit = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
3
icod_ Origin
Substitution = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
4
value :: Int32 -> R Origin
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return Origin
UserWritten
value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return Origin
Inserted
value Int32
2 = forall (m :: * -> *) a. Monad m => a -> m a
return Origin
Reflected
value Int32
3 = forall (m :: * -> *) a. Monad m => a -> m a
return Origin
CaseSplit
value Int32
4 = forall (m :: * -> *) a. Monad m => a -> m a
return Origin
Substitution
value Int32
_ = forall a. R a
malformed
instance EmbPrj a => EmbPrj (WithOrigin a) where
icod_ :: WithOrigin a -> S Int32
icod_ (WithOrigin Origin
a a
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' forall a. Origin -> a -> WithOrigin a
WithOrigin Origin
a a
b
value :: Int32 -> R (WithOrigin a)
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN forall a. Origin -> a -> WithOrigin a
WithOrigin
instance EmbPrj FreeVariables where
icod_ :: FreeVariables -> S Int32
icod_ FreeVariables
UnknownFVs = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' FreeVariables
UnknownFVs
icod_ (KnownFVs IntSet
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' IntSet -> FreeVariables
KnownFVs IntSet
a
value :: Int32 -> R FreeVariables
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R FreeVariables
valu where
valu :: Node
-> Arrows
(Constant Int32 (Domains FreeVariables))
(R (CoDomain FreeVariables))
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN FreeVariables
UnknownFVs
valu [Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN IntSet -> FreeVariables
KnownFVs Int32
a
valu Node
_ = forall a. R a
malformed
instance EmbPrj ConOrigin where
icod_ :: ConOrigin -> S Int32
icod_ ConOrigin
ConOSystem = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
icod_ ConOrigin
ConOCon = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
icod_ ConOrigin
ConORec = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
icod_ ConOrigin
ConOSplit = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
3
value :: Int32 -> R ConOrigin
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConOSystem
value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConOCon
value Int32
2 = forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConORec
value Int32
3 = forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConOSplit
value Int32
_ = forall a. R a
malformed
instance EmbPrj ProjOrigin where
icod_ :: ProjOrigin -> S Int32
icod_ ProjOrigin
ProjPrefix = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
0
icod_ ProjOrigin
ProjPostfix = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
1
icod_ ProjOrigin
ProjSystem = forall (m :: * -> *) a. Monad m => a -> m a
return Int32
2
value :: Int32 -> R ProjOrigin
value Int32
0 = forall (m :: * -> *) a. Monad m => a -> m a
return ProjOrigin
ProjPrefix
value Int32
1 = forall (m :: * -> *) a. Monad m => a -> m a
return ProjOrigin
ProjPostfix
value Int32
2 = forall (m :: * -> *) a. Monad m => a -> m a
return ProjOrigin
ProjSystem
value Int32
_ = forall a. R a
malformed
instance EmbPrj Agda.Syntax.Literal.Literal where
icod_ :: Literal -> S Int32
icod_ (LitNat Integer
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Integer -> Literal
LitNat Integer
a
icod_ (LitFloat Double
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Double -> Literal
LitFloat Double
a
icod_ (LitString Text
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 Text -> Literal
LitString Text
a
icod_ (LitChar Char
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
3 Char -> Literal
LitChar Char
a
icod_ (LitQName QName
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
5 QName -> Literal
LitQName QName
a
icod_ (LitMeta TopLevelModuleName
a MetaId
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
6 TopLevelModuleName -> MetaId -> Literal
LitMeta TopLevelModuleName
a MetaId
b
icod_ (LitWord64 Word64
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
7 Word64 -> Literal
LitWord64 Word64
a
value :: Int32 -> R Literal
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Literal
valu where
valu :: Node -> R Literal
valu [Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Integer -> Literal
LitNat Int32
a
valu [Int32
1, Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Double -> Literal
LitFloat Int32
a
valu [Int32
2, Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Text -> Literal
LitString Int32
a
valu [Int32
3, Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Char -> Literal
LitChar Int32
a
valu [Int32
5, Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN QName -> Literal
LitQName Int32
a
valu [Int32
6, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN TopLevelModuleName -> MetaId -> Literal
LitMeta Int32
a Int32
b
valu [Int32
7, Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Word64 -> Literal
LitWord64 Int32
a
valu Node
_ = forall a. R a
malformed
instance EmbPrj IsAbstract where
icod_ :: IsAbstract -> S Int32
icod_ IsAbstract
AbstractDef = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 IsAbstract
AbstractDef
icod_ IsAbstract
ConcreteDef = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' IsAbstract
ConcreteDef
value :: Int32 -> R IsAbstract
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {a}. (Eq a, Num a) => [a] -> R IsAbstract
valu where
valu :: [a]
-> Arrows
(Constant Int32 (Domains IsAbstract)) (R (CoDomain IsAbstract))
valu [a
0] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN IsAbstract
AbstractDef
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN IsAbstract
ConcreteDef
valu [a]
_ = forall a. R a
malformed
instance EmbPrj Delayed where
icod_ :: Delayed -> S Int32
icod_ Delayed
Delayed = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 Delayed
Delayed
icod_ Delayed
NotDelayed = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Delayed
NotDelayed
value :: Int32 -> R Delayed
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase forall {a}. (Eq a, Num a) => [a] -> R Delayed
valu where
valu :: [a]
-> Arrows (Constant Int32 (Domains Delayed)) (R (CoDomain Delayed))
valu [a
0] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Delayed
Delayed
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Delayed
NotDelayed
valu [a]
_ = forall a. R a
malformed
instance EmbPrj SrcLoc where
icod_ :: SrcLoc -> S Int32
icod_ (SrcLoc String
p String
m String
f Int
sl Int
sc Int
el Int
ec) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
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 :: Int32 -> R SrcLoc
value = forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN String -> String -> String -> Int -> Int -> Int -> Int -> SrcLoc
SrcLoc
instance EmbPrj CallStack where
icod_ :: CallStack -> S Int32
icod_ = forall a. EmbPrj a => a -> S Int32
icode forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> [(String, SrcLoc)]
getCallStack
value :: Int32 -> R CallStack
value = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(String, SrcLoc)] -> CallStack
fromCallSiteList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. EmbPrj a => Int32 -> R a
value
instance EmbPrj Impossible where
icod_ :: Impossible -> S Int32
icod_ (Impossible CallStack
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
0 CallStack -> Impossible
Impossible CallStack
a
icod_ (Unreachable CallStack
a) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 CallStack -> Impossible
Unreachable CallStack
a
icod_ (ImpMissingDefinitions [String]
a String
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
2 [String] -> String -> Impossible
ImpMissingDefinitions [String]
a String
b
value :: Int32 -> R Impossible
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Impossible
valu where
valu :: Node -> R Impossible
valu [Int32
0, Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN CallStack -> Impossible
Impossible Int32
a
valu [Int32
1, Int32
a] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN CallStack -> Impossible
Unreachable Int32
a
valu [Int32
2, Int32
a, Int32
b] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN [String] -> String -> Impossible
ImpMissingDefinitions Int32
a Int32
b
valu Node
_ = forall a. R a
malformed
instance EmbPrj ExpandedEllipsis where
icod_ :: ExpandedEllipsis -> S Int32
icod_ ExpandedEllipsis
NoEllipsis = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ExpandedEllipsis
NoEllipsis
icod_ (ExpandedEllipsis Range
a Int
b) = forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN Int32
1 Range -> Int -> ExpandedEllipsis
ExpandedEllipsis Range
a Int
b
value :: Int32 -> R ExpandedEllipsis
value = forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R ExpandedEllipsis
valu where
valu :: Node
-> Arrows
(Constant Int32 (Domains ExpandedEllipsis))
(R (CoDomain ExpandedEllipsis))
valu [] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN ExpandedEllipsis
NoEllipsis
valu [Int32
1,Int32
a,Int32
b] = forall t.
(VALU t (IsBase t),
Currying (Constant Int32 (Domains t)) (R (CoDomain t)),
All EmbPrj (Domains t)) =>
t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN Range -> Int -> ExpandedEllipsis
ExpandedEllipsis Int32
a Int32
b
valu Node
_ = forall a. R a
malformed