From 98132319569caa71319fc4f04662cb751163e57c Mon Sep 17 00:00:00 2001
From: Brian W Bush <code@functionally.io>
Date: Sun, 16 Nov 2025 09:43:39 -0700
Subject: [PATCH 1/8] Added PATH to nix development shell

---
 flake.nix | 1 +
 1 file changed, 1 insertion(+)

diff --git a/flake.nix b/flake.nix
index 20583da..7f6c705 100644
--- a/flake.nix
+++ b/flake.nix
@@ -26,6 +26,7 @@
           shellHook = ''
             echo "Entering Nix shell with Lean and VS Code..."
             export PS1="\[\e[1;32m\][nix-shell:\w]$\[\e[m\] "
+            export PATH="$PWD/.lake/build/bin:$PATH"
           '';
         };
     in

From c26f8f3a671571fd4024a1fafc2fafa28a5f6795 Mon Sep 17 00:00:00 2001
From: Brian W Bush <code@functionally.io>
Date: Sun, 16 Nov 2025 12:10:12 -0700
Subject: [PATCH 2/8] Implemented effects parsing

---
 src/Ep133.lean         |  4 +++
 src/Ep133/Parsing.lean | 29 +++++++++++++++++
 src/Ep133/Types.lean   | 72 ++++++++++++++++++++++++++++++++++++++++++
 src/Ep133/Util.lean    | 22 +++++++++++++
 src/Ep133Test.lean     | 28 +++++++++++++++-
 5 files changed, 154 insertions(+), 1 deletion(-)
 create mode 100644 src/Ep133/Parsing.lean
 create mode 100644 src/Ep133/Types.lean
 create mode 100644 src/Ep133/Util.lean

diff --git a/src/Ep133.lean b/src/Ep133.lean
index e69de29..a016816 100644
--- a/src/Ep133.lean
+++ b/src/Ep133.lean
@@ -0,0 +1,4 @@
+
+import Ep133.Parsing
+import Ep133.Types
+import Ep133.Util
diff --git a/src/Ep133/Parsing.lean b/src/Ep133/Parsing.lean
new file mode 100644
index 0000000..ca2def0
--- /dev/null
+++ b/src/Ep133/Parsing.lean
@@ -0,0 +1,29 @@
+
+import Ep133.Types
+import Ep133.Util
+
+
+open Ep133.Types
+open Ep133.Util (getFloat32BE require)
+
+
+namespace Ep133.Parsing
+
+
+def parseEffects (raw : ByteArray) : ParseResult Effects :=
+  do
+   require (raw.size = 144)
+      $ ParseResult.throw "Effects not 144 bytes."
+    let effectType := raw.get! 4
+    let offsetBase := (effectType.toNat - 1) * 4
+    let effect ← Effect.ofUInt8 effectType
+    pure
+      {
+        raw
+      , effect
+      , param1 := getFloat32BE raw $ offsetBase + 12
+      , param2 := getFloat32BE raw $ offsetBase + 76
+      }
+
+
+end Ep133.Parsing
diff --git a/src/Ep133/Types.lean b/src/Ep133/Types.lean
new file mode 100644
index 0000000..c4db580
--- /dev/null
+++ b/src/Ep133/Types.lean
@@ -0,0 +1,72 @@
+
+namespace Ep133.Types
+
+
+private instance : Repr ByteArray where
+  reprPrec := reprPrec ∘ ByteArray.toList
+
+
+inductive ParseResult (a : Type) where
+| parsed : a → ParseResult a
+| throw : String → ParseResult a
+deriving Repr, BEq
+
+instance : Monad ParseResult where
+  pure := ParseResult.parsed
+  bind
+  | ParseResult.parsed x, f => f x
+  | ParseResult.throw s, _ => ParseResult.throw s
+
+instance : Alternative ParseResult where
+  failure := ParseResult.throw "Parsing failed."
+  orElse
+  | ParseResult.parsed x, _ => ParseResult.parsed x
+  | ParseResult.throw _, f => f ()
+
+
+inductive Effect where
+| OFF
+| DLY
+| RVB
+| DST
+| CXO
+| FLT
+| CMP
+deriving Repr, BEq
+
+namespace Effect
+
+  open ParseResult
+
+  def ofUInt8 : UInt8 → ParseResult Effect
+  | 0 => parsed OFF
+  | 1 => parsed DLY
+  | 2 => parsed RVB
+  | 3 => parsed DST
+  | 4 => parsed CXO
+  | 5 => parsed FLT
+  | 6 => parsed CMP
+  | i => throw $ "Effect " ++ toString i ++ " is not defined."
+
+end Effect
+
+
+structure Effects where
+  raw : ByteArray
+  effect : Effect
+  param1 : Float32
+  param2 : Float32
+deriving Repr
+
+
+structure Project where
+  pads : ByteArray
+  scenes : ByteArray
+  settings : ByteArray
+  effects : ByteArray
+  scenesSettings  : ByteArray
+  sounds : ByteArray
+deriving Repr
+
+
+end Ep133.Types
diff --git a/src/Ep133/Util.lean b/src/Ep133/Util.lean
new file mode 100644
index 0000000..a783fd9
--- /dev/null
+++ b/src/Ep133/Util.lean
@@ -0,0 +1,22 @@
+
+namespace Ep133.Util
+
+
+def getFloat32BE (bytes : ByteArray) (offset : Nat) : Float32 :=
+  let getUInt32BE (bytes : ByteArray) (offset : Nat) : UInt32 :=
+    let b1 := bytes.get! offset     |> UInt8.toUInt32
+    let b2 := bytes.get! (offset+1) |> UInt8.toUInt32
+    let b3 := bytes.get! (offset+2) |> UInt8.toUInt32
+    let b4 := bytes.get! (offset+3) |> UInt8.toUInt32
+    (b1 <<< 24) ||| (b2 <<< 16) ||| (b3 <<< 8) ||| b4
+  Float32.ofBits $ getUInt32BE bytes offset
+
+
+def require {m : Type → Type} [Monad m] (cond : Bool) (action : m Unit) : m Unit :=
+  if cond then
+    pure ()
+  else
+    action
+
+
+end Ep133.Util
diff --git a/src/Ep133Test.lean b/src/Ep133Test.lean
index 4f2d2b5..445d4ea 100644
--- a/src/Ep133Test.lean
+++ b/src/Ep133Test.lean
@@ -1,4 +1,30 @@
 
