diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index ce2e97411..ed821941a 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -2,7 +2,7 @@ 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 context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp object.cpp environment.cpp replace_visitor.cpp io_state.cpp -# normalizer.cpp +normalizer.cpp # type_checker.cpp kernel.cpp metavar.cpp # justification.cpp unification_constraint.cpp # type_checker_justification.cpp pos_info_provider.cpp diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 20f42d765..6721d489a 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -12,16 +12,12 @@ Author: Leonardo de Moura #include "util/buffer.h" #include "util/interrupt.h" #include "util/sexpr/options.h" -#include "kernel/update_expr.h" #include "kernel/normalizer.h" -#include "kernel/expr.h" -#include "kernel/expr_maps.h" -#include "kernel/context.h" #include "kernel/environment.h" -#include "kernel/kernel.h" -#include "kernel/metavar.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 @@ -45,15 +41,16 @@ value_stack extend(value_stack const & s, expr const & v) { \brief Internal value used to store closures. This is a transient value that is only used during normalization. */ -class closure : public value { +class closure : public macro { expr m_expr; - context m_ctx; value_stack m_stack; public: - closure(expr const & e, context const & ctx, value_stack const & s):m_expr(e), m_ctx(ctx), m_stack(s) {} + closure(expr const & e, value_stack const & s):m_expr(e), m_stack(s) {} virtual ~closure() {} - virtual expr get_type() const { lean_unreachable(); } // LCOV_EXCL_LINE + 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 << " ["; @@ -65,37 +62,25 @@ public: out << "])"; } expr const & get_expr() const { return m_expr; } - context const & get_context() const { return m_ctx; } 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, context const & ctx, value_stack const & s) { return mk_value(*(new closure(e, ctx, s))); } -bool is_closure(expr const & e) { return is_value(e) && dynamic_cast(&to_value(e)) != nullptr; } -closure const & to_closure(expr const & e) { lean_assert(is_closure(e)); return static_cast(to_value(e)); } +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; - context m_ctx; - cached_ro_metavar_env m_menv; cache m_cache; - bool m_unfold_opaque; unsigned m_max_depth; unsigned m_depth; ro_environment env() const { return ro_environment(m_env); } - expr instantiate(expr const & e, unsigned n, expr const * s) { - return ::lean::instantiate(e, n, s, m_menv.to_some_menv()); - } - - expr add_lift(expr const & m, unsigned s, unsigned n) { - return ::lean::add_lift(m, s, n, m_menv.to_some_menv()); - } - expr lookup(value_stack const & s, unsigned i) { unsigned j = i; value_stack const * it1 = &s; @@ -105,25 +90,14 @@ class normalizer::imp { --j; it1 = &tail(*it1); } - auto p = lookup_ext(m_ctx, j); - context_entry const & entry = p.first; - context const & entry_c = p.second; - if (entry.get_body()) { - // Save the current context and cache - freset reset(m_cache); - flet set(m_ctx, entry_c); - unsigned k = m_ctx.size(); - return normalize(*(entry.get_body()), value_stack(), k); - } else { - return mk_var(entry_c.size()); - } + 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)) -> expr { lean_assert(offset == 0); - lean_assert(!is_lambda(e) && !is_pi(e) && !is_metavar(e) && !is_let(e)); + lean_assert(!is_lambda(e) && !is_pi(e) && !is_sigma(e) && !is_let(e)); if (is_var(e)) { // de Bruijn level --> de Bruijn index return mk_var(k - var_idx(e) - 1); @@ -135,87 +109,16 @@ class normalizer::imp { }); } - /** - \brief Return true iff the value_stack does not affect the context of a metavariable - See big comment at reify_closure. - */ - bool is_identity_stack(value_stack const & s, unsigned k) { - unsigned i = 0; - for (auto e : s) { - if (!is_var(e) || k - var_idx(e) - 1 != i) - return false; - ++i; - } - return true; - } - /** \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(); - context const & ctx = c.get_context(); value_stack const & s = c.get_stack(); - if (is_abstraction(e)) { - freset reset(m_cache); - flet set(m_ctx, ctx); - expr new_d = reify(normalize(abst_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(abst_body(e), extend(s, mk_var(k)), k+1), k+1); - return update_abstraction(e, new_d, new_b); - } else { - lean_assert(is_metavar(e)); - // We use the following trick to reify a metavariable in the context of the value_stack s, and context ctx. - // Let v_0, ..., v_{n-1} be the values on the stack s. We assume v_0 is the top of the stack. - // Let v_i' be reify(v_i, k). Then, v_i' is the "value" of the free variable #i in the metavariable e. - // Let m be the size of the context ctx. Thus - // - // The metavariable e may contain free variables. - // Moreover, if we instantiate e with T[x_0, ..., x_{n-1}, x_n, ..., x_{n+m-1}] - // Then, in this occurrence of e, we must have - // - // T[v_0', ..., v_{n-1}', reify(#{m-1}, k), ..., reify(#0, k)] - // - // reify(#j, k) is the index of j-th variable in the context ctx. - // It is just the variable #{k - j - 1}. - // So, we get - // - // T[v_0', ..., v_{n-1}', #{k - m}, ..., #{k - 1}] - // - // Thus, we implement this operation as: - // - // instantiate(e, {#{k - 1}, ..., #{k - m}, v_{n-1}', ..., v_1', v_0'})) - // - // This operation is equivalent to R_{n+m} defined as - // R_0 = e - // R_1 = instantiate(R_0, v_0') - // ... - // R_n = instantiate(R_{n-1}, v_{n-1}') - // R_{n+1} = instantiate(R_n, #{k - m}) - // ... - // R_{n+m} = instantiate(R_{n+m-1}, #{k-1}) - // - // - // Finally, we also use the following optimization. - // If all v_i' are equal to #i and n + m == k, then we just return e, because - // - // T[#0, ..., #n-1, #{n + m - m}, ..., #{m + n - 1}] - // == - // T[#0, ..., #n-1, #n, ..., #{m + n - 1}] - // == - // e - // - unsigned n = length(s); - unsigned m = ctx.size(); - if (k == n + m && is_identity_stack(s, k)) - return e; - buffer subst; - for (auto v : s) - subst.push_back(reify(v, k)); - for (unsigned i = m; i >= 1; i--) - subst.push_back(mk_var(k - i)); - lean_assert(subst.size() == n + m); - std::reverse(subst.begin(), subst.end()); - return instantiate(e, subst.size(), subst.data()); - } + 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. */ @@ -234,16 +137,15 @@ class normalizer::imp { expr r; switch (a.kind()) { - case expr_kind::Sigma: case expr_kind::Pi: - case expr_kind::MetaVar: case expr_kind::Lambda: - r = mk_closure(a, m_ctx, s); + case expr_kind::Sigma: 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 (obj && should_unfold(*obj, m_unfold_opaque)) { + if (should_unfold(obj)) { freset reset(m_cache); r = normalize(obj->get_value(), value_stack(), 0); } else { @@ -251,12 +153,6 @@ class normalizer::imp { } break; } - case expr_kind::HEq: { - expr new_lhs = normalize(heq_lhs(a), s, k); - expr new_rhs = normalize(heq_rhs(a), s, k); - r = update_heq(a, new_lhs, new_rhs); - break; - } case expr_kind::Pair: { expr new_first = normalize(pair_first(a), s, k); expr new_second = normalize(pair_second(a), s, k); @@ -264,10 +160,10 @@ class normalizer::imp { r = update_pair(a, new_first, new_second, new_type); break; } - case expr_kind::Proj: { + case expr_kind::Fst: case expr_kind::Snd: { expr new_arg = normalize(proj_arg(a), s, k); if (is_dep_pair(new_arg)) { - if (proj_first(a)) + if (is_fst(a)) r = pair_first(new_arg); else r = pair_second(new_arg); @@ -276,26 +172,31 @@ class normalizer::imp { } break; } - case expr_kind::Type: case expr_kind::Value: + case expr_kind::Sort: case expr_kind::Macro: case expr_kind::Local: case expr_kind::Meta: r = a; break; case expr_kind::App: { - expr f = normalize(arg(a, 0), s, k); - unsigned i = 1; - unsigned n = num_args(a); + 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, normalize(arg(a, i), s, k)); + new_s = extend(new_s, new_args[n - i - 1]); i++; - fv = abst_body(fv); + fv = binder_body(fv); } { freset reset(m_cache); - flet set(m_ctx, to_closure(f).get_context()); f = normalize(fv, new_s, k); } if (i == n) { @@ -303,20 +204,19 @@ class normalizer::imp { break; } } else { - buffer new_args; - new_args.push_back(f); - for (; i < n; i++) - new_args.push_back(normalize(arg(a, i), s, k)); - if (is_value(f) && !is_closure(f)) { + if (is_macro(f) && !is_closure(f)) { buffer reified_args; - for (auto arg : new_args) reified_args.push_back(reify(arg, k)); - optional m = to_value(f).normalize(reified_args.size(), reified_args.data()); - if (m) { - r = normalize(*m, s, k); - break; + 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); } - r = mk_app(new_args); break; } } @@ -336,51 +236,27 @@ class normalizer::imp { return r; } - void set_ctx(context const & ctx) { - if (!is_eqp(ctx, m_ctx)) { - m_ctx = ctx; - m_cache.clear(); - } - } public: imp(ro_environment const & env, unsigned max_depth): m_env(env) { m_max_depth = max_depth; m_depth = 0; - m_unfold_opaque = false; } - expr operator()(expr const & e, context const & ctx, optional const & menv, bool unfold_opaque) { - if (m_unfold_opaque != unfold_opaque) - m_cache.clear(); - m_unfold_opaque = unfold_opaque; - set_ctx(ctx); - if (m_menv.update(menv)) - m_cache.clear(); - unsigned k = m_ctx.size(); + expr operator()(expr const & e) { + unsigned k = 0; return reify(normalize(e, value_stack(), k), k); } - void clear() { m_ctx = context(); m_cache.clear(); m_menv.clear(); } + 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, context const & ctx, optional const & menv, bool unfold_opaque) { - return (*m_ptr)(e, ctx, menv, unfold_opaque); -} -expr normalizer::operator()(expr const & e, context const & ctx, ro_metavar_env const & menv, bool unfold_opaque) { - return operator()(e, ctx, some_ro_menv(menv), unfold_opaque); -} -expr normalizer::operator()(expr const & e, context const & ctx, bool unfold_opaque) { - return operator()(e, ctx, none_ro_menv(), unfold_opaque); -} +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, context const & ctx, bool unfold_opaque) { - return normalizer(env)(e, ctx, unfold_opaque); -} +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 index 5b19900b2..fe827c7db 100644 --- a/src/kernel/normalizer.h +++ b/src/kernel/normalizer.h @@ -7,13 +7,10 @@ Author: Leonardo de Moura #pragma once #include #include "kernel/expr.h" -#include "kernel/environment.h" -#include "kernel/context.h" namespace lean { -class environment; +class ro_environment; class options; -class ro_metavar_env; /** \brief Functional object for normalizing expressions */ class normalizer { class imp; @@ -24,12 +21,10 @@ public: normalizer(ro_environment const & env, options const & opts); ~normalizer(); - expr operator()(expr const & e, context const & ctx, optional const & menv, bool unfold_opaque = false); - expr operator()(expr const & e, context const & ctx, ro_metavar_env const & menv, bool unfold_opaque = false); - expr operator()(expr const & e, context const & ctx = context(), bool unfold_opaque = false); - + 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, context const & ctx = context(), bool unfold_opaque = false); +expr normalize(expr const & e, ro_environment const & env); } diff --git a/src/kernel/object.h b/src/kernel/object.h index a907ded39..e42617ca9 100644 --- a/src/kernel/object.h +++ b/src/kernel/object.h @@ -141,17 +141,9 @@ void read_object(environment const & env, io_state const & ios, std::string cons /** \brief Helper function whether we should unfold an definition or not. - 1- We unfold definitions. + 1- We unfold non-opaque definitions. 2- We never unfold theorems. - 3- We unfold opaque definitions if \c unfold_opaque == true */ -inline bool should_unfold(object const & obj, bool unfold_opaque) { - return obj.is_definition() && !obj.is_theorem() && (unfold_opaque || !obj.is_opaque()); -} -inline bool should_unfold(optional const & obj, bool unfold_opaque) { - return obj && should_unfold(*obj, unfold_opaque); -} -inline bool should_unfold(optional const & obj) { - return should_unfold(obj, false); -} +inline bool should_unfold(object const & obj) { return obj.is_definition() && !obj.is_theorem() && !obj.is_opaque(); } +inline bool should_unfold(optional const & obj) { return obj && should_unfold(*obj); } } diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt index df23589b5..5e70f37d5 100644 --- a/src/tests/kernel/CMakeLists.txt +++ b/src/tests/kernel/CMakeLists.txt @@ -7,9 +7,9 @@ add_test(diff_cnstrs ${CMAKE_CURRENT_BINARY_DIR}/diff_cnstrs) add_executable(expr expr.cpp) target_link_libraries(expr ${EXTRA_LIBS}) add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr) -# add_executable(normalizer normalizer.cpp) -# target_link_libraries(normalizer ${EXTRA_LIBS}) -# add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer) +add_executable(normalizer normalizer.cpp) +target_link_libraries(normalizer ${EXTRA_LIBS}) +add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer) # set_tests_properties(normalizer PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") # add_executable(threads threads.cpp) # target_link_libraries(threads ${EXTRA_LIBS}) diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index 6f2e357ab..e0cfee19e 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -11,18 +11,10 @@ Author: Leonardo de Moura #include "util/exception.h" #include "util/interrupt.h" #include "kernel/normalizer.h" -#include "kernel/kernel.h" #include "kernel/expr_sets.h" #include "kernel/abstract.h" #include "kernel/kernel_exception.h" -#include "kernel/metavar.h" #include "kernel/free_vars.h" -#include "library/printer.h" -#include "library/io_state_stream.h" -#include "library/deep_copy.h" -#include "library/arith/int.h" -#include "frontends/lean/frontend.h" -#include "frontends/lua/register_modules.h" using namespace lean; expr normalize(expr const & e) { @@ -71,22 +63,19 @@ unsigned count_core(expr const & a, expr_set & s) { return 0; s.insert(a); switch (a.kind()) { - case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: - case expr_kind::Value: case expr_kind::MetaVar: + 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 std::accumulate(begin_args(a), end_args(a), 1, - [&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); }); + return count_core(app_fn(a), s) + count_core(app_arg(a), s) + 1; case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Sigma: - return count_core(abst_domain(a), s) + count_core(abst_body(a), s) + 1; + 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; - case expr_kind::Proj: + case expr_kind::Fst: case expr_kind::Snd: return count_core(proj_arg(a), s) + 1; case expr_kind::Pair: return count_core(pair_first(a), s) + count_core(pair_second(a), s) + count_core(pair_type(a), s) + 1; - case expr_kind::HEq: - return count_core(heq_lhs(a), s) + count_core(heq_rhs(a), s); } return 0; } @@ -98,8 +87,8 @@ unsigned count(expr const & a) { static void tst_church_numbers() { environment env; - env->add_var("t", Type()); - env->add_var("N", Type()); + 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"); @@ -110,19 +99,20 @@ static void tst_church_numbers() { 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(count(normalize(mk_app(four(), N, s, z), env)) == 4 + 2); + 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(count(normalize(mk_app(mk_app(power(), two(), four()), N, s, z), env)) == 16 + 2); + 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(count(normalize(mk_app(mk_app(times(), four(), mk_app(power(), two(), four())), N, s, z), env)) == 64 + 2); + 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(count(big) == 256 + 2); + lean_assert_eq(count(big), 771); expr three = mk_app(plus(), two(), one()); - lean_assert(count(normalize(mk_app(mk_app(power(), three, three), N, s, z), env)) == 27 + 2); + 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"; @@ -130,8 +120,8 @@ static void tst_church_numbers() { static void tst1() { environment env; - env->add_var("t", Type()); - expr t = Type(); + 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); @@ -157,62 +147,10 @@ static void tst1() { static void tst2() { environment env; - 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"); - env->add_var("h", mk_arrow(t, t)); - expr h = Const("h"); - expr x = Var(0); - expr y = Var(1); - lean_assert(normalize(f(x, x), env, extend(context(), name("f"), t, f(a))) == f(f(a), f(a))); - context c1 = extend(extend(context(), name("f"), t, f(a)), name("h"), t, h(x)); - expr F1 = normalize(f(x, f(x)), env, c1); - lean_assert(F1 == f(h(f(a)), f(h(f(a))))); - std::cout << F1 << "\n"; - expr F2 = normalize(mk_lambda("x", t, f(x, f(y))), env, c1); - std::cout << F2 << "\n"; - lean_assert(F2 == mk_lambda("x", t, f(x, f(h(f(a)))))); - expr F3 = normalize(mk_lambda("y", t, mk_lambda("x", t, f(x, f(y)))), env, c1); - std::cout << F3 << "\n"; - lean_assert(F3 == mk_lambda("y", t, mk_lambda("x", t, f(x, f(y))))); - context c2 = extend(extend(context(), name("foo"), t, mk_lambda("x", t, f(x, a))), name("bla"), t, mk_lambda("z", t, h(x, y))); - expr F4 = normalize(mk_lambda("x", t, f(x, f(y))), env, c2); - std::cout << F4 << "\n"; - lean_assert(F4 == mk_lambda("x", t, f(x, f(mk_lambda("z", t, h(x, mk_lambda("x", t, f(x, a)))))))); - context c3 = extend(context(), name("x"), t); - expr f5 = mk_app(mk_lambda("f", t, mk_lambda("z", t, Var(1))), mk_lambda("y", t, Var(1))); - expr F5 = normalize(f5, env, c3); - std::cout << f5 << "\n---->\n"; - std::cout << F5 << "\n"; - lean_assert(F5 == mk_lambda("z", t, mk_lambda("y", t, Var(2)))); - context c4 = extend(extend(context(), name("x"), t), name("x2"), t); - expr F6 = normalize(mk_app(mk_lambda("f", t, mk_lambda("z1", t, mk_lambda("z2", t, mk_app(Var(2), Const("a"))))), - mk_lambda("y", t, mk_app(Var(1), Var(2), Var(0)))), env, c4); - std::cout << F6 << "\n"; - lean_assert(F6 == mk_lambda("z1", t, mk_lambda("z2", t, mk_app(Var(2), Var(3), Const("a"))))); -} - -static void tst3() { - environment env; - init_test_frontend(env); - env->add_var("a", Bool); - expr t1 = Const("a"); - expr t2 = Const("a"); - expr e = mk_eq(Bool, t1, t2); - std::cout << e << " --> " << normalize(e, env) << "\n"; - lean_assert(normalize(e, env) == mk_eq(Bool, t1, t2)); -} - -static void tst4() { - environment env; - env->add_var("b", Type()); - expr t1 = mk_let("a", none_expr(), Const("b"), mk_lambda("c", Type(), Var(1)(Var(0)))); + 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)))); + lean_assert(normalize(t1, env) == mk_lambda("c", Type, Const("b")(Var(0)))); } static expr mk_big(unsigned depth) { @@ -222,11 +160,10 @@ static expr mk_big(unsigned depth) { return Const("f")(mk_big(depth - 1), mk_big(depth - 1)); } -static void tst5() { +static void tst3() { #if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) expr t = mk_big(18); environment env; - init_test_frontend(env); env->add_var("f", Bool >> (Bool >> Bool)); env->add_var("a", Bool); normalizer proc(env); @@ -247,10 +184,10 @@ static void tst5() { #endif } -static void tst6() { +static void tst4() { environment env; expr x = Const("x"); - expr t = Fun({x, Type()}, mk_app(x, x)); + expr t = Fun({x, Type}, mk_app(x, x)); expr omega = mk_app(t, t); normalizer proc(env, 512); try { @@ -260,109 +197,25 @@ static void tst6() { } } -static void tst7() { - environment env; - init_test_frontend(env); - metavar_env menv; - expr m1 = menv->mk_metavar(); - expr x = Const("x"); - expr F = Fun({x, Bool}, m1(x))(True); - normalizer proc(env); - std::cout << F << " --> " << proc(F, context(), menv) << "\n"; - // In the following assertion, we provide the metavar_env to the normalizer. - // Thus, it "knowns" the metavariable does not contain the free variable #0 - lean_assert_eq(proc(F, context(), menv), m1(True)); - // In the following assertion, we did not provide the metavar_env to the normalizer. - // Thus, it assumes the may contain the free variable #0, then it adds - // the local context ?m::0[inst:0 true] - lean_assert_eq(proc(F, context()), add_inst(m1, 0, True)(True)); - // In the following assertion, the normalizer has to use the local context - // because the metavariable m2 was defined in a context of size 1. - // Thus, it may contain the free variable #0. - expr m2 = menv->mk_metavar(context({{"x", Bool}})); - expr F2 = Fun({x, Bool}, m2(x))(True); - lean_assert_eq(proc(F2, context(), menv), add_inst(m2, 0, True)(True)); -} - -static void tst8() { - environment env; - init_test_frontend(env); - env->add_var("P", Int >> (Int >> Bool)); - expr P = Const("P"); - expr v0 = Var(0); - expr v1 = Var(1); - expr F = mk_pi("x", Int, Not(mk_lambda("x", Int, mk_exists(Int, mk_lambda("y", Int, P(v1, v0))))(v0))); - normalizer proc(env); - expr N1 = proc(F); - expr N2 = proc(deep_copy(F)); - std::cout << "F: " << F << "\n====>\n"; - std::cout << N1 << "\n"; - lean_assert_eq(N1, N2); -} - -static void tst9() { +static void tst5() { environment env; expr f = Const("f"); - env->add_var("f", Type() >> (Type() >> Type())); + env->add_var("f", Type >> (Type >> Type)); expr x = Const("x"); expr v = Const("v"); - expr F = Fun({x, Type()}, Let({v, Bool}, f(x, 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))); -} - -static void tst10() { - environment env; - init_test_frontend(env); - metavar_env menv; - context ctx({{"x", Bool}, {"y", Bool}}); - expr m = menv->mk_metavar(ctx); - ctx = extend(ctx, "z", none_expr(), m); - expr N = normalizer(env)(Var(0), ctx); - expr f = Const("f"); - metavar_env menv_copy1 = menv.copy(); - lean_verify(menv_copy1->assign(m, f(Var(0)))); - lean_assert_eq(menv_copy1->instantiate_metavars(N), f(Var(1))); - metavar_env menv_copy2 = menv.copy(); - lean_verify(menv_copy2->assign(m, f(Var(1)))); - lean_assert_eq(menv_copy2->instantiate_metavars(N), f(Var(2))); -} - -static void tst11() { - environment env; - metavar_env menv; - context ctx({{"A", Type()}}); - expr m1 = menv->mk_metavar(extend(ctx, "x", Type())); - expr x = Const("x"); - expr e = Fun({x, Type()}, m1); - expr T = Fun({x, Type()}, lift_free_vars(e, 0, 1)(x)); - context ctx2 = extend(ctx, "C", Type()); - expr T1 = lift_free_vars(T, 0, 1); - expr N = normalizer(env)(T1, ctx2, menv); - std::cout << m1 << " context: " << menv->get_context(m1) << "\n"; - std::cout << T1 << " AT " << ctx2 << "\n==>\n" << N << "\n"; - lean_verify(menv->assign(m1, Var(1))); - std::cout << menv->instantiate_metavars(T1) << "\n"; - std::cout << menv->instantiate_metavars(N) << "\n"; - lean_assert_eq(normalizer(env)(menv->instantiate_metavars(T1), ctx2), - menv->instantiate_metavars(N)); + lean_assert_eq(N, Fun({x, Type}, f(x, Bool))); } int main() { save_stack_info(); - register_modules(); tst_church_numbers(); tst1(); tst2(); tst3(); tst4(); tst5(); - tst6(); - tst7(); - tst8(); - tst9(); - tst10(); - tst11(); return has_violations() ? 1 : 0; }