From 18063fa9ba953bbc17979fd45a4dfd92918e4c1a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 30 May 2017 17:10:32 +0200 Subject: [PATCH] feat(frontends/lean): user-defined notation parsers --- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/init_module.cpp | 3 + src/frontends/lean/tactic_notation.cpp | 27 +------- src/frontends/lean/user_notation.cpp | 79 ++++++++++++++++++++++ src/frontends/lean/user_notation.h | 12 ++++ src/library/constants.cpp | 8 +++ src/library/constants.h | 2 + src/library/constants.txt | 2 + src/library/vm/vm_parser.cpp | 47 ++++++++++--- src/library/vm/vm_parser.h | 2 + tests/lean/run/check_constants.lean | 2 + tests/lean/user_notation.lean | 36 ++++++++++ tests/lean/user_notation.lean.expected.out | 12 ++++ 13 files changed, 197 insertions(+), 37 deletions(-) create mode 100644 src/frontends/lean/user_notation.cpp create mode 100644 src/frontends/lean/user_notation.h create mode 100644 tests/lean/user_notation.lean create mode 100644 tests/lean/user_notation.lean.expected.out diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index f4b24c0287..0a39b218f1 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/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) diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 34c7ef7e29..380117e0cd 100644 --- a/src/frontends/lean/init_module.cpp +++ b/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(); diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index 431c08a35c..20155f870c 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/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 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 { diff --git a/src/frontends/lean/user_notation.cpp b/src/frontends/lean/user_notation.cpp new file mode 100644 index 0000000000..7ee14c1136 --- /dev/null +++ b/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() { +} +} diff --git a/src/frontends/lean/user_notation.h b/src/frontends/lean/user_notation.h new file mode 100644 index 0000000000..5ffd339de6 --- /dev/null +++ b/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(); +} diff --git a/src/library/constants.cpp b/src/library/constants.cpp index b4f94c7197..b357111eb6 100644 --- a/src/library/constants.cpp +++ b/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; } diff --git a/src/library/constants.h b/src/library/constants.h index d946730f23..6aa4e04a89 100644 --- a/src/library/constants.h +++ b/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(); diff --git a/src/library/constants.txt b/src/library/constants.txt index cd05861609..104de4dac6 100644 --- a/src/library/constants.txt +++ b/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 diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp index 0991995341..0e247d9f43 100644 --- a/src/library/vm/vm_parser.cpp +++ b/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 #include #include -#include -#include -#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 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); } diff --git a/src/library/vm/vm_parser.h b/src/library/vm/vm_parser.h index 70cf408b9e..4e583f984b 100644 --- a/src/library/vm/vm_parser.h +++ b/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(); } diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean index d699b598cf..05d2beb1c8 100644 --- a/tests/lean/run/check_constants.lean +++ b/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 diff --git a/tests/lean/user_notation.lean b/tests/lean/user_notation.lean new file mode 100644 index 0000000000..3398ae2049 --- /dev/null +++ b/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 diff --git a/tests/lean/user_notation.lean.expected.out b/tests/lean/user_notation.lean.expected.out new file mode 100644 index 0000000000..012ed60424 --- /dev/null +++ b/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])))) : + ℕ