Choice formats

experiments/idris/src/Fathom/Base.idr

@@ -133,6 +133,12 @@ namespace DecodePart
   (>>=) = bind
 
 
+  public export
+  (<|>) : {0 S, T : Type} -> DecodePart S T -> Lazy (DecodePart S T) -> DecodePart S T
+  (<|>) decode1 decode2 target =
+    Prelude.(<|>) (decode1 target) (decode2 target)
+
+
 ----------------------
 -- ENCODING TARGETS --
 ----------------------

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

@@ -26,6 +26,7 @@ data FormatOf : Type -> Type where
   Fail : FormatOf Void
   Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
   Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
+  Choice : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (Either A B)
   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)
@@ -58,6 +59,8 @@ namespace FormatOf
   decode Fail = const Nothing
   decode (Pure x) = pure (MkSing x)
   decode (Ignore f _) = ignore (decode f)
+  decode (Choice f1 f2) =
+    [| Left (decode f1) |] <|> [| Right (decode f2) |]
   decode (Repeat 0 f) = pure []
   decode (Repeat (S len) f) =
     [| decode f :: decode (Repeat len f) |]
@@ -81,6 +84,8 @@ namespace FormatOf
   encode End () = pure []
   encode (Pure x) (MkSing _) = pure []
   encode (Ignore f def) () = encode f def
+  encode (Choice f1 f2) (Left x) = encode f1 x
+  encode (Choice f1 f2) (Right y) = encode f2 y
   encode (Repeat Z f) [] = pure []
   encode (Repeat (S len) f) (x :: xs) =
     [| encode f x <+> encode (Repeat len f) xs |]

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

@@ -38,6 +38,7 @@ data FormatOf : (A : Type) -> Type where
   Fail : FormatOf Void
   Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
   Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
+  Choice : {0 A, B : Type} -> FormatOf A -> FormatOf B -> FormatOf (Either A B)
   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)
@@ -71,6 +72,8 @@ namespace FormatOf
   decode Fail = const Nothing
   decode (Pure x) = pure (MkSing x)
   decode (Ignore f _) = ignore (decode f)
+  decode (Choice f1 f2) =
+    [| Left (decode f1) |] <|> [| Right (decode f2) |]
   decode (Repeat 0 f) = pure []
   decode (Repeat (S len) f) =
     [| decode f :: decode (Repeat len f) |]
@@ -95,6 +98,8 @@ namespace FormatOf
   encode End () = pure []
   encode (Pure x) (MkSing _) = pure []
   encode (Ignore f def) () = encode f def
+  encode (Choice f1 f2) (Left x) = encode f1 x
+  encode (Choice f1 f2) (Right y) = encode f2 y
   encode (Repeat Z f) [] = pure []
   encode (Repeat (S len) f) (x :: xs) =
     [| encode f x <+> encode (Repeat len f) xs |]

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

@@ -45,6 +45,7 @@ mutual
     Fail : Format
     Pure : {0 A : Type} -> A -> Format
     Ignore : (f : Format) -> (def : f.Rep) -> Format
+    Choice : Format -> Format -> Format
     Repeat : Nat -> Format -> Format
     Tuple : {0 len : Nat} -> Vect len Format -> Format
     Pair : Format -> Format -> Format
@@ -58,6 +59,7 @@ mutual
   Rep Fail = Void
   Rep (Pure x) = Sing x
   Rep (Ignore _ _) = Unit
+  Rep (Choice f1 f2) = Either f1.Rep f2.Rep
   Rep (Repeat len f) = Vect len f.Rep
   Rep (Tuple fs) = HVect (map (.Rep) fs)
   Rep (Pair f1 f2) = (f1.Rep, f2.Rep)
@@ -96,6 +98,8 @@ namespace Format
   decode Fail = const Nothing
   decode (Pure x) = pure (MkSing x)
   decode (Ignore f _) = ignore (decode f)
+  decode (Choice f1 f2) =
+    [| Left (decode f1) |] <|> [| Right (decode f2) |]
   decode (Repeat 0 f) = pure []
   decode (Repeat (S len) f) =
     [| decode f :: decode (Repeat len f) |]
@@ -115,6 +119,8 @@ namespace Format
   encode End () = pure []
   encode (Pure x) (MkSing _) = pure []
   encode (Ignore f def) () = encode f def
+  encode (Choice f1 f2) (Left x) = encode f1 x
+  encode (Choice f1 f2) (Right y) = encode f2 y
   encode (Repeat Z f) [] = pure []
   encode (Repeat (S len) f) (x :: xs) =
     [| encode f x <+> encode (Repeat len f) xs |]

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

@@ -41,6 +41,7 @@ mutual
     Fail : Format
     Pure : {0 A : Type} -> A -> Format
     Ignore : (f : Format) -> (def : f.Rep) -> Format
+    Choice : Format -> Format -> Format
     Repeat : Nat -> Format -> Format
     Tuple : {0 len : Nat} -> Vect len Format -> Format
     Pair : Format -> Format -> Format
@@ -55,6 +56,7 @@ mutual
   Rep Fail = Void
   Rep (Pure x) = Sing x
   Rep (Ignore _ _) = Unit
+  Rep (Choice f1 f2) = Either f1.Rep f2.Rep
   Rep (Repeat len f) = Vect len f.Rep
   Rep (Tuple fs) = HVect (map (.Rep) fs)
   Rep (Pair f1 f2) = (f1.Rep, f2.Rep)
@@ -94,6 +96,8 @@ namespace Format
   decode Fail = const Nothing
   decode (Pure x) = pure (MkSing x)
   decode (Ignore f _) = ignore (decode f)
