From a85a6b685bbf819481b7fb38ec93e01ac8e9492d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 May 2014 12:30:03 -0700 Subject: [PATCH] feat(kernel/formatter): add binding_body_fresh, let_body_fresh, and simplify formatter Signed-off-by: Leonardo de Moura --- src/kernel/formatter.cpp | 125 +++++++++++++++++++++++++-------------- src/kernel/formatter.h | 13 ++++ tests/lua/expr7.lua | 10 ++++ 3 files changed, 103 insertions(+), 45 deletions(-) create mode 100644 tests/lua/expr7.lua diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index d2f57f9b3..78546c14d 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -4,14 +4,44 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "kernel/formatter.h" -#include "kernel/context.h" #include "kernel/environment.h" +#include "kernel/find_fn.h" +#include "kernel/instantiate.h" +#include "kernel/free_vars.h" namespace lean { -name pick_unused_name(expr const &, name const & s) { - // TODO(Leo) - return s; +bool is_used_name(expr const & t, name const & n) { + return static_cast( + find(t, [&](expr const & e, unsigned) { + return (is_constant(e) && const_name(e) == n) // t has a constant named n + || (is_local(e) && (mlocal_name(e) == n || local_pp_name(e) == n)); // t has a local constant named n + })); +} + +name pick_unused_name(expr const & t, name const & s) { + name r = s; + unsigned i = 1; + while (is_used_name(t, r)) { + r = name(s, i); + i++; + } + return r; +} + +std::pair binding_body_fresh(expr const & b, bool preserve_type) { + lean_assert(is_binding(b)); + name n = pick_unused_name(binding_body(b), binding_name(b)); + expr c = mk_local(n, n, preserve_type ? binding_domain(b) : expr()); + return mk_pair(instantiate(binding_body(b), c), c); +} + +std::pair let_body_fresh(expr const & l, bool preserve_type) { + lean_assert(is_let(l)); + name n = pick_unused_name(let_body(l), let_name(l)); + expr c = mk_local(n, n, preserve_type ? let_type(l) : expr()); + return mk_pair(instantiate(let_body(l), c), c); } /** @@ -28,18 +58,18 @@ struct print_expr_fn { return ::lean::is_atomic(a) || is_mlocal(a); } - void print_child(expr const & a, context const & c) { + void print_child(expr const & a) { if (is_atomic(a)) { - print(a, c); + print(a); } else { - out() << "("; print(a, c); out() << ")"; + out() << "("; print(a); out() << ")"; } } - void print_macro(expr const & a, context const & c) { + void print_macro(expr const & a) { macro_def(a).display(out()); for (unsigned i = 0; i < macro_num_args(a); i++) { - out() << " "; print_child(macro_arg(a, i), c); + out() << " "; print_child(macro_arg(a, i)); } } @@ -56,37 +86,53 @@ struct print_expr_fn { } } - void print_app(expr const & e, context const & c) { + void print_app(expr const & e) { expr const & f = app_fn(e); if (is_app(f)) - print(f, c); + print(f); else - print_child(f, c); + print_child(f); out() << " "; - print_child(app_arg(e), c); + print_child(app_arg(e)); } - void print_arrow_body(expr const & a, context const & c) { + void print_arrow_body(expr const & a) { if (is_atomic(a) || is_arrow(a)) - return print(a, c); + return print(a); else - return print_child(a, c); + return print_child(a); } - void print_binding(char const * bname, expr const & e, context const & c) { + void print_let(expr const & a) { + auto p = let_body_fresh(a); + expr const & b = p.first; + expr const & n = p.second; + out() << "let " << n; + out() << " : "; + print(let_type(a)); + out() << " := "; + print(let_value(a)); + out() << " in "; + print_child(b); + } + + void print_binding(char const * bname, expr const & e) { + auto p = binding_body_fresh(e); + expr const & b = p.first; + expr const & n = p.second; out() << bname << " "; if (binding_info(e).is_implicit()) out() << "{"; else if (binding_info(e).is_cast()) out() << "["; - out() << binding_name(e) << " : "; - print_child(binding_domain(e), c); + out() << n << " : "; + print_child(binding_domain(e)); if (binding_info(e).is_implicit()) out() << "}"; else if (binding_info(e).is_cast()) out() << "]"; out() << ", "; - print_child(binding_body(e), extend(c, binding_name(e), binding_domain(e))); + print_child(b); } void print_const(expr const & a) { @@ -103,7 +149,7 @@ struct print_expr_fn { } } - void print(expr const & a, context const & c) { + void print(expr const & a) { switch (a.kind()) { case expr_kind::Meta: out() << "?" << mlocal_name(a); @@ -111,60 +157,49 @@ struct print_expr_fn { case expr_kind::Local: out() << local_pp_name(a); break; - case expr_kind::Var: { - auto e = find(c, var_idx(a)); - if (e) - out() << e->get_name() << "#" << var_idx(a); - else - out() << "#" << var_idx(a); + case expr_kind::Var: + out() << "#" << var_idx(a); break; - } case expr_kind::Constant: print_const(a); break; case expr_kind::App: - print_app(a, c); + print_app(a); break; case expr_kind::Lambda: - print_binding("fun", a, c); + print_binding("fun", a); break; case expr_kind::Pi: if (!is_arrow(a)) { - print_binding("Pi", a, c); + print_binding("Pi", a); } else { - print_child(binding_domain(a), c); + print_child(binding_domain(a)); out() << " -> "; - print_arrow_body(binding_body(a), extend(c, binding_binder(a))); + print_arrow_body(lower_free_vars(binding_body(a), 1)); } break; case expr_kind::Let: - out() << "let " << let_name(a); - out() << " : "; - print(let_type(a), c); - out() << " := "; - print(let_value(a), c); - out() << " in "; - print_child(let_body(a), extend(c, let_name(a), let_value(a))); + print_let(a); break; case expr_kind::Sort: print_sort(a); break; case expr_kind::Macro: - print_macro(a, c); + print_macro(a); break; } } print_expr_fn(std::ostream & out, bool type0_as_bool = true):m_out(out), m_type0_as_bool(type0_as_bool) {} - void operator()(expr const & e, context const & c) { - print(e, c); + void operator()(expr const & e) { + print(e); } }; std::ostream & operator<<(std::ostream & out, expr const & e) { print_expr_fn pr(out); - pr(e, context()); + pr(e); return out; } @@ -173,7 +208,7 @@ public: virtual format operator()(environment const & env, expr const & e, options const &) { std::ostringstream s; print_expr_fn pr(s, env.prop_proof_irrel()); - pr(e, context()); + pr(e); return format(s.str()); } }; diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h index a6e2747be..da5b048e6 100644 --- a/src/kernel/formatter.h +++ b/src/kernel/formatter.h @@ -6,10 +6,23 @@ Author: Leonardo de Moura */ #pragma once #include +#include #include "util/sexpr/options.h" #include "kernel/expr.h" namespace lean { +/** + \brief Return the body of the binding \c b, where variable #0 is replaced by a local constant with a "fresh" name. + The name is considered fresh if it is not used by a constant or local constant occuring in the body of \c b. + The fresh constant is also returned (second return value). + + \remark If preserve_type is false, then the local constant will not use binding_domain. +*/ +std::pair binding_body_fresh(expr const & b, bool preserve_type = false); + +/** \brief Return the body of the let-expression \c l, where variable #0 is replaced by a local constant with a "fresh" name. */ +std::pair let_body_fresh(expr const & l, bool preserve_type = false); + /** \brief API for formatting expressions */ diff --git a/tests/lua/expr7.lua b/tests/lua/expr7.lua new file mode 100644 index 000000000..4f9ea9966 --- /dev/null +++ b/tests/lua/expr7.lua @@ -0,0 +1,10 @@ +local a = Const("a") +local A = Const("A") +local vec = Const("vec") +local T = Const("T") +print(Pi({{A, Type}, {a, A}, {A, vec(A)}, {a, A}}, a)) +local t = mk_pi("A", Type, mk_pi("a", Var(0), mk_pi("A", vec(Var(1)), mk_pi("a", Var(0), T(Var(0), Var(2)))))) +print(t) +print(Let(A, Type, Bool, Pi(a, A, Let(A, Type, A, Pi(a, A, a))))) +print(mk_let("A", Type, Bool, mk_pi("a", Var(0), mk_let("A", Type, Var(1), mk_pi("a", Var(0), T(Var(0), Var(1), Var(2))))))) +print(mk_let("A", Type, Bool, mk_pi("a", Var(0), mk_let("A", Type, Var(1), mk_pi("a", Var(0), T(Var(0), Var(1), Var(2), Var(3)))))))