From d17990ed7869d9084e44a8c0d4c13adbbd0cc301 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Feb 2014 16:10:11 -0800 Subject: [PATCH] refactor(kernel): add formatter and simplify contexts Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 2 +- src/kernel/context.cpp | 78 ++---------------- src/kernel/context.h | 93 +--------------------- src/kernel/expr.cpp | 23 ++++-- src/kernel/expr.h | 4 + src/kernel/formatter.cpp | 161 ++++++++++++++++++++++++++++++++++++++ src/kernel/formatter.h | 26 +++--- src/kernel/replace_fn.cpp | 10 --- src/kernel/replace_fn.h | 1 - 9 files changed, 203 insertions(+), 195 deletions(-) create mode 100644 src/kernel/formatter.cpp diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index af7bf3063..361b617b2 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp -instantiate.cpp +instantiate.cpp context.cpp formatter.cpp # normalizer.cpp context.cpp level.cpp object.cpp environment.cpp # type_checker.cpp kernel.cpp occurs.cpp metavar.cpp # justification.cpp unification_constraint.cpp kernel_exception.cpp diff --git a/src/kernel/context.cpp b/src/kernel/context.cpp index d8bd64aa2..34d4d65e8 100644 --- a/src/kernel/context.cpp +++ b/src/kernel/context.cpp @@ -7,84 +7,16 @@ Author: Leonardo de Moura #include #include "util/exception.h" #include "kernel/context.h" -#include "kernel/metavar.h" -#include "kernel/free_vars.h" namespace lean { -context::context(std::initializer_list> const & l) { - for (auto const & p : l) - m_list = cons(context_entry(name(p.first), p.second), m_list); -} - -std::pair context::lookup_ext(unsigned i) const { - list const * it1 = &m_list; - while (*it1) { +std::pair const & lookup(context const & c, unsigned i) { + auto const * it = &c; + while (*it) { if (i == 0) - return std::pair(head(*it1), context(tail(*it1))); + return head(*it); --i; - it1 = &tail(*it1); + it = &tail(*it); } throw exception("unknown free variable"); } - -context_entry const & context::lookup(unsigned i) const { - list const * it1 = &m_list; - while (*it1) { - if (i == 0) - return head(*it1); - --i; - it1 = &tail(*it1); - } - throw exception("unknown free variable"); -} - -optional context::find(unsigned i) const { - list const * it1 = &m_list; - while (*it1) { - if (i == 0) - return some(head(*it1)); - --i; - it1 = &tail(*it1); - } - return optional(); -} - -list truncate_core(list const & l, unsigned s) { - if (s == 0) { - return list(); - } else { - return cons(head(l), truncate_core(tail(l), s-1)); - } -} - -context context::truncate(unsigned s) const { - return context(truncate_core(m_list, s)); -} - -struct remove_no_applicable {}; -static list remove_core(list const & l, unsigned s, unsigned n, metavar_env const & menv) { - if (l) { - if (s == 0) { - if (n > 0) { - return remove_core(tail(l), 0, n-1, menv); - } else { - return l; - } - } else { - if (has_free_var(head(l), s-1, s+n-1, menv)) - throw remove_no_applicable(); - return cons(lower_free_vars(head(l), s+n-1, n, menv), remove_core(tail(l), s-1, n, menv)); - } - } else { - return l; - } -} - -optional context::remove(unsigned s, unsigned n, metavar_env const & menv) const { - try { - return some(context(remove_core(m_list, s, n, menv))); - } catch (remove_no_applicable&) { - return optional(); - } -} } diff --git a/src/kernel/context.h b/src/kernel/context.h index 156970033..0366fbb90 100644 --- a/src/kernel/context.h +++ b/src/kernel/context.h @@ -11,93 +11,8 @@ Author: Leonardo de Moura #include "kernel/expr.h" namespace lean { -/** - \brief An element of the Lean context. - \see context -*/ -class context_entry { - name m_name; - optional m_domain; - optional m_body; -public: - context_entry(name const & n, optional const & d, expr const & b):m_name(n), m_domain(d), m_body(b) {} - context_entry(name const & n, expr const & d, optional const & b):m_name(n), m_domain(d), m_body(b) {} - context_entry(name const & n, expr const & d, expr const & b):m_name(n), m_domain(d), m_body(b) {} - context_entry(name const & n, expr const & d):m_name(n), m_domain(d) {} - name const & get_name() const { return m_name; } - optional const & get_domain() const { return m_domain; } - optional const & get_body() const { return m_body; } - friend bool operator==(context_entry const & e1, context_entry const & e2) { return e1.m_domain == e2.m_domain && e1.m_body == e2.m_body; } - friend bool operator!=(context_entry const & e1, context_entry const & e2) { return !(e1 == e2); } -}; - -class metavar_env; - -/** - \brief A context is essentially a mapping from free-variables to types (and definition/body). -*/ -class context { - list m_list; - explicit context(list const & l):m_list(l) {} -public: - context() {} - context(context const & c, name const & n, optional const & d, expr const & b):m_list(context_entry(n, d, b), c.m_list) {} - context(context const & c, name const & n, expr const & d, optional const & b):m_list(context_entry(n, d, b), c.m_list) {} - context(context const & c, name const & n, expr const & d, expr const & b):m_list(context_entry(n, d, b), c.m_list) {} - context(context const & c, name const & n, expr const & d):m_list(context_entry(n, d), c.m_list) {} - context(context const & c, context_entry const & e):m_list(e, c.m_list) {} - context(unsigned sz, context_entry const * es):context(to_list(es, es + sz)) {} - context(std::initializer_list> const & l); - context_entry const & lookup(unsigned vidx) const; - std::pair lookup_ext(unsigned vidx) const; - /** \brief Similar to lookup, but always succeed */ - optional find(unsigned vidx) const; - bool empty() const { return is_nil(m_list); } - explicit operator bool() const { return !empty(); } - unsigned size() const { return length(m_list); } - typedef list::iterator iterator; - iterator begin() const { return m_list.begin(); } - iterator end() const { return m_list.end(); } - friend bool is_eqp(context const & c1, context const & c2) { return is_eqp(c1.m_list, c2.m_list); } - /** - \brief Return a new context where entries at positions >= s are removed. - */ - context truncate(unsigned s) const; - /** - \brief Return a new context where the entries at positions [s, s+n) were removed. - - The free variables in entries [0, s) are lowered. - That is, if this context is of the form - [ce_m, ..., ce_{s+n}, ce_{s+n-1}, ..., ce_s, ce_{s-1}, ..., ce_0] - Then, the resultant context is of the form - [ce_m, ..., ce_{s+n}, lower(ce_{s-1}, n, n), ..., lower(ce_0, s+n-1, n)] - - \pre size() >= s + n - - If for some i in [0, s), has_free_var(ce_i, s - 1 - i, s + n - 1 - i), then return none. - That is, the lower operations must be valid. - */ - optional remove(unsigned s, unsigned n, metavar_env const & menv) const; - friend bool operator==(context const & ctx1, context const & ctx2) { return ctx1.m_list == ctx2.m_list; } - friend bool operator!=(context const & ctx1, context const & ctx2) { return !(ctx1 == ctx2); } -}; - -/** - \brief Return the context entry for the free variable with de - Bruijn index \c i, and the context for this entry. -*/ -inline std::pair lookup_ext(context const & c, unsigned i) { return c.lookup_ext(i); } -/** - \brief Return the context entry for the free variable with de - Bruijn index \c i. -*/ -inline context_entry const & lookup(context const & c, unsigned i) { return c.lookup(i); } -inline optional find(context const & c, unsigned i) { return c.find(i); } -inline context extend(context const & c, name const & n, optional const & d, expr const & b) { return context(c, n, d, b); } -inline context extend(context const & c, name const & n, expr const & d, optional const & b) { return context(c, n, d, b); } -inline context extend(context const & c, name const & n, expr const & d, expr const & b) { return context(c, n, d, b); } -inline context extend(context const & c, name const & n, expr const & d) { return context(c, n, d); } -inline bool empty(context const & c) { return c.empty(); } - -std::ostream & operator<<(std::ostream & out, context const & ctx); +typedef list> context; +inline context extend(context const & c, name const & n, expr const & t) { return cons(mk_pair(n, t), c); } +std::pair const & lookup(context const & c, unsigned i); +optional> find(context const & c, unsigned i); } diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 434a49bf4..57c6e9896 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -15,8 +15,7 @@ Author: Leonardo de Moura #include "util/object_serializer.h" #include "kernel/expr.h" #include "kernel/expr_eq_fn.h" -// #include "kernel/free_vars.h" -// #include "kernel/metavar.h" +#include "kernel/free_vars.h" // #include "kernel/max_sharing.h" namespace lean { @@ -336,24 +335,36 @@ expr update_mlocal(expr const & e, expr const & new_type) { return e; } -#if 0 +bool is_atomic(expr const & e) { + switch (e.kind()) { + case expr_kind::Constant: case expr_kind::Sort: + case expr_kind::Macro: case expr_kind::Var: + return true; + case expr_kind::App: case expr_kind::Let: + case expr_kind::Meta: case expr_kind::Local: + case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: + case expr_kind::Pair: case expr_kind::Fst: case expr_kind::Snd: + return false; + } + lean_unreachable(); // LCOV_EXCL_LINE +} bool is_arrow(expr const & t) { optional r = t.raw()->is_arrow(); if (r) { return *r; } else { - bool res = is_pi(t) && !has_free_var(abst_body(t), 0); + bool res = is_pi(t) && !has_free_var(binder_body(t), 0); t.raw()->set_is_arrow(res); return res; } } bool is_cartesian(expr const & t) { - return is_sigma(t) && !has_free_var(abst_body(t), 0); + return is_sigma(t) && !has_free_var(binder_body(t), 0); } - +#if 0 expr copy(expr const & a) { switch (a.kind()) { case expr_kind::Var: return mk_var(var_idx(a)); diff --git a/src/kernel/expr.h b/src/kernel/expr.h index d1dbb1c1e..19555b90a 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -359,6 +359,10 @@ inline bool is_let(expr const & e) { return e.kind() == expr_kind::Let; } inline bool is_binder(expr const & e) { return is_lambda(e) || is_pi(e) || is_sigma(e); } inline bool is_proj(expr const & e) { return is_fst(e) || is_snd(e); } inline bool is_mlocal(expr const & e) { return is_metavar(e) || is_local(e); } + +bool is_atomic(expr const & e); +bool is_arrow(expr const & t); +bool is_cartesian(expr const & t); // ======================================= // ======================================= diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp new file mode 100644 index 000000000..a82ed556e --- /dev/null +++ b/src/kernel/formatter.cpp @@ -0,0 +1,161 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/formatter.h" +#include "kernel/context.h" + +namespace lean { +/** + \brief Very basic printer for expressions. + It is mainly used when debugging code. +*/ +struct print_expr_fn { + std::ostream & m_out; + + std::ostream & out() { return m_out; } + + bool is_atomic(expr const & a) { + return ::lean::is_atomic(a) || is_mlocal(a); + } + + void print_child(expr const & a, context const & c) { + if (is_atomic(a)) { + print(a, c); + } else { + out() << "("; print(a, c); out() << ")"; + } + } + + void print_macro(expr const & a) { + to_macro(a).display(out()); + } + + void print_sort(expr const & a) { + if (is_zero(sort_level(a))) { + out () << "Bool"; + } else { + out() << "(Type " << sort_level(a) << ")"; + } + } + + void print_app(expr const & e, context const & c) { + expr const & f = app_fn(e); + if (is_app(f)) + print(f, c); + else + print_child(f, c); + out() << " "; + print_child(app_arg(e), c); + } + + void print_arrow_body(expr const & a, context const & c) { + if (is_atomic(a) || is_arrow(a)) + return print(a, c); + else + return print_child(a, c); + } + + void print_pair(expr const & e, context const & c) { + out() << "pair "; + print_child(pair_first(e), c); + out() << " "; + print_child(pair_second(e), c); + out() << " "; + print_child(pair_type(e), c); + } + + void print_binder(char const * bname, expr const & e, context const & c) { + out() << bname << " " << binder_name(e) << " : "; + print_child(binder_domain(e), c); + out() << ", "; + print_child(binder_body(e), extend(c, binder_name(e), binder_domain(e))); + } + + void print(expr const & a, context const & c) { + switch (a.kind()) { + case expr_kind::Meta: case expr_kind::Local: + out() << mlocal_name(a); + break; + case expr_kind::Var: { + auto e = find(c, var_idx(a)); + if (e) + out() << e->first << "#" << var_idx(a); + else + out() << "#" << var_idx(a); + break; + } + case expr_kind::Constant: + out() << const_name(a); + break; + case expr_kind::App: + print_app(a, c); + break; + case expr_kind::Pair: + print_pair(a, c); + break; + case expr_kind::Fst: case expr_kind::Snd: + out() << (is_fst(a) ? "fst" : "snd") << " "; + print_child(proj_arg(a), c); + break; + case expr_kind::Sigma: + print_binder("sig", a, c); + break; + case expr_kind::Lambda: + print_binder("fun", a, c); + break; + case expr_kind::Pi: + if (!is_arrow(a)) { + print_binder("Pi", a, c); + } else { + print_child(binder_domain(a), c); + out() << " -> "; + print_arrow_body(binder_body(a), extend(c, binder_name(a), binder_domain(a))); + } + break; + case expr_kind::Let: + out() << "let " << let_name(a); + if (let_type(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))); + break; + case expr_kind::Sort: + print_sort(a); + break; + case expr_kind::Macro: + print_macro(a); + break; + } + } + + print_expr_fn(std::ostream & out):m_out(out) {} + + void operator()(expr const & e, context const & c) { + print(e, c); + } +}; + +std::ostream & operator<<(std::ostream & out, expr const & e) { + print_expr_fn pr(out); + pr(e, context()); + return out; +} + +class simple_formatter_cell : public formatter_cell { +public: + virtual format operator()(expr const & e, options const &) { + std::ostringstream s; s << e; return format(s.str()); + } +}; +formatter mk_simple_formatter() { + return mk_formatter(simple_formatter_cell()); +} +void print(lean::expr const & a) { std::cout << a << std::endl; } +} diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h index e30939101..af6be062a 100644 --- a/src/kernel/formatter.h +++ b/src/kernel/formatter.h @@ -7,8 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include "util/sexpr/options.h" -#include "kernel/context.h" -#include "kernel/environment.h" +#include "kernel/expr.h" namespace lean { /** @@ -19,16 +18,7 @@ public: virtual ~formatter_cell() {} /** \brief Format the given expression. */ virtual format operator()(expr const & e, options const & opts) = 0; - /** \brief Format the given context. */ - virtual format operator()(context const & c, options const & opts) = 0; - /** - \brief Format the given expression with respect to the given - context. - - \remark If format_ctx == false, then the context is not formatted. It just provides names - for the free variables - */ - virtual format operator()(context const & c, expr const & e, bool format_ctx, options const & opts) = 0; +#if 0 /** \brief Format the given object */ virtual format operator()(object const & obj, options const & opts) = 0; /** \brief Format the given environment */ @@ -39,6 +29,7 @@ public: Not every formatter has an associated environment object. */ virtual optional get_environment() const { return optional(); } +#endif }; /** \brief Smart-pointer for the actual formatter object (aka \c formatter_cell). @@ -48,16 +39,21 @@ class formatter { formatter(formatter_cell * c):m_cell(c) {} public: format operator()(expr const & e, options const & opts = options()) const { return (*m_cell)(e, opts); } - format operator()(context const & c, options const & opts = options()) const { return (*m_cell)(c, opts); } - format operator()(context const & c, expr const & e, bool format_ctx = false, options const & opts = options()) const { return (*m_cell)(c, e, format_ctx, opts); } +#if 0 format operator()(object const & obj, options const & opts = options()) const { return (*m_cell)(obj, opts); } format operator()(ro_environment const & env, options const & opts = options()) const { return (*m_cell)(env, opts); } optional get_environment() { return m_cell->get_environment(); } - +#endif template friend formatter mk_formatter(FCell && fcell); }; template formatter mk_formatter(FCell && fcell) { return formatter(new FCell(std::forward(fcell))); } + +std::ostream & operator<<(std::ostream & out, expr const & e); +/** + \brief Create a simple formatter object based on operator<< +*/ +formatter mk_simple_formatter(); } diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp index b443ee7e4..4971c72a5 100644 --- a/src/kernel/replace_fn.cpp +++ b/src/kernel/replace_fn.cpp @@ -7,16 +7,6 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" namespace lean { -bool replace_fn::is_atomic(expr const & e) { - switch (e.kind()) { - case expr_kind::Constant: case expr_kind::Sort: - case expr_kind::Macro: case expr_kind::Var: - return true; - default: - return false; - } -} - void replace_fn::save_result(expr const & e, expr const & r, unsigned offset, bool shared) { if (shared) m_cache.insert(std::make_pair(expr_cell_offset(e.raw(), offset), r)); diff --git a/src/kernel/replace_fn.h b/src/kernel/replace_fn.h index 250628048..4e20833fc 100644 --- a/src/kernel/replace_fn.h +++ b/src/kernel/replace_fn.h @@ -52,7 +52,6 @@ class replace_fn { frame_stack m_fs; result_stack m_rs; - static bool is_atomic(expr const & e); void save_result(expr const & e, expr const & r, unsigned offset, bool shared); bool visit(expr const & e, unsigned offset); bool check_index(frame & f, unsigned idx);