Skip to content

Commit 43c8e50

Browse files
brendanzabbrendanzab
committed
Implement tuple in other format decription styles
1 parent 348f7fd commit 43c8e50

File tree

6 files changed

+54
-2
lines changed

6 files changed

+54
-2
lines changed

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ module Fathom.Format.IndexedInductive
66

77
import Data.Colist
88
import Data.DPair
9+
import Data.HVect
910
import Data.Vect
1011

1112
import Fathom.Base
@@ -26,6 +27,7 @@ data FormatOf : Type -> Type where
2627
Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
2728
Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
2829
Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
30+
Tuple : {len : Nat} -> {reps : Vect len Type} -> HVect (map FormatOf reps) -> FormatOf (HVect reps)
2931
Pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B)
3032
Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
3133

@@ -59,6 +61,13 @@ namespace FormatOf
5961
decode (Repeat 0 f) = pure []
6062
decode (Repeat (S len) f) =
6163
[| decode f :: decode (Repeat len f) |]
64+
decode (Tuple {reps = []} []) = pure []
65+
decode (Tuple {reps = _::_} (f :: fs)) = DecodePart.do
66+
x <- decode f
67+
xs <- decode (Tuple fs)
68+
pure (x :: xs)
69+
-- FIXME: Ambiguous elaboration for some reason??
70+
-- [| decode f :: decode (Tuple fs) |]
6271
decode (Pair f1 f2) =
6372
[| (,) (decode f1) (decode f2) |]
6473
decode (Bind f1 f2) = do
@@ -75,6 +84,9 @@ namespace FormatOf
7584
encode (Repeat Z f) [] = pure []
7685
encode (Repeat (S len) f) (x :: xs) =
7786
[| encode f x <+> encode (Repeat len f) xs |]
87+
encode (Tuple {reps = []} []) [] = pure []
88+
encode (Tuple {reps = _::_} (f :: fs)) (x :: xs) =
89+
[| encode f x <+> encode (Tuple fs) xs |]
7890
encode (Pair f1 f2) (x, y) =
7991
[| encode f1 x <+> encode f2 y |]
8092
encode (Bind f1 f2) (x ** y) =

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ module Fathom.Format.IndexedInductiveCustom
66

77
import Data.Colist
88
import Data.DPair
9+
import Data.HVect
910
import Data.Vect
1011

1112
import Fathom.Base
@@ -38,6 +39,7 @@ data FormatOf : (A : Type) -> Type where
3839
Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
3940
Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
4041
Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
42+
Tuple : {len : Nat} -> {reps : Vect len Type} -> HVect (map FormatOf reps) -> FormatOf (HVect reps)
4143
Pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B)
4244
Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
4345
Custom : {0 A : Type} -> (f : CustomFormatOf A) -> FormatOf A
@@ -72,6 +74,13 @@ namespace FormatOf
7274
decode (Repeat 0 f) = pure []
7375
decode (Repeat (S len) f) =
7476
[| decode f :: decode (Repeat len f) |]
77+
decode (Tuple {reps = []} []) = pure []
78+
decode (Tuple {reps = _::_} (f :: fs)) = DecodePart.do
79+
x <- decode f
80+
xs <- decode (Tuple fs)
81+
pure (x :: xs)
82+
-- FIXME: Ambiguous elaboration for some reason??
83+
-- [| decode f :: decode (Tuple fs) |]
7584
decode (Pair f1 f2) =
7685
[| (,) (decode f1) (decode f2) |]
7786
decode (Bind f1 f2) = do
@@ -89,6 +98,9 @@ namespace FormatOf
8998
encode (Repeat Z f) [] = pure []
9099
encode (Repeat (S len) f) (x :: xs) =
91100
[| encode f x <+> encode (Repeat len f) xs |]
101+
encode (Tuple {reps = []} []) [] = pure []
102+
encode (Tuple {reps = _::_} (f :: fs)) (x :: xs) =
103+
[| encode f x <+> encode (Tuple fs) xs |]
92104
encode (Pair f1 f2) (x, y) =
93105
[| encode f1 x <+> encode f2 y |]
94106
encode (Bind f1 f2) (x ** y) =

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

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ module Fathom.Format.InductiveRecursive
2424

2525
import Data.Colist
2626
import Data.DPair
27+
import Data.HVect
2728
import Data.Vect
2829

