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

Move pretty printer to frontend. Add support for mixfix pretty printing

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-15 18:54:01 -07:00
parent 5395ced0e5
commit 790d4a4447
19 changed files with 654 additions and 323 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/exprlib/CMakeLists.txt Normal file
View file

@ -0,0 +1,2 @@
add_library(exprlib basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp)
target_link_libraries(exprlib ${LEAN_LIBS})

2
src/frontend/CMakeLists.txt
View file

@ -1,2 +1,2 @@
add_library(frontend frontend.cpp operator_info.cpp scanner.cpp)
add_library(frontend frontend.cpp operator_info.cpp scanner.cpp pp.cpp builtin_notation.cpp)
target_link_libraries(frontend ${LEAN_LIBS})

19
src/frontend/builtin_notation.cpp Normal file
View file

@ -0,0 +1,19 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "frontend.h"
#include "builtin.h"
namespace lean {
/**
\brief Initialize builtin notation.
*/
void init_builtin_notation(frontend & f) {
f.add_infixl("\u2227", 13, const_name(mk_and_fn()));
f.add_infixl("\u2228", 14, const_name(mk_or_fn()));
f.add_prefix("\u00ac", 3, const_name(mk_not_fn()));
}
}

11
src/frontend/builtin_notation.h Normal file
View file

@ -0,0 +1,11 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
namespace lean {
class frontend;
void init_builtin_notation(frontend & fe);
}

84
src/frontend/frontend.cpp
View file

