From 43c8e5025fa22bd8ff5c23b2e274c227dde12dfd Mon Sep 17 00:00:00 2001 From: brendanzab Date: Mon, 12 Sep 2022 17:27:37 +1000 Subject: [PATCH] Implement tuple in other format decription styles --- .../idris/src/Fathom/Format/IndexedInductive.idr | 12 ++++++++++++ .../src/Fathom/Format/IndexedInductiveCustom.idr | 12 ++++++++++++ .../idris/src/Fathom/Format/InductiveRecursive.idr | 11 ++++++++++- .../src/Fathom/Format/InductiveRecursiveCustom.idr | 11 ++++++++++- experiments/idris/src/Playground.idr | 6 ++++++ experiments/idris/src/Playground/Extraction.idr | 4 ++++ 6 files changed, 54 insertions(+), 2 deletions(-) diff --git a/experiments/idris/src/Fathom/Format/IndexedInductive.idr b/experiments/idris/src/Fathom/Format/IndexedInductive.idr index 9e2349d67..ed69d226c 100644 --- a/experiments/idris/src/Fathom/Format/IndexedInductive.idr +++ b/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 : {len : Nat} -> {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) = diff --git a/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr b/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr index 717d11ce0..477349531 100644 --- a/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr +++ b/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 : {len : Nat} -> {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) = diff --git a/experiments/idris/src/Fathom/Format/InductiveRecursive.idr b/experiments/idris/src/Fathom/Format/InductiveRecursive.idr index 6c7975dc4..bd1a51d26 100644 --- a/experiments/idris/src/Fathom/Format/InductiveRecursive.idr +++ b/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 : {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) = diff --git a/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr b/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr index 93c8e7301..aed2a7678 100644 --- a/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr +++ b/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 : {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) = diff --git a/experiments/idris/src/Playground.idr b/experiments/idris/src/Playground.idr index 9dc1983a4..53f086502 100644 --- a/experiments/idris/src/Playground.idr +++ b/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) diff --git a/experiments/idris/src/Playground/Extraction.idr b/experiments/idris/src/Playground/Extraction.idr index 7640700f1..6e3fd79fc 100644 --- a/experiments/idris/src/Playground/Extraction.idr +++ b/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) =