Tweaked pad parsing

Author: bwbush

src/Ep133/Parsing.lean

@@ -72,6 +72,8 @@ def parseScenes (raw : ByteArray) : ParseResult Scenes :=
 
 def parsePad (raw : ByteArray) : ParseResult Pad :=
   do
+    require (raw.size = 26)
+      $ throw ("Pad contains " ++ toString raw.size ++ " bytes instead of 27.")
     let playMode ← PlayMode.ofUInt8 raw[23]!
     let volume ← Volume.ofUInt8 raw[16]!
     let timeStretchMode ← TimeStretchMode.ofUInt8 raw[21]!
@@ -84,7 +86,7 @@ def parsePad (raw : ByteArray) : ParseResult Pad :=
         left := getUInt32 0 raw[6]! raw[5]! raw[4]! |> UInt32.toNat
         right := getUInt32 0 raw[10]! raw[9]! raw[8]! |> UInt32.toNat
       }
-    let pitch ← Pitch.ofUInt8s raw[17]! raw[26]!
+    let pitch ← Pitch.ofUInt8s raw[17]! 0  -- raw[26]!
     pure
       {
         raw

src/Ep133Test.lean

@@ -61,6 +61,12 @@ namespace Examples
     , 0x00, 0x00, 0x00, 0x06, 0x00, 0x00, 0x00
     ]
 
+  def rawPad : ByteArray :=
+    ByteArray.mk #[
+      0x00, 0x57, 0x01, 0x00,  0x00, 0x00, 0x00, 0x00,  0x11, 0x69, 0x00, 0x00,  0x00, 0x00, 0x00, 0x00
+    , 0x64, 0x00, 0x00, 0x00,  0xff, 0x00, 0x00, 0x00,  0x3c, 0x00
+    ]
+
 end Examples