+import Ep133
+
+
+open Ep133
+open Ep133.Types
+
+
+namespace Examples
+
+  def rawEffect : ByteArray :=
+    ByteArray.mk #[
+      0x00, 0x00, 0x00, 0x00,  0x00, 0x00, 0x00, 0x00,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x55, 0x3f
+    , 0x00, 0x00, 0x80, 0x3f,  0x00, 0x00, 0xbc, 0x3e,  0x00, 0x00, 0x1f, 0x3f,  0x00, 0x00, 0x00, 0x3f
+    , 0x00, 0x00, 0x06, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f
+    , 0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f
+    , 0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x12, 0x3f,  0x00, 0x00, 0x80, 0x3f
+    , 0x00, 0x00, 0x80, 0x3f,  0x00, 0x00, 0x25, 0x3f,  0x00, 0x00, 0x2e, 0x3f,  0x00, 0x00, 0x00, 0x3f
+    , 0x00, 0x00, 0x7b, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f
+    , 0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f
+    , 0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x00,  0x00, 0x00, 0x00, 0x00
+    ]
+
+end Examples
+
+#guard (Effects.effect <$> Parsing.parseEffects Examples.rawEffect) == ParseResult.parsed Effect.OFF
+
+
 def main (_args : List String) : IO UInt32 :=
   pure 0
-

From 6bb9d22a43c34398f84c1d93a4ee836e1f8c65e5 Mon Sep 17 00:00:00 2001
From: Brian W Bush <code@functionally.io>
Date: Sun, 16 Nov 2025 14:55:41 -0700
Subject: [PATCH 3/8] Implemented parsing of scenes

---
 src/Ep133/Parsing.lean | 39 +++++++++++++++++++++++++++++++++++--
 src/Ep133/Types.lean   | 44 ++++++++++++++++++++++++++++++++++++++++++
 src/Ep133/Util.lean    |  8 ++++----
 src/Ep133Test.lean     | 44 ++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 129 insertions(+), 6 deletions(-)

diff --git a/src/Ep133/Parsing.lean b/src/Ep133/Parsing.lean
index ca2def0..509c522 100644
--- a/src/Ep133/Parsing.lean
+++ b/src/Ep133/Parsing.lean
@@ -6,6 +6,8 @@ import Ep133.Util
 open Ep133.Types
 open Ep133.Util (getFloat32BE require)
 
+open ParseResult (throw)
+
 
 namespace Ep133.Parsing
 
@@ -13,8 +15,8 @@ namespace Ep133.Parsing
 def parseEffects (raw : ByteArray) : ParseResult Effects :=
   do
    require (raw.size = 144)
-      $ ParseResult.throw "Effects not 144 bytes."
-    let effectType := raw.get! 4
+      $ throw "Effects not 144 bytes."
+    let effectType := raw[4]!
     let offsetBase := (effectType.toNat - 1) * 4
     let effect ← Effect.ofUInt8 effectType
     pure
@@ -26,4 +28,37 @@ def parseEffects (raw : ByteArray) : ParseResult Effects :=
       }
 
 
+def makePatternLabel (l : Fin 4) (n : UInt8) : ParseResult PatternLabel :=
+  do
+    require (n > 0 && n < 100)
+      $ throw ("Pattern " ++ toString n ++ " is out of range.")
+    pure {letter := l, number := Fin.ofNat 99 $ n.toNat - 1}
+
+
+def parseScene (raw : ByteArray) (offset : Nat) : ParseResult Scene :=
+  do
+    let patternA ← makePatternLabel 0 $ raw[offset + 0]!
+    let patternB ← makePatternLabel 1 $ raw[offset + 1]!
+    let patternC ← makePatternLabel 2 $ raw[offset + 2]!
+    let patternD ← makePatternLabel 3 $ raw[offset + 3]!
+    pure
+      {
+        patternA, patternB, patternC, patternD
+      , timeSignature := {numerator := raw[offset + 4]!.toNat, denominator := raw[offset + 5]!.toNat}
+      }
+
+
+def parseScenes (raw : ByteArray) : ParseResult Scenes :=
+  do
+    require (raw.size >= 605)
+      $ ParseResult.throw "Scene does not contain at least 605 bytes."
+    let sceneCount := raw[604]! |> UInt8.toNat
+    let scenes : List Scene ← (List.range sceneCount).mapM (fun n ↦ parseScene raw (1 + 6 * n))
+    pure
+      {
+        raw
+      , scenes := scenes.toArray
+      }
+
+
 end Ep133.Parsing
