Play around with heterogeneous sequences

Author: brendanzab

experiments/idris/fathom.ipkg

@@ -27,6 +27,7 @@ modules = Fathom
         , Fathom.Format.Record
 
         , Playground
+        , Playground.HeterogeneousSequences
         , Playground.OpenType.IndexedInductive
         , Playground.OpenType.InductiveRecursive
         , Playground.OpenType.Record

experiments/idris/src/Playground/HeterogeneousSequences.idr

@@ -0,0 +1,43 @@
+-- Heterogeneous sequence example
+
+module Playground.HeterogeneousSequences
+
+
+import Data.Vect
+
+import Fathom.Data.Sing
+import Fathom.Format.Record
+-- import Fathom.Format.InductiveRecursiveCustom
+
+
+namespace Format
+
+  ||| Construct a format based on a type tag
+  value : Nat -> Format
+  value 1 = u8
+  value 2 = u16Be
+  value 4 = u32Be
+  value _ = fail
+
+
+  ||| A heterogeneous sequence of values where the element formats depend on a
+  ||| sequence of type tags
+  values : (ts : Vect len Nat) -> Format
+  values [] = pure ()
+  values (t :: ts) = pair (value t) (values ts)
+
+
+  ||| An annoying example from: https://github.com/yeslogic/fathom/issues/394
+  ouch : Format
+  ouch = do
+    len <- u16Be
+    types <- repeat len u16Be
+    values <- values types
+    pure ()
+
+
+  ||| Access an element at index @i of the in-memory representation of @values.
+  ||| The type of the returned element is dependent on the sequence of type tags.
+  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