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

feat: make RelaxedImplicit the default behavior

Browse source
This commit is contained in:
Leonardo de Moura 2020-05-12 13:57:39 -07:00
parent 861d476a9a
commit 03403ba3c8
6 changed files with 14 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -3510,8 +3510,7 @@ expr elaborator::visit_suffices_expr(expr const & e, optional<expr> const & expe
}
static expr mk_emptyc(expr const & src) {
return copy_pos(src, mk_app(copy_pos(src, mk_constant(get_has_emptyc_emptyc_name())),
copy_pos(src, mk_expr_placeholder())));
return copy_pos(src, mk_constant(get_has_emptyc_emptyc_name()));
}
expr elaborator::visit_emptyc_or_emptys(expr const & e, optional<expr> const & expected_type) {

4
src/frontends/lean/inductive_cmds.cpp
View file

@ -125,7 +125,7 @@ struct inductive_cmd_fn {
if (auto it = m_implicit_infer_map.find(n))
return *it;
else
return implicit_infer_kind::Implicit;
return implicit_infer_kind::RelaxedImplicit;
}
/** \brief Return true if eliminator/recursor can eliminate into any universe */
@ -384,7 +384,7 @@ struct inductive_cmd_fn {
ir_name = get_namespace(m_env) + ir_name;
parser::local_scope S(m_p);
buffer<expr> params;
implicit_infer_kind kind = implicit_infer_kind::Implicit;
implicit_infer_kind kind = implicit_infer_kind::RelaxedImplicit;
m_p.parse_optional_binders(params, kind);
m_implicit_infer_map.insert(ir_name, kind);
for (expr const & param : params)

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

@ -869,11 +869,11 @@ void parser::parse_binders_core(buffer<expr> & r, parse_binders_config & cfg) {
/* Parse {} prefix */
if (is_implicit(*bi) && curr_is_token(get_rcurly_tk())) {
next();
*cfg.m_infer_kind = implicit_infer_kind::RelaxedImplicit;
*cfg.m_infer_kind = implicit_infer_kind::Implicit;
first = false;
continue;
} else {
*cfg.m_infer_kind = implicit_infer_kind::Implicit;
*cfg.m_infer_kind = implicit_infer_kind::RelaxedImplicit;
}
}
unsigned rbp = 0;

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

@ -156,8 +156,8 @@ struct parser : public abstract_parser {
If m_infer_kind != nullptr, then a sequence of binders can be prefixed with '{}'
Moreover, *m_infer_kind will be updated with
- implicit_infer_kind::RelaxedImplicit if prefix is '{}'
- implicit_infer_kind::Implicit, otherwise. */
- implicit_infer_kind::Implicit if prefix is '{}'
- implicit_infer_kind::RelaxedImplicit, otherwise. */
implicit_infer_kind * m_infer_kind{nullptr};
/* (output) It is set to true if the last binder is surrounded
with some kind of bracket (e.g., '()', '{}', '[]'). */

10
src/frontends/lean/structure_cmd.cpp
View file

@ -227,7 +227,7 @@ struct structure_cmd_fn {
bool m_has_new_default; // if true, (re-)declare default value in this structure
field_decl(expr const & local, optional<expr> const & default_val, field_kind kind,
implicit_infer_kind infer_kind = implicit_infer_kind::Implicit):
implicit_infer_kind infer_kind = implicit_infer_kind::RelaxedImplicit):
m_local(local), m_default_val(default_val), m_kind(kind), m_infer_kind(infer_kind),
m_has_new_default(default_val && kind == field_kind::new_field) {}
@ -783,7 +783,7 @@ struct structure_cmd_fn {
expr type;
expr default_value;
bool default_value_initialized = false;
implicit_infer_kind kind = implicit_infer_kind::Implicit;
implicit_infer_kind kind = implicit_infer_kind::RelaxedImplicit;
{
parser::local_scope scope(m_p);
buffer<expr> params;
@ -1065,7 +1065,7 @@ struct structure_cmd_fn {
if (!m_subobjects || field.m_kind != field_kind::from_parent) {
proj_names.push_back(m_name + local_name_p(field.m_local));
infer_kinds.push_back(
field.m_infer_kind != implicit_infer_kind::Implicit ? field.m_infer_kind : m_mk_infer);
field.m_infer_kind != implicit_infer_kind::RelaxedImplicit ? field.m_infer_kind : m_mk_infer);
}
}
m_env = mk_projections(m_env, m_name, proj_names, infer_kinds, m_meta_info.m_attrs.has_class());
@ -1277,7 +1277,7 @@ struct structure_cmd_fn {
if (m_p.curr_is_token(get_lparen_tk()) || m_p.curr_is_token(get_lcurly_tk()) ||
m_p.curr_is_token(get_lbracket_tk())) {
m_mk_short = LEAN_DEFAULT_STRUCTURE_INTRO;
m_mk_infer = implicit_infer_kind::Implicit;
m_mk_infer = implicit_infer_kind::RelaxedImplicit;
} else {
m_mk_short = m_p.check_atomic_id_next("invalid 'structure', atomic identifier expected");
m_mk_infer = parse_implicit_infer_modifier(m_p);
@ -1289,7 +1289,7 @@ struct structure_cmd_fn {
} else {
m_mk_pos = m_name_pos;
m_mk_short = LEAN_DEFAULT_STRUCTURE_INTRO;
m_mk_infer = implicit_infer_kind::Implicit;
m_mk_infer = implicit_infer_kind::RelaxedImplicit;
m_mk = m_name + m_mk_short;
process_empty_new_fields();
}

4
src/frontends/lean/type_util.cpp
View file

@ -36,9 +36,9 @@ implicit_infer_kind parse_implicit_infer_modifier(parser & p) {
if (p.curr_is_token(get_lcurly_tk())) {
p.next();
p.check_token_next(get_rcurly_tk(), "invalid introduction rule, '}' expected");
return implicit_infer_kind::RelaxedImplicit;
} else {
return implicit_infer_kind::Implicit;
} else {
return implicit_infer_kind::RelaxedImplicit;
}
}
}