{-# LANGUAGE UndecidableInstances #-}

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

-- | Serializing types that are not Agda-specific.

module Agda.TypeChecking.Serialise.Instances.General where

import Control.Monad              ( (<=<), (<$!>) )
import Control.Monad.State.Strict ( gets)

import Data.Array.IArray
import qualified Data.Foldable as Fold
import Data.Hashable
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HMap
import Data.Int (Int32)
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Strict.Tuple (Pair(..))
import qualified Data.Text      as T
import qualified Data.Text.Lazy as TL
import Data.Typeable
import Data.Void
import Data.Word (Word32, Word64)

import Agda.TypeChecking.Serialise.Base

import Agda.Utils.BiMap (BiMap)
import qualified Agda.Utils.BiMap as BiMap
import Agda.Utils.DocTree qualified as DocTree
import Agda.Utils.List1 (List1)
import qualified Agda.Utils.List1 as List1
import Agda.Utils.List2 (List2)
import qualified Agda.Utils.List2 as List2
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.SmallSet (SmallSet(..))
import Agda.Utils.Set1 (Set1)
import qualified Agda.Utils.Set1 as Set1
import Agda.Utils.Trie (Trie(..))
import Agda.Utils.VarSet (VarSet(..))
import Agda.Utils.WithDefault

---------------------------------------------------------------------------
-- Base types

instance EmbPrj Void where
  icod_ :: Void -> S Word32
icod_ = Void -> S Word32
forall a. Void -> a
absurd
  value :: Word32 -> R Void
value = ([Word32] -> R Void) -> Word32 -> R Void
forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
vcase [Word32] -> R Void
forall {p} {a}. p -> R a
valu where valu :: p -> R a
valu p
_ = R a
forall a. R a
malformed

instance EmbPrj () where
  icod_ :: () -> S Word32
icod_ () = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
0

  value :: Word32 -> R ()
value Word32
0 = () -> R ()
forall a. a -> StateT St IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  value Word32
_ = R ()
forall a. R a
malformed

instance EmbPrj Bool where
  icod_ :: Bool -> S Word32
icod_ Bool
False = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
0
  icod_ Bool
True  = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word32
1

  value :: Word32 -> R Bool
value Word32
0 = Bool -> R Bool
forall a. a -> StateT St IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
  value Word32
1 = Bool -> R Bool
forall a. a -> StateT St IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
  value Word32
_ = R Bool
forall a. R a
malformed

instance EmbPrj Char where
  icod_ :: Char -> S Word32
icod_ Char
c = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Word32 -> S Word32) -> Word32 -> S Word32
forall a b. (a -> b) -> a -> b
$! Int -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word32) -> Int -> Word32
forall a b. (a -> b) -> a -> b
$ Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c
  value :: Word32 -> R Char
value Word32
i = Char -> R Char
forall a. a -> StateT St IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Char -> R Char) -> Char -> R Char
forall a b. (a -> b) -> a -> b
$! 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
$ Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
i

-- Numeric types

instance EmbPrj Double where
  icod_ :: Double -> S Word32
icod_   = Double -> S Word32
icodeDouble
  value :: Word32 -> R Double
value Word32
i = (Array Word32 Double -> Word32 -> Double
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Word32
i) (Array Word32 Double -> Double)
-> StateT St IO (Array Word32 Double) -> R Double
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> (St -> Array Word32 Double) -> StateT St IO (Array Word32 Double)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Word32 Double
doubleE

-- Andreas, Agda Hackathon 2024-10-15
-- Are we sure we never use an Int that does not fit into 32 bits?
instance EmbPrj Int where
  icod_ :: Int -> S Word32
icod_ Int
i = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Word32 -> S Word32) -> Word32 -> S Word32
forall a b. (a -> b) -> a -> b
$! Int -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i
  value :: Word32 -> R Int
value Word32
i = Int -> R Int
forall a. a -> StateT St IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> R Int) -> Int -> R Int
forall a b. (a -> b) -> a -> b
$! Word32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
i

instance EmbPrj Int32 where
  icod_ :: Int32 -> S Word32
icod_ Int32
i = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Word32 -> S Word32) -> Word32 -> S Word32
forall a b. (a -> b) -> a -> b
$! Int32 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
i
  value :: Word32 -> R Int32
