michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel): normalizer

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-19 17:28:26 -08:00
parent eb046c11fb
commit 6baa59376c
6 changed files with 86 additions and 370 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/CMakeLists.txt
View file

@ -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

220
src/kernel/normalizer.cpp
View file

@ -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<expr> const & ) const { lean_unreachable(); } // LCOV_EXCL_LINE
virtual void write(serializer & ) const { lean_unreachable(); } // LCOV_EXCL_LINE
virtual expr expand1(buffer<expr> const & ) const { lean_unreachable(); }
virtual expr expand(buffer<expr> 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<closure const *>(&to_value(e)) != nullptr; }
closure const & to_closure(expr const & e) { lean_assert(is_closure(e)); return static_cast<closure const &>(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<closure const *>(&to_macro(e)) != nullptr; }
closure const & to_closure(expr const & e) { lean_assert(is_closure(e)); return static_cast<closure const &>(to_macro(e)); }
/** \brief Expression normalizer. */
class normalizer::imp {
typedef expr_map<expr> 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<cache> reset(m_cache);
flet<context> 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)) {
lean_assert(is_binder(e));
freset<cache> reset(m_cache);
flet<context> set(m_ctx, ctx);
expr new_d = reify(normalize(abst_domain(e), s, k), k);
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(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<expr> 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());
}
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<object> obj = env()->find_object(const_name(a));
if (obj && should_unfold(*obj, m_unfold_opaque)) {
if (should_unfold(obj)) {
freset<cache> 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<expr> 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<cache> reset(m_cache);
flet<context> 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<expr> 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<expr> reified_args;
for (auto arg : new_args) reified_args.push_back(reify(arg, k));
optional<expr> 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);
}
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<ro_metavar_env> 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<unsigned>::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<ro_metavar_env> 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); }
}

13
src/kernel/normalizer.h
View file

@ -7,13 +7,10 @@ Author: Leonardo de Moura
#pragma once
#include <memory>
#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<ro_metavar_env> 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);
}

14
src/kernel/object.h
View file

@ -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<object> const & obj, bool unfold_opaque) {
return obj && should_unfold(*obj, unfold_opaque);
}
inline bool should_unfold(optional<object> 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<object> const & obj) { return obj && should_unfold(*obj); }
}

6
src/tests/kernel/CMakeLists.txt
View file

@ -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})

197
src/tests/kernel/normalizer.cpp
View file

@ -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;
}