Remove do keyword from uses of do notation

README.md

@@ -22,7 +22,7 @@ Examples
 
 ```c
 Main: IO(Unit)
-  do IO {
+  IO {
     IO.print("Hello, world!")
   }
 ```

SYNTAX.md

@@ -620,7 +620,7 @@ Do notation
 -----------
 
 ```
-do name {
+name {
   statements
 }
 ```
@@ -635,7 +635,7 @@ of `Monad.bind` and `Monad.pure`. For example,
 
 ```
 ask_user_age: IO(Nat)
-  do IO {
+  IO {
     var name = IO.get_line("What is your name?")
     IO.print("Welcome, " | name)
     var year = IO.get_line("When you were born?")

base/Example/greet.kind

@@ -1,5 +1,5 @@
 Example.greet: IO(Unit)
-  do IO {
+  IO {
     IO.print("What is your name?")
     var name = IO.get_line
     IO.print("Hello, " | name | "!")

base/Fmt/sprintf.kind

@@ -18,35 +18,35 @@ Fmt.Specifier.show(s: Fmt.Specifier): String
   }
 
 Fmt.Parser.string: Parser(Fmt.Specifier)
-  do Parser {
+  Parser {
     Parser.text("%s")
     return Fmt.Specifier.string;
   }
 
 Fmt.Parser.integer: Parser(Fmt.Specifier)
-  do Parser {
+  Parser {
     Parser.text("%d")
     return Fmt.Specifier.integer;
   }
 
 Fmt.Parser.percent: Parser(Fmt.Specifier)
-  do Parser {
+  Parser {
     Parser.text("%%")
     return Fmt.Specifier.char('%');
   }
 
 Fmt.Parser.char: Parser(Fmt.Specifier)
-  do Parser {
+  Parser {
     var c = Parser.one
     return Fmt.Specifier.char(c);
   }
 
 Fmt.Parser.parser(xs: List(Fmt.Specifier)): Parser(List(Fmt.Specifier))
-  do Parser {
+  Parser {
     var stop = Parser.is_eof;
-    if stop then do Parser {
+    if stop then Parser {
       return xs;
-    } else do Parser {
+    } else Parser {
       var x = Parser.first_of!([
         Fmt.Parser.string,
         Fmt.Parser.integer,

base/IO/prompt.kind

@@ -1,5 +1,5 @@
 IO.prompt(text: String): IO(String)
-  do IO {
+  IO {
     IO.put_string(text)
     IO.get_line
   }

base/Kind.kind

@@ -1,5 +1,5 @@
 Kind: IO(Unit)
-  do IO {
+  IO {
     let _ = Kind.to_core.io.one;
     let _ = Kind.checker.io.one;
     let _ = Kind.checker.io.file;

base/Kind/Parser/annotation.kind

@@ -1,5 +1,5 @@
 Kind.Parser.annotation(init: Nat, term: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     Kind.Parser.text("::");
     var type = Kind.Parser.term;
     var orig = Kind.Parser.stop(init);

base/Kind/Parser/application.kind

@@ -1,5 +1,5 @@
 Kind.Parser.application(init: Nat, func: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     Parser.text("(");
     var args = Parser.until1!(
       Kind.Parser.text(")"),

base/Kind/Parser/application/erased.kind

@@ -1,5 +1,5 @@
 Kind.Parser.application.erased(init: Nat, func: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Parser.get_index;
     Parser.text("<");
     var args = Parser.until1!(

base/Kind/Parser/application/hole.kind

@@ -1,5 +1,5 @@
 Kind.Parser.application.hole(init: Nat, term: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     Kind.Parser.text("!");
     var orig = Kind.Parser.stop(init);
     return Kind.Term.ori(orig, Kind.Term.app(term, Kind.Term.hol(Bits.e)));

base/Kind/Parser/apply.kind

@@ -1,5 +1,5 @@
 Kind.Parser.apply: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("apply(");
     var func = Kind.Parser.term;

base/Kind/Parser/arrow.kind

@@ -1,5 +1,5 @@
 Kind.Parser.arrow(init: Nat, xtyp: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     Kind.Parser.text("->");
     var body = Kind.Parser.term;
     var orig = Kind.Parser.stop(init);

base/Kind/Parser/binder.kind

@@ -1,5 +1,5 @@
 Kind.Parser.binder(sep: String): Parser(List(Kind.Binder))
-  do Parser {
+  Parser {
     var lists = Parser.many1!(Parser.first_of!([
       Kind.Parser.binder.homo(sep, Bool.true),
       Kind.Parser.binder.homo(sep, Bool.false),

base/Kind/Parser/binder/homo.kind

@@ -1,5 +1,5 @@
 Kind.Parser.binder.homo(sep: String, eras: Bool): Parser(List(Kind.Binder))
-  do Parser {
+  Parser {
     Kind.Parser.text(if eras then "<" else "(");
     var bind = Parser.until1!(
       Kind.Parser.text(if eras then ">" else ")"),

base/Kind/Parser/case.kind

@@ -1,10 +1,10 @@
 Kind.Parser.case: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("case ");
     Kind.Parser.spaces;
     var expr = Kind.Parser.term;
-    var name = Parser.maybe!(do Parser {
+    var name = Parser.maybe!(Parser {
       Kind.Parser.text("as");
       Kind.Parser.name1;
     });
@@ -19,7 +19,7 @@ Kind.Parser.case: Parser(Kind.Term)
     var wyth = Parser.many!(Kind.Parser.case.with);
     Kind.Parser.text("{");
     var cses = Parser.until!(Kind.Parser.text("}"), Kind.Parser.case.case);
-    var dflt = Parser.maybe!(do Parser {
+    var dflt = Parser.maybe!(Parser {
       Kind.Parser.text("else ");
       var term = Kind.Parser.term;
       return term;
@@ -34,18 +34,18 @@ Kind.Parser.case: Parser(Kind.Term)
     ));
     var moti = Parser.first_of!([
       // Explicit motive
-      do Parser {
+      Parser {
         Kind.Parser.text(":");
         var term = Kind.Parser.term;
         return Maybe.some!(term);
       },
       // Smart motive
-      do Parser {
+      Parser {
         Kind.Parser.text("!");
         return Maybe.none!;
       },
       // Hole motive
-      do Parser {
+      Parser {
         return Maybe.some!(Kind.Term.hol(Bits.e));
       },
     ]);

base/Kind/Parser/case/case.kind

@@ -1,5 +1,5 @@
 Kind.Parser.case.case: Parser(Pair(Kind.Name, Kind.Term))
-  do Parser {
+  Parser {
     var name = Kind.Parser.name1;
     Kind.Parser.text(":");
     var term = Kind.Parser.term;

base/Kind/Parser/case/with.kind

@@ -1,5 +1,5 @@
 Kind.Parser.case.with: Parser(Kind.Def)
-  do Parser {
+  Parser {
     Kind.Parser.text("with");
     var name = Kind.Parser.name1;
     Kind.Parser.text(":");

base/Kind/Parser/char.kind

@@ -1,5 +1,5 @@
 Kind.Parser.char: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("'");
     var chrx = Kind.Parser.char.single;

base/Kind/Parser/char/single.kind

@@ -1,7 +1,7 @@
 Kind.Parser.char.single: Parser(Char)
   Parser.first_of!([
     Parser.first_of!(List.mapped!(Kind.escapes)!((esc) case esc {
-      new: do Parser {
+      new: Parser {
         Parser.text(esc.fst);
         return esc.snd;
       }

base/Kind/Parser/concat.kind

@@ -1,5 +1,5 @@
 Kind.Parser.concat(init: Nat, lst0: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     Kind.Parser.text("++");
     var lst1 = Kind.Parser.term;
     var orig = Kind.Parser.stop(init);

base/Kind/Parser/cons.kind

@@ -1,5 +1,5 @@
 Kind.Parser.cons(init: Nat, head: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     Kind.Parser.text("&");
     var tail = Kind.Parser.term;
     var orig = Kind.Parser.stop(init);

base/Kind/Parser/constructor.kind

@@ -1,8 +1,8 @@
 Kind.Parser.constructor(namespace: Kind.Name): Parser(Kind.Constructor)
-  do Parser {
+  Parser {
     var name = Kind.Parser.name1;
     var args = Parser.maybe!(Kind.Parser.binder(":"));
-    var inds = Parser.maybe!(do Parser {
+    var inds = Parser.maybe!(Parser {
       Kind.Parser.text("~");
       Kind.Parser.binder("=");
     });

base/Kind/Parser/datatype.kind

@@ -1,9 +1,9 @@
 Kind.Parser.datatype: Parser(Kind.Datatype)
-  do Parser {
+  Parser {
     Kind.Parser.text("type ");
     var name = Kind.Parser.name1; 
     var pars = Parser.maybe!(Kind.Parser.binder(":"));
-    var inds = Parser.maybe!(do Parser {
+    var inds = Parser.maybe!(Parser {
       Kind.Parser.text("~");
       Kind.Parser.binder(":");
     });

base/Kind/Parser/def.kind

@@ -1,5 +1,5 @@
 Kind.Parser.def: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("def ");
     var name = Kind.Parser.name;

base/Kind/Parser/do.kind

@@ -1,5 +1,5 @@
 Kind.Parser.do: Parser(Kind.Term)
-  do Parser {
+  Parser {
     Parser.maybe!(Kind.Parser.text("do "));
     var name = Kind.Parser.name1;
     Kind.Parser.text("{");

base/Kind/Parser/do/statements.kind

@@ -1,7 +1,7 @@
 Kind.Parser.do.statements(monad_name: Kind.Name): Parser(Kind.Term)
   Parser.first_of!([
     // Binding call: @ask x = expr; rest@
-    do Parser {
+    Parser {
       var init = Kind.Parser.init;
       Kind.Parser.text("var ");
       var name = Kind.Parser.name1;
@@ -19,7 +19,7 @@ Kind.Parser.do.statements(monad_name: Kind.Name): Parser(Kind.Term)
       return Kind.Term.ori(orig, term);
     },
     // Local definition (let): @let x = expr; rest@
-    do Parser {
+    Parser {
       var init = Kind.Parser.init;
       Kind.Parser.text("let ");
       var name = Kind.Parser.name1;
@@ -31,7 +31,7 @@ Kind.Parser.do.statements(monad_name: Kind.Name): Parser(Kind.Term)
       return Kind.Term.ori(orig, Kind.Term.let(name, expr, (x) body));
     },
     // Return pure: @return expr;@
-    do Parser {
+    Parser {
       var init = Kind.Parser.init;
       Kind.Parser.text("return ");
       var expr = Kind.Parser.term;
@@ -44,7 +44,7 @@ Kind.Parser.do.statements(monad_name: Kind.Name): Parser(Kind.Term)
       return Kind.Term.ori(orig, term);
     },
     // Non-binding call: @expr; rest@
-    do Parser {
+    Parser {
       var init = Kind.Parser.init;
       var expr = Kind.Parser.term;
       Parser.maybe!(Kind.Parser.text(";"));
@@ -59,7 +59,7 @@ Kind.Parser.do.statements(monad_name: Kind.Name): Parser(Kind.Term)
       return Kind.Term.ori(orig, term);
     },
     // Return direct: @expr;@
-    do Parser {
+    Parser {
       var expr = Kind.Parser.term;
       Parser.maybe!(Kind.Parser.text(";"));
       return expr;

base/Kind/Parser/equality.kind

@@ -1,5 +1,5 @@
 Kind.Parser.equality(init: Nat, val0: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     Kind.Parser.text("==");
     var val1 = Kind.Parser.term;
     var orig = Kind.Parser.stop(init);

base/Kind/Parser/file.kind

@@ -1,9 +1,9 @@
 Kind.Parser.file(file: String, code: String, defs: Kind.Defs): Parser(Kind.Defs)
-  do Parser {
+  Parser {
     var stop = Parser.is_eof;
-    if stop then do Parser {
+    if stop then Parser {
       return defs;
-    } else do Parser {
+    } else Parser {
       var defs = Parser.first_of!([
         Kind.Parser.file.def(file, code, defs),
         Kind.Parser.file.adt(file, code, defs),

base/Kind/Parser/file/adt.kind

@@ -1,10 +1,10 @@
 Kind.Parser.file.adt(file: String, code: String, defs: Kind.Defs): Parser(Kind.Defs)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     var adt = Kind.Parser.datatype;
     var orig = Kind.Parser.stop(init);
     case adt {
-      new: do Parser {
+      new: Parser {
         let term = Kind.Datatype.build_term(adt);
         let term = Kind.Term.bind([], (x) Bits.i(x), term);
         let type = Kind.Datatype.build_type(adt);

base/Kind/Parser/file/def.kind

@@ -1,5 +1,5 @@
 Kind.Parser.file.def(file: String, code: String, defs: Kind.Defs): Parser(Kind.Defs)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     var name = Kind.Parser.name1;
     var args = Parser.many!(Kind.Parser.binder(":"));

base/Kind/Parser/file/end.kind

@@ -1,5 +1,5 @@
 Kind.Parser.file.end(file: String, code: String, defs: Kind.Defs): Parser(Kind.Defs)
-  do Parser {
+  Parser {
     Kind.Parser.spaces;
     Parser.eof;
     return defs;

base/Kind/Parser/forall.kind

@@ -1,5 +1,5 @@
 Kind.Parser.forall: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     var self = Kind.Parser.name;
     var bind = Kind.Parser.binder(":");

base/Kind/Parser/get.kind

@@ -1,5 +1,5 @@
 Kind.Parser.get: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("let ");
     Kind.Parser.text("{");

base/Kind/Parser/goal.kind

@@ -1,15 +1,15 @@
 Kind.Parser.goal: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("?");
     var name = Kind.Parser.name;
-    var dref = Parser.many!(do Parser {
+    var dref = Parser.many!(Parser {
       Kind.Parser.text("-");
       var nat = Parser.nat;
       let bits = Bits.reverse(Bits.tail(Bits.reverse(Nat.to_bits(nat))));
-      do Parser { return bits; };
+      Parser { return bits; };
     });
-    var verb = do Parser {
+    var verb = Parser {
       var verb = Parser.maybe!(Parser.text("-"));
       return Maybe.to_bool!(verb);
     };

base/Kind/Parser/goal_rewrite.kind

@@ -1,5 +1,5 @@
 Kind.Parser.goal_rewrite: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("rewrite ");
     var name = Kind.Parser.name1;

base/Kind/Parser/hole.kind

@@ -1,5 +1,5 @@
 Kind.Parser.hole: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("_");
     var orig = Kind.Parser.stop(init);

base/Kind/Parser/if.kind

@@ -1,5 +1,5 @@
 Kind.Parser.if: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("if ");
     var cond = Kind.Parser.term;

base/Kind/Parser/inequality.kind

@@ -1,5 +1,5 @@
 Kind.Parser.inequality(init: Nat, val0: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     Kind.Parser.text("!=");
     var val1 = Kind.Parser.term;
     var orig = Kind.Parser.stop(init);

base/Kind/Parser/init.kind

@@ -1,5 +1,5 @@
 Kind.Parser.init: Parser(Nat)
-  do Parser {
+  Parser {
     Kind.Parser.spaces;
     var from = Parser.get_index;
     return from;

base/Kind/Parser/item.kind

@@ -1,5 +1,5 @@
 Kind.Parser.item<V: Type>(parser: Parser(V)): Parser(V)
-  do Parser {
+  Parser {
     Kind.Parser.spaces;
     var value = parser;
     Parser.maybe!(Kind.Parser.text(","));

base/Kind/Parser/lambda.kind

@@ -1,5 +1,5 @@
 Kind.Parser.lambda: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("(");
     var name = Parser.until1!(

base/Kind/Parser/lambda/erased.kind

@@ -1,5 +1,5 @@
 Kind.Parser.lambda.erased: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("<");
     var name = Parser.until1!(

base/Kind/Parser/lambda/nameless.kind

@@ -1,5 +1,5 @@
 Kind.Parser.lambda.nameless: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("()");
     var body = Kind.Parser.term;

base/Kind/Parser/let.kind

@@ -1,5 +1,5 @@
 Kind.Parser.let: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("let ");
     var name = Kind.Parser.name;

base/Kind/Parser/letforin.kind

@@ -1,5 +1,5 @@
 Kind.Parser.letforin: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("let ");
     var name = Kind.Parser.name1;

base/Kind/Parser/letforrange/nat.kind

@@ -1,5 +1,5 @@
 Kind.Parser.letforrange.nat: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("let ");
     var name = Kind.Parser.name1;

base/Kind/Parser/letforrange/u32.kind

@@ -1,5 +1,5 @@
 Kind.Parser.letforrange.u32: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("let ");
     var name = Kind.Parser.name1;

base/Kind/Parser/list.kind

@@ -1,5 +1,5 @@
 Kind.Parser.list: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("[");
     var vals = Parser.until!(

base/Kind/Parser/log.kind

@@ -1,5 +1,5 @@
 Kind.Parser.log: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("log(");
     var strs = Parser.until!(Kind.Parser.text(")"), Kind.Parser.item!(Kind.Parser.term));

base/Kind/Parser/mirror.kind

@@ -1,5 +1,5 @@
 Kind.Parser.mirror: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("mirror(");
     var equa = Kind.Parser.term;

base/Kind/Parser/name.kind

@@ -1,5 +1,5 @@
 Kind.Parser.name: Parser(Kind.Name)
-  do Parser {
+  Parser {
     Kind.Parser.spaces;
     var chrs = Parser.many<Kind.Letter>(Kind.Parser.letter);
     return List.fold!(chrs)!(String.nil, String.cons);

base/Kind/Parser/name1.kind

@@ -1,5 +1,5 @@
 Kind.Parser.name1: Parser(Kind.Name)
-  do Parser {
+  Parser {
     Kind.Parser.spaces;
     var chrs = Parser.many1<Kind.Letter>(Kind.Parser.letter);
     return List.fold!(chrs)!(String.nil, String.cons);

base/Kind/Parser/name_term.kind

@@ -1,5 +1,5 @@
 Kind.Parser.name_term(sep: String): Parser(Pair(Kind.Name, Kind.Term))
-  do Parser {
+  Parser {
     var name = Kind.Parser.name;
     Kind.Parser.text(sep);
     var type = Kind.Parser.term;

base/Kind/Parser/nat.kind

@@ -1,5 +1,5 @@
 Kind.Parser.nat: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.spaces;
     var natx = Parser.nat;

base/Kind/Parser/op.kind

@@ -1,5 +1,5 @@
 Kind.Parser.op(sym: String, ref: String, init: Nat, val0: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     Kind.Parser.text(sym);
     var val1 = Kind.Parser.term;
     var orig = Kind.Parser.stop(init);

base/Kind/Parser/open.kind

@@ -1,10 +1,10 @@
 Kind.Parser.open: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("open ");
     Kind.Parser.spaces;
     var expr = Kind.Parser.term;
-    var name = Parser.maybe!(do Parser {
+    var name = Parser.maybe!(Parser {
       Kind.Parser.text("as");
       Kind.Parser.name1;
     });

base/Kind/Parser/pair.kind

@@ -1,5 +1,5 @@
 Kind.Parser.pair: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("{");
     var val0 = Kind.Parser.term;

base/Kind/Parser/parenthesis.kind

@@ -1,5 +1,5 @@
 Kind.Parser.parenthesis: Parser(Kind.Term)
-  do Parser {
+  Parser {
     Kind.Parser.text("(");
     var term = Kind.Parser.term;
     Kind.Parser.text(")");

base/Kind/Parser/reference.kind

@@ -1,39 +1,39 @@
 Kind.Parser.reference: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     var name = Kind.Parser.name1;
-    if String.eql(name, "case") then do Parser {
+    if String.eql(name, "case") then Parser {
       Parser.fail!("Reserved keyword.");
-    } else if String.eql(name, "do") then do Parser {
+    } else if String.eql(name, "do") then Parser {
       Parser.fail!("Reserved keyword.");
-    } else if String.eql(name, "if") then do Parser {
+    } else if String.eql(name, "if") then Parser {
       Parser.fail!("Reserved keyword.");
-    } else if String.eql(name, "with") then do Parser {
+    } else if String.eql(name, "with") then Parser {
       Parser.fail!("Reserved keyword.");
-    //} else if String.eql(name, "then") then do Parser {
+    //} else if String.eql(name, "then") then Parser {
       //Parser.fail!("Reserved keyword.");
-    //} else if String.eql(name, "else") then do Parser {
+    //} else if String.eql(name, "else") then Parser {
       //Parser.fail!("Reserved keyword.");
-    } else if String.eql(name, "let") then do Parser {
+    } else if String.eql(name, "let") then Parser {
       Parser.fail!("Reserved keyword.");
-    } else if String.eql(name, "def") then do Parser {
+    } else if String.eql(name, "def") then Parser {
       Parser.fail!("Reserved keyword.");
-    } else if String.eql(name, "true") then do Parser {
+    } else if String.eql(name, "true") then Parser {
       return Kind.Term.ref("Bool.true");
-    } else if String.eql(name, "false") then do Parser {
+    } else if String.eql(name, "false") then Parser {
       return Kind.Term.ref("Bool.false");
-    } else if String.eql(name, "unit") then do Parser {
+    } else if String.eql(name, "unit") then Parser {
       return Kind.Term.ref("Unit.new");
-    } else if String.eql(name, "none") then do Parser {
+    } else if String.eql(name, "none") then Parser {
       let term = Kind.Term.ref("Maybe.none");
       let term = Kind.Term.app(term, Kind.Term.hol(Bits.e));
       return term;
-    } else if String.eql(name, "refl") then do Parser {
+    } else if String.eql(name, "refl") then Parser {
       let term = Kind.Term.ref("Equal.refl");
       let term = Kind.Term.app(term, Kind.Term.hol(Bits.e));
       let term = Kind.Term.app(term, Kind.Term.hol(Bits.e));
       return term;
-    } else do Parser {
+    } else Parser {
       var orig = Kind.Parser.stop(init);
       return Kind.Term.ori(orig, Kind.Term.ref(name));
     };

base/Kind/Parser/rewrite.kind

@@ -1,5 +1,5 @@
 Kind.Parser.rewrite(init: Nat, subt: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     Kind.Parser.text("::");
     Kind.Parser.text("rewrite");
     var name = Kind.Parser.name1;

base/Kind/Parser/sigma.kind

@@ -1,5 +1,5 @@
 Kind.Parser.sigma(init: Nat, val0: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     Kind.Parser.text("~");
     var val1 = Kind.Parser.term;
     var orig = Kind.Parser.stop(init);

base/Kind/Parser/sigma/type.kind

@@ -1,5 +1,5 @@
 Kind.Parser.sigma.type: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("{");
     var name = Kind.Parser.name1;

base/Kind/Parser/some.kind

@@ -1,5 +1,5 @@
 Kind.Parser.some: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("some(");
     var expr = Kind.Parser.term;

base/Kind/Parser/spaces.kind

@@ -3,7 +3,7 @@ Kind.Parser.spaces: Parser(List(Unit))
     Parser.text(" "),
     Parser.text("\t"),
     Parser.text("\n"),
-    do Parser {
+    Parser {
       Parser.text("//");
       Parser.until!(Parser.text("\n"), Parser.one);
       return Unit.new;

base/Kind/Parser/stop.kind

@@ -1,5 +1,5 @@
 Kind.Parser.stop(from: Nat): Parser(Pair(Nat,Nat))
-  do Parser {
+  Parser {
     var upto = Parser.get_index;
     let orig = {from, upto};
     return orig;

base/Kind/Parser/string.kind

@@ -18,7 +18,7 @@ Kind.Parser.string.go(
   }
 
 Kind.Parser.string: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text(String.cons('"', String.nil));
     var strx = Kind.Parser.string.go("");

base/Kind/Parser/string_concat.kind

@@ -1,5 +1,5 @@
 Kind.Parser.string_concat(init: Nat, str0: Kind.Term): Parser(Kind.Term)
-  do Parser {
+  Parser {
     Kind.Parser.text("|");
     var str1 = Kind.Parser.term;
     var orig = Kind.Parser.stop(init);

base/Kind/Parser/switch.kind

@@ -1,5 +1,5 @@
 Kind.Parser.switch.case: Parser(Pair(Kind.Term, Kind.Term))
-  do Parser {
+  Parser {
     var key = Kind.Parser.term;
     Kind.Parser.text(":");
     var val = Kind.Parser.term;
@@ -7,7 +7,7 @@ Kind.Parser.switch.case: Parser(Pair(Kind.Term, Kind.Term))
   }
 
 Kind.Parser.switch: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("switch ");
     var cond = Kind.Parser.term;

base/Kind/Parser/term.kind

@@ -1,5 +1,5 @@
 Kind.Parser.term: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     var term = Parser.first_of!([
       Kind.Parser.type,

base/Kind/Parser/text.kind

@@ -1,5 +1,5 @@
 Kind.Parser.text(text: String): Parser(Unit)
-  do Parser {
+  Parser {
     Kind.Parser.spaces;
     Parser.text(text);
   }

base/Kind/Parser/type.kind

@@ -1,5 +1,5 @@
 Kind.Parser.type: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.text("Type");
     var orig = Kind.Parser.stop(init);

base/Kind/Parser/u16.kind

@@ -1,5 +1,5 @@
 Kind.Parser.u16: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.spaces;
     var natx = Parser.nat;

base/Kind/Parser/u32.kind

@@ -1,5 +1,5 @@
 Kind.Parser.u32: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.spaces;
     var natx = Parser.nat;

base/Kind/Parser/u64.kind

@@ -1,5 +1,5 @@
 Kind.Parser.u64: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.spaces;
     var natx = Parser.nat;

base/Kind/Parser/u8.kind

@@ -1,5 +1,5 @@
 Kind.Parser.u8: Parser(Kind.Term)
-  do Parser {
+  Parser {
     var init = Kind.Parser.init;
     Kind.Parser.spaces;
     var natx = Parser.nat;

base/Kind/Synth/file.kind

@@ -1,12 +1,12 @@
 Kind.Synth.file(file: String, defs: Kind.Defs): IO(Either(String, Pair(List(Kind.Name), Kind.Defs)))
-  do IO {
+  IO {
     var code = IO.get_file(file);
     let read = Kind.Defs.read(file, code, defs);
     case read {
-      left: do IO {
+      left: IO {
         return Either.left!!(read.value);
       },
-      right: do IO {
+      right: IO {
         let file_defs = read.value;
         let file_keys = Map.keys!(file_defs);
         let file_nams = List.mapped!(file_keys)!(Kind.Name.from_bits);

base/Kind/Synth/fix.kind

@@ -13,23 +13,23 @@ Kind.Synth.fix(
 ): IO(Maybe(Kind.Defs))
   case errs {
     nil:
-      if fixd then do IO {
+      if fixd then IO {
         let type = Kind.Term.bind([], (x) Bits.i(x), type);
         let term = Kind.Term.bind([], (x) Bits.o(x), term);
         let defs = Kind.set!(name, Kind.Def.new(file, code, orig, name, term, type, isct, arit, Kind.Status.init), defs);
         return Maybe.some!(defs);
-      } else do IO {
+      } else IO {
         return Maybe.none!;
       },
     cons: case errs.head {
-      waiting: do IO {
+      waiting: IO {
         var new_defs = Kind.Synth.one(errs.head.name, defs);
         case new_defs {
           none: Kind.Synth.fix(file, code, orig, name, term, type, isct, arit, defs, errs.tail, fixd),
           some: Kind.Synth.fix(file, code, orig, name, term, type, isct, arit, new_defs.value, errs.tail, Bool.true),
         }
       },
-      undefined_reference: do IO {
+      undefined_reference: IO {
         var new_defs = Kind.Synth.one(errs.head.name, defs);
         case new_defs {
           none: Kind.Synth.fix(file, code, orig, name, term, type, isct, arit, defs, errs.tail, fixd),
@@ -37,14 +37,14 @@ Kind.Synth.fix(
         }
       },
       patch: case errs.head.path {
-        e: do IO { // shouldn't happen
+        e: IO { // shouldn't happen
           return Maybe.none!;
         },
-        o: do IO { // hole is on term
+        o: IO { // hole is on term
           let term = Kind.Term.patch_at(errs.head.path.pred, term, (x) errs.head.term);
           Kind.Synth.fix(file, code, orig, name, term, type, isct, arit, defs, errs.tail, Bool.true);
         },
-        i: do IO { // hole is on type
+        i: IO { // hole is on type
           let type = Kind.Term.patch_at(errs.head.path.pred, type, (x) errs.head.term);
           Kind.Synth.fix(file, code, orig, name, term, type, isct, arit, defs, errs.tail, Bool.true);
         },

base/Kind/Synth/load/go.kind

@@ -1,18 +1,18 @@
 Kind.Synth.load.go(name: String, files: List(String), defs: Kind.Defs): IO(Maybe(Kind.Defs))
   case files {
-    nil: do IO {
+    nil: IO {
       return none
     }
-    cons: do IO {
+    cons: IO {
       var code = IO.get_file(files.head)
       let read = Kind.Defs.read(files.head, code, defs)
       case read {
         left: Kind.Synth.load.go(name, files.tail, defs)
-        right: do IO {
+        right: IO {
           let defs = read.value
           case Kind.get!(name, defs) as got {
             none: Kind.Synth.load.go(name, files.tail, defs),
-            some: do IO {
+            some: IO {
               return some(defs)
             }
           }

base/Kind/Synth/many.kind

@@ -1,9 +1,9 @@
 Kind.Synth.many(names: List(String), defs: Kind.Defs): IO(Kind.Defs)
   case names {
-    nil: do IO {
+    nil: IO {
       return defs;
     },
-    cons: do IO {
+    cons: IO {
       var new_defs = Kind.Synth.one(names.head, defs);
       case new_defs {
         none: Kind.Synth.many(names.tail, defs),

base/Kind/Synth/one.kind

@@ -1,19 +1,19 @@
 Kind.Synth.one(name: Kind.Name, defs: Kind.Defs): IO(Maybe(Kind.Defs))
   //log("synth ", name)
   case Kind.get!(name, defs) as got {
-    none: do IO {
+    none: IO {
       var loaded = Kind.Synth.load(name, defs);
       case loaded {
-        none: do IO {
+        none: IO {
           return none;
         },
-        some: do IO {
+        some: IO {
           Kind.Synth.one(name, loaded.value);
         },
       };
     },
     some: case got.value {
-      new: do IO {
+      new: IO {
         let file = got.value.file;
         let code = got.value.code;
         let orig = got.value.orig;
@@ -26,10 +26,10 @@ Kind.Synth.one(name: Kind.Name, defs: Kind.Defs): IO(Maybe(Kind.Defs))
         //let skip = Debug.log!(String.flatten([name, ": ", Kind.Term.show(type), " = ", Kind.Term.show(term)]), (x) Unit.new);
         //Debug.log!(String.flatten(["synth ", name, " ", case stat { init: "INIT", wait: "WAIT", done: "DONE", fail: "FAIL" }]), (x)
         case stat {
-          wait: do IO { return some(defs); },
-          done: do IO { return some(defs); },
-          fail: do IO { return some(defs); },
-          init: do IO {
+          wait: IO { return some(defs); },
+          done: IO { return some(defs); },
+          fail: IO { return some(defs); },
+          init: IO {
             let defs = Kind.set!(name, Kind.Def.new(file, code, orig, name, term, type, isct, arit, Kind.Status.wait), defs);
             let checked = do Kind.Check {
               var chk_type = Kind.Term.check(type, Maybe.some!(Kind.Term.typ), defs, [], Kind.MPath.i(Kind.MPath.nil), Maybe.none!);
@@ -39,14 +39,14 @@ Kind.Synth.one(name: Kind.Name, defs: Kind.Defs): IO(Maybe(Kind.Defs))
             case checked {
               result:
                 //let skip = Debug.log!(String.join("\n", List.mapped!(checked.errors)!((x) String.concat("-- ", Kind.Error.show(x,Map.new!)))), (x) Unit.new);
-                if List.is_empty!(checked.errors) then do IO {
+                if List.is_empty!(checked.errors) then IO {
                   let defs = Kind.define(file, code, orig, name, term, type, isct, arit, true, defs);
                   //let defs = Kind.set!(name, Kind.Def.new(file, code, name, term, type, Kind.Status.done), defs);
                   return some(defs);
-                } else do IO {
+                } else IO {
                   var fixed = Kind.Synth.fix(file, code, orig, name, term, type, isct, arit, defs, checked.errors, Bool.false);
                   case fixed {
-                    none: do IO {
+                    none: IO {
                       let stat = Kind.Status.fail(checked.errors);
                       let defs = Kind.set!(name, Kind.Def.new(file, code, orig, name, term, type, isct, arit, stat), defs);
                       return some(defs);

base/Kind/checker/code.kind

@@ -2,7 +2,7 @@ Kind.checker.code(code: String): String
   case Kind.Defs.read("Main.kind", code, Map.new!) as read {
     left:
       read.value,
-    right: IO.purify<String>(do IO {
+    right: IO.purify<String>(IO {
       let defs = read.value;
       let nams = List.mapped!(Map.keys!(defs))!(Kind.Name.from_bits);
       var defs = Kind.Synth.many(nams, defs);

base/Kind/checker/io/file.kind

@@ -1,13 +1,13 @@
 Kind.checker.io.file(file: String): IO(Unit)
-  do IO {
+  IO {
     var loaded = Kind.Synth.file(file, Map.new!);
     case loaded {
-      left: do IO {
+      left: IO {
         IO.print(String.flatten(["On '", file, "':"]));
         IO.print(loaded.value);
       }
       right: case loaded.value {
-        new: do IO {
+        new: IO {
           let nams = loaded.value.fst;
           let defs = loaded.value.snd;
           case nams {

base/Kind/checker/io/one.kind

@@ -1,5 +1,5 @@
 Kind.checker.io.one(name: String): IO(Unit)
-  do IO {
+  IO {
     var new_defs = Kind.Synth.one(name, Map.new!);
     case new_defs {
       none:

base/Kind/go.kind

@@ -1,16 +1,16 @@
 Kind.go(file_names: List(String)): IO(Unit)
   case file_names {
-    nil: do IO {
+    nil: IO {
       return Unit.new
     }
-    cons: do IO {
+    cons: IO {
       let file = file_names.head
       var code = IO.get_file(file)
       let defs = Kind.Defs.read(file, code, Map.new!)
       case defs {
         left:
           IO.print("bad parse")
-        right: do IO {
+        right: IO {
           let list = Map.to_list!(defs.value)
           let files = List.mapped!(list)!((kv)
             let {key, val} = kv

base/Kind/to_core/io/one.kind

@@ -1,5 +1,5 @@
 Kind.to_core.io.one(name: String): IO(String)
-  do IO {
+  IO {
     var new_defs = Kind.Synth.one(name, Map.new!);
     let defs = case new_defs {
       none: Map.new!,

base/Main.kind

@@ -1,4 +1,4 @@
 Main: IO(Unit)
-  do IO {
+  IO {
     IO.print("Hello, world!")
   }

base/Parser/consume.kind

@@ -1,6 +1,6 @@
 // TODO: remove Parser.spaces_text
 Parser.consume(text: String): Parser(Unit)
-  do Parser {
+  Parser {
     Parser.spaces;
     Parser.text(text);
   }

base/Parser/many1.kind

@@ -1,5 +1,5 @@
 Parser.many1<V: Type>(parser: Parser(V)): Parser(List(V))
-  do Parser {
+  Parser {
     var head = parser;
     var tail = Parser.many<V>(parser);
     return List.cons<V>(head, tail);

base/Parser/nat.kind

@@ -1,5 +1,5 @@
 Parser.nat: Parser(Nat)
-  do Parser {
+  Parser {
     var digits = Parser.many1<Nat>(Parser.digit);
     return Nat.from_base(10, digits);
   }

base/Parser/spaces_text.kind

@@ -1,5 +1,5 @@
 Parser.spaces_text(text: String): Parser(Unit)
-  do Parser {
+  Parser {
     Parser.spaces;
     Parser.text(text);
   }

base/Parser/until1.kind

@@ -1,5 +1,5 @@
 Parser.until1<V: Type>(cond: Parser(Unit), parser: Parser(V)): Parser(List(V))
-  do Parser {
+  Parser {
     var head = parser;
     var tail = Parser.until<V>(cond, parser);
     return List.cons<V>(head, tail);