value Word32
i = Int32 -> R Int32
forall a. a -> StateT St IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int32 -> R Int32) -> Int32 -> R Int32
forall a b. (a -> b) -> a -> b
$! Word32 -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
i

instance EmbPrj Integer where
  icod_ :: Integer -> S Word32
icod_   = Integer -> S Word32
icodeInteger
  value :: Word32 -> R Integer
value Word32
i = (Array Word32 Integer -> Word32 -> Integer
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Word32
i) (Array Word32 Integer -> Integer)
-> StateT St IO (Array Word32 Integer) -> R Integer
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> (St -> Array Word32 Integer) -> StateT St IO (Array Word32 Integer)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Word32 Integer
integerE

instance EmbPrj Word32 where
  icod_ :: Word32 -> S Word32
icod_ Word32
i = Word32 -> S Word32
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
i
  value :: Word32 -> R Word32
value Word32
i = Word32 -> R Word32
forall a. a -> StateT St IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Word32
i

instance EmbPrj Word64 where
  icod_ :: Word64 -> S Word32
icod_ Word64
i = (Word32 -> Word32 -> Word32)
-> Arrows (Domains (Word32 -> Word32 -> Word32)) (S Word32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' (Word32 -> Word32 -> Word32
forall a. HasCallStack => a
undefined :: Word32 -> Word32 -> Word32) (Word64 -> Word32
word32 Word64
q) (Word64 -> Word32
word32 Word64
r)
    where (Word64
q, Word64
r) = Word64 -> Word64 -> (Word64, Word64)
forall a. Integral a => a -> a -> (a, a)
quotRem Word64
i (Word64
2 Word64 -> Integer -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
32)
          word32 :: Word64 -> Word32
          word32 :: Word64 -> Word32
word32 = Word64 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral

  value :: Word32 -> R Word64
value = ([Word32] -> R Word64) -> Word32 -> R Word64
forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
vcase [Word32] -> R Word64
valu where
    valu :: [Word32] -> R Word64
valu [Word32
a, Word32
b] = Word64 -> R Word64
forall a. a -> StateT St IO a
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
* Word32 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
a Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word32 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
b
    valu [Word32]
_      = R Word64
forall a. R a
malformed
    n :: Word64
n = Word64
2 Word64 -> Integer -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
32

-- Text types

