Clean up some state passing with do notation

Author: brendanzab

experiments/idris/src/Fathom/Base.idr

@@ -69,21 +69,37 @@ parameters (Source, Target : Type)
 
 namespace DecodePart
 
+  -- TODO: Should probably implement functor, applicative, or monad here. or use
+  -- the reader, writer or state monad transformers
+
   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)
 
 
+  public export
+  bind : {0 S1, S2, T : Type} -> DecodePart S1 T -> (S1 -> DecodePart S2 T) -> DecodePart S2 T
+  bind decode1 decode2 target = do
+    (source1, target') <- decode1 target
+    decode2 source1 target'
+
+
+  public export
+  (>>=) : {0 S1, S2, T : Type} -> DecodePart S1 T -> (S1 -> DecodePart S2 T) -> DecodePart S2 T
+  (>>=) = bind
+
+
 parameters {0 Source, Target : Type}
 
   public export
   toDecodeFull : (Monoid Target, Eq Target) => DecodePart Source Target -> Decode Source Target
-  toDecodeFull decode target = do
+  toDecodeFull decode target = Prelude.do
     (source, target') <- decode target
     if target == neutral then Just source else Nothing
 
@@ -160,14 +176,8 @@ data ByteOrder : Type where
 
 namespace ByteStream
 
-  splitLen : (n : Nat) -> Colist a -> Maybe (Vect n a, Colist a)
-  splitLen 0 _ = Nothing
-  splitLen (S k) [] = Nothing
-  splitLen (S k) (x :: rest) = Prelude.map (\(xs, rest') => (x :: xs, rest')) (splitLen k rest)
-
-
   export
-  decodeU8 : Decode (Bits8, ByteStream) ByteStream
+  decodeU8 : DecodePart Bits8 ByteStream
   decodeU8 [] = Nothing
   decodeU8 (x :: bytes) =  Just (x, bytes)
 
@@ -178,15 +188,15 @@ namespace ByteStream
 
 
   export
-  decodeU16 : ByteOrder -> Decode (Bits16, ByteStream) ByteStream
-  decodeU16 LE bytes = do
-    (bs, bytes') <- splitLen 2 bytes
-    let [b0, b1] = map (cast {to = Bits16}) bs
-    Just (b0 .|. b1 `shiftL` fromNat 8, bytes')
-  decodeU16 BE bytes = do
-    (bs, bytes') <- splitLen 2 bytes
-    let [b0, b1] = map (cast {to = Bits16}) bs
-    Just (b0 `shiftL` fromNat 8 .|. b1, bytes')
+  decodeU16 : ByteOrder -> DecodePart Bits16 ByteStream
+  decodeU16 LE = DecodePart.do
+    b0 <- map (cast {to = Bits16}) decodeU8
+    b1 <- map (cast {to = Bits16}) decodeU8
+    pure (b0 .|. b1 `shiftL` fromNat 8)
+  decodeU16 BE = DecodePart.do
+    b0 <- map (cast {to = Bits16}) decodeU8
+    b1 <- map (cast {to = Bits16}) decodeU8
+    pure (b0 `shiftL` fromNat 8 .|. b1)
 
 
   export
@@ -196,18 +206,26 @@ namespace ByteStream
 
 
   export
-  decodeU32 : ByteOrder -> Decode (Bits32, ByteStream) ByteStream
-  decodeU32 LE bytes = do
-    (bs, bytes') <- splitLen 4 bytes
-    let [b0, b1, b2, b3] = map (cast {to = Bits32}) bs
-    Just (b0 .|. b1 `shiftL` fromNat 8 .|. b2 `shiftL` fromNat 16 .|. b2 `shiftL` fromNat 24, bytes')
-  decodeU32 BE bytes = do
-    (bs, bytes') <- splitLen 4 bytes
-    let [b0, b1, b2, b3] = map (cast {to = Bits32}) bs
-    Just (b0 `shiftL` fromNat 24 .|. b1 `shiftL` fromNat 16 .|. b2 `shiftL` fromNat 8 .|. b3, bytes')
+  decodeU32 : ByteOrder -> DecodePart Bits32 ByteStream
+  decodeU32 LE = DecodePart.do
+    b0 <- map (cast {to = Bits32}) decodeU8
+    b1 <- map (cast {to = Bits32}) decodeU8
+    b2 <- map (cast {to = Bits32}) decodeU8
+    b3 <- map (cast {to = Bits32}) decodeU8
+    pure (b0 .|. b1 `shiftL` fromNat 8 .|. b2 `shiftL` fromNat 16 .|. b2 `shiftL` fromNat 24)
+  decodeU32 BE = DecodePart.do
+    b0 <- map (cast {to = Bits32}) decodeU8
+    b1 <- map (cast {to = Bits32}) decodeU8
+    b2 <- map (cast {to = Bits32}) decodeU8
+    b3 <- map (cast {to = Bits32}) decodeU8
+    pure (b0 `shiftL` fromNat 24 .|. b1 `shiftL` fromNat 16 .|. b2 `shiftL` fromNat 8 .|. b3)
 
 
   export
   encodeU32 : ByteOrder -> Encode Bits32 ByteStream
   encodeU32 LE x = Just [cast x, cast (x `shiftR` fromNat 8), cast (x `shiftR` fromNat 16), cast (x `shiftR` fromNat 24)]
   encodeU32 BE x = Just [cast (x `shiftR` fromNat 24), cast (x `shiftR` fromNat 16), cast (x `shiftR` fromNat 8), cast x]
+
+
+  -- decodeU : Bits a => ByteOrder -> DecodePart a ByteStream
+  -- encodeU : Bits a => ByteOrder -> Encode a ByteStream

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

@@ -49,24 +49,21 @@ namespace FormatOf
 
   export
   decode : {0 A, S : Type} -> (f : FormatOf A) -> Decode (A, Colist S) (Colist S)
-  decode End [] = Just ((), [])
-  decode End (_::_) = Nothing
-  decode Fail _ = Nothing
-  decode (Pure x) buffer =
-    Just (MkSing x, buffer)
-  decode (Skip f _) buffer = do
-    (x, buffer') <- decode f buffer
-    Just ((), buffer')
-  decode (Repeat 0 f) buffer =
-    Just ([], buffer)
-  decode (Repeat (S len) f) buffer = do
-    (x, buffer') <- decode f buffer
-    (xs, buffer'') <- decode (Repeat len f) buffer'
-    Just (x :: xs, buffer'')
-  decode (Bind f1 f2) buffer = do
-    (x, buffer') <- decode f1 buffer
-    (y, buffer'') <- decode (f2 x) buffer'
-    Just ((x ** y), buffer'')
+  decode End =
+    \case [] => Just ((), [])
+          (_::_) => Nothing
+  decode Fail = const Nothing
+  decode (Pure x) = pure (MkSing x)
+  decode (Skip f _) = map (const ()) (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 (Bind f1 f2) = do
+    x <- decode f1
+    y <- decode (f2 x)
+    pure (x ** y)
 
 
   export

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

@@ -62,26 +62,23 @@ namespace FormatOf
 
 
   export
-  decode : {0 A : Type} -> (f : FormatOf A) -> Decode (A, ByteStream) ByteStream
-  decode End [] = Just ((), [])
-  decode End (_::_) = Nothing
-  decode Fail _ = Nothing
-  decode (Pure x) buffer =
-    Just (MkSing x, buffer)
-  decode (Skip f _) buffer = do
-    (x, buffer') <- decode f buffer
-    Just ((), buffer')
-  decode (Repeat 0 f) buffer =
-    Just ([], buffer)
-  decode (Repeat (S len) f) buffer = do
-    (x, buffer') <- decode f buffer
-    (xs, buffer'') <- decode (Repeat len f) buffer'
-    Just (x :: xs, buffer'')
-  decode (Bind f1 f2) buffer = do
-    (x, buffer') <- decode f1 buffer
-    (y, buffer'') <- decode (f2 x) buffer'
-    Just ((x ** y), buffer'')
-  decode (Custom f) buffer = f.decode buffer
+  decode : {0 A : Type} -> (f : FormatOf A) -> DecodePart A ByteStream
+  decode End =
+    \case [] => Just ((), [])
+          (_::_) => Nothing
+  decode Fail = const Nothing
+  decode (Pure x) = pure (MkSing x)
+  decode (Skip f _) = map (const ()) (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 (Bind f1 f2) = do
+    x <- decode f1
+    y <- decode (f2 x)
+    pure (x ** y)
+  decode (Custom f) = f.decode
 
 
   export

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

@@ -80,25 +80,22 @@ namespace Format
 
 
   export
-  decode : (f : Format) -> Decode (Rep f, Colist a) (Colist a)
-  decode End [] = Just ((), [])
-  decode End (_::_) = Nothing
-  decode Fail _ = Nothing
-  decode (Pure x) buffer =
-    Just (MkSing x, buffer)
-  decode (Skip f _) buffer = do
-    (x, buffer') <- decode f buffer
-    Just ((), buffer')
-  decode (Repeat 0 f) buffer =
-    Just ([], buffer)
-  decode (Repeat (S len) f) buffer = do
-    (x, buffer') <- decode f buffer
-    (xs, buffer'') <- decode (Repeat len f) buffer'
-    Just (x :: xs, buffer'')
-  decode (Bind f1 f2) buffer = do
-    (x, buffer') <- decode f1 buffer
-    (y, buffer'') <- decode (f2 x) buffer'
-    Just ((x ** y), buffer'')
+  decode : (f : Format) -> DecodePart (Rep f) (Colist a)
+  decode End =
+    \case [] => Just ((), [])
+          (_::_) => Nothing
+  decode Fail = const Nothing
+  decode (Pure x) = pure (MkSing x)
+  decode (Skip f _) = map (const ()) (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 (Bind f1 f2) = do
+    x <- decode f1
+    y <- decode (f2 x)
+    pure (x ** y)
 
 
   export

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

@@ -81,26 +81,23 @@ namespace Format
 
 
   export
-  decode : (f : Format) -> Decode (Rep f, ByteStream) ByteStream
-  decode End [] = Just ((), [])
-  decode End (_::_) = Nothing
-  decode Fail _ = Nothing
-  decode (Pure x) buffer =
-    Just (MkSing x, buffer)
-  decode (Skip f _) buffer = do
-    (x, buffer') <- decode f buffer
-    Just ((), buffer')
-  decode (Repeat 0 f) buffer =
-    Just ([], buffer)
-  decode (Repeat (S len) f) buffer = do
-    (x, buffer') <- decode f buffer
-    (xs, buffer'') <- decode (Repeat len f) buffer'
-    Just (x :: xs, buffer'')
-  decode (Bind f1 f2) buffer = do
-    (x, buffer') <- decode f1 buffer
-    (y, buffer'') <- decode (f2 x) buffer'
-    Just ((x ** y), buffer'')
-  decode (Custom f) buffer = f.decode buffer
+  decode : (f : Format) -> DecodePart (Rep f) ByteStream
+  decode End =
+    \case [] => Just ((), [])
+          (_::_) => Nothing
+  decode Fail = const Nothing
+  decode (Pure x) = pure (MkSing x)
+  decode (Skip f _) = map (const ()) (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 (Bind f1 f2) = do
+    x <- decode f1
+    y <- decode (f2 x)
+    pure (x ** y)
+  decode (Custom f) = f.decode
 
 
   export

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

@@ -29,7 +29,7 @@ public export
 record Format where
   constructor MkFormat
   Rep : Type
-  decode : Decode (Rep, ByteStream) ByteStream
+  decode : DecodePart Rep ByteStream
   encode : Encode Rep ByteStream
 
 
@@ -41,7 +41,7 @@ namespace Format
     Rep : Type
     Rep = Unit
 
-    decode : Decode (Rep, ByteStream) ByteStream
+    decode : DecodePart Rep ByteStream
     decode [] = Just ((), [])
     decode (_::_) = Nothing
 
@@ -55,8 +55,8 @@ namespace Format
     Rep : Type
     Rep = Void
 
-    decode : Decode (Rep, ByteStream) ByteStream
-    decode _ = Nothing
+    decode : DecodePart Rep ByteStream
+    decode = const Nothing
 
     encode : Encode Rep ByteStream
     encode x = void x
@@ -68,8 +68,8 @@ namespace Format
     Rep : Type
     Rep = Sing x
 
-    decode : Decode (Rep, ByteStream) ByteStream
-    decode buffer = Just (MkSing x, buffer)
+    decode : DecodePart Rep ByteStream
+    decode = pure (MkSing x)
 
     encode : Encode Rep ByteStream
     encode (MkSing _) = Just []
@@ -81,10 +81,8 @@ namespace Format
     Rep : Type
     Rep = ()
 
-    decode : Decode (Rep, ByteStream) ByteStream
-    decode buffer = do
-      (x, buffer') <- f.decode buffer
-      Just ((), buffer')
+    decode : DecodePart Rep ByteStream
+    decode = map (const ()) f.decode
 
     encode : Encode Rep ByteStream
     encode () = f.encode def
@@ -96,14 +94,14 @@ namespace Format
     Rep : Type
     Rep = Vect len f.Rep
 
-    decode : Decode (Rep, ByteStream) ByteStream
+    decode : DecodePart Rep ByteStream
     decode = go len where
-      go : (len : Nat) -> Decode (Vect len f.Rep, ByteStream) ByteStream
-      go 0 buffer = Just ([], buffer)
-      go (S len) buffer = do
-        (x, buffer') <- f.decode buffer
-        (xs, buffer'') <- go len buffer'
-        Just (x :: xs, buffer'')
+      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)
 
     encode : Encode Rep ByteStream
     encode = go len where
@@ -119,11 +117,11 @@ namespace Format
     Rep : Type
     Rep = (x : f1.Rep ** (f2 x).Rep)
 
-    decode : Decode (Rep, ByteStream) ByteStream
-    decode buffer = do
-      (x, buffer') <- f1.decode buffer
-      (y, buffer'') <- (f2 x).decode buffer'
-      Just ((x ** y), buffer'')
+    decode : DecodePart Rep ByteStream
+    decode = do
+      x <- f1.decode
+      y <- (f2 x).decode
+      pure (x ** y)
 
     encode : Encode Rep ByteStream
     encode (x ** y) =
@@ -184,7 +182,7 @@ data FormatOf : (A : Type) -> Type where
 
 namespace FormatOf
 
-  decode : {0 A : Type} -> (f : FormatOf A) -> Decode (A, ByteStream) ByteStream
+  decode : {0 A : Type} -> (f : FormatOf A) -> DecodePart (A) ByteStream
   decode  (MkFormatOf f) = Format.decode f