2930
import Fathom.Base
@@ -45,6 +46,7 @@ mutual
4546
Pure : {0 A : Type} -> A -> Format
4647
Ignore : (f : Format) -> (def : f.Rep) -> Format
4748
Repeat : Nat -> Format -> Format
49+
Tuple : {len : Nat} -> Vect len Format -> Format
4850
Pair : Format -> Format -> Format
4951
Bind : (f : Format) -> (f.Rep -> Format) -> Format
5052

@@ -54,9 +56,10 @@ mutual
5456
Rep : Format -> Type
5557
Rep End = Unit
5658
Rep Fail = Void
59+
Rep (Pure x) = Sing x
5760
Rep (Ignore _ _) = Unit
5861
Rep (Repeat len f) = Vect len f.Rep
59-
Rep (Pure x) = Sing x
62+
Rep (Tuple fs) = HVect (map (.Rep) fs)
6063
Rep (Pair f1 f2) = (f1.Rep, f2.Rep)
6164
Rep (Bind f1 f2) = (x : f1.Rep ** (f2 x).Rep)
6265

@@ -96,6 +99,9 @@ namespace Format
9699
decode (Repeat 0 f) = pure []
97100
decode (Repeat (S len) f) =
98101
[| decode f :: decode (Repeat len f) |]
102+
decode (Tuple []) = pure []
103+
decode (Tuple (f :: fs)) =
104+
[| decode f :: decode (Tuple fs) |]
99105
decode (Pair f1 f2) =
100106
[| (,) (decode f1) (decode f2) |]
101107
decode (Bind f1 f2) = do
@@ -112,6 +118,9 @@ namespace Format
112118
encode (Repeat Z f) [] = pure []
113119
encode (Repeat (S len) f) (x :: xs) =
114120
[| encode f x <+> encode (Repeat len f) xs |]
121+
encode (Tuple []) [] = pure []
122+
encode (Tuple (f :: fs)) (x :: xs) =
123+
[| encode f x <+> encode (Tuple fs) xs |]
115124
encode (Pair f1 f2) (x, y) =
116125
[| encode f1 x <+> encode f2 y |]
117126
encode (Bind f1 f2) (x ** y) =

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

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module Fathom.Format.InductiveRecursiveCustom
77
import Data.Bits
88
import Data.Colist
99
import Data.DPair
10+
import Data.HVect
1011
import Data.Vect
1112

1213
import Fathom.Base
@@ -41,6 +42,7 @@ mutual
4142
Pure : {0 A : Type} -> A -> Format
4243
Ignore : (f : Format) -> (def : f.Rep) -> Format
4344
Repeat : Nat -> Format -> Format
45+
Tuple : {len : Nat} -> Vect len Format -> Format
4446
Pair : Format -> Format -> Format
4547
Bind : (f : Format) -> (f.Rep -> Format) -> Format
4648
Custom : (f : CustomFormat) -> Format
@@ -51,9 +53,10 @@ mutual
5153
Rep : Format -> Type
5254
Rep End = Unit
5355
Rep Fail = Void
56+
Rep (Pure x) = Sing x
5457
Rep (Ignore _ _) = Unit
5558
Rep (Repeat len f) = Vect len f.Rep
56-
Rep (Pure x) = Sing x
59+
Rep (Tuple fs) = HVect (map (.Rep) fs)
5760
Rep (Pair f1 f2) = (f1.Rep, f2.Rep)
5861
Rep (Bind f1 f2) = (x : f1.Rep ** (f2 x).Rep)
5962
Rep (Custom f) = f.Rep
@@ -94,6 +97,9 @@ namespace Format
9497
decode (Repeat 0 f) = pure []
9598
decode (Repeat (S len) f) =
9699
[| decode f :: decode (Repeat len f) |]
100+
decode (Tuple []) = pure []
101+
decode (Tuple (f :: fs)) =
102+
[| decode f :: decode (Tuple fs) |]
97103
decode (Pair f1 f2) =
98104
[| (,) (decode f1) (decode f2) |]
99105
decode (Bind f1 f2) = do
@@ -111,6 +117,9 @@ namespace Format
111117
encode (Repeat Z f) [] = pure []
112118
encode (Repeat (S len) f) (x :: xs) =
113119
[| encode f x <+> encode (Repeat len f) xs |]
120+
encode (Tuple []) [] = pure []
121+
encode (Tuple (f :: fs)) (x :: xs) =
122+
[| encode f x <+> encode (Tuple fs) xs |]
114123
encode (Pair f1 f2) (x, y) =
115124
[| encode f1 x <+> encode f2 y |]
116125
encode (Bind f1 f2) (x ** y) =

