From 14c899e7ca03f42e8549ff46bdc0bef2b2b65bf2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Jul 2013 19:36:54 -0700 Subject: [PATCH] Add normalize Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 3 +- src/kernel/expr.h | 1 + src/kernel/normalize.cpp | 131 ++++++++++++++++++++++++++++++++ src/kernel/normalize.h | 12 +++ src/tests/kernel/CMakeLists.txt | 3 + src/tests/kernel/normalize.cpp | 39 ++++++++++ 6 files changed, 188 insertions(+), 1 deletion(-) create mode 100644 src/kernel/normalize.cpp create mode 100644 src/kernel/normalize.h create mode 100644 src/tests/kernel/normalize.cpp diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index da35b2af0a..46331d21aa 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,2 +1,3 @@ -add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp instantiate.cpp deep_copy.cpp) +add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp + instantiate.cpp deep_copy.cpp normalize.cpp) target_link_libraries(kernel ${EXTRA_LIBS}) diff --git a/src/kernel/expr.h b/src/kernel/expr.h index d56e5fb394..99a4e73ef1 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -224,6 +224,7 @@ inline bool is_numeral(expr_cell * e) { return e->kind() == expr_kind::Numer inline bool is_abstraction(expr_cell * e) { return is_lambda(e) || is_pi(e); } inline bool is_sort(expr_cell * e) { return is_prop(e) || is_type(e); } +inline bool is_null(expr const & e) { return e.raw() == nullptr; } inline bool is_var(expr const & e) { return e.kind() == expr_kind::Var; } inline bool is_constant(expr const & e) { return e.kind() == expr_kind::Constant; } inline bool is_app(expr const & e) { return e.kind() == expr_kind::App; } diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp new file mode 100644 index 0000000000..e94a0f9eaf --- /dev/null +++ b/src/kernel/normalize.cpp @@ -0,0 +1,131 @@ +/* +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 "expr.h" +#include "list.h" +#include "buffer.h" +#include "trace.h" + +namespace lean { + +class value; +typedef list context; +class value { + expr m_expr; + context m_ctx; +public: + value() {} + explicit value(expr const & e):m_expr(e) {} + value(expr const & e, context const & c):m_expr(e), m_ctx(c) {} + + expr const & get_expr() const { return m_expr; } + context const & get_ctx() const { return m_ctx; } +}; + +expr const & to_expr(value const & v) { return v.get_expr(); } +context const & ctx_of(value const & v) { return v.get_ctx(); } + +bool lookup(context const & c, unsigned i, value & r) { + context const * curr = &c; + while (!is_nil(*curr)) { + if (i == 0) { + r = head(*curr); + return !is_null(to_expr(r)); + } + --i; + curr = &tail(*curr); + } + return false; +} + +context extend(context const & c, value const & v = value()) { return cons(v, c); } + +value normalize(expr const & a, context const & c); +expr expand(value const & v); + +expr expand(expr const & a, context const & c) { + if (is_lambda(a)) { + expr new_t = to_expr(normalize(abst_type(a), c)); + expr new_b = expand(normalize(abst_body(a), extend(c))); + if (is_app(new_b)) { + // (lambda (x:T) (app f ... (var 0))) + // check eta-rule applicability + unsigned n = num_args(new_b); + lean_assert(n >= 2); + expr const & last_arg = arg(new_b, n - 1); + if (is_var(last_arg) && var_idx(last_arg) == 0) { + // FIXME: I have to shift the variables in new_b + if (n == 2) + return arg(new_b, 0); + else + return app(n - 1, begin_args(new_b)); + } + } + return lambda(abst_name(a), new_t, new_b); + } + else { + return a; + } +} + +expr expand(value const & v) { + return expand(to_expr(v), ctx_of(v)); +} + +value normalize(expr const & a, context const & c) { + lean_trace("normalize", tout << a << "\n";); + switch (a.kind()) { + case expr_kind::Var: { + value r; + if (lookup(c, var_idx(a), r)) + return r; + else + return value(a); + } + case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral: + return value(a); + case expr_kind::App: { + value f = normalize(arg(a, 0), c); + unsigned i = 1; + unsigned n = num_args(a); + while (true) { + expr const & fv = to_expr(f); + lean_trace("normalize", tout << "fv: " << fv << "\ni: " << i << "\n";); + switch (fv.kind()) { + case expr_kind::Lambda: { + // beta reduction + value a_v = normalize(arg(a, i), c); + f = normalize(abst_body(fv), extend(ctx_of(f), a_v)); + if (i == n - 1) + return f; + i++; + break; + } + default: { + // TODO: support for interpreted symbols + buffer new_args; + new_args.push_back(fv); + for (; i < n; i++) + new_args.push_back(expand(normalize(arg(a, i), c))); + return value(app(new_args.size(), new_args.data())); + }} + } + } + case expr_kind::Lambda: + return value(a, c); + case expr_kind::Pi: { + expr new_t = to_expr(normalize(abst_type(a), c)); + expr new_b = to_expr(normalize(abst_body(a), extend(c))); + return value(pi(abst_name(a), new_t, new_b)); + }} + return value(a); +} + +expr normalize(expr const & e) { + return expand(normalize(e, context())); +} +} diff --git a/src/kernel/normalize.h b/src/kernel/normalize.h new file mode 100644 index 0000000000..11d1d5b1e7 --- /dev/null +++ b/src/kernel/normalize.h @@ -0,0 +1,12 @@ +/* +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 "expr.h" + +namespace lean { +expr normalize(expr const & e); +} diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt index 7c97ab44d7..a928c891a5 100644 --- a/src/tests/kernel/CMakeLists.txt +++ b/src/tests/kernel/CMakeLists.txt @@ -1,3 +1,6 @@ add_executable(expr_tst expr.cpp) target_link_libraries(expr_tst ${EXTRA_LIBS}) add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr_tst) +add_executable(normalize normalize.cpp) +target_link_libraries(normalize ${EXTRA_LIBS}) +add_test(normalize ${CMAKE_CURRENT_BINARY_DIR}/normalize) diff --git a/src/tests/kernel/normalize.cpp b/src/tests/kernel/normalize.cpp new file mode 100644 index 0000000000..dbe23c643d --- /dev/null +++ b/src/tests/kernel/normalize.cpp @@ -0,0 +1,39 @@ +/* +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 "normalize.h" +#include "trace.h" +#include "test.h" +using namespace lean; + +static void eval(expr const & e) { + std::cout << e << " --> " << normalize(e) << "\n"; +} + +static void tst1() { + expr f = constant("f"); + expr a = constant("a"); + expr b = constant("b"); + expr x = var(0); + expr y = var(1); + expr t = prop(); + eval(app(lambda("x", t, x), a)); + eval(app(lambda("x", t, x), a, b)); + eval(lambda("x", t, f(x))); + eval(lambda("y", t, lambda("x", t, f(y, x)))); + eval(app(lambda("x", t, + app(lambda("f", t, + app(var(0), b)), + lambda("g", t, f(var(1))))), + a)); +} + +int main() { + enable_trace("normalize"); + continue_on_violation(true); + tst1(); + return has_violations() ? 1 : 0; +}