max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean): nicer syntax for default parameter values

Browse source 
See #1340
This commit is contained in:
Leonardo de Moura 2017-01-30 15:24:18 -08:00
parent c09f60de6e
commit 4d3ff955d3
6 changed files with 116 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/decl_util.cpp
View file

@ -43,7 +43,7 @@ bool parse_univ_params(parser & p, buffer<name> & lp_names) {
}
expr parse_single_header(parser & p, buffer<name> & lp_names, buffer<expr> & 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<name> & lp_names, buffer<expr> & 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<name> & lp_names, buffer<expr> & par
return p.save_pos(mk_local(c_name, type), c_pos);
}
void parse_mutual_header(parser & p, buffer<name> & lp_names, buffer<expr> & cs, buffer<expr> & params) {
void parse_mutual_header(parser & p, buffer<name> & lp_names, buffer<expr> & cs, buffer<expr> & 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<name> & lp_names, buffer<expr> & 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)

6
src/frontends/lean/decl_util.h
View file

@ -42,7 +42,8 @@ bool parse_univ_params(parser & p, buffer<name> & lp_names);
\remark Caller is responsible for using: parser::local_scope scope2(p, env); */
expr parse_single_header(parser & p, buffer<name> & lp_names, buffer<expr> & 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<name> & lp_names, buffer<expr> & 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<name> & lp_names, buffer<expr> & cs, buffer<expr> & params);
void parse_mutual_header(parser & p, buffer<name> & lp_names, buffer<expr> & cs, buffer<expr> & params,
bool allow_default = false);
/** \brief Parse the header for one of the declarations in a mutually recursive declaration.
It has the form

3
src/frontends/lean/definition_cmds.cpp
View file

@ -173,7 +173,8 @@ static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<ex
bool is_example, bool is_instance) {
parser::local_scope scope1(p);
auto header_pos = p.pos();
expr fn = parse_single_header(p, lp_names, params, is_example, is_instance);
bool allow_default = true;
expr fn = parse_single_header(p, lp_names, params, is_example, is_instance, allow_default);
declaration_name_scope scope2(local_pp_name(fn));
expr val;
if (p.curr_is_token(get_assign_tk())) {

32
src/frontends/lean/parser.cpp
View file

@ -1009,11 +1009,15 @@ bool parser::parse_binder_collection(buffer<pair<pos_info, name>> 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 <tt>ID ... ID ':' expr</tt>, where the expression
represents the type of the identifiers.
*/
void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi, unsigned rbp) {
void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi, unsigned rbp, bool allow_default) {
buffer<pair<pos_info, name>> names;
while (curr_is_identifier() || curr_is_token(get_placeholder_tk())) {
auto p = pos();
@ -1030,6 +1034,15 @@ void parser::parse_binder_block(buffer<expr> & 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<expr> & r) {
}
void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * 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<binder_info> bi = parse_optional_binder_info(simple_only);
if (bi) {
rbp = 0;
@ -1091,7 +1111,7 @@ void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * 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<expr> & r, buffer<notation_entry> * nentr
local_environment parser::parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries,
bool & last_block_delimited, bool allow_empty, unsigned rbp,
bool simple_only) {
bool simple_only, bool allow_default) {
flet<environment> save1(m_env, m_env); // save environment
flet<local_expr_decls> 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);

27
src/frontends/lean/parser.h
View file

@ -222,10 +222,11 @@ class parser : public abstract_parser {
void parse_inst_implicit_decl(buffer<expr> & r);
expr parse_binder_core(binder_info const & bi, unsigned rbp);
bool parse_binder_collection(buffer<pair<pos_info, name>> const & names, binder_info const & bi, buffer<expr> & r);
void parse_binder_block(buffer<expr> & r, binder_info const & bi, unsigned rbp);
void parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited, unsigned rbp, bool simple_only);
void parse_binder_block(buffer<expr> & r, binder_info const & bi, unsigned rbp, bool allow_default);
void parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited, unsigned rbp,
bool simple_only, bool allow_default);
local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> * 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<notation_entry> * entries);
pair<optional<name>, 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<expr> & 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<expr> & 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<expr> & 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<expr> & r) {
local_environment parse_optional_binders(buffer<expr> & 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<expr> & r, buffer<notation_entry> & 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<binder_info> parse_optional_binder_info(bool simple_only = false);
binder_info parse_binder_info(bool simple_only = false);

65
tests/lean/run/default_param2.lean Normal file
View file

@ -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