michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel/formatter): add formatter_factory, and simplify formatter interface

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-10 18:32:00 +01:00
parent 92bb046854
commit 405e57eb2d
33 changed files with 261 additions and 318 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/frontends/lean/builtin_cmds.cpp
View file

@ -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();
}

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

@ -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<expr> 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<tactic>(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<tactic>();
}
}
@ -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);

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

@ -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();

16
src/frontends/lean/pp.cpp
View file

@ -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);
});
};
}
}

2
src/frontends/lean/pp.h
View file

@ -74,5 +74,5 @@ public:
format operator()(expr const & e);
};
formatter mk_pretty_formatter();
formatter_factory mk_pretty_formatter_factory();
}

33
src/kernel/error_msgs.cpp
View file

@ -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;
}
}

15
src/kernel/error_msgs.h
View file

@ -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);
}

2
src/kernel/expr.cpp
View file

@ -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(); }

7
src/kernel/expr.h
View file

@ -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); }

21
src/kernel/formatter.cpp
View file

@ -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; }
}

37
src/kernel/formatter.h
View file

@ -8,9 +8,11 @@ Author: Leonardo de Moura
#include <memory>
#include <utility>
#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<expr, expr> 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<expr, expr> 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<formatter_cell> m_cell;
formatter(formatter_cell * c):m_cell(c) {}
std::function<format(expr const &)> 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<typename FCell> friend formatter mk_formatter(FCell && fcell);
formatter(options const & o, std::function<format(expr const &)> 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<typename FCell> formatter mk_formatter(FCell && fcell) {
return formatter(new FCell(std::forward<FCell>(fcell)));
}
typedef std::function<formatter(environment const &, options const &)> 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<format(formatter const &, options const &)> pp_fn;
typedef std::function<format(formatter const &)> pp_fn;
}

14
src/kernel/justification.cpp
View file

@ -194,18 +194,18 @@ optional<expr> 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<expr> const & s, pp_jst_fn const & fn) {
return justification(new asserted_cell(fn, s));
}
justification mk_justification(optional<expr> 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<expr> 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);
});
}

6
src/kernel/justification.h
View file

@ -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<format(formatter const &, options const &, pos_info_provider const *, substitution const &)> pp_jst_fn;
typedef std::function<format(formatter const &, pos_info_provider const *, substitution const &)> 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<format(formatter const &, options const &, substitution const &)> pp_jst_sfn;
typedef std::function<format(formatter const &, substitution const &)> pp_jst_sfn;
/** \brief Return a format object containing position information for the given expression (if available) */
format to_pos(optional<expr> const & e, pos_info_provider const * p);

6
src/kernel/kernel_exception.cpp
View file

@ -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<expr> 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<expr> 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<expr> const & m) {

2
src/kernel/kernel_exception.h
View file

@ -28,7 +28,7 @@ public:
This information is used to provide better error messages.
*/
virtual optional<expr> 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; }
};

59
src/kernel/type_checker.cpp
View file

@ -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);

5
src/kernel/type_checker.h
View file

@ -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<justification> 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();
};
}

2
src/library/error_handling/error_handling.cpp
View file

@ -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 {

16
src/library/io_state.cpp
View file

@ -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<stdout_channel>()),
m_diagnostic_channel(std::make_shared<stderr_channel>()) {
}
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<stdout_channel>()),
m_diagnostic_channel(std::make_shared<stderr_channel>()) {
}
io_state::io_state(io_state const & ios, std::shared_ptr<output_channel> const & r, std::shared_ptr<output_channel> 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;
}
}

12
src/library/io_state.h
View file

@ -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<output_channel> m_regular_channel;
std::shared_ptr<output_channel> 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<output_channel> const & r, std::shared_ptr<output_channel> 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<output_channel> const & out);
void set_diagnostic_channel(std::shared_ptr<output_channel> const & out);
void set_options(options const & opts);
void set_formatter(formatter const & f);
void set_formatter_factory(formatter_factory const & f);
template<typename T> void set_option(name const & n, T const & v) {
set_options(get_options().update(n, v));
}

4
src/library/io_state_stream.cpp
View file

@ -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;
}
}

36
src/library/io_state_stream.h
View file

@ -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() {} };

139
src/library/kernel_bindings.cpp
View file

@ -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<formatter_factory_call>},
{0, 0}
};
static const struct luaL_Reg formatter_m[] = {
{"__gc", formatter_gc}, // never throws
{"__call", safe_function<formatter_call>},
{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<formatter> get_global_formatter_core(lua_State * L) {
optional<formatter_factory> get_global_formatter_factory_core(lua_State * L) {
io_state * io = get_io_state_ptr(L);
if (io != nullptr) {
return optional<formatter>(io->get_formatter());
return optional<formatter_factory>(io->get_formatter_factory());
} else {
lua_pushlightuserdata(L, static_cast<void *>(&g_formatter_key));
lua_pushlightuserdata(L, static_cast<void *>(&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<formatter>(r);
return optional<formatter_factory>(r);
} else {
lua_pop(L, 1);
return optional<formatter>();
return optional<formatter_factory>();
}
}
}
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<void *>(&g_formatter_key));
push_formatter(L, fmt);
lua_pushlightuserdata(L, static_cast<void *>(&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<io_state_get_options>},
{"set_options", safe_function<io_state_set_options>},
{"get_formatter", safe_function<io_state_get_formatter>},
{"print_diagnostic", safe_function<io_state_print_diagnostic>},
{"print_regular", safe_function<io_state_print_regular>},
{"print", safe_function<io_state_print_regular>},
{"diagnostic", safe_function<io_state_print_diagnostic>},
{"__gc", io_state_gc}, // never throws
{"get_options", safe_function<io_state_get_options>},
{"set_options", safe_function<io_state_set_options>},
{"get_formatter_factory", safe_function<io_state_get_formatter_factory>},
{"print_diagnostic", safe_function<io_state_print_diagnostic>},
{"print_regular", safe_function<io_state_print_regular>},
{"print", safe_function<io_state_print_regular>},
{"diagnostic", safe_function<io_state_print_diagnostic>},
{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);

13
src/library/kernel_bindings.h
View file

@ -28,23 +28,26 @@ int push_optional_declaration(lua_State * L, optional<declaration> const & e);
int push_optional_constraint(lua_State * L, optional<constraint> const & c);
int push_list_expr(lua_State * L, list<expr> 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<formatter> get_global_formatter_core(lua_State * L);
optional<formatter_factory> 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);

2
src/library/string.cpp
View file

@ -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());

20
src/library/tactic/goal.cpp
View file

@ -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()); }

2
src/library/tactic/goal.h
View file

@ -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);

22
src/library/tactic/proof_state.cpp
View file

@ -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<optional<goal>(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[] = {

2
src/library/tactic/proof_state.h
View file

@ -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<proof_state> some_proof_state(proof_state const & s) { return some(s); }

2
src/library/unifier.cpp
View file

@ -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);

2
src/shell/lean.cpp
View file

@ -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();

14
src/tests/kernel/environment.cpp
View file

@ -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);

3
tests/lua/hott1.lua
View file

@ -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")))