feat(frontends/lean): add support for monadic 'do'-notation

library/init/string.lean

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 prelude
 import init.char
 
-definition string := list char
+definition string [reducible] := list char
 
 namespace string
 definition empty : string := list.nil

src/emacs/lean-syntax.el

@@ -20,7 +20,7 @@
     "using" "namespace" "section" "fields" "find_decl"
     "attribute" "local" "set_option" "extends" "include" "omit" "classes"
     "instances" "coercions" "metaclasses" "raw" "migrate" "replacing"
-    "calc" "have" "show" "suffices" "by" "in" "at" "let" "forall" "Pi" "fun"
+    "calc" "have" "show" "suffices" "by" "in" "at" "do" "let" "forall" "Pi" "fun"
     "exists" "if" "dif" "then" "else" "assume" "assert" "take"
     "obtain" "from" "aliases")
   "lean keywords ending with 'word' (not symbol)")

src/frontends/lean/builtin_exprs.cpp

@@ -514,6 +514,61 @@ static expr parse_pattern(parser & p, unsigned, expr const * args, pos_info cons
     throw parser_error("pattern_hints have been disabled", pos);
 }
 
+static expr parse_do(parser & p, unsigned, expr const *, pos_info const & pos) {
+    parser::local_scope scope(p);
+    buffer<expr> es;
+    buffer<expr> locals;
+    while (true) {
+        expr curr;
+        optional<name> id;
+        auto id_pos = p.pos();
+        if (p.curr_is_identifier()) {
+            id = p.get_name_val();
+            p.next();
+            if (p.curr_is_token(get_larrow_tk())) {
+                p.next();
+                curr = p.parse_expr();
+            } else {
+                expr left = p.id_to_expr(*id, id_pos);
+                id        = optional<name>();
+                unsigned rbp = 0;
+                while (rbp < p.curr_expr_lbp()) {
+                    left = p.parse_led(left);
+                }
+                curr = left;
+            }
+        } else {
+            id   = optional<name>();
+            curr = p.parse_expr();
+        }
+        es.push_back(curr);
+        if (p.curr_is_token(get_comma_tk())) {
+            p.next();
+            name n = id ? *id : mk_fresh_name();
+            expr l = p.save_pos(mk_local(n, mk_expr_placeholder()), id_pos);
+            p.add_local(l);
+            locals.push_back(l);
+        } else {
+            if (id) {
+                throw parser_error("invalid 'do' expression, unnecessary binder", id_pos);
+            }
+            break;
+        }
+    }
+    lean_assert(!es.empty());
+    lean_assert(es.size() == locals.size() + 1);
+    if (es.size() == 1)
+        return es[0];
+    unsigned i = es.size();
+    --i;
+    expr r = es[i];
+    while (i > 0) {
+        --i;
+        r = mk_app(mk_constant(get_monad_bind_name()), es[i], Fun(locals[i], r));
+    }
+    return r;
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -550,6 +605,7 @@ parse_table init_nud_table() {
     r = r.add({transition("using", mk_ext_action(parse_using))}, x0);
     r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0);
     r = r.add({transition("match", mk_ext_action(parse_match))}, x0);
+    r = r.add({transition("do", mk_ext_action(parse_do))}, x0);
     init_structure_instance_parsing_rules(r);
     return r;
 }

src/frontends/lean/token_table.cpp

