Implement tuple in other format decription styles

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

@@ -6,6 +6,7 @@ module Fathom.Format.IndexedInductive
 
 import Data.Colist
 import Data.DPair
+import Data.HVect
 import Data.Vect
 
 import Fathom.Base
@@ -26,6 +27,7 @@ data FormatOf : Type -> Type where
   Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
   Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
   Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
+  Tuple : {reps : Vect len Type} -> HVect (map FormatOf reps) -> FormatOf (HVect reps)
   Pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B)
   Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
 
@@ -59,6 +61,13 @@ namespace FormatOf
   decode (Repeat 0 f) = pure []
   decode (Repeat (S len) f) =
     [| decode f :: decode (Repeat len f) |]
+  decode (Tuple {reps = []} []) = pure []
+  decode (Tuple {reps = _::_} (f :: fs)) = DecodePart.do
+    x <- decode f
+    xs <- decode (Tuple fs)
+    pure (x :: xs)
+    -- FIXME: Ambiguous elaboration for some reason??
+    -- [| decode f :: decode (Tuple fs) |]
   decode (Pair f1 f2) =
     [| (,) (decode f1) (decode f2) |]
   decode (Bind f1 f2) = do
@@ -75,6 +84,9 @@ namespace FormatOf
   encode (Repeat Z f) [] = pure []
   encode (Repeat (S len) f) (x :: xs) =
     [| encode f x <+> encode (Repeat len f) xs |]
+  encode (Tuple {reps = []} []) [] = pure []
+  encode (Tuple {reps = _::_} (f :: fs)) (x :: xs) =
+    [| encode f x <+> encode (Tuple fs) xs |]
   encode (Pair f1 f2) (x, y) =
     [| encode f1 x <+> encode f2 y |]
   encode (Bind f1 f2) (x ** y) =

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

@@ -6,6 +6,7 @@ module Fathom.Format.IndexedInductiveCustom
 
 import Data.Colist
 import Data.DPair
+import Data.HVect
 import Data.Vect
 
 import Fathom.Base
@@ -38,6 +39,7 @@ data FormatOf : (A : Type) -> Type where
   Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
   Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
   Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
+  Tuple : {reps : Vect len Type} -> HVect (map FormatOf reps) -> FormatOf (HVect reps)
   Pair : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (A, B)
   Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
   Custom :  {0 A : Type} -> (f : CustomFormatOf A) -> FormatOf A
@@ -72,6 +74,13 @@ namespace FormatOf
   decode (Repeat 0 f) = pure []
   decode (Repeat (S len) f) =
     [| decode f :: decode (Repeat len f) |]
+  decode (Tuple {reps = []} []) = pure []
+  decode (Tuple {reps = _::_} (f :: fs)) = DecodePart.do
+    x <- decode f
+    xs <- decode (Tuple fs)
+    pure (x :: xs)
+    -- FIXME: Ambiguous elaboration for some reason??
+    -- [| decode f :: decode (Tuple fs) |]
   decode (Pair f1 f2) =
     [| (,) (decode f1) (decode f2) |]
   decode (Bind f1 f2) = do
@@ -89,6 +98,9 @@ namespace FormatOf
   encode (Repeat Z f) [] = pure []
   encode (Repeat (S len) f) (x :: xs) =
     [| encode f x <+> encode (Repeat len f) xs |]
+  encode (Tuple {reps = []} []) [] = pure []
+  encode (Tuple {reps = _::_} (f :: fs)) (x :: xs) =
+    [| encode f x <+> encode (Tuple fs) xs |]
   encode (Pair f1 f2) (x, y) =
     [| encode f1 x <+> encode f2 y |]
   encode (Bind f1 f2) (x ** y) =

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

@@ -24,6 +24,7 @@ module Fathom.Format.InductiveRecursive
 
 import Data.Colist
 import Data.DPair
+import Data.HVect
 import Data.Vect
 
 import Fathom.Base
@@ -45,6 +46,7 @@ mutual
     Pure : {0 A : Type} -> A -> Format
     Ignore : (f : Format) -> (def : f.Rep) -> Format
     Repeat : Nat -> Format -> Format
+    Tuple : {0 len : Nat} -> Vect len Format -> Format
     Pair : Format -> Format -> Format
     Bind : (f : Format) -> (f.Rep -> Format) -> Format
 
@@ -54,9 +56,10 @@ mutual
   Rep : Format -> Type
   Rep End = Unit
   Rep Fail = Void
+  Rep (Pure x) = Sing x
   Rep (Ignore _ _) = Unit
   Rep (Repeat len f) = Vect len f.Rep
