Simplify the encoder type

Author: brendanzab

experiments/idris/src/Fathom/Base.idr

@@ -30,16 +30,16 @@ parameters (Source : Type, Target : Type)
   Decode : Type
   Decode = Target -> Maybe (Source, Target)
 
-  ||| Encoders take a _source value_ and _remaining target value_ and produce either:
+  ||| Encoders take a _source value_ and produce either:
   |||
-  ||| - an _updated target value_
+  ||| - a _target value_
   ||| - or nothing if in error occurred
   |||
   ||| @ Source  The type of source values (usually an in-memory data structure)
   ||| @ Target  The type of target values (usually a byte-stream)
   public export
   Encode : Type
-  Encode = Source -> Target -> Maybe Target
+  Encode = Source -> Maybe Target
 
 
 ----------------------

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

@@ -56,17 +56,14 @@ decode (Bind f1 f2) buffer = do
 
 export
 encode : {0 Rep : Type} -> (f : FormatOf Rep) -> Encode Rep (Colist a)
-encode End () _ = Just []
-encode (Pure x) (MkSing _) buffer = Just buffer
-encode (Skip f def) () buffer = do
-  encode f def buffer
-encode (Repeat Z f) [] buffer = Just buffer
-encode (Repeat (S len) f) (x :: xs) buffer = do
-  buffer' <- encode (Repeat len f) xs buffer
-  encode f x buffer'
-encode (Bind f1 f2) (x ** y) buffer = do
-  buffer' <- encode (f2 x) y buffer
-  encode f1 x buffer'
+encode End () = Just []
+encode (Pure x) (MkSing _) = Just []
+encode (Skip f def) () = encode f def
+encode (Repeat Z f) [] = Just []
+encode (Repeat (S len) f) (x :: xs) =
+  [| encode f x <+> encode (Repeat len f) xs |]
+encode (Bind f1 f2) (x ** y) =
+  [| encode f1 x <+> encode (f2 x) y |]
 
 
 -----------------

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

@@ -119,25 +119,22 @@ decode (Bind f1 f2) buffer = do
 
 export
 encode : (f : Format) -> Encode (Rep f) (Colist a)
-encode End () _ = Just []
-encode (Pure x) (MkSing _) buffer = Just buffer
-encode (Skip f def) () buffer = do
-  encode f def buffer
-encode (Repeat Z f) [] buffer = Just buffer
-encode (Repeat (S len) f) (x :: xs) buffer = do
-  buffer' <- encode (Repeat len f) xs buffer
-  encode f x buffer'
-encode (Bind f1 f2) (x ** y) buffer = do
-  buffer' <- encode (f2 x) y buffer
-  encode f1 x buffer'
+encode End () = Just []
+encode (Pure x) (MkSing _) = Just []
+encode (Skip f def) () = encode f def
+encode (Repeat Z f) [] = Just []
+encode (Repeat (S len) f) (x :: xs) = do
+  [| encode f x <+> encode (Repeat len f) xs |]
+encode (Bind f1 f2) (x ** y) = do
+  [| encode f1 x <+> encode (f2 x) y |]
 -- Questionable format descriptions
--- encode (OrPure True f _) x buffer = encode f x buffer
--- encode (OrPure False _ def) x buffer = Just buffer
--- encode (OfSing f r) x buffer = do
---   buffer' <- encode f ?todo_x buffer
+-- encode (OrPure True f _) x = encode f x
+-- encode (OrPure False _ def) x = Just []
+-- encode (OfSing f r) x = do
+--   buffer' <- encode f ?todo_x
 --   ?todo_encode
--- encode (OfEq f _ {prf}) x buffer = do
---   encode f (rewrite prf in x) buffer
+-- encode (OfEq f _ {prf}) x = do
+--   encode f (rewrite prf in x)
 
 
 -----------------

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

@@ -85,18 +85,15 @@ decode (Custom f) buffer = f.decode buffer
 
 export
 encode : (f : Format) -> Encode (Rep f) ByteStream
-encode End () _ = Just []
-encode (Pure x) (MkSing _) buffer = Just buffer
-encode (Skip f def) () buffer = do
-  encode f def buffer
-encode (Repeat Z f) [] buffer = Just buffer
-encode (Repeat (S len) f) (x :: xs) buffer = do
-  buffer' <- encode (Repeat len f) xs buffer
-  encode f x buffer'
-encode (Bind f1 f2) (x ** y) buffer = do
-  buffer' <- encode (f2 x) y buffer
-  encode f1 x buffer'
-encode (Custom f) x buffer = f.encode x buffer
+encode End () = Just []
+encode (Pure x) (MkSing _) = Just []
+encode (Skip f def) () = encode f def
+encode (Repeat Z f) [] = Just []
+encode (Repeat (S len) f) (x :: xs) =
+  [| encode f x <+> encode (Repeat len f) xs |]
+encode (Bind f1 f2) (x ** y) =
+  [| encode f1 x <+> encode (f2 x) y |]
+encode (Custom f) x = f.encode x
 
 
 --------------------
@@ -112,8 +109,7 @@ u8 = Custom (MkCustomFormat
     case buffer of
       [] => Nothing
       x :: buffer => Just (x, buffer)
-  , encode = \x, buffer =>
-    Just (x :: buffer)
+  , encode = \x => Just [x]
   })
 
 

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

@@ -37,7 +37,7 @@ end = MkFormat { Rep, decode, encode } where
   decode (_::_) = Nothing
 
   encode : Encode Rep BitStream
-  encode () _ = Just []
+  encode () = Just []
 
 public export
 fail : Format
@@ -61,7 +61,7 @@ pure x = MkFormat { Rep, decode, encode } where
   decode buffer = Just (MkSing x, buffer)
 
   encode : Encode Rep BitStream
-  encode (MkSing _) buffer = Just buffer
+  encode (MkSing _) = Just []
 
 public export
 skip : (f : Format) -> (def : f.Rep) -> Format
@@ -75,8 +75,7 @@ skip f def = MkFormat { Rep, decode, encode } where
     Just ((), buffer')
 
   encode : Encode Rep BitStream
-  encode () buffer = do
-    f.encode def buffer
+  encode () = f.encode def
 
 
 public export
@@ -97,10 +96,9 @@ repeat len f = MkFormat { Rep, decode, encode } where
   encode : Encode Rep BitStream
   encode = go len where
     go : (len : Nat) -> Encode (Vect len f.Rep) BitStream
-    go 0 [] buffer = Just buffer
-    go (S len) (x :: xs) buffer = do
-      buffer' <- go len xs buffer
-      f.encode x buffer'
+    go 0 [] = Just []
+    go (S len) (x :: xs) =
+      [| f.encode x <+> go len xs |]
 
 
 public export
@@ -116,6 +114,5 @@ bind f1 f2 = MkFormat { Rep, decode, encode } where
     Just ((x ** y), buffer'')
 
   encode : Encode Rep BitStream
-  encode (x ** y) buffer = do
-    buffer' <- (f2 x).encode y buffer
-    f1.encode x buffer'
+  encode (x ** y) =
+    [| f1.encode x <+> (f2 x).encode y |]