From 8cf65f354b9a4a4a425742e1dbc698d0a9d16bb9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Dec 2013 12:50:41 -0800 Subject: [PATCH] fix(frontends/lean/pp): forall and exists pretty printing when used as constants Signed-off-by: Leonardo de Moura --- src/frontends/lean/pp.cpp | 11 +++++++++-- src/kernel/builtin.cpp | 6 ++++++ src/kernel/builtin.h | 4 ++++ 3 files changed, 19 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index bedad0c7f..dac5ee049 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -242,6 +242,12 @@ class pp_fn { name const & n = const_name(e); if (is_placeholder(e)) { 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)) { return mk_result(format(get_explicit_version(m_env, n)), 1); } else { @@ -704,7 +710,8 @@ class pp_fn { // standard function application expr const & f = app.get_function(); 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); else if (is_choice(f)) p = pp_child(f, depth); @@ -712,7 +719,7 @@ class pp_fn { p = mk_result(to_value(f).pp(m_unicode, m_coercion), 1); else 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; format r_format = p.first; unsigned r_weight = p.second; diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 664094de8..b161ac198 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -180,6 +180,9 @@ bool is_not(expr const & e, expr & a) { } MK_CONSTANT(forall_fn, name("forall")); 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")); bool is_homo_eq(expr const & e, expr & lhs, expr & rhs) { 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)))); // 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))))))); + // 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 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))); diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h index e58fc6533..2458bd761 100644 --- a/src/kernel/builtin.h +++ b/src/kernel/builtin.h @@ -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 */ 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); } +/** \brief Return alias \c Forall for \c forall */ +expr mk_Forall_fn(); /** \brief Return the Lean exists operator. It has type: Pi (A : Type), (A -> Bool) -> Bool */ 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 */ 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); } +/** \brief Return alias \c Exists for \c exists */ +expr mk_Exists_fn(); /** \brief Homogeneous equality. It has type: Pi (A : Type), A -> A -> Bool */ expr mk_homo_eq_fn();