Skip to content

Commit 0f475d3

Browse files
brendanzabbrendanzab
committed
Add pair formats
1 parent 0d01ee2 commit 0f475d3

File tree

7 files changed

+93
-0
lines changed

7 files changed

+93
-0
lines changed

‎experiments/idris/src/Fathom/Format/IndexedInductive.idr‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ data FormatOf : Type -> Type where
2626
Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
2727
Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
2828
Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
29+
Pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B)
2930
Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
3031

3132

@@ -60,6 +61,10 @@ namespace FormatOf
6061
x <- decode f
6162
xs <- decode (Repeat len f)
6263
pure (x :: xs)
64+
decode (Pair f1 f2) = do
65+
x <- decode f1
66+
y <- decode f2
67+
pure (x, y)
6368
decode (Bind f1 f2) = do
6469
x <- decode f1
6570
y <- decode (f2 x)
@@ -74,6 +79,8 @@ namespace FormatOf
7479
encode (Repeat Z f) [] = pure []
7580
encode (Repeat (S len) f) (x :: xs) =
7681
[| encode f x <+> encode (Repeat len f) xs |]
82+
encode (Pair f1 f2) (x, y) =
83+
[| encode f1 x <+> encode f2 y |]
7784
encode (Bind f1 f2) (x ** y) =
7885
[| encode f1 x <+> encode (f2 x) y |]
7986

@@ -190,6 +197,11 @@ namespace Format
190197
repeat len f = MkFormat (Vect len f.Rep) (Repeat len (toFormatOf f))
191198

192199

200+
public export
201+
pair : Format -> Format -> Format
202+
pair f1 f2 = MkFormat (f1.Rep, f2.Rep) (Pair (toFormatOf f1) (toFormatOf f2))
203+
204+
193205
public export
194206
bind : (f : Format) -> (Rep f -> Format) -> Format
195207
bind f1 f2 =

‎experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ data FormatOf : (A : Type) -> Type where
3939
Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
4040
Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
4141
Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
42+
Pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B)
4243
Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
4344
Custom : (f : CustomFormat) -> FormatOf f.Rep
4445

@@ -74,6 +75,10 @@ namespace FormatOf
7475
x <- decode f
7576
xs <- decode (Repeat len f)
7677
pure (x :: xs)
78+
decode (Pair f1 f2) = do
79+
x <- decode f1
80+
y <- decode f2
81+
pure (x, y)
7782
decode (Bind f1 f2) = do
7883
x <- decode f1
7984
y <- decode (f2 x)
@@ -89,6 +94,8 @@ namespace FormatOf
8994
encode (Repeat Z f) [] = pure []
9095
encode (Repeat (S len) f) (x :: xs) =
9196
[| encode f x <+> encode (Repeat len f) xs |]
97+
encode (Pair f1 f2) (x, y) =
98+
[| encode f1 x <+> encode f2 y |]
9299
encode (Bind f1 f2) (x ** y) =
93100
[| encode f1 x <+> encode (f2 x) y |]
94101
encode (Custom f) x = f.encode x
@@ -206,6 +213,11 @@ namespace Format
206213
repeat len f = MkFormat (Vect len f.Rep) (Repeat len (toFormatOf f))
207214

208215

216+
public export
217+
pair : Format -> Format -> Format
218+
pair f1 f2 = MkFormat (f1.Rep, f2.Rep) (Pair (toFormatOf f1) (toFormatOf f2))
219+
220+
209221
public export
210222
bind : (f : Format) -> (Rep f -> Format) -> Format
211223
bind f1 f2 =

‎experiments/idris/src/Fathom/Format/InductiveRecursive.idr‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ mutual
4545
Pure : {0 A : Type} -> A -> Format
4646
Ignore : (f : Format) -> (def : f.Rep) -> Format
4747
Repeat : Nat -> Format -> Format
48+
Pair : Format -> Format -> Format
4849
Bind : (f : Format) -> (f.Rep -> Format) -> Format
4950

5051

@@ -56,6 +57,7 @@ mutual
5657
Rep (Ignore _ _) = Unit
5758
Rep (Repeat len f) = Vect len f.Rep
5859
Rep (Pure x) = Sing x
60+
Rep (Pair f1 f2) = (f1.Rep, f2.Rep)
5961
Rep (Bind f1 f2) = (x : f1.Rep ** (f2 x).Rep)
6062

6163

