Enable applicative notation for decoders

Author: brendanzab

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 --
 ----------------------

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)

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)

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)

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)

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) =