From 5494d8185bb85e80c7c694e0bfc6d7373bf34a87 Mon Sep 17 00:00:00 2001 From: dopamane Date: Sat, 10 Aug 2024 16:53:55 +0200 Subject: [PATCH 1/3] Add `queue` --- bayeux.cabal | 1 + lib/Bayeux/Queue.hs | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 34 insertions(+) create mode 100644 lib/Bayeux/Queue.hs diff --git a/bayeux.cabal b/bayeux.cabal index b924060..7e3a5c6 100644 --- a/bayeux.cabal +++ b/bayeux.cabal @@ -30,6 +30,7 @@ library , Bayeux.Ice40.Spi , Bayeux.Ice40.Spram , Bayeux.Lp + , Bayeux.Queue , Bayeux.Rtl , Bayeux.Signal , Bayeux.Tableaux diff --git a/lib/Bayeux/Queue.hs b/lib/Bayeux/Queue.hs new file mode 100644 index 0000000..daababf --- /dev/null +++ b/lib/Bayeux/Queue.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Bayeux.Queue + ( MonadQueue(..) + ) where + +import Bayeux.Rtl +import Bayeux.Signal +import GHC.TypeNats + +class MonadQueue m where + queue :: Natural -- ^ length + -> Sig (Maybe a) + -> m (Sig (Maybe a)) + +instance MonadQueue Rtl where + queue n = withNat n queue' + + +withNat :: forall r. Natural -> (forall n. KnownNat n => SNat n -> r) -> r +withNat n f = withSomeSNat n go + where + go :: forall m. SNat m -> r + go sm = withKnownNat sm $ f sm + +queue' + :: forall n a + . KnownNat n + => SNat n + -> Sig (Maybe a) + -> Rtl (Sig (Maybe a)) +queue' _ = undefined From f9b9130c83415bd603333d994c6a811f48869d32 Mon Sep 17 00:00:00 2001 From: dopamane Date: Sat, 10 Aug 2024 18:22:24 +0200 Subject: [PATCH 2/3] Sketch --- lib/Bayeux/Queue.hs | 59 +++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 54 insertions(+), 5 deletions(-) diff --git a/lib/Bayeux/Queue.hs b/lib/Bayeux/Queue.hs index daababf..9854c1d 100644 --- a/lib/Bayeux/Queue.hs +++ b/lib/Bayeux/Queue.hs @@ -5,17 +5,23 @@ module Bayeux.Queue ( MonadQueue(..) ) where -import Bayeux.Rtl +import Bayeux.Encode +import Bayeux.Rtl (Rtl) import Bayeux.Signal +import Bayeux.Width +import Data.Array +import Data.Finite import GHC.TypeNats class MonadQueue m where - queue :: Natural -- ^ length - -> Sig (Maybe a) + queue :: Width a + => Natural -- ^ size + -> Sig (Maybe a) -- ^ enqueue + -> Sig Bool -- ^ dequeue -> m (Sig (Maybe a)) instance MonadQueue Rtl where - queue n = withNat n queue' + queue sz = withNat sz queue' withNat :: forall r. Natural -> (forall n. KnownNat n => SNat n -> r) -> r @@ -24,10 +30,53 @@ withNat n f = withSomeSNat n go go :: forall m. SNat m -> r go sm = withKnownNat sm $ f sm +data Queue n a = Queue + { rPtr :: Finite n + , rWrap :: Bool + , wPtr :: Finite n + , wWrap :: Bool + , dArray :: Array (Finite n) a + } + deriving (Eq, Read, Show) + +instance (KnownNat n, Width a) => Width (Queue n a) where + width _ = 2 + sum + [ 2 * width (undefined :: Finite n) + , width (undefined :: Array (Finite n) a) + ] + +instance (KnownNat n, Encode a) => Encode (Queue n a) where + encode q = mconcat + [ encode $ rPtr q + , encode $ rWrap q + , encode $ wPtr q + , encode $ wWrap q + , encode $ dArray q + ] + +sliceRPtr :: Sig (Queue n a) -> Sig (Finite n) +sliceRPtr = undefined + +sliceRWrap :: Sig (Queue n a) -> Sig Bool +sliceRWrap = undefined + +sliceWPtr :: Sig (Queue n a) -> Sig (Finite n) +sliceWPtr = undefined + +sliceWWrap :: Sig (Queue n a) -> Sig Bool +sliceWWrap = undefined + +sliceDArray :: Sig (Queue n a) -> Sig (Array (Finite n) a) +sliceDArray = undefined + queue' :: forall n a . KnownNat n + => Width a => SNat n -> Sig (Maybe a) + -> Sig Bool -> Rtl (Sig (Maybe a)) -queue' _ = undefined +queue' _ enqM deq = do + s <- process $ \(s :: Sig (Queue n a)) -> undefined + return $ Sig undefined From b35b65782d791b8d61326cb27978b97e14a44dc3 Mon Sep 17 00:00:00 2001 From: dopamane Date: Tue, 13 Aug 2024 09:58:12 +0200 Subject: [PATCH 3/3] Slicing... --- lib/Bayeux/Queue.hs | 29 +++++++++++++++++++++-------- 1 file changed, 21 insertions(+), 8 deletions(-) diff --git a/lib/Bayeux/Queue.hs b/lib/Bayeux/Queue.hs index 9854c1d..6598b1f 100644 --- a/lib/Bayeux/Queue.hs +++ b/lib/Bayeux/Queue.hs @@ -11,6 +11,7 @@ import Bayeux.Signal import Bayeux.Width import Data.Array import Data.Finite +import Data.Proxy import GHC.TypeNats class MonadQueue m where @@ -55,19 +56,31 @@ instance (KnownNat n, Encode a) => Encode (Queue n a) where ] sliceRPtr :: Sig (Queue n a) -> Sig (Finite n) -sliceRPtr = undefined +sliceRPtr = slice (width (undefined :: Finite n) + base - 1) base + where + base = width (undefined :: Finite n) - 1 + dArrayWidth + 3 sliceRWrap :: Sig (Queue n a) -> Sig Bool -sliceRWrap = undefined +sliceRWrap = slice + (width (undefined :: Finite n) - 1 + dArrayWidth + 2) + (width (undefined :: Finite n) - 1 + dArrayWidth + 2) + +rWrapBase :: forall n. KnownNat n => Proxy n -> Integer +rWrapBase _ = width (undefined :: Finite n) - 1 + dArrayWidth (Proxy :: Proxy n) + 2 + +sliceWPtr :: forall n a. KnownNat n => Sig (Queue n a) -> Sig (Finite n) +sliceWPtr = slice + (width (undefined :: Finite n) - 1 + dArrayWidth (Proxy :: Proxy n) + 1) + (dArrayWidth (Proxy :: Proxy n) + 1) -sliceWPtr :: Sig (Queue n a) -> Sig (Finite n) -sliceWPtr = undefined +sliceWWrap :: forall n a. KnownNat n => Sig (Queue n a) -> Sig Bool +sliceWWrap = slice (dArrayWidth (Proxy :: Proxy n)) (dArrayWidth (Proxy :: Proxy n)) -sliceWWrap :: Sig (Queue n a) -> Sig Bool -sliceWWrap = undefined +sliceDArray :: forall n a. KnownNat n => Sig (Queue n a) -> Sig (Array (Finite n) a) +sliceDArray = slice (dArrayWidth (Proxy :: Proxy n) - 1) 0 -sliceDArray :: Sig (Queue n a) -> Sig (Array (Finite n) a) -sliceDArray = undefined +dArrayWidth :: forall n. KnownNat n => Proxy n -> Integer +dArrayWidth _ = width (undefined :: Array (Finite n) a) queue' :: forall n a