Do not verify lengths in propWithModel

The input length is not always equal to the output length, nor even
predictable. Furthermore, some properties might not be interested in the
length in the first place.

Fixes #81

clash-protocols.cabal

@@ -135,7 +135,8 @@ library
 
   build-depends:
       -- inline-circuit-notation
-      circuit-notation
+    , circuit-notation
+    , clash-prelude-hedgehog
     , data-default
     , deepseq
     , extra

src/Protocols/Avalon/Stream.hs

@@ -251,9 +251,8 @@ instance
   ) =>
   Test (AvalonStream dom conf dataType)
   where
-  expectToLengths Proxy = pure . P.length
-  expectN Proxy options nExpected sampled =
-    expectN (Proxy @(Df.Df dom _)) options nExpected
+  expectN Proxy options sampled =
+    expectN (Proxy @(Df.Df dom _)) options
       $ Df.maybeToData
       <$> sampled
 

src/Protocols/Axi4/Stream.hs

@@ -17,7 +17,6 @@ import Control.DeepSeq (NFData)
 import Data.Hashable (Hashable, hashWithSalt)
 import qualified Data.Maybe as Maybe
 import Data.Proxy
-import qualified Prelude as P
 
 -- clash-prelude
 import Clash.Prelude hiding (concat, length, take)
@@ -129,7 +128,7 @@ instance
     s0 = ()
     blankOtp = Nothing
     stateFn ack _ otpItem =
-      pure (otpItem, Nothing, Maybe.isJust otpItem && _tready ack)
+      pure (otpItem, Nothing, Maybe.isJust otpItem C.&& _tready ack)
 
   fromDfCircuit proxy = DfConv.fromDfCircuitHelper proxy s0 blankOtp stateFn
    where
@@ -153,9 +152,9 @@ instance
   sigToSimFwd _ s = sample_lazy s
   sigToSimBwd _ s = sample_lazy s
 
-  stallC conf (head -> (stallAck, stalls)) =
-    withClockResetEnable clockGen resetGen enableGen
-      $ DfConv.stall Proxy Proxy conf stallAck stalls
+  stallC conf (C.head -> (stallAck, stalls)) =
+    withClockResetEnable clockGen resetGen enableGen $
+      DfConv.stall Proxy Proxy conf stallAck stalls
 
 instance
   (KnownAxi4StreamConfig conf, NFDataX userType, KnownDomain dom) =>
@@ -169,12 +168,12 @@ instance
   fromSimulateType Proxy = Maybe.catMaybes
 
   driveC conf vals =
-    withClockResetEnable clockGen resetGen enableGen
-      $ DfConv.drive Proxy conf vals
+    withClockResetEnable clockGen resetGen enableGen $
+      DfConv.drive Proxy conf vals
   sampleC conf ckt =
-    withClockResetEnable clockGen resetGen enableGen
-      $ DfConv.sample Proxy conf
-      $ ckt
+    withClockResetEnable clockGen resetGen enableGen $
+      DfConv.sample Proxy conf $
+        ckt
 
 instance
   ( KnownAxi4StreamConfig conf
@@ -187,11 +186,10 @@ instance
   ) =>
   Test (Axi4Stream dom conf userType)
   where
-  expectToLengths Proxy = pure . P.length
-  expectN Proxy options nExpected sampled =
-    expectN (Proxy @(Df.Df dom _)) options nExpected
-      $ Df.maybeToData
-      <$> sampled
+  expectN Proxy options sampled =
+    expectN (Proxy @(Df.Df dom _)) options $
+      Df.maybeToData
+        <$> sampled
 
 instance IdleCircuit (Axi4Stream dom conf userType) where
   idleFwd Proxy = C.pure Nothing

src/Protocols/Hedgehog.hs

@@ -41,8 +41,10 @@ import Protocols.Hedgehog.Internal
 -- clash-prelude
 import qualified Clash.Prelude as C
 
--- hedgehog
+-- clash-prelude-hedgehog
+import Clash.Hedgehog.Sized.Vector (genVec)
 
+-- hedgehog
 import Hedgehog ((===))
 import qualified Hedgehog as H
 import qualified Hedgehog.Gen as Gen
@@ -60,6 +62,16 @@ resetGen n =
   C.unsafeFromActiveHigh
     (C.fromList (replicate n True <> repeat False))
 
+smallInt :: H.Range Int
+smallInt = Range.linear 0 10
+
+genSmallInt :: H.Gen Int
+genSmallInt =
+  Gen.frequency
+    [ (90, Gen.integral smallInt)
+    , (10, Gen.constant (Range.lowerBound 99 smallInt))
+    ]
+
 {- | Test a protocol against a pure model implementation. Circuit under test will
 be arbitrarily stalled on the left hand and right hand side and tested for
 a number of properties:
@@ -89,21 +101,23 @@ propWithModel ::
   H.Property
 propWithModel eOpts genData model prot prop = H.property $ do
   dat <- H.forAll genData
-  let n = maximum (expectToLengths (Proxy @a) dat)
+
+  -- TODO: Different 'n's for each output
+  n <- H.forAll (Gen.integral (Range.linear 0 (eoSampleMax eOpts)))
 
   -- TODO: Different distributions?
-  let genStall = Gen.integral (Range.linear 0 10)
+  let genStall = genSmallInt
 
   -- Generate stalls for LHS part of the protocol. The first line determines
   -- whether to stall or not. The second determines how many cycles to stall
   -- on each _valid_ cycle.
-  lhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels a) genStallMode))
+  lhsStallModes <- H.forAll (genVec genStallMode)
   lhsStalls <- H.forAll (traverse (genStalls genStall n) lhsStallModes)
 
   -- Generate stalls for RHS part of the protocol. The first line determines
   -- whether to stall or not. The second determines how many cycles to stall
   -- on each _valid_ cycle.
-  rhsStallModes <- H.forAll (sequenceA (C.repeat @(SimulateChannels b) genStallMode))
+  rhsStallModes <- H.forAll (genVec genStallMode)
   rhsStalls <- H.forAll (traverse (genStalls genStall n) rhsStallModes)
 
   let
@@ -121,10 +135,9 @@ propWithModel eOpts genData model prot prop = H.property $ do
         |> prot
         |> rhsStallC
     sampled = sampleC simConfig stalledProtocol
-    lengths = expectToLengths (Proxy @b) expected
 
   -- expectN errors if circuit does not produce enough data
-  trimmed <- expectN (Proxy @b) eOpts lengths sampled
+  trimmed <- expectN (Proxy @b) eOpts sampled
 
   _ <- H.evalNF trimmed
   _ <- H.evalNF expected