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

Add basic support for hiding implicit arguments when pretty printing.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-26 20:21:05 -07:00
parent fc6cc17925
commit 76c968a5b8
6 changed files with 86 additions and 74 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/frontends/lean/lean_frontend.cpp
View file

@ -17,10 +17,10 @@ Author: Leonardo de Moura
#include "lean_pp.h"
namespace lean {
static std::vector<unsigned> g_empty_vector;
static std::vector<bool> g_empty_vector;
/** \brief Implementation of the Lean frontend */
struct frontend::imp {
typedef std::pair<std::vector<unsigned>, name> implicit_info;
typedef std::pair<std::vector<bool>, name> implicit_info;
// Remark: only named objects are stored in the dictionary.
typedef std::unordered_map<name, operator_info, name_hash, name_eq> operator_table;
typedef std::unordered_map<name, implicit_info, name_hash, name_eq> implicit_table;
@ -167,7 +167,7 @@ struct frontend::imp {
void add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixr(sz, opns, p), d, true); }
void add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixc(sz, opns, p), d, false); }
void mark_implicit_arguments(name const & n, unsigned sz, unsigned * implicit) {
void mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit) {
if (has_children())
throw exception(sstream() << "failed to mark implicit arguments, frontend object is read-only");
object const & obj = m_env.get_object(n);
@ -182,12 +182,9 @@ struct frontend::imp {
unsigned num_args = 0;
expr it = type;
while (is_pi(it)) { num_args++; it = abst_body(it); }
std::vector<unsigned> v;
for (unsigned i = 0; i < sz; i++) {
if (implicit[i] >= num_args)
throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', object has only " << num_args << " arguments, but trying to mark argument " << implicit[i]+1 << " as implicit");
v.push_back(implicit[i]);
}
if (sz > num_args)
throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', object has only " << num_args << " arguments, but trying to mark " << sz << " arguments");
std::vector<bool> v(implicit, implicit+sz);
m_implicit_table[n] = mk_pair(v, explicit_version);
if (obj.is_axiom() || obj.is_theorem()) {
m_env.add_theorem(explicit_version, type, mk_constant(n));
@ -206,7 +203,7 @@ struct frontend::imp {
}
}
std::vector<unsigned> const & get_implicit_arguments(name const & n) {
std::vector<bool> const & get_implicit_arguments(name const & n) {
auto it = m_implicit_table.find(n);
if (it != m_implicit_table.end()) {
return it->second.first;
@ -300,14 +297,10 @@ operator_info frontend::find_op_for(expr const & n) const { return m_imp->find_o
operator_info frontend::find_nud(name const & n) const { return m_imp->find_nud(n); }
operator_info frontend::find_led(name const & n) const { return m_imp->find_led(n); }
void frontend::mark_implicit_arguments(name const & n, unsigned num) {
buffer<unsigned> tmp;
for (unsigned i = 0; i < num; i++) tmp.push_back(i);
mark_implicit_arguments(n, tmp.size(), tmp.data());
}
void frontend::mark_implicit_arguments(name const & n, unsigned sz, unsigned * implicit) { m_imp->mark_implicit_arguments(n, sz, implicit); }
void frontend::mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit) { m_imp->mark_implicit_arguments(n, sz, implicit); }
void frontend::mark_implicit_arguments(name const & n, std::initializer_list<bool> const & l) { mark_implicit_arguments(n, l.size(), l.begin()); }
bool frontend::has_implicit_arguments(name const & n) const { return m_imp->has_implicit_arguments(n); }
std::vector<unsigned> const & frontend::get_implicit_arguments(name const & n) const { return m_imp->get_implicit_arguments(n); }
std::vector<bool> const & frontend::get_implicit_arguments(name const & n) const { return m_imp->get_implicit_arguments(n); }
name const & frontend::get_explicit_version(name const & n) const { return m_imp->get_explicit_version(n); }
state const & frontend::get_state() const { return m_imp->m_state; }

16
src/frontends/lean/lean_frontend.h
View file

@ -119,24 +119,16 @@ public:
/**
@name Implicit arguments.
*/
/**
\brief Mark the first \c num arguments of the definition (or
postulate) named \c n as implicit.
It throws an exception if \c n already has implicit arguments
markups; or if \c n is not a definition or postulate; or if
the number of arguments of \c n is less than \c num.
*/
void mark_implicit_arguments(name const & n, unsigned num);
/**
\brief Mark the given arguments of \c n as implicit.
The array specify the position of the implicit arguments.
The bit-vector array specify the position of the implicit arguments.
*/
void mark_implicit_arguments(name const & n, unsigned sz, unsigned * implicit);
void mark_implicit_arguments(name const & n, unsigned sz, bool const * mask);
void mark_implicit_arguments(name const & n, std::initializer_list<bool> const & l);
/** \brief Return true iff \c n has implicit arguments */
bool has_implicit_arguments(name const & n) const;
/** \brief Return the position of the arguments that are implicit. */
std::vector<unsigned> const & get_implicit_arguments(name const & n) const;
std::vector<bool> const & get_implicit_arguments(name const & n) const;
/**
\brief This frontend associates an definition with each
definition (or postulate) that has implicit arguments. The

36
src/frontends/lean/lean_parser.cpp
View file

@ -522,26 +522,16 @@ class parser::imp {
object_kind k = obj.kind();
if (k == object_kind::Definition || k == object_kind::Postulate) {
if (m_frontend.has_implicit_arguments(obj.get_name())) {
std::vector<unsigned> const & imp_args = m_frontend.get_implicit_arguments(obj.get_name());
unsigned sz = imp_args.size();
lean_assert(sz > 1);
std::vector<bool> const & imp_args = m_frontend.get_implicit_arguments(obj.get_name());
buffer<expr> args;
args.push_back(mk_constant(obj.get_name()));
if (is_imp_arg_prefix(imp_args)) {
for (unsigned i = 0; i < sz; i++) {
args.push_back(save(mk_constant(obj.get_name()), pos()));
// We parse all the arguments to make sure we
// get all explicit arguments.
for (unsigned i = 0; i < imp_args.size(); i++) {
if (imp_args[i]) {
args.push_back(save(mk_metavar(), pos()));
}
} else {
// implicit arguments for id are not just a prefix.
// So, we also parse all explicit arguments
// that occur between implicit arguments.
unsigned last_imp_arg = imp_args[sz-1];
for (unsigned i = 0; i <= last_imp_arg; i++) {
if (std::find(imp_args.begin(), imp_args.end(), i) != imp_args.end()) {
args.push_back(save(mk_metavar(), pos()));
} else {
args.push_back(parse_expr(1));
}
} else {
args.push_back(parse_expr(1));
}
}
return mk_app(args.size(), args.data());
@ -965,12 +955,14 @@ class parser::imp {
is a flag indiciating whether the argument is implicit or not.
*/
void register_implicit_arguments(name const & n, buffer<std::tuple<pos_info, name, expr,bool>> & bindings) {
buffer<unsigned> imp_args;
bool found = false;
buffer<bool> imp_args;
for (unsigned i = 0; i < bindings.size(); i++) {
if (std::get<3>(bindings[i]))
imp_args.push_back(i);
imp_args.push_back(std::get<3>(bindings[i]));
if (imp_args.back())
found = true;
}
if (!imp_args.empty())
if (found)
m_frontend.mark_implicit_arguments(n, imp_args.size(), imp_args.data());
}

65
src/frontends/lean/lean_pp.cpp
View file

@ -178,10 +178,13 @@ class pp_fn {
}
result pp_constant(expr const & e) {
name const & n = const_name(e);
if (is_metavar(e)) {
return mk_result(format("_"), 1);
} else if (m_frontend.has_implicit_arguments(n)) {
return mk_result(format(m_frontend.get_explicit_version(n)), 1);
} else {
return mk_result(::lean::pp(const_name(e)), 1);
return mk_result(format(n), 1);
}
}
@ -478,15 +481,47 @@ class pp_fn {
return pp_exists(e, depth);
} else {
// standard function application
result p = pp_child(arg(e, 0), depth);
bool simple = is_constant(arg(e, 0)) && const_name(arg(e, 0)).size() <= m_indent + 4;
unsigned indent = simple ? const_name(arg(e, 0)).size()+1 : m_indent;
format r_format = p.first;
unsigned r_weight = p.second;
expr f = arg(e, 0);
std::vector<bool> const * implicit_args = nullptr;
format r_format;
unsigned r_weight;
bool simple = false;
unsigned indent = m_indent;
if (is_constant(f)) {
name const & n = const_name(f);
simple = const_name(f).size() <= m_indent + 4;
indent = simple ? const_name(f).size()+1 : m_indent;
if (m_frontend.has_implicit_arguments(n)) {
implicit_args = &(m_frontend.get_implicit_arguments(n));
lean_assert(implicit_args->size() != 0);
if (m_implict || num_args(e) - 1 < implicit_args->size()) {
// If implicit arguments should be displayed, or
// If we do not have enough arguments, then
// we use the explicit representation
implicit_args = nullptr;
// we should use the explicit version of the
// definition, since we are not hiding implicit arguments
r_format = format(m_frontend.get_explicit_version(n));
simple = false;
indent = m_indent;
} else {
r_format = format(n);
}
} else {
r_format = format(n);
}
r_weight = 1;
} else {
result p = pp_child(f, depth);
r_format = p.first;
r_weight = p.second;
}
for (unsigned i = 1; i < num_args(e); i++) {
result p_arg = pp_child(arg(e, i), depth);
r_format += format{i == 1 && simple ? space() : line(), p_arg.first};
r_weight += p_arg.second;
if (!is_implicit(implicit_args, i-1)) {
result p_arg = pp_child(arg(e, i), depth);
r_format += format{i == 1 && simple ? space() : line(), p_arg.first};
r_weight += p_arg.second;
}
}
return mk_result(group(nest(indent, r_format)), r_weight);
}
@ -562,8 +597,8 @@ class pp_fn {
return r;
}
bool is_implicit(std::vector<unsigned> const * implicit_args, unsigned arg_pos) {
return implicit_args && std::find(implicit_args->begin(), implicit_args->end(), arg_pos) != implicit_args->end();
bool is_implicit(std::vector<bool> const * implicit_args, unsigned arg_pos) {
return implicit_args && (*implicit_args)[arg_pos];
}
/**
@ -583,7 +618,7 @@ class pp_fn {
\remark if T != 0, then T is Pi(x : A), B
*/
result pp_abstraction_core(expr const & e, unsigned depth, expr T, std::vector<unsigned> const * implicit_args = nullptr) {
result pp_abstraction_core(expr const & e, unsigned depth, expr T, std::vector<bool> const * implicit_args = nullptr) {
if (is_arrow(e) && !implicit_args) {
lean_assert(!T);
result p_lhs = pp_child(abst_domain(e), depth);
@ -822,13 +857,13 @@ public:
return pp_scoped_child(e, 0).first;
}
format pp_definition(expr const & v, expr const & t, std::vector<unsigned> const * implicit_args) {
format pp_definition(expr const & v, expr const & t, std::vector<bool> const * implicit_args) {
init(mk_app(v, t));
expr T(t);
return pp_abstraction_core(v, 0, T, implicit_args).first;
}
format pp_pi_with_implicit_args(expr const & e, std::vector<unsigned> const & implicit_args) {
format pp_pi_with_implicit_args(expr const & e, std::vector<bool> const & implicit_args) {
init(e);
return pp_abstraction_core(e, 0, expr(), &implicit_args).first;
}
@ -901,7 +936,7 @@ class pp_formatter_cell : public formatter_cell {
return pp_definition(kwd, n, t, v, opts);
} else {
lean_assert(is_lambda(v));
std::vector<unsigned> const * implicit_args = nullptr;
std::vector<bool> const * implicit_args = nullptr;
if (m_frontend.has_implicit_arguments(n))
implicit_args = &(m_frontend.get_implicit_arguments(n));
pp_fn fn(m_frontend, opts);

2
src/shell/lean.cpp
View file

@ -31,7 +31,7 @@ int main(int argc, char ** argv) {
frontend f;
for (int i = 1; i < argc; i++) {
std::ifstream in(argv[i]);
parser p(f, in);
parser p(f, in, false, false);
if (!p())
ok = false;
}

14
src/tests/frontends/lean/lean_frontend.cpp
View file

@ -168,22 +168,22 @@ static void tst11() {
frontend f;
expr A = Const("A");
f.add_var("g", Pi({A, Type()}, A >> (A >> A)));
lean_assert(!f.has_implicit_arguments("g"))
f.mark_implicit_arguments("g", 1);
lean_assert(!f.has_implicit_arguments("g"));
f.mark_implicit_arguments("g", {true, false, false});
lean_assert(f.has_implicit_arguments("g"))
name gexp = f.get_explicit_version("g");
lean_assert(f.find_object(gexp));
lean_assert(f.find_object("g").get_type() == f.find_object(gexp).get_type());
lean_assert(f.get_implicit_arguments("g") == std::vector<unsigned>{0});
lean_assert(f.get_implicit_arguments("g") == std::vector<bool>({true, false, false}));
try {
f.mark_implicit_arguments("g", 1);
f.mark_implicit_arguments("g", {true, false, false});
lean_unreachable();
} catch (exception & ex) {
std::cout << "Expected error: " << ex.what() << std::endl;
}
f.add_var("s", Pi({A, Type()}, A >> (A >> A)));
try {
f.mark_implicit_arguments("s", 4);
f.mark_implicit_arguments("s", {true, true, true, true});
lean_unreachable();
} catch (exception & ex) {
std::cout << "Expected error: " << ex.what() << std::endl;
@ -191,13 +191,13 @@ static void tst11() {
f.add_var(name{"h","explicit"}, Pi({A, Type()}, A >> (A >> A)));
f.add_var("h", Pi({A, Type()}, A >> (A >> A)));
try {
f.mark_implicit_arguments("h", 1);
f.mark_implicit_arguments("h", {true, false, false});
lean_unreachable();
} catch (exception & ex) {
std::cout << "Expected error: " << ex.what() << std::endl;
}
try {
f.mark_implicit_arguments("u", 1);
f.mark_implicit_arguments("u", {true, false});
lean_unreachable();
} catch (exception & ex) {
std::cout << "Expected error: " << ex.what() << std::endl;