feat(frontends/lean): user-defined notation parsers

src/frontends/lean/CMakeLists.txt

@@ -8,4 +8,4 @@ init_module.cpp type_util.cpp decl_attributes.cpp
 prenum.cpp print_cmd.cpp elaborator.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
 brackets.cpp tactic_notation.cpp info_manager.cpp json.cpp module_parser.cpp
-equations_validator.cpp parser_state.cpp interactive.cpp completion.cpp)
+equations_validator.cpp parser_state.cpp interactive.cpp completion.cpp user_notation.cpp)

src/frontends/lean/init_module.cpp

@@ -28,6 +28,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/brackets.h"
 #include "frontends/lean/interactive.h"
 #include "frontends/lean/completion.h"
+#include "frontends/lean/user_notation.h"
 
 namespace lean {
 void initialize_frontend_lean_module() {
@@ -55,8 +56,10 @@ void initialize_frontend_lean_module() {
     initialize_brackets();
     initialize_interactive();
     initialize_completion();
+    initialize_user_notation();
 }
 void finalize_frontend_lean_module() {
+    finalize_user_notation();
     finalize_completion();
     finalize_interactive();
     finalize_brackets();

src/frontends/lean/tactic_notation.cpp

@@ -137,28 +137,6 @@ static expr parse_nested_interactive_tactic(parser & p, name const & tac_class,
     }
 }
 
-static expr parse_interactive_param(parser & p, expr const & ty, expr const & quote_inst, expr const & lean_parser) {
-    try {
-        vm_obj vm_parsed = run_parser(p, lean_parser);
-        type_context ctx(p.env());
-        name n("_quote_inst");
-        tactic_evaluator eval(ctx, p.get_options(), ty);
-        auto env = eval.compile(n, quote_inst);
-        vm_state S(env, p.get_options());
-        auto vm_res = S.invoke(n, vm_parsed);
-        expr r = to_expr(vm_res);
-        if (is_app_of(r, get_expr_subst_name())) {
-            return r; // HACK
-        } else {
-            return mk_as_is(r);
-        }
-    } catch (exception & ex) {
-        if (!p.has_error_recovery()) throw;
-        p.mk_message(ERROR).set_exception(ex).report();
-        return p.mk_sorry(p.pos(), true);
-    }
-}
-
 static expr parse_interactive_tactic(parser & p, name const & decl_name, name const & tac_class, bool use_istep) {
     auto pos = p.pos();
     expr type     = p.env().get(decl_name).get_type();
@@ -172,10 +150,7 @@ static expr parse_interactive_tactic(parser & p, name const & decl_name, name co
                 if (is_explicit(binding_info(type))) {
                     expr arg_type = binding_domain(type);
                     if (is_app_of(arg_type, get_interactive_parse_name())) {
-                        buffer<expr> arg_args;
-                        get_app_args(arg_type, arg_args);
-                        lean_assert(arg_args.size() == 3);
-                        args.push_back(parse_interactive_param(p, arg_args[0], arg_args[1], arg_args[2]));
+                        args.push_back(parse_interactive_param(p, arg_type));
                     } else if (is_constant(arg_type, itactic)) {
                         args.push_back(parse_nested_interactive_tactic(p, tac_class, use_istep));
                     } else {

src/frontends/lean/user_notation.cpp

@@ -0,0 +1,79 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Sebastian Ullrich
+*/
+#include "kernel/abstract.h"
+#include "library/constants.h"
+#include "library/attribute_manager.h"
+#include "library/tactic/elaborator_exception.h"
+#include "library/string.h"
+#include "library/vm/vm_expr.h"
+#include "library/vm/vm_parser.h"
+#include "library/quote.h"
+#include "frontends/lean/elaborator.h"
+
+namespace lean {
+static environment add_user_notation(environment const & env, name const & d, unsigned prio, bool persistent) {
+    auto type = env.get(d).get_type();
+    bool is_nud = true;
+    name tk;
+    if (is_app_of(binding_domain(type), get_interactive_parse_name(), 3)) {
+        auto const & parser = app_arg(binding_domain(type));
+        if (is_app_of(parser, get_lean_parser_qexpr_name(), 1)) {
+            is_nud = false;
+            type = binding_body(type);
+        }
+    }
+    if (is_app_of(binding_domain(type), get_interactive_parse_name(), 3)) {
+        auto const & parser = app_arg(binding_domain(type));
+        if (is_app_of(parser, get_lean_parser_tk_name(), 1)) {
+            if (auto lit = to_string(app_arg(parser))) {
+                tk = *lit;
+                type = binding_body(type);
+            } else {
+                throw elaborator_exception(app_arg(parser),
+                                           "invalid user-defined notation, token must be a name literal");
+            }
+        }
+    }
+    if (!tk) {
+        throw exception("invalid user-defined notation, must start with `interactive.parse (lean.parser.tk c)` "
+                                "parameter, optionally preceded by `interactive.parse lean.parser.qexpr` parameter");
+    }
+    expr dummy = mk_true();
+    return add_notation(env, notation_entry(is_nud, {notation::transition(tk, notation::mk_ext_action(
+            [=](parser & p, unsigned num, expr const * args, pos_info const &) -> expr {
+                lean_assert(num == (is_nud ? 0 : 1));
+                expr tactic = mk_constant(d);
+                if (!is_nud)
+                    tactic = mk_app(tactic, mk_pexpr_quote(args[0]));
+                // `parse (tk c)` arg
+                tactic = mk_app(tactic, mk_constant(get_unit_star_name()));
+                for (expr t = type; is_pi(t); t = binding_body(t)) {
+                    expr arg_type = binding_domain(t);
+                    if (is_app_of(arg_type, get_interactive_parse_name())) {
+                        tactic = mk_app(tactic, parse_interactive_param(p, arg_type));
+                    } else {
+                        tactic = mk_app(tactic, p.parse_expr(get_max_prec()));
+                    }
+                }
+                tactic = p.elaborate("_user_notation", {}, tactic).first;
+                tactic_state s = mk_tactic_state_for(p.env(), p.get_options(), "_user_notation", local_context(), dummy);
+                type_context ctx(p.env());
+                auto result = tactic::evaluator(ctx, p.get_options())(tactic, s);
+                return to_expr(tactic::get_result_value(result));
+            }))}, Var(0), /* overload */ persistent, prio, notation_entry_group::Main, /* parse_only */ true));
+}
+
+void initialize_user_notation() {
+    register_system_attribute(basic_attribute(
+            "user_notation", "user-defined notation",
+            [](environment const & env, io_state const &, name const & d, unsigned prio, bool persistent) {
+                return add_user_notation(env, d, prio, persistent);
+            }));
+}
+void finalize_user_notation() {
+}
+}

src/frontends/lean/user_notation.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Sebastian Ullrich
+*/
+#pragma once
+
+namespace lean {
+void initialize_user_notation();
+void finalize_user_notation();
+}

src/library/constants.cpp

@@ -174,6 +174,8 @@ name const * g_is_associative_assoc = nullptr;
 name const * g_is_commutative = nullptr;
 name const * g_is_commutative_comm = nullptr;
 name const * g_ite = nullptr;
+name const * g_lean_parser_qexpr = nullptr;
+name const * g_lean_parser_tk = nullptr;
 name const * g_left_distrib = nullptr;
 name const * g_left_comm = nullptr;
 name const * g_le_refl = nullptr;
@@ -542,6 +544,8 @@ void initialize_constants() {
     g_is_commutative = new name{"is_commutative"};
     g_is_commutative_comm = new name{"is_commutative", "comm"};
     g_ite = new name{"ite"};
+    g_lean_parser_qexpr = new name{"lean", "parser", "qexpr"};
+    g_lean_parser_tk = new name{"lean", "parser", "tk"};
     g_left_distrib = new name{"left_distrib"};
     g_left_comm = new name{"left_comm"};
     g_le_refl = new name{"le_refl"};
@@ -911,6 +915,8 @@ void finalize_constants() {
     delete g_is_commutative;
     delete g_is_commutative_comm;
     delete g_ite;
+    delete g_lean_parser_qexpr;
+    delete g_lean_parser_tk;
     delete g_left_distrib;
     delete g_left_comm;
     delete g_le_refl;
@@ -1279,6 +1285,8 @@ name const & get_is_associative_assoc_name() { return *g_is_associative_assoc; }
 name const & get_is_commutative_name() { return *g_is_commutative; }
 name const & get_is_commutative_comm_name() { return *g_is_commutative_comm; }
 name const & get_ite_name() { return *g_ite; }
+name const & get_lean_parser_qexpr_name() { return *g_lean_parser_qexpr; }
+name const & get_lean_parser_tk_name() { return *g_lean_parser_tk; }
 name const & get_left_distrib_name() { return *g_left_distrib; }
 name const & get_left_comm_name() { return *g_left_comm; }
 name const & get_le_refl_name() { return *g_le_refl; }

src/library/constants.h

@@ -176,6 +176,8 @@ name const & get_is_associative_assoc_name();
 name const & get_is_commutative_name();
 name const & get_is_commutative_comm_name();
 name const & get_ite_name();
+name const & get_lean_parser_qexpr_name();
+name const & get_lean_parser_tk_name();
 name const & get_left_distrib_name();
 name const & get_left_comm_name();
 name const & get_le_refl_name();

src/library/constants.txt

@@ -169,6 +169,8 @@ is_associative.assoc
 is_commutative
 is_commutative.comm
 ite
+lean.parser.qexpr
+lean.parser.tk
 left_distrib
 left_comm
 le_refl

src/library/vm/vm_parser.cpp

@@ -4,25 +4,25 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Sebastian Ullrich
 */
-#include "library/vm/vm_parser.h"
 #include <string>
 #include <iostream>
 #include <vector>
-#include <library/num.h>
-#include <library/quote.h>
-#include "frontends/lean/parser.h"
-#include "library/trace.h"
 #include "library/type_context.h"
-#include "frontends/lean/info_manager.h"
-#include "frontends/lean/elaborator.h"
+#include "library/num.h"
+#include "library/quote.h"
+#include "library/trace.h"
+#include "library/tactic/tactic_evaluator.h"
+#include "library/explicit.h"
 #include "library/tactic/elaborate.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_string.h"
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_nat.h"
-#include "library/vm/vm_name.h"
+#include "library/vm/vm_parser.h"
 #include "library/vm/vm_pos_info.h"
 #include "library/vm/interaction_state_imp.h"
+#include "frontends/lean/info_manager.h"
+#include "frontends/lean/elaborator.h"
 
 namespace lean {
 
@@ -43,6 +43,33 @@ vm_obj run_parser(parser & p, expr const & spec) {
     return lean_parser::get_result_value(lean_parser::evaluator(ctx, p.get_options())(spec, lean_parser_state {&p}));
 }
 
+expr parse_interactive_param(parser & p, expr const & param_ty) {
+    lean_assert(is_app_of(param_ty, get_interactive_parse_name()));
+    buffer<expr> param_args;
+    get_app_args(param_ty, param_args);
+    // alpha, has_reflect alpha, parser alpha
+    lean_assert(param_args.size() == 3);
+    try {
+        vm_obj vm_parsed = run_parser(p, param_args[2]);
+        type_context ctx(p.env());
+        name n("_reflect");
+        tactic_evaluator eval(ctx, p.get_options(), param_args[0]);
+        auto env = eval.compile(n, param_args[1]);
+        vm_state S(env, p.get_options());
+        auto vm_res = S.invoke(n, vm_parsed);
+        expr r = to_expr(vm_res);
+        if (is_app_of(r, get_expr_subst_name())) {
+            return r; // HACK
+        } else {
+            return mk_as_is(r);
+        }
+    } catch (exception & ex) {
+        if (!p.has_error_recovery()) throw;
+        p.mk_message(ERROR).set_exception(ex).report();
+        return p.mk_sorry(p.pos(), true);
+    }
+}
+
 vm_obj vm_parser_state_cur_pos(vm_obj const & o) {
     auto const & s = lean_parser::to_state(o);
     return to_obj(s.m_p->pos());
@@ -102,8 +129,8 @@ vm_obj vm_parser_set_goal_info_pos(vm_obj const &, vm_obj const & vm_p, vm_obj c
 void initialize_vm_parser() {
     DECLARE_VM_BUILTIN(name({"lean", "parser_state", "cur_pos"}),     vm_parser_state_cur_pos);
     DECLARE_VM_BUILTIN(name({"lean", "parser", "ident"}),             vm_parser_ident);
-    DECLARE_VM_BUILTIN(name({"lean", "parser", "tk"}),                vm_parser_tk);
-    DECLARE_VM_BUILTIN(name({"lean", "parser", "qexpr"}),             vm_parser_qexpr);
+    DECLARE_VM_BUILTIN(get_lean_parser_tk_name(),                     vm_parser_tk);
+    DECLARE_VM_BUILTIN(get_lean_parser_qexpr_name(),                  vm_parser_qexpr);
     DECLARE_VM_BUILTIN(name({"lean", "parser", "skip_info"}),         vm_parser_skip_info);
     DECLARE_VM_BUILTIN(name({"lean", "parser", "set_goal_info_pos"}), vm_parser_set_goal_info_pos);
 }

src/library/vm/vm_parser.h

@@ -10,6 +10,8 @@ Author: Sebastian Ullrich
 
 namespace lean {
 vm_obj run_parser(parser & p, expr const & spec);
+expr parse_interactive_param(parser & p, expr const & param_ty);
+
 void initialize_vm_parser();
 void finalize_vm_parser();
 }

tests/lean/run/check_constants.lean

@@ -174,6 +174,8 @@ run_cmd script_check_id `is_associative.assoc
 run_cmd script_check_id `is_commutative
 run_cmd script_check_id `is_commutative.comm
 run_cmd script_check_id `ite
+run_cmd script_check_id `lean.parser.qexpr
+run_cmd script_check_id `lean.parser.tk
 run_cmd script_check_id `left_distrib
 run_cmd script_check_id `left_comm
 run_cmd script_check_id `le_refl

tests/lean/user_notation.lean

@@ -0,0 +1,36 @@
+open lean.parser
+open interactive
+open tactic
+
+reserve prefix `unquote! `:100
+@[user_notation]
+meta def unquote_macro (_ : parse $ tk "unquote!") (e : parse qexpr) : tactic pexpr :=
+to_expr e >>= eval_expr pexpr
+
+meta def e := ``(1 + 1)
+#eval unquote! e
+
+private meta def parse_format : string → string → ℕ × pexpr
+| acc [] := (0, pexpr.of_expr (reflect acc))
+| acc ('{'::'{'::s) := parse_format (acc ++ "{") s
+| acc ('{'::'}'::s) :=
+  let (n, f) := parse_format [] s in
+  (n + 1, ``(to_fmt %%(reflect acc) ++ to_fmt %%(expr.var n : pexpr) ++ %%f))
+| acc (c::s) := parse_format (acc ++ [c]) s
+
+reserve prefix `format! `:100
+@[user_notation]
+meta def format_macro (_ : parse $ tk "format!") (s : string) : tactic pexpr :=
+let (n, f) := parse_format "" s.reverse in
+pure $ n.repeat (λ _ e, expr.lam `_ binder_info.default pexpr.mk_placeholder e) f
+
+#eval format! "a{}c" "b"
+-- #eval format! "{} {}" "a" "bla" -- TODO: delayed abstractions issue
+
+reserve infix ` +⋯+ `:65
+@[user_notation]
+meta def upto_notation (e₁ : parse qexpr) (_ : parse $ tk "+⋯+") (n₂ : ℕ) : tactic pexpr :=
+do n₁ ← to_expr e₁ >>= eval_expr nat,
+   pure $ (n₂+1-n₁).repeat (λ i e, ``(%%e + %%(reflect $ n₁ + i))) ``(0)
+
+#check 1 +⋯+ 10

tests/lean/user_notation.lean.expected.out

@@ -0,0 +1,12 @@
+2
+abc
+0 + (bit1 [nat_value_macro] + [nat_value_macro]) + (bit1 [nat_value_macro] + bit1 [nat_value_macro]) +
+                (bit1 [nat_value_macro] + bit0 (bit1 [nat_value_macro])) +
+              (bit1 [nat_value_macro] + bit1 (bit1 [nat_value_macro])) +
+            (bit1 [nat_value_macro] + bit0 (bit0 (bit1 [nat_value_macro]))) +
+          (bit1 [nat_value_macro] + bit1 (bit0 (bit1 [nat_value_macro]))) +
+        (bit1 [nat_value_macro] + bit0 (bit1 (bit1 [nat_value_macro]))) +
+      (bit1 [nat_value_macro] + bit1 (bit1 (bit1 [nat_value_macro]))) +
+    (bit1 [nat_value_macro] + bit0 (bit0 (bit0 (bit1 [nat_value_macro])))) +
+  (bit1 [nat_value_macro] + bit1 (bit0 (bit0 (bit1 [nat_value_macro])))) :
+  ℕ