diff --git a/src/Ep133/Types.lean b/src/Ep133/Types.lean
index c4db580..4362625 100644
--- a/src/Ep133/Types.lean
+++ b/src/Ep133/Types.lean
@@ -59,6 +59,50 @@ structure Effects where
 deriving Repr
 
 
+structure TimeSignature where
+  numerator : Nat
+  denominator : Nat
+deriving Repr, BEq
+
+
+structure PatternLabel where
+  letter : Fin 4
+  number : Fin 99
+deriving Repr, BEq
+
+instance : ToString PatternLabel where
+  toString
+  | ⟨ l , n ⟩ =>
+    let letter := l.toNat + 'A'.toNat |> Char.ofNat
+    let number := if n.toNat < 9 then "0" ++ toString (n.toNat + 1) else toString (n.toNat + 1)
+    letter.toString ++ number
+
+
+structure Scene where
+  patternA : PatternLabel
+  patternB : PatternLabel
+  patternC : PatternLabel
+  patternD : PatternLabel
+  timeSignature : TimeSignature
+deriving Repr, BEq
+
+instance : Inhabited Scene where
+  default :=
+    {
+      timeSignature := {numerator := 4, denominator := 4}
+    , patternA := {letter := 0, number := 0}
+    , patternB := {letter := 1, number := 0}
+    , patternC := {letter := 2, number := 0}
+    , patternD := {letter := 3, number := 0}
+    }
+
+
+structure Scenes where
+  raw : ByteArray
+  scenes : Array Scene
+deriving Repr, BEq
+
+
 structure Project where
   pads : ByteArray
   scenes : ByteArray
diff --git a/src/Ep133/Util.lean b/src/Ep133/Util.lean
index a783fd9..80da4c9 100644
--- a/src/Ep133/Util.lean
+++ b/src/Ep133/Util.lean
@@ -4,10 +4,10 @@ namespace Ep133.Util
 
 def getFloat32BE (bytes : ByteArray) (offset : Nat) : Float32 :=
   let getUInt32BE (bytes : ByteArray) (offset : Nat) : UInt32 :=
-    let b1 := bytes.get! offset     |> UInt8.toUInt32
-    let b2 := bytes.get! (offset+1) |> UInt8.toUInt32
-    let b3 := bytes.get! (offset+2) |> UInt8.toUInt32
-    let b4 := bytes.get! (offset+3) |> UInt8.toUInt32
+    let b1 := bytes[offset    ]! |> UInt8.toUInt32
+    let b2 := bytes[offset + 1]! |> UInt8.toUInt32
+    let b3 := bytes[offset + 2]! |> UInt8.toUInt32
+    let b4 := bytes[offset + 3]! |> UInt8.toUInt32
     (b1 <<< 24) ||| (b2 <<< 16) ||| (b3 <<< 8) ||| b4
   Float32.ofBits $ getUInt32BE bytes offset
 
diff --git a/src/Ep133Test.lean b/src/Ep133Test.lean
index 445d4ea..4d5d196 100644
--- a/src/Ep133Test.lean
+++ b/src/Ep133Test.lean
@@ -21,10 +21,54 @@ namespace Examples
     , 0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x3f,  0x00, 0x00, 0x00, 0x00,  0x00, 0x00, 0x00, 0x00
     ]
 
+  def rawScenes : ByteArray :=
+    ByteArray.mk #[
+      0x00, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x03, 0x03, 0x02, 0x02, 0x04, 0x04,  0x03, 0x04, 0x03, 0x03, 0x04, 0x04
+    , 0x05, 0x05, 0x04, 0x04, 0x04, 0x04,  0x02, 0x02, 0x05, 0x04, 0x04, 0x04,  0x07, 0x06, 0x06, 0x05, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04,  0x01, 0x01, 0x01, 0x01, 0x04, 0x04
+    , 0x00, 0x00, 0x00, 0x04
+    , 0x00, 0x00, 0x00, 0x06, 0x00, 0x00, 0x00
+    ]
+
 end Examples
 
 #guard (Effects.effect <$> Parsing.parseEffects Examples.rawEffect) == ParseResult.parsed Effect.OFF
 
+#guard ((Array.size ∘ Scenes.scenes) <$> Parsing.parseScenes Examples.rawScenes) == ParseResult.parsed 4
+
+#guard ((fun x ↦ x.scenes[0]!.timeSignature) <$> Parsing.parseScenes Examples.rawScenes) == ParseResult.parsed {numerator := 4, denominator := 4}
+
 
 def main (_args : List String) : IO UInt32 :=
   pure 0

From a72281bf21880af07fdd0d7c609f8982ff9c9b4d Mon Sep 17 00:00:00 2001
From: Brian W Bush <code@functionally.io>
Date: Sun, 16 Nov 2025 15:13:03 -0700
Subject: [PATCH 4/8] Expanded parsing of effects

---
 src/Ep133/Parsing.lean | 23 +++++++++++++++--------
 src/Ep133/Types.lean   | 24 ++++++++++++++++--------
 src/Ep133Test.lean     |  3 ++-
 3 files changed, 33 insertions(+), 17 deletions(-)

