From fd5bfc7dfe51b68e4e2859e15fe0d13be619e26a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Jun 2018 15:22:08 -0700 Subject: [PATCH] refactor(kernel): simplify binder_info Now, it is an enumeration type like its Lean counterpart. --- src/frontends/lean/builtin_exprs.cpp | 12 +-- src/frontends/lean/decl_cmds.cpp | 8 +- src/frontends/lean/decl_util.cpp | 2 +- src/frontends/lean/elaborator.cpp | 30 +++--- src/frontends/lean/elaborator.h | 4 +- src/frontends/lean/json.cpp | 2 +- src/frontends/lean/parser.cpp | 34 +++---- src/frontends/lean/parser.h | 10 +- src/frontends/lean/pp.cpp | 22 ++--- src/frontends/lean/pp.h | 2 +- src/frontends/lean/structure_cmd.cpp | 10 +- src/frontends/lean/util.cpp | 20 ++-- src/frontends/lean/util.h | 4 +- src/kernel/abstract_type_context.cpp | 2 +- src/kernel/abstract_type_context.h | 4 +- src/kernel/expr.cpp | 36 ++----- src/kernel/expr.h | 98 +++++++------------ src/kernel/inductive/inductive.cpp | 8 +- src/kernel/local_ctx.cpp | 10 +- src/kernel/local_ctx.h | 20 ++-- src/library/app_builder.cpp | 4 +- src/library/constructions/brec_on.cpp | 4 +- src/library/constructions/drec.cpp | 6 +- src/library/constructions/has_sizeof.cpp | 2 +- src/library/constructions/no_confusion.cpp | 16 +-- src/library/constructions/projection.cpp | 6 +- src/library/equations_compiler/compiler.cpp | 6 +- .../equations_compiler/structural_rec.cpp | 2 +- src/library/error_msgs.cpp | 4 +- src/library/fun_info.cpp | 5 +- src/library/inductive_compiler/mutual.cpp | 2 +- src/library/inductive_compiler/nested.cpp | 2 +- src/library/kernel_serializer.cpp | 10 +- src/library/local_context.cpp | 14 +-- src/library/local_context.h | 8 +- src/library/print.cpp | 13 +-- src/library/quote.cpp | 2 +- src/library/tactic/apply_tactic.cpp | 2 +- src/library/tactic/clear_tactic.cpp | 2 +- src/library/tactic/induction_tactic.cpp | 2 +- src/library/tactic/rewrite_tactic.cpp | 2 +- src/library/tactic/simp_lemmas.cpp | 8 +- src/library/type_context.cpp | 8 +- src/library/type_context.h | 4 +- src/library/user_recursors.cpp | 2 +- src/library/vm/vm_expr.cpp | 27 +---- src/library/vm/vm_expr.h | 2 +- 47 files changed, 223 insertions(+), 280 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 64f5b7245c..f01582b3d1 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -333,7 +333,7 @@ static expr parse_do(parser & p, bool has_braces) { } // add case // _ := else_case - expr x = mk_local(p.next_name(), "_x", mk_expr_placeholder(), binder_info()); + expr x = mk_local(p.next_name(), "_x", mk_expr_placeholder(), mk_binder_info()); expr else_eq = Fun(fn, Fun(x, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, x), pos), else_case, ignore_if_unused), @@ -748,7 +748,7 @@ static expr parse_lambda_constructor(parser & p, pos_info const & ini_pos) { expr fn = p.save_pos(mk_local(p.next_name(), *g_lambda_match_name, mk_expr_placeholder(), mk_rec_info()), pos); expr eqn = Fun(fn, Fun(locals, p.save_pos(mk_equation(p.rec_save_pos(mk_app(fn, pattern), pos), body), pos), p), p); equations_header h = mk_match_header(match_scope.get_name(), match_scope.get_actual_name()); - expr x = p.rec_save_pos(mk_local(p.next_name(), "_x", mk_expr_placeholder(), binder_info()), pos); + expr x = p.rec_save_pos(mk_local(p.next_name(), "_x", mk_expr_placeholder(), mk_binder_info()), pos); return p.rec_save_pos(Fun(x, mk_app(mk_equations(h, 1, &eqn), x)), pos); } @@ -825,12 +825,12 @@ static expr parse_infix_paren(parser & p, list const & accs expr args[2]; buffer vars; bool fixed_second_arg = false; - args[0] = mk_local(p.next_name(), "_x", mk_expr_placeholder(), binder_info()); + args[0] = mk_local(p.next_name(), "_x", mk_expr_placeholder(), mk_binder_info()); vars.push_back(args[0]); p.next(); if (p.curr_is_token(get_rparen_tk())) { p.next(); - args[1] = mk_local(p.next_name(), "_y", mk_expr_placeholder(), binder_info()); + args[1] = mk_local(p.next_name(), "_y", mk_expr_placeholder(), mk_binder_info()); vars.push_back(args[1]); } else { fixed_second_arg = true; @@ -893,9 +893,9 @@ static expr parse_lambda_cons(parser & p, unsigned, expr const *, pos_info const throw parser_error("invalid '(::)' notation, declaration for operator '::' is not compatible with the `(::)` syntactic sugar", pos); expr args[2]; buffer vars; - args[0] = mk_local(p.next_name(), "_x", mk_expr_placeholder(), binder_info()); + args[0] = mk_local(p.next_name(), "_x", mk_expr_placeholder(), mk_binder_info()); vars.push_back(args[0]); - args[1] = mk_local(p.next_name(), "_y", mk_expr_placeholder(), binder_info()); + args[1] = mk_local(p.next_name(), "_y", mk_expr_placeholder(), mk_binder_info()); vars.push_back(args[1]); buffer cs; for (notation::accepting const & acc : head(ts).second.is_accepting()) { diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 02b4ab13b4..eab0a0c601 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -94,7 +94,7 @@ static environment declare_var(parser & p, environment env, variable_kind k, optional const & _bi, pos_info const & pos, cmd_meta const & meta) { binder_info bi; - if (_bi) bi = *_bi; + if (_bi) bi = *_bi; else bi = mk_binder_info(); if (k == variable_kind::Parameter || k == variable_kind::Variable) { if (k == variable_kind::Parameter) { check_in_section(p); @@ -171,7 +171,7 @@ static void check_variable_kind(parser & p, variable_kind k) { static void update_local_binder_info(parser & p, variable_kind k, name const & n, optional const & bi, pos_info const & pos) { binder_info new_bi; - if (bi) new_bi = *bi; + if (bi) new_bi = *bi; else new_bi = mk_binder_info(); if (k == variable_kind::Parameter) { if (p.is_local_variable_user_name(n)) throw parser_error(sstream() << "invalid parameter binder type update, '" @@ -221,7 +221,7 @@ static environment variable_cmd_core(parser & p, variable_kind k, cmd_meta const name n; expr type; buffer ls_buffer; - if (bi && bi->is_inst_implicit() && (k == variable_kind::Parameter || k == variable_kind::Variable)) { + if (bi && is_inst_implicit(*bi) && (k == variable_kind::Parameter || k == variable_kind::Variable)) { var_decl_scope var_scope(p, meta.m_modifiers); /* instance implicit */ if (p.curr_is_identifier()) { @@ -351,7 +351,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, cmd_meta cons buffer ids; optional scope1; expr type; - if (bi && bi->is_inst_implicit() && (k == variable_kind::Parameter || k == variable_kind::Variable)) { + if (bi && is_inst_implicit(*bi) && (k == variable_kind::Parameter || k == variable_kind::Variable)) { /* instance implicit */ if (p.curr_is_identifier()) { auto id_pos = p.pos(); diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index e473150969..9e9bc4341c 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/src/frontends/lean/decl_util.cpp @@ -171,7 +171,7 @@ void collect_annonymous_inst_implicit(parser const & p, collected_locals & local while (i > 0) { --i; auto const & entry = entries[i]; - if (is_local(entry.second) && !locals.contains(entry.second) && local_info(entry.second).is_inst_implicit() && + if (is_local(entry.second) && !locals.contains(entry.second) && is_inst_implicit(local_info(entry.second)) && // remark: remove the following condition condition, if we want to auto inclusion also for non anonymous ones. is_anonymous_inst_name(entry.first)) { bool ok = true; diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 817f1641bf..4a69303f37 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1061,7 +1061,7 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< { while (is_pi(type)) { expr const & d = binding_domain(type); - binder_info const & bi = binding_info(type); + binder_info bi = binding_info(type); expr new_arg; optional postponed; if (std::find(main_idxs.begin(), main_idxs.end(), i) != main_idxs.end()) { @@ -1091,7 +1091,7 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< new_arg = mk_metavar(d, arg_ref); postponed = args[j]; j++; - } else if (bi.is_inst_implicit()) { + } else if (is_inst_implicit(bi)) { new_arg = mk_instance(d, ref); } else { new_arg = mk_metavar(d, ref); @@ -1292,15 +1292,15 @@ void elaborator::first_pass(expr const & fn, buffer const & args, /* Outer loop is used to make sure we consume implicit arguments occurring after auto/option params. */ while (true) { while (is_pi(type)) { - binder_info const & bi = binding_info(type); + binder_info bi = binding_info(type); expr const & d = binding_domain(type); - if (bi.is_strict_implicit() && i == args.size()) + if (is_strict_implicit(bi) && i == args.size()) break; expr new_arg; if (!is_explicit(bi)) { // implicit argument new_arg = mk_metavar(d, ref); - if (bi.is_inst_implicit()) + if (is_inst_implicit(bi)) info.new_instances.push_back(new_arg); new_arg = post_process_implicit_arg(new_arg, ref); } else if (i < args.size()) { @@ -1494,15 +1494,15 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer< while (true) { while (true) { if (is_pi(type)) { - binder_info const & bi = binding_info(type); + binder_info bi = binding_info(type); expr const & d = binding_domain(type); expr new_arg; - if (amask == arg_mask::Default && bi.is_strict_implicit() && i == args.size()) + if (amask == arg_mask::Default && is_strict_implicit(bi) && i == args.size()) break; if ((amask == arg_mask::Default && !is_explicit(bi)) || - (amask == arg_mask::InstHoExplicit && !is_explicit(bi) && !bi.is_inst_implicit() && !is_pi(d))) { + (amask == arg_mask::InstHoExplicit && !is_explicit(bi) && !is_inst_implicit(bi) && !is_pi(d))) { // implicit argument - if (bi.is_inst_implicit()) + if (is_inst_implicit(bi)) new_arg = mk_instance(d, ref); else new_arg = mk_metavar(d, ref); @@ -1516,7 +1516,7 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer< expr ref_arg = get_ref_for_child(args[i], ref); if (args_already_visited) { new_arg = mk_thunk_if_needed(args[i], thunk_of); - } else if (bi.is_inst_implicit() && is_placeholder(args[i])) { + } else if (is_inst_implicit(bi) && is_placeholder(args[i])) { lean_assert(amask != arg_mask::Default); /* If '@' or '@@' have been used, and the argument is '_', then we use type class resolution. */ @@ -2636,7 +2636,7 @@ expr elaborator::visit_equation(expr const & e, unsigned num_fns) { type_context_old::tmp_locals new_locals(m_ctx); for (expr & m : unassigned_mvars) { expr type = instantiate_mvars(m_ctx.infer(m)); - expr new_local = new_locals.push_local(mlocal_pp_name(m), type, binder_info()); + expr new_local = new_locals.push_local(mlocal_pp_name(m), type, mk_binder_info()); m_ctx.assign(m, new_local); } // replace metavariables with new locals @@ -2807,7 +2807,7 @@ elaborator::field_resolution elaborator::field_to_decl(expr const & e, expr cons name full_fname = const_name(I) + fname; name local_name = full_fname.replace_prefix(get_namespace(env()), {}); if (auto ldecl = m_ctx.lctx().find_if([&](local_decl const & decl) { - return decl.get_info().is_rec() && decl.get_user_name() == local_name; + return is_rec(decl.get_info()) && decl.get_user_name() == local_name; })) { // projection is recursive call return field_resolution(full_fname, ldecl); @@ -3075,7 +3075,7 @@ class visit_structure_instance_fn { } else if (!is_explicit(binding_info(c_type))) { /* implicit field */ m_field2elab.insert(S_fname, [=](expr const & d) { - return binding_info(c_type).is_inst_implicit() ? m_elab.mk_instance(d, m_ref) : m_elab.mk_metavar(d, m_ref); + return is_inst_implicit(binding_info(c_type)) ? m_elab.mk_instance(d, m_ref) : m_elab.mk_metavar(d, m_ref); }); } else if (m_info.m_catchall) { /* catchall: insert placeholder */ @@ -3312,7 +3312,7 @@ expr elaborator::visit_expr_quote(expr const & e, optional const & expecte s = replace_propagating_pos(s, [&](expr const & t, unsigned) { if (is_antiquote(t)) { expr local = mk_local(mk_fresh_name(), x.append_after(locals.size() + 1), - mk_expr_placeholder(), binder_info()); + mk_expr_placeholder(), mk_binder_info()); locals.push_back(local); substs.push_back(get_antiquote_expr(t)); return some_expr(local); @@ -3407,7 +3407,7 @@ expr elaborator::visit_mdata(expr const & e, optional const & expected_typ /* If the instance fingerprint has been set, then make sure `type` is not a local instance. Then, add a new local declaration to locals. */ expr elaborator::push_local(type_context_old::tmp_locals & locals, - name const & n, expr const & type, binder_info const & binfo, expr const & /* ref */) { + name const & n, expr const & type, binder_info binfo, expr const & /* ref */) { #if 0 // TODO(Leo): the following check is too restrictive if (m_ctx.lctx().get_instance_fingerprint() && m_ctx.is_class(type)) { diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index b564f8683c..73275f8791 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -123,7 +123,7 @@ private: bool is_mvar_assigned(expr const & e) const { return m_ctx.is_assigned(e); } expr push_local(type_context_old::tmp_locals & locals, name const & n, expr const & type, - binder_info const & binfo, expr const & ref); + binder_info binfo, expr const & ref); expr push_let(type_context_old::tmp_locals & locals, name const & n, expr const & type, expr const & value, expr const & ref); @@ -307,7 +307,7 @@ public: m_ctx.set_env(m_env); } - expr push_local(name const & n, expr const & type, binder_info const & bi = binder_info()) { + expr push_local(name const & n, expr const & type, binder_info bi = mk_binder_info()) { return m_ctx.push_local(n, type, bi); } expr mk_pi(buffer const & params, expr const & type) { return m_ctx.mk_pi(params, type); } diff --git a/src/frontends/lean/json.cpp b/src/frontends/lean/json.cpp index db9eaa0fcc..4efc962973 100644 --- a/src/frontends/lean/json.cpp +++ b/src/frontends/lean/json.cpp @@ -63,7 +63,7 @@ json serialize_decl(name const & short_name, name const & long_name, environment while (true) { if (!is_pi(type)) break; - if (!binding_info(type).is_implicit() && !binding_info(type).is_inst_implicit()) + if (!is_implicit(binding_info(type)) && !is_inst_implicit(binding_info(type))) break; std::string q("?"); q += binding_name(type).to_string(); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index b0d191c0cf..0c76f18e6b 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -545,7 +545,7 @@ bool parser::is_local_decl(expr const & l) { return false; } -bool parser::update_local_binder_info(name const & n, binder_info const & bi) { +bool parser::update_local_binder_info(name const & n, binder_info bi) { auto it = get_local(n); if (!it || !is_local(*it)) return false; @@ -800,7 +800,7 @@ void parser::throw_invalid_open_binder(pos_info const & pos) { optional parser::parse_optional_binder_info(bool simple_only) { if (curr_is_token(get_lparen_tk())) { next(); - return some(binder_info()); + return some(mk_binder_info()); } else if (simple_only) { return optional(); } else if (curr_is_token(get_lcurly_tk())) { @@ -834,7 +834,7 @@ binder_info parser::parse_binder_info(bool simple_only) { return *bi; } else { throw_invalid_open_binder(p); - return binder_info(); + return mk_binder_info(); } } @@ -849,11 +849,11 @@ binder_info parser::parse_binder_info(bool simple_only) { void parser::parse_close_binder_info(optional const & bi) { if (!bi) { return; - } else if (bi->is_implicit()) { + } else if (is_implicit(*bi)) { check_token_next(get_rcurly_tk(), "invalid declaration, '}' expected"); - } else if (bi->is_inst_implicit()) { + } else if (is_inst_implicit(*bi)) { check_token_next(get_rbracket_tk(), "invalid declaration, ']' expected"); - } else if (bi->is_strict_implicit()) { + } else if (is_strict_implicit(*bi)) { if (curr_is_token(get_rcurly_tk())) { next(); check_token_next(get_rcurly_tk(), "invalid declaration, '}' expected"); @@ -866,7 +866,7 @@ void parser::parse_close_binder_info(optional const & bi) { } /** \brief Parse ID ':' expr, where the expression represents the type of the identifier. */ -expr parser::parse_binder_core(binder_info const & bi, unsigned rbp) { +expr parser::parse_binder_core(binder_info bi, unsigned rbp) { auto p = pos(); name id; if (curr_is_token(get_placeholder_tk())) { @@ -887,7 +887,7 @@ expr parser::parse_binder_core(binder_info const & bi, unsigned rbp) { expr parser::parse_binder(unsigned rbp) { if (curr_is_identifier()) { - return parse_binder_core(binder_info(), rbp); + return parse_binder_core(mk_binder_info(), rbp); } else { bool simple_only = false; binder_info bi = parse_binder_info(simple_only); @@ -906,7 +906,7 @@ expr parser::parse_binder(unsigned rbp) { This method return true if the next token is an infix operator, and populates r with the locals above. */ -bool parser::parse_binder_collection(buffer> const & names, binder_info const & bi, buffer & r) { +bool parser::parse_binder_collection(buffer> const & names, binder_info bi, buffer & r) { if (!curr_is_keyword()) return false; name tk = get_token_info().value(); @@ -953,7 +953,7 @@ bool parser::parse_binder_collection(buffer> const & names, \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, bool allow_default) { +void parser::parse_binder_block(buffer & r, binder_info bi, unsigned rbp, bool allow_default) { buffer> names; while (curr_is_identifier() || curr_is_token(get_placeholder_tk())) { auto p = pos(); @@ -1038,7 +1038,7 @@ void parser::parse_binders_core(buffer & r, parse_binders_config & cfg) { /* We only allow the default parameter value syntax for declarations with surrounded by () */ bool new_allow_default = false; - parse_binder_block(r, binder_info(), cfg.m_rbp, new_allow_default); + parse_binder_block(r, mk_binder_info(), cfg.m_rbp, new_allow_default); cfg.m_last_block_delimited = false; } else { /* We only allow the default parameter value syntax for declarations with @@ -1048,7 +1048,7 @@ void parser::parse_binders_core(buffer & r, parse_binders_config & cfg) { if (bi) { if (first && cfg.m_infer_kind != nullptr) { /* Parse {} or () prefix */ - if (bi->is_implicit() && curr_is_token(get_rcurly_tk())) { + if (is_implicit(*bi) && curr_is_token(get_rcurly_tk())) { next(); *cfg.m_infer_kind = implicit_infer_kind::RelaxedImplicit; first = false; @@ -1064,7 +1064,7 @@ void parser::parse_binders_core(buffer & r, parse_binders_config & cfg) { } unsigned rbp = 0; cfg.m_last_block_delimited = true; - if (bi->is_inst_implicit()) { + if (is_inst_implicit(*bi)) { parse_inst_implicit_decl(r); } else { if (cfg.m_simple_only || !parse_local_notation_decl(cfg.m_nentries)) @@ -1383,7 +1383,7 @@ expr parser::parse_notation(parse_table t, expr * left) { unsigned idx = 1; for (expr & arg : args) { actual_args.push_back(arg); - arg = mk_local(next_name(), x.append_after(idx), mk_expr_placeholder(), binder_info()); + arg = mk_local(next_name(), x.append_after(idx), mk_expr_placeholder(), mk_binder_info()); idx++; } } @@ -1434,7 +1434,7 @@ expr parser::parse_placeholder() { expr parser::parse_anonymous_var_pattern() { auto p = pos(); next(); - expr t = mk_local(next_name(), "_x", mk_expr_placeholder(), binder_info()); + expr t = mk_local(next_name(), "_x", mk_expr_placeholder(), mk_binder_info()); return save_pos(t, p); } @@ -1584,7 +1584,7 @@ struct to_pattern_fn { } else if (is_inaccessible(e)) { // do nothing } else if (is_placeholder(e)) { - expr r = copy_pos(e, mk_local(m_parser.next_name(), "_x", copy_pos(e, mk_expr_placeholder()), binder_info())); + expr r = copy_pos(e, mk_local(m_parser.next_name(), "_x", copy_pos(e, mk_expr_placeholder()), mk_binder_info())); m_new_locals.push_back(r); m_anonymous_vars.insert(mk_pair(e, r)); } else if (is_as_pattern(e)) { @@ -1787,7 +1787,7 @@ static expr elaborate_quote(parser & p, expr e) { e = replace_propagating_pos(e, [&](expr const & t, unsigned) { if (is_antiquote(t)) { expr local = mk_local(p.next_name(), x.append_after(locals.size() + 1), - mk_expr_placeholder(), binder_info()); + mk_expr_placeholder(), mk_binder_info()); locals.push_back(local); aqs.push_back(t); return some_expr(local); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 83a96189b5..400af8aa3a 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -114,9 +114,9 @@ class parser : public abstract_parser { expr parse_char_expr(); expr parse_inst_implicit_decl(); 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, bool allow_default); + expr parse_binder_core(binder_info bi, unsigned rbp); + bool parse_binder_collection(buffer> const & names, binder_info bi, buffer & r); + void parse_binder_block(buffer & r, binder_info bi, unsigned rbp, bool allow_default); struct parse_binders_config { /* (input) If m_allow_empty is true, then parse_binders will succeed even if not binder is parsed. */ bool m_allow_empty{false}; @@ -395,7 +395,7 @@ public: binder_info parse_binder_info(bool simple_only = false); void parse_close_binder_info(optional const & bi); - void parse_close_binder_info(binder_info const & bi) { return parse_close_binder_info(optional(bi)); } + void parse_close_binder_info(binder_info bi) { return parse_close_binder_info(optional(bi)); } /** \brief Convert an identifier into an expression (constant or local constant) based on the current scope */ expr id_to_expr(name const & id, pos_info const & p, bool resolve_only = false, bool allow_field_notation = true, @@ -487,7 +487,7 @@ public: return false; } /** \brief Update binder information for the section parameter n, return true if success, and false if n is not a section parameter. */ - bool update_local_binder_info(name const & n, binder_info const & bi); + bool update_local_binder_info(name const & n, binder_info bi); void include_variable(name const & n) { m_include_vars.insert(n); } void omit_variable(name const & n) { m_include_vars.erase(n); } bool is_include_variable(name const & n) const { return m_include_vars.contains(n); } diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index ca7742d351..5ceb87f366 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -433,7 +433,7 @@ bool pretty_fn::is_implicit(expr const & f) { expr t = m_ctx.relaxed_whnf(m_ctx.infer(f)); if (is_pi(t)) { binder_info bi = binding_info(t); - return bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit(); + return !is_explicit(bi); } else { return false; } @@ -785,7 +785,7 @@ bool pretty_fn::has_implicit_args(expr const & f) { push_local_fn push_local(m_ctx); while (is_pi(type)) { binder_info bi = binding_info(type); - if (bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit()) + if (!is_explicit(bi)) return true; expr local = push_local(binding_name(type), binding_domain(type), binding_info(type)); type = m_ctx.relaxed_whnf(instantiate(binding_body(type), local)); @@ -898,21 +898,21 @@ auto pretty_fn::pp_app(expr const & e) -> result { format pretty_fn::pp_binder(expr const & local) { format r; auto bi = local_info(local); - if (bi != binder_info()) + if (!is_default(bi)) r += format(open_binder_string(bi, m_unicode)); r += escape(mlocal_pp_name(local)); if (m_binder_types) { r += space(); r += compose(colon(), nest(m_indent, compose(line(), pp_child(mlocal_type(local), 0).fmt()))); } - if (bi != binder_info()) + if (!is_default(bi)) r += format(close_binder_string(bi, m_unicode)); return r; } -format pretty_fn::pp_binder_block(buffer const & names, expr const & type, binder_info const & bi) { +format pretty_fn::pp_binder_block(buffer const & names, expr const & type, binder_info bi) { format r; - if (m_binder_types || bi != binder_info()) + if (m_binder_types || !is_default(bi)) r += format(open_binder_string(bi, m_unicode)); for (name const & n : names) { r += escape(n); @@ -921,7 +921,7 @@ format pretty_fn::pp_binder_block(buffer const & names, expr const & type, r += space(); r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).fmt()))); } - if (m_binder_types || bi != binder_info()) + if (m_binder_types || !is_default(bi)) r += format(close_binder_string(bi, m_unicode)); return group(r); } @@ -936,7 +936,7 @@ format pretty_fn::pp_binders(buffer const & locals) { format r; for (unsigned i = 1; i < num; i++) { expr local = locals[i]; - if (!bi.is_inst_implicit() && mlocal_type(local) == type && local_info(local) == bi) { + if (!is_inst_implicit(bi) && mlocal_type(local) == type && local_info(local) == bi) { names.push_back(mlocal_pp_name(local)); } else { r += group(compose(line(), pp_binder_block(names, type, bi))); @@ -968,7 +968,7 @@ auto pretty_fn::pp_lambda(expr const & e) -> result { That is, we don't want to lose binder info when pretty printing. */ static bool is_default_arrow(expr const & e) { - return is_arrow(e) && binding_info(e) == binder_info(); + return is_arrow(e) && is_default(binding_info(e)); } auto pretty_fn::pp_pi(expr const & e) -> result { @@ -1286,8 +1286,8 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer> & a fn_type = m_ctx.relaxed_whnf(fn_type); if (!is_pi(fn_type)) return false; - expr const & body = binding_body(fn_type); - binder_info const & info = binding_info(fn_type); + expr const & body = binding_body(fn_type); + binder_info info = binding_info(fn_type); if (is_explicit(info)) { if (j >= p_args.size()) return false; diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index 4d151a612b..7898a04f80 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -109,7 +109,7 @@ private: format pp_level(level const & l); format pp_binder(expr const & local); - format pp_binder_block(buffer const & names, expr const & type, binder_info const & bi); + format pp_binder_block(buffer const & names, expr const & type, binder_info bi); format pp_binders(buffer const & locals); bool match(level const & p, level const & l); diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index b685860a87..79c3f482ee 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -500,7 +500,7 @@ struct structure_cmd_fn { fname = *ref; else fname = name(parent_name.get_string()).append_before("to_"); - binder_info bi; + binder_info bi = mk_binder_info(); if (m_meta_info.m_attrs.has_class() && is_class(m_env, parent_name)) // make superclass fields inst implicit bi = mk_inst_implicit_binder_info(); @@ -653,7 +653,7 @@ struct structure_cmd_fn { if (i == nparams + 1) return mk_as_is(e); return mk_lambda(binding_name(e), mk_as_is(binding_domain(e)), pi_to_lam(binding_body(e), i + 1), - i < nparams ? mk_implicit_binder_info() : binder_info()); + i < nparams ? mk_implicit_binder_info() : mk_binder_info()); }; type = pi_to_lam(type, 0); type = mk_app(type, base_obj); @@ -793,7 +793,7 @@ struct structure_cmd_fn { } } - void parse_field_block(binder_info const & bi) { + void parse_field_block(binder_info bi) { buffer> names; auto start_pos = m_p.pos(); while (m_p.curr_is_identifier()) { @@ -1127,7 +1127,7 @@ struct structure_cmd_fn { /* Copy fields it depends on */ for (expr const & local : used_locals.get_collected()) { if (!is_param(local)) - args.push_back(update_local(local, binder_info())); + args.push_back(update_local(local, mk_binder_info())); } name decl_name = name(m_name + field.get_name(), "_default"); name decl_prv_name; @@ -1238,7 +1238,7 @@ struct structure_cmd_fn { throw_ill_formed_parent(parent_name); level parent_rlvl = sort_level(parent_type); expr st_type = mk_app(mk_constant(m_name, st_ls), m_params); - binder_info bi; + binder_info bi = mk_binder_info(); if (m_meta_info.m_attrs.has_class()) bi = mk_inst_implicit_binder_info(); expr st = mk_local(m_p.next_name(), "s", st_type, bi); diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 7a1b05b706..246d3fb021 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -307,19 +307,19 @@ environment open_prec_aliases(environment const & env) { return overwrite_aliases(env, prec, name()); } -char const * open_binder_string(binder_info const & bi, bool unicode) { - if (bi.is_implicit()) return "{"; - else if (bi.is_inst_implicit()) return "["; - else if (bi.is_strict_implicit() && unicode) return "⦃"; - else if (bi.is_strict_implicit() && !unicode) return "{{"; +char const * open_binder_string(binder_info bi, bool unicode) { + if (is_implicit(bi)) return "{"; + else if (is_inst_implicit(bi)) return "["; + else if (is_strict_implicit(bi) && unicode) return "⦃"; + else if (is_strict_implicit(bi) && !unicode) return "{{"; else return "("; } -char const * close_binder_string(binder_info const & bi, bool unicode) { - if (bi.is_implicit()) return "}"; - else if (bi.is_inst_implicit()) return "]"; - else if (bi.is_strict_implicit() && unicode) return "⦄"; - else if (bi.is_strict_implicit() && !unicode) return "}}"; +char const * close_binder_string(binder_info bi, bool unicode) { + if (is_implicit(bi)) return "}"; + else if (is_inst_implicit(bi)) return "]"; + else if (is_strict_implicit(bi) && unicode) return "⦄"; + else if (is_strict_implicit(bi) && !unicode) return "}}"; else return ")"; } diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 1f13dec2e4..b45a46abdf 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -95,8 +95,8 @@ environment open_prec_aliases(environment const & env); environment open_priority_aliases(environment const & env); name get_priority_namespace(); -char const * open_binder_string(binder_info const & bi, bool unicode); -char const * close_binder_string(binder_info const & bi, bool unicode); +char const * open_binder_string(binder_info bi, bool unicode); +char const * close_binder_string(binder_info bi, bool unicode); /** \brief Parse option name */ pair parse_option_name(parser & p, char const * error_msg); diff --git a/src/kernel/abstract_type_context.cpp b/src/kernel/abstract_type_context.cpp index 6695c6dbab..59522a7bf1 100644 --- a/src/kernel/abstract_type_context.cpp +++ b/src/kernel/abstract_type_context.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" namespace lean { -expr abstract_type_context::push_local(name const & pp_name, expr const & type, binder_info const & bi) { +expr abstract_type_context::push_local(name const & pp_name, expr const & type, binder_info bi) { return mk_local(next_name(), pp_name, type, bi); } diff --git a/src/kernel/abstract_type_context.h b/src/kernel/abstract_type_context.h index eff7da93ec..3402de0a8b 100644 --- a/src/kernel/abstract_type_context.h +++ b/src/kernel/abstract_type_context.h @@ -29,7 +29,7 @@ public: virtual expr check(expr const & e) { return infer(e); } virtual optional is_stuck(expr const &) { return none_expr(); } - virtual expr push_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()); + virtual expr push_local(name const & pp_name, expr const & type, binder_info bi = mk_binder_info()); virtual void pop_local(); expr check(expr const & e, bool infer_only) { return infer_only ? infer(e) : check(e); } @@ -46,7 +46,7 @@ class push_local_fn { public: push_local_fn(abstract_type_context & ctx):m_ctx(ctx), m_counter(0) {} ~push_local_fn(); - expr operator()(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) { + expr operator()(name const & pp_name, expr const & type, binder_info bi = mk_binder_info()) { m_counter++; return m_ctx.push_local(pp_name, type, bi); } diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 73f7737e06..d7d701676d 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -162,7 +162,7 @@ void expr_mlocal::dealloc(buffer & todelete) { expr_mlocal::expr_mlocal(expr_mlocal const & src, expr const & new_type): expr_composite(src), m_name(src.m_name), m_pp_name(src.m_pp_name), m_type(new_type) {} -expr_fvar::expr_fvar(name const & n, name const & pp_n, expr const & t, binder_info const & bi): +expr_fvar::expr_fvar(name const & n, name const & pp_n, expr const & t, binder_info bi): expr_mlocal(false, n, pp_n, t), m_bi(bi) {} expr_fvar::expr_fvar(expr_fvar const & src, expr const & new_type): @@ -215,7 +215,7 @@ void expr_app::dealloc(buffer & todelete) { static unsigned dec(unsigned k) { return k == 0 ? 0 : k - 1; } // Expr binders (Lambda, Pi) -expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr const & b, binder_info const & i): +expr_binding::expr_binding(expr_kind k, name const & n, expr const & t, expr const & b, binder_info i): expr_composite(k, ::lean::hash(t.hash(), b.hash()), t.has_expr_metavar() || b.has_expr_metavar(), t.has_univ_metavar() || b.has_univ_metavar(), @@ -372,7 +372,7 @@ expr mk_bvar(unsigned idx) { return expr(new expr_bvar(idx)); } expr mk_fvar(name const & n) { - return expr(new expr_fvar(n, n, expr(), binder_info())); + return expr(new expr_fvar(n, n, expr(), mk_binder_info())); } expr mk_constant(name const & n, levels const & ls) { return expr(new expr_const(n, ls)); @@ -389,13 +389,13 @@ expr mk_mdata(kvmap const & d, expr const & e) { expr mk_proj(nat const & idx, expr const & e) { return expr(new expr_proj(idx, e)); } -expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi) { +expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info bi) { return expr(new expr_fvar(n, pp_n, t, bi)); } expr mk_app(expr const & f, expr const & a) { return expr(new expr_app(f, a)); } -expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i) { +expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info i) { return expr(new expr_binding(k, n, t, e, i)); } expr mk_let(name const & n, expr const & t, expr const & v, expr const & b) { @@ -539,7 +539,7 @@ static name const & get_default_var_name() { bool is_default_var_name(name const & n) { return n == get_default_var_name(); } expr mk_arrow(expr const & t, expr const & e) { - return mk_pi(get_default_var_name(), t, e, binder_info()); + return mk_pi(get_default_var_name(), t, e, mk_binder_info()); } static expr * g_Prop = nullptr; @@ -608,7 +608,7 @@ expr update_binding(expr const & e, expr const & new_domain, expr const & new_bo return e; } -expr update_binding(expr const & e, expr const & new_domain, expr const & new_body, binder_info const & bi) { +expr update_binding(expr const & e, expr const & new_domain, expr const & new_body, binder_info bi) { if (!is_eqp(binding_domain(e), new_domain) || !is_eqp(binding_body(e), new_body) || bi != binding_info(e)) return mk_binding(e.kind(), binding_name(e), new_domain, new_body, bi); else @@ -624,14 +624,14 @@ expr update_mlocal(expr const & e, expr const & new_type) { return mk_local(mlocal_name(e), mlocal_pp_name(e), new_type, local_info(e)); } -expr update_local(expr const & e, expr const & new_type, binder_info const & bi) { +expr update_local(expr const & e, expr const & new_type, binder_info bi) { if (is_eqp(mlocal_type(e), new_type) && local_info(e) == bi) return e; else return mk_local(mlocal_name(e), mlocal_pp_name(e), new_type, bi); } -expr update_local(expr const & e, binder_info const & bi) { +expr update_local(expr const & e, binder_info bi) { return update_local(e, mlocal_type(e), bi); } @@ -781,7 +781,7 @@ expr infer_implicit(expr const & t, unsigned num_params, bool strict) { return t; } else if (is_pi(t)) { expr new_body = infer_implicit(binding_body(t), num_params-1, strict); - if (binding_info(t).is_implicit() || binding_info(t).is_strict_implicit() || binding_info(t).is_inst_implicit()) { + if (!is_explicit(binding_info(t))) { // argument is already marked as implicit return update_binding(t, binding_domain(t), new_body); } else if (has_loose_bvars_in_domain(new_body, 0, strict)) { @@ -798,22 +798,6 @@ expr infer_implicit(expr const & t, bool strict) { return infer_implicit(t, std::numeric_limits::max(), strict); } -unsigned hash_bi(expr const & e) { - unsigned h = e.hash(); - for_each(e, [&](expr const & e, unsigned) { - if (is_binding(e)) { - h = hash(h, hash(binding_name(e).hash(), binding_info(e).hash())); - } else if (is_local(e)) { - h = hash(h, hash(mlocal_name(e).hash(), local_info(e).hash())); - return false; // do not visit type - } else if (is_metavar(e)) { - return false; // do not visit type - } - return true; - }); - return h; -} - std::ostream & operator<<(std::ostream & out, expr_kind const & k) { switch (k) { case expr_kind::MData: out << "MData"; break; diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 8b9789634b..a19aecf74e 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -26,9 +26,22 @@ Author: Leonardo de Moura #include "kernel/expr_eq_fn.h" namespace lean { -class abstract_type_context; +/* Binder annotations for Pi/lambda expressions */ +enum class binder_info { Default, Implicit, StrictImplicit, InstImplicit, Rec }; + +inline binder_info mk_binder_info() { return binder_info::Default; } +inline binder_info mk_implicit_binder_info() { return binder_info::Implicit; } +inline binder_info mk_strict_implicit_binder_info() { return binder_info::StrictImplicit; } +inline binder_info mk_inst_implicit_binder_info() { return binder_info::InstImplicit; } +inline binder_info mk_rec_info() { return binder_info::Rec; } + +inline bool is_default(binder_info bi) { return bi == binder_info::Default; } +inline bool is_implicit(binder_info bi) { return bi == binder_info::Implicit; } +inline bool is_strict_implicit(binder_info bi) { return bi == binder_info::StrictImplicit; } +inline bool is_inst_implicit(binder_info bi) { return bi == binder_info::InstImplicit; } +inline bool is_explicit(binder_info bi) { return !is_implicit(bi) && !is_strict_implicit(bi) && !is_inst_implicit(bi); } +inline bool is_rec(binder_info bi) { return bi == binder_info::Rec; } -class expr; /* ======================================= Expressions expr ::= BVar idx @@ -48,6 +61,7 @@ class expr; | Quote bool expr */ +class expr; enum class expr_kind { BVar, FVar, Sort, Constant, MVar, App, Lambda, Pi, Let, Lit, MData, Proj, Quote }; class expr_cell { protected: @@ -82,7 +96,6 @@ public: typedef expr_cell * expr_ptr; -class binder_info; class literal; /** @@ -131,14 +144,14 @@ public: friend expr mk_constant(name const & n, levels const & ls); friend expr mk_metavar(name const & n, name const & pp_n, expr const & t); friend expr mk_app(expr const & f, expr const & a); - friend expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i); + friend expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info i); friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & b); friend expr mk_lit(literal const & lit); friend expr mk_mdata(kvmap const & m, expr const & e); friend expr mk_proj(nat const & idx, expr const & e); friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; } // TODO(Leo): delete - friend expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi); + friend expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info bi); friend expr mk_quote(bool reflected, expr const & val); }; @@ -206,43 +219,6 @@ public: expr const & get_type() const { return m_type; } }; -/** \brief Auxiliary annotation for binders (Lambda and Pi). */ -class binder_info { - enum kind { Default, Implicit, StrictImplicit, InstImplicit, Rec }; - object * m_val; - binder_info(object * v):m_val(v) {} -public: - binder_info():m_val(box(static_cast(Default))) {} - friend binder_info mk_implicit_binder_info(); - friend binder_info mk_strict_implicit_binder_info(); - friend binder_info mk_inst_implicit_binder_info(); - friend binder_info mk_rec_info(); - bool is_implicit() const { return unbox(m_val) == static_cast(Implicit); } - bool is_strict_implicit() const { return unbox(m_val) == static_cast(StrictImplicit); } - bool is_inst_implicit() const { return unbox(m_val) == static_cast(InstImplicit); } - bool is_rec() const { return unbox(m_val) == static_cast(Rec); } - unsigned hash() const { return unbox(m_val); } - friend bool operator==(binder_info const & i1, binder_info const & i2) { return i1.m_val == i2.m_val; } - friend bool operator!=(binder_info const & i1, binder_info const & i2) { return !(i1 == i2); } - friend binder_info read_binder_info(deserializer & d); - void serialize(serializer & s) const { s.write_object(m_val); } -}; - -inline binder_info mk_implicit_binder_info() { return binder_info(box(static_cast(binder_info::Implicit))); } -inline binder_info mk_strict_implicit_binder_info() { return binder_info(box(static_cast(binder_info::StrictImplicit))); } -inline binder_info mk_inst_implicit_binder_info() { return binder_info(box(static_cast(binder_info::InstImplicit))); } -inline binder_info mk_rec_info() { return binder_info(box(static_cast(binder_info::Rec))); } -inline bool is_explicit(binder_info const & bi) { - return !bi.is_implicit() && !bi.is_strict_implicit() && !bi.is_inst_implicit(); -} -inline serializer & operator<<(serializer & s, binder_info const & bi) { bi.serialize(s); return s; } -inline binder_info read_binder_info(deserializer & d) { return binder_info(d.read_object()); } -inline deserializer & operator>>(deserializer & d, binder_info & bi) { bi = read_binder_info(d); return d; } - -/** \brief Compute a hash code that takes binder_info into account. - \remark This information is not cached like hash(). */ -unsigned hash_bi(expr const & e); - /** \brief expr_mlocal subclass for local constants. */ class expr_fvar : public expr_mlocal { binder_info m_bi; @@ -250,8 +226,8 @@ class expr_fvar : public expr_mlocal { void dealloc(buffer & todelete); expr_fvar(expr_fvar const &, expr const & new_type); // for hash_consing public: - expr_fvar(name const & n, name const & pp_name, expr const & t, binder_info const & bi); - binder_info const & get_info() const { return m_bi; } + expr_fvar(name const & n, name const & pp_name, expr const & t, binder_info bi); + binder_info get_info() const { return m_bi; } }; /** \brief Applications */ @@ -275,11 +251,11 @@ class binder { binder(binder const & src, expr const & new_type): // for hash_consing m_name(src.m_name), m_type(new_type), m_info(src.m_info) {} public: - binder(name const & n, expr const & t, binder_info const & bi): + binder(name const & n, expr const & t, binder_info bi): m_name(n), m_type(t), m_info(bi) {} name const & get_name() const { return m_name; } expr const & get_type() const { return m_type; } - binder_info const & get_info() const { return m_info; } + binder_info get_info() const { return m_info; } binder update_type(expr const & t) const { return binder(m_name, t, m_info); } }; @@ -292,11 +268,11 @@ class expr_binding : public expr_composite { expr_binding(expr_binding const &, expr const & new_domain, expr const & new_body); // for hash_consing public: expr_binding(expr_kind k, name const & n, expr const & t, expr const & e, - binder_info const & i); + binder_info i); name const & get_name() const { return m_binder.get_name(); } expr const & get_domain() const { return m_binder.get_type(); } expr const & get_body() const { return m_body; } - binder_info const & get_info() const { return m_binder.get_info(); } + binder_info get_info() const { return m_binder.get_info(); } binder const & get_binder() const { return m_binder; } }; @@ -444,13 +420,11 @@ inline expr mk_rev_app(buffer const & args) { return mk_rev_app(args.size( inline expr mk_rev_app(expr const & f, buffer const & args) { return mk_rev_app(f, args.size(), args.data()); } -expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, - binder_info const & i = binder_info()); -inline expr mk_lambda(name const & n, expr const & t, expr const & e, - binder_info const & i = binder_info()) { +expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info i = mk_binder_info()); +inline expr mk_lambda(name const & n, expr const & t, expr const & e, binder_info i = mk_binder_info()) { return mk_binding(expr_kind::Lambda, n, t, e, i); } -inline expr mk_pi(name const & n, expr const & t, expr const & e, binder_info const & i = binder_info()) { +inline expr mk_pi(name const & n, expr const & t, expr const & e, binder_info i = mk_binder_info()) { return mk_binding(expr_kind::Pi, n, t, e, i); } expr mk_let(name const & n, expr const & t, expr const & v, expr const & b); @@ -513,7 +487,7 @@ inline expr const & app_arg(expr_ptr e) { return to_app(e)->get inline name const & binding_name(expr_ptr e) { return to_binding(e)->get_name(); } inline expr const & binding_domain(expr_ptr e) { return to_binding(e)->get_domain(); } inline expr const & binding_body(expr_ptr e) { return to_binding(e)->get_body(); } -inline binder_info const & binding_info(expr_ptr e) { return to_binding(e)->get_info(); } +inline binder_info binding_info(expr_ptr e) { return to_binding(e)->get_info(); } inline binder const & binding_binder(expr_ptr e) { return to_binding(e)->get_binder(); } inline name const & let_name(expr_ptr e) { return to_let(e)->get_name(); } inline expr const & let_type(expr_ptr e) { return to_let(e)->get_type(); } @@ -584,10 +558,10 @@ struct expr_hash { unsigned operator()(expr const & e) const { return e.hash(); // Update expr update_app(expr const & e, expr const & new_fn, expr const & new_arg); expr update_binding(expr const & e, expr const & new_domain, expr const & new_body); -expr update_binding(expr const & e, expr const & new_domain, expr const & new_body, binder_info const & bi); +expr update_binding(expr const & e, expr const & new_domain, expr const & new_body, binder_info bi); expr update_mlocal(expr const & e, expr const & new_type); -expr update_local(expr const & e, expr const & new_type, binder_info const & bi); -expr update_local(expr const & e, binder_info const & bi); +expr update_local(expr const & e, expr const & new_type, binder_info bi); +expr update_local(expr const & e, binder_info bi); expr update_sort(expr const & e, level const & new_level); expr update_constant(expr const & e, levels const & new_levels); expr update_let(expr const & e, expr const & new_type, expr const & new_value, expr const & new_body); @@ -671,16 +645,16 @@ inline expr_quote * to_quote(expr_ptr e) { lean_assert(is_quote(e)); inline name const & mlocal_name(expr_ptr e) { return to_mlocal(e)->get_name(); } inline expr const & mlocal_type(expr_ptr e) { return to_mlocal(e)->get_type(); } inline name const & mlocal_pp_name(expr_ptr e) { return to_mlocal(e)->get_pp_name(); } -inline binder_info const & local_info(expr_ptr e) { return to_local(e)->get_info(); } +inline binder_info local_info(expr_ptr e) { return to_local(e)->get_info(); } inline expr mk_var(unsigned idx) { return mk_bvar(idx); } inline expr Var(unsigned idx) { return mk_bvar(idx); } expr mk_quote(bool reflected, expr const & val); -expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi); -inline expr mk_local(name const & n, expr const & t) { return mk_local(n, n, t, binder_info()); } -inline expr mk_local(name const & n, expr const & t, binder_info const & bi) { +expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info bi); +inline expr mk_local(name const & n, expr const & t) { return mk_local(n, n, t, mk_binder_info()); } +inline expr mk_local(name const & n, expr const & t, binder_info bi) { return mk_local(n, n, t, bi); } -inline expr Local(name const & n, expr const & t, binder_info const & bi = binder_info()) { +inline expr Local(name const & n, expr const & t, binder_info bi = mk_binder_info()) { return mk_local(n, t, bi); } inline bool has_local(expr const & e) { return has_fvar(e); } diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index c3c7b0d136..87132a5e8d 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -536,13 +536,13 @@ struct add_inductive_fn { void mk_elim_info() { // First, populate the fields m_C and m_major_premise m_elim_info.m_major_premise = mk_local(m_name_generator.next(), "n", - mk_app(mk_app(m_it_const, m_param_consts), m_elim_info.m_indices), binder_info()); + mk_app(mk_app(m_it_const, m_param_consts), m_elim_info.m_indices), mk_binder_info()); expr C_ty = mk_sort(m_elim_level); if (m_dep_elim) C_ty = Pi(m_elim_info.m_major_premise, C_ty); C_ty = Pi(m_elim_info.m_indices, C_ty); name C_name("C"); - m_elim_info.m_C = mk_local(m_name_generator.next(), C_name, C_ty, binder_info()); + m_elim_info.m_C = mk_local(m_name_generator.next(), C_name, C_ty, mk_binder_info()); // Populate the field m_minor_premises unsigned minor_idx = 1; @@ -607,11 +607,11 @@ struct add_inductive_fn { ih = ih.append_after(i+1); } } - expr v_i = mk_local(m_name_generator.next(), ih, v_i_ty, binder_info()); + expr v_i = mk_local(m_name_generator.next(), ih, v_i_ty, mk_binder_info()); v.push_back(v_i); } expr minor_ty = Pi(b_u, Pi(v, C_app)); - expr minor = mk_local(m_name_generator.next(), name("e").append_after(minor_idx), minor_ty, binder_info()); + expr minor = mk_local(m_name_generator.next(), name("e").append_after(minor_idx), minor_ty, mk_binder_info()); m_elim_info.m_minor_premises.push_back(minor); minor_idx++; } diff --git a/src/kernel/local_ctx.cpp b/src/kernel/local_ctx.cpp index c0dcc4752d..215b2dd9c1 100644 --- a/src/kernel/local_ctx.cpp +++ b/src/kernel/local_ctx.cpp @@ -13,7 +13,7 @@ namespace lean { static expr * g_dummy_type; static local_decl * g_dummy_decl; -static expr mk_local_ref(name const & n, name const & un, binder_info const & bi) { +static expr mk_local_ref(name const & n, name const & un, binder_info bi) { return mk_local(n, un, *g_dummy_type, bi); // TODO(Leo): fix after we remove legacy code } @@ -25,12 +25,12 @@ void local_decl::cell::dealloc() { delete this; } -local_decl::cell::cell(unsigned idx, name const & n, name const & un, expr const & t, optional const & v, binder_info const & bi): +local_decl::cell::cell(unsigned idx, name const & n, name const & un, expr const & t, optional const & v, binder_info bi): m_name(n), m_user_name(un), m_type(t), m_value(v), m_bi(bi), m_idx(idx), m_rc(1) {} local_decl::local_decl():local_decl(*g_dummy_decl) {} -local_decl::local_decl(unsigned idx, name const & n, name const & un, expr const & t, optional const & v, binder_info const & bi) { +local_decl::local_decl(unsigned idx, name const & n, name const & un, expr const & t, optional const & v, binder_info bi) { m_ptr = new cell(idx, n, un, t, v, bi); } @@ -41,7 +41,7 @@ expr local_decl::mk_ref() const { return mk_local_ref(m_ptr->m_name, m_ptr->m_user_name, m_ptr->m_bi); } -local_decl local_ctx::mk_local_decl(name const & n, name const & un, expr const & type, optional const & value, binder_info const & bi) { +local_decl local_ctx::mk_local_decl(name const & n, name const & un, expr const & type, optional const & value, binder_info bi) { lean_assert(!m_name2local_decl.contains(n)); unsigned idx = m_next_idx; m_next_idx++; @@ -123,7 +123,7 @@ void initialize_local_ctx() { g_dummy_type = new expr(mk_constant(name::mk_internal_unique_name())); g_dummy_decl = new local_decl(std::numeric_limits::max(), name("__local_decl_for_default_constructor"), name("__local_decl_for_default_constructor"), - mk_Prop(), optional(), binder_info()); + mk_Prop(), optional(), mk_binder_info()); } void finalize_local_ctx() { diff --git a/src/kernel/local_ctx.h b/src/kernel/local_ctx.h index 1fba7f5782..0eeb7fa552 100644 --- a/src/kernel/local_ctx.h +++ b/src/kernel/local_ctx.h @@ -26,14 +26,14 @@ public: MK_LEAN_RC(); // Declare m_rc counter void dealloc(); cell(unsigned idx, name const & n, name const & un, expr const & t, optional const & v, - binder_info const & bi); + binder_info bi); }; private: cell * m_ptr; friend class local_ctx; friend class local_context; friend void initialize_local_ctx(); - local_decl(unsigned idx, name const & n, name const & un, expr const & t, optional const & v, binder_info const & bi); + local_decl(unsigned idx, name const & n, name const & un, expr const & t, optional const & v, binder_info bi); local_decl(local_decl const & d, expr const & t, optional const & v); public: local_decl(); @@ -49,7 +49,7 @@ public: name const & get_user_name() const { return m_ptr->m_user_name; } expr const & get_type() const { return m_ptr->m_type; } optional const & get_value() const { return m_ptr->m_value; } - binder_info const & get_info() const { return m_ptr->m_bi; } + binder_info get_info() const { return m_ptr->m_bi; } expr mk_ref() const; unsigned get_idx() const { return m_ptr->m_idx; } }; @@ -65,34 +65,34 @@ protected: template expr mk_binding(unsigned num, expr const * fvars, expr const & b) const; local_decl mk_local_decl(name const & n, name const & un, expr const & type, - optional const & value, binder_info const & bi); + optional const & value, binder_info bi); public: local_ctx():m_next_idx(0) {} bool empty() const { return m_idx2local_decl.empty(); } - expr mk_local_decl(name const & n, expr const & type, binder_info const & bi = binder_info()) { + expr mk_local_decl(name const & n, expr const & type, binder_info bi = mk_binder_info()) { return mk_local_decl(n, n, type, none_expr(), bi).mk_ref(); } expr mk_local_decl(name const & n, expr const & type, expr const & value) { - return mk_local_decl(n, n, type, some_expr(value), binder_info()).mk_ref(); + return mk_local_decl(n, n, type, some_expr(value), mk_binder_info()).mk_ref(); } - expr mk_local_decl(name const & n, name const & un, expr const & type, binder_info const & bi = binder_info()) { + expr mk_local_decl(name const & n, name const & un, expr const & type, binder_info bi = mk_binder_info()) { return mk_local_decl(n, un, type, none_expr(), bi).mk_ref(); } expr mk_local_decl(name const & n, name const & un, expr const & type, expr const & value) { - return mk_local_decl(n, un, type, some_expr(value), binder_info()).mk_ref(); + return mk_local_decl(n, un, type, some_expr(value), mk_binder_info()).mk_ref(); } - expr mk_local_decl(name_generator & g, name const & un, expr const & type, binder_info const & bi = binder_info()) { + expr mk_local_decl(name_generator & g, name const & un, expr const & type, binder_info bi = mk_binder_info()) { return mk_local_decl(g.next(), un, type, bi); } expr mk_local_decl(name_generator & g, name const & un, expr const & type, expr const & value) { - return mk_local_decl(g.next(), un, type, some_expr(value), binder_info()).mk_ref(); + return mk_local_decl(g.next(), un, type, some_expr(value), mk_binder_info()).mk_ref(); } /** \brief Return the local declarations for the given reference. diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 1d1ae50e1d..3d2099d2d6 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -163,7 +163,7 @@ class app_builder { expr type = m_ctx.relaxed_whnf(instantiate_type_univ_params(d, lvls)); while (is_pi(type)) { expr mvar = m_ctx.mk_tmp_mvar(binding_domain(type)); - if (binding_info(type).is_inst_implicit()) + if (is_inst_implicit(binding_info(type))) inst_args.push_back(some_expr(mvar)); else inst_args.push_back(none_expr()); @@ -215,7 +215,7 @@ class app_builder { throw app_builder_exception(); } expr mvar = m_ctx.mk_tmp_mvar(binding_domain(type)); - if (binding_info(type).is_inst_implicit()) + if (is_inst_implicit(binding_info(type))) inst_args.push_back(some_expr(mvar)); else inst_args.push_back(none_expr()); diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index 9bd4f7554b..790e654904 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -256,9 +256,9 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) to_telescope(mlocal_type(C), F_args); expr F_result = mk_app(C, F_args); expr F_below = mk_app(belows[j], F_args); - F_args.push_back(mk_local(ngen.next(), "f", F_below, binder_info())); + F_args.push_back(mk_local(ngen.next(), "f", F_below, mk_binder_info())); expr F_type = Pi(F_args, F_result); - expr F = mk_local(ngen.next(), F_name, F_type, binder_info()); + expr F = mk_local(ngen.next(), F_name, F_type, mk_binder_info()); Fs.push_back(F); args.push_back(F); } diff --git a/src/library/constructions/drec.cpp b/src/library/constructions/drec.cpp index 9f7ed317c5..e9430f9613 100644 --- a/src/library/constructions/drec.cpp +++ b/src/library/constructions/drec.cpp @@ -92,7 +92,7 @@ struct mk_drec_fn { motive_params.push_back(local); } expr new_param_type = mk_app(mk_app(mk_constant(I, I_lvls), num_params, rec_params.data()), motive_params); - expr new_param = mk_local(ngen.next(), "h", new_param_type, binder_info()); + expr new_param = mk_local(ngen.next(), "h", new_param_type, mk_binder_info()); expr new_motive_type = Pi(motive_params, Pi(new_param, rec_motive_type)); expr new_motive = update_mlocal(rec_motive, new_motive_type); expr motive_arg = Fun(motive_params, Pi(new_param, mk_app(mk_app(new_motive, motive_params), new_param))); @@ -149,7 +149,7 @@ struct mk_drec_fn { while (is_pi(h_type)) h_type = binding_body(h_type); h_type = instantiate_rev(h_type, ih_params); - expr h = mk_local(ngen.next(), "_h", h_type, binder_info()); + expr h = mk_local(ngen.next(), "_h", h_type, mk_binder_info()); expr app_ih_type = Pi(ih_params, Pi(h, mk_app(new_C_pre, h))); expr app_ih = update_mlocal(local, app_ih_type); app_params.push_back(app_ih); @@ -173,7 +173,7 @@ struct mk_drec_fn { expr new_minor = update_mlocal(minor, new_minor_type); drec_params.push_back(new_minor); expr _h_type = tc.infer(constructor_app); - expr _h = mk_local(ngen.next(), "_", _h_type, binder_info()); + expr _h = mk_local(ngen.next(), "_", _h_type, mk_binder_info()); rec_args.push_back(Fun(app_params, Fun(_h, mk_app(new_minor, app_args)))); i++; } diff --git a/src/library/constructions/has_sizeof.cpp b/src/library/constructions/has_sizeof.cpp index 75843df155..45982cd2e3 100644 --- a/src/library/constructions/has_sizeof.cpp +++ b/src/library/constructions/has_sizeof.cpp @@ -63,7 +63,7 @@ class mk_has_sizeof_fn { } expr mk_local_pp(name const & n, expr const & ty) { - return mk_local(m_ngen.next(), n, ty, binder_info()); + return mk_local(m_ngen.next(), n, ty, mk_binder_info()); } optional mk_has_sizeof(type_context_old & ctx, expr const & type) { diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index a40098922a..fcfe9ac08c 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -50,11 +50,11 @@ optional mk_no_confusion_type(environment const & env, name const & // Create inductive datatype expr I = mk_app(mk_constant(n, ilvls), args); // Add (P : Type) - expr P = mk_local(ngen.next(), "P", mk_sort(plvl), binder_info()); + expr P = mk_local(ngen.next(), "P", mk_sort(plvl), mk_binder_info()); args.push_back(P); // add v1 and v2 elements of the inductive type - expr v1 = mk_local(ngen.next(), "v1", I, binder_info()); - expr v2 = mk_local(ngen.next(), "v2", I, binder_info()); + expr v1 = mk_local(ngen.next(), "v1", I, mk_binder_info()); + expr v2 = mk_local(ngen.next(), "v2", I, mk_binder_info()); args.push_back(v1); args.push_back(v2); expr R = mk_sort(rlvl); @@ -108,7 +108,7 @@ optional mk_no_confusion_type(environment const & env, name const & } else { h_type = mk_app(mk_constant(get_heq_name(), levels(l)), lhs_type, lhs, rhs_type, rhs); } - rtype_hyp.push_back(mk_local(ngen.next(), mlocal_pp_name(lhs).append_after("_eq"), h_type, binder_info())); + rtype_hyp.push_back(mk_local(ngen.next(), mlocal_pp_name(lhs).append_after("_eq"), h_type, mk_binder_info())); } } inner_cases_on_args.push_back(Fun(minor2_args, mk_arrow(Pi(rtype_hyp, P), Pres))); @@ -158,7 +158,7 @@ environment mk_no_confusion(environment const & env, name const & n) { expr v_type = mlocal_type(v1); level v_lvl = sort_level(tc.ensure_type(v_type)); expr eq_v = mk_app(mk_constant(get_eq_name(), levels(v_lvl)), v_type); - expr H12 = mk_local(ngen.next(), "h12", mk_app(eq_v, v1, v2), binder_info()); + expr H12 = mk_local(ngen.next(), "h12", mk_app(eq_v, v1, v2), mk_binder_info()); args.push_back(H12); name no_confusion_name{n, "no_confusion"}; expr no_confusion_ty = Pi(args, range); @@ -170,7 +170,7 @@ environment mk_no_confusion(environment const & env, name const & n) { // ) // H11 is for creating the generalization - expr H11 = mk_local(ngen.next(), "h11", mk_app(eq_v, v1, v1), binder_info()); + expr H11 = mk_local(ngen.next(), "h11", mk_app(eq_v, v1, v1), mk_binder_info()); // Create the type former (fun Indices v1, no_confusion_type Params Indices P v1 v1) buffer type_former_args; for (unsigned i = nparams; i < nparams + nindices; i++) @@ -221,8 +221,8 @@ environment mk_no_confusion(environment const & env, name const & n) { expr eq_rec = mk_app(mk_constant(get_eq_ndrec_name(), {eq_rec_l1, v_lvl}), v_type, v1); // create eq_rec type_former // (fun (a : InductiveType), v1 = a -> no_confusion_type Params Indices v1 a) - expr a = mk_local(ngen.next(), "a", v_type, binder_info()); - expr H1a = mk_local(ngen.next(), "h1a", mk_app(eq_v, v1, a), binder_info()); + expr a = mk_local(ngen.next(), "a", v_type, mk_binder_info()); + expr H1a = mk_local(ngen.next(), "h1a", mk_app(eq_v, v1, a), mk_binder_info()); // reusing no_confusion_type_args... we just replace the last argument with a no_confusion_type_args.pop_back(); no_confusion_type_args.push_back(a); diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index ca00e76240..080ed30298 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -78,9 +78,9 @@ environment mk_projections(environment const & env, name const & n, buffer throw_ill_formed(n); auto bi = binding_info(intro_type); auto type = binding_domain(intro_type); - if (!bi.is_inst_implicit()) + if (!is_inst_implicit(bi)) // We reset implicit binders in favor of having them inferred by `infer_implicit_params` later - bi = binder_info(); + bi = mk_binder_info(); if (is_class_out_param(type)) { // hide `out_param` type = app_arg(type); @@ -92,7 +92,7 @@ environment mk_projections(environment const & env, name const & n, buffer params.push_back(param); } expr C_A = mk_app(mk_constant(n, lvls), params); - binder_info c_bi = inst_implicit ? mk_inst_implicit_binder_info() : binder_info(); + binder_info c_bi = inst_implicit ? mk_inst_implicit_binder_info() : mk_binder_info(); expr c = mk_local(ngen.next(), name("c"), C_A, c_bi); buffer intro_type_args; // arguments that are not parameters expr it = intro_type; diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp index fdef21ff05..eea959ae50 100644 --- a/src/library/equations_compiler/compiler.cpp +++ b/src/library/equations_compiler/compiler.cpp @@ -25,7 +25,7 @@ namespace lean { static bool has_nested_rec(expr const & eqns) { return static_cast(find(eqns, [&](expr const & e, unsigned) { - return is_local(e) && local_info(e).is_rec(); + return is_local(e) && is_rec(local_info(e)); })); } @@ -213,7 +213,7 @@ struct pull_nested_rec_fn : public replace_visitor { lctx().for_each([&](local_decl const & d) { if (!base_lctx().find_local_decl(d.get_name()) && !found.contains(d.get_name()) && - !d.get_info().is_rec() && + !is_rec(d.get_info()) && ctx.is_prop(d.get_type())) { found.insert(d.get_name()); R.push_back(d.mk_ref()); @@ -253,7 +253,7 @@ struct pull_nested_rec_fn : public replace_visitor { virtual expr visit_app(expr const & _e) override { expr const & fn = get_app_fn(_e); - if (is_local(fn) && local_info(fn).is_rec() && base_lctx().find_local_decl(fn)) { + if (is_local(fn) && is_rec(local_info(fn)) && base_lctx().find_local_decl(fn)) { /* `_e` may contain references to let-variables. Here is an example from issue #1917 diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp index e2ce6b26be..bd5e4ece8c 100644 --- a/src/library/equations_compiler/structural_rec.cpp +++ b/src/library/equations_compiler/structural_rec.cpp @@ -556,7 +556,7 @@ struct structural_rec_fn { void update_eqs(type_context_old & ctx, unpack_eqns & ues, expr const & fn, expr const & new_fn) { /* C is a temporary "abstract" motive, we use it to access the "brec_on dictionary". The "brec_on dictionary is an element of type below, and it is the last argument of the new function. */ - expr C = mk_local(ctx.next_name(), "_C", m_motive_type, binder_info()); + expr C = mk_local(ctx.next_name(), "_C", m_motive_type, mk_binder_info()); buffer & eqns = ues.get_eqns_of(0); buffer new_eqns; bool complete = must_complete_rec_arg(ctx, ues); diff --git a/src/library/error_msgs.cpp b/src/library/error_msgs.cpp index 7becd4de9f..d448ffb5b6 100644 --- a/src/library/error_msgs.cpp +++ b/src/library/error_msgs.cpp @@ -53,9 +53,9 @@ expr erase_binder_info(expr const & e) { return replace(e, [](expr const & e) { if (is_local(e) || is_metavar(e)) { return some_expr(e); - } else if (is_binding(e) && binding_info(e) != binder_info()) { + } else if (is_binding(e) && binding_info(e) != mk_binder_info()) { return some_expr(update_binding(e, erase_binder_info(binding_domain(e)), - erase_binder_info(binding_body(e)), binder_info())); + erase_binder_info(binding_body(e)), mk_binder_info())); } else { return none_expr(); } diff --git a/src/library/fun_info.cpp b/src/library/fun_info.cpp index 84f93ec7a1..4b9a629f62 100644 --- a/src/library/fun_info.cpp +++ b/src/library/fun_info.cpp @@ -72,8 +72,9 @@ static list get_core(type_context_old & ctx, expr new_type = ctx.relaxed_try_to_pi(instantiate(binding_body(type), local)); bool is_prop = ctx.is_prop(local_type); bool is_dep = false; /* it is set by collect_deps */ - pinfos.emplace_back(binding_info(type).is_implicit(), - binding_info(type).is_inst_implicit(), + binder_info bi = binding_info(type); + pinfos.emplace_back(is_implicit(bi), + is_inst_implicit(bi), is_prop, is_dep, collect_deps(local_type, locals.as_buffer(), pinfos)); type = new_type; i++; diff --git a/src/library/inductive_compiler/mutual.cpp b/src/library/inductive_compiler/mutual.cpp index 43dba88cca..02bddca394 100644 --- a/src/library/inductive_compiler/mutual.cpp +++ b/src/library/inductive_compiler/mutual.cpp @@ -60,7 +60,7 @@ class add_mutual_inductive_decl_fn { expr punit_star() const { return mk_constant(get_punit_star_name(), {m_elim_level}); } expr mk_local_for(expr const & b) { return mk_local(m_ngen.next(), binding_name(b), binding_domain(b), binding_info(b)); } - expr mk_local_pp(name const & n, expr const & ty) { return mk_local(m_ngen.next(), n, ty, binder_info()); } + expr mk_local_pp(name const & n, expr const & ty) { return mk_local(m_ngen.next(), n, ty, mk_binder_info()); } expr to_sigma_type(expr const & _ty) { expr ty = m_tctx.whnf(_ty); diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index debd5a5de5..dd6ce04b93 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -117,7 +117,7 @@ class add_nested_inductive_decl_fn { expr mk_local_for(expr const & b) { return mk_local(m_ngen.next(), binding_name(b), binding_domain(b), binding_info(b)); } expr mk_local_for(expr const & b, name const & n) { return mk_local(m_ngen.next(), n, binding_domain(b), binding_info(b)); } - expr mk_local_pp(name const & n, expr const & ty) { return mk_local(m_ngen.next(), n, ty, binder_info()); } + expr mk_local_pp(name const & n, expr const & ty) { return mk_local(m_ngen.next(), n, ty, mk_binder_info()); } // For sizeof local_context m_synth_lctx; diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index eb42021678..8924f4e04a 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -61,7 +61,8 @@ class expr_serializer : public object_serializer(binding_info(a))); + write_core(binding_domain(a)); write_core(binding_body(a)); break; case expr_kind::Let: s << let_name(a); @@ -74,7 +75,8 @@ class expr_serializer : public object_serializer(local_info(a))); write_core(mlocal_type(a)); break; case expr_kind::Quote: @@ -97,7 +99,7 @@ public: expr read_binding(expr_kind k) { deserializer & d = get_owner(); name n = read_name(d); - binder_info i = read_binder_info(d); + binder_info i = static_cast(d.read_char()); expr t = read(); return mk_binding(k, n, t, read(), i); } @@ -145,7 +147,7 @@ public: case expr_kind::FVar: { name n = read_name(d); name pp_n = read_name(d); - binder_info bi = read_binder_info(d); + binder_info bi = static_cast(d.read_char()); return mk_local(n, pp_n, read(), bi); } diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index 6bd12dcb75..1ab1a2c907 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -158,36 +158,36 @@ void local_context::erase_user_name(local_decl const & d) { } } -expr local_context::mk_local_decl(name const & n, name const & un, expr const & type, optional const & value, binder_info const & bi) { +expr local_context::mk_local_decl(name const & n, name const & un, expr const & type, optional const & value, binder_info bi) { local_decl d = local_ctx::mk_local_decl(n, un, type, value, bi); insert_user_name(d); return d.mk_ref(); } -expr local_context::mk_local_decl(expr const & type, binder_info const & bi) { +expr local_context::mk_local_decl(expr const & type, binder_info bi) { name n = mk_local_decl_name(); return mk_local_decl(n, n, type, none_expr(), bi); } expr local_context::mk_local_decl(expr const & type, expr const & value) { name n = mk_local_decl_name(); - return mk_local_decl(n, n, type, some_expr(value), binder_info()); + return mk_local_decl(n, n, type, some_expr(value), mk_binder_info()); } -expr local_context::mk_local_decl(name const & un, expr const & type, binder_info const & bi) { +expr local_context::mk_local_decl(name const & un, expr const & type, binder_info bi) { return mk_local_decl(mk_local_decl_name(), un, type, none_expr(), bi); } expr local_context::mk_local_decl(name const & un, expr const & type, expr const & value) { - return mk_local_decl(mk_local_decl_name(), un, type, some_expr(value), binder_info()); + return mk_local_decl(mk_local_decl_name(), un, type, some_expr(value), mk_binder_info()); } -expr local_context::mk_local_decl(name const & n, name const & un, expr const & type, binder_info const & bi) { +expr local_context::mk_local_decl(name const & n, name const & un, expr const & type, binder_info bi) { return mk_local_decl(n, un, type, none_expr(), bi); } expr local_context::mk_local_decl(name const & n, name const & un, expr const & type, expr const & value) { - return mk_local_decl(n, un, type, some_expr(value), binder_info()); + return mk_local_decl(n, un, type, some_expr(value), mk_binder_info()); } optional local_context::find_local_decl_from_user_name(name const & n) const { diff --git a/src/library/local_context.h b/src/library/local_context.h index 4269bca6ba..8fb13f8049 100644 --- a/src/library/local_context.h +++ b/src/library/local_context.h @@ -53,7 +53,7 @@ class local_context : public local_ctx { local_context remove(buffer const & locals) const; expr mk_local_decl(name const & n, name const & un, expr const & type, - optional const & value, binder_info const & bi); + optional const & value, binder_info bi); static local_decl update_local_decl(local_decl const & d, expr const & t, optional const & v) { return local_decl(d, t, v); @@ -67,16 +67,16 @@ public: bool empty() const { return m_idx2local_decl.empty(); } - expr mk_local_decl(expr const & type, binder_info const & bi = binder_info()); + expr mk_local_decl(expr const & type, binder_info bi = mk_binder_info()); expr mk_local_decl(expr const & type, expr const & value); - expr mk_local_decl(name const & un, expr const & type, binder_info const & bi = binder_info()); + expr mk_local_decl(name const & un, expr const & type, binder_info bi = mk_binder_info()); expr mk_local_decl(name const & un, expr const & type, expr const & value); /* Low-level version of the methods above. \pre `n` was created using mk_local_decl_name \pre there is no local_decl named `n` in this local_context. */ - expr mk_local_decl(name const & n, name const & un, expr const & type, binder_info const & bi = binder_info()); + expr mk_local_decl(name const & n, name const & un, expr const & type, binder_info bi = mk_binder_info()); expr mk_local_decl(name const & n, name const & un, expr const & type, expr const & value); /** \brief Return the most recently added local_decl \c d s.t. d.get_user_name() == n diff --git a/src/library/print.cpp b/src/library/print.cpp index 492bcf6e9b..112ada62af 100644 --- a/src/library/print.cpp +++ b/src/library/print.cpp @@ -157,21 +157,22 @@ struct print_expr_fn { out() << " "; auto p = binding_body_fresh(e); expr const & n = p.second; - if (binding_info(e).is_implicit()) + binder_info bi = binding_info(e); + if (is_implicit(bi)) out() << "{"; - else if (binding_info(e).is_inst_implicit()) + else if (is_inst_implicit(bi)) out() << "["; - else if (binding_info(e).is_strict_implicit()) + else if (is_strict_implicit(bi)) out() << "{{"; else out() << "("; out() << n << " : "; print(binding_domain(e)); - if (binding_info(e).is_implicit()) + if (is_implicit(bi)) out() << "}"; - else if (binding_info(e).is_inst_implicit()) + else if (is_inst_implicit(bi)) out() << "]"; - else if (binding_info(e).is_strict_implicit()) + else if (is_strict_implicit(bi)) out() << "}}"; else out() << ")"; diff --git a/src/library/quote.cpp b/src/library/quote.cpp index 84e0b2d7cf..ca3dbdf9b9 100644 --- a/src/library/quote.cpp +++ b/src/library/quote.cpp @@ -79,7 +79,7 @@ expr mk_pexpr_quote_and_substs(expr const & e, bool is_strict) { expr s = replace(e, [&](expr const & t, unsigned) { if (is_antiquote(t)) { expr local = mk_local(ngen.next(), x.append_after(locals.size() + 1), - mk_expr_placeholder(), binder_info()); + mk_expr_placeholder(), mk_binder_info()); locals.push_back(local); aqs.push_back(get_antiquote_expr(t)); return some_expr(local); diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 7565e7aa72..85bc43fee0 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -191,7 +191,7 @@ static optional apply(type_context_old & ctx, expr e, apply_cfg co for (unsigned i = 0; i < num_e_t; i++) { e_type = ctx.relaxed_whnf(e_type); expr meta = ctx.mk_metavar_decl(lctx, binding_domain(e_type)); - is_instance.push_back(binding_info(e_type).is_inst_implicit()); + is_instance.push_back(is_inst_implicit(binding_info(e_type))); metas.push_back(meta); meta_names.push_back(binding_name(e_type)); e = mk_app(e, meta); diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp index 801565a9ea..61cfb83945 100644 --- a/src/library/tactic/clear_tactic.cpp +++ b/src/library/tactic/clear_tactic.cpp @@ -33,7 +33,7 @@ expr clear_rec_core(metavar_context & mctx, expr const & mvar) { optional g = mctx.find_metavar_decl(mvar); lean_assert(g); local_context lctx = g->get_context(); - if (optional d = lctx.find_if([](local_decl const & decl) { return decl.get_info().is_rec(); })) { + if (optional d = lctx.find_if([](local_decl const & decl) { return is_rec(decl.get_info()); })) { return clear(mctx, mvar, d->mk_ref()); } else { return mvar; diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index de4fe21610..504e09dc97 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -292,7 +292,7 @@ list induction(environment const & env, options const & opts, transparency name b_name = binding_name(rec_type); expr new_type = annotated_head_beta_reduce(binding_domain(rec_type)); expr rec_arg; - if (binding_info(rec_type).is_inst_implicit()) { + if (is_inst_implicit(binding_info(rec_type))) { if (optional inst = ctx2.mk_class_instance(new_type)) { rec_arg = *inst; } else { diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index b45a28ad72..fb816e392f 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -44,7 +44,7 @@ static vm_obj rewrite_core(expr h, expr e, rewrite_cfg const & cfg, tactic_state if (!is_pi(h_type)) break; expr meta = ctx.mk_metavar_decl(ctx.lctx(), binding_domain(h_type)); - is_instance.push_back(binding_info(h_type).is_inst_implicit()); + is_instance.push_back(is_inst_implicit(binding_info(h_type))); metas.push_back(meta); h = mk_app(h, meta); h_type = instantiate(binding_body(h_type), meta); diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index 71a0567b3e..da17346b4c 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -585,7 +585,7 @@ static bool is_ceqv(type_context_old & ctx, name const & id, expr e) { for_each(binding_domain(e), visitor_fn); } expr local = locals.push_local(name(), binding_domain(e)); - if (binding_info(e).is_inst_implicit()) { + if (is_inst_implicit(binding_info(e))) { // If the argument can be instantiated by type class resolution, then // we don't need to find it in the lhs } else if (ctx.is_prop(binding_domain(e))) { @@ -720,7 +720,7 @@ static simp_lemmas add_core(type_context_old & ctx, simp_lemmas const & s, name while (is_pi(rule)) { expr mvar = ctx.mk_tmp_mvar(binding_domain(rule)); emetas.push_back(mvar); - instances.push_back(binding_info(rule).is_inst_implicit()); + instances.push_back(is_inst_implicit(binding_info(rule))); rule = instantiate(binding_body(rule), mvar); proof = mk_app(proof, mvar); } @@ -791,7 +791,7 @@ static simp_lemmas add_core(type_context_old & ctx, simp_lemmas const & s, name while (is_pi(type)) { expr mvar = ctx.mk_tmp_mvar(binding_domain(type)); emetas.push_back(mvar); - instances.push_back(binding_info(type).is_inst_implicit()); + instances.push_back(is_inst_implicit(binding_info(type))); type = instantiate(binding_body(type), mvar); proof = mk_app(proof, mvar); } @@ -902,7 +902,7 @@ static simp_lemmas add_congr_core(type_context_old & ctx, simp_lemmas const & s, expr mvar = ctx.mk_tmp_mvar(binding_domain(rule)); emetas.push_back(mvar); explicits.push_back(is_explicit(binding_info(rule))); - instances.push_back(binding_info(rule).is_inst_implicit()); + instances.push_back(is_inst_implicit(binding_info(rule))); rule = instantiate(binding_body(rule), mvar); proof = mk_app(proof, mvar); } diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index b566ed34a2..5e713ca9a1 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -103,7 +103,7 @@ void type_context_old::init_local_instances() { meta def nat_has_false : has_false ℕ := by apply_instance */ - if (!decl.get_info().is_rec()) { + if (!is_rec(decl.get_info())) { if (auto cls_name = is_class(decl.get_type())) { m_local_instances = local_instances(local_instance(*cls_name, decl.mk_ref()), m_local_instances); } @@ -192,7 +192,7 @@ void type_context_old::update_local_instances(expr const & new_local, expr const } } -expr type_context_old::push_local(name const & pp_name, expr const & type, binder_info const & bi) { +expr type_context_old::push_local(name const & pp_name, expr const & type, binder_info bi) { expr local = m_lctx.mk_local_decl(pp_name, type, bi); update_local_instances(local, type); return local; @@ -307,7 +307,7 @@ pair type_context_old::revert_core(buffer & to_revert We don't need to follow the value of local definitions (x := v) here because we are using for_each_after. */ if (depends_on(d, m_mctx, to_revert)) { - if (d.get_info().is_rec()) { + if (is_rec(d.get_info())) { /* We should not revert auxiliary declarations added by the equation compiler. See discussion at issue #1258 at github. */ sstream out; @@ -3465,7 +3465,7 @@ struct instance_synthesizer { break; type = new_type; expr new_mvar = m_ctx.mk_tmp_mvar(locals.mk_pi(binding_domain(type))); - if (binding_info(type).is_inst_implicit()) { + if (is_inst_implicit(binding_info(type))) { new_inst_mvars.push_back(new_mvar); } expr new_arg = mk_app(new_mvar, locals.as_buffer()); diff --git a/src/library/type_context.h b/src/library/type_context.h index 0bd95a703c..3e1650fef0 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -667,7 +667,7 @@ public: optional is_stuck_projection(expr const & e); virtual optional is_stuck(expr const &) override; - virtual expr push_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) override; + virtual expr push_local(name const & pp_name, expr const & type, binder_info bi = mk_binder_info()) override; virtual expr push_local_from_binding(expr const & e) { lean_assert(is_binding(e)); return push_local(binding_name(e), binding_domain(e), binding_info(e)); @@ -1021,7 +1021,7 @@ public: type_context_old & ctx() { return m_ctx; } - expr push_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) { + expr push_local(name const & pp_name, expr const & type, binder_info bi = mk_binder_info()) { expr r = m_ctx.push_local(pp_name, type, bi); m_locals.push_back(r); return r; diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp index 2a1580fd85..d5204a7fe7 100644 --- a/src/library/user_recursors.cpp +++ b/src/library/user_recursors.cpp @@ -183,7 +183,7 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional break; } if (j == I_args.size()) { - if (local_info(tele[i]).is_inst_implicit()) { + if (is_inst_implicit(local_info(tele[i]))) { params_pos.push_back(optional()); } else { throw exception(sstream() << "invalid user defined recursor, type of the major premise '" << major diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index 055f427221..acb4c5872c 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -62,30 +62,11 @@ vm_obj to_obj(optional const & e) { binder_info to_binder_info(vm_obj const & o) { lean_assert(is_simple(o)); - /* - inductive binder_info := - | default | implicit | strict_implicit | inst_implicit | aux_decl - */ - switch (cidx(o)) { - case 0: return binder_info(); - case 1: return mk_implicit_binder_info(); - case 2: return mk_strict_implicit_binder_info(); - case 3: return mk_inst_implicit_binder_info(); - default: return mk_rec_info(); - } + return static_cast(cidx(o)); } -vm_obj to_obj(binder_info const & bi) { - if (bi.is_implicit()) - return mk_vm_simple(1); - else if (bi.is_strict_implicit()) - return mk_vm_simple(2); - else if (bi.is_inst_implicit()) - return mk_vm_simple(3); - else if (bi.is_rec()) - return mk_vm_simple(4); - else - return mk_vm_simple(0); +vm_obj to_obj(binder_info bi) { + return mk_vm_simple(static_cast(bi)); } // The expr_bvar_intro function has an _intro suffix so that it doesn't clash @@ -119,7 +100,7 @@ vm_obj expr_mvar_intro(vm_obj const & n, vm_obj const & pp_n, vm_obj const & t) } vm_obj expr_fvar_const_intro(vm_obj const & n) { - return to_obj(mk_local(to_name(n), to_name(n), expr(), binder_info())); + return to_obj(mk_local(to_name(n), to_name(n), expr(), mk_binder_info())); } vm_obj expr_app_intro(vm_obj const & f, vm_obj const & a) { diff --git a/src/library/vm/vm_expr.h b/src/library/vm/vm_expr.h index 6c3ac6534d..c5aaadb6db 100644 --- a/src/library/vm/vm_expr.h +++ b/src/library/vm/vm_expr.h @@ -10,7 +10,7 @@ Author: Leonardo de Moura namespace lean { binder_info to_binder_info(vm_obj const & o); -vm_obj to_obj(binder_info const & bi); +vm_obj to_obj(binder_info bi); bool is_expr(vm_obj const & o); expr const & to_expr(vm_obj const & o); vm_obj to_obj(expr const & e);