-  Rep (Pure x) = Sing x
+  Rep (Tuple fs) = HVect (map (.Rep) fs)
   Rep (Pair f1 f2) = (f1.Rep, f2.Rep)
   Rep (Bind f1 f2) = (x : f1.Rep ** (f2 x).Rep)
 
@@ -96,6 +99,9 @@ namespace Format
   decode (Repeat 0 f) = pure []
   decode (Repeat (S len) f) =
     [| decode f :: decode (Repeat len f) |]
+  decode (Tuple []) = pure []
+  decode (Tuple (f :: fs)) =
+    [| decode f :: decode (Tuple fs) |]
   decode (Pair f1 f2) =
     [| (,) (decode f1) (decode f2) |]
   decode (Bind f1 f2) = do
@@ -112,6 +118,9 @@ namespace Format
   encode (Repeat Z f) [] = pure []
   encode (Repeat (S len) f) (x :: xs) =
     [| encode f x <+> encode (Repeat len f) xs |]
+  encode (Tuple []) [] = pure []
+  encode (Tuple (f :: fs)) (x :: xs) =
+    [| encode f x <+> encode (Tuple fs) xs |]
   encode (Pair f1 f2) (x, y) =
     [| encode f1 x <+> encode f2 y |]
   encode (Bind f1 f2) (x ** y) =

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

@@ -7,6 +7,7 @@ module Fathom.Format.InductiveRecursiveCustom
 import Data.Bits
 import Data.Colist
 import Data.DPair
+import Data.HVect
 import Data.Vect
 
 import Fathom.Base
@@ -41,6 +42,7 @@ mutual
     Pure : {0 A : Type} -> A -> Format
     Ignore : (f : Format) -> (def : f.Rep) -> Format
     Repeat : Nat -> Format -> Format
+    Tuple : {0 len : Nat} -> Vect len Format -> Format
     Pair : Format -> Format -> Format
     Bind : (f : Format) -> (f.Rep -> Format) -> Format
     Custom :  (f : CustomFormat) -> Format
@@ -51,9 +53,10 @@ mutual
   Rep : Format -> Type
   Rep End = Unit
   Rep Fail = Void
+  Rep (Pure x) = Sing x
   Rep (Ignore _ _) = Unit
   Rep (Repeat len f) = Vect len f.Rep
-  Rep (Pure x) = Sing x
+  Rep (Tuple fs) = HVect (map (.Rep) fs)
   Rep (Pair f1 f2) = (f1.Rep, f2.Rep)
   Rep (Bind f1 f2) = (x : f1.Rep ** (f2 x).Rep)
   Rep (Custom f) = f.Rep
@@ -94,6 +97,9 @@ namespace Format
   decode (Repeat 0 f) = pure []
   decode (Repeat (S len) f) =
     [| decode f :: decode (Repeat len f) |]
+  decode (Tuple []) = pure []
+  decode (Tuple (f :: fs)) =
+    [| decode f :: decode (Tuple fs) |]
   decode (Pair f1 f2) =
     [| (,) (decode f1) (decode f2) |]
   decode (Bind f1 f2) = do
@@ -111,6 +117,9 @@ namespace Format
   encode (Repeat Z f) [] = pure []
   encode (Repeat (S len) f) (x :: xs) =
     [| encode f x <+> encode (Repeat len f) xs |]
+  encode (Tuple []) [] = pure []
+  encode (Tuple (f :: fs)) (x :: xs) =
+    [| encode f x <+> encode (Tuple fs) xs |]
   encode (Pair f1 f2) (x, y) =
     [| encode f1 x <+> encode f2 y |]
   encode (Bind f1 f2) (x ** y) =

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

@@ -109,22 +109,22 @@ namespace Format
 
 
   public export
-  tuple : {len : Nat} -> Vect len Format -> Format
+  tuple : {0 len : Nat} -> Vect len Format -> Format
   tuple fs = MkFormat { Rep, decode, encode } where
     Rep : Type
     Rep = HVect (map (.Rep) fs)
 
     decode : DecodePart Rep ByteStream
     decode = go fs where
-      go : {len : Nat} -> (fs : Vect len Format) -> DecodePart (HVect (map (.Rep) fs)) ByteStream
-      go {len = Z} [] = pure []
-      go {len = S _} (f :: fs) = [| f.decode :: go fs |]
+      go : {0 len : Nat} -> (fs : Vect len Format) -> DecodePart (HVect (map (.Rep) fs)) ByteStream
+      go [] = pure []
+      go (f :: fs) = [| f.decode :: go fs |]
 
     encode : Encode Rep ByteStream
     encode = go fs where
