From 88cc3dc20df4bcc698d6558a880541d9fd8dee1a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Aug 2013 20:00:35 -0700 Subject: [PATCH] Add interrupt to normalizer. Fix tests (they were not using the basic printer). Signed-off-by: Leonardo de Moura --- src/kernel/environment.cpp | 1 + src/kernel/normalize.cpp | 153 ++++++++++++++++++++++----------- src/kernel/normalize.h | 19 ++++ src/kernel/type_check.cpp | 27 ------ src/kernel/type_check.h | 1 - src/tests/kernel/arith.cpp | 1 + src/tests/kernel/expr.cpp | 1 + src/tests/kernel/normalize.cpp | 1 + src/tests/kernel/replace.cpp | 1 + 9 files changed, 128 insertions(+), 77 deletions(-) diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index e1aaa57fd..7d6ad63d3 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "environment.h" #include "safe_arith.h" #include "type_check.h" +#include "normalize.h" namespace lean { diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp index ad0280673..910ae8808 100644 --- a/src/kernel/normalize.cpp +++ b/src/kernel/normalize.cpp @@ -14,11 +14,9 @@ Author: Leonardo de Moura #include "free_vars.h" #include "list.h" #include "buffer.h" -#include "trace.h" #include "exception.h" namespace lean { - class svalue; typedef list value_stack; //!< Normalization stack enum class svalue_kind { Expr, Closure, BoundedVar }; @@ -53,12 +51,24 @@ unsigned to_bvar(svalue const & v) { return v.get_var_idx(); } value_stack extend(value_stack const & s, svalue const & v) { return cons(v, s); } /** \brief Expression normalizer. */ -class normalize_fn { +class normalizer::imp { typedef scoped_map cache; - environment const & m_env; - context const & m_ctx; - cache m_cache; + environment m_env; + context m_ctx; + cache m_cache; + volatile bool m_interrupted; + + /** + \brief Auxiliary object for saving the current context. + We need this to be able to process values in the context. + */ + struct save_context { + imp & m_imp; + context m_old_ctx; + save_context(imp & imp):m_imp(imp), m_old_ctx(m_imp.m_ctx) { m_imp.m_cache.clear(); } + ~save_context() { m_imp.m_ctx = m_old_ctx; } + }; svalue lookup(value_stack const & s, unsigned i, unsigned k) { unsigned j = i; @@ -72,10 +82,14 @@ class normalize_fn { auto p = lookup_ext(m_ctx, j); context_entry const & entry = p.first; context const & entry_c = p.second; - if (entry.get_body()) - return svalue(::lean::normalize(entry.get_body(), m_env, entry_c)); - else + if (entry.get_body()) { + save_context save(*this); // it restores the context and cache + m_ctx = entry_c; + unsigned k = length(m_ctx); + return svalue(reify(normalize(entry.get_body(), value_stack(), k), k)); + } else { return svalue(length(entry_c)); + } } /** \brief Convert the closure \c a into an expression using the given stack in a context that contains \c k binders. */ @@ -84,42 +98,10 @@ class normalize_fn { expr new_t = reify(normalize(abst_domain(a), s, k), k); expr new_b = reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1); return mk_lambda(abst_name(a), new_t, new_b); -#if 0 - // Eta-reduction + Cumulativity + Set theoretic interpretation is unsound. - // Example: - // f : (Type 2) -> (Type 2) - // (lambda (x : (Type 1)) (f x)) : (Type 1) -> (Type 2) - // The domains of these two terms are different. So, they must have different denotations. - // However, by eta-reduction, we have: - // (lambda (x : (Type 1)) (f x)) == f - // For now, we will disable it. - // REMARK: we can workaround this problem by applying only when the domain of f is equal - // to the domain of the lambda abstraction. - // - if (is_app(new_b)) { - // (lambda (x:T) (app f ... (var 0))) - // check eta-rule applicability - unsigned n = num_args(new_b); - if (is_var(arg(new_b, n - 1), 0) && - std::all_of(begin_args(new_b), - end_args(new_b) - 1, - [](expr const & arg) { return !has_free_var(arg, 0); })) { - if (n == 2) - return lower_free_vars(arg(new_b, 0), 1); - else - return lower_free_vars(app(n - 1, begin_args(new_b)), 1); - } - return lambda(abst_name(a), new_t, new_b); - } else { - return lambda(abst_name(a), new_t, new_b); - } -#endif } /** \brief Convert the value \c v back into an expression in a context that contains \c k binders. */ expr reify(svalue const & v, unsigned k) { - lean_trace("normalize", tout << "Reify kind: " << static_cast(v.kind()) << "\n"; - if (v.is_bounded_var()) tout << "#" << to_bvar(v); else tout << to_expr(v); tout << "\n";); switch (v.kind()) { case svalue_kind::Expr: return to_expr(v); case svalue_kind::BoundedVar: return mk_var(k - to_bvar(v) - 1); @@ -131,7 +113,8 @@ class normalize_fn { /** \brief Normalize the expression \c a in a context composed of stack \c s and \c k binders. */ svalue normalize(expr const & a, value_stack const & s, unsigned k) { - lean_trace("normalize", tout << "Normalize, k: " << k << "\n" << a << "\n";); + if (m_interrupted) + throw interrupted(); bool shared = false; if (is_shared(a)) { @@ -167,7 +150,6 @@ class normalize_fn { if (f.is_closure()) { // beta reduction expr const & fv = to_expr(f); - lean_trace("normalize", tout << "beta reduction...\n" << fv << "\n";); { cache::mk_scope sc(m_cache); value_stack new_s = extend(stack_of(f), normalize(arg(a, i), s, k)); @@ -236,19 +218,92 @@ class normalize_fn { return r; } -public: - normalize_fn(environment const & env, context const & ctx): - m_env(env), - m_ctx(ctx) { + bool is_convertible_core(expr const & expected, expr const & given) { + if (expected == given) { + return true; + } else { + expr const * e = &expected; + expr const * g = &given; + while (true) { + if (is_type(*e) && is_type(*g)) { + if (m_env.is_ge(ty_level(*e), ty_level(*g))) + return true; + } + if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) { + e = &abst_body(*e); + g = &abst_body(*g); + } else { + return false; + } + } + } } - expr operator()(expr const & e) { + void set_ctx(context const & ctx) { + if (!is_eqp(ctx, m_ctx)) { + m_ctx = ctx; + m_cache.clear(); + } + } + +public: + imp(environment const & env): + m_env(env) { + m_interrupted = false; + } + + expr operator()(expr const & e, context const & ctx) { + set_ctx(ctx); unsigned k = length(m_ctx); return reify(normalize(e, value_stack(), k), k); } + + bool is_convertible(expr const & expected, expr const & given, context const & ctx) { + if (is_convertible_core(expected, given)) + return true; + set_ctx(ctx); + unsigned k = length(m_ctx); + expr e_n = reify(normalize(expected, value_stack(), k), k); + expr g_n = reify(normalize(given, value_stack(), k), k); + return is_convertible_core(e_n, g_n); + } + + void clear() { m_ctx = context(); m_cache.clear(); } + void set_interrupt(bool flag) { m_interrupted = flag; } }; +normalizer::normalizer(environment const & env):m_ptr(new imp(env)) {} +normalizer::~normalizer() {} +expr normalizer::operator()(expr const & e, context const & ctx) { return (*m_ptr)(e, ctx); } +bool normalizer::is_convertible(expr const & t1, expr const & t2, context const & ctx) { return m_ptr->is_convertible(t1, t2, ctx); } +void normalizer::clear() { m_ptr->clear(); } +void normalizer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } + expr normalize(expr const & e, environment const & env, context const & ctx) { - return normalize_fn(env, ctx)(e); + return normalizer(env)(e, ctx); +} +bool is_convertible(expr const & expected, expr const & given, environment const & env, context const & ctx) { + return normalizer(env).is_convertible(expected, given, ctx); } } + +/* + Remark: + + Eta-reduction + Cumulativity + Set theoretic interpretation is unsound. + Example: + f : (Type 2) -> (Type 2) + (fun (x : (Type 1)) (f x)) : (Type 1) -> (Type 2) + The domains of these two terms are different. So, they must have different denotations. + + However, by eta-reduction, we have: + (fun (x : (Type 1)) (f x)) == f + + For now, we will disable it. + REMARK: we can workaround this problem by applying only when the domain of f is equal + to the domain of the lambda abstraction. + + Cody Roux suggested we use Eta-expanded normal forms. + + Remark: The source code for eta-reduction can be found in the commit 519a290f320c6a +*/ diff --git a/src/kernel/normalize.h b/src/kernel/normalize.h index 4c239a42d..bdfaad5dd 100644 --- a/src/kernel/normalize.h +++ b/src/kernel/normalize.h @@ -5,12 +5,31 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include "expr.h" #include "environment.h" #include "context.h" namespace lean { class environment; +/** \brief Functional object for normalizing expressions */ +class normalizer { + struct imp; + std::unique_ptr m_ptr; +public: + normalizer(environment const & env); + ~normalizer(); + + expr operator()(expr const & e, context const & ctx = context()); + bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context()); + + void clear(); + + void set_interrupt(bool flag); + void interrupt() { set_interrupt(true); } + void reset_interrupt() { set_interrupt(false); } +}; /** \brief Normalize \c e using the environment \c env and context \c ctx */ expr normalize(expr const & e, environment const & env, context const & ctx = context()); +bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context()); } diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp index 72783115f..5ae83d8a2 100644 --- a/src/kernel/type_check.cpp +++ b/src/kernel/type_check.cpp @@ -14,33 +14,6 @@ Author: Leonardo de Moura #include "free_vars.h" namespace lean { -bool is_convertible_core(expr const & expected, expr const & given, environment const & env) { - if (expected == given) - return true; - expr const * e = &expected; - expr const * g = &given; - while (true) { - if (is_type(*e) && is_type(*g)) { - if (env.is_ge(ty_level(*e), ty_level(*g))) - return true; - } - if (is_pi(*e) && is_pi(*g) && abst_domain(*e) == abst_domain(*g)) { - e = &abst_body(*e); - g = &abst_body(*g); - } else { - return false; - } - } -} - -bool is_convertible(expr const & expected, expr const & given, environment const & env, context const & ctx) { - if (is_convertible_core(expected, given, env)) - return true; - expr e_n = normalize(expected, env, ctx); - expr g_n = normalize(given, env, ctx); - return is_convertible_core(e_n, g_n, env); -} - /** \brief Auxiliary functional object used to implement infer_type. */ class type_checker::imp { typedef scoped_map cache; diff --git a/src/kernel/type_check.h b/src/kernel/type_check.h index ed697e1de..48b1719aa 100644 --- a/src/kernel/type_check.h +++ b/src/kernel/type_check.h @@ -31,5 +31,4 @@ public: expr infer_type(expr const & e, environment const & env, context const & ctx = context()); level infer_universe(expr const & t, environment const & env, context const & ctx = context()); -bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context()); } diff --git a/src/tests/kernel/arith.cpp b/src/tests/kernel/arith.cpp index 1702fe3be..bcb64b321 100644 --- a/src/tests/kernel/arith.cpp +++ b/src/tests/kernel/arith.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "arith.h" #include "normalize.h" #include "abstract.h" +#include "printer.h" #include "test.h" using namespace lean; diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 83539853f..38883ff91 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "test.h" #include "abstract.h" #include "instantiate.h" +#include "printer.h" #include "deep_copy.h" #include "arith.h" using namespace lean; diff --git a/src/tests/kernel/normalize.cpp b/src/tests/kernel/normalize.cpp index 0d7774ac3..6926b7ef9 100644 --- a/src/tests/kernel/normalize.cpp +++ b/src/tests/kernel/normalize.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "trace.h" #include "test.h" #include "expr_sets.h" +#include "printer.h" using namespace lean; expr normalize(expr const & e) { diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp index 1134a8faf..8dd1ad0f9 100644 --- a/src/tests/kernel/replace.cpp +++ b/src/tests/kernel/replace.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "abstract.h" #include "instantiate.h" #include "deep_copy.h" +#include "printer.h" #include "name.h" #include "test.h" using namespace lean;