Bus types typecheck!!!

bs/Bus.bs

@@ -21,11 +21,11 @@ mkTestTop = do
     testType <- mkTestType
     return $ interface Empty { }
 
-mkBus :: Vector numClients (BusClient (UInt (TLog numClients)))
+mkBus :: Vector numClients (BusClient inFlightTransactions)
-      -> Vector numServers (BusServer (UInt (TLog numClients)) clientTagType)
+      -> Vector numServers (BusServer inFlightTransactions numClients)
       -> Module Empty
 mkBus clientVec serverVec = do
-    tagEngineByClient :: Vector numClients (TagEngine (TLog numClients))
+    tagEngineByClient :: Vector numClients (TagEngine inFlightTransactions)
     tagEngineByClient <- replicateM mkTagEngine
 
     return $ interface Empty { }

bs/BusTypes.bs

@@ -1,5 +1,5 @@
 package BusTypes(
-    Bus(..),
+    ClientTagType,
     BusClient(..), BusServer(..),
     BusRequest(..), BusResponse(..),
     ReadRequest(..), ReadResponse(..), WriteRequest(..), WriteResponse(..),
@@ -8,6 +8,9 @@ package BusTypes(
 
 import Types
 import Vector
+import TagEngine
+
+type ClientTagType a = (UInt (TLog a))
 
 data BusError
     = UnMapped
@@ -68,25 +71,31 @@ data BusResponse
 --   * 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 =
+interface (BusClient :: # -> *) inFlightTransactions =
-  dequeueRequest  :: transactionTagType -> ActionValue BusRequest
+  dequeueRequest  :: TagType inFlightTransactions
-  enqueueResponse :: (BusResponse, transactionTagType) -> Action
+                  -> ActionValue BusRequest
+  enqueueResponse :: (BusResponse, TagType inFlightTransactions)
+                  -> 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
+--   * The arbiter looks at (peekClientTagDestination :: clientTagType) 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 =
+interface (BusServer :: # -> # -> *) inFlightTransactions numClients =
-  enqueueRequest  :: (transactionTagType, BusRequest) -> Action
+  enqueueRequest  :: (TagType inFlightTransactions, BusRequest)
-  dequeueResponse :: ActionValue (clientTagType, BusResponse, transactionTagType)
+                  -> Action
-  peekClientTagDestination :: clientTagTye
+  dequeueResponse :: ActionValue (
+                      ClientTagType numClients,
+                      BusResponse, transactionTagType
+                      )
+  peekClientTagDestination :: clientTagType
 
 type Token = UInt 5
 type Numeric = 5

bs/TagEngine.bs

@@ -1,4 +1,5 @@
 package TagEngine(
+    TagType,
     TagEngine(..),
     Util.BasicResult(..),
     mkTagEngine) where
@@ -9,11 +10,11 @@ import FIFO
 import FIFOF
 import SpecialFIFOs
 
-#define UIntLog2N(n) (UInt (TLog n))
+type TagType a = (UInt (TLog a))
 
 interface (TagEngine :: # -> *) numTags =
-    requestTag :: ActionValue UIntLog2N(numTags)
+    requestTag :: ActionValue (TagType numTags)
-    retireTag  :: UIntLog2N(numTags) -> Action
+    retireTag  :: (TagType numTags) -> Action
 
 -- The tag engine returns a tag that is unique for the duration of
 -- the lifetime of the tag. Useful when you need to tag transactions
@@ -79,7 +80,7 @@ mkTagEngine = do
     -- Interface
     return $
         interface TagEngine
-            requestTag :: ActionValue UIntLog2N(numTags)
+            requestTag :: ActionValue (TagType numTags)
             requestTag = do
                 case initialTagDistributor of
                     Just 0 -> do
@@ -100,7 +101,7 @@ mkTagEngine = do
             -- so it is advisable that the caller of `retireTag` only attempt to retire valid tags.
             -- Internally, the tagEngine will keep a correct and consistent state since TagEngine
             -- validates tags before attempting to retire them.
-            retireTag :: UIntLog2N(numTags) -> Action
+            retireTag :: (TagType numTags) -> Action
             retireTag tag =
                 do
                     let