From 45436e8453d2a93f66c5b0bc444eb5548f86ccfc Mon Sep 17 00:00:00 2001 From: Martijn Bastiaan Date: Tue, 5 Jan 2021 15:16:34 +0100 Subject: [PATCH] Drop injectivity requirement of Bwd --- src/Protocols/Df.hs | 21 +++++------------ src/Protocols/DfLike.hs | 3 ++- src/Protocols/Internal.hs | 47 ++++++++++++++++++--------------------- 3 files changed, 30 insertions(+), 41 deletions(-) diff --git a/src/Protocols/Df.hs b/src/Protocols/Df.hs index 26f18707..a8ab8412 100644 --- a/src/Protocols/Df.hs +++ b/src/Protocols/Df.hs @@ -16,7 +16,7 @@ carries data, no metadata. For documentation see: module Protocols.Df ( -- * Types - Df, Data(..), Ack(..) + Df, Data(..) -- * Operations on Df like protocols , const, void, pure @@ -65,7 +65,6 @@ import Prelude hiding import Data.Bifunctor (Bifunctor) import Data.Coerce (coerce) -import Data.Default (Default) import Data.Kind (Type) import qualified Data.Maybe as Maybe import Data.Proxy @@ -77,7 +76,7 @@ import Clash.Signal.Internal (Signal) import qualified Clash.Prelude as C -- me -import Protocols.Internal hiding (Ack(..)) +import Protocols.Internal import Protocols.DfLike (DfLike) import qualified Protocols.DfLike as DfLike @@ -98,11 +97,11 @@ instance Protocol (Df dom a) where -- | Forward part of simple dataflow: @Signal dom (Data meta a)@ type Fwd (Df dom a) = Signal dom (Data a) - -- | Backward part of simple dataflow: @Signal dom (Ack meta a)@ - type Bwd (Df dom a) = Signal dom (Ack a) + -- | Backward part of simple dataflow: @Signal dom Bool@ + type Bwd (Df dom a) = Signal dom Ack instance Backpressure (Df dom a) where - boolsToBwd = C.fromList_lazy . coerce + boolsToBwd _ = C.fromList_lazy . coerce -- | Data sent over forward channel of 'Df'. Note that this data type is strict -- on its data field. @@ -135,14 +134,6 @@ dataToMaybe :: Data a -> Maybe a dataToMaybe NoData = Nothing dataToMaybe (Data a) = Just a --- | Like 'Protocols.Df.Ack', but carrying phantom type variables to satisfy --- 'Bwd's injectivity requirement. -newtype Ack a = Ack Bool - deriving (Show) - -instance Default (Ack a) where - def = Ack True - instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Simulate (Df dom a) where type SimulateType (Df dom a) = [Data a] type ExpectType (Df dom a) = [a] @@ -158,7 +149,7 @@ instance (C.KnownDomain dom, C.NFDataX a, C.ShowX a, Show a) => Simulate (Df dom instance DfLike dom (Df dom) a where type Data (Df dom) a = Data a type Payload a = a - type Ack (Df dom) a = Ack a + type Ack (Df dom) a = Ack getPayload _ (Data a) = Just a getPayload _ NoData = Nothing diff --git a/src/Protocols/DfLike.hs b/src/Protocols/DfLike.hs index f6e7cc59..844ce715 100644 --- a/src/Protocols/DfLike.hs +++ b/src/Protocols/DfLike.hs @@ -96,7 +96,7 @@ class ( Protocol (df a) type Payload a = (r :: Type) | r -> a -- | Acknowledgement data carried on backward channel - type Ack df a = (r :: Type) | r -> a + type Ack df a noData :: Proxy (df a) -> @@ -108,6 +108,7 @@ class ( Protocol (df a) Maybe (Payload a) setPayload :: + HasCallStack => DfLike dom df b => Proxy (df a) -> Proxy (df b) -> diff --git a/src/Protocols/Internal.hs b/src/Protocols/Internal.hs index 066482eb..03023854 100644 --- a/src/Protocols/Internal.hs +++ b/src/Protocols/Internal.hs @@ -98,19 +98,16 @@ import GHC.Generics (Generic) -- data. Similar to /Bool/ we define: -- -- @ --- data Ack a = DfNack | Ack +-- newtype Ack = Ack Bool -- @ -- --- (For technical reasons[1] we need the type variable /a/ in this definition, --- even though we don't use it on the right hand side.) --- -- With these three definitions we're ready to make an instance for /Fwd/ and -- /Bwd/: -- -- @ -- instance Protocol (Df dom a) where -- type Fwd (Df dom a) = Signal dom (Data a) --- type Bwd (Df dom a) = Signal dom (Ack a) +-- type Bwd (Df dom a) = Signal dom Ack -- @ -- -- Having defined all this, we can take a look at /Circuit/ once more: now @@ -128,7 +125,7 @@ import GHC.Generics (Generic) -- +------------------------>+ +-------------------------> -- | | -- | | --- Signal dom (Ack a) | | Signal dom (Ack b) +-- Signal dom Ack | | Signal dom Ack -- <-------------------------+ +<------------------------+ -- | | -- +-----------+ @@ -141,15 +138,6 @@ import GHC.Generics (Generic) -- -- 2. It eliminates the need for manually routing acknowledgement lines -- --- Footnotes: --- --- 1. Fwd and Bwd are injective type families. I.e., something on --- the right hand side of a type instance must uniquely identify the left --- hand side and vice versa. This helps type inference and error messages --- substantially, in exchange for a slight syntactical artifact. As a --- result, any type variables on the left hand side must occur on the right --- hand side too. --- newtype Circuit a b = Circuit ( (Fwd a, Bwd b) -> (Bwd a, Fwd b) ) @@ -157,11 +145,17 @@ newtype Circuit a b = newtype Ack = Ack Bool deriving (Generic, C.NFDataX) +-- | Acknowledge. Used in circuit-notation plugin to drive ignore components. +instance Default Ack where + def = Ack True + -- | Circuit protocol with /CSignal dom a/ in its forward direction, and -- /CSignal dom ()/ in its backward direction. Convenient for exposing -- protocol internals. data CSignal dom a = CSignal (Signal dom a) +instance Default a => Default (CSignal dom a) where + def = CSignal def -- | A protocol describes the in- and outputs of one side of a 'Circuit'. class Protocol a where @@ -171,7 +165,7 @@ class Protocol a where -- | Receiver to sender type family. See 'Circuit' for an explanation on the -- existence of 'Bwd'. - type Bwd (a :: Type) = (r :: Type) | r -> a + type Bwd (a :: Type) instance Protocol () where type Fwd () = () @@ -196,7 +190,7 @@ instance C.KnownNat n => Protocol (C.Vec n a) where -- XXX: Type families with Signals on LHS are currently broken on Clash: instance Protocol (CSignal dom a) where type Fwd (CSignal dom a) = CSignal dom a - type Bwd (CSignal dom a) = CSignal dom (Const () a) + type Bwd (CSignal dom a) = CSignal dom () -- | Left-to-right circuit composition. -- @@ -231,22 +225,25 @@ infixr 1 |> class Protocol a => Backpressure a where -- | Interpret list of booleans as a list of acknowledgements at every cycle. -- Implementations don't have to account for finite lists. - boolsToBwd :: [Bool] -> Bwd a + boolsToBwd :: Proxy a -> [Bool] -> Bwd a instance Backpressure () where - boolsToBwd _ = () + boolsToBwd _ _ = () instance (Backpressure a, Backpressure b) => Backpressure (a, b) where - boolsToBwd bs = (boolsToBwd bs, boolsToBwd bs) + boolsToBwd _ bs = (boolsToBwd (Proxy @a) bs, boolsToBwd (Proxy @b) bs) instance (Backpressure a, Backpressure b, Backpressure c) => Backpressure (a, b, c) where - boolsToBwd bs = (boolsToBwd bs, boolsToBwd bs, boolsToBwd bs) + boolsToBwd _ bs = + ( boolsToBwd (Proxy @a) bs + , boolsToBwd (Proxy @b) bs + , boolsToBwd (Proxy @c) bs ) instance (C.KnownNat n, Backpressure a) => Backpressure (C.Vec n a) where - boolsToBwd bs = C.repeat (boolsToBwd bs) + boolsToBwd _ bs = C.repeat (boolsToBwd (Proxy @a) bs) instance Backpressure (CSignal dom a) where - boolsToBwd _ = CSignal (pure (Const ())) + boolsToBwd _ _ = CSignal (pure ()) -- | Right-to-left circuit composition. -- @@ -480,7 +477,7 @@ instance (Simulate a, Simulate b) => Simulate (a, b) where sampleC conf (Circuit f) = let bools = replicate (resetCycles conf) False <> repeat True - (_, (fwd1, fwd2)) = f ((), (boolsToBwd bools, boolsToBwd bools)) + (_, (fwd1, fwd2)) = f ((), (boolsToBwd (Proxy @a) bools, boolsToBwd (Proxy @b) bools)) in ( sampleC conf (Circuit $ \_ -> ((), fwd1)) , sampleC conf (Circuit $ \_ -> ((), fwd2)) ) @@ -517,7 +514,7 @@ instance (C.KnownNat n, Simulate a) => Simulate (C.Vec n a) where sampleC conf (Circuit f) = let bools = replicate (resetCycles conf) False <> repeat True - (_, fwds) = f ((), (C.repeat (boolsToBwd bools))) + (_, fwds) = f ((), (C.repeat (boolsToBwd (Proxy @a) bools))) in C.map (\fwd -> sampleC conf (Circuit $ \_ -> ((), fwd))) fwds