From d11c5d47f3f69161ce7377489a2efcafaaf3b4c9 Mon Sep 17 00:00:00 2001 From: brendanzab Date: Sat, 3 Sep 2022 11:07:25 +1000 Subject: [PATCH] Enable applicative notation for decoders --- experiments/idris/src/Fathom/Base.idr | 54 +++++++++++-------- .../src/Fathom/Format/IndexedInductive.idr | 12 ++--- .../Fathom/Format/IndexedInductiveCustom.idr | 12 ++--- .../src/Fathom/Format/InductiveRecursive.idr | 12 ++--- .../Format/InductiveRecursiveCustom.idr | 12 ++--- .../idris/src/Fathom/Format/Record.idr | 14 ++--- 6 files changed, 51 insertions(+), 65 deletions(-) diff --git a/experiments/idris/src/Fathom/Base.idr b/experiments/idris/src/Fathom/Base.idr index d229cf75e..a98ce37b5 100644 --- a/experiments/idris/src/Fathom/Base.idr +++ b/experiments/idris/src/Fathom/Base.idr @@ -73,24 +73,51 @@ parameters (Source, Target : Type) EncodePart = Encode (Source, Target) Target +parameters {0 Source, Target : Type} + + public export + toDecodeFull : (Monoid Target, Eq Target) => DecodePart Source Target -> Decode Source Target + toDecodeFull decode target = Prelude.do + (source, target') <- decode target + if target == neutral then Just source else Nothing + + + public export + toEncodeFull : Monoid Target => EncodePart Source Target -> Encode Source Target + toEncodeFull encode source = encode (source, neutral) + + + public export + toEncodePart : Monoid Target => Encode Source Target -> EncodePart Source Target + toEncodePart encode (source, target) = [| encode source <+> Just target |] + + namespace DecodePart -- TODO: Should probably implement functor, applicative, or monad here. or use -- the reader, writer or state monad transformers + public export + map : {0 S1, S2, T : Type} -> (S1 -> S2) -> DecodePart S1 T -> DecodePart S2 T + map f decode target = + Prelude.map (\(source, target') => (f source, target)) (decode target) + + public export pure : {0 S, T : Type} -> S -> DecodePart S T pure source target = Just (source, target) public export - map : {0 S1, S2, T : Type} -> (S1 -> S2) -> DecodePart S1 T -> DecodePart S2 T - map f decode target = - Prelude.map (\(source, target') => (f source, target)) (decode target) + (<*>) : {0 S1, S2, T : Type} -> DecodePart (S1 -> S2) T -> DecodePart S1 T -> DecodePart S2 T + (<*>) decodeFun decode target = do + (fun, target1) <- decodeFun target + (source, target2) <- decode target1 + Just (fun source, target2) public export - ignore :{0 S, T : Type} -> DecodePart S T -> DecodePart () T + ignore : {0 S, T : Type} -> DecodePart S T -> DecodePart () T ignore = map (const ()) @@ -106,25 +133,6 @@ namespace DecodePart (>>=) = bind -parameters {0 Source, Target : Type} - - public export - toDecodeFull : (Monoid Target, Eq Target) => DecodePart Source Target -> Decode Source Target - toDecodeFull decode target = Prelude.do - (source, target') <- decode target - if target == neutral then Just source else Nothing - - - public export - toEncodeFull : Monoid Target => EncodePart Source Target -> Encode Source Target - toEncodeFull encode source = encode (source, neutral) - - - public export - toEncodePart : Monoid Target => Encode Source Target -> EncodePart Source Target - toEncodePart encode (source, target) = [| encode source <+> Just target |] - - ---------------------- -- ENCODING TARGETS -- ---------------------- diff --git a/experiments/idris/src/Fathom/Format/IndexedInductive.idr b/experiments/idris/src/Fathom/Format/IndexedInductive.idr index d4fd40e59..9e2349d67 100644 --- a/experiments/idris/src/Fathom/Format/IndexedInductive.idr +++ b/experiments/idris/src/Fathom/Format/IndexedInductive.idr @@ -57,14 +57,10 @@ namespace FormatOf decode (Pure x) = pure (MkSing x) decode (Ignore f _) = ignore (decode f) decode (Repeat 0 f) = pure [] - decode (Repeat (S len) f) = do - x <- decode f - xs <- decode (Repeat len f) - pure (x :: xs) - decode (Pair f1 f2) = do - x <- decode f1 - y <- decode f2 - pure (x, y) + decode (Repeat (S len) f) = + [| decode f :: decode (Repeat len f) |] + decode (Pair f1 f2) = + [| (,) (decode f1) (decode f2) |] decode (Bind f1 f2) = do x <- decode f1 y <- decode (f2 x) diff --git a/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr b/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr index 27c1ff0e5..1fc7367f9 100644 --- a/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr +++ b/experiments/idris/src/Fathom/Format/IndexedInductiveCustom.idr @@ -71,14 +71,10 @@ namespace FormatOf decode (Pure x) = pure (MkSing x) decode (Ignore f _) = ignore (decode f) decode (Repeat 0 f) = pure [] - decode (Repeat (S len) f) = do - x <- decode f - xs <- decode (Repeat len f) - pure (x :: xs) - decode (Pair f1 f2) = do - x <- decode f1 - y <- decode f2 - pure (x, y) + decode (Repeat (S len) f) = + [| decode f :: decode (Repeat len f) |] + decode (Pair f1 f2) = + [| (,) (decode f1) (decode f2) |] decode (Bind f1 f2) = do x <- decode f1 y <- decode (f2 x) diff --git a/experiments/idris/src/Fathom/Format/InductiveRecursive.idr b/experiments/idris/src/Fathom/Format/InductiveRecursive.idr index b3c937e96..6c7975dc4 100644 --- a/experiments/idris/src/Fathom/Format/InductiveRecursive.idr +++ b/experiments/idris/src/Fathom/Format/InductiveRecursive.idr @@ -94,14 +94,10 @@ namespace Format decode (Pure x) = pure (MkSing x) decode (Ignore f _) = ignore (decode f) decode (Repeat 0 f) = pure [] - decode (Repeat (S len) f) = do - x <- decode f - xs <- decode (Repeat len f) - pure (x :: xs) - decode (Pair f1 f2) = do - x <- decode f1 - y <- decode f2 - pure (x, y) + decode (Repeat (S len) f) = + [| decode f :: decode (Repeat len f) |] + decode (Pair f1 f2) = + [| (,) (decode f1) (decode f2) |] decode (Bind f1 f2) = do x <- decode f1 y <- decode (f2 x) diff --git a/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr b/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr index 357476348..7d12f330c 100644 --- a/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr +++ b/experiments/idris/src/Fathom/Format/InductiveRecursiveCustom.idr @@ -92,14 +92,10 @@ namespace Format decode (Pure x) = pure (MkSing x) decode (Ignore f _) = ignore (decode f) decode (Repeat 0 f) = pure [] - decode (Repeat (S len) f) = do - x <- decode f - xs <- decode (Repeat len f) - pure (x :: xs) - decode (Pair f1 f2) = do - x <- decode f1 - y <- decode f2 - pure (x, y) + decode (Repeat (S len) f) = + [| decode f :: decode (Repeat len f) |] + decode (Pair f1 f2) = + [| (,) (decode f1) (decode f2) |] decode (Bind f1 f2) = do x <- decode f1 y <- decode (f2 x) diff --git a/experiments/idris/src/Fathom/Format/Record.idr b/experiments/idris/src/Fathom/Format/Record.idr index 20426a116..5a3c986af 100644 --- a/experiments/idris/src/Fathom/Format/Record.idr +++ b/experiments/idris/src/Fathom/Format/Record.idr @@ -98,17 +98,13 @@ namespace Format decode = go len where go : (len : Nat) -> DecodePart (Vect len f.Rep) ByteStream go 0 = pure [] - go (S len) = do - x <- f.decode - xs <- go len - pure (x :: xs) + go (S len) = [| f.decode :: go len |] encode : Encode Rep ByteStream encode = go len where go : (len : Nat) -> Encode (Vect len f.Rep) ByteStream go 0 [] = pure [] - go (S len) (x :: xs) = - [| f.encode x <+> go len xs |] + go (S len) (x :: xs) = [| f.encode x <+> go len xs |] public export @@ -118,10 +114,8 @@ namespace Format Rep = (f1.Rep, f2.Rep) decode : DecodePart Rep ByteStream - decode = do - x <- f1.decode - y <- f2.decode - pure (x, y) + decode = + [| (,) f1.decode f2.decode |] encode : Encode Rep ByteStream encode (x, y) =