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

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

import Prelude hiding (mapM)

import Control.Monad.Reader hiding (mapM)
import Control.Monad.State.Strict (gets, modify)


import Data.Array.IArray
import Data.Word
import qualified Data.Foldable as Fold
import Data.Hashable
import qualified Data.HashTable.IO as H
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 Data.List.NonEmpty (NonEmpty(..), nonEmpty)
import qualified Data.List.NonEmpty as NonEmpty
import qualified Data.Set as Set
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.Text.Lazy (Text)
import Data.Traversable ( mapM )
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.Info
import Agda.Syntax.Position as P
import Agda.Syntax.Notation
import Agda.Syntax.Literal
import Agda.Interaction.FindFile

import Agda.TypeChecking.Serialise.Base

import Agda.Utils.BiMap (BiMap)
import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.FileName
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Trie (Trie(..))


import Agda.Utils.Except

import Agda.Utils.Empty (Empty)
import qualified Agda.Utils.Empty as Empty

import Agda.Utils.WithDefault

import Agda.Utils.Impossible

instance {-# OVERLAPPING #-} EmbPrj String where
  icod_ :: String -> S Int32
icod_   = String -> S Int32
icodeString
  value :: Int32 -> R String
value i :: Int32
i = (Array Int32 String -> Int32 -> String
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int32
i) (Array Int32 String -> String)
-> ExceptT TypeError (StateT St IO) (Array Int32 String)
-> R String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (St -> Array Int32 String)
-> ExceptT TypeError (StateT St IO) (Array Int32 String)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Int32 String
stringE

instance EmbPrj Text where
  icod_ :: Text -> S Int32
icod_   = (Dict -> HashTable Text Int32)
-> (Dict -> IORef FreshAndReuse) -> Text -> S Int32
forall k.
(Eq k, Hashable k) =>
(Dict -> HashTable k Int32)
-> (Dict -> IORef FreshAndReuse) -> k -> S Int32
icodeX Dict -> HashTable Text Int32
textD Dict -> IORef FreshAndReuse
textC
  value :: Int32 -> R Text
value i :: Int32
i = (Array Int32 Text -> Int32 -> Text
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int32
i) (Array Int32 Text -> Text)
-> ExceptT TypeError (StateT St IO) (Array Int32 Text) -> R Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (St -> Array Int32 Text)
-> ExceptT TypeError (StateT St IO) (Array Int32 Text)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Int32 Text
textE

instance EmbPrj Integer where
  icod_ :: Integer -> S Int32
icod_   = Integer -> S Int32
icodeInteger
  value :: Int32 -> R Integer
value i :: Int32
i = (Array Int32 Integer -> Int32 -> Integer
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int32
i) (Array Int32 Integer -> Integer)
-> ExceptT TypeError (StateT St IO) (Array Int32 Integer)
-> R Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (St -> Array Int32 Integer)
-> ExceptT TypeError (StateT St IO) (Array Int32 Integer)
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_ i :: Word64
i = (Int32 -> Int32 -> Int32) -> Int32 -> Int32 -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (Int32 -> Int32 -> Int32
forall a. HasCallStack => a
undefined :: Int32 -> Int32 -> Int32) (Word64 -> Int32
int32 Word64
q) (Word64 -> Int32
int32 Word64
r)
    where (q :: Word64
q, r :: Word64
r) = Word64 -> Word64 -> (Word64, Word64)
forall a. Integral a => a -> a -> (a, a)
quotRem Word64
i (2Word64 -> Integer -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^32)
          int32 :: Word64 -> Int32
          int32 :: Word64 -> Int32
int32 = Word64 -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral

  value :: Int32 -> R Word64
value = (Node -> R Word64) -> Int32 -> R Word64
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Word64
forall a. Integral a => [a] -> R Word64
valu where
    valu :: [a] -> R Word64
valu [a :: a
a, b :: a
b] = Word64 -> R Word64
forall (m :: * -> *) a. Monad m => a -> m a
return (Word64 -> R Word64) -> Word64 -> R Word64
forall a b. (a -> b) -> a -> b
$ Word64
n Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
mod (a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) Word64
n Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
mod (a -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
b) Word64
n
    valu _      = R Word64
forall a. R a
malformed
    n :: Word64
n = 2Word64 -> Integer -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^32

instance EmbPrj Int32 where
  icod_ :: Int32 -> S Int32
icod_ i :: Int32
i = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i
  value :: Int32 -> R Int32
value i :: Int32
i = Int32 -> R Int32
forall (m :: * -> *) a. Monad m => a -> m a
return Int32
i

instance EmbPrj Int where
  icod_ :: Int -> S Int32
icod_ i :: Int
i = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)
  value :: Int32 -> R Int
value i :: Int32
i = Int -> R Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
i)

instance EmbPrj Char where
  icod_ :: Char -> S Int32
icod_ c :: Char
c = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int32) -> Int -> Int32
forall a b. (a -> b) -> a -> b
$ Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c)
  value :: Int32 -> R Char
value i :: Int32
i = Char -> R Char
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Char
forall a. Enum a => Int -> a
toEnum (Int -> Char) -> Int -> Char
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int) -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ Int32 -> Integer
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 i :: Int32
i = (Array Int32 Double -> Int32 -> Double
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int32
i) (Array Int32 Double -> Double)
-> ExceptT TypeError (StateT St IO) (Array Int32 Double)
-> R Double
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (St -> Array Int32 Double)
-> ExceptT TypeError (StateT St IO) (Array Int32 Double)
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_ = Void -> S Int32
forall a. Void -> a
absurd
  value :: Int32 -> R Void
value = (Node -> R Void) -> Int32 -> R Void
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Void
forall p a. p -> R a
valu where valu :: p -> R a
valu _ = R a
forall a. R a
malformed

instance EmbPrj () where
  icod_ :: () -> S Int32
icod_ () = () -> Arrows (Domains ()) (S Int32)
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 = (Node -> R ()) -> Int32 -> R ()
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R ()
forall a. [a] -> R ()
valu where
    valu :: [a] -> R ()
valu [] = () -> Arrows (Constant Int32 (Domains ())) (R (CoDomain ()))
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 _  = R ()
forall a. R a
malformed

instance (EmbPrj a, EmbPrj b) => EmbPrj (a, b) where
  icod_ :: (a, b) -> S Int32
icod_ (a :: a
a, b :: b
b) = (a -> b -> (a, b)) -> a -> b -> S Int32
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 = (a -> b -> (a, b)) -> Int32 -> R (CoDomain (a -> b -> (a, b)))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN (,)

instance (EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c) where
  icod_ :: (a, b, c) -> S Int32
icod_ (a :: a
a, b :: b
b, c :: c
c) = (a -> b -> c -> (a, b, c)) -> a -> b -> c -> S Int32
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 = (a -> b -> c -> (a, b, c))
-> Int32 -> R (CoDomain (a -> b -> c -> (a, b, c)))
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  x :: a
x) = Int32 -> (a -> Either a Any) -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 a -> Either a Any
forall a b. a -> Either a b
Left a
x
  icod_ (Right x :: b
x) = Int32 -> (b -> Either Any b) -> b -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 b -> Either Any b
forall a b. b -> Either a b
Right b
x

  value :: Int32 -> R (Either a b)
value = (Node -> R (Either a b)) -> Int32 -> R (Either a b)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Either a b)
forall a b. (EmbPrj a, EmbPrj b) => Node -> R (Either a b)
valu where
    valu :: Node -> R (Either a b)