diff --git a/src/Ep133/Parsing.lean b/src/Ep133/Parsing.lean
index 509c522..9771860 100644
--- a/src/Ep133/Parsing.lean
+++ b/src/Ep133/Parsing.lean
@@ -14,17 +14,24 @@ namespace Ep133.Parsing
 
 def parseEffects (raw : ByteArray) : ParseResult Effects :=
   do
-   require (raw.size = 144)
-      $ throw "Effects not 144 bytes."
+   require (raw.size >= 100)
+      $ throw ("Effects only contains " ++ toString raw.size ++ " bytes.")
     let effectType := raw[4]!
-    let offsetBase := (effectType.toNat - 1) * 4
-    let effect ← Effect.ofUInt8 effectType
+    let active ← EffectLabel.ofUInt8 effectType
+    let effects ←
+      (List.range 7).mapM
+        (fun i ↦
+          do
+            let label ← EffectLabel.ofUInt8 i.toUInt8
+            let param1 := getFloat32BE raw $ 8 + 4 * i
+            let param2 := getFloat32BE raw $ 72 + 4 * i
+            pure ⟨ label , {param1, param2} ⟩
+        )
     pure
       {
         raw
-      , effect
-      , param1 := getFloat32BE raw $ offsetBase + 12
-      , param2 := getFloat32BE raw $ offsetBase + 76
+      , active
+      , effects := Std.HashMap.ofList effects
       }
 
 
@@ -51,7 +58,7 @@ def parseScene (raw : ByteArray) (offset : Nat) : ParseResult Scene :=
 def parseScenes (raw : ByteArray) : ParseResult Scenes :=
   do
     require (raw.size >= 605)
-      $ ParseResult.throw "Scene does not contain at least 605 bytes."
+      $ throw ("Scenes only contains " ++ toString raw.size ++ " bytes.")
     let sceneCount := raw[604]! |> UInt8.toNat
     let scenes : List Scene ← (List.range sceneCount).mapM (fun n ↦ parseScene raw (1 + 6 * n))
     pure
diff --git a/src/Ep133/Types.lean b/src/Ep133/Types.lean
index 4362625..29f6294 100644
--- a/src/Ep133/Types.lean
+++ b/src/Ep133/Types.lean
@@ -1,4 +1,7 @@
 
+import Std.Data.HashMap.Basic
+
+
 namespace Ep133.Types
 
 
@@ -24,7 +27,7 @@ instance : Alternative ParseResult where
   | ParseResult.throw _, f => f ()
 
 
-inductive Effect where
+inductive EffectLabel where
 | OFF
 | DLY
 | RVB
@@ -32,13 +35,13 @@ inductive Effect where
 | CXO
 | FLT
 | CMP
-deriving Repr, BEq
+deriving Repr, BEq, Hashable
 
-namespace Effect
+namespace EffectLabel
 
   open ParseResult
 
-  def ofUInt8 : UInt8 → ParseResult Effect
+  def ofUInt8 : UInt8 → ParseResult EffectLabel
   | 0 => parsed OFF
   | 1 => parsed DLY
   | 2 => parsed RVB
@@ -48,14 +51,19 @@ namespace Effect
   | 6 => parsed CMP
   | i => throw $ "Effect " ++ toString i ++ " is not defined."
 
-end Effect
+end EffectLabel
 
 
-structure Effects where
-  raw : ByteArray
-  effect : Effect
+structure EffectParams where
   param1 : Float32
   param2 : Float32
+deriving Repr, BEq
+
+
+structure Effects where
+  raw : ByteArray
+  active : EffectLabel
+  effects : Std.HashMap EffectLabel EffectParams
 deriving Repr
 
 
diff --git a/src/Ep133Test.lean b/src/Ep133Test.lean
index 4d5d196..c00ec87 100644
--- a/src/Ep133Test.lean
+++ b/src/Ep133Test.lean
@@ -63,7 +63,8 @@ namespace Examples
 
 end Examples
 
-#guard (Effects.effect <$> Parsing.parseEffects Examples.rawEffect) == ParseResult.parsed Effect.OFF
+
+#guard (Effects.active <$> Parsing.parseEffects Examples.rawEffect) == ParseResult.parsed EffectLabel.OFF
 
 #guard ((Array.size ∘ Scenes.scenes) <$> Parsing.parseScenes Examples.rawScenes) == ParseResult.parsed 4
 

From b6895bfd5a70cba52fcb94c548fa391a281e5551 Mon Sep 17 00:00:00 2001
From: Brian W Bush <code@functionally.io>
Date: Sun, 16 Nov 2025 16:16:07 -0700
Subject: [PATCH 5/8] Implemented several minor types

---
 src/Ep133/Parsing.lean |  2 +
 src/Ep133/Types.lean   | 99 ++++++++++++++++++++++++++++++++++++++----
 2 files changed, 92 insertions(+), 9 deletions(-)

diff --git a/src/Ep133/Parsing.lean b/src/Ep133/Parsing.lean
index 9771860..dde74fd 100644
--- a/src/Ep133/Parsing.lean
+++ b/src/Ep133/Parsing.lean
@@ -9,6 +9,8 @@ open Ep133.Util (getFloat32BE require)
 open ParseResult (throw)
 
 
+-- See <https://github.com/phones24/ep133-export-to-daw/blob/99454368f8da44b8b5bf495df0f89c72603b8dc4/docs/EP133_FORMATS.md> for reference.
+
 namespace Ep133.Parsing
 
 
