Fix partial function warnings in PacketStream

Author: DigitalBrains1

clash-protocols/src/Protocols/PacketStream/Hedgehog.hs

@@ -216,7 +216,12 @@ depacketizerModel toMetaOut ps = L.concat dataWidthPackets
       _ -> fwdF
 
     hdr = bitCoerce $ Vec.unsafeFromList @headerBytes $ _data <$> hdrF
-    metaOut = toMetaOut hdr (_meta $ L.head hdrF)
+    metaIn = case hdrF of
+      [] ->
+        -- There are @headerBytes@ packets in this list, and (1 <= headerBytes)
+        error "depacketizerModel: absurd"
+      (hdrF0 : _) -> _meta hdrF0
+    metaOut = toMetaOut hdr metaIn
 
   bytePackets :: [[PacketStreamM2S 1 metaIn]]
   bytePackets =
@@ -257,10 +262,14 @@ depacketizeToDfModel ::
 depacketizeToDfModel toOut ps = L.map parseHdr bytePackets
  where
   parseHdr :: [PacketStreamM2S 1 metaIn] -> a
-  parseHdr hdrF =
+  parseHdr [] =
+    -- There are at least @headerBytes@ packets in this list, and
+    -- (1 <= headerBytes)
+    error "depacketizeToDfModel: absurd"
+  parseHdr hdrF@(hdrF0 : _) =
     toOut
       (bitCoerce $ Vec.unsafeFromList $ L.map _data hdrF)
-      (_meta $ L.head hdrF)
+      (_meta hdrF0)
 
   bytePackets :: [[PacketStreamM2S 1 metaIn]]
   bytePackets =
@@ -313,9 +322,12 @@ packetizerModel ::
 packetizerModel toMetaOut toHeader ps = L.concatMap (upConvert . prependHdr) bytePackets
  where
   prependHdr :: [PacketStreamM2S 1 metaIn] -> [PacketStreamM2S 1 metaOut]
-  prependHdr fragments = hdr L.++ L.map (\f -> f{_meta = metaOut}) fragments
+  prependHdr [] =
+    -- All elements of bytePackets are guaranteed to be non-null
+    error "packetizerModel: Unreachable state"
+  prependHdr fragments@(h : _) =
+    hdr L.++ L.map (\f -> f{_meta = metaOut}) fragments
    where
-    h = L.head fragments
     metaOut = toMetaOut (_meta h)
     hdr = L.map go (toList $ bitCoerce (toHeader (_meta h)))
     go byte = PacketStreamM2S (singleton byte) Nothing metaOut (_abort h)

clash-protocols/tests/Tests/Protocols/PacketStream/Padding.hs

@@ -33,7 +33,12 @@ stripPaddingModel packets = L.concatMap go (chunkByPacket packets)
   go packet
     | packetBytes == expectedSize = packet
     | packetBytes > expectedSize =
-        x L.++ [(L.head padding){_last = Just 0, _abort = any _abort padding}]
+        case padding of
+          [] ->
+            -- There are (packetBytes - expectedSize) bytes, so more than 0
+            error "stripPaddingModel: absurd"
+          (padding0 : _) ->
+            x L.++ [padding0{_last = Just 0, _abort = any _abort padding}]
     | otherwise = a L.++ [b{_abort = True}]
    where
     (a, b) = case L.unsnoc packet of

clash-protocols/tests/Tests/Protocols/PacketStream/Routing.hs

@@ -62,10 +62,13 @@ makePropPacketArbiter SNat SNat mode =
     pure $ L.map (\pkt -> pkt{_meta = j}) pkts
 
   partitionPackets packets =
-    L.sortOn (_meta . L.head . L.head)
+    L.sortOn getMeta
       $ L.groupBy (\a b -> _meta a == _meta b)
       <$> chunkByPacket packets
 
+  getMeta ((pkt : _) : _) = _meta pkt
+  getMeta _ = error "makePropPacketArbiter: empty partition"
+
 {- |
 Generic test function for the packet dispatcher, testing for all data widths,
 dispatch functions, and some meta types.