From 405e57eb2d7bd7aaabcf27d39136ed58b659555c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Jul 2014 18:32:00 +0100 Subject: [PATCH] refactor(kernel/formatter): add formatter_factory, and simplify formatter interface Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_cmds.cpp | 11 +- src/frontends/lean/elaborator.cpp | 48 ++---- src/frontends/lean/parser.h | 4 +- src/frontends/lean/pp.cpp | 16 +- src/frontends/lean/pp.h | 2 +- src/kernel/error_msgs.cpp | 33 ++--- src/kernel/error_msgs.h | 15 +- src/kernel/expr.cpp | 2 +- src/kernel/expr.h | 7 +- src/kernel/formatter.cpp | 21 ++- src/kernel/formatter.h | 37 ++--- src/kernel/justification.cpp | 14 +- src/kernel/justification.h | 6 +- src/kernel/kernel_exception.cpp | 6 +- src/kernel/kernel_exception.h | 2 +- src/kernel/type_checker.cpp | 59 +++----- src/kernel/type_checker.h | 5 +- src/library/error_handling/error_handling.cpp | 2 +- src/library/io_state.cpp | 16 +- src/library/io_state.h | 12 +- src/library/io_state_stream.cpp | 4 +- src/library/io_state_stream.h | 36 ++--- src/library/kernel_bindings.cpp | 139 ++++++++++-------- src/library/kernel_bindings.h | 13 +- src/library/string.cpp | 2 +- src/library/tactic/goal.cpp | 20 +-- src/library/tactic/goal.h | 2 +- src/library/tactic/proof_state.cpp | 22 ++- src/library/tactic/proof_state.h | 2 +- src/library/unifier.cpp | 2 +- src/shell/lean.cpp | 2 +- src/tests/kernel/environment.cpp | 14 +- tests/lua/hott1.lua | 3 +- 33 files changed, 261 insertions(+), 318 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index b0c055398..add612d7c 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -99,11 +99,12 @@ environment check_cmd(parser & p) { e = instantiate(binding_body(e), local); type = instantiate(binding_body(type), local); } - formatter fmt = p.ios().get_formatter(); - options opts = p.ios().get_options(); - unsigned indent = get_pp_indent(opts); - format r = group(format{fmt(p.env(), e, opts), space(), colon(), nest(indent, compose(line(), fmt(p.env(), type, opts)))}); - p.regular_stream() << mk_pair(r, opts) << endl; + auto reg = p.regular_stream(); + formatter const & fmt = reg.get_formatter(); + options opts = p.ios().get_options(); + unsigned indent = get_pp_indent(opts); + format r = group(format{fmt(e), space(), colon(), nest(indent, compose(line(), fmt(type)))}); + reg << mk_pair(r, opts) << endl; return p.env(); } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 0063ae313..95c37c11f 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -592,9 +592,7 @@ public: f_type = infer_type(f); lean_assert(is_pi(f_type)); } else { - environment env = m_env; - throw_kernel_exception(env, f, - [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, env, o, f); }); + throw_kernel_exception(m_env, f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); }); } } lean_assert(is_pi(f_type)); @@ -644,7 +642,7 @@ public: expr mk_delayed_coercion(expr const & e, expr const & d_type, expr const & a_type) { expr a = app_arg(e); expr m = mk_meta(some_expr(d_type), a.get_tag()); - justification j = mk_app_justification(m_env, e, d_type, a_type); + justification j = mk_app_justification(e, d_type, a_type); add_cnstr(mk_delayed_coercion_cnstr(m, a, a_type, j, to_delay_factor(cnstr_group::Basic))); return update_app(e, app_fn(e), m); } @@ -674,7 +672,7 @@ public: } else if (is_meta(a_type) && has_coercions_to(d_type)) { return mk_delayed_coercion(r, d_type, a_type); } else { - app_delayed_justification j(m_env, r, f_type, a_type); + app_delayed_justification j(r, f_type, a_type); if (!m_tc->is_def_eq(a_type, d_type, j)) { expr new_a = apply_coercion(a, a_type, d_type); bool coercion_worked = false; @@ -689,11 +687,7 @@ public: // rely on unification hints to solve this constraint add_cnstr(mk_eq_cnstr(a_type, d_type, j.get())); } else { - environment env = m_env; - throw_kernel_exception(m_env, a, - [=](formatter const & fmt, options const & o) { - return pp_app_type_mismatch(fmt, env, o, e, d_type, a_type); - }); + throw_kernel_exception(m_env, a, [=](formatter const & fmt) { return pp_app_type_mismatch(fmt, e, d_type, a_type); }); } } } @@ -778,9 +772,7 @@ public: optional c = get_coercion_to_sort(m_env, t); if (c) return mk_app(*c, e, e.get_tag()); - environment env = m_env; - throw_kernel_exception(env, e, - [=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, env, o, e); }); + throw_kernel_exception(m_env, e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); }); } expr visit_pi(expr const & e) { @@ -874,15 +866,11 @@ public: }); } - format pp_indent_expr(expr const & e) { - return ::lean::pp_indent_expr(m_ios.get_formatter(), m_env, m_ios.get_options(), e); - } - void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg) { lean_assert(is_metavar(mvar)); if (!m_displayed_errors.contains(mlocal_name(mvar))) { m_displayed_errors.insert(mlocal_name(mvar)); - regular out(m_env, m_ios); + auto out = regular(m_env, m_ios); display_error_pos(out, m_pos_provider, mvar); out << " unsolved placeholder, " << msg << "\n" << ps << "\n"; } @@ -918,10 +906,11 @@ public: try { return optional(expr_to_tactic(m_env, pre_tac, m_pos_provider)); } catch (expr_to_tactic_exception & ex) { - regular out(m_env, m_ios); + auto out = regular(m_env, m_ios); display_error_pos(out, m_pos_provider, mvar); out << " " << ex.what(); - out << pp_indent_expr(pre_tac) << endl << "failed at:" << pp_indent_expr(ex.get_expr()) << endl; + out << pp_indent_expr(out.get_formatter(), pre_tac) << endl << "failed at:" + << pp_indent_expr(out.get_formatter(), ex.get_expr()) << endl; return optional(); } } @@ -963,7 +952,7 @@ public: } } catch (tactic_exception & ex) { if (report_failure) { - regular out(m_env, m_ios); + auto out = regular(m_env, m_ios); display_error_pos(out, m_pos_provider, ex.get_expr()); out << " tactic failed: " << ex.what() << "\n"; } @@ -1066,12 +1055,11 @@ public: return apply(s, r); } - static format pp_type_mismatch(formatter const & fmt, environment const & env, options const & opts, - expr const & expected_type, expr const & given_type) { + static format pp_type_mismatch(formatter const & fmt, expr const & expected_type, expr const & given_type) { format r("type mismatch, expected type"); - r += ::lean::pp_indent_expr(fmt, env, opts, expected_type); + r += ::lean::pp_indent_expr(fmt, expected_type); r += compose(line(), format("given type:")); - r += ::lean::pp_indent_expr(fmt, env, opts, given_type); + r += ::lean::pp_indent_expr(fmt, given_type); return r; } @@ -1079,15 +1067,11 @@ public: expr r_t = ensure_type(visit(t)); expr r_v = visit(v); expr r_v_type = infer_type(r_v); - environment env = m_env; - justification j = mk_justification(v, [=](formatter const & fmt, options const & o, substitution const & subst) { - return pp_def_type_mismatch(fmt, env, o, n, subst.instantiate(r_t), subst.instantiate(r_v_type)); + justification j = mk_justification(v, [=](formatter const & fmt, substitution const & subst) { + return pp_def_type_mismatch(fmt, n, subst.instantiate(r_t), subst.instantiate(r_v_type)); }); if (!m_tc->is_def_eq(r_v_type, r_t, j)) { - throw_kernel_exception(env, v, - [=](formatter const & fmt, options const & o) { - return pp_def_type_mismatch(fmt, env, o, n, r_t, r_v_type); - }); + throw_kernel_exception(m_env, v, [=](formatter const & fmt) { return pp_def_type_mismatch(fmt, n, r_t, r_v_type); }); } auto p = solve().pull(); lean_assert(p); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 89649a764..16844eab8 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -193,8 +193,8 @@ public: token_info const & get_token_info() const { return m_scanner.get_token_info(); } std::string const & get_stream_name() const { return m_scanner.get_stream_name(); } - regular regular_stream() const { return regular(env(), ios()); } - diagnostic diagnostic_stream() const { return diagnostic(env(), ios()); } + io_state_stream regular_stream() const { return regular(env(), ios()); } + io_state_stream diagnostic_stream() const { return diagnostic(env(), ios()); } unsigned get_small_nat(); unsigned parse_small_nat(); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 73b28fa99..c84487a1c 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -366,15 +366,11 @@ format pretty_fn::operator()(expr const & e) { return pp_child(purify(e), 0).first; } -class pretty_formatter_cell : public formatter_cell { -public: - /** \brief Format the given expression. */ - virtual format operator()(environment const & env, expr const & e, options const & o) const { - return pretty_fn(env, o)(e); - } -}; - -formatter mk_pretty_formatter() { - return mk_formatter(pretty_formatter_cell()); +formatter_factory mk_pretty_formatter_factory() { + return [](environment const & env, options const & o) { // NOLINT + return formatter(o, [=](expr const & e) { + return pretty_fn(env, o)(e); + }); + }; } } diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index 3f8834502..f7fb341f4 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -74,5 +74,5 @@ public: format operator()(expr const & e); }; -formatter mk_pretty_formatter(); +formatter_factory mk_pretty_formatter_factory(); } diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp index 638594b3b..10863f6b8 100644 --- a/src/kernel/error_msgs.cpp +++ b/src/kernel/error_msgs.cpp @@ -7,43 +7,40 @@ Author: Leonardo de Moura #include "kernel/error_msgs.h" namespace lean { -format pp_indent_expr(formatter const & fmt, environment const & env, options const & opts, expr const & e) { - return nest(get_pp_indent(opts), compose(line(), fmt(env, e, opts))); +format pp_indent_expr(formatter const & fmt, expr const & e) { + return nest(get_pp_indent(fmt.get_options()), compose(line(), fmt(e))); } -format pp_type_expected(formatter const & fmt, environment const & env, options const & opts, expr const & e) { - return compose(format("type expected at"), pp_indent_expr(fmt, env, opts, e)); +format pp_type_expected(formatter const & fmt, expr const & e) { + return compose(format("type expected at"), pp_indent_expr(fmt, e)); } -format pp_function_expected(formatter const & fmt, environment const & env, options const & opts, expr const & e) { - return compose(format("function expected at"), pp_indent_expr(fmt, env, opts, e)); +format pp_function_expected(formatter const & fmt, expr const & e) { + return compose(format("function expected at"), pp_indent_expr(fmt, e)); } -format pp_app_type_mismatch(formatter const & fmt, environment const & env, options const & opts, expr const & app, - expr const & expected_type, expr const & given_type) { +format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const & expected_type, expr const & given_type) { format r; r += format("type mismatch at application"); - r += pp_indent_expr(fmt, env, opts, app); + r += pp_indent_expr(fmt, app); r += compose(line(), format("expected type:")); - r += pp_indent_expr(fmt, env, opts, expected_type); + r += pp_indent_expr(fmt, expected_type); r += compose(line(), format("given type:")); - r += pp_indent_expr(fmt, env, opts, given_type); + r += pp_indent_expr(fmt, given_type); return r; } -format pp_def_type_mismatch(formatter const & fmt, environment const & env, options const & opts, name const & n, - expr const & expected_type, expr const & given_type) { +format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const & expected_type, expr const & given_type) { format r("type mismatch at definition '"); r += format(n); r += format("', expected type"); - r += pp_indent_expr(fmt, env, opts, expected_type); + r += pp_indent_expr(fmt, expected_type); r += compose(line(), format("given type:")); - r += pp_indent_expr(fmt, env, opts, given_type); + r += pp_indent_expr(fmt, given_type); return r; } -format pp_decl_has_metavars(formatter const & fmt, environment const & env, options const & opts, name const & n, - expr const & e, bool is_type) { +format pp_decl_has_metavars(formatter const & fmt, name const & n, expr const & e, bool is_type) { format r("failed to add declaration '"); r += format(n); r += format("' to environment, "); @@ -52,7 +49,7 @@ format pp_decl_has_metavars(formatter const & fmt, environment const & env, opti else r += format("value"); r += format(" has metavariables"); - r += pp_indent_expr(fmt, env, opts, e); + r += pp_indent_expr(fmt, e); return r; } } diff --git a/src/kernel/error_msgs.h b/src/kernel/error_msgs.h index f0672e41b..8d6cf15a0 100644 --- a/src/kernel/error_msgs.h +++ b/src/kernel/error_msgs.h @@ -8,13 +8,10 @@ Author: Leonardo de Moura #include "kernel/expr.h" #include "kernel/formatter.h" namespace lean { -format pp_indent_expr(formatter const & fmt, environment const & env, options const & opts, expr const & e); -format pp_type_expected(formatter const & fmt, environment const & env, options const & opts, expr const & e); -format pp_function_expected(formatter const & fmt, environment const & env, options const & opts, expr const & e); -format pp_app_type_mismatch(formatter const & fmt, environment const & env, options const & opts, expr const & app, - expr const & expected_type, expr const & given_type); -format pp_def_type_mismatch(formatter const & fmt, environment const & env, options const & opts, name const & n, - expr const & expected_type, expr const & given_type); -format pp_decl_has_metavars(formatter const & fmt, environment const & env, options const & opts, name const & n, - expr const & e, bool is_type); +format pp_indent_expr(formatter const & fmt, expr const & e); +format pp_type_expected(formatter const & fmt, expr const & e); +format pp_function_expected(formatter const & fmt, expr const & e); +format pp_app_type_mismatch(formatter const & fmt, expr const & app, expr const & expected_type, expr const & given_type); +format pp_def_type_mismatch(formatter const & fmt, name const & n, expr const & expected_type, expr const & given_type); +format pp_decl_has_metavars(formatter const & fmt, name const & n, expr const & e, bool is_type); } diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 833a6a587..7ea1747fd 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -193,7 +193,7 @@ bool macro_definition_cell::lt(macro_definition_cell const &) const { return fal bool macro_definition_cell::operator==(macro_definition_cell const & other) const { return typeid(*this) == typeid(other); } unsigned macro_definition_cell::trust_level() const { return 0; } -format macro_definition_cell::pp(formatter const &, options const &) const { return format(get_name()); } +format macro_definition_cell::pp(formatter const &) const { return format(get_name()); } void macro_definition_cell::display(std::ostream & out) const { out << get_name(); } bool macro_definition_cell::is_atomic_pp(bool, bool) const { return true; } unsigned macro_definition_cell::hash() const { return get_name().hash(); } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 11baadb16..0a0581945 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -23,6 +23,7 @@ Author: Leonardo de Moura #include "util/sexpr/format.h" #include "util/name_generator.h" #include "kernel/level.h" +#include "kernel/formatter.h" #include "kernel/extension_context.h" namespace lean { @@ -309,8 +310,6 @@ public: level const & get_level() const { return m_level; } }; -class formatter; - /** \brief Abstract class for macro_definitions */ class macro_definition_cell { protected: @@ -332,7 +331,7 @@ public: virtual unsigned trust_level() const; virtual bool operator==(macro_definition_cell const & other) const; virtual void display(std::ostream & out) const; - virtual format pp(formatter const & fmt, options const & opts) const; + virtual format pp(formatter const & fmt) const; virtual bool is_atomic_pp(bool unicode, bool coercion) const; virtual unsigned hash() const; virtual void write(serializer & s) const = 0; @@ -361,7 +360,7 @@ public: bool operator!=(macro_definition const & other) const { return !operator==(other); } bool operator<(macro_definition const & other) const; void display(std::ostream & out) const { return m_ptr->display(out); } - format pp(formatter const & fmt, options const & opts) const { return m_ptr->pp(fmt, opts); } + format pp(formatter const & fmt) const { return m_ptr->pp(fmt); } bool is_atomic_pp(bool unicode, bool coercion) const { return m_ptr->is_atomic_pp(unicode, coercion); } unsigned hash() const { return m_ptr->hash(); } void write(serializer & s) const { return m_ptr->write(s); } diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index e4a0fae9d..dce6a7f13 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -243,17 +243,16 @@ std::ostream & operator<<(std::ostream & out, expr const & e) { return out; } -class simple_formatter_cell : public formatter_cell { -public: - virtual format operator()(environment const & env, expr const & e, options const &) const { - std::ostringstream s; - print_expr_fn pr(s, env.prop_proof_irrel()); - pr(e); - return format(s.str()); - } -}; -formatter mk_simple_formatter() { - return mk_formatter(simple_formatter_cell()); +formatter_factory mk_simple_formatter_factory() { + return [](environment const & env, options const & o) { // NOLINT + return formatter(o, [=](expr const & e) { + std::ostringstream s; + print_expr_fn pr(s, env.prop_proof_irrel()); + pr(e); + return format(s.str()); + }); + }; } + void print(lean::expr const & a) { std::cout << a << std::endl; } } diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h index e4b209ce1..e9279b71b 100644 --- a/src/kernel/formatter.h +++ b/src/kernel/formatter.h @@ -8,9 +8,11 @@ Author: Leonardo de Moura #include #include #include "util/sexpr/options.h" -#include "kernel/expr.h" namespace lean { +class expr; +class environment; + /** \brief Return true iff \c t contains a constant named \c n or a local constant with named (pp or not) \c n */ bool is_used_name(expr const & t, name const & n); /** @@ -25,35 +27,20 @@ std::pair binding_body_fresh(expr const & b, bool preserve_type = fa /** \brief Return the body of the let-expression \c l, where variable #0 is replaced by a local constant with a "fresh" name. */ std::pair let_body_fresh(expr const & l, bool preserve_type = false); -/** - \brief API for formatting expressions -*/ -class formatter_cell { -public: - virtual ~formatter_cell() {} - /** \brief Format the given expression. */ - virtual format operator()(environment const & env, expr const & e, options const & opts) const = 0; -}; -/** - \brief Smart-pointer for the actual formatter object (aka \c formatter_cell). -*/ class formatter { - std::shared_ptr m_cell; - formatter(formatter_cell * c):m_cell(c) {} + std::function m_fn; + options m_options; public: - format operator()(environment const & env, expr const & e, options const & opts = options()) const { return (*m_cell)(env, e, opts); } - template friend formatter mk_formatter(FCell && fcell); + formatter(options const & o, std::function const & fn):m_fn(fn), m_options(o) {} + format operator()(expr const & e) const { return m_fn(e); } + options const & get_options() const { return m_options; } }; -template formatter mk_formatter(FCell && fcell) { - return formatter(new FCell(std::forward(fcell))); -} +typedef std::function formatter_factory; std::ostream & operator<<(std::ostream & out, expr const & e); -/** - \brief Create a simple formatter object based on operator<< -*/ -formatter mk_simple_formatter(); +/** \brief Create a simple formatter object based on operator */ +formatter_factory mk_simple_formatter_factory(); -typedef std::function pp_fn; +typedef std::function pp_fn; } diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp index 29cafa590..bd9337a14 100644 --- a/src/kernel/justification.cpp +++ b/src/kernel/justification.cpp @@ -194,18 +194,18 @@ optional justification::get_main_expr() const { } } } -format justification::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & s) const { +format justification::pp(formatter const & fmt, pos_info_provider const * p, substitution const & s) const { justification_cell * it = m_ptr; while (true) { if (!it) return format(); switch (it->m_kind) { case justification_kind::Asserted: - return to_asserted(it)->m_fn(fmt, opts, p, s); + return to_asserted(it)->m_fn(fmt, p, s); case justification_kind::ExtAssumption: - return to_ext_assumption(it)->m_fn(fmt, opts, p, s); + return to_ext_assumption(it)->m_fn(fmt, p, s); case justification_kind::ExtComposite: - return to_ext_composite(it)->m_fn(fmt, opts, p, s); + return to_ext_composite(it)->m_fn(fmt, p, s); case justification_kind::Assumption: return format(format("Assumption "), format(to_assumption(it)->m_idx)); case justification_kind::Composite: @@ -239,12 +239,12 @@ justification mk_justification(optional const & s, pp_jst_fn const & fn) { return justification(new asserted_cell(fn, s)); } justification mk_justification(optional const & s, pp_jst_sfn const & fn) { - return mk_justification(s, [=](formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & subst) { - return compose(to_pos(s, p), fn(fmt, opts, subst)); }); + return mk_justification(s, [=](formatter const & fmt, pos_info_provider const * p, substitution const & subst) { + return compose(to_pos(s, p), fn(fmt, subst)); }); } justification mk_justification(char const * msg, optional const & s) { std::string _msg(msg); - return mk_justification(s, [=](formatter const &, options const &, pos_info_provider const *, substitution const &) { + return mk_justification(s, [=](formatter const &, pos_info_provider const *, substitution const &) { return format(_msg); }); } diff --git a/src/kernel/justification.h b/src/kernel/justification.h index f076ea21c..ff2e553c7 100644 --- a/src/kernel/justification.h +++ b/src/kernel/justification.h @@ -23,7 +23,7 @@ struct justification_cell; The pp_jst_fn is a generic funciton that produces these messages. We can associate these functions to justification objects. */ -typedef std::function pp_jst_fn; +typedef std::function pp_jst_fn; /** \brief Objects used to justify unification (and level) constraints and metavariable assignments. @@ -61,7 +61,7 @@ public: \brief Convert this justification into a format object. This method is usually used to report "error" messages to users. */ - format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & s) const; + format pp(formatter const & fmt, pos_info_provider const * p, substitution const & s) const; /** \brief Return an expression associated with the justification object. */ @@ -79,7 +79,7 @@ public: /** \brief Simpler version of pp_jst_fn */ -typedef std::function pp_jst_sfn; +typedef std::function pp_jst_sfn; /** \brief Return a format object containing position information for the given expression (if available) */ format to_pos(optional const & e, pos_info_provider const * p); diff --git a/src/kernel/kernel_exception.cpp b/src/kernel/kernel_exception.cpp index dd75961aa..8c4b69bfb 100644 --- a/src/kernel/kernel_exception.cpp +++ b/src/kernel/kernel_exception.cpp @@ -10,7 +10,7 @@ Author: Leonardo de Moura #include "kernel/kernel_exception.h" namespace lean { -format kernel_exception::pp(formatter const &, options const &) const { return format(what()); } +format kernel_exception::pp(formatter const &) const { return format(what()); } class generic_kernel_exception : public kernel_exception { protected: @@ -23,14 +23,14 @@ public: m_pp_fn(fn) {} virtual ~generic_kernel_exception() noexcept {} virtual optional get_main_expr() const { return m_main_expr; } - virtual format pp(formatter const & fmt, options const & opts) const { return m_pp_fn(fmt, opts); } + virtual format pp(formatter const & fmt) const { return m_pp_fn(fmt); } virtual exception * clone() const { return new generic_kernel_exception(m_env, m_msg.c_str(), m_main_expr, m_pp_fn); } virtual void rethrow() const { throw *this; } }; [[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional const & m) { std::string msg_str = msg; - throw generic_kernel_exception(env, msg, m, [=](formatter const &, options const &) { return format(msg_str); }); + throw generic_kernel_exception(env, msg, m, [=](formatter const &) { return format(msg_str); }); } [[ noreturn ]] void throw_kernel_exception(environment const & env, sstream const & strm, optional const & m) { diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 9b603db4c..edfed46c1 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -28,7 +28,7 @@ public: This information is used to provide better error messages. */ virtual optional get_main_expr() const { return none_expr(); } - virtual format pp(formatter const & fmt, options const & opts) const; + virtual format pp(formatter const & fmt) const; virtual exception * clone() const { return new kernel_exception(m_env, m_msg.c_str()); } virtual void rethrow() const { throw *this; } }; diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 12a959c55..8b0db49e2 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -133,17 +133,13 @@ expr type_checker::ensure_sort_core(expr e, expr const & s) { } else if (is_meta(e)) { expr r = mk_sort(mk_meta_univ(m_gen.next())); justification j = mk_justification(s, - [=](formatter const & fmt, options const & o, substitution const & subst) { - return pp_type_expected(fmt, m_env, o, subst.instantiate(s)); + [=](formatter const & fmt, substitution const & subst) { + return pp_type_expected(fmt, subst.instantiate(s)); }); add_cnstr(mk_eq_cnstr(e, r, j)); return r; } else { - // We don't want m_env (i.e., this->m_env) inside the following closure, - // because the type checker may be gone, when the closure is executed. - environment env = m_env; - throw_kernel_exception(env, s, - [=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, env, o, s); }); + throw_kernel_exception(m_env, s, [=](formatter const & fmt) { return pp_type_expected(fmt, s); }); } } @@ -156,26 +152,22 @@ expr type_checker::ensure_pi_core(expr e, expr const & s) { return e; } else if (is_meta(e)) { expr r = mk_pi_for(m_gen, e); - justification j = mk_justification(s, - [=](formatter const & fmt, options const & o, substitution const & subst) { - return pp_function_expected(fmt, m_env, o, subst.instantiate(s)); - }); + justification j = mk_justification(s, [=](formatter const & fmt, substitution const & subst) { + return pp_function_expected(fmt, subst.instantiate(s)); + }); add_cnstr(mk_eq_cnstr(e, r, j)); return r; } else { - environment env = m_env; - throw_kernel_exception(env, s, - [=](formatter const & fmt, options const & o) { return pp_function_expected(fmt, env, o, s); }); + throw_kernel_exception(m_env, s, [=](formatter const & fmt) { return pp_function_expected(fmt, s); }); } } static constexpr char const * g_macro_error_msg = "failed to type check macro expansion"; justification type_checker::mk_macro_jst(expr const & e) { - return mk_justification(e, - [=](formatter const &, options const &, substitution const &) { - return format(g_macro_error_msg); - }); + return mk_justification(e, [=](formatter const &, substitution const &) { + return format(g_macro_error_msg); + }); } void type_checker::check_level(level const & l, expr const & s) { @@ -185,12 +177,12 @@ void type_checker::check_level(level const & l, expr const & s) { throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '" << *n2 << "'", s); } -app_delayed_justification::app_delayed_justification(environment const & env, expr const & e, expr const & f_type, expr const & a_type): - m_env(env), m_e(e), m_fn_type(f_type), m_arg_type(a_type) {} +app_delayed_justification::app_delayed_justification(expr const & e, expr const & f_type, expr const & a_type): + m_e(e), m_fn_type(f_type), m_arg_type(a_type) {} -justification mk_app_justification(environment const & env, expr const & e, expr const & d_type, expr const & a_type) { - auto pp_fn = [=](formatter const & fmt, options const & o, substitution const & subst) { - return pp_app_type_mismatch(fmt, env, o, subst.instantiate(e), subst.instantiate(d_type), subst.instantiate(a_type)); +justification mk_app_justification(expr const & e, expr const & d_type, expr const & a_type) { + auto pp_fn = [=](formatter const & fmt, substitution const & subst) { + return pp_app_type_mismatch(fmt, subst.instantiate(e), subst.instantiate(d_type), subst.instantiate(a_type)); }; return mk_justification(e, pp_fn); } @@ -199,7 +191,7 @@ justification app_delayed_justification::get() { if (!m_jst) { // We should not have a reference to this object inside the closure. // So, we create the following locals that will be captured by the closure instead of 'this'. - m_jst = mk_app_justification(m_env, m_e, binding_domain(m_fn_type), m_arg_type); + m_jst = mk_app_justification(m_e, binding_domain(m_fn_type), m_arg_type); } return *m_jst; } @@ -287,12 +279,11 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) { expr f_type = ensure_pi_core(infer_type_core(app_fn(e), infer_only), app_fn(e)); if (!infer_only) { expr a_type = infer_type_core(app_arg(e), infer_only); - app_delayed_justification jst(m_env, e, f_type, a_type); + app_delayed_justification jst(e, f_type, a_type); if (!is_def_eq(a_type, binding_domain(f_type), jst)) { - environment env = m_env; throw_kernel_exception(m_env, app_arg(e), - [=](formatter const & fmt, options const & o) { - return pp_app_type_mismatch(fmt, env, o, e, binding_domain(f_type), a_type); + [=](formatter const & fmt) { + return pp_app_type_mismatch(fmt, e, binding_domain(f_type), a_type); }); } } @@ -407,10 +398,7 @@ type_checker::~type_checker() {} static void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) { if (has_metavar(e)) - throw_kernel_exception(env, e, - [=](formatter const & fmt, options const & o) { - return pp_decl_has_metavars(fmt, env, o, n, e, is_type); - }); + throw_kernel_exception(env, e, [=](formatter const & fmt) { return pp_decl_has_metavars(fmt, n, e, is_type); }); } static void check_no_local(environment const & env, expr const & e) { @@ -456,10 +444,9 @@ certified_declaration check(environment const & env, declaration const & d, name type_checker checker2(env, g, mk_default_converter(env, midx, memoize, extra_opaque)); expr val_type = checker2.check(d.get_value(), d.get_univ_params()); if (!checker2.is_def_eq(val_type, d.get_type())) { - throw_kernel_exception(env, d.get_value(), - [=](formatter const & fmt, options const & o) { - return pp_def_type_mismatch(fmt, env, o, d.get_name(), d.get_type(), val_type); - }); + throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt) { + return pp_def_type_mismatch(fmt, d.get_name(), d.get_type(), val_type); + }); } } return certified_declaration(env.get_id(), d); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 31ef7dd95..cd555cdc4 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -189,20 +189,19 @@ certified_declaration check(environment const & env, declaration const & d, name \brief Create a justification for an application \c e where the expected type must be \c d_type and the argument type is \c a_type. */ -justification mk_app_justification(environment const & env, expr const & e, expr const & d_type, expr const & a_type); +justification mk_app_justification(expr const & e, expr const & d_type, expr const & a_type); /** \brief Create a justification for a application type mismatch, \c e is the application, \c fn_type and \c arg_type are the function and argument type. */ class app_delayed_justification : public delayed_justification { - environment const & m_env; expr const & m_e; expr const & m_fn_type; expr const & m_arg_type; optional m_jst; public: - app_delayed_justification(environment const & env, expr const & e, expr const & f_type, expr const & a_type); + app_delayed_justification(expr const & e, expr const & f_type, expr const & a_type); virtual justification get(); }; } diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp index f0587f820..df19257b0 100644 --- a/src/library/error_handling/error_handling.cpp +++ b/src/library/error_handling/error_handling.cpp @@ -54,7 +54,7 @@ static void display_error(io_state_stream const & ios, pos_info_provider const * options opts = ios.get_options(); auto j = ex.get_justification(); display_error_pos(ios, p, j.get_main_expr()); - ios << " " << mk_pair(j.pp(fmt, opts, p, ex.get_substitution()), opts) << endl; + ios << " " << mk_pair(j.pp(fmt, p, ex.get_substitution()), opts) << endl; } // struct delta_pos_info_provider : public pos_info_provider { diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp index bc0066e1a..ce637ed4e 100644 --- a/src/library/io_state.cpp +++ b/src/library/io_state.cpp @@ -8,26 +8,26 @@ Author: Leonardo de Moura #include "library/io_state.h" namespace lean { -static io_state g_dummy_ios(mk_simple_formatter()); +static io_state g_dummy_ios(mk_simple_formatter_factory()); io_state const & get_dummy_ios() { return g_dummy_ios; } -io_state::io_state(formatter const & fmt): - m_formatter(fmt), +io_state::io_state(formatter_factory const & fmtf): + m_formatter_factory(fmtf), m_regular_channel(std::make_shared()), m_diagnostic_channel(std::make_shared()) { } -io_state::io_state(options const & opts, formatter const & fmt): +io_state::io_state(options const & opts, formatter_factory const & fmtf): m_options(opts), - m_formatter(fmt), + m_formatter_factory(fmtf), m_regular_channel(std::make_shared()), m_diagnostic_channel(std::make_shared()) { } io_state::io_state(io_state const & ios, std::shared_ptr const & r, std::shared_ptr const d): m_options(ios.m_options), - m_formatter(ios.m_formatter), + m_formatter_factory(ios.m_formatter_factory), m_regular_channel(r), m_diagnostic_channel(d) { } @@ -48,7 +48,7 @@ void io_state::set_options(options const & opts) { m_options = opts; } -void io_state::set_formatter(formatter const & f) { - m_formatter = f; +void io_state::set_formatter_factory(formatter_factory const & f) { + m_formatter_factory = f; } } diff --git a/src/library/io_state.h b/src/library/io_state.h index 93e5d70cf..c9f42149a 100644 --- a/src/library/io_state.h +++ b/src/library/io_state.h @@ -7,7 +7,7 @@ Author: Leonardo de Moura #pragma once #include "util/output_channel.h" #include "util/sexpr/options.h" -#include "kernel/formatter.h" +#include "kernel/expr.h" namespace lean { /** @@ -19,24 +19,24 @@ namespace lean { */ class io_state { options m_options; - formatter m_formatter; + formatter_factory m_formatter_factory; std::shared_ptr m_regular_channel; std::shared_ptr m_diagnostic_channel; public: - io_state(formatter const & fmt); - io_state(options const & opts, formatter const & fmt); + io_state(formatter_factory const & fmtf); + io_state(options const & opts, formatter_factory const & fmtf); io_state(io_state const & ios, std::shared_ptr const & r, std::shared_ptr const d); ~io_state(); options get_options() const { return m_options; } - formatter get_formatter() const { return m_formatter; } + formatter_factory const & get_formatter_factory() const { return m_formatter_factory; } output_channel & get_regular_channel() const { return *m_regular_channel; } output_channel & get_diagnostic_channel() const { return *m_diagnostic_channel; } void set_regular_channel(std::shared_ptr const & out); void set_diagnostic_channel(std::shared_ptr const & out); void set_options(options const & opts); - void set_formatter(formatter const & f); + void set_formatter_factory(formatter_factory const & f); template void set_option(name const & n, T const & v) { set_options(get_options().update(n, v)); } diff --git a/src/library/io_state_stream.cpp b/src/library/io_state_stream.cpp index 317c462d2..a9520047c 100644 --- a/src/library/io_state_stream.cpp +++ b/src/library/io_state_stream.cpp @@ -14,13 +14,13 @@ io_state_stream const & operator<<(io_state_stream const & out, endl_class) { io_state_stream const & operator<<(io_state_stream const & out, expr const & e) { options const & opts = out.get_options(); - out.get_stream() << mk_pair(out.get_formatter()(out.get_environment(), e, opts), opts); + out.get_stream() << mk_pair(out.get_formatter()(e), opts); return out; } io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex) { options const & opts = out.get_options(); - out.get_stream() << mk_pair(ex.pp(out.get_formatter(), opts), opts); + out.get_stream() << mk_pair(ex.pp(out.get_formatter()), opts); return out; } } diff --git a/src/library/io_state_stream.h b/src/library/io_state_stream.h index b09d32705..355056c1a 100644 --- a/src/library/io_state_stream.h +++ b/src/library/io_state_stream.h @@ -13,36 +13,22 @@ namespace lean { */ class io_state_stream { protected: - environment const & m_env; - io_state const & m_io_state; + environment const & m_env; + formatter m_formatter; + output_channel & m_stream; public: - io_state_stream(environment const & env, io_state const & s):m_env(env), m_io_state(s) {} - virtual std::ostream & get_stream() const = 0; + io_state_stream(environment const & env, io_state const & ios, bool regular = true): + m_env(env), m_formatter(ios.get_formatter_factory()(env, ios.get_options())), + m_stream(regular ? ios.get_regular_channel() : ios.get_diagnostic_channel()) {} + std::ostream & get_stream() const { return m_stream.get_stream(); } void flush() { get_stream().flush(); } - formatter get_formatter() const { return m_io_state.get_formatter(); } - options get_options() const { return m_io_state.get_options(); } + formatter const & get_formatter() const { return m_formatter; } + options get_options() const { return m_formatter.get_options(); } environment const & get_environment() const { return m_env; } }; -/** - \brief Wrapper for the io_state object that provides access to the - io_state's regular channel -*/ -class regular : public io_state_stream { -public: - regular(environment const & env, io_state const & s):io_state_stream(env, s) {} - std::ostream & get_stream() const { return m_io_state.get_regular_channel().get_stream(); } -}; - -/** - \brief Wrapper for the io_state object that provides access to the - io_state's diagnostic channel -*/ -class diagnostic : public io_state_stream { -public: - diagnostic(environment const & env, io_state const & s):io_state_stream(env, s) {} - std::ostream & get_stream() const { return m_io_state.get_diagnostic_channel().get_stream(); } -}; +inline io_state_stream regular(environment const & env, io_state const & ios) { return io_state_stream(env, ios, true); } +inline io_state_stream diagnostic(environment const & env, io_state const & ios) { return io_state_stream(env, ios, false); } // hack for using std::endl with channels struct endl_class { endl_class() {} }; diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 33385c0b6..cc7977b78 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -331,10 +331,9 @@ expr & to_macro_app(lua_State * L, int idx) { static int expr_tostring(lua_State * L) { std::ostringstream out; - formatter fmt = get_global_formatter(L); - options opts = get_global_options(L); - environment env = get_global_environment(L); - out << mk_pair(fmt(env, to_expr(L, 1), opts), opts); + formatter fmt = mk_formatter(L); + options opts = get_global_options(L); + out << mk_pair(fmt(to_expr(L, 1)), opts); return push_string(L, out.str().c_str()); } @@ -712,9 +711,9 @@ static int macro_eq(lua_State * L) { return push_boolean(L, to_macro_definition( static int macro_hash(lua_State * L) { return push_integer(L, to_macro_definition(L, 1).hash()); } static int macro_tostring(lua_State * L) { std::ostringstream out; - formatter fmt = get_global_formatter(L); + formatter fmt = mk_formatter(L); options opts = get_global_options(L); - out << mk_pair(to_macro_definition(L, 1).pp(fmt, opts), opts); + out << mk_pair(to_macro_definition(L, 1).pp(fmt), opts); return push_string(L, out.str().c_str()); } @@ -845,80 +844,92 @@ static void open_declaration(lua_State * L) { } // Formatter +DECL_UDATA(formatter_factory) DECL_UDATA(formatter) static int formatter_call(lua_State * L) { - int nargs = lua_gettop(L); formatter & fmt = to_formatter(L, 1); - if (nargs == 2) { - return push_format(L, fmt(get_global_environment(L), to_expr(L, 2), get_global_options(L))); - } else if (nargs == 3) { - if (is_expr(L, 2)) - return push_format(L, fmt(get_global_environment(L), to_expr(L, 2), to_options(L, 3))); - else - return push_format(L, fmt(to_environment(L, 2), to_expr(L, 3), get_global_options(L))); - } else { - return push_format(L, fmt(to_environment(L, 2), to_expr(L, 3), to_options(L, 4))); - } + return push_format(L, fmt(to_expr(L, 2))); } +static int formatter_factory_call(lua_State * L) { + int nargs = lua_gettop(L); + formatter_factory & fmtf = to_formatter_factory(L, 1); + if (nargs == 1) + return push_formatter(L, fmtf(get_global_environment(L), get_global_options(L))); + else if (nargs == 2) + return push_formatter(L, fmtf(to_environment(L, 2), get_global_options(L))); + else + return push_formatter(L, fmtf(to_environment(L, 2), to_options(L, 3))); +} + +static const struct luaL_Reg formatter_factory_m[] = { + {"__gc", formatter_factory_gc}, // never throws + {"__call", safe_function}, + {0, 0} +}; + static const struct luaL_Reg formatter_m[] = { {"__gc", formatter_gc}, // never throws {"__call", safe_function}, {0, 0} }; -static char g_formatter_key; -static formatter g_simple_formatter = mk_simple_formatter(); +static char g_formatter_factory_key; +static formatter_factory g_simple_formatter_factory = mk_simple_formatter_factory(); -optional get_global_formatter_core(lua_State * L) { +optional get_global_formatter_factory_core(lua_State * L) { io_state * io = get_io_state_ptr(L); if (io != nullptr) { - return optional(io->get_formatter()); + return optional(io->get_formatter_factory()); } else { - lua_pushlightuserdata(L, static_cast(&g_formatter_key)); + lua_pushlightuserdata(L, static_cast(&g_formatter_factory_key)); lua_gettable(L, LUA_REGISTRYINDEX); - if (is_formatter(L, -1)) { - formatter r = to_formatter(L, -1); + if (is_formatter_factory(L, -1)) { + formatter_factory r = to_formatter_factory(L, -1); lua_pop(L, 1); - return optional(r); + return optional(r); } else { lua_pop(L, 1); - return optional(); + return optional(); } } } -formatter get_global_formatter(lua_State * L) { - auto r = get_global_formatter_core(L); +formatter_factory get_global_formatter_factory(lua_State * L) { + auto r = get_global_formatter_factory_core(L); if (r) return *r; else - return g_simple_formatter; + return g_simple_formatter_factory; } -void set_global_formatter(lua_State * L, formatter const & fmt) { +void set_global_formatter_factory(lua_State * L, formatter_factory const & fmtf) { io_state * io = get_io_state_ptr(L); if (io != nullptr) { - io->set_formatter(fmt); + io->set_formatter_factory(fmtf); } else { - lua_pushlightuserdata(L, static_cast(&g_formatter_key)); - push_formatter(L, fmt); + lua_pushlightuserdata(L, static_cast(&g_formatter_factory_key)); + push_formatter_factory(L, fmtf); lua_settable(L, LUA_REGISTRYINDEX); } } -static int get_formatter(lua_State * L) { +static int get_formatter_factory(lua_State * L) { io_state * io = get_io_state_ptr(L); if (io != nullptr) { - return push_formatter(L, io->get_formatter()); + return push_formatter_factory(L, io->get_formatter_factory()); } else { - return push_formatter(L, get_global_formatter(L)); + return push_formatter_factory(L, get_global_formatter_factory(L)); } } -static int set_formatter(lua_State * L) { - set_global_formatter(L, to_formatter(L, 1)); +formatter mk_formatter(lua_State * L) { + return get_global_formatter_factory(L)(get_global_environment(L), get_global_options(L)); +} + +static int set_formatter_factory(lua_State * L) { + set_global_formatter_factory(L, to_formatter_factory(L, 1)); return 0; } @@ -928,9 +939,15 @@ static void open_formatter(lua_State * L) { lua_setfield(L, -2, "__index"); setfuncs(L, formatter_m, 0); + luaL_newmetatable(L, formatter_factory_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, formatter_factory_m, 0); + SET_GLOBAL_FUN(formatter_pred, "is_formatter"); - SET_GLOBAL_FUN(get_formatter, "get_formatter"); - SET_GLOBAL_FUN(set_formatter, "set_formatter"); + SET_GLOBAL_FUN(formatter_factory_pred, "is_formatter_factory"); + SET_GLOBAL_FUN(get_formatter_factory, "get_formatter_factory"); + SET_GLOBAL_FUN(set_formatter_factory, "set_formatter_factory"); } // Environment_id @@ -1190,15 +1207,15 @@ io_state to_io_state_ext(lua_State * L, int idx) { int mk_io_state(lua_State * L) { int nargs = lua_gettop(L); if (nargs == 0) - return push_io_state(L, io_state(mk_simple_formatter())); + return push_io_state(L, io_state(mk_simple_formatter_factory())); else if (nargs == 1) return push_io_state(L, io_state(to_io_state(L, 1))); else - return push_io_state(L, io_state(to_options(L, 1), to_formatter(L, 2))); + return push_io_state(L, io_state(to_options(L, 1), to_formatter_factory(L, 2))); } static int io_state_get_options(lua_State * L) { return push_options(L, to_io_state(L, 1).get_options()); } -static int io_state_get_formatter(lua_State * L) { return push_formatter(L, to_io_state(L, 1).get_formatter()); } +static int io_state_get_formatter_factory(lua_State * L) { return push_formatter_factory(L, to_io_state(L, 1).get_formatter_factory()); } static int io_state_set_options(lua_State * L) { to_io_state(L, 1).set_options(to_options(L, 2)); return 0; } static mutex g_print_mutex; @@ -1250,14 +1267,14 @@ static int io_state_print_regular(lua_State * L) { return print(L, to_io_state(L static int io_state_print_diagnostic(lua_State * L) { return print(L, to_io_state(L, 1), 2, false); } static const struct luaL_Reg io_state_m[] = { - {"__gc", io_state_gc}, // never throws - {"get_options", safe_function}, - {"set_options", safe_function}, - {"get_formatter", safe_function}, - {"print_diagnostic", safe_function}, - {"print_regular", safe_function}, - {"print", safe_function}, - {"diagnostic", safe_function}, + {"__gc", io_state_gc}, // never throws + {"get_options", safe_function}, + {"set_options", safe_function}, + {"get_formatter_factory", safe_function}, + {"print_diagnostic", safe_function}, + {"print_regular", safe_function}, + {"print", safe_function}, + {"diagnostic", safe_function}, {0, 0} }; @@ -1319,7 +1336,7 @@ io_state * get_io_state_ptr(lua_State * L) { } io_state get_tmp_io_state(lua_State * L) { - return io_state(get_global_options(L), get_global_formatter(L)); + return io_state(get_global_options(L), get_global_formatter_factory(L)); } // Justification @@ -1345,17 +1362,13 @@ static int justification_pp(lua_State * L) { int nargs = lua_gettop(L); justification & j = to_justification(L, 1); if (nargs == 1) - return push_format(L, j.pp(get_global_formatter(L), get_global_options(L), nullptr, substitution())); + return push_format(L, j.pp(mk_formatter(L), nullptr, substitution())); else if (nargs == 2 && is_substitution(L, 2)) - return push_format(L, j.pp(get_global_formatter(L), get_global_options(L), nullptr, to_substitution(L, 2))); + return push_format(L, j.pp(mk_formatter(L), nullptr, to_substitution(L, 2))); else if (nargs == 2) - return push_format(L, j.pp(to_formatter(L, 2), get_global_options(L), nullptr, substitution())); - else if (nargs == 3 && is_substitution(L, 3)) - return push_format(L, j.pp(to_formatter(L, 2), get_global_options(L), nullptr, to_substitution(L, 3))); - else if (nargs == 3) - return push_format(L, j.pp(to_formatter(L, 2), to_options(L, 3), nullptr, substitution())); + return push_format(L, j.pp(to_formatter(L, 2), nullptr, substitution())); else - return push_format(L, j.pp(to_formatter(L, 2), to_options(L, 3), nullptr, to_substitution(L, 4))); + return push_format(L, j.pp(to_formatter(L, 2), nullptr, to_substitution(L, 3))); } static int justification_assumption_idx(lua_State * L) { if (!to_justification(L, 1).is_assumption()) @@ -1381,18 +1394,18 @@ static int mk_justification(lua_State * L) { return push_justification(L, justification()); } else if (nargs == 1) { std::string s = lua_tostring(L, 1); - return push_justification(L, mk_justification(none_expr(), [=](formatter const &, options const &, substitution const &) { + return push_justification(L, mk_justification(none_expr(), [=](formatter const &, substitution const &) { return format(s.c_str()); })); } else { std::string s = lua_tostring(L, 1); environment env = to_environment(L, 2); expr e = to_expr(L, 3); - justification j = mk_justification(some_expr(e), [=](formatter const & fmt, options const & opts, substitution const & subst) { + justification j = mk_justification(some_expr(e), [=](formatter const & fmt, substitution const & subst) { expr new_e = subst.instantiate(e); format r; r += format(s.c_str()); - r += pp_indent_expr(fmt, env, opts, new_e); + r += pp_indent_expr(fmt, new_e); return r; }); return push_justification(L, j); diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h index a1d809b0a..39a7ed487 100644 --- a/src/library/kernel_bindings.h +++ b/src/library/kernel_bindings.h @@ -28,23 +28,26 @@ int push_optional_declaration(lua_State * L, optional const & e); int push_optional_constraint(lua_State * L, optional const & c); int push_list_expr(lua_State * L, list const & l); /** - \brief Return the formatter object associated with the given Lua State. + \brief Return the formatter factory object associated with the given Lua State. This procedure checks for options at: 1- Lean state object associated with \c L 2- Lua Registry associated with \c L */ -optional get_global_formatter_core(lua_State * L); +optional get_global_formatter_factory_core(lua_State * L); /** - \brief Similar to \c get_global_formatter_core, but returns + \brief Similar to \c get_global_formatter_factory_core, but returns the simple_formatter if a formatter can't be found. */ -formatter get_global_formatter(lua_State * L); +formatter_factory get_global_formatter_factory(lua_State * L); /** \brief Update the formatter object associated with the given Lua State. If \c L is associated with a Lean state object \c S, then we update the formatter of \c S. Otherwise, we update the registry of \c L. */ -void set_global_formatter(lua_State * L, formatter const & fmt); +void set_global_formatter_factory(lua_State * L, formatter_factory const & fmtf); + +/** \brief Make a fresh formatter object using the global formatter factory associated with L, and the global environment */ +formatter mk_formatter(lua_State * L); /** \brief Set the Lua registry of a Lua state with an environment object. */ void set_global_environment(lua_State * L, environment const & env); diff --git a/src/library/string.cpp b/src/library/string.cpp index 02335d169..f3b6ad21c 100644 --- a/src/library/string.cpp +++ b/src/library/string.cpp @@ -64,7 +64,7 @@ public: } out << "\""; } - virtual format pp(formatter const &, options const &) const { + virtual format pp(formatter const &) const { std::ostringstream out; display(out); return format(out.str()); diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 188fefcf3..99631e65f 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -50,7 +50,8 @@ static void update_local(expr * begin, expr * end, expr & conclusion, update_local(conclusion, old_local, new_local); } -format goal::pp(environment const & env, formatter const & fmt, options const & opts) const { +format goal::pp(formatter const & fmt) const { + options const & opts = fmt.get_options(); unsigned indent = get_pp_indent(opts); bool unicode = get_pp_unicode(opts); format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); @@ -66,10 +67,10 @@ format goal::pp(environment const & env, formatter const & fmt, options const & expr new_l = pick_unused_pp_name(tmp.begin(), it, l); if (!is_eqp(l, new_l)) update_local(it+1, end, conclusion, l, new_l); - r += format{format(local_pp_name(new_l)), space(), colon(), nest(indent, compose(line(), fmt(env, mlocal_type(new_l), opts)))}; + r += format{format(local_pp_name(new_l)), space(), colon(), nest(indent, compose(line(), fmt(mlocal_type(new_l))))}; } r = group(r); - r += format{line(), turnstile, space(), nest(indent, fmt(env, conclusion, opts))}; + r += format{line(), turnstile, space(), nest(indent, fmt(conclusion))}; return group(r); } @@ -137,10 +138,9 @@ static int goal_type(lua_State * L) { return push_expr(L, to_goal(L, 1).get_type static int goal_tostring(lua_State * L) { std::ostringstream out; goal & g = to_goal(L, 1); - environment env = get_global_environment(L); - formatter fmt = get_global_formatter(L); + formatter fmt = mk_formatter(L); options opts = get_global_options(L); - out << mk_pair(g.pp(env, fmt, opts), opts); + out << mk_pair(g.pp(fmt), opts); lua_pushstring(L, out.str().c_str()); return 1; } @@ -153,13 +153,9 @@ static int goal_pp(lua_State * L) { int nargs = lua_gettop(L); goal & g = to_goal(L, 1); if (nargs == 1) { - return push_format(L, g.pp(get_global_environment(L), get_global_formatter(L), get_global_options(L))); - } else if (nargs == 2) { - return push_format(L, g.pp(to_environment(L, 2), get_global_formatter(L), get_global_options(L))); - } else if (nargs == 3) { - return push_format(L, g.pp(to_environment(L, 2), to_formatter(L, 3), get_global_options(L))); + return push_format(L, g.pp(mk_formatter(L))); } else { - return push_format(L, g.pp(to_environment(L, 2), to_formatter(L, 3), to_options(L, 4))); + return push_format(L, g.pp(to_formatter(L, 2))); } } static int goal_validate_locals(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate_locals()); } diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index 7b7fd9c1d..5716f38ea 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -70,7 +70,7 @@ public: */ bool validate(environment const & env) const; - format pp(environment const & env, formatter const & fmt, options const & opts) const; + format pp(formatter const & fmt) const; }; io_state_stream const & operator<<(io_state_stream const & out, goal const & g); diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 89bb5d116..93ce5e6d8 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -27,7 +27,8 @@ static name g_proof_state_goal_names {"tactic", "goal_names"}; RegisterBoolOption(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES, "(tactic) display goal names when pretty printing proof state"); bool get_proof_state_goal_names(options const & opts) { return opts.get_bool(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES); } -format proof_state::pp(environment const & env, formatter const & fmt, options const & opts) const { +format proof_state::pp(formatter const & fmt) const { + options const & opts = fmt.get_options(); bool show_goal_names = get_proof_state_goal_names(opts); unsigned indent = get_pp_indent(opts); format r; @@ -35,9 +36,9 @@ format proof_state::pp(environment const & env, formatter const & fmt, options c for (auto const & g : get_goals()) { if (first) first = false; else r += line(); if (show_goal_names) { - r += group(format{format(g.get_name()), colon(), nest(indent, compose(line(), g.pp(env, fmt, opts)))}); + r += group(format{format(g.get_name()), colon(), nest(indent, compose(line(), g.pp(fmt)))}); } else { - r += g.pp(env, fmt, opts); + r += g.pp(fmt); } } if (first) r = format("no goals"); @@ -59,7 +60,7 @@ goals map_goals(proof_state const & s, std::function(goal const & io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s) { options const & opts = out.get_options(); - out.get_stream() << mk_pair(s.pp(out.get_environment(), out.get_formatter(), opts), opts); + out.get_stream() << mk_pair(s.pp(out.get_formatter()), opts); return out; } @@ -165,10 +166,9 @@ static int to_proof_state(lua_State * L) { static int proof_state_tostring(lua_State * L) { std::ostringstream out; proof_state & s = to_proof_state(L, 1); - environment env = get_global_environment(L); - formatter fmt = get_global_formatter(L); + formatter fmt = mk_formatter(L); options opts = get_global_options(L); - out << mk_pair(s.pp(env, fmt, opts), opts); + out << mk_pair(s.pp(fmt), opts); lua_pushstring(L, out.str().c_str()); return 1; } @@ -181,13 +181,9 @@ static int proof_state_pp(lua_State * L) { int nargs = lua_gettop(L); proof_state & s = to_proof_state(L, 1); if (nargs == 1) - return push_format(L, s.pp(get_global_environment(L), get_global_formatter(L), get_global_options(L))); - else if (nargs == 2) - return push_format(L, s.pp(to_environment(L, 2), get_global_formatter(L), get_global_options(L))); - else if (nargs == 3) - return push_format(L, s.pp(to_environment(L, 2), to_formatter(L, 3), get_global_options(L))); + return push_format(L, s.pp(mk_formatter(L))); else - return push_format(L, s.pp(to_environment(L, 2), to_formatter(L, 3), to_options(L, 4))); + return push_format(L, s.pp(to_formatter(L, 2))); } static const struct luaL_Reg proof_state_m[] = { diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 6ba892240..8f34485b7 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -31,7 +31,7 @@ public: /** \brief Return true iff this state does not have any goals left */ bool is_final_state() const { return empty(m_goals); } - format pp(environment const & env, formatter const & fmt, options const & opts) const; + format pp(formatter const & fmt) const; }; inline optional some_proof_state(proof_state const & s) { return some(s); } diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 9d71bbd35..725f4a1fa 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -658,7 +658,7 @@ struct unifier_fn { void display(std::ostream & out, justification const & j, unsigned indent = 0) { for (unsigned i = 0; i < indent; i++) out << " "; - out << j.pp(mk_simple_formatter(), options(), nullptr, m_subst) << "\n"; + out << j.pp(mk_simple_formatter_factory()(m_env, options()), nullptr, m_subst) << "\n"; if (j.is_composite()) { display(out, composite_child1(j), indent+2); display(out, composite_child2(j), indent+2); diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 5096d6e71..6e7946180 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -195,7 +195,7 @@ int main(int argc, char ** argv) { } environment env = mode == lean_mode::Standard ? mk_environment(trust_lvl) : mk_hott_environment(trust_lvl); - io_state ios(lean::mk_pretty_formatter()); + io_state ios(lean::mk_pretty_formatter_factory()); if (quiet) ios.set_option("verbose", false); script_state S = lean::get_thread_script_state(); diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index b48dda4a9..13e0d556f 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -19,6 +19,10 @@ static environment add_decl(environment const & env, declaration const & d) { return env.add(cd); } +formatter mk_formatter(environment const & env) { + return mk_simple_formatter_factory()(env, options()); +} + static void tst1() { environment env1; auto env2 = add_decl(env1, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool())); @@ -29,31 +33,31 @@ static void tst1() { auto env3 = add_decl(env2, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool())); lean_unreachable(); } catch (kernel_exception & ex) { - std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n"; + std::cout << "expected error: " << ex.pp(mk_formatter(ex.get_environment())) << "\n"; } try { auto env4 = add_decl(env2, mk_definition("BuggyBool", level_param_names(), mk_Bool(), mk_Bool())); lean_unreachable(); } catch (kernel_exception & ex) { - std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n"; + std::cout << "expected error: " << ex.pp(mk_formatter(ex.get_environment())) << "\n"; } try { auto env5 = add_decl(env2, mk_definition("Type1", level_param_names(), mk_metavar("T", mk_sort(mk_meta_univ("l"))), mk_Type())); lean_unreachable(); } catch (kernel_exception & ex) { - std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n"; + std::cout << "expected error: " << ex.pp(mk_formatter(ex.get_environment())) << "\n"; } try { auto env6 = add_decl(env2, mk_definition("Type1", level_param_names(), mk_Type(), mk_metavar("T", mk_sort(mk_meta_univ("l"))))); lean_unreachable(); } catch (kernel_exception & ex) { - std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n"; + std::cout << "expected error: " << ex.pp(mk_formatter(ex.get_environment())) << "\n"; } try { auto env7 = add_decl(env2, mk_definition("foo", level_param_names(), mk_Type() >> mk_Type(), mk_Bool())); lean_unreachable(); } catch (kernel_exception & ex) { - std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n"; + std::cout << "expected error: " << ex.pp(mk_formatter(ex.get_environment())) << "\n"; } expr A = Local("A", Type); expr x = Local("x", A); diff --git a/tests/lua/hott1.lua b/tests/lua/hott1.lua index 613733825..825b43aef 100644 --- a/tests/lua/hott1.lua +++ b/tests/lua/hott1.lua @@ -38,7 +38,6 @@ print("H1 : " .. tostring(tc:check(Const("H1")))) print("H2 : " .. tostring(tc:check(Const("H2")))) print("H3 : " .. tostring(tc:check(Const("H3")))) print("H4 : " .. tostring(tc:check(Const("H4")))) -print("N : " .. tostring(get_formatter()(env, tc:check(Const("N"))))) +print("N : " .. tostring(get_formatter_factory()(env)(tc:check(Const("N"))))) -- N : Type.{0} assert(not tc:is_def_eq(Const("a"), Const("b"))) -