diff --git a/src/Ep133/Types.lean b/src/Ep133/Types.lean
index 29f6294..5bb6a17 100644
--- a/src/Ep133/Types.lean
+++ b/src/Ep133/Types.lean
@@ -13,6 +13,7 @@ inductive ParseResult (a : Type) where
 | parsed : a → ParseResult a
 | throw : String → ParseResult a
 deriving Repr, BEq
+open ParseResult (throw)
 
 instance : Monad ParseResult where
   pure := ParseResult.parsed
@@ -39,16 +40,14 @@ deriving Repr, BEq, Hashable
 
 namespace EffectLabel
 
-  open ParseResult
-
   def ofUInt8 : UInt8 → ParseResult EffectLabel
-  | 0 => parsed OFF
-  | 1 => parsed DLY
-  | 2 => parsed RVB
-  | 3 => parsed DST
-  | 4 => parsed CXO
-  | 5 => parsed FLT
-  | 6 => parsed CMP
+  | 0 => pure OFF
+  | 1 => pure DLY
+  | 2 => pure RVB
+  | 3 => pure DST
+  | 4 => pure CXO
+  | 5 => pure FLT
+  | 6 => pure CMP
   | i => throw $ "Effect " ++ toString i ++ " is not defined."
 
 end EffectLabel
@@ -111,6 +110,88 @@ structure Scenes where
 deriving Repr, BEq
 
 
+inductive TimeStretch where
+| OFF
+| BPM
+| BARS
+deriving Repr, BEq
+
+namespace TimeStretch
+
+  def ofUInt8 : UInt8 → ParseResult TimeStretch
+  | 0 => pure OFF
+  | 1 => pure BPM
+  | 2 => pure BARS
+  | i => throw $ "Time stretch " ++ toString i ++ " is not defined."
+
+end TimeStretch
+
+
+inductive TimeStretchBars where
+| WHOLE
+| DOUBLE
+| QUADRUPLE
+| HALF
+| QUARTER
+deriving Repr, BEq
+
+namespace TimeStretchBars
+
+  def ofUInt8 : UInt8 → ParseResult TimeStretchBars
+  | 0 => pure WHOLE
+  | 1 => pure DOUBLE
+  | 2 => pure QUADRUPLE
+  | 255 => pure HALF
+  | 254 => pure QUARTER
+  | i => throw $ "Time stretch bars " ++ toString i ++ " is not defined."
+
+end TimeStretchBars
+
+
+inductive PlayMode where
+| ONE
+| KEY
+| LEG
+deriving Repr, BEq
+
+namespace PlayMode
+
+  def ofUInt8 : UInt8 → ParseResult PlayMode
+  | 0 => pure ONE
+  | 1 => pure KEY
+  | 2 => pure LEG
+  | i => throw $ "Play mode " ++ toString i ++ " is not defined."
+
+end PlayMode
+
+
+inductive ChokeGroup where
+| TRUE
+| FALSE
+deriving Repr, BEq
+
+namespace ChokeGroup
+
+  def ofUInt8 : UInt8 → ParseResult ChokeGroup
+  | 0 => pure TRUE
+  | 1 => pure FALSE
+  | i => throw $ "Choke group " ++ toString i ++ " is not defined."
+
+end ChokeGroup
+
+
+def Volume := Fin 201
+deriving Repr, BEq
+
+
+def Attack := UInt8
+deriving Repr, BEq
+
+
+def Release := UInt8
+deriving Repr, BEq
+
+
 structure Project where
   pads : ByteArray
   scenes : ByteArray

From a36f41737b6249f5c3037f5c3ee12146b6227c46 Mon Sep 17 00:00:00 2001
From: Brian W Bush <code@functionally.io>
Date: Mon, 17 Nov 2025 10:28:55 -0700
Subject: [PATCH 6/8] Implemented pads, and json

---
 src/Ep133/Parsing.lean |  39 ++++++++-
 src/Ep133/Types.lean   | 192 ++++++++++++++++++++++++++++++++++++-----
 src/Ep133/Util.lean    |   8 +-
 3 files changed, 215 insertions(+), 24 deletions(-)

diff --git a/src/Ep133/Parsing.lean b/src/Ep133/Parsing.lean
index dde74fd..dc2f230 100644
--- a/src/Ep133/Parsing.lean
+++ b/src/Ep133/Parsing.lean
@@ -4,7 +4,7 @@ import Ep133.Util
 
 
 open Ep133.Types
-open Ep133.Util (getFloat32BE require)
+open Ep133.Util (getFloat32BE getUInt32 require)
 
 open ParseResult (throw)
 
@@ -70,4 +70,41 @@ def parseScenes (raw : ByteArray) : ParseResult Scenes :=
       }
 
 
+def parsePad (raw : ByteArray) : ParseResult Pad :=
+  do
+    let playMode ← PlayMode.ofUInt8 raw[23]!
+    let volume ← Volume.ofUInt8 raw[16]!
+    let timeStretchMode ← TimeStretchMode.ofUInt8 raw[21]!
+    let timeStretchBars ← TimeStretchBars.ofUInt8 raw[25]!
+    let chokeGroup ← ChokeGroup.ofUInt8 raw[22]!
+    let soundId ← SoundId.ofUInt8s raw[2]! raw[1]!
+    let pan ← Pan.ofUInt8 raw[18]!
+    let trim :=
+      {
+        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]!
+    pure
+      {
+        raw
+      , soundId
+      , volume
+      , attack := raw[19]!
+      , release := raw[20]!
+      , playMode
+      , timeStretch :=
+          {
+            mode := timeStretchMode
+          , bars:= timeStretchBars
+          , bpm := getFloat32BE raw 12
+          }
+      , pitch
+      , trim
+      , pan
+      , chokeGroup
+      , midiChannel := raw[3]!
+      }
+
+
 end Ep133.Parsing
