Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Tuple kinds, categories and arrows #65

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion clash-protocols.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -211,7 +211,7 @@ test-suite unittests
Tests.Protocols.DfConv
Tests.Protocols.Avalon
Tests.Protocols.Axi4
Tests.Protocols.Plugin
-- Tests.Protocols.Plugin
Tests.Protocols.Wishbone

Util
Expand Down
8 changes: 7 additions & 1 deletion src/Protocols.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,15 @@ definitions in @circuit-notation@ at <https://github.com/cchalmers/circuit-notat
module Protocols
( -- * Circuit definition
Circuit(Circuit)
, Protocol(Fwd, Bwd)
, Fwd
, Bwd
, Backpressure(boolsToBwd)
, Ack(..)
, NC
, I2
, I3
, IVec
, type (><)

-- * Combinators & functions
, (|>), (<|)
Expand Down
24 changes: 8 additions & 16 deletions src/Protocols/Avalon/MemMap.hs
Original file line number Diff line number Diff line change
Expand Up @@ -85,8 +85,8 @@ module Protocols.Avalon.MemMap
, subordinateInRemoveNonDf

-- * Protocols
, AvalonMmManager(..)
, AvalonMmSubordinate(..)
, AvalonMmManager
, AvalonMmSubordinate
) where

-- base
Expand Down Expand Up @@ -1001,25 +1001,17 @@ mmManagerInToBool ::
mmManagerInToBool = not . mi_waitRequest

-- | Datatype for the manager end of the Avalon memory-mapped protocol.
data AvalonMmManager (dom :: Domain) (config :: AvalonMmManagerConfig)
= AvalonMmManager
type AvalonMmManager (dom :: Domain) (config :: AvalonMmManagerConfig)
= (Signal dom (AvalonManagerOut config))
>< (Signal dom (AvalonManagerIn config))

-- | Datatype for the subordinate end of the Avalon memory-mapped protocol.
data AvalonMmSubordinate
type AvalonMmSubordinate
(dom :: Domain)
(fixedWaitTime :: Nat)
(config :: AvalonMmSubordinateConfig)
= AvalonMmSubordinate

instance Protocol (AvalonMmManager dom config) where
type Fwd (AvalonMmManager dom config) = Signal dom (AvalonManagerOut config)
type Bwd (AvalonMmManager dom config) = Signal dom (AvalonManagerIn config)

instance Protocol (AvalonMmSubordinate dom fixedWaitTime config) where
type Fwd (AvalonMmSubordinate dom fixedWaitTime config)
= Signal dom (AvalonSubordinateIn config)
type Bwd (AvalonMmSubordinate dom fixedWaitTime config)
= Signal dom (AvalonSubordinateOut config)
= (Signal dom (AvalonSubordinateIn config))
>< (Signal dom (AvalonSubordinateOut config))

