{-# LANGUAGE GeneralizedNewtypeDeriving, UndecidableInstances, MagicHash, UnboxedTuples #-}

{-# OPTIONS_GHC -ddump-to-file -ddump-simpl -dsuppress-all -dno-suppress-type-signatures #-}

module Agda.Utils.MinimalArray.Lifted where

import qualified Data.Foldable
import GHC.Exts
import qualified GHC.Arr as GHC
import qualified Data.Primitive.Array as A
import Control.Monad.Primitive

import Agda.Utils.Serialize
import qualified Agda.Utils.Serialize as Ser

newtype Array a = Array {forall a. Array a -> Array a
unwrap :: A.Array a}
  deriving (Array a -> Array a -> Bool
(Array a -> Array a -> Bool)
-> (Array a -> Array a -> Bool) -> Eq (Array a)
forall a. Eq a => Array a -> Array a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Array a -> Array a -> Bool
== :: Array a -> Array a -> Bool
$c/= :: forall a. Eq a => Array a -> Array a -> Bool
/= :: Array a -> Array a -> Bool
Eq, Int -> Array a -> ShowS
[Array a] -> ShowS
Array a -> String
(Int -> Array a -> ShowS)
-> (Array a -> String) -> ([Array a] -> ShowS) -> Show (Array a)
forall a. Show a => Int -> Array a -> ShowS
forall a. Show a => [Array a] -> ShowS
forall a. Show a => Array a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Array a -> ShowS
showsPrec :: Int -> Array a -> ShowS
$cshow :: forall a. Show a => Array a -> String
show :: Array a -> String
$cshowList :: forall a. Show a => [Array a] -> ShowS
showList :: [Array a] -> ShowS
Show, Int -> [Item (Array a)] -> Array a
[Item (Array a)] -> Array a
Array a -> [Item (Array a)]
([Item (Array a)] -> Array a)
-> (Int -> [Item (Array a)] -> Array a)
-> (Array a -> [Item (Array a)])
-> IsList (Array a)
forall a. Int -> [Item (Array a)] -> Array a
forall a. [Item (Array a)] -> Array a
forall a. Array a -> [Item (Array a)]
forall l.
([Item l] -> l)
-> (Int -> [Item l] -> l) -> (l -> [Item l]) -> IsList l
$cfromList :: forall a. [Item (Array a)] -> Array a
fromList :: [Item (Array a)] -> Array a
$cfromListN :: forall a. Int -> [Item (Array a)] -> Array a
fromListN :: Int -> [Item (Array a)] -> Array a
$ctoList :: forall a. Array a -> [Item (Array a)]
toList :: Array a -> [Item (Array a)]
IsList, (forall a b. (a -> b) -> Array a -> Array b)
-> (forall a b. a -> Array b -> Array a) -> Functor Array
forall a b. a -> Array b -> Array a
forall a b. (a -> b) -> Array a -> Array b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Array a -> Array b
fmap :: forall a b. (a -> b) -> Array a -> Array b
$c<$ :: forall a b. a -> Array b -> Array a
<$ :: forall a b. a -> Array b -> Array a
Functor, (forall m. Monoid m => Array m -> m)
-> (forall m a. Monoid m => (a -> m) -> Array a -> m)
-> (forall m a. Monoid m => (a -> m) -> Array a -> m)
-> (forall a b. (a -> b -> b) -> b -> Array a -> b)
-> (forall a b. (a -> b -> b) -> b -> Array a -> b)
-> (forall b a. (b -> a -> b) -> b -> Array a -> b)
-> (forall b a. (b -> a -> b) -> b -> Array a -> b)
-> (forall a. (a -> a -> a) -> Array a -> a)
-> (forall a. (a -> a -> a) -> Array a -> a)
-> (forall a. Array a -> [a])
-> (forall a. Array a -> Bool)
-> (forall a. Array a -> Int)
-> (forall a. Eq a => a -> Array a -> Bool)
-> (forall a. Ord a => Array a -> a)
-> (forall a. Ord a => Array a -> a)
-> (forall a. Num a => Array a -> a)
-> (forall a. Num a => Array a -> a)
-> Foldable Array
forall a. Eq a => a -> Array a -> Bool
forall a. Num a => Array a -> a
forall a. Ord a => Array a -> a
forall m. Monoid m => Array m -> m
forall a. Array a -> Bool
forall a. Array a -> Int
forall a. Array a -> [a]
forall a. (a -> a -> a) -> Array a -> a
forall m a. Monoid m => (a -> m) -> Array a -> m
forall b a. (b -> a -> b) -> b -> Array a -> b
forall a b. (a -> b -> b) -> b -> Array a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Array m -> m
fold :: forall m. Monoid m => Array m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Array a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Array a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Array a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Array a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Array a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Array a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Array a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Array a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Array a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Array a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Array a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Array a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Array a -> a
foldr1 :: forall a. (a -> a -> a) -> Array a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Array a -> a
foldl1 :: forall a. (a -> a -> a) -> Array a -> a
$ctoList :: forall a. Array a -> [a]
toList :: forall a. Array a -> [a]
$cnull :: forall a. Array a -> Bool
null :: forall a. Array a -> Bool
$clength :: forall a. Array a -> Int
length :: forall a. Array a -> Int
$celem :: forall a. Eq a => a -> Array a -> Bool
elem :: forall a. Eq a => a -> Array a -> Bool
$cmaximum :: forall a. Ord a => Array a -> a
maximum :: forall a. Ord a => Array a -> a
$cminimum :: forall a. Ord a => Array a -> a
minimum :: forall a. Ord a => Array a -> a
$csum :: forall a. Num a => Array a -> a
sum :: forall a. Num a => Array a -> a
$cproduct :: forall a. Num a => Array a -> a
product :: forall a. Num a => Array a -> a
Foldable, Functor Array
Foldable Array
(Functor Array, Foldable Array) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Array a -> f (Array b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Array (f a) -> f (Array a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Array a -> m (Array b))
-> (forall (m :: * -> *) a. Monad m => Array (m a) -> m (Array a))
-> Traversable Array
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Array (m a) -> m (Array a)
forall (f :: * -> *) a. Applicative f => Array (f a) -> f (Array a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Array a -> m (Array b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Array a -> f (Array b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Array a -> f (Array b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Array a -> f (Array b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Array (f a) -> f (Array a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Array (f a) -> f (Array a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Array a -> m (Array b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Array a -> m (Array b)
$csequence :: forall (m :: * -> *) a. Monad m => Array (m a) -> m (Array a)
sequence :: forall (m :: * -> *) a. Monad m => Array (m a) -> m (Array a)
Traversable)

{-# INLINE size #-}
size :: Array a -> Int
size :: forall a. Array a -> Int
size (Array Array a
arr) = Array a -> Int
forall a. Array a -> Int
A.sizeofArray Array a
arr

{-# INLINE unsafeIndex #-}
unsafeIndex :: Array a -> Int -> a
unsafeIndex :: forall a. Array a -> Int -> a
unsafeIndex (Array Array a
arr) Int
i = Array a -> Int -> a
forall a. Array a -> Int -> a
A.indexArray Array a
arr Int
i

{-# INLINE index #-}
index :: Array a -> Int -> a
index :: forall a. Array a -> Int -> a
index Array a
arr Int
i | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Array a -> Int
forall a. Array a -> Int
Agda.Utils.MinimalArray.Lifted.size Array a
arr =
  Array a -> Int -> a
forall a. Array a -> Int -> a
unsafeIndex Array a
arr Int
i
index Array a
arr Int
i = String -> a
forall a. HasCallStack => String -> a
error String
"Array: out of bounds"

toList :: Array a -> [a]
toList :: forall a. Array a -> [a]
toList = Array a -> [a]
Array a -> [Item (Array a)]
forall l. IsList l => l -> [Item l]
GHC.Exts.toList

fromList :: [a] -> Array a
fromList :: forall a. [a] -> Array a
fromList = [a] -> Array a
[Item (Array a)] -> Array a
forall l. IsList l => [Item l] -> l
GHC.Exts.fromList

fromListN :: Int -> [a] -> Array a
fromListN :: forall a. Int -> [a] -> Array a
fromListN = Int -> [a] -> Array a
Int -> [Item (Array a)] -> Array a
forall l. IsList l => Int -> [Item l] -> l
GHC.Exts.fromListN

fromGHCArray :: GHC.Array i e -> Array e
fromGHCArray :: forall i e. Array i e -> Array e
fromGHCArray (GHC.Array i
_ i
_ Int
_ Array# e
arr) = Array e -> Array e
forall a. Array a -> Array a
Array (Array# e -> Array e
forall a. Array# a -> Array a
A.Array Array# e
arr)

instance Serialize a => Serialize (Array a) where
  size :: Array a -> Int
size = (Int -> a -> Int) -> Int -> Array a -> Int
forall b a. (b -> a -> b) -> b -> Array a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Data.Foldable.foldl' (\Int
s a
a -> a -> Int
forall a. Serialize a => a -> Int
Ser.size a
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
s) (Int -> Int
forall a. Serialize a => a -> Int
Ser.size (Int
0::Int))

  put :: Array a -> Put
put (Array (A.Array Array# a
arr)) = (Addr# -> RW -> (# Addr#, RW #)) -> Put
Put \Addr#
p RW
s ->
    let go :: Addr# -> State# RealWorld -> Int#
              -> Int# -> Array# a -> (# Addr#, State# RealWorld #)
        go :: Addr# -> RW -> Int# -> Int# -> Array# a -> (# Addr#, RW #)
go Addr#
p RW
s Int#
i Int#
sz Array# a
arr = case Int#
i Int# -> Int# -> Int#
==# Int#
sz of
          Int#
1# -> (# Addr#
p, RW
s #)
          Int#
_  -> case Array# a -> Int# -> (# a #)
forall a. Array# a -> Int# -> (# a #)
indexArray# Array# a
arr Int#
i of
            (# a
a #) -> case Put -> Addr# -> RW -> (# Addr#, RW #)
unPut (a -> Put
forall a. Serialize a => a -> Put
put a
a) Addr#
p RW
s of
              (# Addr#
p, RW
s #) -> Addr# -> RW -> Int# -> Int# -> Array# a -> (# Addr#, RW #)
go Addr#
p RW
s (Int#
i Int# -> Int# -> Int#
+# Int#
1#) Int#
sz Array# a
arr
        sz :: Int#
sz = Array# a -> Int#
forall a. Array# a -> Int#
sizeofArray# Array# a
arr
    in case Put -> Addr# -> RW -> (# Addr#, RW #)
unPut (Int -> Put
forall a. Serialize a => a -> Put
put (Int# -> Int
I# Int#
sz)) Addr#
p RW
s of
      (# Addr#
p, RW
s #) -> Addr# -> RW -> Int# -> Int# -> Array# a -> (# Addr#, RW #)
go Addr#
p RW
s Int#
0# Int#
sz Array# a
arr

  get :: Get (Array a)
get = do
    I# l <- forall a. Serialize a => Get a
get @Int
    Get \Addr#
e Addr#
p RW
s ->
      let go :: Addr# -> Addr# -> State# RealWorld -> MutableArray# RealWorld a
                -> Int# -> Int# -> (# Addr#, State# RealWorld #)
          go :: Addr#
-> Addr#
-> RW
-> MutableArray# RealWorld a
-> Int#
-> Int#
-> (# Addr#, RW #)
go Addr#
e Addr#
p RW
s MutableArray# RealWorld a
marr Int#
i Int#
l = case Int#
i Int# -> Int# -> Int#
==# Int#
l of
            Int#
1# -> (# Addr#
p, RW
s #)
            Int#
_  -> case Get a -> Addr# -> Addr# -> RW -> (# Addr#, RW, a #)
forall a. Get a -> Addr# -> Addr# -> RW -> (# Addr#, RW, a #)
unGet (forall a. Serialize a => Get a
get @a) Addr#
e Addr#
p RW
s of
              (# Addr#
p, RW
s, a
a #) -> case MutableArray# RealWorld a -> Int# -> a -> RW -> RW
forall d a. MutableArray# d a -> Int# -> a -> State# d -> State# d
writeArray# MutableArray# RealWorld a
marr Int#
i a
a RW
s of
                RW
s -> Addr#
-> Addr#
-> RW
-> MutableArray# RealWorld a
-> Int#
-> Int#
-> (# Addr#, RW #)
go Addr#
e Addr#
p RW
s MutableArray# RealWorld a
marr (Int#
i Int# -> Int# -> Int#
+# Int#
1#) Int#
l
      in case Int# -> a -> RW -> (# RW, MutableArray# RealWorld a #)
forall a d.
Int# -> a -> State# d -> (# State# d, MutableArray# d a #)
newArray# Int#
l a
forall a. HasCallStack => a
undefined RW
s of
        (# RW
s, MutableArray# RealWorld a
marr #) -> case Addr#
-> Addr#
-> RW
-> MutableArray# RealWorld a
-> Int#
-> Int#
-> (# Addr#, RW #)
go Addr#
e Addr#
p RW
s MutableArray# RealWorld a
marr Int#
0# Int#
l of
          (# Addr#
p, RW
s #) -> case MutableArray# RealWorld a -> RW -> (# RW, Array# a #)
forall d a.
MutableArray# d a -> State# d -> (# State# d, Array# a #)
unsafeFreezeArray# MutableArray# RealWorld a
marr RW
s of
            (# RW
s, Array# a
arr #) -> (# Addr#
p, RW
s, Array a -> Array a
forall a. Array a -> Array a
Array (Array# a -> Array a
forall a. Array# a -> Array a
A.Array Array# a
arr) #)

-- | Strict traversal.
{-# INLINE traverseIO' #-}
traverseIO' :: (a -> IO b) -> Array a -> IO (Array b)
traverseIO' :: forall a b. (a -> IO b) -> Array a -> IO (Array b)
traverseIO' a -> IO b
f (Array Array a
arr) = do
  !arr <- (a -> IO b) -> Array a -> IO (Array b)
forall (m :: * -> *) a b.
PrimMonad m =>
(a -> m b) -> Array a -> m (Array b)
A.traverseArrayP a -> IO b
f Array a
arr
  pure (Array arr)