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

refactor(beta_reduction): move beta reduction functions to the kernel, delete reduce.cpp file and tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-23 15:44:26 -07:00
parent c1e451151a
commit f1e0d6ec29
12 changed files with 59 additions and 131 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/elaborator.cpp
View file

@ -19,7 +19,6 @@ Author: Leonardo de Moura
#include "kernel/metavar.h"
#include "kernel/printer.h"
#include "library/placeholder.h"
#include "library/reduce.h"
#include "library/update_expr.h"
#include "library/expr_pair.h"
#include "frontends/lean/frontend.h"

48
src/kernel/instantiate.cpp
View file

@ -64,4 +64,52 @@ expr instantiate(expr const & e, unsigned n, expr const * s) {
expr instantiate(expr const & e, unsigned i, expr const & s) {
return instantiate(e, i, 1, &s);
}
bool is_head_beta(expr const & t) {
return is_app(t) && is_lambda(arg(t, 0));
}
expr head_beta_reduce(expr const & t) {
if (!is_head_beta(t)) {
return t;
} else {
unsigned num = num_args(t);
unsigned num1 = num - 1;
expr const * f = &arg(t, 0);
lean_assert(is_lambda(*f));
unsigned m = 1;
while (is_lambda(abst_body(*f)) && m < num1) {
f = &abst_body(*f);
m++;
}
lean_assert(m <= num1);
expr r = instantiate(abst_body(*f), m, &arg(t, 1));
if (m == num1) {
return r;
} else {
buffer<expr> args;
args.push_back(r);
m++;
for (; m < num; m++)
args.push_back(arg(t, m));
return mk_app(args.size(), args.data());
}
}
}
expr beta_reduce(expr t) {
auto f = [=](expr const & m, unsigned) -> expr {
if (is_head_beta(m))
return head_beta_reduce(m);
else
return m;
};
while (true) {
expr new_t = replace_fn<decltype(f)>(f)(t);
if (new_t == t)
return new_t;
else
t = new_t;
}
}
}

4
src/kernel/instantiate.h
View file

@ -29,4 +29,8 @@ inline expr instantiate(expr const & e, expr const & s) { return instantiate(e,
\brief Replace free variable \c i with \c s in \c e.
*/
expr instantiate(expr const & e, unsigned i, expr const & s);
bool is_head_beta(expr const & t);
expr head_beta_reduce(expr const & t);
expr beta_reduce(expr t);
}

4
src/library/CMakeLists.txt
View file

@ -1,5 +1,5 @@
add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
context_to_lambda.cpp state.cpp update_expr.cpp reduce.cpp
type_inferer.cpp placeholder.cpp expr_lt.cpp)
context_to_lambda.cpp state.cpp update_expr.cpp type_inferer.cpp
placeholder.cpp expr_lt.cpp)
target_link_libraries(library ${LEAN_LIBS})

1
src/library/elaborator/elaborator.cpp
View file

@ -16,7 +16,6 @@ Author: Leonardo de Moura
#include "kernel/builtin.h"
#include "library/type_inferer.h"
#include "library/update_expr.h"
#include "library/reduce.h"
#include "library/elaborator/elaborator.h"
#include "library/elaborator/elaborator_justification.h"

97
src/library/reduce.cpp
View file

