Skip to content

Commit 6bb9d22

Browse files
bwbushbwbush
committed
Implemented parsing of scenes
1 parent c26f8f3 commit 6bb9d22

4 files changed

Lines changed: 129 additions & 6 deletions

File tree

‎src/Ep133/Parsing.lean‎

Lines changed: 37 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,15 +6,17 @@ import Ep133.Util
66
open Ep133.Types
77
open Ep133.Util (getFloat32BE require)
88

9+
open ParseResult (throw)
10+
911

1012
namespace Ep133.Parsing
1113

1214

1315
def parseEffects (raw : ByteArray) : ParseResult Effects :=
1416
do
1517
require (raw.size = 144)
16-
$ ParseResult.throw "Effects not 144 bytes."
17-
let effectType := raw.get! 4
18+
$ throw "Effects not 144 bytes."
19+
let effectType := raw[4]!
1820
let offsetBase := (effectType.toNat - 1) * 4
1921
let effect ← Effect.ofUInt8 effectType
2022
pure
@@ -26,4 +28,37 @@ def parseEffects (raw : ByteArray) : ParseResult Effects :=
2628
}
2729

2830

31+
def makePatternLabel (l : Fin 4) (n : UInt8) : ParseResult PatternLabel :=
32+
do
33+
require (n > 0 && n < 100)
34+
$ throw ("Pattern " ++ toString n ++ " is out of range.")
35+
pure {letter := l, number := Fin.ofNat 99 $ n.toNat - 1}
36+
37+
38+
def parseScene (raw : ByteArray) (offset : Nat) : ParseResult Scene :=
39+
do
40+
let patternA ← makePatternLabel 0 $ raw[offset + 0]!
41+
let patternB ← makePatternLabel 1 $ raw[offset + 1]!
42+
let patternC ← makePatternLabel 2 $ raw[offset + 2]!
43+
let patternD ← makePatternLabel 3 $ raw[offset + 3]!
44+
pure
45+
{
46+
patternA, patternB, patternC, patternD
47+
, timeSignature := {numerator := raw[offset + 4]!.toNat, denominator := raw[offset + 5]!.toNat}
48+
}
49+
50+
51+
def parseScenes (raw : ByteArray) : ParseResult Scenes :=
52+
do
53+
require (raw.size >= 605)
54+
$ ParseResult.throw "Scene does not contain at least 605 bytes."
55+
let sceneCount := raw[604]! |> UInt8.toNat
56+
let scenes : List Scene ← (List.range sceneCount).mapM (fun n ↦ parseScene raw (1 + 6 * n))
57+
pure
58+
{
59+
raw
60+
, scenes := scenes.toArray
61+
}
62+
63+
2964
end Ep133.Parsing

‎src/Ep133/Types.lean‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,50 @@ structure Effects where
5959
deriving Repr
6060

6161

62+
structure TimeSignature where
63+
numerator : Nat
64+
denominator : Nat
65+
deriving Repr, BEq
66+
67+
68+
structure PatternLabel where
69+
letter : Fin 4
70+
number : Fin 99
71+
deriving Repr, BEq
72+
73+
instance : ToString PatternLabel where
74+
toString
75+
| ⟨ l , n ⟩ =>
76+
let letter := l.toNat + 'A'.toNat |> Char.ofNat
77+
let number := if n.toNat < 9 then "0" ++ toString (n.toNat + 1) else toString (n.toNat + 1)
78+
letter.toString ++ number
79+
80+
81+
structure Scene where
82+
patternA : PatternLabel
83+
patternB : PatternLabel
84+
patternC : PatternLabel
85+
patternD : PatternLabel
86+
timeSignature : TimeSignature
87+
deriving Repr, BEq
88+
89+
instance : Inhabited Scene where
90+
default :=
91+
{
92+
timeSignature := {numerator := 4, denominator := 4}
93+
, patternA := {letter := 0, number := 0}
94+
, patternB := {letter := 1, number := 0}
95+
, patternC := {letter := 2, number := 0}
96+
, patternD := {letter := 3, number := 0}
97+
}
98+
99+
100+
structure Scenes where
101+
raw : ByteArray
102+
scenes : Array Scene
103+
deriving Repr, BEq
104+
105+
62106
structure Project where
63107
pads : ByteArray
64108
scenes : ByteArray

‎src/Ep133/Util.lean‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,10 @@ namespace Ep133.Util
44

55
def getFloat32BE (bytes : ByteArray) (offset : Nat) : Float32 :=
66
let getUInt32BE (bytes : ByteArray) (offset : Nat) : UInt32 :=
7-
let b1 := bytes.get! offset |> UInt8.toUInt32
8-
let b2 := bytes.get! (offset+1) |> UInt8.toUInt32
9-
let b3 := bytes.get! (offset+2) |> UInt8.toUInt32
10-
let b4 := bytes.get! (offset+3) |> UInt8.toUInt32
7+
let b1 := bytes[offset ]! |> UInt8.toUInt32
8+
let b2 := bytes[offset + 1]! |> UInt8.toUInt32
9+
let b3 := bytes[offset + 2]! |> UInt8.toUInt32
10+
let b4 := bytes[offset + 3]! |> UInt8.toUInt32
1111
(b1 <<< 24) ||| (b2 <<< 16) ||| (b3 <<< 8) ||| b4
1212
Float32.ofBits $ getUInt32BE bytes offset
1313

‎src/Ep133Test.lean‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,10 +21,54 @@ namespace Examples
2121
, 0x00, 0x00, 0x00, 0x3f, 0x00, 0x00, 0x00, 0x3f, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00
2222
]
2323

24+
def rawScenes : ByteArray :=
25+
ByteArray.mk #[
26+
0x00, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
27+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x03, 0x03, 0x02, 0x02, 0x04, 0x04, 0x03, 0x04, 0x03, 0x03, 0x04, 0x04
28+
, 0x05, 0x05, 0x04, 0x04, 0x04, 0x04, 0x02, 0x02, 0x05, 0x04, 0x04, 0x04, 0x07, 0x06, 0x06, 0x05, 0x04, 0x04
29+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
30+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
31+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
32+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
33+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
34+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
35+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
36+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
37+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
38+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
39+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
40+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
41+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
42+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
43+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
44+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
45+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
46+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
47+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
48+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
49+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
50+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
51+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
52+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
53+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
54+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
55+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
56+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
57+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
58+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
59+
, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04, 0x01, 0x01, 0x01, 0x01, 0x04, 0x04
60+
, 0x00, 0x00, 0x00, 0x04
61+
, 0x00, 0x00, 0x00, 0x06, 0x00, 0x00, 0x00
62+
]
63+
2464
end Examples
2565

2666
#guard (Effects.effect <$> Parsing.parseEffects Examples.rawEffect) == ParseResult.parsed Effect.OFF
2767

68+
#guard ((Array.size ∘ Scenes.scenes) <$> Parsing.parseScenes Examples.rawScenes) == ParseResult.parsed 4
69+
70+
#guard ((fun x ↦ x.scenes[0]!.timeSignature) <$> Parsing.parseScenes Examples.rawScenes) == ParseResult.parsed {numerator := 4, denominator := 4}
71+
2872

2973
def main (_args : List String) : IO UInt32 :=
3074
pure 0

0 commit comments

Comments
 (0)