Create a hetrogeneous repetition format with HVect

yeslogic · Sep 12, 2022 · 1c37a1c · 1c37a1c
1 parent 1599762
commit 1c37a1c
Show file tree

Hide file tree

Showing 3 changed files with 44 additions and 2 deletions.
diff --git a/experiments/idris/fathom.ipkg b/experiments/idris/fathom.ipkg
@@ -10,7 +10,7 @@ package fathom
 -- bugtracker =
 
 -- packages to add to search path
--- depends =
+depends = contrib
 
 -- modules to install
 modules = Fathom

diff --git a/experiments/idris/src/Fathom/Format/Record.idr b/experiments/idris/src/Fathom/Format/Record.idr
@@ -13,6 +13,7 @@ module Fathom.Format.Record
 
 import Data.Colist
 import Data.DPair
+import Data.HVect
 import Data.Vect
 
 import Fathom.Base
@@ -107,6 +108,25 @@ namespace Format
       go (S len) (x :: xs) = [| f.encode x <+> go len xs |]
 
 
+  public export
+  hrepeat : {len : Nat} -> Vect len Format -> Format
+  hrepeat 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 |]
+
+    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 |]
+
+
   public export
   pair : Format -> Format -> Format
   pair f1 f2 = MkFormat { Rep, decode, encode } where

diff --git a/experiments/idris/src/Playground/HeterogeneousSequences.idr b/experiments/idris/src/Playground/HeterogeneousSequences.idr
@@ -4,13 +4,15 @@ module Playground.HeterogeneousSequences
 
 
 import Data.Vect
+import Data.HVect
 
+import Fathom.Base
 import Fathom.Data.Sing
 import Fathom.Format.Record
 -- import Fathom.Format.InductiveRecursiveCustom
 
 
-namespace Format
+namespace Format.Pairs
 
   ||| Construct a format based on a type tag
   value : Nat -> Format
@@ -41,3 +43,23 @@ namespace Format
   index : {ts : Vect len Nat} -> (i : Fin len) -> (values ts).Rep -> (value (index i ts)).Rep
   index {ts = _ :: _} FZ (x, _) = x
   index {ts = _ :: _} (FS i) (_, xs) = Format.index i xs
+
+
+namespace Format.HRepeat
+
+  ||| Construct a format based on a type tag
+  value : Nat -> Format
+  value 1 = u8
+  value 2 = u16Be
+  value 4 = u32Be
+  value _ = fail
+
+
+  ||| An annoying example from: https://github.com/yeslogic/fathom/issues/394
+  ouch : Format
+  ouch = do
+    len <- u16Be
+    types <- repeat len u16Be
+    values <- hrepeat (map value types)
+    --        ^^^^^^^ heterogeneous repetitions
+    pure ()