@ -1,97 +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 "util/name_set.h"
#include "kernel/context.h"
#include "kernel/instantiate.h"
#include "kernel/environment.h"
#include "kernel/free_vars.h"
#include "kernel/replace.h"
#include "library/update_expr.h"
namespace lean {
bool is_head_beta(expr const & t) {
return is_app(t) && is_lambda(arg(t, 0));
}
expr head_beta_reduce(expr const & t) {
if (!is_head_beta(t)) {
return t;
} else {
unsigned num = num_args(t);
unsigned num1 = num - 1;
expr const * f = &arg(t, 0);
lean_assert(is_lambda(*f));
unsigned m = 1;
while (is_lambda(abst_body(*f)) && m < num1) {
f = &abst_body(*f);
m++;
}
lean_assert(m <= num1);
expr r = instantiate(abst_body(*f), m, &arg(t, 1));
if (m == num1) {
return r;
} else {
buffer<expr> args;
args.push_back(r);
m++;
for (; m < num; m++)
args.push_back(arg(t, m));
return mk_app(args.size(), args.data());
}
}
}
expr beta_reduce(expr t) {
auto f = [=](expr const & m, unsigned) -> expr {
if (is_head_beta(m))
return head_beta_reduce(m);
else
return m;
};
while (true) {
expr new_t = replace_fn<decltype(f)>(f)(t);
if (new_t == t)
return new_t;
else
t = new_t;
}
}
expr head_reduce(expr const & t, environment const & e, context const & c, name_set const * defs) {
if (is_head_beta(t)) {
return head_beta_reduce(t);
} else if (is_app(t)) {
expr f = arg(t, 0);
if (is_head_beta(f) || is_let(f) || is_constant(f) || is_var(f)) {
expr new_f = head_reduce(f, e, c, defs);
if (!is_eqp(f, new_f))
return update_app(t, 0, new_f);
else
return t;
} else {
return t;
}
} else if (is_var(t)) {
auto p = lookup_ext(c, var_idx(t));
context_entry const & ce = p.first;
if (ce.get_body()) {
return lift_free_vars(ce.get_body(), c.size() - p.second.size());
} else {
return t;
}
} else if (is_let(t)) {
return instantiate(let_body(t), let_value(t));
} else if (is_constant(t)) {
name const & n = const_name(t);
if (defs == nullptr || defs->find(n) != defs->end()) {
object const & obj = e.find_object(n);
if (obj && obj.is_definition() && !obj.is_opaque())
return obj.get_value();
}
}
return t;
}
}

17
src/library/reduce.h
View file

@ -1,17 +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 "util/name_set.h"
#include "kernel/context.h"
#include "kernel/environment.h"
namespace lean {
bool is_head_beta(expr const & t);
expr head_beta_reduce(expr const & t);
expr beta_reduce(expr t);
expr head_reduce(expr const & t, environment const & e, context const & c = context(), name_set const * defs = nullptr);
}

1
src/library/type_inferer.cpp
View file

@ -14,7 +14,6 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/free_vars.h"
#include "kernel/metavar.h"
#include "library/reduce.h"
#include "library/type_inferer.h"
namespace lean {

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

@ -31,3 +31,6 @@ add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs)
add_executable(metavar metavar.cpp)
target_link_libraries(metavar ${EXTRA_LIBS})
add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar)
add_executable(instantiate instantiate.cpp)
target_link_libraries(instantiate ${EXTRA_LIBS})
add_test(instantiate ${CMAKE_CURRENT_BINARY_DIR}/instantiate)

9
src/tests/library/reduce.cpp → src/tests/kernel/instantiate.cpp
View file

@ -6,7 +6,7 @@ Author: Leonardo de Moura
*/
#include "util/test.h"
#include "kernel/abstract.h"
#include "library/reduce.h"
#include "kernel/instantiate.h"
using namespace lean;
static void tst1() {
@ -36,19 +36,12 @@ static void tst1() {
}
static void tst2() {
environment env;
expr x = Const("x");
expr a = Const("a");
expr f = Const("f");
expr N = Const("N");
expr F1 = Let({x, a}, f(x));
lean_assert_eq(head_beta_reduce(F1), F1);
lean_assert_eq(head_reduce(F1, env), f(a));
context ctx;
ctx = extend(ctx, "x", N, f(a));
ctx = extend(ctx, "y", N, f(Var(0)));
std::cout << head_reduce(Var(0), env, ctx) << "\n";
lean_assert_eq(head_reduce(Var(0), env, ctx), f(Var(1)));
}
int main() {

3
src/tests/library/CMakeLists.txt
View file

@ -13,9 +13,6 @@ add_test(expr_lt ${CMAKE_CURRENT_BINARY_DIR}/expr_lt)
add_executable(deep_copy deep_copy.cpp)
target_link_libraries(deep_copy ${EXTRA_LIBS})
add_test(deep_copy ${CMAKE_CURRENT_BINARY_DIR}/deep_copy)
add_executable(reduce reduce.cpp)
target_link_libraries(reduce ${EXTRA_LIBS})
add_test(reduce ${CMAKE_CURRENT_BINARY_DIR}/reduce)
add_executable(arith_tst arith.cpp)
target_link_libraries(arith_tst ${EXTRA_LIBS})
add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst)

2
src/tests/library/elaborator/elaborator.cpp
View file

@ -10,8 +10,8 @@ Author: Leonardo de Moura
#include "kernel/abstract.h"
#include "kernel/kernel_exception.h"
#include "kernel/normalizer.h"
#include "kernel/instantiate.h"
#include "library/basic_thms.h"
#include "library/reduce.h"
#include "library/placeholder.h"
#include "library/arith/arith.h"
#include "library/all/all.h"