Skip to content

Commit 41832aa

Browse files
brendanzabbrendanzab
committed
Add some more formats
1 parent 0d5fa66 commit 41832aa

File tree

3 files changed

+137
-23
lines changed

3 files changed

+137
-23
lines changed

‎experiments/idris/src/Fathom/Base.idr‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
11
module Fathom.Base
22

33

4+
import Data.Bits
45
import Data.Colist
56
import Data.List
7+
import Data.Vect
68

79

810
---------------------------
@@ -135,3 +137,65 @@ ByteArray : Nat -> Type
135137
ByteArray len = Vect len Bits8
136138

137139
%name ByteArray bytes
140+
141+
142+
||| The byte order of some encoded data, usually a number.
143+
public export
144+
data ByteOrder : Type where
145+
LE : ByteOrder
146+
BE : ByteOrder
147+
148+
149+
namespace ByteStream
150+
151+
splitLen : (n : Nat) -> Colist a -> Maybe (Vect n a, Colist a)
152+
splitLen 0 _ = Nothing
153+
splitLen (S k) [] = Nothing
154+
splitLen (S k) (x :: rest) = map (\(xs, rest') => (x :: xs, rest')) (splitLen k rest)
155+
156+
157+
export
158+
decodeU8 : Decode (Bits8, ByteStream) ByteStream
159+
decodeU8 [] = Nothing
160+
decodeU8 (x :: bytes) = Just (x, bytes)
161+
162+
163+
export
164+
encodeU8 : Encode Bits8 ByteStream
165+
encodeU8 x = Just [x]
166+
167+
168+
export
169+
decodeU16 : ByteOrder -> Decode (Bits16, ByteStream) ByteStream
170+
decodeU16 LE bytes = do
171+
(bs, bytes') <- splitLen 2 bytes
172+
let [b0, b1] = map (cast {to = Bits16}) bs
173+
Just (b0 .|. b1 `shiftL` fromNat 8, bytes')
174+
decodeU16 BE bytes = do
175+
(bs, bytes') <- splitLen 2 bytes
176+
let [b0, b1] = map (cast {to = Bits16}) bs
177+
Just (b0 `shiftL` fromNat 8 .|. b1, bytes')
178+
179+
180+
export
181+
encodeU16 : ByteOrder -> Encode Bits16 ByteStream
182+
encodeU16 LE x = Just [cast x, cast (x `shiftR` fromNat 8)]
183+
encodeU16 BE x = Just [cast (x `shiftR` fromNat 8), cast x]
184+
185+
186+
export
187+
decodeU32 : ByteOrder -> Decode (Bits32, ByteStream) ByteStream
188+
decodeU32 LE bytes = do
189+
(bs, bytes') <- splitLen 4 bytes
190+
let [b0, b1, b2, b3] = map (cast {to = Bits32}) bs
191+
Just (b0 .|. b1 `shiftL` fromNat 8 .|. b2 `shiftL` fromNat 16 .|. b2 `shiftL` fromNat 24, bytes')
192+
decodeU32 BE bytes = do
193+
(bs, bytes') <- splitLen 4 bytes
194+
let [b0, b1, b2, b3] = map (cast {to = Bits32}) bs
195+
Just (b0 `shiftL` fromNat 24 .|. b1 `shiftL` fromNat 16 .|. b2 `shiftL` fromNat 8 .|. b3, bytes')
196+
197+
198+
export
199+
encodeU32 : ByteOrder -> Encode Bits32 ByteStream
200+
encodeU32 LE x = Just [cast x, cast (x `shiftR` fromNat 8), cast (x `shiftR` fromNat 16), cast (x `shiftR` fromNat 24)]
201+
encodeU32 BE x = Just [cast (x `shiftR` fromNat 24), cast (x `shiftR` fromNat 16), cast (x `shiftR` fromNat 8), cast x]

‎experiments/idris/src/Fathom/Closed/InductiveRecursiveCustom.idr‎

Lines changed: 25 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,10 @@
44
module Fathom.Closed.InductiveRecursiveCustom
55

66

7+
import Data.Bits
78
import Data.Colist
89
import Data.Vect
10+
import Data.DPair
911

1012
import Fathom.Base
1113
import Fathom.Data.Sing
@@ -120,11 +122,26 @@ public export
120122
u8 : Format
121123
u8 = Custom (MkCustomFormat
122124
{ Rep = Bits8
123-
, decode = \buffer =>
124-
case buffer of
125-
[] => Nothing
126-
x :: buffer => Just (x, buffer)
127-
, encode = \x => Just [x]
125+
, decode = decodeU8
126+
, encode = encodeU8
127+
})
128+
129+
130+
public export
131+
u16Le : Format
132+
u16Le = Custom (MkCustomFormat
133+
{ Rep = Bits16
134+
, decode = decodeU16 LE
135+
, encode = encodeU16 LE
136+
})
137+
138+
139+
public export
140+
u16Be : Format
141+
u16Be = Custom (MkCustomFormat
142+
{ Rep = Bits16
143+
, decode = decodeU16 BE
144+
, encode = encodeU16 BE
128145
})
129146
130147
@@ -173,8 +190,9 @@ orPure' False _ def = MkFormatOf (Pure def)
173190
flag : Format
174191
flag = do
175192
flag <- u8
176-
if flag == 0 then u8 else
193+
repeat <- if flag == 0 then u8 else
177194
Pure {A = Bits8} 0
195+
Pure ()
178196

179197
-- def simple_glyph = fun (number_of_contours : U16) => {
180198
-- ...
@@ -183,7 +201,7 @@ flag = do
183201
-- };
184202
simple_glyph : Format
185203
simple_glyph = do
186-
(flag ** repeat) <- flag
204+
(flag ** repeat ** MkSing ()) <- flag
187205
let
188206
repeat' : Bits8
189207
repeat' = case flag of

‎experiments/idris/src/Fathom/Open/Record.idr‎

Lines changed: 48 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,8 @@ public export
2727
record Format where
2828
constructor MkFormat
2929
Rep : Type
30-
decode : Decode (Rep, BitStream) BitStream
31-
encode : Encode Rep BitStream
30+
decode : Decode (Rep, ByteStream) ByteStream
31+
encode : Encode Rep ByteStream
3232

3333

3434
--------------
@@ -42,11 +42,11 @@ end = MkFormat { Rep, decode, encode } where
4242
Rep : Type
4343
Rep = Unit
4444

45-
decode : Decode (Rep, BitStream) BitStream
45+
decode : Decode (Rep, ByteStream) ByteStream
4646
decode [] = Just ((), [])
4747
decode (_::_) = Nothing
4848

49-
encode : Encode Rep BitStream
49+
encode : Encode Rep ByteStream
5050
encode () = Just []
5151

5252

@@ -56,10 +56,10 @@ fail = MkFormat { Rep, decode, encode } where
5656
Rep : Type
5757
Rep = Void
5858

59-
decode : Decode (Rep, BitStream) BitStream
59+
decode : Decode (Rep, ByteStream) ByteStream
6060
decode _ = Nothing
6161

62-
encode : Encode Rep BitStream
62+
encode : Encode Rep ByteStream
6363
encode x = void x
6464

6565

@@ -69,10 +69,10 @@ pure x = MkFormat { Rep, decode, encode } where
6969
Rep : Type
7070
Rep = Sing x
7171

72-
decode : Decode (Rep, BitStream) BitStream
72+
decode : Decode (Rep, ByteStream) ByteStream
7373
decode buffer = Just (MkSing x, buffer)
7474

75-
encode : Encode Rep BitStream
75+
encode : Encode Rep ByteStream
7676
encode (MkSing _) = Just []
7777

7878

@@ -82,12 +82,12 @@ skip f def = MkFormat { Rep, decode, encode } where
8282
Rep : Type
8383
Rep = ()
8484

85-
decode : Decode (Rep, BitStream) BitStream
85+
decode : Decode (Rep, ByteStream) ByteStream
8686
decode buffer = do
8787
(x, buffer') <- f.decode buffer
8888
Just ((), buffer')
8989

90-
encode : Encode Rep BitStream
90+
encode : Encode Rep ByteStream
9191
encode () = f.encode def
9292

9393

@@ -97,18 +97,18 @@ repeat len f = MkFormat { Rep, decode, encode } where
9797
Rep : Type
9898
Rep = Vect len f.Rep
9999

100-
decode : Decode (Rep, BitStream) BitStream
100+
decode : Decode (Rep, ByteStream) ByteStream
101101
decode = go len where
102-
go : (len : Nat) -> Decode (Vect len f.Rep, BitStream) BitStream
102+
go : (len : Nat) -> Decode (Vect len f.Rep, ByteStream) ByteStream
103103
go 0 buffer = Just ([], buffer)
104104
go (S len) buffer = do
105105
(x, buffer') <- f.decode buffer
106106
(xs, buffer'') <- go len buffer'
107107
Just (x :: xs, buffer'')
108108
109-
encode : Encode Rep BitStream
109+
encode : Encode Rep ByteStream
110110
encode = go len where
111-
go : (len : Nat) -> Encode (Vect len f.Rep) BitStream
111+
go : (len : Nat) -> Encode (Vect len f.Rep) ByteStream
112112
go 0 [] = Just []
113113
go (S len) (x :: xs) =
114114
[| f.encode x <+> go len xs |]
@@ -120,13 +120,13 @@ bind f1 f2 = MkFormat { Rep, decode, encode } where
120120
Rep : Type
121121
Rep = (x : f1.Rep ** (f2 x).Rep)
122122
123-
decode : Decode (Rep, BitStream) BitStream
123+
decode : Decode (Rep, ByteStream) ByteStream
124124
decode buffer = do
125125
(x, buffer') <- f1.decode buffer
126126
(y, buffer'') <- (f2 x).decode buffer'
127127
Just ((x ** y), buffer'')
128128
129-
encode : Encode Rep BitStream
129+
encode : Encode Rep ByteStream
130130
encode (x ** y) =
131131
[| f1.encode x <+> (f2 x).encode y |]
132132
@@ -138,6 +138,38 @@ public export
138138
(>>=) = bind
139139
140140
141+
--------------------
142+
-- CUSTOM FORMATS --
143+
--------------------
144+
145+
146+
public export
147+
u8 : Format
148+
u8 = MkFormat
149+
{ Rep = Bits8
150+
, decode = decodeU8
151+
, encode = encodeU8
152+
}
153+
154+
155+
public export
156+
u16Le : Format
157+
u16Le = MkFormat
158+
{ Rep = Bits16
159+
, decode = decodeU16 LE
160+
, encode = encodeU16 LE
161+
}
162+
163+
164+
public export
165+
u16Be : Format
166+
u16Be = MkFormat
167+
{ Rep = Bits16
168+
, decode = decodeU16 BE
169+
, encode = encodeU16 BE
170+
}
171+
172+
141173
142174
-----------------
143175
-- EXPERIMENTS --

0 commit comments

Comments
 (0)