Add support for do notation

Author: brendanzab

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

@@ -27,6 +27,16 @@ data FormatOf : (0 Rep : Type) -> Type where
   Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
 
 
+-- Support for do notation
+
+public export
+pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
+pure = Pure
+
+public export
+(>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
+(>>=) = Bind
+
 
 ---------------------------
 -- ENCODER/DECODER PAIRS --

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

@@ -78,6 +78,17 @@ mutual
   -- Rep (Custom f) = f.Rep
 
 
+-- Support for do notation
+
+public export
+pure : {0 A : Type} -> A -> Format
+pure = Pure
+
+public export
+(>>=) : (f : Format) -> (Rep f -> Format) -> Format
+(>>=) = Bind
+
+
 ---------------------------
 -- ENCODER/DECODER PAIRS --
 ---------------------------

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

@@ -96,6 +96,21 @@ encode (Bind f1 f2) (x ** y) =
 encode (Custom f) x = f.encode x
 
 
+--------------
+-- NOTATION --
+--------------
+
+-- Support for do notation
+
+public export
+pure : {0 A : Type} -> A -> Format
+pure = Pure
+
+public export
+(>>=) : (f : Format) -> (Rep f -> Format) -> Format
+(>>=) = Bind
+
+
 --------------------
 -- CUSTOM FORMATS --
 --------------------
@@ -164,33 +179,37 @@ foo cond f def = case orPure cond (toFormatOf f) def of
 --     },
 -- };
 flag : Format
-flag =
-  Bind u8 (\flag =>
-    if flag == 0 then u8 else Pure {A = Bits8} 0)
+flag = do
+  flag <- u8
+  if flag == 0 then u8 else
+    Pure {A = Bits8} 0
 
 -- def simple_glyph = fun (number_of_contours : U16) => {
 --     ...
 --     let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8),
 --     ...
 -- };
 simple_glyph : Format
-simple_glyph =
-  -- ...
-  Bind flag (\(flag ** repeat) =>
-    let
-      repeat' : Bits8
-      repeat' = case flag of
-        0 => repeat
-        x => ?todo4
-
-      -- repeat' : Bits8
-      -- repeat' with (MkSingEq flag)
-      --   repeat' | MkSingEq 0 {prf} = rewrite sym prf in repeat
-      --   repeat' | MkSingEq x {prf} = ?todo4
-
-      -- repeat' : Bits8
-      -- repeat' = case MkSingEq flag of
-      --   MkSingEq 0 {prf} => ?todo3
-      --   MkSingEq x {prf} => ?todo4
-    in
-      Pure (repeat' + 1))
+simple_glyph = do
+  (flag ** repeat) <- flag
+  let
+    repeat' : Bits8
+    repeat' = case flag of
+      0 => repeat
+      x => ?todo4
+
+    -- repeat' : Bits8
+    -- repeat' with (flag)
+    --   repeat' | 0 = ?todo3
+    --   repeat' | x = ?todo4
+
+    -- repeat' : Bits8
+    -- repeat' with (MkSingEq flag)
+    --   repeat' | MkSingEq 0 {prf} = ?help
+    --   repeat' | MkSingEq x {prf} = ?todo4
+
+    -- repeat' : Bits8
+    -- repeat' = case MkSingEq flag of
+    --   MkSingEq 0 {prf} => ?todo3
+    --   MkSingEq x {prf} => ?todo4
+  Pure (repeat' + 1)

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

@@ -15,9 +15,15 @@ import Data.Colist
 import Data.Vect
 
 import Fathom.Base
+import Fathom.Data.Refine
 import Fathom.Data.Sing
 
 
+-------------------------
+-- FORMAT DESCRIPTIONS --
+-------------------------
+
+
 public export
 record Format where
   constructor MkFormat
@@ -26,6 +32,11 @@ record Format where
   encode : Encode Rep BitStream
 
 
+--------------
+-- FORMATS --
+--------------
+
+
 public export
 end : Format
 end = MkFormat { Rep, decode, encode } where
@@ -39,6 +50,7 @@ end = MkFormat { Rep, decode, encode } where
   encode : Encode Rep BitStream
   encode () = Just []
 
+
 public export
 fail : Format
 fail = MkFormat { Rep, decode, encode } where
@@ -51,6 +63,7 @@ fail = MkFormat { Rep, decode, encode } where
   encode : Encode Rep BitStream
   encode x = void x
 
+
 public export
 pure : {0 A : Type} -> A -> Format
 pure x = MkFormat { Rep, decode, encode } where
@@ -63,6 +76,7 @@ pure x = MkFormat { Rep, decode, encode } where
   encode : Encode Rep BitStream
   encode (MkSing _) = Just []
 
+
 public export
 skip : (f : Format) -> (def : f.Rep) -> Format
 skip f def = MkFormat { Rep, decode, encode } where
@@ -116,3 +130,26 @@ bind f1 f2 = MkFormat { Rep, decode, encode } where
   encode : Encode Rep BitStream
   encode (x ** y) =
     [| f1.encode x <+> (f2 x).encode y |]
+
+
+-- Support for do notation
+
+public export
+(>>=) : (f : Format) -> (Rep f -> Format) -> Format
+(>>=) = bind
+
+
+
+-----------------
+-- EXPERIMENTS --
+-----------------
+
+
+||| A format description refined with a fixed representation
+public export
+FormatOf : (0 Rep : Type) -> Type
+FormatOf rep = Refine Format (\f => f.Rep = rep)
+
+
+toFormatOf : (f : Format) -> FormatOf f.Rep
+toFormatOf f = MkRefine f