diff --git a/src/Ep133/Types.lean b/src/Ep133/Types.lean
index 5bb6a17..d5b0984 100644
--- a/src/Ep133/Types.lean
+++ b/src/Ep133/Types.lean
@@ -1,6 +1,11 @@
 
+import Ep133.Util
+import Lean.Data.Json.FromToJson
 import Std.Data.HashMap.Basic
+import Std.Data.TreeMap.Raw.Basic
 
+open Ep133.Util (require)
+open Lean (Json ToJson)
 
 namespace Ep133.Types
 
@@ -36,7 +41,7 @@ inductive EffectLabel where
 | CXO
 | FLT
 | CMP
-deriving Repr, BEq, Hashable
+deriving Repr, BEq, Hashable, ToJson
 
 namespace EffectLabel
 
@@ -54,9 +59,9 @@ end EffectLabel
 
 
 structure EffectParams where
-  param1 : Float32
-  param2 : Float32
-deriving Repr, BEq
+  param1 : Float
+  param2 : Float
+deriving Repr, BEq, ToJson
 
 
 structure Effects where
@@ -71,6 +76,12 @@ structure TimeSignature where
   denominator : Nat
 deriving Repr, BEq
 
+instance : ToString TimeSignature where
+  toString x := toString x.numerator ++ "/" ++ toString x.denominator
+
+instance : ToJson TimeSignature where
+  toJson := ToJson.toJson ∘ toString
+
 
 structure PatternLabel where
   letter : Fin 4
@@ -84,6 +95,9 @@ instance : ToString PatternLabel where
     let number := if n.toNat < 9 then "0" ++ toString (n.toNat + 1) else toString (n.toNat + 1)
     letter.toString ++ number
 
+instance : ToJson PatternLabel where
+  toJson := ToJson.toJson ∘ toString
+
 
 structure Scene where
   patternA : PatternLabel
@@ -91,7 +105,7 @@ structure Scene where
   patternC : PatternLabel
   patternD : PatternLabel
   timeSignature : TimeSignature
-deriving Repr, BEq
+deriving Repr, BEq, ToJson
 
 instance : Inhabited Scene where
   default :=
@@ -109,22 +123,25 @@ structure Scenes where
   scenes : Array Scene
 deriving Repr, BEq
 
+instance : ToJson Scenes where
+  toJson := ToJson.toJson ∘ Scenes.scenes
+
 
-inductive TimeStretch where
+inductive TimeStretchMode where
 | OFF
 | BPM
 | BARS
-deriving Repr, BEq
+deriving Repr, BEq, ToJson
 
-namespace TimeStretch
+namespace TimeStretchMode
 
-  def ofUInt8 : UInt8 → ParseResult TimeStretch
+  def ofUInt8 : UInt8 → ParseResult TimeStretchMode
   | 0 => pure OFF
   | 1 => pure BPM
   | 2 => pure BARS
   | i => throw $ "Time stretch " ++ toString i ++ " is not defined."
 
-end TimeStretch
+end TimeStretchMode
 
 
 inductive TimeStretchBars where
@@ -133,7 +150,7 @@ inductive TimeStretchBars where
 | QUADRUPLE
 | HALF
 | QUARTER
-deriving Repr, BEq
+deriving Repr, BEq, ToJson
 
 namespace TimeStretchBars
 
@@ -148,11 +165,18 @@ namespace TimeStretchBars
 end TimeStretchBars
 
 
+structure TimeStretch where
+  mode : TimeStretchMode
+  bars : TimeStretchBars
+  bpm : Float
+deriving Repr, BEq, ToJson
+
+
 inductive PlayMode where
 | ONE
 | KEY
 | LEG
-deriving Repr, BEq
+deriving Repr, BEq, ToJson
 
 namespace PlayMode
 
@@ -168,7 +192,7 @@ end PlayMode
 inductive ChokeGroup where
 | TRUE
 | FALSE
-deriving Repr, BEq
+deriving Repr, BEq, ToJson
 
 namespace ChokeGroup
 
@@ -183,23 +207,149 @@ end ChokeGroup
 def Volume := Fin 201
 deriving Repr, BEq
 
