From bac57891602c03fadb81a1ddc8755d02da58bf6f Mon Sep 17 00:00:00 2001 From: brendanzab Date: Tue, 13 Sep 2022 11:10:51 +1000 Subject: [PATCH] Choice formats --- experiments/idris/src/Fathom/Base.idr | 6 ++++++ .../idris/src/Fathom/Format/IndexedInductive.idr | 5 +++++ .../src/Fathom/Format/IndexedInductiveCustom.idr | 5 +++++ .../src/Fathom/Format/InductiveRecursive.idr | 6 ++++++ .../Fathom/Format/InductiveRecursiveCustom.idr | 6 ++++++ experiments/idris/src/Fathom/Format/Record.idr | 15 +++++++++++++++ experiments/idris/src/Playground.idr | 5 +++++ experiments/idris/src/Playground/Extraction.idr | 4 ++++ 8 files changed, 52 insertions(+) diff --git a/experiments/idris/src/Fathom/Base.idr b/experiments/idris/src/Fathom/Base.idr index a98ce37b5..298246392 100644 --- a/experiments/idris/src/Fathom/Base.idr +++ b/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 -- ---------------------- diff --git a/experiments/idris/src/Fathom/Format/IndexedInductive.idr b/experiments/idris/src/Fathom/Format/IndexedInductive.idr index 92d1c2eaa..f20dc19ac 100644 --- a/experiments/idris/src/Fathom/Format/IndexedInductive.idr +++ b/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 |] diff --git a/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr b/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr index 895db3853..72c035bb3 100644 --- a/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr +++ b/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 |] diff --git a/experiments/idris/src/Fathom/Format/InductiveRecursive.idr b/experiments/idris/src/Fathom/Format/InductiveRecursive.idr index b2c6458ff..336fb8d71 100644 --- a/experiments/idris/src/Fathom/Format/InductiveRecursive.idr +++ b/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 |] diff --git a/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr b/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr index 3a624640e..ec24f85f6 100644 --- a/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr +++ b/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 |] diff --git a/experiments/idris/src/Fathom/Format/Record.idr b/experiments/idris/src/Fathom/Format/Record.idr index 34f7d00bb..8e033a116 100644 --- a/experiments/idris/src/Fathom/Format/Record.idr +++ b/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 diff --git a/experiments/idris/src/Playground.idr b/experiments/idris/src/Playground.idr index 53f086502..6f56d8a4f 100644 --- a/experiments/idris/src/Playground.idr +++ b/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) = diff --git a/experiments/idris/src/Playground/Extraction.idr b/experiments/idris/src/Playground/Extraction.idr index 6e3fd79fc..75e0c99e0 100644 --- a/experiments/idris/src/Playground/Extraction.idr +++ b/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