From 15c1c978735f7849535fccf61e908473a576ff43 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 16 Aug 2013 20:39:24 -0700 Subject: [PATCH] Refactor frontend pretty printer Signed-off-by: Leonardo de Moura --- src/exprlib/context_to_lambda.cpp | 27 +++- src/exprlib/context_to_lambda.h | 45 +++++- src/exprlib/printer.cpp | 2 +- src/frontend/frontend.cpp | 4 +- src/frontend/frontend.h | 8 +- src/frontend/operator_info.cpp | 2 +- src/frontend/pp.cpp | 219 ++++++++++++++++++++---------- src/frontend/pp.h | 25 +--- src/kernel/expr.h | 4 + src/tests/frontend/frontend.cpp | 22 ++- 10 files changed, 247 insertions(+), 111 deletions(-) diff --git a/src/exprlib/context_to_lambda.cpp b/src/exprlib/context_to_lambda.cpp index 4c66528b7..14e607ed8 100644 --- a/src/exprlib/context_to_lambda.cpp +++ b/src/exprlib/context_to_lambda.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include "context_to_lambda.h" namespace lean { -static expr g_foo = Const("foo"); +static expr g_fake = Const(name(name(0u), "context_to_lambda")); expr context_to_lambda(context const & c, expr const & e) { if (!c) { return e; @@ -15,10 +15,31 @@ expr context_to_lambda(context const & c, expr const & e) { context_entry const & entry = head(c); expr t; if (entry.get_body()) - t = g_foo(entry.get_domain(), entry.get_body()); + t = mk_app(g_fake, entry.get_domain(), entry.get_body()); else - t = g_foo(entry.get_domain()); + t = mk_app(g_fake, entry.get_domain()); return context_to_lambda(tail(c), mk_lambda(entry.get_name(), t, e)); } } +bool is_fake_context(expr const & e) { + return is_lambda(e) && is_app(abst_domain(e)) && arg(abst_domain(e),0) == g_fake; +} +name const & fake_context_name(expr const & e) { + lean_assert(is_fake_context(e)); + return abst_name(e); +} +expr const & fake_context_domain(expr const & e) { + lean_assert(is_fake_context(e)); + return arg(abst_domain(e), 1); +} +expr const & fake_context_value(expr const & e) { + lean_assert(is_fake_context(e)); + if (num_args(abst_domain(e)) > 2) + return arg(abst_domain(e), 2); + else + return expr::null(); +} +expr const & fake_context_rest(expr const & e) { + return abst_body(e); +} } diff --git a/src/exprlib/context_to_lambda.h b/src/exprlib/context_to_lambda.h index db83ade85..175764d68 100644 --- a/src/exprlib/context_to_lambda.h +++ b/src/exprlib/context_to_lambda.h @@ -11,16 +11,55 @@ namespace lean { \brief Given the context (n_1 : T_1 [:= V_1]) ... (n_k : T_k [:= V_k]) and expression e into, return the "meaningless" lambda expression: - (lambda (n_1 : (foo T_1 V_1)) ... (lambda (n_k : (foo T_k V_k)) e)) + (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e)) - The constant "foo" is irrelevant, it is just used as a marker. + The constant "fake" is irrelevant, it is just used as a marker. It is used to "glue" T_i and V_i. This little hack allows us to use the machinery for instantiating lambdas with contexts. \remark If a context entry (n_i : T_i [:= V_i]) does not have a - value V_i, then we just use (foo T_i). + value V_i, then we just use (fake T_i). */ expr context_to_lambda(context const & c, expr const & e); + +/** + \brief Return true if \c e is a fake context created using + context_to_lambda. + (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e)) +*/ +bool is_fake_context(expr const & e); + +/** + \brief Return the name n_1 of the head of the (fake) context + (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e)) + + \pre is_fake_context(e) +*/ +name const & fake_context_name(expr const & e); + +/** + \brief Return the domain T_1 of the head of the (fake) context + (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e)) + + \pre is_fake_context(e) +*/ +expr const & fake_context_domain(expr const & e); + +/** + \brief Return the value V_1 of the head of the (fake) context + (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e)) + + \pre is_fake_context(e) + \remark If the head does not have a value, then return a null expression +*/ +expr const & fake_context_value(expr const & e); +/** + \brief Return the rest (lambda (n_2 : (fake T_2 V_2)) ... (lambda (n_k : (fake T_k V_k)) e)) of the fake context + (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e)) + + \pre is_fake_context(e) +*/ +expr const & fake_context_rest(expr const & e); } diff --git a/src/exprlib/printer.cpp b/src/exprlib/printer.cpp index 08c4466e2..9c1b9f9c5 100644 --- a/src/exprlib/printer.cpp +++ b/src/exprlib/printer.cpp @@ -144,7 +144,7 @@ std::ostream & operator<<(std::ostream & out, context const & ctx) { out << tail(ctx); out << head(ctx).get_name() << " : " << head(ctx).get_domain(); if (head(ctx).get_body()) { - out << " := " << head(ctx).get_body(); + out << " := " << mk_pair(head(ctx).get_body(), tail(ctx)); } out << "\n"; } diff --git a/src/frontend/frontend.cpp b/src/frontend/frontend.cpp index 7e6e587c2..b983a5116 100644 --- a/src/frontend/frontend.cpp +++ b/src/frontend/frontend.cpp @@ -189,7 +189,7 @@ bool frontend::has_children() const { return m_imp->has_children(); } bool frontend::has_parent() const { return m_imp->has_parent(); } frontend frontend::parent() const { lean_assert(has_parent()); return frontend(m_imp->m_parent); } -environment const & frontend::env() const { return m_imp->m_env; } +environment const & frontend::get_environment() const { return m_imp->m_env; } level frontend::add_uvar(name const & n, level const & l) { return m_imp->m_env.add_uvar(n, l); } level frontend::add_uvar(name const & n) { return m_imp->m_env.add_uvar(n); } @@ -203,7 +203,5 @@ void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, name cons void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixr(sz, opns, p, n); } void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixc(sz, opns, p, n); } operator_info frontend::find_op_for(name const & n) const { return m_imp->find_op_for(n); } - -void frontend::display(std::ostream & out) const { m_imp->m_env.display(out); } } diff --git a/src/frontend/frontend.h b/src/frontend/frontend.h index fa0b3d8fc..e20263c48 100644 --- a/src/frontend/frontend.h +++ b/src/frontend/frontend.h @@ -43,8 +43,8 @@ public: // ======================================= /** \brief Coercion frontend -> environment. */ - environment const & env() const; - operator environment const &() const { return env(); } + environment const & get_environment() const; + operator environment const &() const { return get_environment(); } level add_uvar(name const & n, level const & l); level add_uvar(name const & n); @@ -68,9 +68,5 @@ public: */ operator_info find_op_for(name const & n) const; // ======================================= - - /** \brief Display universal variable constraints and objects stored in this environment and its parents. */ - void display(std::ostream & out) const; }; -inline std::ostream & operator<<(std::ostream & out, frontend const & f) { f.display(out); return out; } } diff --git a/src/frontend/operator_info.cpp b/src/frontend/operator_info.cpp index e5a8351c9..b98c5df4c 100644 --- a/src/frontend/operator_info.cpp +++ b/src/frontend/operator_info.cpp @@ -118,7 +118,7 @@ char const * to_string(fixity f) { format pp(operator_info const & o) { format r; - r = format(to_string(o.get_fixity())); + r = highlight_command(format(to_string(o.get_fixity()))); if (o.get_precedence() != 0) r += format{space(), format(o.get_precedence())}; for (auto p : o.get_op_name_parts()) diff --git a/src/frontend/pp.cpp b/src/frontend/pp.cpp index 0496d4c7f..a09e7308c 100644 --- a/src/frontend/pp.cpp +++ b/src/frontend/pp.cpp @@ -13,35 +13,10 @@ Author: Leonardo de Moura #include "occurs.h" #include "instantiate.h" #include "builtin_notation.h" +#include "context_to_lambda.h" +#include "printer.h" #include "options.h" -namespace lean { - -format expr_formatter::operator()(char const * kwd, name const & n, expr const & t, expr const & v) { - format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), - operator()(t), space(), highlight_keyword(format(":=")), line(), operator()(v)}; - return group(nest(def)); -} - -format expr_formatter::operator()(char const * kwd, name const & n, expr const & t) { - format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), operator()(t)}; - return group(nest(def)); -} - -void expr_formatter::pp(std::ostream & out, expr const & e, context const & c) { - out << mk_pair(operator()(e, c), get_options()); -} - -void expr_formatter::pp(std::ostream & out, expr const & e) { - pp(out, e, context()); -} - -format expr_formatter::nest(format const & f) { - return ::lean::nest(get_pp_indent(get_options()), f); -} - -} - #ifndef LEAN_DEFAULT_PP_MAX_DEPTH #define LEAN_DEFAULT_PP_MAX_DEPTH std::numeric_limits::max() #endif @@ -67,17 +42,19 @@ format expr_formatter::nest(format const & f) { #endif namespace lean { -static format g_Type_fmt = highlight_builtin(format("Type")); -static format g_eq_fmt = format("="); -static char const * g_eq_sym = "eq"; -static unsigned g_eq_sz = strlen(g_eq_sym); -static format g_eq_sym_fmt = format(g_eq_sym); -static format g_lambda_fmt = highlight_keyword(format("\u03BB")); -static format g_Pi_fmt = highlight_keyword(format("\u03A0")); -static format g_arrow_fmt = highlight_keyword(format("\u2192")); -static format g_ellipsis_fmt = highlight(format("\u2026")); -static format g_let_fmt = highlight_keyword(format("let")); -static format g_in_fmt = highlight_keyword(format("in")); +static format g_Type_fmt = highlight_builtin(format("Type")); +static format g_eq_fmt = format("="); +static char const * g_eq_sym = "eq"; +static unsigned g_eq_sz = strlen(g_eq_sym); +static format g_eq_sym_fmt = format(g_eq_sym); +static format g_lambda_fmt = highlight_keyword(format("\u03BB")); +static format g_Pi_fmt = highlight_keyword(format("\u03A0")); +static format g_arrow_fmt = highlight_keyword(format("\u2192")); +static format g_ellipsis_fmt = highlight(format("\u2026")); +static format g_let_fmt = highlight_keyword(format("let")); +static format g_in_fmt = highlight_keyword(format("in")); +static format g_assign_fmt = highlight_keyword(format(":=")); +static format g_geq_fmt = format("\u2265"); static name g_pp_max_depth {"pp", "max_depth"}; static name g_pp_max_steps {"pp", "max_steps"}; @@ -93,12 +70,27 @@ bool get_pp_notation(options const & opts) { return opts.get_bool(g_p bool get_pp_extra_lets(options const & opts) { return opts.get_bool(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS); } unsigned get_pp_alias_min_depth(options const & opts) { return opts.get_unsigned(g_pp_alias_min_depth, LEAN_DEFAULT_PP_ALIAS_MIN_DEPTH); } +/** + \brief Return a fresh name for the given abstraction. + By fresh, we mean a name that is not used for any constant in abst_body(e). + The resultant name is based on abst_name(e). +*/ +name get_unused_name(expr const & e) { + name const & n = abst_name(e); + name n1 = n; + unsigned i = 1; + while (occurs(n1, abst_body(e))) { + n1 = name(n, i); + i++; + } + return n1; +} + /** \brief Functional object for pretty printing expressions */ class pp_fn { typedef scoped_map aliases; typedef std::vector> aliases_defs; frontend const & m_frontend; - context const & m_context; // State aliases m_aliases; aliases_defs m_aliases_defs; @@ -349,13 +341,7 @@ class pp_fn { */ std::pair collect_nested(expr const & e, expr T, expr_kind k, buffer> & r) { if (e.kind() == k) { - name const & n = abst_name(e); - name n1 = n; - unsigned i = 1; - while (occurs(n1, abst_body(e))) { - n1 = name(n, i); - i++; - } + name n1 = get_unused_name(e); r.push_back(mk_pair(n1, abst_domain(e))); expr b = instantiate_with_closed(abst_body(e), mk_constant(n1)); if (T) @@ -432,7 +418,7 @@ class pp_fn { format body_sep; if (T) { format T_f = pp(T, 0).first; - body_sep = format{space(), colon(), space(), T_f, space(), highlight_keyword(format(":="))}; + body_sep = format{space(), colon(), space(), T_f, space(), g_assign_fmt}; } else { body_sep = comma(); } @@ -570,9 +556,8 @@ class pp_fn { } public: - pp_fn(frontend const & fe, context const & ctx, options const & opts): - m_frontend(fe), - m_context(ctx) { + pp_fn(frontend const & fe, options const & opts): + m_frontend(fe) { set_options(opts); } @@ -588,49 +573,141 @@ public: } }; -class pp_expr_formatter : public expr_formatter { +class pp_formatter : public formatter { frontend const & m_frontend; options m_options; -public: - pp_expr_formatter(frontend const & fe, options const & opts): - m_frontend(fe), - m_options(opts) { + unsigned m_indent; + + format pp(expr const & e) { + return pp_fn(m_frontend, m_options)(e); } - virtual ~pp_expr_formatter() { + format pp(context const & c, expr const & e, bool include_e) { + format r; + bool first = true; + expr c2 = context_to_lambda(c, e); + while (is_fake_context(c2)) { + name n1 = get_unused_name(c2); + format entry = format{format(n1), space(), colon(), space(), pp(fake_context_domain(c2))}; + expr val = fake_context_value(c2); + if (val) + entry += format{space(), g_assign_fmt, nest(m_indent, format{line(), pp(val)})}; + if (first) { + r = group(entry); + first = false; + } else { + r += format{line(), group(entry)}; + } + c2 = instantiate_with_closed(fake_context_rest(c2), mk_constant(n1)); + } + if (include_e) { + if (first) + r += format{line(), pp(c2)}; + else + r = pp(c2); + } else { + return r; + } + return r; } - virtual options get_options() const { - return m_options; + format pp_definition(char const * kwd, name const & n, expr const & t, expr const & v) { + format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), + pp(t), space(), g_assign_fmt, line(), pp(v)}; + return group(nest(m_indent, def)); } - // TODO: remove context parameter from expr_formatter - // The context pretty printer must open the expression - // before pretty-printing it. - virtual format operator()(expr const & e, context const & c) { - return pp_fn(m_frontend, c, m_options)(e); - } - - virtual format operator()(char const * kwd, name const & n, expr const & t, expr const & v) { + format pp_compact_definition(char const * kwd, name const & n, expr const & t, expr const & v) { expr it1 = t; expr it2 = v; while (is_pi(it1) && is_lambda(it2)) { if (abst_domain(it1) != abst_domain(it2)) - return expr_formatter::operator()(kwd, n, t, v); + return pp_definition(kwd, n, t, v); it1 = abst_body(it1); it2 = abst_body(it2); } if (!is_lambda(v) || is_pi(it1) || is_lambda(it2)) { - return expr_formatter::operator()(kwd, n, t, v); + return pp_definition(kwd, n, t, v); } else { lean_assert(is_lambda(v)); - format def = pp_fn(m_frontend, context(), m_options).pp_definition(v, t); + format def = pp_fn(m_frontend, m_options).pp_definition(v, t); return format{highlight_command(format(kwd)), space(), format(n), def}; } } + + format pp_uvar_decl(object const & obj) { + return format{highlight_command(format(obj.keyword())), space(), format(obj.get_name()), space(), format("\u2265"), space(), ::lean::pp(obj.get_cnstr_level())}; + } + + format pp_postulate(object const & obj) { + return format{highlight_command(format(obj.keyword())), space(), format(obj.get_name()), space(), colon(), space(), pp(obj.get_type())}; + } + + format pp_definition(object const & obj) { + return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value()); + } + + format pp_notation_decl(object const & obj) { + return ::lean::pp(*(static_cast(obj.cell()))); + } + +public: + pp_formatter(frontend const & fe, options const & opts): + m_frontend(fe), + m_options(opts) { + m_indent = get_pp_indent(opts); + } + + virtual ~pp_formatter() { + } + + virtual format operator()(expr const & e) { + return pp(e); + } + + virtual format operator()(context const & c) { + return pp(c, Type(), false); + } + + virtual format operator()(context const & c, expr const & e, bool format_ctx) { + if (format_ctx) { + return pp(c, e, true); + } else { + expr c2 = context_to_lambda(c, e); + while (is_fake_context(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); + } + } + + virtual format operator()(environment const & env) { + format r; + bool first = true; + std::for_each(env.begin_objects(), + env.end_objects(), + [&](object const & obj) { + if (first) first = false; else r += line(); + switch (obj.kind()) { + case object_kind::UVarDeclaration: r += pp_uvar_decl(obj); break; + case object_kind::Postulate: r += pp_postulate(obj); break; + case object_kind::Definition: r += pp_definition(obj); break; + case object_kind::Neutral: r += pp_notation_decl(obj); break; + } + }); + return r; + } }; -std::shared_ptr mk_pp_expr_formatter(frontend const & fe, options const & opts) { - return std::shared_ptr(new pp_expr_formatter(fe, opts)); +std::shared_ptr mk_pp_formatter(frontend const & fe, options const & opts) { + return std::shared_ptr(new pp_formatter(fe, opts)); +} + +std::ostream & operator<<(std::ostream & out, frontend const & fe) { + auto pp = mk_pp_formatter(fe, options()); + out << (*pp)(fe.get_environment()); + return out; } } diff --git a/src/frontend/pp.h b/src/frontend/pp.h index 3b784981d..c05ac6921 100644 --- a/src/frontend/pp.h +++ b/src/frontend/pp.h @@ -6,28 +6,11 @@ Author: Leonardo de Moura */ #pragma once #include "context.h" +#include "formatter.h" +#include "options.h" namespace lean { - class frontend; -class expr_formatter { -public: - virtual ~expr_formatter() {} - /** \brief Convert expression in the given context into a format object. */ - virtual format operator()(expr const & e, context const & c = context()) = 0; - /** \brief format a definition. */ - virtual format operator()(char const * kwd, name const & n, expr const & t, expr const & v); - /** \brief format a postulate. */ - virtual format operator()(char const * kwd, name const & n, expr const & t); - - /** \brief Return options for pretty printing. */ - virtual options get_options() const = 0; - - void pp(std::ostream & out, expr const & e, context const & c); - void pp(std::ostream & out, expr const & e); - - /** \brief Nest the given format object using the setting provided by get_options. */ - format nest(format const & f); -}; -std::shared_ptr mk_pp_formatter(frontend const & fe, options const & opts); +std::shared_ptr mk_pp_formatter(frontend const & fe, options const & opts = options()); +std::ostream & operator<<(std::ostream & out, frontend const & fe); } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index bcc721906..e8f7b5146 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -337,6 +337,10 @@ inline unsigned var_idx(expr const & e) { return to_var(e)->ge /** \brief Return true iff the given expression is a variable with de Bruijn index equal to \c i. */ inline bool is_var(expr const & e, unsigned i) { return is_var(e) && var_idx(e) == i; } inline name const & const_name(expr const & e) { return to_constant(e)->get_name(); } +/** \brief Return true iff the given expression is a constant with name \c n. */ +inline bool is_constant(expr const & e, name const & n) { + return is_constant(e) && const_name(e) == n; +} inline value const & to_value(expr const & e) { return to_value(e.raw()); } inline unsigned num_args(expr const & e) { return to_app(e)->get_num_args(); } inline expr const & arg(expr const & e, unsigned idx) { return to_app(e)->get_arg(idx); } diff --git a/src/tests/frontend/frontend.cpp b/src/tests/frontend/frontend.cpp index 3048b2e7c..8f412d947 100644 --- a/src/tests/frontend/frontend.cpp +++ b/src/tests/frontend/frontend.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "frontend.h" #include "environment.h" #include "operator_info.h" +#include "pp.h" #include "test.h" using namespace lean; @@ -15,7 +16,7 @@ static void tst1() { f.add_uvar("tst"); frontend c = f.mk_child(); lean_assert(c.get_uvar("tst") == f.get_uvar("tst")); - lean_assert(f.env().has_children()); + lean_assert(f.get_environment().has_children()); } static void tst2() { @@ -49,10 +50,27 @@ static void tst2() { static void tst3() { frontend f; std::cout << "====================\n"; - std::cout << f; + std::cout << f << "\n"; +} + +static void tst4() { + frontend f; + std::shared_ptr fmt_ptr = mk_pp_formatter(f); + formatter & fmt = *fmt_ptr; + expr Bool = Const("Bool"); + context c; + c = extend(c, "x", Bool); + c = extend(c, "y", Bool); + c = extend(c, "x", Bool, Var(1)); + c = extend(c, "x", Bool, Var(2)); + c = extend(c, "z", Bool, Var(1)); + c = extend(c, "x", Bool, Var(4)); + std::cout << fmt(c) << "\n"; } int main() { + tst4(); + return 0; tst1(); tst2(); tst3();