@@ -101,7 +101,7 @@ void init_token_table(token_table & t) {
          {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"#tactic", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec},
          {"proof", g_max_prec}, {"qed", 0}, {"@@", g_max_prec}, {"@", g_max_prec},
-         {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
+         {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"<-", 0},
          {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},
          {"<d", g_decreasing_prec}, {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
 
@@ -154,6 +154,7 @@ void init_token_table(token_table & t) {
         it3++;
     }
     t = add_token(t, g_arrow_unicode, "->", get_arrow_prec());
+    t = add_token(t, "←", "<-", 0);
     t = add_token(t, g_decreasing_unicode, "<d", get_decreasing_prec());
 
     auto it4 = cmd_aliases;

src/frontends/lean/tokens.cpp

@@ -63,6 +63,7 @@ static name const * g_instances_tk = nullptr;
 static name const * g_classes_tk = nullptr;
 static name const * g_coercions_tk = nullptr;
 static name const * g_arrow_tk = nullptr;
+static name const * g_larrow_tk = nullptr;
 static name const * g_declaration_tk = nullptr;
 static name const * g_decl_tk = nullptr;
 static name const * g_hiding_tk = nullptr;
@@ -211,6 +212,7 @@ void initialize_tokens() {
     g_classes_tk = new name{"classes"};
     g_coercions_tk = new name{"coercions"};
     g_arrow_tk = new name{"->"};
+    g_larrow_tk = new name{"<-"};
     g_declaration_tk = new name{"declaration"};
     g_decl_tk = new name{"decl"};
     g_hiding_tk = new name{"hiding"};
@@ -360,6 +362,7 @@ void finalize_tokens() {
     delete g_classes_tk;
     delete g_coercions_tk;
     delete g_arrow_tk;
+    delete g_larrow_tk;
     delete g_declaration_tk;
     delete g_decl_tk;
     delete g_hiding_tk;
@@ -508,6 +511,7 @@ name const & get_instances_tk() { return *g_instances_tk; }
 name const & get_classes_tk() { return *g_classes_tk; }
 name const & get_coercions_tk() { return *g_coercions_tk; }
 name const & get_arrow_tk() { return *g_arrow_tk; }
+name const & get_larrow_tk() { return *g_larrow_tk; }
 name const & get_declaration_tk() { return *g_declaration_tk; }
 name const & get_decl_tk() { return *g_decl_tk; }
 name const & get_hiding_tk() { return *g_hiding_tk; }

src/frontends/lean/tokens.h

@@ -65,6 +65,7 @@ name const & get_instances_tk();
 name const & get_classes_tk();
 name const & get_coercions_tk();
 name const & get_arrow_tk();
+name const & get_larrow_tk();
 name const & get_declaration_tk();
 name const & get_decl_tk();
 name const & get_hiding_tk();

src/frontends/lean/tokens.txt

@@ -58,6 +58,7 @@ instances    instances
 classes      classes
 coercions    coercions
 arrow        ->
+larrow       <-
 declaration  declaration
 decl         decl
 hiding       hiding

src/library/constants.cpp

@@ -51,6 +51,8 @@ name const * g_eq_trans = nullptr;
 name const * g_eq_of_heq = nullptr;
 name const * g_eq_rec_heq = nullptr;
 name const * g_exists_elim = nullptr;
+name const * g_functor = nullptr;
+name const * g_functorIO = nullptr;
 name const * g_false = nullptr;
 name const * g_false_of_true_iff_false = nullptr;
 name const * g_false_rec = nullptr;
@@ -101,6 +103,11 @@ name const * g_linear_ordered_semiring = nullptr;
 name const * g_list = nullptr;
 name const * g_list_nil = nullptr;
 name const * g_list_cons = nullptr;
+name const * g_monad = nullptr;
+name const * g_monad_map = nullptr;
+name const * g_monad_bind = nullptr;
+name const * g_monad_return = nullptr;
+name const * g_monadIO = nullptr;
 name const * g_monoid = nullptr;
 name const * g_mul = nullptr;
 name const * g_mul_one = nullptr;
@@ -349,6 +356,8 @@ void initialize_constants() {
     g_eq_of_heq = new name{"eq_of_heq"};
     g_eq_rec_heq = new name{"eq_rec_heq"};
     g_exists_elim = new name{"exists", "elim"};
+    g_functor = new name{"functor"};
+    g_functorIO = new name{"functorIO"};
     g_false = new name{"false"};
     g_false_of_true_iff_false = new name{"false_of_true_iff_false"};
     g_false_rec = new name{"false", "rec"};
@@ -399,6 +408,11 @@ void initialize_constants() {
     g_list = new name{"list"};
     g_list_nil = new name{"list", "nil"};
     g_list_cons = new name{"list", "cons"};
+    g_monad = new name{"monad"};
+    g_monad_map = new name{"monad", "map"};
+    g_monad_bind = new name{"monad", "bind"};
+    g_monad_return = new name{"monad", "return"};
+    g_monadIO = new name{"monadIO"};
     g_monoid = new name{"monoid"};
     g_mul = new name{"mul"};
     g_mul_one = new name{"mul_one"};
@@ -648,6 +662,8 @@ void finalize_constants() {
     delete g_eq_of_heq;
     delete g_eq_rec_heq;
     delete g_exists_elim;
+    delete g_functor;
+    delete g_functorIO;
     delete g_false;
     delete g_false_of_true_iff_false;
     delete g_false_rec;
@@ -698,6 +714,11 @@ void finalize_constants() {
     delete g_list;
     delete g_list_nil;
     delete g_list_cons;
+    delete g_monad;
+    delete g_monad_map;
+    delete g_monad_bind;
+    delete g_monad_return;
+    delete g_monadIO;
     delete g_monoid;
     delete g_mul;
     delete g_mul_one;
@@ -946,6 +967,8 @@ name const & get_eq_trans_name() { return *g_eq_trans; }
 name const & get_eq_of_heq_name() { return *g_eq_of_heq; }
 name const & get_eq_rec_heq_name() { return *g_eq_rec_heq; }
 name const & get_exists_elim_name() { return *g_exists_elim; }
+name const & get_functor_name() { return *g_functor; }
+name const & get_functorIO_name() { return *g_functorIO; }
 name const & get_false_name() { return *g_false; }
 name const & get_false_of_true_iff_false_name() { return *g_false_of_true_iff_false; }
 name const & get_false_rec_name() { return *g_false_rec; }
@@ -996,6 +1019,11 @@ name const & get_linear_ordered_semiring_name() { return *g_linear_ordered_semir
 name const & get_list_name() { return *g_list; }
 name const & get_list_nil_name() { return *g_list_nil; }
 name const & get_list_cons_name() { return *g_list_cons; }
+name const & get_monad_name() { return *g_monad; }
+name const & get_monad_map_name() { return *g_monad_map; }
+name const & get_monad_bind_name() { return *g_monad_bind; }
+name const & get_monad_return_name() { return *g_monad_return; }
+name const & get_monadIO_name() { return *g_monadIO; }
 name const & get_monoid_name() { return *g_monoid; }
 name const & get_mul_name() { return *g_mul; }
 name const & get_mul_one_name() { return *g_mul_one; }

src/library/constants.h

@@ -53,6 +53,8 @@ name const & get_eq_trans_name();
 name const & get_eq_of_heq_name();
 name const & get_eq_rec_heq_name();
 name const & get_exists_elim_name();
+name const & get_functor_name();
+name const & get_functorIO_name();
 name const & get_false_name();
 name const & get_false_of_true_iff_false_name();
 name const & get_false_rec_name();
@@ -103,6 +105,11 @@ name const & get_linear_ordered_semiring_name();
 name const & get_list_name();
 name const & get_list_nil_name();
 name const & get_list_cons_name();
+name const & get_monad_name();
+name const & get_monad_map_name();
+name const & get_monad_bind_name();
+name const & get_monad_return_name();
+name const & get_monadIO_name();
 name const & get_monoid_name();
 name const & get_mul_name();
 name const & get_mul_one_name();

src/library/constants.txt

@@ -46,6 +46,8 @@ eq.trans
 eq_of_heq
 eq_rec_heq
 exists.elim
+functor
+functorIO
 false
 false_of_true_iff_false
 false.rec
@@ -96,6 +98,11 @@ linear_ordered_semiring
 list
 list.nil
 list.cons
+monad
+monad.map
+monad.bind
+monad.return
+monadIO
 monoid
 mul
 mul_one