Make Decode type match Source more closely

Author: brendanzab

experiments/idris/src/Fathom/Base.idr

@@ -21,14 +21,13 @@ parameters (Source : Type, Target : Type)
 
   ||| Decoders consume a _target value_ and produce either:
   |||
-  ||| - a _source value_ and _remaining target value_
+  ||| - 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, Target)
+  Decode = Target -> Maybe Source
 
   ||| Encoders take a _source value_ and produce either:
   |||

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

@@ -43,7 +43,7 @@ public export
 ---------------------------
 
 export
-decode : {0 Rep : Type} -> (f : FormatOf Rep) -> Decode Rep (Colist a)
+decode : {0 Rep : Type} -> (f : FormatOf Rep) -> Decode (Rep, Colist a) (Colist a)
 decode End [] = Just ((), [])
 decode End (_::_) = Nothing
 decode Fail _ = Nothing

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

@@ -95,7 +95,7 @@ public export
 
 
 export
-decode : (f : Format) -> Decode (Rep f) (Colist a)
+decode : (f : Format) -> Decode (Rep f, Colist a) (Colist a)
 decode End [] = Just ((), [])
 decode End (_::_) = Nothing
 decode Fail _ = Nothing

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

@@ -26,7 +26,7 @@ public export
 record CustomFormat where
   constructor MkCustomFormat
   Rep : Type
-  decode : Decode Rep ByteStream
+  decode : Decode (Rep, ByteStream) ByteStream
   encode : Encode Rep ByteStream
 
 
@@ -61,7 +61,7 @@ mutual
 
 
 export
-decode : (f : Format) -> Decode (Rep f) ByteStream
+decode : (f : Format) -> Decode (Rep f, ByteStream) ByteStream
 decode End [] = Just ((), [])
 decode End (_::_) = Nothing
 decode Fail _ = Nothing

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

@@ -28,7 +28,7 @@ public export
 record Format where
   constructor MkFormat
   Rep : Type
-  decode : Decode Rep BitStream
+  decode : Decode (Rep, BitStream) BitStream
   encode : Encode Rep BitStream
 
 
@@ -43,7 +43,7 @@ end = MkFormat { Rep, decode, encode } where
   Rep : Type
   Rep = Unit
 
-  decode : Decode Rep BitStream
+  decode : Decode (Rep, BitStream) BitStream
   decode [] = Just ((), [])
   decode (_::_) = Nothing
 
@@ -57,7 +57,7 @@ fail = MkFormat { Rep, decode, encode } where
   Rep : Type
   Rep = Void
 
-  decode : Decode Rep BitStream
+  decode : Decode (Rep, BitStream) BitStream
   decode _ = Nothing
 
   encode : Encode Rep BitStream
@@ -70,7 +70,7 @@ pure x = MkFormat { Rep, decode, encode } where
   Rep : Type
   Rep = Sing x
 
-  decode : Decode Rep BitStream
+  decode : Decode (Rep, BitStream) BitStream
   decode buffer = Just (MkSing x, buffer)
 
   encode : Encode Rep BitStream
@@ -83,7 +83,7 @@ skip f def = MkFormat { Rep, decode, encode } where
   Rep : Type
   Rep = ()
 
-  decode : Decode Rep BitStream
+  decode : Decode (Rep, BitStream) BitStream
   decode buffer = do
     (x, buffer') <- f.decode buffer
     Just ((), buffer')
@@ -98,9 +98,9 @@ repeat len f = MkFormat { Rep, decode, encode } where
   Rep : Type
   Rep = Vect len f.Rep
 
-  decode : Decode Rep BitStream
+  decode : Decode (Rep, BitStream) BitStream
   decode = go len where
-    go : (len : Nat) -> Decode (Vect len f.Rep) BitStream
+    go : (len : Nat) -> Decode (Vect len f.Rep, BitStream) BitStream
     go 0 buffer = Just ([], buffer)
     go (S len) buffer = do
       (x, buffer') <- f.decode buffer
@@ -121,7 +121,7 @@ bind f1 f2 = MkFormat { Rep, decode, encode } where
   Rep : Type
   Rep = (x : f1.Rep ** (f2 x).Rep)
 
-  decode : Decode Rep BitStream
+  decode : Decode (Rep, BitStream) BitStream
   decode buffer = do
     (x, buffer') <- f1.decode buffer
     (y, buffer'') <- (f2 x).decode buffer'