diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp deleted file mode 100644 index 4b82dc2fb0..0000000000 --- a/src/kernel/normalizer.cpp +++ /dev/null @@ -1,244 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/list.h" -#include "util/flet.h" -#include "util/freset.h" -#include "util/buffer.h" -#include "util/interrupt.h" -#include "util/sexpr/options.h" -#include "kernel/normalizer.h" -#include "kernel/environment.h" -#include "kernel/expr_maps.h" -#include "kernel/free_vars.h" -#include "kernel/instantiate.h" -#include "kernel/replace_fn.h" -#include "kernel/kernel_exception.h" - -#ifndef LEAN_KERNEL_NORMALIZER_MAX_DEPTH -#define LEAN_KERNEL_NORMALIZER_MAX_DEPTH std::numeric_limits::max() -#endif - -namespace lean { -static name g_kernel_normalizer_max_depth {"kernel", "normalizer", "max_depth"}; -RegisterUnsignedOption(g_kernel_normalizer_max_depth, LEAN_KERNEL_NORMALIZER_MAX_DEPTH, "(kernel) maximum recursion depth for expression normalizer"); -unsigned get_normalizer_max_depth(options const & opts) { - return opts.get_unsigned(g_kernel_normalizer_max_depth, LEAN_KERNEL_NORMALIZER_MAX_DEPTH); -} - -typedef list value_stack; -value_stack extend(value_stack const & s, expr const & v) { - lean_assert(!is_lambda(v) && !is_pi(v) && !is_metavar(v) && !is_let(v)); - return cons(v, s); -} - -/** - \brief Internal value used to store closures. - This is a transient value that is only used during normalization. -*/ -class closure : public macro { - expr m_expr; - value_stack m_stack; -public: - closure(expr const & e, value_stack const & s):m_expr(e), m_stack(s) {} - virtual ~closure() {} - virtual expr get_type(buffer const & ) const { lean_unreachable(); } // LCOV_EXCL_LINE - virtual void write(serializer & ) const { lean_unreachable(); } // LCOV_EXCL_LINE - virtual expr expand1(buffer const & ) const { lean_unreachable(); } - virtual expr expand(buffer const & ) const { lean_unreachable(); } - virtual name get_name() const { return name("Closure"); } - virtual void display(std::ostream & out) const { - out << "(Closure " << m_expr << " ["; - bool first = true; - for (auto v : m_stack) { - if (first) first = false; else out << " "; - out << v; - } - out << "])"; - } - expr const & get_expr() const { return m_expr; } - value_stack const & get_stack() const { return m_stack; } - virtual bool is_atomic_pp(bool /* unicode */, bool /* coercion */) const { return false; } // NOLINT -}; - -expr mk_closure(expr const & e, value_stack const & s) { return mk_macro(new closure(e, s)); } -bool is_closure(expr const & e) { return is_macro(e) && dynamic_cast(&to_macro(e)) != nullptr; } -closure const & to_closure(expr const & e) { lean_assert(is_closure(e)); return static_cast(to_macro(e)); } - -/** \brief Expression normalizer. */ -class normalizer::imp { - typedef expr_map cache; - - ro_environment::weak_ref m_env; - cache m_cache; - unsigned m_max_depth; - unsigned m_depth; - - ro_environment env() const { return ro_environment(m_env); } - - expr lookup(value_stack const & s, unsigned i) { - unsigned j = i; - value_stack const * it1 = &s; - while (*it1) { - if (j == 0) - return head(*it1); - --j; - it1 = &tail(*it1); - } - throw kernel_exception(env(), "normalizer failure, unexpected occurrence of free variable"); - } - - /** \brief Convert the value \c v back into an expression in a context that contains \c k binders. */ - expr reify(expr const & v, unsigned k) { - return replace(v, [&](expr const & e, unsigned DEBUG_CODE(offset)) -> optional { - lean_assert(offset == 0); - lean_assert(!is_lambda(e) && !is_pi(e) && !is_let(e)); - if (is_var(e)) { - // de Bruijn level --> de Bruijn index - return some_expr(mk_var(k - var_idx(e) - 1)); - } else if (is_closure(e)) { - return some_expr(reify_closure(to_closure(e), k)); - } else { - return none_expr(); - } - }); - } - - /** \brief Convert the closure \c c into an expression in a context that contains \c k binders. */ - expr reify_closure(closure const & c, unsigned k) { - expr const & e = c.get_expr(); - value_stack const & s = c.get_stack(); - lean_assert(is_binder(e)); - freset reset(m_cache); - expr new_d = reify(normalize(binder_domain(e), s, k), k); - m_cache.clear(); // make sure we do not reuse cached values from the previous call - expr new_b = reify(normalize(binder_body(e), extend(s, mk_var(k)), k+1), k+1); - return update_binder(e, new_d, new_b); - } - - /** \brief Normalize the expression \c a in a context composed of stack \c s and \c k binders. */ - expr normalize(expr const & a, value_stack const & s, unsigned k) { - flet l(m_depth, m_depth+1); - check_system("normalizer"); - if (m_depth > m_max_depth) - throw kernel_exception(env(), "normalizer maximum recursion depth exceeded"); - bool shared = false; - if (is_shared(a)) { - shared = true; - auto it = m_cache.find(a); - if (it != m_cache.end()) - return it->second; - } - - expr r; - switch (a.kind()) { - case expr_kind::Pi: case expr_kind::Lambda: - r = mk_closure(a, s); - break; - case expr_kind::Var: - r = lookup(s, var_idx(a)); - break; - case expr_kind::Constant: { - optional obj = env()->find_object(const_name(a)); - if (should_unfold(obj)) { - // TODO(Leo): instantiate level parameters - freset reset(m_cache); - r = normalize(obj->get_value(), value_stack(), 0); - } else { - r = a; - } - break; - } - case expr_kind::Sort: case expr_kind::Macro: case expr_kind::Local: case expr_kind::Meta: - r = a; - break; - case expr_kind::App: { - buffer new_args; - expr const * it = &a; - while (is_app(*it)) { - new_args.push_back(normalize(app_arg(*it), s, k)); - it = &app_fn(*it); - } - expr f = normalize(*it, s, k); - unsigned i = 0; - unsigned n = new_args.size(); - while (true) { - if (is_closure(f) && is_lambda(to_closure(f).get_expr())) { - // beta reduction - expr fv = to_closure(f).get_expr(); - value_stack new_s = to_closure(f).get_stack(); - while (is_lambda(fv) && i < n) { - new_s = extend(new_s, new_args[n - i - 1]); - i++; - fv = binder_body(fv); - } - { - freset reset(m_cache); - f = normalize(fv, new_s, k); - } - if (i == n) { - r = f; - break; - } - } else { - if (is_macro(f) && !is_closure(f)) { - buffer reified_args; - unsigned i = new_args.size(); - while (i > 0) { - --i; - reified_args.push_back(reify(new_args[i], k)); - } - r = to_macro(f).expand(reified_args); - } else { - new_args.push_back(f); - std::reverse(new_args.begin(), new_args.end()); - r = mk_app(new_args); - } - break; - } - } - break; - } - case expr_kind::Let: { - expr v = normalize(let_value(a), s, k); - { - freset reset(m_cache); - r = normalize(let_body(a), extend(s, v), k); - } - break; - }} - if (shared) { - m_cache[a] = r; - } - return r; - } - - -public: - imp(ro_environment const & env, unsigned max_depth): - m_env(env) { - m_max_depth = max_depth; - m_depth = 0; - } - - expr operator()(expr const & e) { - unsigned k = 0; - return reify(normalize(e, value_stack(), k), k); - } - - void clear() { m_cache.clear(); } -}; - -normalizer::normalizer(ro_environment const & env, unsigned max_depth):m_ptr(new imp(env, max_depth)) {} -normalizer::normalizer(ro_environment const & env):normalizer(env, std::numeric_limits::max()) {} -normalizer::normalizer(ro_environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {} -normalizer::~normalizer() {} -expr normalizer::operator()(expr const & e) { return (*m_ptr)(e); } -void normalizer::clear() { m_ptr->clear(); } -expr normalize(expr const & e, ro_environment const & env) { return normalizer(env)(e); } -} diff --git a/src/kernel/normalizer.h b/src/kernel/normalizer.h deleted file mode 100644 index fe827c7db7..0000000000 --- a/src/kernel/normalizer.h +++ /dev/null @@ -1,30 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include "kernel/expr.h" - -namespace lean { -class ro_environment; -class options; -/** \brief Functional object for normalizing expressions */ -class normalizer { - class imp; - std::unique_ptr m_ptr; -public: - normalizer(ro_environment const & env); - normalizer(ro_environment const & env, unsigned max_depth); - normalizer(ro_environment const & env, options const & opts); - ~normalizer(); - - expr operator()(expr const & e); - void clear(); -}; - -/** \brief Normalize \c e using the environment \c env and context \c ctx */ -expr normalize(expr const & e, ro_environment const & env); -} diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt index 56478bfc3b..cabd1bd7b3 100644 --- a/src/tests/kernel/CMakeLists.txt +++ b/src/tests/kernel/CMakeLists.txt @@ -10,9 +10,6 @@ add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr) add_executable(max_sharing max_sharing.cpp) target_link_libraries(max_sharing ${EXTRA_LIBS}) add_test(max_sharing ${CMAKE_CURRENT_BINARY_DIR}/max_sharing) -# add_executable(normalizer normalizer.cpp) -# target_link_libraries(normalizer ${EXTRA_LIBS}) -# add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer) # add_executable(threads threads.cpp) # target_link_libraries(threads ${EXTRA_LIBS}) # add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads) diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp deleted file mode 100644 index 3f6ad2a2a0..0000000000 --- a/src/tests/kernel/normalizer.cpp +++ /dev/null @@ -1,217 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "util/thread.h" -#include "util/test.h" -#include "util/trace.h" -#include "util/exception.h" -#include "util/interrupt.h" -#include "kernel/normalizer.h" -#include "kernel/expr_sets.h" -#include "kernel/abstract.h" -#include "kernel/kernel_exception.h" -#include "kernel/free_vars.h" -using namespace lean; - -expr normalize(expr const & e) { - environment env; - return normalize(e, env); -} - -static void eval(expr const & e, environment & env) { std::cout << e << " --> " << normalize(e, env) << "\n"; } -static expr t() { return Const("t"); } -static expr lam(expr const & e) { return mk_lambda("_", t(), e); } -static expr lam(expr const & t, expr const & e) { return mk_lambda("_", t, e); } -static expr v(unsigned i) { return Var(i); } -static expr zero() { - // fun (t : T) (s : t -> t) (z : t) z - return lam(t(), lam(mk_arrow(v(0), v(0)), lam(v(1), v(0)))); -} -static expr one() { - // fun (t : T) (s : t -> t) s - return lam(t(), lam(mk_arrow(v(0), v(0)), v(0))); -} -static expr num() { return Const("num"); } -static expr plus() { - // fun (m n : numeral) (A : Type 0) (f : A -> A) (x : A) => m A f (n A f x). - expr x = v(0), f = v(1), A = v(2), n = v(3), m = v(4); - expr body = m(A, f, n(A, f, x)); - return lam(num(), lam(num(), lam(t(), lam(mk_arrow(v(0), v(0)), lam(v(1), body))))); -} -static expr two() { return mk_app({plus(), one(), one()}); } -static expr three() { return mk_app({plus(), two(), one()}); } -static expr four() { return mk_app({plus(), two(), two()}); } -static expr times() { - // fun (m n : numeral) (A : Type 0) (f : A -> A) (x : A) => m A (n A f) x. - expr x = v(0), f = v(1), A = v(2), n = v(3), m = v(4); - expr body = m(A, n(A, f), x); - return lam(num(), lam(num(), lam(t(), lam(mk_arrow(v(0), v(0)), lam(v(1), body))))); -} -static expr power() { - // fun (m n : numeral) (A : Type 0) => m (A -> A) (n A). - expr A = v(0), n = v(1), m = v(2); - expr body = n(mk_arrow(A, A), m(A)); - return lam(num(), lam(num(), lam(mk_arrow(v(0), v(0)), body))); -} - -unsigned count_core(expr const & a, expr_set & s) { - if (s.find(a) != s.end()) - return 0; - s.insert(a); - switch (a.kind()) { - case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort: - case expr_kind::Meta: case expr_kind::Local: case expr_kind::Macro: - return 1; - case expr_kind::App: - return count_core(app_fn(a), s) + count_core(app_arg(a), s) + 1; - case expr_kind::Lambda: case expr_kind::Pi: - return count_core(binder_domain(a), s) + count_core(binder_body(a), s) + 1; - case expr_kind::Let: - return count_core(let_value(a), s) + count_core(let_body(a), s) + 1; - } - return 0; -} - -unsigned count(expr const & a) { - expr_set s; - return count_core(a, s); -} - -static void tst_church_numbers() { - environment env; - env->add_var("t", Type); - env->add_var("N", Type); - env->add_var("z", Const("N")); - env->add_var("s", Const("N")); - expr N = Const("N"); - expr z = Const("z"); - expr s = Const("s"); - std::cout << normalize(mk_app(zero(), N, s, z), env) << "\n"; - std::cout << normalize(mk_app(one(), N, s, z), env) << "\n"; - std::cout << normalize(mk_app(two(), N, s, z), env) << "\n"; - std::cout << normalize(mk_app(four(), N, s, z), env) << "\n"; - std::cout << count(normalize(mk_app(four(), N, s, z), env)) << "\n"; - lean_assert_eq(count(normalize(mk_app(four(), N, s, z), env)), 15); - std::cout << normalize(mk_app(mk_app(times(), four(), four()), N, s, z), env) << "\n"; - std::cout << normalize(mk_app(mk_app(power(), two(), four()), N, s, z), env) << "\n"; - lean_assert_eq(count(normalize(mk_app(mk_app(power(), two(), four()), N, s, z), env)), 51); - std::cout << normalize(mk_app(mk_app(times(), two(), mk_app(power(), two(), four())), N, s, z), env) << "\n"; - std::cout << normalize(mk_app(mk_app(times(), four(), mk_app(power(), two(), four())), N, s, z), env) << "\n"; - std::cout << count(normalize(mk_app(mk_app(times(), two(), mk_app(power(), two(), four())), N, s, z), env)) << "\n"; - std::cout << count(normalize(mk_app(mk_app(times(), four(), mk_app(power(), two(), four())), N, s, z), env)) << "\n"; - lean_assert_eq(count(normalize(mk_app(mk_app(times(), four(), mk_app(power(), two(), four())), N, s, z), env)), 195); - expr big = normalize(mk_app(mk_app(power(), two(), mk_app(power(), two(), three())), N, s, z), env); - std::cout << count(big) << "\n"; - lean_assert_eq(count(big), 771); - expr three = mk_app(plus(), two(), one()); - lean_assert_eq(count(normalize(mk_app(mk_app(power(), three, three), N, s, z), env)), 84); - // expr big2 = normalize(mk_app(mk_app(power(), two(), mk_app(times(), mk_app(plus(), four(), one()), four())), N, s, z), env); - // std::cout << count(big2) << "\n"; - std::cout << normalize(lam(lam(mk_app(mk_app(times(), four(), four()), N, Var(0), z))), env) << "\n"; -} - -static void tst1() { - environment env; - env->add_var("t", Type); - expr t = Type; - env->add_var("f", mk_arrow(t, t)); - expr f = Const("f"); - env->add_var("a", t); - expr a = Const("a"); - env->add_var("b", t); - expr b = Const("b"); - expr x = Var(0); - expr y = Var(1); - eval(mk_app(mk_lambda("x", t, x), a), env); - eval(mk_app(mk_lambda("x", t, x), a, b), env); - eval(mk_lambda("x", t, f(x)), env); - eval(mk_lambda("y", t, mk_lambda("x", t, f(y, x))), env); - eval(mk_app(mk_lambda("x", t, - mk_app(mk_lambda("f", t, - mk_app(Var(0), b)), - mk_lambda("g", t, f(Var(1))))), - a), env); - expr l01 = lam(v(0)(v(1))); - expr l12 = lam(lam(v(1)(v(2)))); - eval(lam(l12(l01)), env); - lean_assert(normalize(lam(l12(l01)), env) == lam(lam(v(1)(v(1))))); -} - -static void tst2() { - environment env; - env->add_var("b", Type); - expr t1 = mk_let("a", Type, Const("b"), mk_lambda("c", Type, Var(1)(Var(0)))); - std::cout << t1 << " --> " << normalize(t1, env) << "\n"; - lean_assert(normalize(t1, env) == mk_lambda("c", Type, Const("b")(Var(0)))); -} - -static expr mk_big(unsigned depth) { - if (depth == 0) - return Const("a"); - else - return Const("f")(mk_big(depth - 1), mk_big(depth - 1)); -} - -static void tst3() { -#if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) - expr t = mk_big(18); - environment env; - env->add_var("f", Bool >> (Bool >> Bool)); - env->add_var("a", Bool); - normalizer proc(env); - chrono::milliseconds dura(50); - interruptible_thread thread([&]() { - try { - proc(t); - // Remark: if the following code is reached, we - // should decrease dura. - lean_unreachable(); - } catch (interrupted & it) { - std::cout << "interrupted\n"; - } - }); - this_thread::sleep_for(dura); - thread.request_interrupt(); - thread.join(); -#endif -} - -static void tst4() { - environment env; - expr x = Const("x"); - expr t = Fun({x, Type}, mk_app(x, x)); - expr omega = mk_app(t, t); - normalizer proc(env, 512); - try { - proc(omega); - } catch (kernel_exception & ex) { - std::cout << ex.what() << "\n"; - } -} - -static void tst5() { - environment env; - expr f = Const("f"); - env->add_var("f", Type >> (Type >> Type)); - expr x = Const("x"); - expr v = Const("v"); - expr F = Fun({x, Type}, Let(v, Type, Bool, f(x, v))); - expr N = normalizer(env)(F); - std::cout << F << " ==> " << N << "\n"; - lean_assert_eq(N, Fun({x, Type}, f(x, Bool))); -} - -int main() { - save_stack_info(); - tst_church_numbers(); - tst1(); - tst2(); - tst3(); - tst4(); - tst5(); - return has_violations() ? 1 : 0; -}