+instance : ToJson Volume where
+  toJson := ToJson.toJson ∘ Fin.toNat
+
+namespace Volume
+
+  def ofUInt8 (i : UInt8) : ParseResult Volume :=
+    do
+      require (i <= 200)
+        $ throw ("Volume " ++ toString i ++ " is too large.")
+      pure $ Fin.ofNat 201 i.toNat
+
+end Volume
+
+
+structure Pitch where
+  integral : Fin 25
+  decimal : UInt8
+deriving Repr, BEq
+
+instance : ToString Pitch where
+  toString x := toString x.integral ++ "." ++ toString x.decimal
+
+instance : ToJson Pitch where
+  toJson := ToJson.toJson ∘ toString
+
+namespace Pitch
+
+  def ofUInt8s (i d : UInt8) : ParseResult Pitch :=
+    do
+      require (i <= 12 || i >= 244)
+        $ throw ("Pitch " ++ toString i ++ " is out of range.")
+      pure
+        {
+          integral := Fin.ofNat 25 $ if i <= 12 then i.toNat + 13 else 256 - i.toNat
+        , decimal := d
+        }
+
+end Pitch
+
+
+def SoundId := Fin 999
+deriving Repr, BEq
+
+instance : ToString SoundId where
+  toString i :=
+    let j := i.toNat + 1
+    if j < 10
+      then "00" ++ toString j
+      else if j < 99
+        then "0" ++ toString j
+        else toString j
+
+instance : ToJson SoundId where
+  toJson := ToJson.toJson ∘ toString
+
+namespace SoundId
+
+  def ofUInt8s (i j : UInt8) : ParseResult SoundId :=
+    do
+      let n := (i.toNat <<< 8) + j.toNat
+      require (n > 0 && n < 1000)
+        $ throw ("Sound ID " ++ toString n ++ " out of range.")
+      pure $ Fin.ofNat 999 (n - 1)
+
+end SoundId
+
+
+def Pan := Fin 33
+deriving Repr, BEq
+
+instance : ToString Pan where
+  toString i := (i.toNat.toFloat / 16 - 1) |> toString
+
+instance : ToJson Pan where
+  toJson i := ToJson.toJson (i.toNat.toFloat / 16 - 1)
+
+namespace Pan
+
+  def ofUInt8 (i : UInt8) : ParseResult Pan :=
+    do
+      require (i <= 16 || i >= 240)
+        $ throw ("Pan " ++ toString i ++ " is out of range.")
+      if i <= 16
+        then pure ∘ Fin.ofNat 33 $ i.toNat + 17
+        else pure ∘ Fin.ofNat 33 $ 255 - i.toNat
+
+end Pan
+
+
+
+structure Trim where
+  left : Nat
+  right : Nat
+deriving Repr, BEq, ToJson
+
 
 def Attack := UInt8
 deriving Repr, BEq
 
+instance : ToJson Attack where
+  toJson := ToJson.toJson ∘ UInt8.toNat
+
 
 def Release := UInt8
 deriving Repr, BEq
 
+instance : ToJson Release where
+  toJson := ToJson.toJson ∘ UInt8.toNat
 
-structure Project where
-  pads : ByteArray
-  scenes : ByteArray
-  settings : ByteArray
-  effects : ByteArray
-  scenesSettings  : ByteArray
-  sounds : ByteArray
-deriving Repr
+
+structure Pad where
+  raw : ByteArray
+  soundId : SoundId
+  volume : Volume
+  attack : Attack
+  release : Release
+  playMode : PlayMode
+  timeStretch : TimeStretch
+  pitch : Pitch
+  trim : Trim
+  pan : Pan
+  chokeGroup : ChokeGroup
+  midiChannel : UInt8
+deriving Repr, BEq
+
+instance : ToJson Pad where
+  toJson x :=
+    open Lean.ToJson (toJson) in
+    ToJson.toJson
+      $ Json.mkObj
+      [
+        ⟨ "soundId" , toJson x.soundId              ⟩
+      , ⟨ "volume"  , toJson x.volume               ⟩
+      , ⟨ "attack"  , toJson x.attack               ⟩
+      , ⟨ "release" , toJson x.release              ⟩
+      , ⟨ "playMode", toJson x.playMode             ⟩
+      , ⟨ "timeStretch", toJson x.timeStretch       ⟩
+      , ⟨ "pitch"      , toJson x.pitch             ⟩
+      , ⟨ "trim"       , toJson x.trim              ⟩
+      , ⟨ "pan"        , toJson x.pan               ⟩
+      , ⟨ "chokeGroup" , toJson x.chokeGroup        ⟩
+      , ⟨ "midiChannel", toJson x.midiChannel.toNat ⟩
+      ]
 
 
 end Ep133.Types
diff --git a/src/Ep133/Util.lean b/src/Ep133/Util.lean
index 80da4c9..57bf354 100644
--- a/src/Ep133/Util.lean
+++ b/src/Ep133/Util.lean
@@ -2,14 +2,18 @@
 namespace Ep133.Util
 
 
-def getFloat32BE (bytes : ByteArray) (offset : Nat) : Float32 :=
+def getFloat32BE (bytes : ByteArray) (offset : Nat) : Float :=
   let getUInt32BE (bytes : ByteArray) (offset : Nat) : UInt32 :=
     let b1 := bytes[offset    ]! |> UInt8.toUInt32
     let b2 := bytes[offset + 1]! |> UInt8.toUInt32
     let b3 := bytes[offset + 2]! |> UInt8.toUInt32
     let b4 := bytes[offset + 3]! |> UInt8.toUInt32
     (b1 <<< 24) ||| (b2 <<< 16) ||| (b3 <<< 8) ||| b4
-  Float32.ofBits $ getUInt32BE bytes offset
+  Float32.toFloat ∘ Float32.ofBits $ getUInt32BE bytes offset
+
+
+def getUInt32 (i j k l : UInt8) : UInt32 :=
+  (i.toUInt32 <<< 24) + (j.toUInt32 <<< 16) + (k.toUInt32 <<< 8) + l.toUInt32
 
 
 def require {m : Type → Type} [Monad m] (cond : Bool) (action : m Unit) : m Unit :=