valu [0, x :: Int32
x] = (a -> Either a b) -> Int32 -> R (Either a 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 a -> Either a b
forall a b. a -> Either a b
Left  Int32
x
    valu [1, x :: Int32
x] = (b -> Either a b) -> Int32 -> R (Either a 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 b -> Either a b
forall a b. b -> Either a b
Right Int32
x
    valu _   = R (Either a b)
forall a. R a
malformed

instance EmbPrj a => EmbPrj (Maybe a) where
  icod_ :: Maybe a -> S Int32
icod_ Nothing  = Maybe Any -> Arrows (Domains (Maybe Any)) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Maybe Any
forall a. Maybe a
Nothing
  icod_ (Just x :: a
x) = (a -> Maybe a) -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' a -> Maybe a
forall a. a -> Maybe a
Just a
x

  value :: Int32 -> R (Maybe a)
value = (Node -> R (Maybe a)) -> Int32 -> R (Maybe a)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R (Maybe a)
forall a. EmbPrj a => Node -> R (Maybe a)
valu where
    valu :: Node -> R (Maybe a)
valu []  = Maybe a
-> Arrows
     (Constant Int32 (Domains (Maybe a))) (R (CoDomain (Maybe 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 Maybe a
forall a. Maybe a
Nothing
    valu [x :: Int32
x] = (a -> Maybe a) -> Int32 -> R (Maybe 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 a -> Maybe a
forall a. a -> Maybe a
Just Int32
x
    valu _   = R (Maybe a)
forall a. R a
malformed

instance EmbPrj a => EmbPrj (Strict.Maybe a) where
  icod_ :: Maybe a -> S Int32
icod_ m :: Maybe a
m = Maybe a -> S Int32
forall a. EmbPrj a => a -> S Int32
icode (Maybe a -> Maybe a
forall a. Maybe a -> Maybe a
Strict.toLazy Maybe a
m)
  value :: Int32 -> R (Maybe a)
value m :: Int32
m = Maybe a -> Maybe a
forall a. Maybe a -> Maybe a
Strict.toStrict (Maybe a -> Maybe a)
-> ExceptT TypeError (StateT St IO) (Maybe a) -> R (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Int32 -> ExceptT TypeError (StateT St IO) (Maybe a)
forall a. EmbPrj a => Int32 -> R a
value Int32
m

instance EmbPrj Bool where
  icod_ :: Bool -> S Int32
icod_ True  = Bool -> Arrows (Domains Bool) (S Int32)
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_ False = Int32 -> Bool -> Arrows (Domains Bool) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 Bool
False

  value :: Int32 -> R Bool
value = (Node -> R Bool) -> Int32 -> R Bool
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Bool
forall a. (Eq a, Num a) => [a] -> R Bool
valu where
    valu :: [a] -> R Bool
valu []  = Bool -> Arrows (Constant Int32 (Domains Bool)) (R (CoDomain Bool))
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 [0] = Bool -> Arrows (Constant Int32 (Domains Bool)) (R (CoDomain Bool))
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 _   = R Bool
forall a. R a
malformed

instance EmbPrj FileType where
  icod_ :: FileType -> S Int32
icod_ AgdaFileType = DataOrRecord -> Arrows (Domains DataOrRecord) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' DataOrRecord
IsData
  icod_ MdFileType   = Int32 -> DataOrRecord -> Arrows (Domains DataOrRecord) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 DataOrRecord
IsRecord
  icod_ RstFileType  = Int32 -> DataOrRecord -> Arrows (Domains DataOrRecord) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 DataOrRecord
IsRecord
  icod_ TexFileType  = Int32 -> DataOrRecord -> Arrows (Domains DataOrRecord) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 2 DataOrRecord
IsRecord
  icod_ OrgFileType  = Int32 -> DataOrRecord -> Arrows (Domains DataOrRecord) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 3 DataOrRecord
IsRecord

  value :: Int32 -> R FileType
value = (Node -> R FileType) -> Int32 -> R FileType
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase ((Node -> R FileType) -> Int32 -> R FileType)
-> (Node -> R FileType) -> Int32 -> R FileType
forall a b. (a -> b) -> a -> b
$ \case
    []  -> FileType
-> Arrows
     (Constant Int32 (Domains FileType)) (R (CoDomain FileType))
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
    [0] -> FileType
-> Arrows
     (Constant Int32 (Domains FileType)) (R (CoDomain FileType))
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
    [1] -> FileType
-> Arrows
     (Constant Int32 (Domains FileType)) (R (CoDomain FileType))
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
    [2] -> FileType
-> Arrows
     (Constant Int32 (Domains FileType)) (R (CoDomain FileType))
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
    [3] -> FileType
-> Arrows
     (Constant Int32 (Domains FileType)) (R (CoDomain FileType))
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
    _   -> R FileType
forall a. R a
malformed

instance EmbPrj DataOrRecord where
  icod_ :: DataOrRecord -> S Int32
icod_ IsData   = DataOrRecord -> Arrows (Domains DataOrRecord) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' DataOrRecord
IsData
  icod_ IsRecord = Int32 -> DataOrRecord -> Arrows (Domains DataOrRecord) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 DataOrRecord
IsRecord

  value :: Int32 -> R DataOrRecord
value = (Node -> R DataOrRecord) -> Int32 -> R DataOrRecord
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase ((Node -> R DataOrRecord) -> Int32 -> R DataOrRecord)
-> (Node -> R DataOrRecord) -> Int32 -> R DataOrRecord
forall a b. (a -> b) -> a -> b
$ \case
    []  -> DataOrRecord
-> Arrows
     (Constant Int32 (Domains DataOrRecord)) (R (CoDomain DataOrRecord))
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 DataOrRecord
IsData
    [0] -> DataOrRecord
-> Arrows
     (Constant Int32 (Domains DataOrRecord)) (R (CoDomain DataOrRecord))
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 DataOrRecord
IsRecord
    _   -> R DataOrRecord
forall a. R a
malformed

instance EmbPrj AbsolutePath where
  icod_ :: AbsolutePath -> S Int32
icod_ file :: AbsolutePath
file = do
    HashTable RealWorld AbsolutePath Int32
d <- (Dict -> HashTable RealWorld AbsolutePath Int32)
-> ReaderT Dict IO (HashTable RealWorld AbsolutePath Int32)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks Dict -> HashTable RealWorld AbsolutePath Int32
Dict -> HashTable AbsolutePath Int32
absPathD
    IO Int32 -> S Int32
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int32 -> S Int32) -> IO Int32 -> S Int32
forall a b. (a -> b) -> a -> b
$ (IO Int32 -> IO (Maybe Int32) -> IO Int32)
-> IO (Maybe Int32) -> IO Int32 -> IO Int32
forall a b c. (a -> b -> c) -> b -> a -> c
flip IO Int32 -> IO (Maybe Int32) -> IO Int32
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (HashTable AbsolutePath Int32 -> AbsolutePath -> IO (Maybe Int32)
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> k -> IO (Maybe v)
H.lookup HashTable RealWorld AbsolutePath Int32
HashTable AbsolutePath Int32
d AbsolutePath
file) (IO Int32 -> IO Int32) -> IO Int32 -> IO Int32
forall a b. (a -> b) -> a -> b
$ do
      -- The path @file@ should be cached in the dictionary @d@.
      -- This seems not to be the case, thus, crash here.
      -- But leave some hints for the posterity why things could go so wrong.
      -- reportSLn "impossible" 10 -- does not work here
      String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
        [ "Panic while serializing absolute path: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> String
forall a. Show a => a -> String
show AbsolutePath
file
        , "The path could not be found in the dictionary:"
        ]
      String -> IO ()
putStrLn (String -> IO ())
-> ([(AbsolutePath, Int32)] -> String)
-> [(AbsolutePath, Int32)]
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(AbsolutePath, Int32)] -> String
forall a. Show a => a -> String
show ([(AbsolutePath, Int32)] -> IO ())
-> IO [(AbsolutePath, Int32)] -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HashTable AbsolutePath Int32 -> IO [(AbsolutePath, Int32)]
forall (h :: * -> * -> * -> *) k v.
(HashTable h, Eq k, Hashable k) =>
IOHashTable h k v -> IO [(k, v)]
H.toList HashTable RealWorld AbsolutePath Int32
HashTable AbsolutePath Int32
d
      IO Int32
forall a. HasCallStack => a
__IMPOSSIBLE__

  value :: Int32 -> R AbsolutePath
value m :: Int32
m = do
    TopLevelModuleName
m :: TopLevelModuleName
            <- Int32 -> R TopLevelModuleName
forall a. EmbPrj a => Int32 -> R a
value Int32
m
    ModuleToSource
mf      <- (St -> ModuleToSource)
-> ExceptT TypeError (StateT St IO) ModuleToSource
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> ModuleToSource
modFile
    [AbsolutePath]
incs    <- (St -> [AbsolutePath])
-> ExceptT TypeError (StateT St IO) [AbsolutePath]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> [AbsolutePath]
includes
    (r :: Either FindError SourceFile
r, mf :: ModuleToSource
mf) <- IO (Either FindError SourceFile, ModuleToSource)
-> ExceptT
     TypeError
     (StateT St IO)
     (Either FindError SourceFile, ModuleToSource)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either FindError SourceFile, ModuleToSource)
 -> ExceptT
      TypeError
      (StateT St IO)
      (Either FindError SourceFile, ModuleToSource))
-> IO (Either FindError SourceFile, ModuleToSource)
-> ExceptT
     TypeError
     (StateT St IO)
     (Either FindError SourceFile, ModuleToSource)
forall a b. (a -> b) -> a -> b
$ [AbsolutePath]
-> TopLevelModuleName
-> ModuleToSource
-> IO (Either FindError SourceFile, ModuleToSource)
findFile'' [AbsolutePath]
incs TopLevelModuleName
m ModuleToSource
mf
    (St -> St) -> R ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((St -> St) -> R ()) -> (St -> St) -> R ()
forall a b. (a -> b) -> a -> b
$ \s :: St
s -> St
s { modFile :: ModuleToSource
modFile = ModuleToSource
mf }
    case Either FindError SourceFile
r of
      Left err :: FindError
err -> TypeError -> R AbsolutePath
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TypeError -> R AbsolutePath) -> TypeError -> R AbsolutePath
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> FindError -> TypeError
findErrorToTypeError TopLevelModuleName
m FindError
err
      Right f :: SourceFile
f  -> AbsolutePath -> R AbsolutePath
forall (m :: * -> *) a. Monad m => a -> m a
return (SourceFile -> AbsolutePath
srcFilePath SourceFile
f)

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

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

instance Typeable b => EmbPrj (WithDefault b) where
  icod_ :: WithDefault b -> S Int32
icod_ = \case
    Default -> WithDefault Any -> Arrows (Domains (WithDefault Any)) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' WithDefault Any
forall (b :: Bool). WithDefault b
Default
    Value b :: Bool
b -> (Bool -> WithDefault Any) -> Bool -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Bool -> WithDefault Any
forall (b :: Bool). Bool -> WithDefault b
Value Bool
b

  value :: Int32 -> R (WithDefault b)
value = (Node -> R (WithDefault b)) -> Int32 -> R (WithDefault b)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase ((Node -> R (WithDefault b)) -> Int32 -> R (WithDefault b))
-> (Node -> R (WithDefault b)) -> Int32 -> R (WithDefault b)
forall a b. (a -> b) -> a -> b
$ \case
    []  -> WithDefault b
-> Arrows
     (Constant Int32 (Domains (WithDefault b)))
     (R (CoDomain (WithDefault 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 WithDefault b
forall (b :: Bool). WithDefault b
Default
    [a :: Int32
a] -> (Bool -> WithDefault b) -> Int32 -> R (WithDefault 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 Bool -> WithDefault b
forall (b :: Bool). Bool -> WithDefault b
Value Int32
a
    _ -> R (WithDefault b)
forall a. R a
malformed

instance EmbPrj TopLevelModuleName where
  icod_ :: TopLevelModuleName -> S Int32
icod_ (TopLevelModuleName a :: Range
a b :: [String]
b) = (Range -> [String] -> TopLevelModuleName)
-> Range -> [String] -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Range -> [String] -> TopLevelModuleName
TopLevelModuleName Range
a [String]
b

  value :: Int32 -> R TopLevelModuleName
value = (Range -> [String] -> TopLevelModuleName)
-> Int32 -> R (CoDomain (Range -> [String] -> TopLevelModuleName))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Range -> [String] -> TopLevelModuleName
TopLevelModuleName

instance {-# OVERLAPPABLE #-} EmbPrj a => EmbPrj [a] where
  icod_ :: [a] -> S Int32
icod_ xs :: [a]
xs = Node -> S Int32
icodeNode (Node -> S Int32) -> ReaderT Dict IO Node -> S Int32
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (a -> S Int32) -> [a] -> ReaderT Dict IO Node
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> S Int32
forall a. EmbPrj a => a -> S Int32
icode [a]
xs
  value :: Int32 -> R [a]
value    = (Node -> R [a]) -> Int32 -> R [a]
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase ((Int32 -> ExceptT TypeError (StateT St IO) a) -> Node -> R [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Int32 -> ExceptT TypeError (StateT St IO) a
forall a. EmbPrj a => Int32 -> R a
value)
--   icode []       = icode0'
--   icode (x : xs) = icode2' x xs
--   value = vcase valu where valu []      = valu0 []
--                            valu [x, xs] = valu2 (:) x xs
--                            valu _       = malformed

instance EmbPrj a => EmbPrj (NonEmpty a) where
  icod_ :: NonEmpty a -> S Int32
icod_ = [a] -> S Int32
forall a. EmbPrj a => a -> S Int32
icod_ ([a] -> S Int32) -> (NonEmpty a -> [a]) -> NonEmpty a -> S Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NonEmpty.toList
  value :: Int32 -> R (NonEmpty a)
value = R (NonEmpty a)
-> (NonEmpty a -> R (NonEmpty a))
-> Maybe (NonEmpty a)
-> R (NonEmpty a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe R (NonEmpty a)
forall a. R a
malformed NonEmpty a -> R (NonEmpty a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (NonEmpty a) -> R (NonEmpty a))
-> ([a] -> Maybe (NonEmpty a)) -> [a] -> R (NonEmpty a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
nonEmpty ([a] -> R (NonEmpty a))
-> (Int32 -> ExceptT TypeError (StateT St IO) [a])
-> Int32
-> R (NonEmpty a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Int32 -> ExceptT TypeError (StateT St IO) [a]
forall a. EmbPrj a => Int32 -> R a
value

instance (Ord a, Ord b, EmbPrj a, EmbPrj b) => EmbPrj (BiMap a b) where
  icod_ :: BiMap a b -> S Int32
icod_ m :: BiMap a b
m = [(a, b)] -> S Int32
forall a. EmbPrj a => a -> S Int32
icode (BiMap a b -> [(a, b)]
forall a b. BiMap a b -> [(a, b)]
BiMap.toList BiMap a b
m)
  value :: Int32 -> R (BiMap a b)
value m :: Int32
m = [(a, b)] -> BiMap a b
forall a b. (Ord a, Ord b) => [(a, b)] -> BiMap a b
BiMap.fromList ([(a, b)] -> BiMap a b)
-> ExceptT TypeError (StateT St IO) [(a, b)] -> R (BiMap a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int32 -> ExceptT TypeError (StateT St IO) [(a, b)]
forall a. EmbPrj a => Int32 -> R a
value Int32
m

instance (Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) where
  icod_ :: Map a b -> S Int32
icod_ m :: Map a b
m = [(a, b)] -> S Int32
forall a. EmbPrj a => a -> S Int32
icode (Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
Map.toList Map a b
m)
  value :: Int32 -> R (Map a b)
value m :: Int32
m = [(a, b)] -> Map a b
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(a, b)] -> Map a b)
-> ExceptT TypeError (StateT St IO) [(a, b)] -> R (Map a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Int32 -> ExceptT TypeError (StateT St IO) [(a, b)]
forall a. EmbPrj a => Int32 -> R a
value Int32
m

instance (Ord a, EmbPrj a) => EmbPrj (Set a) where
  icod_ :: Set a -> S Int32
icod_ s :: Set a
s = [a] -> S Int32
forall a. EmbPrj a => a -> S Int32
icode (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
s)
  value :: Int32 -> R (Set a)
value s :: Int32
s = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList ([a] -> Set a) -> ExceptT TypeError (StateT St IO) [a] -> R (Set a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Int32 -> ExceptT TypeError (StateT St IO) [a]
forall a. EmbPrj a => Int32 -> R a
value Int32
s

instance EmbPrj IntSet where
  icod_ :: IntSet -> S Int32
icod_ s :: IntSet
s = [Int] -> S Int32
forall a. EmbPrj a => a -> S Int32
icode (IntSet -> [Int]
IntSet.toList IntSet
s)
  value :: Int32 -> R IntSet
value s :: Int32
s = [Int] -> IntSet
IntSet.fromList ([Int] -> IntSet)
-> ExceptT TypeError (StateT St IO) [Int] -> R IntSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int32 -> ExceptT TypeError (StateT St IO) [Int]
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 a :: Maybe b
a b :: Map a (Trie a b)
b)= (Maybe b -> Map a (Trie a b) -> Trie a b)
-> Maybe b -> Map a (Trie a b) -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Maybe b -> Map a (Trie a b) -> Trie a b
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 = (Maybe b -> Map a (Trie a b) -> Trie a b)
-> Int32 -> R (CoDomain (Maybe b -> Map a (Trie a b) -> Trie a b))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Maybe b -> Map a (Trie a b) -> Trie a b
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_ s :: Seq a
s = [a] -> S Int32
forall a. EmbPrj a => a -> S Int32
icode (Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq a
s)
  value :: Int32 -> R (Seq a)
value s :: Int32
s = [a] -> Seq a
forall a. [a] -> Seq a
Seq.fromList ([a] -> Seq a) -> ExceptT TypeError (StateT St IO) [a] -> R (Seq a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Int32 -> ExceptT TypeError (StateT St IO) [a]
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 p :: Position' a
p q :: Position' a
q) = (Position' a -> Position' a -> Interval' a)
-> Position' a -> Position' a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Position' a -> Position' a -> Interval' a
forall a. Position' a -> Position' a -> Interval' a
P.Interval Position' a
p Position' a
q

  value :: Int32 -> R (Interval' a)
value = (Position' a -> Position' a -> Interval' a)
-> Int32
-> R (CoDomain (Position' a -> Position' a -> Interval' a))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> R (CoDomain t)
valueN Position' a -> Position' a -> Interval' a
forall a. Position' a -> Position' a -> Interval' a
P.Interval

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

instance EmbPrj Range where
  icod_ :: Range -> S Int32
icod_ _ = () -> Arrows (Domains ()) (S Int32)
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 _ = Range -> R Range
forall (m :: * -> *) a. Monad m => a -> m a
return Range
forall a. Range' a
noRange

-- | Ranges that should be serialised properly.

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

instance EmbPrj SerialisedRange where
  icod_ :: SerialisedRange -> S Int32
icod_ (SerialisedRange r :: Range
r) =
    (SrcFile -> [IntervalWithoutFile] -> SerialisedRange)
-> SrcFile -> [IntervalWithoutFile] -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (SrcFile -> [IntervalWithoutFile] -> SerialisedRange
forall a. HasCallStack => a
undefined :: SrcFile -> [IntervalWithoutFile] -> SerialisedRange)
            (Range -> SrcFile
P.rangeFile Range
r) (Range -> [IntervalWithoutFile]
forall a. Range' a -> [IntervalWithoutFile]
P.rangeIntervals Range
r)

  value :: Int32 -> R SerialisedRange
value = (Node -> R SerialisedRange) -> Int32 -> R SerialisedRange
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R SerialisedRange
valu where
    valu :: Node -> R SerialisedRange
valu [a :: Int32
a, b :: Int32
b] = Range -> SerialisedRange
SerialisedRange (Range -> SerialisedRange) -> R Range -> R SerialisedRange
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SrcFile -> [IntervalWithoutFile] -> Range)
-> Int32 -> Int32 -> R Range
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 SrcFile -> [IntervalWithoutFile] -> Range
forall a. a -> [IntervalWithoutFile] -> Range' a
P.intervalsToRange Int32
a Int32
b
    valu _      = R SerialisedRange
forall a. R a
malformed

instance EmbPrj C.Name where
  icod_ :: Name -> S Int32
icod_ (C.NoName a :: Range
a b :: NameId
b)     = Int32 -> (Range -> NameId -> Name) -> Range -> NameId -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 Range -> NameId -> Name
C.NoName Range
a NameId
b
  icod_ (C.Name r :: Range
r nis :: NameInScope
nis xs :: [NamePart]
xs)  = Int32
-> (Range -> NameInScope -> [NamePart] -> Name)
-> Range
-> NameInScope
-> [NamePart]
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 Range -> NameInScope -> [NamePart] -> Name
C.Name Range
r NameInScope
nis [NamePart]
xs

  value :: Int32 -> R Name
value = (Node -> R Name) -> Int32 -> R Name
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Name
valu where
    valu :: Node -> R Name
valu [0, a :: Int32
a, b :: Int32
b]       = (Range -> NameId -> Name) -> Int32 -> Int32 -> R Name
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 [1, r :: Int32
r, nis :: Int32
nis, xs :: Int32
xs] = (Range -> NameInScope -> [NamePart] -> Name)
-> Int32 -> Int32 -> Int32 -> R Name
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 -> [NamePart] -> Name
C.Name   Int32
r Int32
nis Int32
xs
    valu _               = R Name
forall a. R a
malformed

instance EmbPrj NamePart where
  icod_ :: NamePart -> S Int32
icod_ Hole   = NamePart -> Arrows (Domains NamePart) (S Int32)
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 a :: String
a) = (String -> NamePart) -> String -> S Int32
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 = (Node -> R NamePart) -> Int32 -> R NamePart
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R NamePart
valu where
    valu :: Node -> R NamePart
valu []  = NamePart
-> Arrows
     (Constant Int32 (Domains NamePart)) (R (CoDomain NamePart))
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 [a :: Int32
a] = (String -> NamePart) -> Int32 -> R NamePart
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 _   = R NamePart
forall a. R a
malformed

instance EmbPrj NameInScope where
  icod_ :: NameInScope -> S Int32
icod_ InScope    = NameInScope -> Arrows (Domains NameInScope) (S Int32)
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_ NotInScope = Int32 -> NameInScope -> Arrows (Domains NameInScope) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 NameInScope
NotInScope

  value :: Int32 -> R NameInScope
value = (Node -> R NameInScope) -> Int32 -> R NameInScope
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R NameInScope
forall a. (Eq a, Num a) => [a] -> R NameInScope
valu where
    valu :: [a] -> R NameInScope
valu []  = NameInScope
-> Arrows
     (Constant Int32 (Domains NameInScope)) (R (CoDomain NameInScope))
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 [0] = NameInScope
-> Arrows
     (Constant Int32 (Domains NameInScope)) (R (CoDomain NameInScope))
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 _   = R NameInScope
forall a. R a
malformed

instance EmbPrj C.QName where
  icod_ :: QName -> S Int32
icod_ (Qual    a :: Name
a b :: QName
b) = (Name -> QName -> QName) -> Name -> QName -> S Int32
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 a :: Name
a  ) = (Name -> QName) -> Name -> S Int32
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 = (Node -> R QName) -> Int32 -> R QName
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R QName
valu where
    valu :: Node -> R QName
valu [a :: Int32
a, b :: Int32
b] = (Name -> QName -> QName) -> Int32 -> Int32 -> R QName
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 [a :: Int32
a]    = (Name -> QName) -> Int32 -> R QName
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 _      = R QName
forall a. R a
malformed

instance (EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) where
  icod_ :: ImportedName' a b -> S Int32
icod_ (ImportedModule a :: b
a) = Int32 -> (b -> ImportedName' Any b) -> b -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 b -> ImportedName' Any b
forall n m. m -> ImportedName' n m
ImportedModule b
a
  icod_ (ImportedName a :: a
a)   = Int32 -> (a -> ImportedName' a Any) -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 2 a -> ImportedName' a Any
forall n m. n -> ImportedName' n m
ImportedName a
a

  value :: Int32 -> R (ImportedName' a b)
value = (Node -> R (ImportedName' a b)) -> Int32 -> R (ImportedName' a b)
forall a. EmbPrj a => (Node -> R a) -> Int32 -> 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 [1, a :: Int32
a] = (m -> ImportedName' n m) -> Int32 -> R (ImportedName' n m)
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 m -> ImportedName' n m
forall n m. m -> ImportedName' n m
ImportedModule Int32
a
    valu [2, a :: Int32
a] = (n -> ImportedName' n m) -> Int32 -> R (ImportedName' n m)
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 n -> ImportedName' n m
forall n m. n -> ImportedName' n m
ImportedName Int32
a
    valu _ = R (ImportedName' n m)
forall a. R a
malformed

instance EmbPrj Associativity where
  icod_ :: Associativity -> S Int32
icod_ LeftAssoc  = Associativity -> Arrows (Domains Associativity) (S Int32)
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_ RightAssoc = Int32 -> Associativity -> Arrows (Domains Associativity) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 Associativity
RightAssoc
  icod_ NonAssoc   = Int32 -> Associativity -> Arrows (Domains Associativity) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 2 Associativity
NonAssoc

  value :: Int32 -> R Associativity
value = (Node -> R Associativity) -> Int32 -> R Associativity
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Associativity
forall a. (Eq a, Num a) => [a] -> R Associativity
valu where
    valu :: [a] -> R Associativity
valu []  = Associativity
-> Arrows
     (Constant Int32 (Domains Associativity))
     (R (CoDomain Associativity))
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 [1] = Associativity
-> Arrows
     (Constant Int32 (Domains Associativity))
     (R (CoDomain Associativity))
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 [2] = Associativity
-> Arrows
     (Constant Int32 (Domains Associativity))
     (R (CoDomain Associativity))
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 _   = R Associativity
forall a. R a
malformed

instance EmbPrj FixityLevel where
  icod_ :: FixityLevel -> S Int32
icod_ Unrelated   = FixityLevel -> Arrows (Domains FixityLevel) (S Int32)
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 a :: Double
a) = (Double -> FixityLevel) -> Double -> S Int32
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 = (Node -> R FixityLevel) -> Int32 -> R FixityLevel
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R FixityLevel
valu where
    valu :: Node -> R FixityLevel
valu []  = FixityLevel
-> Arrows
     (Constant Int32 (Domains FixityLevel)) (R (CoDomain FixityLevel))
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 [a :: Int32
a] = (Double -> FixityLevel) -> Int32 -> R FixityLevel
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 _   = R FixityLevel
forall a. R a
malformed

instance EmbPrj Fixity where
  icod_ :: Fixity -> S Int32
icod_ (Fixity a :: Range
a b :: FixityLevel
b c :: Associativity
c) = (Range -> FixityLevel -> Associativity -> Fixity)
-> Range -> FixityLevel -> Associativity -> S Int32
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 = (Range -> FixityLevel -> Associativity -> Fixity)
-> Int32
-> R (CoDomain (Range -> FixityLevel -> Associativity -> Fixity))
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' a :: Fixity
a b :: Notation
b r :: Range
r) = (Fixity -> Notation -> Fixity') -> Fixity -> Notation -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (\ a :: Fixity
a b :: Notation
b -> Fixity -> Notation -> Range -> Fixity'
Fixity' Fixity
a Notation
b Range
r) Fixity
a Notation
b  -- discard theNameRange

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

instance EmbPrj GenPart where
  icod_ :: GenPart -> S Int32
icod_ (BindHole a :: Range
a b :: Ranged Int
b)   = Int32
-> (Range -> Ranged Int -> GenPart)
-> Range
-> Ranged Int
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 Range -> Ranged Int -> GenPart
BindHole Range
a Ranged Int
b
  icod_ (NormalHole a :: Range
a b :: NamedArg (Ranged Int)
b) = Int32
-> (Range -> NamedArg (Ranged Int) -> GenPart)
-> Range
-> NamedArg (Ranged Int)
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 Range -> NamedArg (Ranged Int) -> GenPart
NormalHole Range
a NamedArg (Ranged Int)
b
  icod_ (WildHole a :: Ranged Int
a)     = Int32 -> (Ranged Int -> GenPart) -> Ranged Int -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 2 Ranged Int -> GenPart
WildHole Ranged Int
a
  icod_ (IdPart a :: RString
a)       = (RString -> GenPart) -> RString -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' RString -> GenPart
IdPart RString
a

  value :: Int32 -> R GenPart
value = (Node -> R GenPart) -> Int32 -> R GenPart
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R GenPart
valu where
    valu :: Node -> R GenPart
valu [0, a :: Int32
a, b :: Int32
b] = (Range -> Ranged Int -> GenPart) -> Int32 -> Int32 -> R GenPart
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 Int -> GenPart
BindHole Int32
a Int32
b
    valu [1, a :: Int32
a, b :: Int32
b] = (Range -> NamedArg (Ranged Int) -> GenPart)
-> Int32 -> Int32 -> R GenPart
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) -> GenPart
NormalHole Int32
a Int32
b
    valu [2, a :: Int32
a]    = (Ranged Int -> GenPart) -> Int32 -> R GenPart
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 Int -> GenPart
WildHole Int32
a
    valu [a :: Int32
a]       = (RString -> GenPart) -> Int32 -> R GenPart
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 -> GenPart
IdPart Int32
a
    valu _         = R GenPart
forall a. R a
malformed

instance EmbPrj MetaId where
  icod_ :: MetaId -> S Int32
icod_ (MetaId n :: Int
n) = Int -> S Int32
forall a. EmbPrj a => a -> S Int32
icod_ Int
n
  value :: Int32 -> R MetaId
value i :: Int32
i = Int -> MetaId
MetaId (Int -> MetaId) -> R Int -> R MetaId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int32 -> R Int
forall a. EmbPrj a => Int32 -> R a
value Int32
i

instance EmbPrj A.QName where
  icod_ :: QName -> S Int32
icod_ n :: QName
n@(A.QName a :: ModuleName
a b :: Name
b) = (Dict -> HashTable QNameId Int32)
-> (Dict -> IORef FreshAndReuse) -> QNameId -> S Int32 -> S Int32
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) (S Int32 -> S Int32) -> S Int32 -> S Int32
forall a b. (a -> b) -> a -> b
$ (ModuleName -> Name -> QName) -> ModuleName -> Name -> S Int32
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 = (ModuleName -> Name -> QName)
-> Int32 -> R (CoDomain (ModuleName -> Name -> QName))
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 a :: NonEmpty QName
a) = NonEmpty QName -> S Int32
forall a. EmbPrj a => a -> S Int32
icode NonEmpty QName
a
  value :: Int32 -> R AmbiguousQName
value n :: Int32
n          = NonEmpty QName -> AmbiguousQName
A.AmbQ (NonEmpty QName -> AmbiguousQName)
-> ExceptT TypeError (StateT St IO) (NonEmpty QName)
-> R AmbiguousQName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Int32 -> ExceptT TypeError (StateT St IO) (NonEmpty QName)
forall a. EmbPrj a => Int32 -> R a
value Int32
n

instance EmbPrj A.ModuleName where
  icod_ :: ModuleName -> S Int32
icod_ (A.MName a :: [Name]
a) = [Name] -> S Int32
forall a. EmbPrj a => a -> S Int32
icode [Name]
a
  value :: Int32 -> R ModuleName
value n :: Int32
n           = [Name] -> ModuleName
A.MName ([Name] -> ModuleName)
-> ExceptT TypeError (StateT St IO) [Name] -> R ModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Int32 -> ExceptT TypeError (StateT St IO) [Name]
forall a. EmbPrj a => Int32 -> R a
value Int32
n

instance EmbPrj A.Name where
  icod_ :: Name -> S Int32
icod_ (A.Name a :: NameId
a b :: Name
b c :: Range
c d :: Fixity'
d e :: Bool
e) = (Dict -> HashTable NameId Int32)
-> (Dict -> IORef FreshAndReuse) -> NameId -> S Int32 -> S Int32
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 (S Int32 -> S Int32) -> S Int32 -> S Int32
forall a b. (a -> b) -> a -> b
$
    (NameId -> Name -> SerialisedRange -> Fixity' -> Bool -> Name)
-> NameId -> Name -> SerialisedRange -> Fixity' -> Bool -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' (\ a :: NameId
a b :: Name
b -> NameId -> Name -> Range -> Fixity' -> Bool -> Name
A.Name NameId
a Name
b (Range -> Fixity' -> Bool -> Name)
-> (SerialisedRange -> Range)
-> SerialisedRange
-> Fixity'
-> Bool
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SerialisedRange -> Range
underlyingRange) NameId
a Name
b (Range -> SerialisedRange
SerialisedRange Range
c) Fixity'
d Bool
e

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

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

  value :: Int32 -> R (FieldAssignment' a)
value = (Name -> a -> FieldAssignment' a)
-> Int32 -> R (CoDomain (Name -> a -> FieldAssignment' a))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> 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 Int32
icod_ (Named a :: Maybe s
a b :: t
b) = (Maybe s -> t -> Named s t) -> Maybe s -> t -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Maybe s -> t -> Named s t
forall name a. Maybe name -> a -> Named name a
Named Maybe s
a t
b

  value :: Int32 -> R (Named s t)
value = (Maybe s -> t -> Named s t)
-> Int32 -> R (CoDomain (Maybe s -> t -> Named s t))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> 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 Int32
icod_ (Ranged r :: Range
r x :: a
x) = (Range -> a -> Ranged a) -> Range -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Range -> a -> Ranged a
forall a. Range -> a -> Ranged a
Ranged Range
r a
x

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

instance EmbPrj ArgInfo where
  icod_ :: ArgInfo -> S Int32
icod_ (ArgInfo h :: Hiding
h r :: Modality
r o :: Origin
o fv :: FreeVariables
fv) = (Hiding -> Modality -> Origin -> FreeVariables -> ArgInfo)
-> Hiding -> Modality -> Origin -> FreeVariables -> S Int32
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 -> ArgInfo
ArgInfo Hiding
h Modality
r Origin
o FreeVariables
fv

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

instance EmbPrj NameId where
  icod_ :: NameId -> S Int32
icod_ (NameId a :: Word64
a b :: Word64
b) = (Word64 -> Word64 -> NameId) -> Word64 -> Word64 -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Word64 -> Word64 -> NameId
NameId Word64
a Word64
b

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

instance (Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v) where
  icod_ :: HashMap k v -> S Int32
icod_ m :: HashMap k v
m = [(k, v)] -> S Int32
forall a. EmbPrj a => a -> S Int32
icode (HashMap k v -> [(k, v)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList HashMap k v
m)
  value :: Int32 -> R (HashMap k v)
value m :: Int32
m = [(k, v)] -> HashMap k v
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HMap.fromList ([(k, v)] -> HashMap k v)
-> ExceptT TypeError (StateT St IO) [(k, v)] -> R (HashMap k v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Int32 -> ExceptT TypeError (StateT St IO) [(k, v)]
forall a. EmbPrj a => Int32 -> R a
value Int32
m

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

  value :: Int32 -> R (WithHiding a)
value = (Hiding -> a -> WithHiding a)
-> Int32 -> R (CoDomain (Hiding -> a -> WithHiding a))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Int32 -> 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 Int32
icod_ (Arg i :: ArgInfo
i e :: a
e) = (ArgInfo -> a -> Arg a) -> ArgInfo -> a -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
i a
e

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

instance EmbPrj HasEta where
  icod_ :: HasEta -> S Int32
icod_ YesEta = HasEta -> Arrows (Domains HasEta) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' HasEta
YesEta
  icod_ NoEta  = Int32 -> HasEta -> Arrows (Domains HasEta) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 HasEta
NoEta

  value :: Int32 -> R HasEta
value = (Node -> R HasEta) -> Int32 -> R HasEta
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R HasEta
forall a. (Eq a, Num a) => [a] -> R HasEta
valu where
    valu :: [a] -> R HasEta
valu []  = HasEta
-> Arrows (Constant Int32 (Domains HasEta)) (R (CoDomain HasEta))
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 HasEta
YesEta
    valu [1] = HasEta
-> Arrows (Constant Int32 (Domains HasEta)) (R (CoDomain HasEta))
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 HasEta
NoEta
    valu _   = R HasEta
forall a. R a
malformed

instance EmbPrj Induction where
  icod_ :: Induction -> S Int32
icod_ Inductive   = Induction -> Arrows (Domains Induction) (S Int32)
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_ CoInductive = Int32 -> Induction -> Arrows (Domains Induction) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 Induction
CoInductive

  value :: Int32 -> R Induction
value = (Node -> R Induction) -> Int32 -> R Induction
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Induction
forall a. (Eq a, Num a) => [a] -> R Induction
valu where
    valu :: [a] -> R Induction
valu []  = Induction
-> Arrows
     (Constant Int32 (Domains Induction)) (R (CoDomain Induction))
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 [1] = Induction
-> Arrows
     (Constant Int32 (Domains Induction)) (R (CoDomain Induction))
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 _   = R Induction
forall a. R a
malformed

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

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

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

  value :: Int32 -> R Q0Origin
value = \case
    0 -> Q0Origin -> R Q0Origin
forall (m :: * -> *) a. Monad m => a -> m a
return (Q0Origin -> R Q0Origin) -> Q0Origin -> R Q0Origin
forall a b. (a -> b) -> a -> b
$ Q0Origin
Q0Inferred
    1 -> Q0Origin -> R Q0Origin
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
    2 -> Q0Origin -> R Q0Origin
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
    _ -> R Q0Origin
forall a. R a
malformed

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

  value :: Int32 -> R Q1Origin
value = \case
    0 -> Q1Origin -> R Q1Origin
forall (m :: * -> *) a. Monad m => a -> m a
return (Q1Origin -> R Q1Origin) -> Q1Origin -> R Q1Origin
forall a b. (a -> b) -> a -> b
$ Q1Origin
Q1Inferred
    1 -> Q1Origin -> R Q1Origin
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
    2 -> Q1Origin -> R Q1Origin
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
    _ -> R Q1Origin
forall a. R a
malformed

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

  value :: Int32 -> R QωOrigin
value = \case
    0 -> QωOrigin -> R QωOrigin
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
    1 -> QωOrigin -> R QωOrigin
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
       Range
forall a. Range' a
noRange
    2 -> QωOrigin -> R QωOrigin
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
    _ -> R QωOrigin
forall a. R a
malformed

instance EmbPrj Quantity where
  icod_ :: Quantity -> S Int32
icod_ = \case
    Quantity0 a :: Q0Origin
a -> Int32 -> (Q0Origin -> Quantity) -> Q0Origin -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 Q0Origin -> Quantity
Quantity0 Q0Origin
a
    Quantity1 a :: Q1Origin
a -> Int32 -> (Q1Origin -> Quantity) -> Q1Origin -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 Q1Origin -> Quantity
Quantity1 Q1Origin
a
    Quantityω a :: QωOrigin
a -> (QωOrigin -> Quantity) -> QωOrigin -> S Int32
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  -- default quantity, shorter code

  value :: Int32 -> R Quantity
value = (Node -> R Quantity) -> Int32 -> R Quantity
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase ((Node -> R Quantity) -> Int32 -> R Quantity)
-> (Node -> R Quantity) -> Int32 -> R Quantity
forall a b. (a -> b) -> a -> b
$ \case
    [0, a :: Int32
a] -> (Q0Origin -> Quantity) -> Int32 -> R Quantity
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
    [1, a :: Int32
a] -> (Q1Origin -> Quantity) -> Int32 -> R Quantity
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
    [a :: Int32
a]    -> (QωOrigin -> Quantity) -> Int32 -> R Quantity
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
    _      -> R Quantity
forall a. 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 Int32
icod_ Flat       = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 0
  icod_ Continuous = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 1
  icod_ Squash     = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 2

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

instance EmbPrj Modality where
  icod_ :: Modality -> S Int32
icod_ (Modality a :: Relevance
a b :: Quantity
b c :: Cohesion
c) = (Relevance -> Quantity -> Cohesion -> Modality)
-> Relevance -> Quantity -> Cohesion -> S Int32
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 = (Node -> R Modality) -> Int32 -> R Modality
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase ((Node -> R Modality) -> Int32 -> R Modality)
-> (Node -> R Modality) -> Int32 -> R Modality
forall a b. (a -> b) -> a -> b
$ \case
    [a :: Int32
a, b :: Int32
b, c :: Int32
c] -> (Relevance -> Quantity -> Cohesion -> Modality)
-> Int32 -> Int32 -> Int32 -> R Modality
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
    _ -> R Modality
forall a. R a
malformed

instance EmbPrj Relevance where
  icod_ :: Relevance -> S Int32
icod_ Relevant       = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 0
  icod_ Irrelevant     = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 1
  icod_ NonStrict      = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 2

  value :: Int32 -> R Relevance
value 0 = Relevance -> R Relevance
forall (m :: * -> *) a. Monad m => a -> m a
return Relevance
Relevant
  value 1 = Relevance -> R Relevance
forall (m :: * -> *) a. Monad m => a -> m a
return Relevance
Irrelevant
  value 2 = Relevance -> R Relevance
forall (m :: * -> *) a. Monad m => a -> m a
return Relevance
NonStrict
  value _ = R Relevance
forall a. R a
malformed

instance EmbPrj Origin where
  icod_ :: Origin -> S Int32
icod_ UserWritten = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 0
  icod_ Inserted    = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 1
  icod_ Reflected   = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 2
  icod_ CaseSplit   = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 3
  icod_ Substitution = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 4

  value :: Int32 -> R Origin
value 0 = Origin -> R Origin
forall (m :: * -> *) a. Monad m => a -> m a
return Origin
UserWritten
  value 1 = Origin -> R Origin
forall (m :: * -> *) a. Monad m => a -> m a
return Origin
Inserted
  value 2 = Origin -> R Origin
forall (m :: * -> *) a. Monad m => a -> m a
return Origin
Reflected
  value 3 = Origin -> R Origin
forall (m :: * -> *) a. Monad m => a -> m a
return Origin
CaseSplit
  value 4 = Origin -> R Origin
forall (m :: * -> *) a. Monad m => a -> m a
return Origin
Substitution
  value _ = R Origin
forall a. R a
malformed

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

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

instance EmbPrj FreeVariables where
  icod_ :: FreeVariables -> S Int32
icod_ UnknownFVs   = FreeVariables -> Arrows (Domains FreeVariables) (S Int32)
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 a :: IntSet
a) = (IntSet -> FreeVariables) -> IntSet -> S Int32
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 = (Node -> R FreeVariables) -> Int32 -> R FreeVariables
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R FreeVariables
valu where
    valu :: Node -> R FreeVariables
valu []  = FreeVariables
-> Arrows
     (Constant Int32 (Domains FreeVariables))
     (R (CoDomain FreeVariables))
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 [a :: Int32
a] = (IntSet -> FreeVariables) -> Int32 -> R FreeVariables
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 _   = R FreeVariables
forall a. R a
malformed

instance EmbPrj ConOrigin where
  icod_ :: ConOrigin -> S Int32
icod_ ConOSystem = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 0
  icod_ ConOCon    = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 1
  icod_ ConORec    = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 2
  icod_ ConOSplit  = Int32 -> S Int32
forall (m :: * -> *) a. Monad m => a -> m a
return 3

  value :: Int32 -> R ConOrigin
value 0 = ConOrigin -> R ConOrigin
forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConOSystem
  value 1 = ConOrigin -> R ConOrigin
forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConOCon
  value 2 = ConOrigin -> R ConOrigin
forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConORec
  value 3 = ConOrigin -> R ConOrigin
forall (m :: * -> *) a. Monad m => a -> m a
return ConOrigin
ConOSplit
  value _ = R ConOrigin
forall a. R a
malformed

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

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

instance EmbPrj Agda.Syntax.Literal.Literal where
  icod_ :: Literal -> S Int32
icod_ (LitNat    a :: Range
a b :: Integer
b)   = (Range -> Integer -> Literal) -> Range -> Integer -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Int32)
icodeN' Range -> Integer -> Literal
LitNat Range
a Integer
b
  icod_ (LitFloat  a :: Range
a b :: Double
b)   = Int32 -> (Range -> Double -> Literal) -> Range -> Double -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 Range -> Double -> Literal
LitFloat Range
a Double
b
  icod_ (LitString a :: Range
a b :: String
b)   = Int32 -> (Range -> String -> Literal) -> Range -> String -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 2 Range -> String -> Literal
LitString Range
a String
b
  icod_ (LitChar   a :: Range
a b :: Char
b)   = Int32 -> (Range -> Char -> Literal) -> Range -> Char -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 3 Range -> Char -> Literal
LitChar Range
a Char
b
  icod_ (LitQName  a :: Range
a b :: QName
b)   = Int32 -> (Range -> QName -> Literal) -> Range -> QName -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 5 Range -> QName -> Literal
LitQName Range
a QName
b
  icod_ (LitMeta   a :: Range
a b :: AbsolutePath
b c :: MetaId
c) = Int32
-> (Range -> AbsolutePath -> MetaId -> Literal)
-> Range
-> AbsolutePath
-> MetaId
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 6 Range -> AbsolutePath -> MetaId -> Literal
LitMeta Range
a AbsolutePath
b MetaId
c
  icod_ (LitWord64 a :: Range
a b :: Word64
b)   = Int32 -> (Range -> Word64 -> Literal) -> Range -> Word64 -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 7 Range -> Word64 -> Literal
LitWord64 Range
a Word64
b

  value :: Int32 -> R Literal
value = (Node -> R Literal) -> Int32 -> R Literal
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Literal
valu where
    valu :: Node -> R Literal
valu [a :: Int32
a, b :: Int32
b]       = (Range -> Integer -> Literal) -> Int32 -> Int32 -> R Literal
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 -> Integer -> Literal
LitNat    Int32
a Int32
b
    valu [1, a :: Int32
a, b :: Int32
b]    = (Range -> Double -> Literal) -> Int32 -> Int32 -> R Literal
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 -> Double -> Literal
LitFloat  Int32
a Int32
b
    valu [2, a :: Int32
a, b :: Int32
b]    = (Range -> String -> Literal) -> Int32 -> Int32 -> R Literal
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 -> String -> Literal
LitString Int32
a Int32
b
    valu [3, a :: Int32
a, b :: Int32
b]    = (Range -> Char -> Literal) -> Int32 -> Int32 -> R Literal
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 -> Char -> Literal
LitChar   Int32
a Int32
b
    valu [5, a :: Int32
a, b :: Int32
b]    = (Range -> QName -> Literal) -> Int32 -> Int32 -> R Literal
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 -> QName -> Literal
LitQName  Int32
a Int32
b
    valu [6, a :: Int32
a, b :: Int32
b, c :: Int32
c] = (Range -> AbsolutePath -> MetaId -> Literal)
-> Int32 -> Int32 -> Int32 -> R Literal
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 -> AbsolutePath -> MetaId -> Literal
LitMeta   Int32
a Int32
b Int32
c
    valu [7, a :: Int32
a, b :: Int32
b]    = (Range -> Word64 -> Literal) -> Int32 -> Int32 -> R Literal
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 -> Word64 -> Literal
LitWord64 Int32
a Int32
b
    valu _            = R Literal
forall a. R a
malformed

instance EmbPrj IsAbstract where
  icod_ :: IsAbstract -> S Int32
icod_ AbstractDef = Int32 -> IsAbstract -> Arrows (Domains IsAbstract) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 IsAbstract
AbstractDef
  icod_ ConcreteDef = IsAbstract -> Arrows (Domains IsAbstract) (S Int32)
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 = (Node -> R IsAbstract) -> Int32 -> R IsAbstract
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R IsAbstract
forall a. (Eq a, Num a) => [a] -> R IsAbstract
valu where
    valu :: [a] -> R IsAbstract
valu [0] = IsAbstract
-> Arrows
     (Constant Int32 (Domains IsAbstract)) (R (CoDomain IsAbstract))
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 []  = IsAbstract
-> Arrows
     (Constant Int32 (Domains IsAbstract)) (R (CoDomain IsAbstract))
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 _   = R IsAbstract
forall a. R a
malformed

instance EmbPrj Delayed where
  icod_ :: Delayed -> S Int32
icod_ Delayed    = Int32 -> Delayed -> Arrows (Domains Delayed) (S Int32)
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 Delayed
Delayed
  icod_ NotDelayed = Delayed -> Arrows (Domains Delayed) (S Int32)
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 = (Node -> R Delayed) -> Int32 -> R Delayed
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Delayed
forall a. (Eq a, Num a) => [a] -> R Delayed
valu where
    valu :: [a] -> R Delayed
valu [0] = Delayed
-> Arrows (Constant Int32 (Domains Delayed)) (R (CoDomain Delayed))
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 []  = Delayed
-> Arrows (Constant Int32 (Domains Delayed)) (R (CoDomain Delayed))
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 _   = R Delayed
forall a. R a
malformed

instance EmbPrj Impossible where
  icod_ :: Impossible -> S Int32
icod_ (Impossible a :: String
a b :: Integer
b)  = Int32
-> (String -> Integer -> Impossible)
-> String
-> Integer
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 0 String -> Integer -> Impossible
Impossible String
a Integer
b
  icod_ (Unreachable a :: String
a b :: Integer
b) = Int32
-> (String -> Integer -> Impossible)
-> String
-> Integer
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 String -> Integer -> Impossible
Unreachable String
a Integer
b
  icod_ (ImpMissingDefinitions a :: [String]
a b :: String
b) = Int32
-> ([String] -> String -> Impossible)
-> [String]
-> String
-> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 2 [String] -> String -> Impossible
ImpMissingDefinitions [String]
a String
b

  value :: Int32 -> R Impossible
value = (Node -> R Impossible) -> Int32 -> R Impossible
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R Impossible
valu where
    valu :: Node -> R Impossible
valu [0, a :: Int32
a, b :: Int32
b] = (String -> Integer -> Impossible) -> Int32 -> Int32 -> R Impossible
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 -> Integer -> Impossible
Impossible  Int32
a Int32
b
    valu [1, a :: Int32
a, b :: Int32
b] = (String -> Integer -> Impossible) -> Int32 -> Int32 -> R Impossible
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 -> Integer -> Impossible
Unreachable Int32
a Int32
b
    valu [2, a :: Int32
a, b :: Int32
b] = ([String] -> String -> Impossible)
-> Int32 -> Int32 -> R Impossible
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 _         = R Impossible
forall a. R a
malformed

instance EmbPrj Empty where
  icod_ :: Empty -> S Int32
icod_ a :: Empty
a = Impossible -> S Int32
forall a. EmbPrj a => a -> S Int32
icod_ (Impossible -> S Int32) -> ReaderT Dict IO Impossible -> S Int32
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO Impossible -> ReaderT Dict IO Impossible
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Empty -> IO Impossible
Empty.toImpossible Empty
a)

  value :: Int32 -> R Empty
value = (Impossible -> Empty) -> R Impossible -> R Empty
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Impossible -> Empty
forall a. Impossible -> a
throwImpossible (R Impossible -> R Empty)
-> (Int32 -> R Impossible) -> Int32 -> R Empty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int32 -> R Impossible
forall a. EmbPrj a => Int32 -> R a
value

instance EmbPrj ExpandedEllipsis where
  icod_ :: ExpandedEllipsis -> S Int32
icod_ NoEllipsis = ExpandedEllipsis -> Arrows (Domains ExpandedEllipsis) (S Int32)
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 a :: Range
a b :: Int
b) = Int32
-> (Range -> Int -> ExpandedEllipsis) -> Range -> Int -> S Int32
forall t.
(ICODE t (IsBase t), Currying (Domains t) (S Int32),
 All EmbPrj (Domains t)) =>
Int32 -> t -> Arrows (Domains t) (S Int32)
icodeN 1 Range -> Int -> ExpandedEllipsis
ExpandedEllipsis Range
a Int
b

  value :: Int32 -> R ExpandedEllipsis
value = (Node -> R ExpandedEllipsis) -> Int32 -> R ExpandedEllipsis
forall a. EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase Node -> R ExpandedEllipsis
valu where
    valu :: Node -> R ExpandedEllipsis
valu []      = ExpandedEllipsis
-> Arrows
     (Constant Int32 (Domains ExpandedEllipsis))
     (R (CoDomain ExpandedEllipsis))
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 [1,a :: Int32
a,b :: Int32
b] = (Range -> Int -> ExpandedEllipsis)
-> Int32 -> Int32 -> R ExpandedEllipsis
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 _       = R ExpandedEllipsis
forall a. R a
malformed