From 4d3ff955d32ba4e6d4837fc312465243b44e262b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Jan 2017 15:24:18 -0800 Subject: [PATCH] feat(frontends/lean): nicer syntax for default parameter values See #1340 --- src/frontends/lean/decl_util.cpp | 9 ++-- src/frontends/lean/decl_util.h | 6 ++- src/frontends/lean/definition_cmds.cpp | 3 +- src/frontends/lean/parser.cpp | 32 ++++++++++--- src/frontends/lean/parser.h | 27 +++++------ tests/lean/run/default_param2.lean | 65 ++++++++++++++++++++++++++ 6 files changed, 116 insertions(+), 26 deletions(-) create mode 100644 tests/lean/run/default_param2.lean diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index 896fd5906b..4d42e42217 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/src/frontends/lean/decl_util.cpp @@ -43,7 +43,7 @@ bool parse_univ_params(parser & p, buffer & lp_names) { } expr parse_single_header(parser & p, buffer & lp_names, buffer & params, - bool is_example, bool is_instance) { + bool is_example, bool is_instance, bool allow_default) { lean_assert(!is_example || !is_instance); auto c_pos = p.pos(); name c_name; @@ -56,7 +56,7 @@ expr parse_single_header(parser & p, buffer & lp_names, buffer & par c_name = p.check_decl_id_next("invalid declaration, identifier expected"); } declaration_name_scope scope(c_name); - p.parse_optional_binders(params); + p.parse_optional_binders(params, allow_default); for (expr const & param : params) p.add_local(param); expr type; @@ -85,7 +85,8 @@ expr parse_single_header(parser & p, buffer & lp_names, buffer & par return p.save_pos(mk_local(c_name, type), c_pos); } -void parse_mutual_header(parser & p, buffer & lp_names, buffer & cs, buffer & params) { +void parse_mutual_header(parser & p, buffer & lp_names, buffer & cs, buffer & params, + bool allow_default) { parse_univ_params(p, lp_names); while (true) { auto c_pos = p.pos(); @@ -95,7 +96,7 @@ void parse_mutual_header(parser & p, buffer & lp_names, buffer & cs, break; p.next(); } - p.parse_optional_binders(params); + p.parse_optional_binders(params, allow_default); for (expr const & param : params) p.add_local(param); for (expr const & c : cs) diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h index 8a41dca885..aa7962a558 100644 --- a/src/frontends/lean/decl_util.h +++ b/src/frontends/lean/decl_util.h @@ -42,7 +42,8 @@ bool parse_univ_params(parser & p, buffer & lp_names); \remark Caller is responsible for using: parser::local_scope scope2(p, env); */ expr parse_single_header(parser & p, buffer & lp_names, buffer & params, - bool is_example = false, bool is_instance = false); + bool is_example = false, bool is_instance = false, + bool allow_default = false); /** \brief Parse the header of a mutually recursive declaration. It has the form {u_1 ... u_k} id_1, ... id_n (params) @@ -56,7 +57,8 @@ expr parse_single_header(parser & p, buffer & lp_names, buffer & par \remark Caller is responsible for adding expressions encoding the c_names to the parser scope. \remark Caller is responsible for using: parser::local_scope scope2(p, env); */ -void parse_mutual_header(parser & p, buffer & lp_names, buffer & cs, buffer & params); +void parse_mutual_header(parser & p, buffer & lp_names, buffer & cs, buffer & params, + bool allow_default = false); /** \brief Parse the header for one of the declarations in a mutually recursive declaration. It has the form diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 822abefe53..6d967d6d10 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -173,7 +173,8 @@ static expr_pair parse_definition(parser & p, buffer & lp_names, buffer> const & names, return true; } +static expr mk_opt_param(expr const & t, expr const & val) { + return copy_tag(val, mk_app(copy_tag(val, mk_constant(get_opt_param_name())), t, val)); +} + /** \brief Parse ID ... ID ':' expr, where the expression represents the type of the identifiers. */ -void parser::parse_binder_block(buffer & r, binder_info const & bi, unsigned rbp) { +void parser::parse_binder_block(buffer & r, binder_info const & bi, unsigned rbp, bool allow_default) { buffer> names; while (curr_is_identifier() || curr_is_token(get_placeholder_tk())) { auto p = pos(); @@ -1030,6 +1034,15 @@ void parser::parse_binder_block(buffer & r, binder_info const & bi, unsign if (curr_is_token(get_colon_tk())) { next(); type = parse_expr(rbp); + if (allow_default && curr_is_token(get_assign_tk())) { + next(); + expr val = parse_expr(rbp); + type = mk_opt_param(*type, val); + } + } else if (allow_default && curr_is_token(get_assign_tk())) { + next(); + expr val = parse_expr(rbp); + type = mk_opt_param(copy_tag(val, mk_expr_placeholder()), val); } else if (parse_binder_collection(names, bi, r)) { return; } @@ -1077,12 +1090,19 @@ void parser::parse_inst_implicit_decl(buffer & r) { } void parser::parse_binders_core(buffer & r, buffer * nentries, - bool & last_block_delimited, unsigned rbp, bool simple_only) { + bool & last_block_delimited, unsigned rbp, bool simple_only, + bool allow_default) { while (true) { if (curr_is_identifier() || curr_is_token(get_placeholder_tk())) { - parse_binder_block(r, binder_info(), rbp); + /* We only allow the default parameter value syntax for declarations with + surrounded by () */ + bool new_allow_default = false; + parse_binder_block(r, binder_info(), rbp, new_allow_default); last_block_delimited = false; } else { + /* We only allow the default parameter value syntax for declarations with + surrounded by () */ + bool new_allow_default = allow_default && curr_is_token(get_lparen_tk()); optional bi = parse_optional_binder_info(simple_only); if (bi) { rbp = 0; @@ -1091,7 +1111,7 @@ void parser::parse_binders_core(buffer & r, buffer * nentr parse_inst_implicit_decl(r); } else { if (simple_only || !parse_local_notation_decl(nentries)) - parse_binder_block(r, *bi, rbp); + parse_binder_block(r, *bi, rbp, new_allow_default); } parse_close_binder_info(bi); } else { @@ -1103,11 +1123,11 @@ void parser::parse_binders_core(buffer & r, buffer * nentr local_environment parser::parse_binders(buffer & r, buffer * nentries, bool & last_block_delimited, bool allow_empty, unsigned rbp, - bool simple_only) { + bool simple_only, bool allow_default) { flet save1(m_env, m_env); // save environment flet save2(m_local_decls, m_local_decls); unsigned old_sz = r.size(); - parse_binders_core(r, nentries, last_block_delimited, rbp, simple_only); + parse_binders_core(r, nentries, last_block_delimited, rbp, simple_only, allow_default); if (!allow_empty && old_sz == r.size()) throw_invalid_open_binder(pos()); return local_environment(m_env); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 9825bccb97..5e3d745392 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -222,10 +222,11 @@ class parser : public abstract_parser { void parse_inst_implicit_decl(buffer & r); expr parse_binder_core(binder_info const & bi, unsigned rbp); bool parse_binder_collection(buffer> const & names, binder_info const & bi, buffer & r); - void parse_binder_block(buffer & r, binder_info const & bi, unsigned rbp); - void parse_binders_core(buffer & r, buffer * nentries, bool & last_block_delimited, unsigned rbp, bool simple_only); + void parse_binder_block(buffer & r, binder_info const & bi, unsigned rbp, bool allow_default); + void parse_binders_core(buffer & r, buffer * nentries, bool & last_block_delimited, unsigned rbp, + bool simple_only, bool allow_default); local_environment parse_binders(buffer & r, buffer * nentries, bool & last_block_delimited, - bool allow_empty, unsigned rbp, bool simple_only); + bool allow_empty, unsigned rbp, bool simple_only, bool allow_default); bool parse_local_notation_decl(buffer * entries); pair, expr> parse_id_tk_expr(name const & tk, unsigned rbp); @@ -371,24 +372,24 @@ public: expr parse_binder(unsigned rbp); local_environment parse_binders(buffer & r, bool & last_block_delimited) { - unsigned rbp = 0; bool allow_empty = false; bool simple_only = false; - return parse_binders(r, nullptr, last_block_delimited, allow_empty, rbp, simple_only); + unsigned rbp = 0; bool allow_empty = false; bool simple_only = false; bool allow_default = false; + return parse_binders(r, nullptr, last_block_delimited, allow_empty, rbp, simple_only, allow_default); } local_environment parse_binders(buffer & r, unsigned rbp) { - bool tmp; bool allow_empty = false; bool simple_only = false; - return parse_binders(r, nullptr, tmp, allow_empty, rbp, simple_only); + bool tmp; bool allow_empty = false; bool simple_only = false; bool allow_default = false; + return parse_binders(r, nullptr, tmp, allow_empty, rbp, simple_only, allow_default); } void parse_simple_binders(buffer & r, unsigned rbp) { - bool tmp; bool allow_empty = false; bool simple_only = true; - parse_binders(r, nullptr, tmp, allow_empty, rbp, simple_only); + bool tmp; bool allow_empty = false; bool simple_only = true; bool allow_default = false; + parse_binders(r, nullptr, tmp, allow_empty, rbp, simple_only, allow_default); } - local_environment parse_optional_binders(buffer & r) { + local_environment parse_optional_binders(buffer & r, bool allow_default = false) { bool tmp; bool allow_empty = true; unsigned rbp = 0; bool simple_only = false; - return parse_binders(r, nullptr, tmp, allow_empty, rbp, simple_only); + return parse_binders(r, nullptr, tmp, allow_empty, rbp, simple_only, allow_default); } local_environment parse_binders(buffer & r, buffer & nentries) { - bool tmp; bool allow_empty = false; unsigned rbp = 0; bool simple_only = false; - return parse_binders(r, &nentries, tmp, allow_empty, rbp, simple_only); + bool tmp; bool allow_empty = false; unsigned rbp = 0; bool simple_only = false; bool allow_default = false; + return parse_binders(r, &nentries, tmp, allow_empty, rbp, simple_only, allow_default); } optional parse_optional_binder_info(bool simple_only = false); binder_info parse_binder_info(bool simple_only = false); diff --git a/tests/lean/run/default_param2.lean b/tests/lean/run/default_param2.lean new file mode 100644 index 0000000000..db1a8955a2 --- /dev/null +++ b/tests/lean/run/default_param2.lean @@ -0,0 +1,65 @@ +universe variable u + +def f (a : nat) (o : nat := 5) := +a + o + +example : f 1 = f 1 5 := +rfl + +check f 1 + +structure config := +(v1 := 10) +(v2 := 20) +(flag := tt) +(ps := ["hello", "world"]) + +def g (a : nat) (c : config := {}) : nat := +if c^.flag then a + c^.v1 else a + c^.v2 + +example : g 1 = 11 := +rfl + +example : g 1 {flag := ff} = 21 := +rfl + +example : g 1 {v1 := 100} = 101 := +rfl + +def h (a : nat) (c : config := {v1 := a}) : nat := +g a c + +example : h 2 = 4 := +rfl + +example : h 3 = 6 := +rfl + +example : h 2 {flag := ff} = 22 := +rfl + +def boo (a : nat) (b : nat := a) (c : bool := ff) (d : config := {v2 := b, flag := c}) := +g a d + +check boo 2 + +example : boo 2 = 4 := +rfl + +example : boo 2 20 = 22 := +rfl + +example : boo 2 0 tt = 12 := +rfl + +open tactic +set_option pp.all true + +meta def check_expr (p : pexpr) (t : expr) : tactic unit := +do e ← to_expr p, guard (t = e) + +run_command do + e ← to_expr `(boo 2), + check_expr `(boo 2 (2:nat) ff {v1 := config.v1._default, v2 := 2, flag := ff, ps := config.ps._default}) e, + e ← to_expr `(f 1), + check_expr `(f 1 (5:nat)) e