From d387fc0ddb05f2cabcfd7cd485b90d4d55a59df7 Mon Sep 17 00:00:00 2001
From: Brian W Bush <code@functionally.io>
Date: Mon, 17 Nov 2025 12:13:23 -0700
Subject: [PATCH 7/8] Tweaked pad parsing

---
 src/Ep133/Parsing.lean | 4 +++-
 src/Ep133Test.lean     | 6 ++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/Ep133/Parsing.lean b/src/Ep133/Parsing.lean
index dc2f230..f78bdc3 100644
--- a/src/Ep133/Parsing.lean
+++ b/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
diff --git a/src/Ep133Test.lean b/src/Ep133Test.lean
index c00ec87..6783ecd 100644
--- a/src/Ep133Test.lean
+++ b/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
 
 

From 319647f092130917183b95b91e27029b9281d73d Mon Sep 17 00:00:00 2001
From: Brian W Bush <code@functionally.io>
Date: Mon, 17 Nov 2025 13:20:32 -0700
Subject: [PATCH 8/8] Created CLI interface

---
 src/Ep133/Types.lean | 20 +++++++++++
 src/Main.lean        | 79 ++++++++++++++++++++++++++++++++++++++++++--
 2 files changed, 97 insertions(+), 2 deletions(-)

diff --git a/src/Ep133/Types.lean b/src/Ep133/Types.lean
index d5b0984..92b1b55 100644
--- a/src/Ep133/Types.lean
+++ b/src/Ep133/Types.lean
@@ -43,6 +43,16 @@ inductive EffectLabel where
 | CMP
 deriving Repr, BEq, Hashable, ToJson
 
+instance : ToString EffectLabel where
+  toString
+  | EffectLabel.OFF => "OFF"
+  | EffectLabel.DLY => "DLY"
+  | EffectLabel.RVB => "RVB"
+  | EffectLabel.DST => "DST"
+  | EffectLabel.CXO => "CXO"
+  | EffectLabel.FLT => "FLT"
+  | EffectLabel.CMP => "CMP"
+
 namespace EffectLabel
 
   def ofUInt8 : UInt8 → ParseResult EffectLabel
@@ -70,6 +80,16 @@ structure Effects where
   effects : Std.HashMap EffectLabel EffectParams
 deriving Repr
 
+instance : ToJson Effects where
+  toJson x :=
+    open Lean.ToJson (toJson) in
+    ToJson.toJson
+      $ Json.mkObj
+      [
+        ⟨ "active" , toJson x.active ⟩
+      , ⟨ "effects", Json.mkObj $ x.effects.toList.map (fun ⟨ k , v ⟩ ↦ ⟨ toString k , toJson v ⟩) ⟩
+      ]
+
 
 structure TimeSignature where
   numerator : Nat
diff --git a/src/Main.lean b/src/Main.lean
index c3ff52a..4752160 100644
--- a/src/Main.lean
+++ b/src/Main.lean
@@ -1,3 +1,78 @@
 
-def main (_args : List String) : IO UInt32 :=
-  pure 0
+import Cli
+import Ep133
+
+
+open Cli
+open Ep133.Parsing (parseEffects parsePad parseScenes)
+open Ep133.Types (ParseResult)
+open Lean (ToJson)
+
+
+def dump {α : Type} [ToJson α] (filepathFlag : String) (parse : ByteArray → ParseResult α) (p : Parsed) : IO UInt32 :=
+  do
+    let filepath : String := p.flag! filepathFlag |>.as! String
+    let raw ← IO.FS.readBinFile filepath
+    match parse raw with
+    | ParseResult.parsed x =>
+      IO.println (ToJson.toJson x).pretty
+      pure 0
+    | ParseResult.throw message =>
+      IO.println message
+      pure 1
+
+
+def dumpEffects : Parsed → IO UInt32 := dump "effects-file" parseEffects
+
+def dumpEffectsCmd := `[Cli|
+  "dump-effects" VIA dumpEffects;
+  "Dump the contents of effects."
+  FLAGS:
+    "effects-file" : String ; "The effects file."
+  EXTENSIONS:
+    defaultValues! #[
+      ("effects-file", "/dev/stdin")
+    ]
+]
+
+
+def dumpPad : Parsed → IO UInt32 := dump "pad-file" parsePad
+
+def dumpPadCmd := `[Cli|
+  "dump-pad" VIA dumpPad;
+  "Dump the contents of a pad."
+  FLAGS:
+    "pad-file" : String ; "The pad file."
+  EXTENSIONS:
+    defaultValues! #[
+      ("pad-file", "/dev/stdin")
+    ]
+]
+
+
+def dumpScene : Parsed → IO UInt32 := dump "scenes-file" parseScenes
+
+def dumpSceneCmd := `[Cli|
+  "dump-scenes" VIA dumpScene;
+  "Dump the contents of scenes."
+  FLAGS:
+    "scenes-file" : String ; "The scenes file."
+  EXTENSIONS:
+    defaultValues! #[
+      ("scenes-file", "/dev/stdin")
+    ]
+]
+
+
+def ep133 : Cmd := `[Cli|
+  ep133 NOOP; ["0.0.1"]
+  "Manipulate EP-133 K.O. II backup files."
+  SUBCOMMANDS:
+    dumpEffectsCmd;
+    dumpPadCmd;
+    dumpSceneCmd
+]
+
+
+def main (args : List String) : IO UInt32 :=
+  ep133.validate args