diff --git a/src/frontends/lean/lean_frontend.cpp b/src/frontends/lean/lean_frontend.cpp index b7e525051..db050bae6 100644 --- a/src/frontends/lean/lean_frontend.cpp +++ b/src/frontends/lean/lean_frontend.cpp @@ -306,10 +306,9 @@ void frontend::mark_implicit_arguments(name const & n, unsigned num) { mark_implicit_arguments(n, tmp.size(), tmp.data()); } void frontend::mark_implicit_arguments(name const & n, unsigned sz, unsigned * implicit) { m_imp->mark_implicit_arguments(n, sz, implicit); } -bool frontend::has_implicit_arguments(name const & n) { return m_imp->has_implicit_arguments(n); } -std::vector const & frontend::get_implicit_arguments(name const & n) { return m_imp->get_implicit_arguments(n); } -name const & frontend::get_explicit_version(name const & n) { return m_imp->get_explicit_version(n); } - +bool frontend::has_implicit_arguments(name const & n) const { return m_imp->has_implicit_arguments(n); } +std::vector const & frontend::get_implicit_arguments(name const & n) const { return m_imp->get_implicit_arguments(n); } +name const & frontend::get_explicit_version(name const & n) const { return m_imp->get_explicit_version(n); } state const & frontend::get_state() const { return m_imp->m_state; } state & frontend::get_state_core() { return m_imp->m_state; } diff --git a/src/frontends/lean/lean_frontend.h b/src/frontends/lean/lean_frontend.h index bfacc7fd1..c18becaa8 100644 --- a/src/frontends/lean/lean_frontend.h +++ b/src/frontends/lean/lean_frontend.h @@ -134,9 +134,9 @@ public: */ void mark_implicit_arguments(name const & n, unsigned sz, unsigned * implicit); /** \brief Return true iff \c n has implicit arguments */ - bool has_implicit_arguments(name const & n); + bool has_implicit_arguments(name const & n) const; /** \brief Return the position of the arguments that are implicit. */ - std::vector const & get_implicit_arguments(name const & n); + std::vector const & get_implicit_arguments(name const & n) const; /** \brief This frontend associates an definition with each definition (or postulate) that has implicit arguments. The @@ -145,7 +145,7 @@ public: frontend can't figure out the value for the implicit arguments. */ - name const & get_explicit_version(name const & n); + name const & get_explicit_version(name const & n) const; /*@}*/ /** diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index 36b6f1bc4..cf96f5645 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -1298,8 +1298,6 @@ class parser::imp { /** \brief Parse a Lean command. */ void parse_command() { - if (m_interactive && !m_use_exceptions) - reset_interrupt(); m_elaborator.clear(); m_expr_pos_info.clear(); m_last_cmd_pos = pos(); @@ -1419,6 +1417,7 @@ public: } catch (interrupted & ex) { if (m_verbose) regular(m_frontend) << "\n!!!Interrupted!!!" << endl; + reset_interrupt(); sync(); if (m_use_exceptions) throw; diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp index 32344e35b..6c5940374 100644 --- a/src/frontends/lean/lean_pp.cpp +++ b/src/frontends/lean/lean_pp.cpp @@ -100,6 +100,7 @@ static name g_nu("\u03BD"); The resultant name is based on abst_name(e). */ name get_unused_name(expr const & e) { + lean_assert(is_abstraction(e) || is_let(e)); name const & n = is_abstraction(e) ? abst_name(e) : let_name(e); name n1 = n; unsigned i = 1; @@ -561,6 +562,10 @@ class pp_fn { return r; } + bool is_implicit(std::vector const * implicit_args, unsigned arg_pos) { + return implicit_args && std::find(implicit_args->begin(), implicit_args->end(), arg_pos) != implicit_args->end(); + } + /** \brief Pretty print Lambdas, Pis and compact definitions. When T != 0, it is a compact definition. @@ -578,8 +583,8 @@ class pp_fn { \remark if T != 0, then T is Pi(x : A), B */ - result pp_abstraction_core(expr const & e, unsigned depth, expr T) { - if (is_arrow(e)) { + result pp_abstraction_core(expr const & e, unsigned depth, expr T, std::vector const * implicit_args = nullptr) { + if (is_arrow(e) && !implicit_args) { lean_assert(!T); result p_lhs = pp_child(abst_domain(e), depth); result p_rhs = pp_arrow_body(abst_body(e), depth); @@ -592,7 +597,7 @@ class pp_fn { T = p.second; unsigned head_indent = m_indent; format head; - if (!T) { + if (!T && !implicit_args) { if (m_notation) { head = is_lambda(e) ? g_lambda_n_fmt : g_Pi_n_fmt; head_indent = 2; @@ -605,11 +610,15 @@ class pp_fn { if (T) { format T_f = pp(T, 0).first; body_sep = format{space(), colon(), space(), T_f, space(), g_assign_fmt}; + } else if (implicit_args) { + // This is a little hack to pretty print Variable and + // Axiom declarations that contain implicit arguments + body_sep = compose(space(), colon()); } else { body_sep = comma(); } expr domain0 = nested[0].second; - if (std::all_of(nested.begin() + 1, nested.end(), [&](std::pair const & p) { return p.second == domain0; })) { + if (std::all_of(nested.begin() + 1, nested.end(), [&](std::pair const & p) { return p.second == domain0; }) && !implicit_args) { // Domain of all binders is the same format names = pp_bnames(nested.begin(), nested.end(), false); result p_domain = pp_scoped_child(domain0, depth); @@ -623,18 +632,24 @@ class pp_fn { auto it = nested.begin(); auto end = nested.end(); unsigned r_weight = 1; + unsigned arg_pos = 0; // PP binders in blocks (names ... : type) bool first = true; format bindings; while (it != end) { auto it2 = it; ++it2; - while (it2 != end && it2->second == it->second) { + bool implicit = is_implicit(implicit_args, arg_pos); + ++arg_pos; + while (it2 != end && it2->second == it->second && implicit == is_implicit(implicit_args, arg_pos)) { ++it2; + ++arg_pos; } result p_domain = pp_scoped_child(it->second, depth); r_weight += p_domain.second; - format block = group(nest(m_indent, format{lp(), pp_bnames(it, it2, true), space(), colon(), space(), p_domain.first, rp()})); + format const & par_open = implicit ? lcurly() : lp(); + format const & par_close = implicit ? rcurly() : rp(); + format block = group(nest(m_indent, format{par_open, pp_bnames(it, it2, true), space(), colon(), space(), p_domain.first, par_close})); if (first) { bindings = block; first = false; @@ -807,10 +822,15 @@ public: return pp_scoped_child(e, 0).first; } - format pp_definition(expr const & v, expr const & t) { + format pp_definition(expr const & v, expr const & t, std::vector const * implicit_args) { init(mk_app(v, t)); expr T(t); - return pp_abstraction_core(v, 0, T).first; + return pp_abstraction_core(v, 0, T, implicit_args).first; + } + + format pp_pi_with_implicit_args(expr const & e, std::vector const & implicit_args) { + init(e); + return pp_abstraction_core(e, 0, expr(), &implicit_args).first; } void set_interrupt(bool flag) { @@ -881,9 +901,12 @@ class pp_formatter_cell : public formatter_cell { return pp_definition(kwd, n, t, v, opts); } else { lean_assert(is_lambda(v)); + std::vector const * implicit_args = nullptr; + if (m_frontend.has_implicit_arguments(n)) + implicit_args = &(m_frontend.get_implicit_arguments(n)); pp_fn fn(m_frontend, opts); scoped_set_interruptable_ptr set(m_pp_fn, &fn); - format def = fn.pp_definition(v, t); + format def = fn.pp_definition(v, t, implicit_args); return format{highlight_command(format(kwd)), space(), format(n), def}; } } @@ -893,7 +916,17 @@ class pp_formatter_cell : public formatter_cell { } format pp_postulate(object const & obj, options const & opts) { - return format{highlight_command(format(obj.keyword())), space(), format(obj.get_name()), space(), colon(), space(), pp(obj.get_type(), opts)}; + char const * kwd = obj.keyword(); + name const & n = obj.get_name(); + format r = format{highlight_command(format(kwd)), space(), format(n)}; + if (m_frontend.has_implicit_arguments(n)) { + pp_fn fn(m_frontend, opts); + scoped_set_interruptable_ptr set(m_pp_fn, &fn); + r += fn.pp_pi_with_implicit_args(obj.get_type(), m_frontend.get_implicit_arguments(n)); + } else { + r += format{space(), colon(), space(), pp(obj.get_type(), opts)}; + } + return r; } format pp_definition(object const & obj, options const & opts) { @@ -929,8 +962,8 @@ public: expr c2 = context_to_lambda(c, e); while (is_fake_context(c2)) { check_interrupted(m_interrupted); + name n1 = get_unused_name(c2); expr const & rest = fake_context_rest(c2); - name n1 = get_unused_name(rest); c2 = instantiate_with_closed(rest, mk_constant(n1)); } return pp(c2, opts); diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index d7390705c..45dfdae06 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -133,30 +133,20 @@ static format g_line(mk_line()); static format g_space(" "); static format g_lp("("); static format g_rp(")"); +static format g_lcurly("{"); +static format g_rcurly("}"); static format g_comma(","); static format g_colon(":"); static format g_dot("."); -format const & line() { - return g_line; -} -format const & space() { - return g_space; -} -format const & lp() { - return g_lp; -} -format const & rp() { - return g_rp; -} -format const & comma() { - return g_comma; -} -format const & colon() { - return g_colon; -} -format const & dot() { - return g_dot; -} +format const & line() { return g_line; } +format const & space() { return g_space; } +format const & lp() { return g_lp; } +format const & rp() { return g_rp; } +format const & lcurly() { return g_lcurly; } +format const & rcurly() { return g_rcurly; } +format const & comma() { return g_comma; } +format const & colon() { return g_colon; } +format const & dot() { return g_dot; } // Auxiliary flag used to mark whether flatten // produce a different sexpr static bool thread_local g_diff_flatten = false; diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h index 95c1b3a26..779b02684 100644 --- a/src/util/sexpr/format.h +++ b/src/util/sexpr/format.h @@ -231,6 +231,8 @@ format const & line(); format const & space(); format const & lp(); format const & rp(); +format const & lcurly(); +format const & rcurly(); format const & comma(); format const & colon(); format const & dot();