@ -9,6 +9,9 @@ Author: Leonardo de Moura
#include "frontend.h"
#include "environment.h"
#include "operator_info.h"
#include "toplevel.h"
#include "builtin_notation.h"
#include "pp.h"
namespace lean {
/**
@ -26,9 +29,10 @@ public:
virtual format pp(environment const &) const {
char const * cmd;
switch (m_op.get_fixity()) {
case fixity::Infixl: cmd = "Infixl"; break;
case fixity::Infixr: cmd = "Infixr"; break;
case fixity::Prefix: cmd = "Prefix"; break;
case fixity::Infix: cmd = "Infix"; break;
case fixity::Infixl: cmd = "Infixl"; break;
case fixity::Infixr: cmd = "Infixr"; break;
case fixity::Prefix: cmd = "Prefix"; break;
case fixity::Postfix: cmd = "Postfix"; break;
case fixity::Mixfixl: cmd = "Mixfixl"; break;
case fixity::Mixfixr: cmd = "Mixfixr"; break;
@ -132,7 +136,7 @@ struct frontend::imp {
/** \brief Remove all internal operators that are associated with the given operator symbol (aka notation) */
void remove_bindings(operator_info const & op) {
for (name const & n : op.get_internal_names()) {
if (has_parent() && !is_nil(m_parent->find_op_for(n))) {
if (has_parent() && m_parent->find_op_for(n)) {
// parent has a binding for n... we must hide it.
insert(m_name_to_operator, n, operator_info());
} else {
@ -162,7 +166,7 @@ struct frontend::imp {
void add_op(operator_info new_op, name const & n, bool led) {
name const & opn = new_op.get_op_name();
operator_info old_op = find_op(opn, led);
if (is_nil(old_op)) {
if (!old_op) {
register_new_op(new_op, n, led);
} else if (old_op == new_op) {
// overload
@ -182,24 +186,17 @@ struct frontend::imp {
m_env.add_anonymous_object(new notation_declaration(new_op, n));
}
void add_infixl(name const & opn, unsigned precedence, name const & n) {
add_op(infixl(opn, precedence), n, true);
}
void add_infixl(name const & opn, unsigned p, name const & n) { add_op(infixl(opn, p), n, true); }
void add_infixr(name const & opn, unsigned p, name const & n) { add_op(infixr(opn, p), n, true); }
void add_prefix(name const & opn, unsigned p, name const & n) { add_op(prefix(opn, p), n, false); }
void add_postfix(name const & opn, unsigned p, name const & n) { add_op(postfix(opn, p), n, true); }
void add_mixfixl(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixl(sz, opns, p), n, false); }
void add_mixfixr(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixr(sz, opns, p), n, true); }
void add_mixfixc(unsigned sz, name const * opns, unsigned p, name const & n) { add_op(mixfixc(sz, opns, p), n, false); }
void add_infixr(name const & opn, unsigned precedence, name const & n) {
add_op(infixr(opn, precedence), n, true);
}
void add_prefix(name const & opn, unsigned precedence, name const & n) {
add_op(prefix(opn, precedence), n, false);
}
void add_postfix(name const & opn, unsigned precedence, name const & n) {
add_op(postfix(opn, precedence), n, true);
}
imp():
m_num_children(0) {
imp(frontend & fe):
m_num_children(0),
m_env(mk_toplevel()) {
}
explicit imp(std::shared_ptr<imp> const & parent):
@ -215,37 +212,18 @@ struct frontend::imp {
}
};
frontend::frontend():
m_imp(new imp()) {
frontend::frontend():m_imp(new imp(*this)) {
init_builtin_notation(*this);
m_imp->m_env.set_formatter(mk_pp_expr_formatter(*this, options()));
}
frontend::frontend(imp * new_ptr):m_imp(new_ptr) {}
frontend::frontend(std::shared_ptr<imp> const & ptr):m_imp(ptr) {}
frontend::~frontend() {}
frontend::frontend(imp * new_ptr):
m_imp(new_ptr) {
}
frontend::frontend(std::shared_ptr<imp> const & ptr):
m_imp(ptr) {
}
frontend::~frontend() {
}
frontend frontend::mk_child() const {
return frontend(new imp(m_imp));
}
bool frontend::has_children() const {
return m_imp->has_children();
}
bool frontend::has_parent() const {
return m_imp->has_parent();
}
frontend frontend::parent() const {
lean_assert(has_parent());
return frontend(m_imp->m_parent);
}
frontend frontend::mk_child() const { return frontend(new imp(m_imp)); }
bool frontend::has_children() const { return m_imp->has_children(); }
bool frontend::has_parent() const { return m_imp->has_parent(); }
frontend frontend::parent() const { lean_assert(has_parent()); return frontend(m_imp->m_parent); }
environment const & frontend::env() const { return m_imp->m_env; }
@ -257,6 +235,10 @@ void frontend::add_infixl(name const & opn, unsigned p, name const & n) { m_imp
void frontend::add_infixr(name const & opn, unsigned p, name const & n) { m_imp->add_infixr(opn, p, n); }
void frontend::add_prefix(name const & opn, unsigned p, name const & n) { m_imp->add_prefix(opn, p, n); }
void frontend::add_postfix(name const & opn, unsigned p, name const & n) { m_imp->add_postfix(opn, p, n); }
void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixl(sz, opns, p, n); }
void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixr(sz, opns, p, n); }
void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixc(sz, opns, p, n); }
operator_info frontend::find_op_for(name const & n) const { return m_imp->find_op_for(n); }
void frontend::display(std::ostream & out) const { m_imp->m_env.display(out); }
}

15
src/frontend/frontend.h
View file

@ -6,10 +6,10 @@ Author: Leonardo de Moura
*/
#pragma once
#include <memory>
#include "level.h"
#include "environment.h"
#include "operator_info.h"
namespace lean {
class environment;
/**
\brief Object for managing the environment, parser, pretty printer,
elaborator, etc.
@ -56,6 +56,17 @@ public:
void add_infixr(name const & opn, unsigned precedence, name const & n);
void add_prefix(name const & opn, unsigned precedence, name const & n);
void add_postfix(name const & opn, unsigned precedence, name const & n);
void add_mixfixl(unsigned sz, name const * opns, unsigned precedence, name const & n);
void add_mixfixr(unsigned sz, name const * opns, unsigned precedence, name const & n);
void add_mixfixc(unsigned sz, name const * opns, unsigned precedence, name const & n);
/**
\brief Return the operator (if it exists) associated with the
given internal name.
\remark If an operator is not associated with \c n, then
return the nil operator.
*/
operator_info find_op_for(name const & n) const;
// =======================================
/** \brief Display universal variable constraints and objects stored in this environment and its parents. */

6
src/frontend/operator_info.cpp
View file

@ -76,6 +76,9 @@ bool operator==(operator_info const & op1, operator_info const & op2) {
return true;
}
operator_info infix(name const & op, unsigned precedence) {
return operator_info(new operator_info::imp(op, fixity::Infix, precedence));
}
operator_info infixr(name const & op, unsigned precedence) {
return operator_info(new operator_info::imp(op, fixity::Infixr, precedence));
}
@ -103,6 +106,7 @@ static char const * g_arrow = "\u21a6";
format pp(operator_info const & o) {
format r;
switch (o.get_fixity()) {
case fixity::Infix: r = format("Infix"); break;
case fixity::Infixl: r = format("Infixl"); break;
case fixity::Infixr: r = format("Infixr"); break;
case fixity::Prefix: r = format("Prefix"); break;
@ -118,7 +122,7 @@ format pp(operator_info const & o) {
r += format{format(o.get_precedence()), space()};
switch (o.get_fixity()) {
case fixity::Infixl: case fixity::Infixr: case fixity::Prefix: case fixity::Postfix:
case fixity::Infix: case fixity::Infixl: case fixity::Infixr: case fixity::Prefix: case fixity::Postfix:
r += pp(o.get_op_name()); break;
case fixity::Mixfixl:
for (auto p : o.get_op_name_parts()) r += format{pp(p), format(" _")};

6
src/frontend/operator_info.h
View file

@ -20,7 +20,7 @@ namespace lean {
Mixfixr: _ ID _ ID ... _ ID (has at least two parts)
Mixfixc: ID _ ID _ ... ID _ ID (has at least two parts)
*/
enum class fixity { Prefix, Infixl, Infixr, Postfix, Mixfixl, Mixfixr, Mixfixc };
enum class fixity { Prefix, Infix, Infixl, Infixr, Postfix, Mixfixl, Mixfixr, Mixfixc };
/**
\brief Data-structure for storing user defined operator
@ -43,8 +43,9 @@ public:
friend void swap(operator_info & o1, operator_info & o2) { std::swap(o1.m_ptr, o2.m_ptr); }
friend bool is_nil(operator_info const & o) { return o.m_ptr == nullptr; }
operator bool() const { return m_ptr != nullptr; }
friend operator_info infix(name const & op, unsigned precedence);
friend operator_info infixl(name const & op, unsigned precedence);
friend operator_info infixr(name const & op, unsigned precedence);
friend operator_info prefix(name const & op, unsigned precedence);
@ -86,6 +87,7 @@ public:
friend bool operator==(operator_info const & op1, operator_info const & op2);
friend bool operator!=(operator_info const & op1, operator_info const & op2) { return !(op1 == op2); }
};
operator_info infix(name const & op, unsigned precedence);
operator_info infixl(name const & op, unsigned precedence);
operator_info infixr(name const & op, unsigned precedence);
operator_info prefix(name const & op, unsigned precedence);

539
src/frontend/pp.cpp Normal file
View file

@ -0,0 +1,539 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <limits>
#include <memory>
#include "frontend.h"
#include "context.h"
#include "scoped_map.h"
#include "expr_formatter.h"
#include "occurs.h"
#include "instantiate.h"
#include "options.h"
#ifndef LEAN_DEFAULT_PP_MAX_DEPTH
#define LEAN_DEFAULT_PP_MAX_DEPTH std::numeric_limits<unsigned>::max()
#endif
#ifndef LEAN_DEFAULT_PP_MAX_STEPS
#define LEAN_DEFAULT_PP_MAX_STEPS std::numeric_limits<unsigned>::max()
#endif
#ifndef LEAN_DEFAULT_PP_IMPLICIT
#define LEAN_DEFAULT_PP_IMPLICIT false
#endif
#ifndef LEAN_DEFAULT_PP_NOTATION
#define LEAN_DEFAULT_PP_NOTATION true
#endif
#ifndef LEAN_DEFAULT_PP_EXTRA_LETS
#define LEAN_DEFAULT_PP_EXTRA_LETS true
#endif
#ifndef LEAN_DEFAULT_PP_ALIAS_MIN_DEPTH
#define LEAN_DEFAULT_PP_ALIAS_MIN_DEPTH 1000 //TODO: fix to reasonable value
#endif
namespace lean {
static format g_Type_fmt = highlight_builtin(format("Type"));
static unsigned g_eq_prec = 20;
static format g_eq_fmt = format("=");
static char const * g_eq_sym = "eq";
static unsigned g_eq_sz = strlen(g_eq_sym);
static format g_eq_sym_fmt = format(g_eq_sym);
static format g_lambda_fmt = highlight_keyword(format("\u03BB"));
static format g_Pi_fmt = highlight_keyword(format("\u03A0"));
static format g_arrow_fmt = highlight_keyword(format("\u2192"));
static format g_ellipsis_fmt = highlight(format("\u2026"));
static format g_let_fmt = highlight_keyword(format("let"));
static format g_in_fmt = highlight_keyword(format("in"));
static name g_pp_max_depth {"pp", "max_depth"};
static name g_pp_max_steps {"pp", "max_steps"};
static name g_pp_implicit {"pp", "implicit"};
static name g_pp_notation {"pp", "notation"};
static name g_pp_extra_lets {"pp", "extra_lets"};
static name g_pp_alias_min_depth {"pp", "alias_min_depth"};
unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
bool get_pp_implicit(options const & opts) { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); }
bool get_pp_notation(options const & opts) { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); }
bool get_pp_extra_lets(options const & opts) { return opts.get_bool(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS); }
unsigned get_pp_alias_min_depth(options const & opts) { return opts.get_unsigned(g_pp_alias_min_depth, LEAN_DEFAULT_PP_ALIAS_MIN_DEPTH); }
/** \brief Functional object for pretty printing expressions */
struct pp_fn {
typedef scoped_map<expr, name, expr_hash, expr_eqp> aliases;
typedef std::vector<std::pair<name, format>> aliases_defs;
frontend const & m_frontend;
context const & m_context;
// State
aliases m_aliases;
aliases_defs m_aliases_defs;
unsigned m_num_steps;
name m_aux;
// Configuration
unsigned m_indent;
unsigned m_max_depth;
unsigned m_max_steps;
bool m_implict;
bool m_notation; //!< if true use notation
bool m_extra_lets; //!< introduce extra let-expression to cope with sharing.
unsigned m_alias_min_depth; //!< minimal depth to create an alias
// Create a scope for local definitions
struct mk_scope {
pp_fn & m_fn;
unsigned m_old_size;
mk_scope(pp_fn & fn):m_fn(fn), m_old_size(fn.m_aliases_defs.size()) {
m_fn.m_aliases.push();
}
~mk_scope() {
lean_assert(m_old_size <= m_fn.m_aliases_defs.size());
m_fn.m_aliases.pop();
m_fn.m_aliases_defs.resize(m_old_size);
}
};
format nest(unsigned i, format const & f) { return ::lean::nest(i, f); }
typedef std::pair<format, unsigned> result;
/**
\brief Return true iff \c e is an atomic operation.
*/
bool is_atomic(expr const & e) {
switch (e.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type:
return true;
case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let:
return false;
}
return false;
}
result mk_result(format const & fmt, unsigned depth) {
return mk_pair(fmt, depth);
}
result pp_ellipsis() {
return mk_result(g_ellipsis_fmt, 1);
}
result pp_var(expr const & e) {
unsigned vidx = var_idx(e);
return mk_result(compose(format("#"), format(vidx)), 1);
}
result pp_constant(expr const & e) {
return mk_result(::lean::pp(const_name(e)), 1);
}
result pp_value(expr const & e) {
return mk_result(to_value(e).pp(), 1);
}
result pp_type(expr const & e) {
if (e == Type()) {
return mk_result(g_Type_fmt, 1);
} else {
return mk_result(format{g_Type_fmt, space(), ::lean::pp(ty_level(e))}, 1);
}
}
/**
\brief Return the operator associated with \c e.
Return the nil operator if there is none.
We say \c e has an operator associated with it, if:
1) It is a constant and there is an operator associated with it.
2) It is an application, and the function is a constant \c c with an
operator associated with \c c.
*/
operator_info get_operator(expr const & e) {
if (is_constant(e))
return m_frontend.find_op_for(const_name(e));
else if (is_app(e) && is_constant(arg(e, 0)))
return m_frontend.find_op_for(const_name(arg(e, 0)));
else
return operator_info();
}
/** \brief Return true if the application \c e has the number of arguments expected by the operator \c op. */
bool has_expected_num_args(expr const & e, operator_info const & op) {
switch (op.get_fixity()) {
case fixity::Infix: case fixity::Infixl: case fixity::Infixr:
return num_args(e) == 3;
case fixity::Prefix: case fixity::Postfix:
return num_args(e) == 2;
case fixity::Mixfixl: case fixity::Mixfixr:
return num_args(e) == length(op.get_op_name_parts()) + 1;
case fixity::Mixfixc:
return num_args(e) == length(op.get_op_name_parts());
}
lean_unreachable();
return false;
}
/**
\brief Pretty print given expression and put parenthesis around it.
*/
result pp_child_with_paren(expr const & e, unsigned depth) {
result r = pp(e, depth + 1);
return mk_result(format{lp(), r.first, rp()}, r.second);
}
/**
\brief Pretty print given expression and put parenthesis around
it if it is not atomic.
*/
result pp_child(expr const & e, unsigned depth) {
if (is_atomic(e))
return pp(e, depth + 1);
else
return pp_child_with_paren(e, depth);
}
/**
\brief Pretty print the child of an infix, prefix, postfix or
mixfix operator. It will add parethesis when needed.
*/
result pp_mixfix_child(operator_info const & op, expr const & e, unsigned depth) {
if (is_atomic(e)) {
return pp(e, depth + 1);
} else {
operator_info op_child = get_operator(e);
if (op_child && op.get_precedence() < op_child.get_precedence())
return pp(e, depth + 1);
else
return pp_child_with_paren(e, depth);
}
}
/**
\brief Pretty print the child of an associative infix
operator. It will add parethesis when needed.
*/
result pp_infix_child(operator_info const & op, expr const & e, unsigned depth) {
if (is_atomic(e)) {
return pp(e, depth + 1);
} else {
operator_info op_child = get_operator(e);
if (op_child && (op == op_child || op.get_precedence() < op_child.get_precedence()))
return pp(e, depth + 1);
else
return pp_child_with_paren(e, depth);
}
}
result mk_infix(operator_info const & op, result const & lhs, result const & rhs) {
unsigned r_depth = std::max(lhs.second, rhs.second) + 1;
format r_format = group(format{lhs.first, space(), format(op.get_op_name()), line(), rhs.first});
return mk_result(r_format, r_depth);
}
/**
\brief Pretty print an application.
*/
result pp_app(expr const & e, unsigned depth) {
operator_info op;
if (m_notation && (op = get_operator(e)) && has_expected_num_args(e, op)) {
result p_arg;
format r_format;
unsigned sz;
unsigned r_depth = 0;
switch (op.get_fixity()) {
case fixity::Infix:
return mk_infix(op, pp_mixfix_child(op, arg(e, 1), depth), pp_mixfix_child(op, arg(e, 2), depth));
case fixity::Infixr:
return mk_infix(op, pp_mixfix_child(op, arg(e, 1), depth), pp_infix_child(op, arg(e, 2), depth));
case fixity::Infixl:
return mk_infix(op, pp_infix_child(op, arg(e, 1), depth), pp_mixfix_child(op, arg(e, 2), depth));
case fixity::Prefix:
p_arg = pp_infix_child(op, arg(e, 1), depth);
sz = op.get_op_name().size();
return mk_result(group(format{format(op.get_op_name()), nest(sz+1, format{line(), p_arg.first})}),
p_arg.second + 1);
case fixity::Postfix:
p_arg = pp_mixfix_child(op, arg(e, 1), depth);
return mk_result(group(format{p_arg.first, space(), format(op.get_op_name())}),
p_arg.second + 1);
case fixity::Mixfixr: {
// _ ID ... _ ID
list<name> parts = op.get_op_name_parts();
auto it = parts.begin();
for (unsigned i = 1; i < num_args(e); i++) {
result p_arg = pp_mixfix_child(op, arg(e, i), depth);
r_format += format{p_arg.first, space(), format(*it), line()};
r_depth = std::max(r_depth, p_arg.second);
++it;
}
return mk_result(group(r_format), r_depth + 1);
}
case fixity::Mixfixl: case fixity::Mixfixc: {
// ID _ ... _
// ID _ ... _ ID
list<name> parts = op.get_op_name_parts();
auto it = parts.begin();
for (unsigned i = 1; i < num_args(e); i++) {
result p_arg = pp_mixfix_child(op, arg(e, i), depth);
unsigned sz = (*it).size();
r_format += format{format(*it), nest(sz+1, format{line(), p_arg.first})};
r_depth = std::max(r_depth, p_arg.second);
++it;
}
if (it != parts.end()) {
// it is Mixfixc
r_format += format{space(), format(*it)};
}
return mk_result(group(r_format), r_depth + 1);
}}
lean_unreachable();
return mk_result(format(), 0);
} else {
// standard function application
result p = pp_child(arg(e, 0), depth);
format r_format = p.first;
unsigned r_depth = p.second;
for (unsigned i = 1; i < num_args(e); i++) {
result p_arg = pp_child(arg(e, i), depth);
r_format += format{line(), p_arg.first};
r_depth = std::max(r_depth, p_arg.second);
}
return mk_result(group(nest(m_indent, r_format)), r_depth + 1);
}
}
/**
\brief Collect nested Lambdas (or Pis), and instantiate
variables with unused names. Store in \c r the selected names
and associated domains. Return the body of the sequence of
Lambda (of Pis).
*/
expr collect_nested(expr const & e, expr_kind k, buffer<std::pair<name, expr>> & r) {
if (e.kind() == k) {
name const & n = abst_name(e);
name n1 = n;
unsigned i = 1;
while (occurs(n1, abst_body(e))) {
n1 = name(n, i);
i++;
}
r.push_back(mk_pair(n1, abst_domain(e)));
expr b = instantiate_with_closed(abst_body(e), mk_constant(n1));
return collect_nested(b, k, r);
} else {
return e;
}
}
result pp_scoped_child(expr const & e, unsigned depth) {
if (is_atomic(e)) {
return pp(e, depth + 1);
} else {
mk_scope s(*this);
// TODO: create Let with new aliases
return pp(e, depth+1);
}
}
result pp_arrow_body(expr const & e, unsigned depth) {
if (is_atomic(e) || is_arrow(e)) {
return pp(e, depth + 1);
} else {
return pp_child_with_paren(e, depth);
}
}
template<typename It>
format pp_bnames(It const & begin, It const & end, bool use_line) {
auto it = begin;
format r = format(it->first);
++it;
for (; it != end; ++it) {
r += compose(use_line ? line() : space(), format(it->first));
}
return r;
}
result pp_abstraction(expr const & e, unsigned depth) {
if (is_arrow(e)) {
result p_lhs = pp_child(abst_domain(e), depth);
result p_rhs = pp_arrow_body(abst_body(e), depth);
format r_format = group(format{p_lhs.first, space(), g_arrow_fmt, line(), p_rhs.first});
return mk_result(r_format, std::max(p_lhs.second, p_rhs.second) + 1);
} else {
buffer<std::pair<name, expr>> nested;
expr b = collect_nested(e, e.kind(), nested);
lean_assert(b.kind() != e.kind());
format head = is_lambda(e) ? g_lambda_fmt : g_Pi_fmt;
format body_sep = comma();
expr domain0 = nested[0].second;
if (std::all_of(nested.begin() + 1, nested.end(), [&](std::pair<name, expr> const & p) { return p.second == domain0; })) {
// Domain of all binders is the same
format names = pp_bnames(nested.begin(), nested.end(), false);
result p_domain = pp_scoped_child(domain0, depth);
result p_body = pp_scoped_child(b, depth);
format r_format = group(nest(m_indent, format{head, space(), names, space(), colon(), space(), p_domain.first, body_sep, line(), p_body.first}));
return mk_result(r_format, std::max(p_domain.second, p_body.second)+1);
} else {
auto it = nested.begin();
auto end = nested.end();
unsigned r_depth;
// PP binders in blocks (names ... : type)
bool first = true;
format bindings;
while (it != end) {
auto it2 = it;
++it2;
while (it2 != end && it2->second == it->second) {
++it2;
}
result p_domain = pp_scoped_child(it->second, depth);
r_depth = std::max(r_depth, p_domain.second);
format block = group(nest(m_indent, format{lp(), pp_bnames(it, it2, true), space(), colon(), space(), p_domain.first, rp()}));
if (first) {
bindings = block;
first = false;
} else {
bindings += compose(line(), block);
}
it = it2;
}
result p_body = pp_scoped_child(b, depth);
format r_format = group(nest(m_indent, format{head, space(), group(bindings), body_sep, line(), p_body.first}));
return mk_result(r_format, std::max(r_depth, p_body.second)+1);
}
}
}
result pp_let(expr const & e, unsigned depth) {
// TODO
return mk_result(format("TODO"), 1);
}
/** \brief Pretty print the child of an equality. */
result pp_eq_child(expr const & e, unsigned depth) {
if (is_atomic(e)) {
return pp(e, depth + 1);
} else {
operator_info op_child = get_operator(e);
if (op_child && g_eq_prec < op_child.get_precedence())
return pp(e, depth + 1);
else
return pp_child_with_paren(e, depth);
}
}
/** \brief Pretty print an equality */
result pp_eq(expr const & e, unsigned depth) {
result p_arg1, p_arg2;
format r_format;
if (m_notation) {
p_arg1 = pp_eq_child(eq_lhs(e), depth);
p_arg2 = pp_eq_child(eq_rhs(e), depth);
r_format = group(format{p_arg1.first, space(), g_eq_fmt, line(), p_arg2.first});
} else {
p_arg1 = pp_child(eq_lhs(e), depth);
p_arg2 = pp_child(eq_rhs(e), depth);
r_format = group(format{g_eq_sym_fmt, nest(g_eq_sz + 1,
format{line(), p_arg1.first,
line(), p_arg2.first})});
}
return mk_result(r_format, std::max(p_arg1.second, p_arg2.second) + 1);
}
result pp(expr const & e, unsigned depth) {
if (m_num_steps > m_max_steps || depth > m_max_depth) {
return pp_ellipsis();
} else {
m_num_steps++;
if (m_extra_lets && is_shared(e)) {
auto it = m_aliases.find(e);
if (it != m_aliases.end())
return mk_result(format(it->second), 1);
}
result r;
switch (e.kind()) {
case expr_kind::Var: r = pp_var(e); break;
case expr_kind::Constant: r = pp_constant(e); break;
case expr_kind::Value: r = pp_value(e); break;
case expr_kind::App: r = pp_app(e, depth); break;
case expr_kind::Lambda:
case expr_kind::Pi: r = pp_abstraction(e, depth); break;
case expr_kind::Type: r = pp_type(e); break;
case expr_kind::Eq: r = pp_eq(e, depth); break;
case expr_kind::Let: r = pp_let(e, depth); break;
}
if (m_extra_lets && is_shared(e) && r.second > m_alias_min_depth) {
std::cout << "DEPTH: " << r.second << "\n";
name new_aux = name(m_aux, m_aliases.size());
m_aliases.insert(e, new_aux);
return mk_result(format(new_aux), 1);
}
return r;
}
}
void set_options(options const & opts) {
m_indent = get_pp_indent(opts);
m_max_depth = get_pp_max_depth(opts);
m_max_steps = get_pp_max_steps(opts);
m_implict = get_pp_implicit(opts);
m_notation = get_pp_notation(opts);
m_extra_lets = get_pp_extra_lets(opts);
m_alias_min_depth = get_pp_alias_min_depth(opts);
}
pp_fn(frontend const & fe, context const & ctx, options const & opts):
m_frontend(fe),
m_context(ctx) {
set_options(opts);
}
format operator()(expr const & e) {
m_aliases.clear();
m_aliases_defs.clear();
m_num_steps = 0;
m_aux = name("aux"); // TODO: find non used prefix
return pp(e, 0).first;
}
};
class pp_expr_formatter : public expr_formatter {
frontend const & m_frontend;
options m_options;
public:
pp_expr_formatter(frontend const & fe, options const & opts):
m_frontend(fe),
m_options(opts) {
}
virtual ~pp_expr_formatter() {
}
virtual options get_options() const {
return m_options;
}
// TODO: remove context parameter from expr_formatter
// The context pretty printer must open the expression
// before pretty-printing it.
virtual format operator()(expr const & e, context const & c) {
return pp_fn(m_frontend, c, m_options)(e);
}
};
std::shared_ptr<expr_formatter> mk_pp_expr_formatter(frontend const & fe, options const & opts) {
return std::shared_ptr<expr_formatter>(new pp_expr_formatter(fe, opts));
}
}

7
src/kernel/pp.h → src/frontend/pp.h
View file

@ -5,11 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "expr.h"
#include "format.h"
#include "expr_formatter.h"
namespace lean {
class environment;
format pp(expr const & n);
format pp(expr const & n, environment const & env);
std::shared_ptr<expr_formatter> mk_pp_expr_formatter(frontend const & fe, options const & opts);
}

2
src/kernel/CMakeLists.txt
View file

@ -1,6 +1,6 @@
add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
normalize.cpp context.cpp level.cpp object.cpp environment.cpp
type_check.cpp builtin.cpp expr_formatter.cpp expr_locator.cpp
occurs.cpp pp.cpp)
occurs.cpp)
target_link_libraries(kernel ${LEAN_LIBS})

1
src/kernel/environment.cpp
View file

@ -13,7 +13,6 @@ Author: Leonardo de Moura
#include "safe_arith.h"
#include "type_check.h"
#include "exception.h"
#include "pp.h"
#include "debug.h"
namespace lean {

2
src/kernel/expr_formatter.h
View file

@ -15,7 +15,7 @@ class expr_formatter {
public:
virtual ~expr_formatter() {}
/** \brief Convert expression in the given context into a format object. */
virtual format operator()(expr const & e, context const & c) = 0;
virtual format operator()(expr const & e, context const & c = context()) = 0;
/** \brief Return options for pretty printing. */
virtual options get_options() const = 0;

18
src/kernel/object.cpp
View file

@ -6,14 +6,8 @@ Author: Leonardo de Moura
*/
#include "object.h"
#include "environment.h"
#include "pp.h" // TODO: move to front-end
namespace lean {
// TODO: delete hardcoded
format pp_object_kind(char const * n) { return highlight_command(format(n)); }
constexpr unsigned indentation = 2; // TODO: must be option
//
object::~object() {}
void object::display(std::ostream & out, environment const & env) const { out << pp(env); }
@ -41,9 +35,10 @@ bool definition::is_definition() const { return true; }
bool definition::is_opaque() const { return m_opaque; }
expr const & definition::get_value() const { return m_value; }
format definition::pp(environment const & env) const {
return nest(indentation,
format{pp_object_kind(keyword()), format(" "), format(get_name()), format(" : "), ::lean::pp(get_type(), env), format(" :="),
line(), ::lean::pp(get_value()), format(".")});
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));
}
char const * theorem::g_keyword = "Theorem";
@ -57,8 +52,9 @@ bool fact::is_definition() const { return false; }
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 {
return nest(indentation,
format{pp_object_kind(keyword()), format(" "), format(get_name()), format(" : "), ::lean::pp(get_type(), env), format(".")});
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));
}
char const * axiom::g_keyword = "Axiom";

213
src/kernel/pp.cpp
View file

@ -1,213 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "pp.h"
#include "environment.h"
#include "scoped_set.h"
#include "for_each.h"
#include "instantiate.h"
namespace lean {
struct pp_fn {
environment const * m_env;
pp_fn(environment const * env):m_env(env) {}
unsigned indent() const { return 2; }
format pp_keyword(char const * k) { return highlight_keyword(format(k)); }
format pp_type_kwd() { return highlight_builtin(format("Type")); }
format pp_eq_kwd() { return format(" = "); }
format pp_lambda_kwd() { return pp_keyword("\u03BB "); }
format pp_lambda_sep() { return format(","); }
format pp_pi_kwd() { return pp_keyword("\u03A0 "); }
format pp_pi_sep() { return format(","); }
format pp_type_arrow() { return format(" \u2192 "); }
format pp_colon() { return format(" : "); }
format pp_space() { return format(" "); }
format pp_lp() { return format("("); }
format pp_rp() { return format(")"); }
bool is_atomic(expr const & e) {
switch (e.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type:
return true;
case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let:
return false;
}
return false;
}
format pp_var(expr const & e) {
unsigned vidx = var_idx(e);
return compose(format("#"), format(vidx));
}
format pp_constant(expr const & e) {
return ::lean::pp(const_name(e));
}
format pp_value(expr const & e) {
return to_value(e).pp();
}
format pp_type(expr const & e) {
if (e == Type()) {
return pp_type_kwd();
} else {
return format{pp_type_kwd(), pp_space(), ::lean::pp(ty_level(e))};
}
}
format pp_child(expr const & c) {
if (is_atomic(c))
return pp(c);
else
return format{pp_lp(), pp(c), pp_rp()};
}
format pp_eq(expr const & e) {
return format{pp_child(eq_lhs(e)), pp_eq_kwd(), pp_child(eq_rhs(e))};
}
format pp_app(expr const & e) {
// TODO: infix operators, implicit arguments
// Prefix case
format r = pp_child(arg(e, 0));
for (unsigned i = 1; i < num_args(e); i++) {
r += compose(line(), pp_child(arg(e, i)));
}
return group(nest(indent(), r));
}
format pp_arrow_body(expr const & e) {
if (is_atomic(e) || is_arrow(e))
return pp(e);
else
return pp_child(e);
}
struct is_used {};
/** \brief Return true iff \c n is already used in body */
bool used(name const & n, expr const & body) {
auto visitor = [&](expr const & e, unsigned offset) -> void {
if (is_constant(e)) {
if (const_name(e) == n)
throw is_used();
}
};
try {
for_each_fn<decltype(visitor)> f(visitor);
f(body);
return false;
} catch (is_used) {
return true;
}
}
format pp_bname(expr const & binder) {
return ::lean::pp(abst_name(binder));
}
template<typename It>
format pp_bnames(It const & begin, It const & end, bool use_line) {
static_assert(std::is_same<typename std::iterator_traits<It>::value_type, expr>::value,
"pp_bnames takes an argument which is not an iterator containing expr.");
auto it = begin;
format r = pp_bname(*it);
++it;
for (; it != end; ++it) {
r += compose(use_line ? line() : pp_space(), pp_bname(*it));
}
return r;
}
expr collect_nested(expr const & e, expr_kind k, buffer<expr> & r) {
if (e.kind() == k) {
r.push_back(e);
name const & n = abst_name(e);
name n1 = n;
unsigned i = 1;
while (used(n1, abst_body(e))) {
n1 = name(n, i);
i++;
}
expr b = instantiate_with_closed(abst_body(e), mk_constant(n1));
return collect_nested(b, k, r);
} else {
return e;
}
}
format pp_abstraction(expr const & e) {
if (is_arrow(e)) {
return format{pp_child(abst_domain(e)), pp_type_arrow(), pp_arrow_body(abst_body(e))};
} else {
buffer<expr> nested;
expr b = collect_nested(e, e.kind(), nested);
lean_assert(b.kind() != e.kind());
format head = is_lambda(e) ? pp_lambda_kwd() : pp_pi_kwd();
format body_sep = is_lambda(e) ? pp_lambda_sep() : pp_pi_sep();
if (std::all_of(nested.begin(), nested.end(), [&](expr const & a) { return abst_domain(a) == abst_domain(e); })) {
// Domain of all binders is the same
format names = pp_bnames(nested.begin(), nested.end(), false);
return group(nest(indent(), format{head, names, pp_colon(), pp(abst_domain(e)), body_sep, line(), pp(b)}));
} else {
auto it = nested.begin();
auto end = nested.end();
// PP binders in blocks (names ... : type)
bool first = true;
format bindings;
while (it != end) {
auto it2 = it;
++it2;
while (it2 != end && abst_domain(*it2) == abst_domain(*it)) {
++it2;
}
format block = group(nest(indent(), format{pp_lp(), pp_bnames(it, it2, true), pp_colon(), pp(abst_domain(*it)), pp_rp()}));
if (first) {
bindings = block;
first = false;
} else {
bindings += compose(line(), block);
}
it = it2;
}
return group(nest(indent(), format{head, group(bindings), body_sep, line(), pp(b)}));
}
}
}
format pp_let(expr const & e) {
return format("TODO");
}
format pp(expr const & e) {
switch (e.kind()) {
case expr_kind::Var: return pp_var(e);
case expr_kind::Constant: return pp_constant(e);
case expr_kind::Value: return pp_value(e);
case expr_kind::App: return pp_app(e);
case expr_kind::Lambda:
case expr_kind::Pi: return pp_abstraction(e);
case expr_kind::Type: return pp_type(e);
case expr_kind::Eq: return pp_eq(e);
case expr_kind::Let: return pp_let(e);
}
lean_unreachable();
return format();
}
format operator()(expr const & e) {
return pp(e);
}
};
format pp(expr const & n) { return pp_fn(0)(n); }
format pp(expr const & n, environment const & env) { return pp_fn(&env)(n); }
}

34
src/tests/kernel/expr.cpp
View file

@ -15,7 +15,6 @@ Author: Leonardo de Moura
#include "instantiate.h"
#include "deep_copy.h"
#include "arith.h"
#include "pp.h"
using namespace lean;
void tst1() {
@ -39,23 +38,6 @@ void tst1() {
std::cout << mk_pi("x", ty, Var(0)) << "\n";
}
void tst1_pp() {
std::cerr << "=============== PP =====================\n";
expr a;
a = Const("a");
expr f;
f = Var(0);
expr fa = f(a);
expr ty = Type();
std::cout << pp(fa(a)) << "\n";
std::cout << pp(fa(fa, fa)) << "\n";
std::cout << pp(mk_lambda("x", ty, Var(0))) << "\n";
std::cout << pp(mk_pi("x", ty, Var(0))) << "\n";
std::cout << pp(mk_pi("x", ty, mk_lambda("y", ty, Var(0)))) << "\n";
std::cerr << "=============== PP =====================\n";
}
expr mk_dag(unsigned depth, bool _closed = false) {
expr f = Const("f");
expr a = _closed ? Const("a") : Var(0);
@ -214,9 +196,9 @@ void tst5() {
std::cout << "count(r1): " << count(r1) << "\n";
std::cout << "count(r2): " << count(r2) << "\n";
std::cout << "r1 = " << std::endl;
std::cout << pp(r1) << std::endl;
std::cout << r1 << std::endl;
std::cout << "r2 = " << std::endl;
std::cout << pp(r2) << std::endl;
std::cout << r2 << std::endl;
lean_assert(r1 == r2);
}
{
@ -278,10 +260,6 @@ void tst8() {
r = mk_lambda("y", p, mk_app({mk_lambda("x", p, Var(0)), Var(1)}));
lean_assert(!closed(r));
lean_assert(closed(mk_lambda("z", p, r)));
std::cout << pp(mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)}))) << std::endl;
std::cout << pp(mk_pi("x", p, f(f(f(a))))) << std::endl;
}
void tst9() {
@ -371,18 +349,11 @@ void tst15() {
lean_assert(closed(l));
}
void tst16() {
std::cout << pp(Type() >> ((Int >> Int) >> (Int >> Bool))) << "\n";
expr x = Const("x"); expr y = Const("y"); expr f = Const("f");
std::cout << pp(Fun({{x, Int}, {y, Int}, {x, Bool}, {f, Pi({x,Bool}, x)}}, f(x, f(Eq(y,Var(3)), iVal(10))))) << "\n";
}
int main() {
std::cout << "sizeof(expr): " << sizeof(expr) << "\n";
std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n";
std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n";
tst1();
tst1_pp();
tst2();
tst3();
tst4();
@ -397,7 +368,6 @@ int main() {
tst13();
tst14();
tst15();
tst16();
std::cout << "done" << "\n";
return has_violations() ? 1 : 0;
}

4
src/util/sexpr/format.cpp
View file

@ -41,7 +41,7 @@ static name g_pp_colors{"pp", "colors"};
static name g_pp_width{"pp", "width"};
unsigned get_pp_indent(options const & o) {
return o.get_int(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION);
return o.get_unsigned(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION);
}
bool get_pp_colors(options const & o) {
@ -49,7 +49,7 @@ bool get_pp_colors(options const & o) {
}
unsigned get_pp_width(options const & o) {
return o.get_int(g_pp_width, LEAN_DEFAULT_PP_WIDTH);
return o.get_unsigned(g_pp_width, LEAN_DEFAULT_PP_WIDTH);
}
std::ostream & layout(std::ostream & out, bool colors, sexpr const & s) {

10
src/util/sexpr/options.cpp
View file

@ -35,6 +35,11 @@ int options::get_int(name const & n, int default_value) const {
return !is_nil(r) && is_int(r) ? to_int(r) : default_value;
}
unsigned options::get_unsigned(name const & n, unsigned default_value) const {
sexpr const & r = get_sexpr(n);
return !is_nil(r) && is_int(r) ? static_cast<unsigned>(to_int(r)) : default_value;
}
bool options::get_bool(name const & n, bool default_value) const {
sexpr const & r = get_sexpr(n);
return !is_nil(r) && is_bool(r) ? to_bool(r) != 0 : default_value;
@ -60,6 +65,11 @@ int options::get_int(char const * n, int default_value) const {
return !is_nil(r) && is_int(r) ? to_int(r) : default_value;
}
unsigned options::get_unsigned(char const * n, unsigned default_value) const {
sexpr const & r = get_sexpr(n);
return !is_nil(r) && is_int(r) ? static_cast<unsigned>(to_int(r)) : default_value;
}
bool options::get_bool(char const * n, bool default_value) const {
sexpr const & r = get_sexpr(n);
return !is_nil(r) && is_bool(r) ? to_bool(r) != 0 : default_value;

2
src/util/sexpr/options.h
View file

@ -31,12 +31,14 @@ public:
bool get_bool(name const & n, bool default_value=false) const;
int get_int(name const & n, int default_value=0) const;
unsigned get_unsigned(name const & n, unsigned default_value=0) const;
double get_double(name const & n, double default_value=0.0) const;
char const * get_string(name const & n, char const * default_value=nullptr) const;
sexpr get_sexpr(name const & n, sexpr const & default_value=sexpr()) const;
bool get_bool(char const * n, bool default_value=false) const;
int get_int(char const * n, int default_value=0) const;
unsigned get_unsigned(char const * n, unsigned default_value=0) const;
double get_double(char const * n, double default_value=0.0) const;
char const * get_string(char const * n, char const * default_value=nullptr) const;
sexpr get_sexpr(char const * n, sexpr const & default_value=sexpr()) const;