Type system progress on bus design

bs/Bus.bs

@@ -3,5 +3,18 @@ package Bus(a) where
 import Types
 import BusTypes
 
+interface (TestType :: * -> *) t = {}
+    -- doSomething :: t -> Action
+
+mkTestType :: (Bits t n, Arith t, Eq t) => Module (TestType t)
+mkTestType = do
+    return $ interface TestType {}
+
+mkTestTop :: Module Empty
+mkTestTop = do
+    testType :: TestType (UInt 5)
+    testType <- mkTestType
+    return $ interface Empty { }
+
 a :: UInt 5
 a = 3

bs/BusTypes.bs

@@ -1,12 +1,12 @@
 package BusTypes(
-    BusVal(..),
-    BusError(..),
-    TransactionSize(..),
-    ReadRequest(..),
-    WriteRequest(..)
+    BusClient(..), BusServer(..),
+    BusRequest(..), BusResponse(..),
+    ReadRequest(..), ReadResponse(..), WriteRequest(..), WriteResponse(..),
+    BusVal(..), BusError(..), TransactionSize(..)
     ) where
 
 import Types
+import Vector
 
 data BusError
     = UnMapped
@@ -48,21 +48,51 @@ data BusResponse
   | BusWriteResponse    WriteResponse
   deriving (Bits, Eq, FShow)
 
-interface BusMaster =
-  -- The Bus arbiter will call the Bus Master's request method
-  -- if and only if it's the Bus Master's turn to make a request, and the Bus Master
-  -- has a request to make.
-  -- It is up to the BusMaster to guard it's request method such that calling
-  -- it's request method is only valid when the BusMaster has a request to make.
-  -- This has implications about for the implementor of BusMaster, namely, that it
-  -- should hold its request until it's request method gets called.
-  request  :: BusRequest
-  -- From the masters's perspective, the response should not be called by the
-  -- arbiter until the master is ready to accept the response. In other words,
-  -- response should be guarded by the client.
-  response :: BusResponse -> Action
+-- # BusClient.dequeueRequest
+--   * The Bus arbiter will call the Bus Client's request method if it is
+--     the Bus Client's turn to make a request, or if another client forfits
+--     its turn.
+--   * The BusClient must guard its request method such that calling its
+--     request method is only valid when the BusClient has a request to make.
+--   * This has implications about for the implementor of BusClient,
+--     namely, that it should hold its request until it's request method
+--     gets called. The arbiter tags the request so that the client can
+--     later correctly correlate the response.
+--   * Although the tag is technically passed in as an argument from the
+--     arbiter to the client's request method, given that methods are
+--     atomic in Bluespec, this is effectively equivalent to tagging the
+--     transaction from the client's perspective. Thus, the client must
+--     take care to appropiately store the tag.
+-- # BusClient.enqueueResponse
+--   * From the client's perspective, the response should not be called
+--     by the arbiter until the client is ready to accept the response.
+--     In other words, the response method should be guarded by the client.
+interface (BusClient :: * -> *) transactionTagType =
+  dequeueRequest  :: transactionTagType -> ActionValue BusRequest
+  enqueueResponse :: (BusResponse, transactionTagType) -> Action
+
+-- # BusServer.dequeueResponse
+--   * If the arbiter is able to successfully call `dequeueResponse`, then
+--     the BusServer's internal logici must update such that it understand
+--     the response has been handed off.
+-- # BusServer.peekClientTagDestination
+--   * The arbiter looks at (peekClientTagDestination :: clientTagTye) to
+--     determine whether or not it is currently safe whether to dequeue the
+--     response as well as where to route the response should it dequeue the
+--     response.
+--   * `peekClientTagDestination` should be guarded on whether or not there is
+--     a valid response available.
+interface (BusServer :: * -> * -> *) transactionTagType clientTagType =
+  enqueueRequest  :: (transactionTagType, BusRequest) -> Action
+  dequeueResponse :: ActionValue (clientTagType, BusResponse, transactionTagType)
+  peekClientTagDestination :: clientTagTye
+
+interface (Bus :: # -> # -> * -> * -> *) numClients numServers transactionTagType clientTagType =
+  clients :: Vector numClients (BusClient transactionTagType)
+  servers :: Vector numServers (BusServer transactionTagType clientTagType)
 
 type Token = UInt 5
+type Numeric = 5
 
 a :: UInt 5
 a = 3