instance (KnownSubordinateConfig config, KeepWaitRequest config ~ 'True) =>
Backpressure (AvalonMmSubordinate dom 0 config) where
Expand Down
43 changes: 25 additions & 18 deletions src/Protocols/Avalon/Stream.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
Expand Down Expand Up @@ -136,25 +137,31 @@
deriving (Generic, C.NFDataX, C.ShowX, Eq, NFData, Show, Bundle)

-- | Type for Avalon Stream protocol.
data AvalonStream (dom :: Domain) (conf :: AvalonStreamConfig) (dataType :: Type)
type AvalonStream (dom :: Domain) (conf :: AvalonStreamConfig) (dataType :: Type)
= AvalonStream# dom conf dataType (ReadyLatency conf)

instance Protocol (AvalonStream dom conf dataType) where
type Fwd (AvalonStream dom conf dataType)
= Signal dom (Maybe (AvalonStreamM2S conf dataType))
type Bwd (AvalonStream dom conf dataType)
= Signal dom (AvalonStreamS2M (ReadyLatency conf))
type AvalonStream#
(dom :: Domain)
(conf :: AvalonStreamConfig)
(dataType :: Type)
(n :: Nat)
= (Signal dom (Maybe (AvalonStreamM2S conf dataType)))
>< (Signal dom (AvalonStreamS2M n))

instance (ReadyLatency conf ~ 0) =>
Backpressure (AvalonStream dom conf dataType) where
Backpressure (AvalonStream# dom conf dataType 0) where
boolsToBwd _ = C.fromList_lazy . fmap AvalonStreamS2M

instance (KnownAvalonStreamConfig conf, NFDataX dataType) =>
DfConv.DfConv (AvalonStream dom conf dataType) where
type Dom (AvalonStream dom conf dataType) = dom
type FwdPayload (AvalonStream dom conf dataType)
instance
( ReadyLatency conf ~ n
, KnownAvalonStreamConfig conf
, NFDataX dataType ) =>
DfConv.DfConv (AvalonStream# dom conf dataType n) where
type Dom (AvalonStream# dom conf dataType n) = dom
type FwdPayload (AvalonStream# dom conf dataType n)
= AvalonStreamM2S conf dataType

toDfCircuit proxy = DfConv.toDfCircuitHelper proxy s0 blankOtp stateFn where

Check failure on line 164 in src/Protocols/Avalon/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.0.2 / clash 1.6.1

• Could not deduce: (n + 1) ~ (1 + n)

Check failure on line 164 in src/Protocols/Avalon/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 8.10.7 / clash 1.6.1

• Could not deduce: (n + 1) ~ (1 + n)

Check failure on line 164 in src/Protocols/Avalon/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 8.10.7 / clash 1.8.1

• Could not deduce: (n + 1) ~ (1 + n)

Check failure on line 164 in src/Protocols/Avalon/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.0.2 / clash 1.8.1

• Could not deduce: (n + 1) ~ (1 + n)

Check failure on line 164 in src/Protocols/Avalon/Stream.hs

View workflow job for this annotation

GitHub Actions / Stack tests

• Could not deduce: (n + 1) ~ (1 + n)
s0 = C.repeat @((ReadyLatency conf)+1) False
blankOtp = Nothing
stateFn (AvalonStreamS2M thisAck) _ otpItem = do
Expand All @@ -181,11 +188,11 @@
, KnownAvalonStreamConfig conf
, NFDataX dataType
, KnownDomain dom ) =>
Simulate (AvalonStream dom conf dataType) where
type SimulateFwdType (AvalonStream dom conf dataType)
Simulate (AvalonStream# dom conf dataType 0) where
type SimulateFwdType (AvalonStream# dom conf dataType 0)
= [Maybe (AvalonStreamM2S conf dataType)]
type SimulateBwdType (AvalonStream dom conf dataType) = [AvalonStreamS2M 0]
type SimulateChannels (AvalonStream dom conf dataType) = 1
type SimulateBwdType (AvalonStream# dom conf dataType 0) = [AvalonStreamS2M 0]
type SimulateChannels (AvalonStream# dom conf dataType 0) = 1

simToSigFwd _ = fromList_lazy
simToSigBwd _ = fromList_lazy
Expand All @@ -201,8 +208,8 @@
, KnownAvalonStreamConfig conf
, NFDataX dataType
, KnownDomain dom ) =>
Drivable (AvalonStream dom conf dataType) where
type ExpectType (AvalonStream dom conf dataType)
Drivable (AvalonStream# dom conf dataType 0) where
type ExpectType (AvalonStream# dom conf dataType 0)
= [AvalonStreamM2S conf dataType]

toSimulateType Proxy = P.map Just
Expand All @@ -225,7 +232,7 @@
, Show dataType
, Eq dataType
, KnownDomain dom ) =>
Test (AvalonStream dom conf dataType) where
Test (AvalonStream# dom conf dataType 0) where

expectToLengths Proxy = pure . P.length
expectN Proxy options nExpected sampled
Expand Down
10 changes: 3 additions & 7 deletions src/Protocols/Axi4/ReadAddress.hs
Original file line number Diff line number Diff line change
Expand Up @@ -124,16 +124,12 @@
ARKeepQos ('Axi4ReadAddressConfig _ _ _ _ _ _ _ _ _ a) = a

-- | AXI4 Read Address channel protocol
data Axi4ReadAddress
type Axi4ReadAddress
(dom :: C.Domain)
(conf :: Axi4ReadAddressConfig)
(userType :: Type)

instance Protocol (Axi4ReadAddress dom conf userType) where
type Fwd (Axi4ReadAddress dom conf userType) =
C.Signal dom (M2S_ReadAddress conf userType)
type Bwd (Axi4ReadAddress dom conf userType) =
C.Signal dom S2M_ReadAddress
= C.Signal dom (M2S_ReadAddress conf userType)
>< C.Signal dom S2M_ReadAddress

instance Backpressure (Axi4ReadAddress dom conf userType) where
boolsToBwd _ = C.fromList_lazy . coerce
Expand Down Expand Up @@ -183,7 +179,7 @@
-- | See Table A2-5 "Read address channel signals"
newtype S2M_ReadAddress = S2M_ReadAddress
{ _arready :: Bool }
deriving (Show, Generic, C.NFDataX)

Check warning on line 182 in src/Protocols/Axi4/ReadAddress.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.6.4 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 182 in src/Protocols/Axi4/ReadAddress.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.2.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 182 in src/Protocols/Axi4/ReadAddress.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.4.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

-- | Shorthand for a "well-behaved" read address config,
-- so that we don't need to write out a bunch of type constraints later.
Expand Down
10 changes: 3 additions & 7 deletions src/Protocols/Axi4/ReadData.hs
Original file line number Diff line number Diff line change
Expand Up @@ -55,17 +55,13 @@
RIdWidth ('Axi4ReadDataConfig _ a) = a

-- | AXI4 Read Data channel protocol
data Axi4ReadData
type Axi4ReadData
(dom :: C.Domain)
(conf :: Axi4ReadDataConfig)
(userType :: Type)
(dataType :: Type)

instance Protocol (Axi4ReadData dom conf userType dataType) where
type Fwd (Axi4ReadData dom conf userType dataType) =
C.Signal dom (S2M_ReadData conf userType dataType)
type Bwd (Axi4ReadData dom conf userType dataType) =
C.Signal dom M2S_ReadData
= C.Signal dom (S2M_ReadData conf userType dataType)
>< C.Signal dom M2S_ReadData

instance Backpressure (Axi4ReadData dom conf userType dataType) where
boolsToBwd _ = C.fromList_lazy . coerce
Expand Down Expand Up @@ -96,7 +92,7 @@

-- | See Table A2-6 "Read data channel signals"
newtype M2S_ReadData = M2S_ReadData { _rready :: Bool }
deriving (Show, Generic, C.NFDataX)

Check warning on line 95 in src/Protocols/Axi4/ReadData.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.6.4 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 95 in src/Protocols/Axi4/ReadData.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.2.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 95 in src/Protocols/Axi4/ReadData.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.4.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

-- | Shorthand for a "well-behaved" read data config,
-- so that we don't need to write out a bunch of type constraints later.
Expand Down
8 changes: 3 additions & 5 deletions src/Protocols/Axi4/Stream.hs
Original file line number Diff line number Diff line change
Expand Up @@ -98,14 +98,12 @@
-- Manager may not decide whether or not to send 'Nothing' based on
-- the '_tready' signal.
newtype Axi4StreamS2M = Axi4StreamS2M { _tready :: Bool }
deriving (Generic, C.NFDataX, C.ShowX, Eq, NFData, Show, Bundle)

Check warning on line 101 in src/Protocols/Axi4/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.6.4 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 101 in src/Protocols/Axi4/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.6.4 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 101 in src/Protocols/Axi4/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.6.4 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 101 in src/Protocols/Axi4/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.2.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 101 in src/Protocols/Axi4/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.2.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 101 in src/Protocols/Axi4/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.2.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 101 in src/Protocols/Axi4/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.4.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 101 in src/Protocols/Axi4/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.4.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 101 in src/Protocols/Axi4/Stream.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.4.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

-- | Type for AXI4 Stream protocol.
data Axi4Stream (dom :: Domain) (conf :: Axi4StreamConfig) (userType :: Type)

instance Protocol (Axi4Stream dom conf userType) where
type Fwd (Axi4Stream dom conf userType) = Signal dom (Maybe (Axi4StreamM2S conf userType))
type Bwd (Axi4Stream dom conf userType) = Signal dom Axi4StreamS2M
type Axi4Stream (dom :: Domain) (conf :: Axi4StreamConfig) (userType :: Type)
= Signal dom (Maybe (Axi4StreamM2S conf userType))
>< Signal dom Axi4StreamS2M

instance Backpressure (Axi4Stream dom conf userType) where
boolsToBwd _ = C.fromList_lazy . fmap Axi4StreamS2M
Expand Down
10 changes: 3 additions & 7 deletions src/Protocols/Axi4/WriteAddress.hs
Original file line number Diff line number Diff line change
Expand Up @@ -124,16 +124,12 @@
AWKeepQos ('Axi4WriteAddressConfig _ _ _ _ _ _ _ _ _ a) = a

-- | AXI4 Write Address channel protocol
data Axi4WriteAddress
type Axi4WriteAddress
(dom :: C.Domain)
(conf :: Axi4WriteAddressConfig)
(userType :: Type)

instance Protocol (Axi4WriteAddress dom conf userType) where
type Fwd (Axi4WriteAddress dom conf userType) =
C.Signal dom (M2S_WriteAddress conf userType)
type Bwd (Axi4WriteAddress dom conf userType) =
C.Signal dom S2M_WriteAddress
= C.Signal dom (M2S_WriteAddress conf userType)
>< C.Signal dom S2M_WriteAddress

instance Backpressure (Axi4WriteAddress dom conf userType) where
boolsToBwd _ = C.fromList_lazy . coerce
Expand Down Expand Up @@ -182,7 +178,7 @@

-- | See Table A2-2 "Write address channel signals"
newtype S2M_WriteAddress = S2M_WriteAddress { _awready :: Bool }
deriving (Show, Generic, C.NFDataX)

Check warning on line 181 in src/Protocols/Axi4/WriteAddress.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.6.4 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 181 in src/Protocols/Axi4/WriteAddress.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.2.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 181 in src/Protocols/Axi4/WriteAddress.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.4.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

-- | Shorthand for a "well-behaved" write address config,
-- so that we don't need to write out a bunch of type constraints later.
Expand Down
10 changes: 3 additions & 7 deletions src/Protocols/Axi4/WriteData.hs
Original file line number Diff line number Diff line change
Expand Up @@ -55,16 +55,12 @@
WNBytes ('Axi4WriteDataConfig _ a) = a

-- | AXI4 Write Data channel protocol
data Axi4WriteData
type Axi4WriteData
(dom :: C.Domain)
(conf :: Axi4WriteDataConfig)
(userType :: Type)

instance Protocol (Axi4WriteData dom conf userType) where
type Fwd (Axi4WriteData dom conf userType) =
C.Signal dom (M2S_WriteData conf userType)
type Bwd (Axi4WriteData dom conf userType) =
C.Signal dom S2M_WriteData
= C.Signal dom (M2S_WriteData conf userType)
>< C.Signal dom S2M_WriteData

instance Backpressure (Axi4WriteData dom conf userType) where
boolsToBwd _ = C.fromList_lazy . coerce
Expand All @@ -90,7 +86,7 @@

-- | See Table A2-3 "Write data channel signals"
newtype S2M_WriteData = S2M_WriteData { _wready :: Bool }
deriving (Show, Generic, C.NFDataX)

Check warning on line 89 in src/Protocols/Axi4/WriteData.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.6.4 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 89 in src/Protocols/Axi4/WriteData.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.2.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 89 in src/Protocols/Axi4/WriteData.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.4.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

-- | Shorthand for a "well-behaved" write data config,
-- so that we don't need to write out a bunch of type constraints later.
Expand Down
10 changes: 3 additions & 7 deletions src/Protocols/Axi4/WriteResponse.hs
Original file line number Diff line number Diff line change
Expand Up @@ -53,16 +53,12 @@
BIdWidth ('Axi4WriteResponseConfig _ a) = a

-- | AXI4 Read Data channel protocol
data Axi4WriteResponse
type Axi4WriteResponse
(dom :: C.Domain)
(conf :: Axi4WriteResponseConfig)
(userType :: Type)

instance Protocol (Axi4WriteResponse dom conf userType) where
type Fwd (Axi4WriteResponse dom conf userType) =
C.Signal dom (S2M_WriteResponse conf userType)
type Bwd (Axi4WriteResponse dom conf userType) =
C.Signal dom M2S_WriteResponse
= C.Signal dom (S2M_WriteResponse conf userType)
>< C.Signal dom M2S_WriteResponse

instance Backpressure (Axi4WriteResponse dom conf userType) where
boolsToBwd _ = C.fromList_lazy . coerce
Expand All @@ -86,7 +82,7 @@

-- | See Table A2-4 "Write response channel signals"
newtype M2S_WriteResponse = M2S_WriteResponse { _bready :: Bool }
deriving (Show, Generic, C.NFDataX)

Check warning on line 85 in src/Protocols/Axi4/WriteResponse.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.6.4 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 85 in src/Protocols/Axi4/WriteResponse.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.2.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

Check warning on line 85 in src/Protocols/Axi4/WriteResponse.hs

View workflow job for this annotation

GitHub Actions / Cabal tests - ghc 9.4.8 / clash 1.8.1

• Both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled

-- | Shorthand for a "well-behaved" write response config,
-- so that we don't need to write out a bunch of type constraints later.
Expand Down
Loading
Loading