@@ -96,6 +98,10 @@ namespace Format
9698
x <- decode f
9799
xs <- decode (Repeat len f)
98100
pure (x :: xs)
101+
decode (Pair f1 f2) = do
102+
x <- decode f1
103+
y <- decode f2
104+
pure (x, y)
99105
decode (Bind f1 f2) = do
100106
x <- decode f1
101107
y <- decode (f2 x)
@@ -110,6 +116,8 @@ namespace Format
110116
encode (Repeat Z f) [] = pure []
111117
encode (Repeat (S len) f) (x :: xs) =
112118
[| encode f x <+> encode (Repeat len f) xs |]
119+
encode (Pair f1 f2) (x, y) =
120+
[| encode f1 x <+> encode f2 y |]
113121
encode (Bind f1 f2) (x ** y) =
114122
[| encode f1 x <+> encode (f2 x) y |]
115123

@@ -225,6 +233,14 @@ namespace FormatOf
225233
toFormatOfEq (Element (Repeat len f) (cong (Vect len) prf))
226234

227235

236+
public export
237+
pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B)
238+
pair f1 f2 with (toFormatEq f1, toFormatEq f2)
239+
pair _ _ | (Element f1 prf1, Element f2 prf2) =
240+
toFormatOfEq (Element (Pair f1 f2)
241+
(rewrite prf1 in rewrite prf2 in Refl))
242+
243+
228244
public export
229245
bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
230246
bind f1 f2 with (toFormatEq f1)

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

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,7 @@ mutual
4141
Pure : {0 A : Type} -> A -> Format
4242
Ignore : (f : Format) -> (def : f.Rep) -> Format
4343
Repeat : Nat -> Format -> Format
44+
Pair : Format -> Format -> Format
4445
Bind : (f : Format) -> (f.Rep -> Format) -> Format
4546
Custom : (f : CustomFormat) -> Format
4647

@@ -53,6 +54,7 @@ mutual
5354
Rep (Ignore _ _) = Unit
5455
Rep (Repeat len f) = Vect len f.Rep
5556
Rep (Pure x) = Sing x
57+
Rep (Pair f1 f2) = (f1.Rep, f2.Rep)
5658
Rep (Bind f1 f2) = (x : f1.Rep ** (f2 x).Rep)
5759
Rep (Custom f) = f.Rep
5860

@@ -94,6 +96,10 @@ namespace Format
9496
x <- decode f
9597
xs <- decode (Repeat len f)
9698
pure (x :: xs)
99+
decode (Pair f1 f2) = do
100+
x <- decode f1
101+
y <- decode f2
102+
pure (x, y)
97103
decode (Bind f1 f2) = do
98104
x <- decode f1
99105
y <- decode (f2 x)
@@ -109,6 +115,8 @@ namespace Format
109115
encode (Repeat Z f) [] = pure []
110116
encode (Repeat (S len) f) (x :: xs) =
111117
[| encode f x <+> encode (Repeat len f) xs |]
118+
encode (Pair f1 f2) (x, y) =
119+
[| encode f1 x <+> encode f2 y |]
112120
encode (Bind f1 f2) (x ** y) =
113121
[| encode f1 x <+> encode (f2 x) y |]
114122
encode (Custom f) x = f.encode x
@@ -257,6 +265,14 @@ namespace FormatOf
257265
toFormatOfEq (Element (Repeat len f) (cong (Vect len) prf))
258266

259267

268+
public export
269+
pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B)
270+
pair f1 f2 with (toFormatEq f1, toFormatEq f2)
271+
pair _ _ | (Element f1 prf1, Element f2 prf2) =
272+
toFormatOfEq (Element (Pair f1 f2)
273+
(rewrite prf1 in rewrite prf2 in Refl))
274+
275+
260276
public export
261277
bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
262278
bind f1 f2 with (toFormatEq f1)

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

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -111,6 +111,23 @@ namespace Format
111111
[| f.encode x <+> go len xs |]
112112

113113

114+
public export
115+
pair : Format -> Format -> Format
116+
pair f1 f2 = MkFormat { Rep, decode, encode } where
117+
Rep : Type
118+
Rep = (f1.Rep, f2.Rep)
119+
120+
decode : DecodePart Rep ByteStream
121+
decode = do
122+
x <- f1.decode
123+
y <- f2.decode
124+
pure (x, y)
125+
126+
encode : Encode Rep ByteStream
127+
encode (x, y) =
128+
[| f1.encode x <+> f2.encode y |]
129+
130+
114131
public export
115132
bind : (f : Format) -> (f.Rep -> Format) -> Format
116133
bind f1 f2 = MkFormat { Rep, decode, encode } where
@@ -280,6 +297,14 @@ namespace FormatOf
280297
toFormatOfEq (Element (repeat len f) (cong (Vect len) prf))
281298