‎experiments/idris/src/Playground.idr‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ module Playground
33

44
import Data.Colist
55
import Data.Vect
6+
import Data.HVect
67

78
import Fathom.Base
89
import Fathom.Data.Sing
@@ -70,6 +71,7 @@ indRecToIndexed Fail = Indexed.Fail
7071
indRecToIndexed (Pure x) = Indexed.Pure x
7172
indRecToIndexed (Ignore f def) = Indexed.Ignore (indRecToIndexed f) def
7273
indRecToIndexed (Repeat len f) = Indexed.Repeat len (indRecToIndexed f)
74+
indRecToIndexed (Tuple fs) = ?todo_indRecToIndexedTuple
7375
indRecToIndexed (Pair f1 f2) = Indexed.Pair (indRecToIndexed f1) (indRecToIndexed f2)
7476
indRecToIndexed (Bind f g) = Indexed.Bind (indRecToIndexed f) (\x => indRecToIndexed (g x))
7577

@@ -85,6 +87,8 @@ mutual
8587
_ | MkFormatOf f' = (Ignore f' def ** Refl)
8688
indexedToIndRecFormat (MkFormat (Vect len _) (Repeat len f)) with (indexedToIndRecFormatOf f)
8789
_ | MkFormatOf f' = (Repeat len f' ** Refl)
90+
indexedToIndRecFormat (MkFormat (HVect reps) (Tuple fs)) =
91+
?todo_indexedToIndRecFormatTuple
8892
indexedToIndRecFormat (MkFormat (_, _) (Pair f1 f2)) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2)
8993
_ | (MkFormatOf f1', MkFormatOf f2') = (Pair f1' f2' ** Refl)
9094
indexedToIndRecFormat (MkFormat (x : _ ** _) (Bind f1 f2)) with (indexedToIndRecFormatOf f1)
@@ -101,6 +105,8 @@ mutual
101105
_ | MkFormatOf f' = MkFormatOf (Ignore f' def)
102106
indexedToIndRecFormatOf (Repeat len f) with (indexedToIndRecFormatOf f)
103107
_ | MkFormatOf f' = MkFormatOf (Repeat len f')
108+
indexedToIndRecFormatOf (Tuple fs) =
109+
?todo_indexedToIndRecFormatOfTuple
104110
indexedToIndRecFormatOf (Pair f1 f2) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2)
105111
_ | (MkFormatOf f1', MkFormatOf f2') = MkFormatOf (Pair f1' f2')
106112
indexedToIndRecFormatOf (Bind f1 f2) with (indexedToIndRecFormatOf f1)

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,8 @@ namespace Compile
5858
Just (Rust.Vec !(compileRep f)) -- TODO: Compile to a contract? Or maybe a
5959
-- fixed size array if the length is known
6060
-- or just throw away the info
61+
compileRep (Tuple fs) =
62+
?todo_compileRepTuple
6163
compileRep (Pure x) =
6264
?todo_compileSingRep -- TODO: interpret an Idris type as a Rust type??
6365
-- perhaps we need to restrict this?
@@ -84,6 +86,7 @@ namespace Compile
8486
compileDecode (Pure x) = ?todo_compileDecodePure
8587
compileDecode (Ignore f _) = ?todo_compileDecodeIgnore
8688
compileDecode (Repeat len f) = ?todo_compileDecodeRepeat
89+
compileDecode (Tuple fs) = ?todo_compileDecodeTuple
8790
compileDecode (Pair f1 f2) = ?todo_compileDecodePair
8891
compileDecode (Bind f1 f2) = ?todo_compileDecodeBind
8992
compileDecode (Custom f) =
@@ -97,6 +100,7 @@ namespace Compile
97100
compileEncode (Pure x) = ?todo_compileEncodePure
98101
compileEncode (Ignore f def) = ?todo_compileEncodeIgnore
99102
compileEncode (Repeat len f) = ?todo_compileEncodeRepeat
103+
compileEncode (Tuple fs) = ?todo_compileEncodeTuple
100104
compileEncode (Pair f1 f2) = ?todo_compileEncodePair
101105
compileEncode (Bind f1 f2) = ?todo_compileEncodeBind
102106
compileEncode (Custom f) =

0 commit comments

Comments
 (0)