instance {-# OVERLAPPING #-} EmbPrj String where
  icod_ :: String -> S Word32
icod_   = String -> S Word32
icodeString
  value :: Word32 -> R String
value Word32
i = (Array Word32 String -> Word32 -> String
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Word32
i) (Array Word32 String -> String)
-> StateT St IO (Array Word32 String) -> R String
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> (St -> Array Word32 String) -> StateT St IO (Array Word32 String)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Word32 String
stringE

instance EmbPrj TL.Text where
  icod_ :: Text -> S Word32
icod_   = (Dict -> HashTable Text Word32)
-> (Dict -> IORef FreshAndReuse) -> Text -> S Word32
forall k.
(Eq k, Hashable k) =>
(Dict -> HashTable k Word32)
-> (Dict -> IORef FreshAndReuse) -> k -> S Word32
icodeX Dict -> HashTable Text Word32
lTextD Dict -> IORef FreshAndReuse
lTextC
  value :: Word32 -> R Text
value Word32
i = (Array Word32 Text -> Word32 -> Text
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Word32
i) (Array Word32 Text -> Text)
-> StateT St IO (Array Word32 Text) -> R Text
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> (St -> Array Word32 Text) -> StateT St IO (Array Word32 Text)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Word32 Text
lTextE

instance EmbPrj T.Text where
  icod_ :: Text -> S Word32
icod_   = (Dict -> HashTable Text Word32)
-> (Dict -> IORef FreshAndReuse) -> Text -> S Word32
forall k.
(Eq k, Hashable k) =>
(Dict -> HashTable k Word32)
-> (Dict -> IORef FreshAndReuse) -> k -> S Word32
icodeX Dict -> HashTable Text Word32
sTextD Dict -> IORef FreshAndReuse
sTextC
  value :: Word32 -> R Text
value Word32
i = (Array Word32 Text -> Word32 -> Text
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Word32
i) (Array Word32 Text -> Text)
-> StateT St IO (Array Word32 Text) -> R Text
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> (St -> Array Word32 Text) -> StateT St IO (Array Word32 Text)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Word32 Text
sTextE

---------------------------------------------------------------------------
-- Non-recursive types

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

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

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

  value :: Word32 -> R (Pair a b)
value = (a -> b -> Pair a b) -> Word32 -> R (CoDomain (a -> b -> Pair a b))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN a -> b -> Pair a b
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 Word32
icod_ (a
a, b
b, c
c) = (a -> b -> c -> (a, b, c))
-> Arrows (Domains (a -> b -> c -> (a, b, c))) (S Word32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' (,,) a
a b
b c
c

  value :: Word32 -> R (a, b, c)
value = (a -> b -> c -> (a, b, c))
-> Word32 -> R (CoDomain (a -> b -> c -> (a, b, c)))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN (,,)

instance (EmbPrj a, EmbPrj b) => EmbPrj (Either a b) where
  icod_ :: Either a b -> S Word32
icod_ (Left  a
x) = Word32
-> (a -> Either a (ZonkAny 6))
-> Arrows (Domains (a -> Either a (ZonkAny 6))) (S Word32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
0 a -> Either a (ZonkAny 6)
forall a b. a -> Either a b
Left a
x
  icod_ (Right b
x) = Word32
-> (b -> Either (ZonkAny 7) b)
-> Arrows (Domains (b -> Either (ZonkAny 7) b)) (S Word32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
Word32 -> t -> Arrows (Domains t) (S Word32)
icodeN Word32
1 b -> Either (ZonkAny 7) b
forall a b. b -> Either a b
Right b
x

  value :: Word32 -> R (Either a b)
value = ([Word32] -> R (Either a b)) -> Word32 -> R (Either a b)
forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
vcase [Word32] -> R (Either a b)
forall {a} {b}. (EmbPrj a, EmbPrj b) => [Word32] -> R (Either a b)
valu where
    valu :: [Word32] -> R (Either a b)
valu [Word32
0, Word32
x] = (a -> Either a b)
-> Arrows
     (Constant Word32 (Domains (a -> Either a b)))
     (R (CoDomain (a -> Either a b)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN a -> Either a b
forall a b. a -> Either a b
Left  Word32
x
    valu [Word32
1, Word32
x] = (b -> Either a b)
-> Arrows
     (Constant Word32 (Domains (b -> Either a b)))
     (R (CoDomain (b -> Either a b)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN b -> Either a b
forall a b. b -> Either a b
Right Word32
x
    valu [Word32]
_   = R (Either a b)
forall a. R a
malformed

instance EmbPrj a => EmbPrj (Maybe a) where
  icod_ :: Maybe a -> S Word32
icod_ Maybe a
Nothing  = Maybe (ZonkAny 5)
-> Arrows (Domains (Maybe (ZonkAny 5))) (S Word32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Maybe (ZonkAny 5)
forall a. Maybe a
Nothing
  icod_ (Just a
x) = (a -> Maybe a) -> Arrows (Domains (a -> Maybe a)) (S Word32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' a -> Maybe a
forall a. a -> Maybe a
Just a
x

  value :: Word32 -> R (Maybe a)
value = ([Word32] -> R (Maybe a)) -> Word32 -> R (Maybe a)
forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
vcase [Word32] -> R (Maybe a)
forall {a}. EmbPrj a => [Word32] -> StateT St IO (Maybe a)
valu where
    valu :: [Word32]
-> Arrows
     (Constant Word32 (Domains (Maybe a))) (R (CoDomain (Maybe a)))
valu []  = Maybe a
-> Arrows
     (Constant Word32 (Domains (Maybe a))) (R (CoDomain (Maybe a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Maybe a
forall a. Maybe a
Nothing
    valu [Word32
x] = (a -> Maybe a)
-> Arrows
     (Constant Word32 (Domains (a -> Maybe a)))
     (R (CoDomain (a -> Maybe a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN a -> Maybe a
forall a. a -> Maybe a
Just Word32
x
    valu [Word32]
_   = StateT St IO (Maybe a)
Arrows
  (Constant Word32 (Domains (Maybe a))) (R (CoDomain (Maybe a)))
forall a. R a
malformed

instance EmbPrj a => EmbPrj (Strict.Maybe a) where
  icod_ :: Maybe a -> S Word32
icod_ Maybe a
m = Maybe a -> S Word32
forall a. EmbPrj a => a -> S Word32
icode (Maybe a -> Maybe a
forall lazy strict. Strict lazy strict => strict -> lazy
Strict.toLazy Maybe a
m)
  value :: Word32 -> R (Maybe a)
value Word32
m = Maybe a -> Maybe a
forall lazy strict. Strict lazy strict => lazy -> strict
Strict.toStrict (Maybe a -> Maybe a) -> StateT St IO (Maybe a) -> R (Maybe a)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Word32 -> StateT St IO (Maybe a)
forall a. EmbPrj a => Word32 -> R a
value Word32
m

instance (EmbPrj a, Typeable b) => EmbPrj (WithDefault' a b) where
  icod_ :: WithDefault' a b -> S Word32
icod_ = \case
    WithDefault' a b
Default -> WithDefault' (ZonkAny 2) (ZonkAny 3)
-> Arrows
     (Domains (WithDefault' (ZonkAny 2) (ZonkAny 3))) (S Word32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' WithDefault' (ZonkAny 2) (ZonkAny 3)
forall a (b :: Bool). WithDefault' a b
Default
    Value a
b -> (a -> WithDefault' a (ZonkAny 4))
-> Arrows (Domains (a -> WithDefault' a (ZonkAny 4))) (S Word32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' a -> WithDefault' a (ZonkAny 4)
forall a (b :: Bool). a -> WithDefault' a b
Value a
b

  value :: Word32 -> R (WithDefault' a b)
value = ([Word32] -> R (WithDefault' a b))
-> Word32 -> R (WithDefault' a b)
forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
vcase (([Word32] -> R (WithDefault' a b))
 -> Word32 -> R (WithDefault' a b))
-> ([Word32] -> R (WithDefault' a b))
-> Word32
-> R (WithDefault' a b)
forall a b. (a -> b) -> a -> b
$ \case
    []  -> WithDefault' a b
-> Arrows
     (Constant Word32 (Domains (WithDefault' a b)))
     (R (CoDomain (WithDefault' a b)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN WithDefault' a b
forall a (b :: Bool). WithDefault' a b
Default
    [Word32
a] -> (a -> WithDefault' a b)
-> Arrows
     (Constant Word32 (Domains (a -> WithDefault' a b)))
     (R (CoDomain (a -> WithDefault' a b)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN a -> WithDefault' a b
forall a (b :: Bool). a -> WithDefault' a b
Value Word32
a
    [Word32]
_ -> R (WithDefault' a b)
forall a. R a
malformed

---------------------------------------------------------------------------
-- Sequences

instance {-# OVERLAPPABLE #-} EmbPrj a => EmbPrj [a] where
  icod_ :: [a] -> S Word32
icod_ [a]
xs = Node -> S Word32
icodeNode (Node -> S Word32) -> ReaderT Dict IO Node -> S Word32
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [a] -> ReaderT Dict IO Node
go [a]
xs where
    go :: [a] -> S Node
    go :: [a] -> ReaderT Dict IO Node
go []     = Node -> ReaderT Dict IO Node
forall a. a -> ReaderT Dict IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Node
Empty
    go (a
a:[a]
as) = do {n <- a -> S Word32
forall a. EmbPrj a => a -> S Word32
icode a
a; ns <- go as; pure $! Cons n ns}

  value :: Word32 -> R [a]
value = ([Word32] -> R [a]) -> Word32 -> R [a]
forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
vcase ((Word32 -> StateT St IO a) -> [Word32] -> R [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Word32 -> StateT St IO a
forall a. EmbPrj a => Word32 -> R a
value)

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

instance EmbPrj a => EmbPrj (List2 a) where
  icod_ :: List2 a -> S Word32
icod_ = [a] -> S Word32
forall a. EmbPrj a => a -> S Word32
icod_ ([a] -> S Word32) -> (List2 a -> [a]) -> List2 a -> S Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List2 a -> [a]
List2 a -> [Item (List2 a)]
forall l. IsList l => l -> [Item l]
List2.toList
  value :: Word32 -> R (List2 a)
value = R (List2 a)
-> (List2 a -> R (List2 a)) -> Maybe (List2 a) -> R (List2 a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe R (List2 a)
forall a. R a
malformed List2 a -> R (List2 a)
forall a. a -> StateT St IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (List2 a) -> R (List2 a))
-> ([a] -> Maybe (List2 a)) -> [a] -> R (List2 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Maybe (List2 a)
forall a. [a] -> Maybe (List2 a)
List2.fromListMaybe ([a] -> R (List2 a))
-> (Word32 -> StateT St IO [a]) -> Word32 -> R (List2 a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Word32 -> StateT St IO [a]
forall a. EmbPrj a => Word32 -> R a
value

instance EmbPrj a => EmbPrj (Seq a) where
  icod_ :: Seq a -> S Word32
icod_ Seq a
s = [a] -> S Word32
forall a. EmbPrj a => a -> S Word32
icode (Seq a -> [a]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq a
s)
  value :: Word32 -> R (Seq a)
value Word32
s = [a] -> Seq a
forall a. [a] -> Seq a
Seq.fromList ([a] -> Seq a) -> StateT St IO [a] -> R (Seq a)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Word32 -> StateT St IO [a]
forall a. EmbPrj a => Word32 -> R a
value Word32
s

-- | Encode a list of key-value pairs as a flat list.
mapPairsIcode :: (EmbPrj k, EmbPrj v) => [(k, v)] -> S Word32
mapPairsIcode :: forall k v. (EmbPrj k, EmbPrj v) => [(k, v)] -> S Word32
mapPairsIcode [(k, v)]
xs = Node -> S Word32
icodeNode (Node -> S Word32) -> ReaderT Dict IO Node -> S Word32
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Node -> [(k, v)] -> ReaderT Dict IO Node
forall {a} {a}.
(EmbPrj a, EmbPrj a) =>
Node -> [(a, a)] -> ReaderT Dict IO Node
convert Node
Empty [(k, v)]
xs where
  -- As we need to call `convert' in the tail position, the resulting list is
  -- written (and read) in reverse order, with the highest pair first in the
  -- resulting list.
  convert :: Node -> [(a, a)] -> ReaderT Dict IO Node
convert !Node
ys [] = Node -> ReaderT Dict IO Node
forall a. a -> ReaderT Dict IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Node
ys
  convert  Node
ys ((a
start, a
entry):[(a, a)]
xs) = do
    start <- a -> S Word32
forall a. EmbPrj a => a -> S Word32
icode a
start
    entry <- icode entry
    convert (Cons start (Cons entry ys)) xs

mapPairsValue :: (EmbPrj k, EmbPrj v) => [Word32] -> R [(k, v)]
mapPairsValue :: forall k v. (EmbPrj k, EmbPrj v) => [Word32] -> R [(k, v)]
mapPairsValue = [(k, v)] -> [Word32] -> StateT St IO [(k, v)]
forall {a} {b}.
(EmbPrj a, EmbPrj b) =>
[(a, b)] -> [Word32] -> StateT St IO [(a, b)]
convert [] where
  convert :: [(a, b)] -> [Word32] -> StateT St IO [(a, b)]
convert [(a, b)]
ys [] = [(a, b)] -> StateT St IO [(a, b)]
forall a. a -> StateT St IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(a, b)]
ys
  convert [(a, b)]
ys (Word32
start:Word32
entry:[Word32]
xs) = do
    !start <- Word32 -> R a
forall a. EmbPrj a => Word32 -> R a
value Word32
start
    !entry <- value entry
    convert ((start, entry):ys) xs
  convert [(a, b)]
_ [Word32]
_ = StateT St IO [(a, b)]
forall a. R a
malformed

---------------------------------------------------------------------------
-- Maps

instance (EmbPrj k, EmbPrj v, EmbPrj (BiMap.Tag v)) =>
         EmbPrj (BiMap k v) where
  icod_ :: BiMap k v -> S Word32
icod_ BiMap k v
m = ([(k, v)], [(Tag v, k)]) -> S Word32
forall a. EmbPrj a => a -> S Word32
icode (BiMap k v -> ([(k, v)], [(Tag v, k)])
forall k v. BiMap k v -> ([(k, v)], [(Tag v, k)])
BiMap.toDistinctAscendingLists BiMap k v
m)
  value :: Word32 -> R (BiMap k v)
value Word32
m = ([(k, v)], [(Tag v, k)]) -> BiMap k v
forall k v. ([(k, v)], [(Tag v, k)]) -> BiMap k v
BiMap.fromDistinctAscendingLists (([(k, v)], [(Tag v, k)]) -> BiMap k v)
-> StateT St IO ([(k, v)], [(Tag v, k)]) -> R (BiMap k v)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Word32 -> StateT St IO ([(k, v)], [(Tag v, k)])
forall a. EmbPrj a => Word32 -> R a
value Word32
m

instance (Eq k, Hashable k, EmbPrj k, EmbPrj v) => EmbPrj (HashMap k v) where
  icod_ :: HashMap k v -> S Word32
icod_ HashMap k v
m = [(k, v)] -> S Word32
forall k v. (EmbPrj k, EmbPrj v) => [(k, v)] -> S Word32
mapPairsIcode (HashMap k v -> [(k, v)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList HashMap k v
m)
  value :: Word32 -> R (HashMap k v)
value = ([Word32] -> R (HashMap k v)) -> Word32 -> R (HashMap k v)
forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
vcase (([(k, v)] -> HashMap k v
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HMap.fromList ([(k, v)] -> HashMap k v)
-> StateT St IO [(k, v)] -> R (HashMap k v)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!>) (StateT St IO [(k, v)] -> R (HashMap k v))
-> ([Word32] -> StateT St IO [(k, v)])
-> [Word32]
-> R (HashMap k v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word32] -> StateT St IO [(k, v)]
forall k v. (EmbPrj k, EmbPrj v) => [Word32] -> R [(k, v)]
mapPairsValue)

instance (Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) where
  icod_ :: Map a b -> S Word32
icod_ Map a b
m = [(a, b)] -> S Word32
forall k v. (EmbPrj k, EmbPrj v) => [(k, v)] -> S Word32
mapPairsIcode (Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map a b
m)
  value :: Word32 -> R (Map a b)
value = ([Word32] -> R (Map a b)) -> Word32 -> R (Map a b)
forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
vcase (([(a, b)] -> Map a b
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList ([(a, b)] -> Map a b) -> StateT St IO [(a, b)] -> R (Map a b)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!>) (StateT St IO [(a, b)] -> R (Map a b))
-> ([Word32] -> StateT St IO [(a, b)]) -> [Word32] -> R (Map a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word32] -> StateT St IO [(a, b)]
forall k v. (EmbPrj k, EmbPrj v) => [Word32] -> R [(k, v)]
mapPairsValue)

---------------------------------------------------------------------------
-- Sets

instance EmbPrj IntSet where
  icod_ :: IntSet -> S Word32
icod_ IntSet
s = [Int] -> S Word32
forall a. EmbPrj a => a -> S Word32
icode (IntSet -> [Int]
IntSet.toAscList IntSet
s)
  value :: Word32 -> R IntSet
value Word32
s = [Int] -> IntSet
IntSet.fromDistinctAscList ([Int] -> IntSet) -> StateT St IO [Int] -> R IntSet
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Word32 -> StateT St IO [Int]
forall a. EmbPrj a => Word32 -> R a
value Word32
s

instance (Ord a, EmbPrj a) => EmbPrj (Set a) where
  icod_ :: Set a -> S Word32
icod_ Set a
s = [a] -> S Word32
forall a. EmbPrj a => a -> S Word32
icode (Set a -> [a]
forall a. Set a -> [a]
Set.toAscList Set a
s)
  value :: Word32 -> R (Set a)
value Word32
s = [a] -> Set a
forall a. [a] -> Set a
Set.fromDistinctAscList ([a] -> Set a) -> StateT St IO [a] -> R (Set a)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Word32 -> StateT St IO [a]
forall a. EmbPrj a => Word32 -> R a
value Word32
s

instance (Ord a, EmbPrj a) => EmbPrj (Set1 a) where
  icod_ :: Set1 a -> S Word32
icod_ Set1 a
s = NonEmpty a -> S Word32
forall a. EmbPrj a => a -> S Word32
icode (Set1 a -> NonEmpty a
forall a. NESet a -> NonEmpty a
Set1.toAscList Set1 a
s)
  value :: Word32 -> R (Set1 a)
value Word32
s = NonEmpty a -> Set1 a
forall a. NonEmpty a -> NESet a
Set1.fromDistinctAscList (NonEmpty a -> Set1 a) -> StateT St IO (NonEmpty a) -> R (Set1 a)
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> Word32 -> StateT St IO (NonEmpty a)
forall a. EmbPrj a => Word32 -> R a
value Word32
s

instance Typeable a => EmbPrj (SmallSet a) where
  icod_ :: SmallSet a -> S Word32
icod_ (SmallSet Word64
a) = (Word64 -> SmallSet (ZonkAny 1))
-> Arrows (Domains (Word64 -> SmallSet (ZonkAny 1))) (S Word32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Word64 -> SmallSet (ZonkAny 1)
forall a. Word64 -> SmallSet a
SmallSet Word64
a
  value :: Word32 -> R (SmallSet a)
value = (Word64 -> SmallSet a)
-> Word32 -> R (CoDomain (Word64 -> SmallSet a))
forall t.
(VALU t (IsBase t), All EmbPrj (CoDomain t : Domains t)) =>
t -> Word32 -> R (CoDomain t)
valueN Word64 -> SmallSet a
forall a. Word64 -> SmallSet a
SmallSet

instance EmbPrj VarSet where
  icod_ :: VarSet -> S Word32
icod_   = VarSet -> S Word32
icodeVarSet
  value :: Word32 -> R VarSet
value Word32
i = (Array Word32 VarSet -> Word32 -> VarSet
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Word32
i) (Array Word32 VarSet -> VarSet)
-> StateT St IO (Array Word32 VarSet) -> R VarSet
forall (m :: * -> *) a b. Monad m => (a -> b) -> m a -> m b
<$!> (St -> Array Word32 VarSet) -> StateT St IO (Array Word32 VarSet)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St -> Array Word32 VarSet
varSetE

---------------------------------------------------------------------------
-- Trees

instance (Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Trie a b) where
  icod_ :: Trie a b -> S Word32
icod_ (Trie Maybe b
a Map a (Trie a b)
b) = (Maybe b -> Map a (Trie a b) -> Trie a b)
-> Arrows
     (Domains (Maybe b -> Map a (Trie a b) -> Trie a b)) (S Word32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
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 :: Word32 -> R (Trie a b)
value = (Maybe b -> Map a (Trie a b) -> Trie a b)
-> Word32 -> 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 -> Word32 -> 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 (DocTree.DocTree a) where
  icod_ :: DocTree a -> S Word32
icod_ = \case
    DocTree.Text Text
a   -> (Text -> DocTree (ZonkAny 0))
-> Arrows (Domains (Text -> DocTree (ZonkAny 0))) (S Word32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' Text -> DocTree (ZonkAny 0)
forall ann. Text -> DocTree ann
DocTree.Text Text
a
    DocTree.Node a
a [DocTree a]
b -> (a -> [DocTree a] -> DocTree a)
-> Arrows (Domains (a -> [DocTree a] -> DocTree a)) (S Word32)
forall t.
(ICODE t (IsBase t), StrictCurrying (Domains t) (S Word32),
 All EmbPrj (Domains t)) =>
t -> Arrows (Domains t) (S Word32)
icodeN' a -> [DocTree a] -> DocTree a
forall ann. ann -> [DocTree ann] -> DocTree ann
DocTree.Node a
a [DocTree a]
b

  value :: Word32 -> R (DocTree a)
value = ([Word32] -> R (DocTree a)) -> Word32 -> R (DocTree a)
forall a. EmbPrj a => ([Word32] -> R a) -> Word32 -> R a
vcase \case
    [Word32
a]    -> (Text -> DocTree a)
-> Arrows
     (Constant Word32 (Domains (Text -> DocTree a)))
     (R (CoDomain (Text -> DocTree a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN Text -> DocTree a
forall ann. Text -> DocTree ann
DocTree.Text Word32
a
    [Word32
a, Word32
b] -> (a -> [DocTree a] -> DocTree a)
-> Arrows
     (Constant Word32 (Domains (a -> [DocTree a] -> DocTree a)))
     (R (CoDomain (a -> [DocTree a] -> DocTree a)))
forall t.
(VALU t (IsBase t),
 StrictCurrying (Constant Word32 (Domains t)) (R (CoDomain t)),
 All EmbPrj (Domains t)) =>
t -> Arrows (Constant Word32 (Domains t)) (R (CoDomain t))
valuN a -> [DocTree a] -> DocTree a
forall ann. ann -> [DocTree ann] -> DocTree ann
DocTree.Node Word32
a Word32
b
    [Word32]
_      -> R (DocTree a)
forall a. R a
malformed