Add more type aliases for encoder/decoder pairs

Author: brendanzab

experiments/idris/src/Fathom/Base.idr

@@ -17,18 +17,20 @@ import Data.List
 --
 -- TODO: Add support for [Narcissus-style stores](https://github.com/mit-plv/fiat/tree/master/src/Narcissus/Stores)
 
-parameters (Source : Type, Target : Type)
+parameters (Source, Target : Type)
 
   ||| Decoders consume a _target value_ and produce either:
   |||
   ||| - a _source 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
   Decode : Type
   Decode = Target -> Maybe Source
 
+
   ||| Encoders take a _source value_ and produce either:
   |||
   ||| - a _target value_
@@ -41,6 +43,47 @@ parameters (Source : Type, Target : Type)
   Encode = Source -> Maybe Target
 
 
+parameters (Source, Target : Type)
+
+  ||| Decode a portion of a _target value_, leaving some remaining for
+  ||| subsequent decoding.
+  |||
+  ||| @ Source  The type of source values (usually an in-memory data structure)
+  ||| @ Target  The type of target values (usually a byte-stream)
+  public export
+  DecodePart : Type
+  DecodePart = Decode (Source, Target) Target
+
+
+  ||| Consumes a _source value_ and the remaining _target value_, returning
+  ||| a fully encoded target value.
+  |||
+  ||| @ Source  The type of source values (usually an in-memory data structure)
+  ||| @ Target  The type of target values (usually a byte-stream)
+  public export
+  EncodePart : 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 = 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 --
 ----------------------