module Data.Microgroove.MRec
(MRec(MRec#,MRNil,MRCons)
,new#
,rmap, crmap
,toMVector, ctoMVector
,modify, setAt
,module X
) where
import Data.Microgroove.TypeLevel as X
import Data.Microgroove.Lib
import Data.Vector.Mutable (MVector)
import qualified Data.Vector.Mutable as VM
import GHC.Exts (Any,Constraint)
import Control.Monad.Primitive (PrimMonad(..))
import GHC.TypeLits
import Data.Proxy
newtype MRec s (f :: u -> *) (us :: [u]) = MRec# (MVector s Any)
data MRec' s (f :: u -> *) (us :: [u]) where
MRNil' :: MRec' s f '[]
MRCons' :: MVector s (f u) -> MRec s f us -> MRec' s f (u ': us)
upMRec :: MRec s f us -> MRec' s f us
upMRec (MRec# v) | VM.null v = cast# MRNil'
| otherwise = cast# $ MRCons' (cast# $ VM.take 1 v) (MRec# $ VM.tail v)
pattern MRNil :: () => (us ~ '[]) => MRec s f us
pattern MRNil <- (upMRec -> MRNil')
pattern MRCons :: () => (us' ~ (u ': us)) => VM.MVector s (f u) -> MRec s f us -> MRec s f us'
pattern MRCons x xs <- (upMRec -> MRCons' x xs)
rmap :: forall g m f xs. PrimMonad m => (forall x. f x -> g x) -> MRec (PrimState m) f xs -> m (MRec (PrimState m) g xs)
rmap f xs = cast# xs <$ go xs where
go :: MRec (PrimState m) f as -> m ()
go = \case
MRNil -> pure ()
MRCons x xs' -> VM.modify x (castf# @f . f) 0 >> go xs'
_ -> error "impossible! MRNil and MRCons were inexhaustive in rmap"
crmap :: forall (c :: * -> Constraint) g m f xs. (AllF c f xs, PrimMonad m)
=> (forall x. c (f x) => f x -> g x) -> MRec (PrimState m) f xs -> m (MRec (PrimState m) g xs)
crmap f xs = cast# xs <$ go xs where
go :: forall as. (AllF c f as) => MRec (PrimState m) f as -> m ()
go = \case
MRNil -> pure ()
MRCons x xs' -> VM.modify x (castf# @f . f) 0 >> go xs'
_ -> error "impossible! MRNil and MRCons were inexhaustive in crmap"
toMVector :: forall r m f xs. PrimMonad m
=> (forall x. f x -> r) -> MRec (PrimState m) f xs -> m (MVector (PrimState m) r)
toMVector f xs = cast# xs <$ go xs where
go :: MRec (PrimState m) f as -> m ()
go = \case
MRNil -> pure ()
MRCons x xs' -> VM.modify x (cast# . f) 0 >> go xs'
_ -> error "impossible! MRNil and MRCons were inexhaustive in toMVector"
ctoMVector :: forall (c :: * -> Constraint) r m f xs. (AllF c f xs, PrimMonad m)
=> (forall x. c (f x) => f x -> r) -> MRec (PrimState m) f xs -> m (MVector (PrimState m) r)
ctoMVector f xs = cast# xs <$ go xs where
go :: forall as. (AllF c f as) => MRec (PrimState m) f as -> m ()
go = \case
MRNil -> pure ()
MRCons x xs' -> VM.modify x (cast# . f) 0 >> go xs'
_ -> error "impossible! MRNil and MRCons were inexhaustive in ctoMVector"
new# :: forall f xs m. (KnownNat (Length xs), PrimMonad m) => m (MRec (PrimState m) f xs)
new# = MRec# <$> VM.unsafeNew (fromInteger (natVal (Proxy @(Length xs))))
modify :: forall n xs fx f m. (fx ~ f (xs !! n), PrimMonad m, KnownNat n)
=> (fx -> fx) -> MRec (PrimState m) f xs -> m ()
modify f (MRec# vm) = VM.modify vm (overcast# @fx f) (fromInteger (natVal (Proxy @n)))
setAt :: forall n x xs f m. (PrimMonad m, KnownNat n)
=> f x -> MRec (PrimState m) f xs -> m (MRec (PrimState m) f (SetAt n xs x))
setAt x rm@(MRec# vm) = cast# rm <$ VM.modify vm (cast# @Any . (\_ -> x)) (fromInteger (natVal (Proxy @n)))