Skip to content

Commit bac5789

Browse files
brendanzabbrendanzab
committed
Choice formats
1 parent 1cc1602 commit bac5789

File tree

8 files changed

+52
-0
lines changed

8 files changed

+52
-0
lines changed

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -133,6 +133,12 @@ namespace DecodePart
133133
(>>=) = bind
134134

135135

136+
public export
137+
(<|>) : {0 S, T : Type} -> DecodePart S T -> Lazy (DecodePart S T) -> DecodePart S T
138+
(<|>) decode1 decode2 target =
139+
Prelude.(<|>) (decode1 target) (decode2 target)
140+
141+
136142
----------------------
137143
-- ENCODING TARGETS --
138144
----------------------

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ data FormatOf : Type -> Type where
2626
Fail : FormatOf Void
2727
Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
2828
Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
29+
Choice : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (Either A B)
2930
Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
3031
Tuple : {reps : Vect len Type} -> HVect (map FormatOf reps) -> FormatOf (HVect reps)
3132
Pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B)
@@ -58,6 +59,8 @@ namespace FormatOf
5859
decode Fail = const Nothing
5960
decode (Pure x) = pure (MkSing x)
6061
decode (Ignore f _) = ignore (decode f)
62+
decode (Choice f1 f2) =
63+
[| Left (decode f1) |] <|> [| Right (decode f2) |]
6164
decode (Repeat 0 f) = pure []
6265
decode (Repeat (S len) f) =
6366
[| decode f :: decode (Repeat len f) |]
@@ -81,6 +84,8 @@ namespace FormatOf
8184
encode End () = pure []
8285
encode (Pure x) (MkSing _) = pure []
8386
encode (Ignore f def) () = encode f def
87+
encode (Choice f1 f2) (Left x) = encode f1 x
88+
encode (Choice f1 f2) (Right y) = encode f2 y
8489
encode (Repeat Z f) [] = pure []
8590
encode (Repeat (S len) f) (x :: xs) =
8691
[| encode f x <+> encode (Repeat len f) xs |]

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ data FormatOf : (A : Type) -> Type where
3838
Fail : FormatOf Void
3939
Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
4040
Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
41+
Choice : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (Either A B)
4142
Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
4243
Tuple : {reps : Vect len Type} -> HVect (map FormatOf reps) -> FormatOf (HVect reps)
4344
Pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B)
@@ -71,6 +72,8 @@ namespace FormatOf
7172
decode Fail = const Nothing
7273
decode (Pure x) = pure (MkSing x)
7374
decode (Ignore f _) = ignore (decode f)
75+
decode (Choice f1 f2) =
76+
[| Left (decode f1) |] <|> [| Right (decode f2) |]
7477
decode (Repeat 0 f) = pure []
7578
decode (Repeat (S len) f) =
7679
[| decode f :: decode (Repeat len f) |]
@@ -95,6 +98,8 @@ namespace FormatOf
9598
encode End () = pure []
9699
encode (Pure x) (MkSing _) = pure []
97100
encode (Ignore f def) () = encode f def
101+
encode (Choice f1 f2) (Left x) = encode f1 x
102+
encode (Choice f1 f2) (Right y) = encode f2 y
98103
encode (Repeat Z f) [] = pure []
99104
encode (Repeat (S len) f) (x :: xs) =
100105
[| encode f x <+> encode (Repeat len f) xs |]

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ mutual
4545
Fail : Format
4646
Pure : {0 A : Type} -> A -> Format
4747
Ignore : (f : Format) -> (def : f.Rep) -> Format
48+
Choice : Format -> Format -> Format
4849
Repeat : Nat -> Format -> Format
4950
Tuple : {0 len : Nat} -> Vect len Format -> Format
5051
Pair : Format -> Format -> Format
@@ -58,6 +59,7 @@ mutual
5859
Rep Fail = Void
5960
Rep (Pure x) = Sing x
6061
Rep (Ignore _ _) = Unit
62+
Rep (Choice f1 f2) = Either f1.Rep f2.Rep
6163
Rep (Repeat len f) = Vect len f.Rep
6264
Rep (Tuple fs) = HVect (map (.Rep) fs)
6365
Rep (Pair f1 f2) = (f1.Rep, f2.Rep)
@@ -96,6 +98,8 @@ namespace Format
9698
decode Fail = const Nothing
9799
decode (Pure x) = pure (MkSing x)
98100
decode (Ignore f _) = ignore (decode f)
101+
decode (Choice f1 f2) =
102+
[| Left (decode f1) |] <|> [| Right (decode f2) |]
99103
decode (Repeat 0 f) = pure []
100104
decode (Repeat (S len) f) =
101105
[| decode f :: decode (Repeat len f) |]
@@ -115,6 +119,8 @@ namespace Format
115119
encode End () = pure []
116120
encode (Pure x) (MkSing _) = pure []
117121
encode (Ignore f def) () = encode f def
122+
encode (Choice f1 f2) (Left x) = encode f1 x
123+
encode (Choice f1 f2) (Right y) = encode f2 y
118124
encode (Repeat Z f) [] = pure []
119125
encode (Repeat (S len) f) (x :: xs) =
120126
[| encode f x <+> encode (Repeat len f) xs |]

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,7 @@ mutual
4141
Fail : Format
4242
Pure : {0 A : Type} -> A -> Format
4343
Ignore : (f : Format) -> (def : f.Rep) -> Format
44+
Choice : Format -> Format -> Format
4445
Repeat : Nat -> Format -> Format
4546
Tuple : {0 len : Nat} -> Vect len Format -> Format
4647
Pair : Format -> Format -> Format
@@ -55,6 +56,7 @@ mutual
5556
Rep Fail = Void
5657
Rep (Pure x) = Sing x
5758
Rep (Ignore _ _) = Unit
59+
Rep (Choice f1 f2) = Either f1.Rep f2.Rep
5860
Rep (Repeat len f) = Vect len f.Rep
5961
Rep (Tuple fs) = HVect (map (.Rep) fs)
6062
Rep (Pair f1 f2) = (f1.Rep, f2.Rep)
@@ -94,6 +96,8 @@ namespace Format
9496
decode Fail = const Nothing
9597
decode (Pure x) = pure (MkSing x)
9698
decode (Ignore f _) = ignore (decode f)
99+
decode (Choice f1 f2) =
100+
[| Left (decode f1) |] <|> [| Right (decode f2) |]
97101
decode (Repeat 0 f) = pure []
98102
decode (Repeat (S len) f) =
99103
[| decode f :: decode (Repeat len f) |]
@@ -114,6 +118,8 @@ namespace Format
114118
encode End () = pure []
115119
encode (Pure x) (MkSing _) = pure []
116120
encode (Ignore f def) () = encode f def
121+
encode (Choice f1 f2) (Left x) = encode f1 x
122+
encode (Choice f1 f2) (Right y) = encode f2 y
117123
encode (Repeat Z f) [] = pure []
118124
encode (Repeat (S len) f) (x :: xs) =
119125
[| encode f x <+> encode (Repeat len f) xs |]

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,21 @@ namespace Format
8989
encode () = f.encode def
9090