-      go : {len : Nat} -> (fs : Vect len Format) -> Encode (HVect (map (.Rep) fs)) ByteStream
-      go {len = Z} [] [] = pure []
-      go {len = S _} (f :: fs) (x :: xs) = [| f.encode x <+> go fs xs |]
+      go : {0 len : Nat} -> (fs : Vect len Format) -> Encode (HVect (map (.Rep) fs)) ByteStream
+      go [] [] = pure []
+      go (f :: fs) (x :: xs) = [| f.encode x <+> go fs xs |]
 
 
   public export

experiments/idris/src/Playground.idr

@@ -3,6 +3,7 @@ module Playground
 
 import Data.Colist
 import Data.Vect
+import Data.HVect
 
 import Fathom.Base
 import Fathom.Data.Sing
@@ -70,6 +71,7 @@ indRecToIndexed Fail = Indexed.Fail
 indRecToIndexed (Pure x) = Indexed.Pure x
 indRecToIndexed (Ignore f def) = Indexed.Ignore (indRecToIndexed f) def
 indRecToIndexed (Repeat len f) = Indexed.Repeat len (indRecToIndexed f)
+indRecToIndexed (Tuple fs) = ?todo_indRecToIndexedTuple
 indRecToIndexed (Pair f1 f2) = Indexed.Pair (indRecToIndexed f1) (indRecToIndexed f2)
 indRecToIndexed (Bind f g) = Indexed.Bind (indRecToIndexed f) (\x => indRecToIndexed (g x))
 
@@ -85,6 +87,8 @@ mutual
     _ | MkFormatOf f' = (Ignore f' def ** Refl)
   indexedToIndRecFormat (MkFormat (Vect len _) (Repeat len f)) with (indexedToIndRecFormatOf f)
     _ | MkFormatOf f' = (Repeat len f' ** Refl)
+  indexedToIndRecFormat (MkFormat (HVect reps) (Tuple fs)) =
+    ?todo_indexedToIndRecFormatTuple
   indexedToIndRecFormat (MkFormat (_, _) (Pair f1 f2)) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2)
     _ | (MkFormatOf f1', MkFormatOf f2') = (Pair f1' f2' ** Refl)
   indexedToIndRecFormat (MkFormat (x : _ ** _) (Bind f1 f2)) with (indexedToIndRecFormatOf f1)
@@ -101,6 +105,8 @@ mutual
     _ | MkFormatOf f' = MkFormatOf (Ignore f' def)
   indexedToIndRecFormatOf (Repeat len f) with (indexedToIndRecFormatOf f)
     _ | MkFormatOf f' = MkFormatOf (Repeat len f')
+  indexedToIndRecFormatOf (Tuple fs) =
+    ?todo_indexedToIndRecFormatOfTuple
   indexedToIndRecFormatOf (Pair f1 f2) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2)
     _ | (MkFormatOf f1', MkFormatOf f2') = MkFormatOf (Pair f1' f2')
   indexedToIndRecFormatOf (Bind f1 f2) with (indexedToIndRecFormatOf f1)

experiments/idris/src/Playground/Extraction.idr

@@ -58,6 +58,8 @@ namespace Compile
     Just (Rust.Vec !(compileRep f)) -- TODO: Compile to a contract? Or maybe a
                                     --       fixed size array if the length is known
                                     --       or just throw away the info
+  compileRep (Tuple fs) =
+    ?todo_compileRepTuple
   compileRep (Pure x) =
     ?todo_compileSingRep -- TODO: interpret an Idris type as a Rust type??
                          --       perhaps we need to restrict this?
@@ -84,6 +86,7 @@ namespace Compile
   compileDecode (Pure x) = ?todo_compileDecodePure
   compileDecode (Ignore f _) = ?todo_compileDecodeIgnore
   compileDecode (Repeat len f) = ?todo_compileDecodeRepeat
+  compileDecode (Tuple fs) = ?todo_compileDecodeTuple
   compileDecode (Pair f1 f2) = ?todo_compileDecodePair
   compileDecode (Bind f1 f2) = ?todo_compileDecodeBind
   compileDecode (Custom f) =
@@ -97,6 +100,7 @@ namespace Compile
   compileEncode (Pure x) = ?todo_compileEncodePure
   compileEncode (Ignore f def) = ?todo_compileEncodeIgnore
   compileEncode (Repeat len f) = ?todo_compileEncodeRepeat
+  compileEncode (Tuple fs) = ?todo_compileEncodeTuple
   compileEncode (Pair f1 f2) = ?todo_compileEncodePair
   compileEncode (Bind f1 f2) = ?todo_compileEncodeBind
   compileEncode (Custom f) =