282299

300+
public export
301+
pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B)
302+
pair f1 f2 with (toFormatEq f1, toFormatEq f2)
303+
pair _ _ | (Element f1 prf1, Element f2 prf2) =
304+
toFormatOfEq (Element (pair f1 f2)
305+
(rewrite prf1 in rewrite prf2 in Refl))
306+
307+
283308
public export
284309
bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
285310
bind f1 f2 with (toFormatEq f1)

‎experiments/idris/src/Playground.idr‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,7 @@ indRecToIndexed Fail = Indexed.Fail
7070
indRecToIndexed (Pure x) = Indexed.Pure x
7171
indRecToIndexed (Ignore f def) = Indexed.Ignore (indRecToIndexed f) def
7272
indRecToIndexed (Repeat len f) = Indexed.Repeat len (indRecToIndexed f)
73+
indRecToIndexed (Pair f1 f2) = Indexed.Pair (indRecToIndexed f1) (indRecToIndexed f2)
7374
indRecToIndexed (Bind f g) = Indexed.Bind (indRecToIndexed f) (\x => indRecToIndexed (g x))
7475

7576

@@ -84,6 +85,8 @@ mutual
8485
_ | MkFormatOf f' = (Ignore f' def ** Refl)
8586
indexedToIndRecFormat (MkFormat (Vect len _) (Repeat len f)) with (indexedToIndRecFormatOf f)
8687
_ | MkFormatOf f' = (Repeat len f' ** Refl)
88+
indexedToIndRecFormat (MkFormat (_, _) (Pair f1 f2)) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2)
89+
_ | (MkFormatOf f1', MkFormatOf f2') = (Pair f1' f2' ** Refl)
8790
indexedToIndRecFormat (MkFormat (x : _ ** _) (Bind f1 f2)) with (indexedToIndRecFormatOf f1)
8891
_ | MkFormatOf f1' =
8992
(Bind f1' (\x => ?indexedToIndRecFormatBind_f2) ** ?todoBindPrf)
@@ -98,6 +101,8 @@ mutual
98101
_ | MkFormatOf f' = MkFormatOf (Ignore f' def)
99102
indexedToIndRecFormatOf (Repeat len f) with (indexedToIndRecFormatOf f)
100103
_ | MkFormatOf f' = MkFormatOf (Repeat len f')
104+
indexedToIndRecFormatOf (Pair f1 f2) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2)
105+
_ | (MkFormatOf f1', MkFormatOf f2') = MkFormatOf (Pair f1' f2')
101106
indexedToIndRecFormatOf (Bind f1 f2) with (indexedToIndRecFormatOf f1)
102107
_ | MkFormatOf f1' =
103108
-- -- let

‎experiments/idris/src/Playground/OpenType/InductiveRecursive.idr‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -146,6 +146,11 @@ namespace Compile
146146
compileRep (Pure x) =
147147
?todo_compileSingRep -- TODO: interpret an Idris type as a Rust type??
148148
-- perhaps we need to restrict this?
149+
compileRep (Pair f1 f2) =
150+
Just (Rust.Tuple
151+
[ !(compileRep f1)
152+
, !(compileRep f2)
153+
])
149154
compileRep (Bind f1 f2) =
150155
Just (Tuple
151156
[ !(compileRep f1)
@@ -164,6 +169,7 @@ namespace Compile
164169
compileDecode (Pure x) = ?todo_compileDecodePure
165170
compileDecode (Ignore f _) = ?todo_compileDecodeIgnore
166171
compileDecode (Repeat len f) = ?todo_compileDecodeRepeat
172+
compileDecode (Pair f1 f2) = ?todo_compileDecodePair
167173
compileDecode (Bind f1 f2) = ?todo_compileDecodeBind
168174
compileDecode (Custom f) =
169175
-- TODO: f.rustDecode
@@ -176,6 +182,7 @@ namespace Compile
176182
compileEncode (Pure x) = ?todo_compileEncodePure
177183
compileEncode (Ignore f def) = ?todo_compileEncodeIgnore
178184
compileEncode (Repeat len f) = ?todo_compileEncodeRepeat
185+
compileEncode (Pair f1 f2) = ?todo_compileEncodePair
179186
compileEncode (Bind f1 f2) = ?todo_compileEncodeBind
180187
compileEncode (Custom f) =
181188
-- TODO: f.rustEncode

0 commit comments

Comments
 (0)