9191

92+
public export
93+
choice : Format -> Format -> Format
94+
choice f1 f2 = MkFormat { Rep, decode, encode } where
95+
Rep : Type
96+
Rep = Either f1.Rep f2.Rep
97+
98+
decode : DecodePart Rep ByteStream
99+
decode =
100+
[| Left f1.decode |] <|> [| Right f2.decode |]
101+
102+
encode : Encode Rep ByteStream
103+
encode (Left x) = f1.encode x
104+
encode (Right y) = f2.encode y
105+
106+
92107
public export
93108
repeat : Nat -> Format -> Format
94109
repeat len f = MkFormat { Rep, decode, encode } where

‎experiments/idris/src/Playground.idr‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,7 @@ indRecToIndexed End = Indexed.End
7070
indRecToIndexed Fail = Indexed.Fail
7171
indRecToIndexed (Pure x) = Indexed.Pure x
7272
indRecToIndexed (Ignore f def) = Indexed.Ignore (indRecToIndexed f) def
73+
indRecToIndexed (Choice f1 f2) = Indexed.Choice (indRecToIndexed f1) (indRecToIndexed f2)
7374
indRecToIndexed (Repeat len f) = Indexed.Repeat len (indRecToIndexed f)
7475
indRecToIndexed (Tuple fs) = ?todo_indRecToIndexedTuple
7576
indRecToIndexed (Pair f1 f2) = Indexed.Pair (indRecToIndexed f1) (indRecToIndexed f2)
@@ -85,6 +86,8 @@ mutual
8586
indexedToIndRecFormat (MkFormat (Sing x) (Pure x)) = (Pure x ** Refl)
8687
indexedToIndRecFormat (MkFormat () (Ignore f def)) with (indexedToIndRecFormatOf f)
8788
_ | MkFormatOf f' = (Ignore f' def ** Refl)
89+
indexedToIndRecFormat (MkFormat (Either _ _) (Choice f1 f2)) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2)
90+
_ | (MkFormatOf f1', MkFormatOf f2') = (Choice f1' f2' ** Refl)
8891
indexedToIndRecFormat (MkFormat (Vect len _) (Repeat len f)) with (indexedToIndRecFormatOf f)
8992
_ | MkFormatOf f' = (Repeat len f' ** Refl)
9093
indexedToIndRecFormat (MkFormat (HVect reps) (Tuple fs)) =
@@ -103,6 +106,8 @@ mutual
103106
indexedToIndRecFormatOf (Pure x) = MkFormatOf (Pure x)
104107
indexedToIndRecFormatOf (Ignore f def) with (indexedToIndRecFormatOf f)
105108
_ | MkFormatOf f' = MkFormatOf (Ignore f' def)
109+
indexedToIndRecFormatOf (Choice f1 f2) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2)
110+
_ | (MkFormatOf f1', MkFormatOf f2') = MkFormatOf (Choice f1' f2')
106111
indexedToIndRecFormatOf (Repeat len f) with (indexedToIndRecFormatOf f)
107112
_ | MkFormatOf f' = MkFormatOf (Repeat len f')
108113
indexedToIndRecFormatOf (Tuple fs) =