+  decode (Choice f1 f2) =
+    [| Left (decode f1) |] <|> [| Right (decode f2) |]
   decode (Repeat 0 f) = pure []
   decode (Repeat (S len) f) =
     [| decode f :: decode (Repeat len f) |]
@@ -114,6 +118,8 @@ namespace Format
   encode End () = pure []
   encode (Pure x) (MkSing _) = pure []
   encode (Ignore f def) () = encode f def
+  encode (Choice f1 f2) (Left x) = encode f1 x
+  encode (Choice f1 f2) (Right y) = encode f2 y
   encode (Repeat Z f) [] = pure []
   encode (Repeat (S len) f) (x :: xs) =
     [| encode f x <+> encode (Repeat len f) xs |]

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

@@ -89,6 +89,21 @@ namespace Format
     encode () = f.encode def
 
 
+  public export
+  choice : Format -> Format -> Format
+  choice f1 f2 = MkFormat { Rep, decode, encode } where
+    Rep : Type
+    Rep = Either f1.Rep f2.Rep
+
+    decode : DecodePart Rep ByteStream
+    decode =
+      [| Left f1.decode |] <|> [| Right f2.decode |]
+
+    encode : Encode Rep ByteStream
+    encode (Left x) = f1.encode x
+    encode (Right y) = f2.encode y
+
+
   public export
   repeat : Nat -> Format -> Format
   repeat len f = MkFormat { Rep, decode, encode } where

experiments/idris/src/Playground.idr

@@ -70,6 +70,7 @@ indRecToIndexed End = Indexed.End
 indRecToIndexed Fail = Indexed.Fail
 indRecToIndexed (Pure x) = Indexed.Pure x
 indRecToIndexed (Ignore f def) = Indexed.Ignore (indRecToIndexed f) def
+indRecToIndexed (Choice f1 f2) = Indexed.Choice (indRecToIndexed f1) (indRecToIndexed f2)
 indRecToIndexed (Repeat len f) = Indexed.Repeat len (indRecToIndexed f)
 indRecToIndexed (Tuple fs) = ?todo_indRecToIndexedTuple
 indRecToIndexed (Pair f1 f2) = Indexed.Pair (indRecToIndexed f1) (indRecToIndexed f2)
@@ -85,6 +86,8 @@ mutual
   indexedToIndRecFormat (MkFormat (Sing x) (Pure x)) = (Pure x ** Refl)
   indexedToIndRecFormat (MkFormat () (Ignore f def)) with (indexedToIndRecFormatOf f)
     _ | MkFormatOf f' = (Ignore f' def ** Refl)
+  indexedToIndRecFormat (MkFormat (Either _ _) (Choice f1 f2)) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2)
+    _ | (MkFormatOf f1', MkFormatOf f2') = (Choice f1' f2' ** Refl)
   indexedToIndRecFormat (MkFormat (Vect len _) (Repeat len f)) with (indexedToIndRecFormatOf f)
     _ | MkFormatOf f' = (Repeat len f' ** Refl)
   indexedToIndRecFormat (MkFormat (HVect reps) (Tuple fs)) =
@@ -103,6 +106,8 @@ mutual
   indexedToIndRecFormatOf (Pure x) = MkFormatOf (Pure x)
   indexedToIndRecFormatOf (Ignore f def) with (indexedToIndRecFormatOf f)
     _ | MkFormatOf f' = MkFormatOf (Ignore f' def)
+  indexedToIndRecFormatOf (Choice f1 f2) with (indexedToIndRecFormatOf f1, indexedToIndRecFormatOf f2)
+    _ | (MkFormatOf f1', MkFormatOf f2') = MkFormatOf (Choice f1' f2')
   indexedToIndRecFormatOf (Repeat len f) with (indexedToIndRecFormatOf f)
     _ | MkFormatOf f' = MkFormatOf (Repeat len f')
   indexedToIndRecFormatOf (Tuple fs) =

experiments/idris/src/Playground/Extraction.idr

@@ -54,6 +54,8 @@ namespace Compile
   compileRep End = Just (Rust.Tuple [])
   compileRep Fail = Just (Rust.Never)
   compileRep (Ignore _ _) = Just (Rust.Tuple [])
+  compileRep (Choice f1 f2) =
+    ?todo_compileRepChoice
   compileRep (Repeat _ f) =
     Just (Rust.Vec !(compileRep f)) -- TODO: Compile to a contract? Or maybe a
                                     --       fixed size array if the length is known
@@ -85,6 +87,7 @@ namespace Compile
   compileDecode Fail = ?todo_compileDecodeFail
   compileDecode (Pure x) = ?todo_compileDecodePure
   compileDecode (Ignore f _) = ?todo_compileDecodeIgnore
+  compileDecode (Choice f1 f2) = ?todo_compileDecodeChoice
   compileDecode (Repeat len f) = ?todo_compileDecodeRepeat
   compileDecode (Tuple fs) = ?todo_compileDecodeTuple
   compileDecode (Pair f1 f2) = ?todo_compileDecodePair
@@ -99,6 +102,7 @@ namespace Compile
   compileEncode Fail = ?todo_compileEncodeFail
   compileEncode (Pure x) = ?todo_compileEncodePure
   compileEncode (Ignore f def) = ?todo_compileEncodeIgnore
+  compileEncode (Choice f1 f2) = ?todo_compileEncodeChoice
   compileEncode (Repeat len f) = ?todo_compileEncodeRepeat
   compileEncode (Tuple fs) = ?todo_compileEncodeTuple
   compileEncode (Pair f1 f2) = ?todo_compileEncodePair