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

Extend formatter with support for definitions and postulates.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-15 19:26:49 -07:00
parent 790d4a4447
commit 5ec2780321
3 changed files with 19 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/kernel/expr_formatter.cpp
View file

@ -8,6 +8,18 @@ Author: Leonardo de Moura
#include "exception.h"
namespace lean {
format expr_formatter::operator()(char const * kwd, name const & n, expr const & t, expr const & v) {
format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(),
operator()(t), format(" :="), line(), operator()(v)};
return group(nest(def));
}
format expr_formatter::operator()(char const * kwd, name const & n, expr const & t) {
format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), operator()(t)};
return group(nest(def));
}
void expr_formatter::pp(std::ostream & out, expr const & e, context const & c) {
out << mk_pair(operator()(e, c), get_options());
}

5
src/kernel/expr_formatter.h
View file

@ -16,6 +16,11 @@ public:
virtual ~expr_formatter() {}
/** \brief Convert expression in the given context into a format object. */
virtual format operator()(expr const & e, context const & c = context()) = 0;
/** \brief format a definition. */
virtual format operator()(char const * kwd, name const & n, expr const & t, expr const & v);
/** \brief format a postulate. */
virtual format operator()(char const * kwd, name const & n, expr const & t);
/** \brief Return options for pretty printing. */
virtual options get_options() const = 0;

7
src/kernel/object.cpp
View file

@ -36,9 +36,7 @@ bool definition::is_opaque() const { return m_opaque; }
expr const & definition::get_value() const { return m_value; }
format definition::pp(environment const & env) const {
expr_formatter & fmt = env.get_formatter();
format def = format{highlight_command(format(keyword())), space(), format(get_name()), space(), colon(), space(),
fmt(get_type()), format(" :="), line(), fmt(get_value())};
return group(fmt.nest(def));
return fmt(keyword(), get_name(), get_type(), get_value());
}
char const * theorem::g_keyword = "Theorem";
@ -53,8 +51,7 @@ bool fact::is_opaque() const { lean_unreachable(); return false; }
expr const & fact::get_value() const { lean_unreachable(); return expr::null(); }
format fact::pp(environment const & env) const {
expr_formatter & fmt = env.get_formatter();
format def = format{highlight_command(format(keyword())), space(), format(get_name()), space(), colon(), space(), fmt(get_type())};
return group(fmt.nest(def));
return fmt(keyword(), get_name(), get_type());
}
char const * axiom::g_keyword = "Axiom";