‎experiments/idris/src/Playground/Extraction.idr‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,8 @@ namespace Compile
5454
compileRep End = Just (Rust.Tuple [])
5555
compileRep Fail = Just (Rust.Never)
5656
compileRep (Ignore _ _) = Just (Rust.Tuple [])
57+
compileRep (Choice f1 f2) =
58+
?todo_compileRepChoice
5759
compileRep (Repeat _ f) =
5860
Just (Rust.Vec !(compileRep f)) -- TODO: Compile to a contract? Or maybe a
5961
-- fixed size array if the length is known
@@ -85,6 +87,7 @@ namespace Compile
8587
compileDecode Fail = ?todo_compileDecodeFail
8688
compileDecode (Pure x) = ?todo_compileDecodePure
8789
compileDecode (Ignore f _) = ?todo_compileDecodeIgnore
90+
compileDecode (Choice f1 f2) = ?todo_compileDecodeChoice
8891
compileDecode (Repeat len f) = ?todo_compileDecodeRepeat
8992
compileDecode (Tuple fs) = ?todo_compileDecodeTuple
9093
compileDecode (Pair f1 f2) = ?todo_compileDecodePair
@@ -99,6 +102,7 @@ namespace Compile
99102
compileEncode Fail = ?todo_compileEncodeFail
100103
compileEncode (Pure x) = ?todo_compileEncodePure
101104
compileEncode (Ignore f def) = ?todo_compileEncodeIgnore
105+
compileEncode (Choice f1 f2) = ?todo_compileEncodeChoice
102106
compileEncode (Repeat len f) = ?todo_compileEncodeRepeat
103107
compileEncode (Tuple fs) = ?todo_compileEncodeTuple
104108
compileEncode (Pair f1 f2) = ?todo_compileEncodePair

0 commit comments

Comments
 (0)