fix(frontends/lean/pp): forall and exists pretty printing when used as constants

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-27 12:50:41 -08:00
parent a02c6e70fa
commit 8cf65f354b
3 changed files with 19 additions and 2 deletions

View file

@ -242,6 +242,12 @@ class pp_fn {
name const & n = const_name(e); name const & n = const_name(e);
if (is_placeholder(e)) { if (is_placeholder(e)) {
return mk_result(format("_"), 1); return mk_result(format("_"), 1);
} else if (is_forall_fn(e)) {
// use alias when forall is used as a function symbol
return mk_result(format(const_name(mk_Forall_fn())), 1);
} else if (is_exists_fn(e)) {
// use alias when exists is used as a function symbol
return mk_result(format(const_name(mk_Exists_fn())), 1);
} else if (has_implicit_arguments(n)) { } else if (has_implicit_arguments(n)) {
return mk_result(format(get_explicit_version(m_env, n)), 1); return mk_result(format(get_explicit_version(m_env, n)), 1);
} else { } else {
@ -704,7 +710,8 @@ class pp_fn {
// standard function application // standard function application
expr const & f = app.get_function(); expr const & f = app.get_function();
result p; result p;
if (is_constant(f)) bool is_const = is_constant(f) && !is_forall_fn(f) && !is_exists_fn(f);
if (is_const)
p = mk_result(format(const_name(f)), 1); p = mk_result(format(const_name(f)), 1);
else if (is_choice(f)) else if (is_choice(f))
p = pp_child(f, depth); p = pp_child(f, depth);
@ -712,7 +719,7 @@ class pp_fn {
p = mk_result(to_value(f).pp(m_unicode, m_coercion), 1); p = mk_result(to_value(f).pp(m_unicode, m_coercion), 1);
else else
p = pp_child(f, depth); p = pp_child(f, depth);
bool simple = is_constant(f) && const_name(f).size() <= m_indent + 4; bool simple = is_const && const_name(f).size() <= m_indent + 4;
unsigned indent = simple ? const_name(f).size()+1 : m_indent; unsigned indent = simple ? const_name(f).size()+1 : m_indent;
format r_format = p.first; format r_format = p.first;
unsigned r_weight = p.second; unsigned r_weight = p.second;

View file

@ -180,6 +180,9 @@ bool is_not(expr const & e, expr & a) {
} }
MK_CONSTANT(forall_fn, name("forall")); MK_CONSTANT(forall_fn, name("forall"));
MK_CONSTANT(exists_fn, name("exists")); MK_CONSTANT(exists_fn, name("exists"));
MK_CONSTANT(Forall_fn, name("Forall"));
MK_CONSTANT(Exists_fn, name("Exists"));
MK_CONSTANT(homo_eq_fn, name("eq")); MK_CONSTANT(homo_eq_fn, name("eq"));
bool is_homo_eq(expr const & e, expr & lhs, expr & rhs) { bool is_homo_eq(expr const & e, expr & lhs, expr & rhs) {
if (is_homo_eq(e)) { if (is_homo_eq(e)) {
@ -255,6 +258,9 @@ void import_basic(environment const & env) {
env->add_opaque_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True)))); env->add_opaque_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
// TODO(Leo): introduce epsilon // TODO(Leo): introduce epsilon
env->add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x))))))); env->add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
// Aliases for forall and exists
env->add_definition(Forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Forall(A, P)));
env->add_definition(Exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Exists(A, P)));
// homogeneous equality // homogeneous equality
env->add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y))); env->add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y)));

View file

@ -121,6 +121,8 @@ inline bool is_forall(expr const & e) { return is_app(e) && is_forall_fn(arg(e,
/** \brief Return the term (Forall A P), where A is a type and P : A -> bool */ /** \brief Return the term (Forall A P), where A is a type and P : A -> bool */
inline expr mk_forall(expr const & A, expr const & P) { return mk_app(mk_forall_fn(), A, P); } inline expr mk_forall(expr const & A, expr const & P) { return mk_app(mk_forall_fn(), A, P); }
inline expr Forall(expr const & A, expr const & P) { return mk_forall(A, P); } inline expr Forall(expr const & A, expr const & P) { return mk_forall(A, P); }
/** \brief Return alias \c Forall for \c forall */
expr mk_Forall_fn();
/** \brief Return the Lean exists operator. It has type: <tt>Pi (A : Type), (A -> Bool) -> Bool</tt> */ /** \brief Return the Lean exists operator. It has type: <tt>Pi (A : Type), (A -> Bool) -> Bool</tt> */
expr mk_exists_fn(); expr mk_exists_fn();
@ -129,6 +131,8 @@ inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e,
/** \brief Return the term (exists A P), where A is a type and P : A -> bool */ /** \brief Return the term (exists A P), where A is a type and P : A -> bool */
inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); } inline expr mk_exists(expr const & A, expr const & P) { return mk_app(mk_exists_fn(), A, P); }
inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); } inline expr Exists(expr const & A, expr const & P) { return mk_exists(A, P); }
/** \brief Return alias \c Exists for \c exists */
expr mk_Exists_fn();
/** \brief Homogeneous equality. It has type: <tt>Pi (A : Type), A -> A -> Bool</tt> */ /** \brief Homogeneous equality. It has type: <tt>Pi (A : Type), A -> A -> Bool</tt> */
expr mk_homo_eq_fn(); expr mk_homo_eq_fn();