2013-07-25 02:36:54 +00:00
|
|
|
/*
|
|
|
|
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 <algorithm>
|
2013-07-30 08:39:29 +00:00
|
|
|
#include "normalize.h"
|
2013-07-25 02:36:54 +00:00
|
|
|
#include "expr.h"
|
2013-07-30 07:25:19 +00:00
|
|
|
#include "context.h"
|
|
|
|
#include "environment.h"
|
2013-07-26 19:37:13 +00:00
|
|
|
#include "free_vars.h"
|
2013-07-25 02:36:54 +00:00
|
|
|
#include "list.h"
|
|
|
|
#include "buffer.h"
|
|
|
|
#include "trace.h"
|
2013-07-26 02:13:45 +00:00
|
|
|
#include "exception.h"
|
2013-07-25 02:36:54 +00:00
|
|
|
|
|
|
|
namespace lean {
|
|
|
|
|
|
|
|
class value;
|
2013-07-30 08:39:29 +00:00
|
|
|
typedef list<value> stack; //!< Normalization stack
|
2013-07-26 02:13:45 +00:00
|
|
|
enum class value_kind { Expr, Closure, BoundedVar };
|
2013-07-25 02:36:54 +00:00
|
|
|
class value {
|
2013-07-30 08:39:29 +00:00
|
|
|
value_kind m_kind;
|
|
|
|
unsigned m_bvar;
|
|
|
|
expr m_expr;
|
|
|
|
stack m_ctx;
|
2013-07-25 02:36:54 +00:00
|
|
|
public:
|
2013-07-30 08:39:29 +00:00
|
|
|
explicit value(expr const & e):m_kind(value_kind::Expr), m_expr(e) {}
|
|
|
|
explicit value(unsigned k):m_kind(value_kind::BoundedVar), m_bvar(k) {}
|
|
|
|
value(expr const & e, stack const & c):m_kind(value_kind::Closure), m_expr(e), m_ctx(c) { lean_assert(is_lambda(e)); }
|
2013-07-25 02:36:54 +00:00
|
|
|
|
2013-07-30 08:39:29 +00:00
|
|
|
value_kind kind() const { return m_kind; }
|
2013-07-26 02:13:45 +00:00
|
|
|
|
|
|
|
bool is_expr() const { return kind() == value_kind::Expr; }
|
|
|
|
bool is_closure() const { return kind() == value_kind::Closure; }
|
|
|
|
bool is_bounded_var() const { return kind() == value_kind::BoundedVar; }
|
|
|
|
|
2013-07-30 08:39:29 +00:00
|
|
|
expr const & get_expr() const { lean_assert(is_expr() || is_closure()); return m_expr; }
|
|
|
|
stack const & get_ctx() const { lean_assert(is_closure()); return m_ctx; }
|
|
|
|
unsigned get_var_idx() const { lean_assert(is_bounded_var()); return m_bvar; }
|
2013-07-25 02:36:54 +00:00
|
|
|
};
|
|
|
|
|
2013-08-02 01:52:28 +00:00
|
|
|
value_kind kind(value const & v) { return v.kind(); }
|
|
|
|
expr const & to_expr(value const & v) { return v.get_expr(); }
|
|
|
|
stack const & stack_of(value const & v) { return v.get_ctx(); }
|
|
|
|
unsigned to_bvar(value const & v) { return v.get_var_idx(); }
|
2013-07-30 07:25:19 +00:00
|
|
|
|
2013-07-30 08:39:29 +00:00
|
|
|
stack extend(stack const & s, value const & v) { return cons(v, s); }
|
2013-07-25 02:36:54 +00:00
|
|
|
|
2013-07-30 07:25:19 +00:00
|
|
|
class normalize_fn {
|
|
|
|
environment const & m_env;
|
|
|
|
context const & m_ctx;
|
|
|
|
|
2013-07-30 08:39:29 +00:00
|
|
|
value lookup(stack const & s, unsigned i, unsigned k) {
|
|
|
|
unsigned j = i;
|
|
|
|
stack const * it1 = &s;
|
|
|
|
while (*it1) {
|
|
|
|
if (j == 0)
|
2013-07-30 07:25:19 +00:00
|
|
|
return head(*it1);
|
2013-07-30 08:39:29 +00:00
|
|
|
--j;
|
2013-07-30 07:25:19 +00:00
|
|
|
it1 = &tail(*it1);
|
|
|
|
}
|
2013-07-30 08:39:29 +00:00
|
|
|
context const & c = ::lean::lookup(m_ctx, j);
|
|
|
|
if (c) {
|
|
|
|
context_entry const & entry = head(c);
|
|
|
|
if (entry.get_body())
|
|
|
|
return value(::lean::normalize(entry.get_body(), m_env, tail(c)));
|
|
|
|
else
|
|
|
|
return value(length(c) - 1);
|
2013-07-25 02:36:54 +00:00
|
|
|
}
|
2013-07-30 07:25:19 +00:00
|
|
|
throw exception("unknown free variable");
|
2013-07-25 02:36:54 +00:00
|
|
|
}
|
2013-07-30 07:25:19 +00:00
|
|
|
|
2013-07-30 08:39:29 +00:00
|
|
|
expr reify_closure(expr const & a, stack const & c, unsigned k) {
|
2013-07-30 07:25:19 +00:00
|
|
|
lean_assert(is_lambda(a));
|
|
|
|
expr new_t = reify(normalize(abst_type(a), c, k), k);
|
|
|
|
expr new_b = reify(normalize(abst_body(a), extend(c, value(k)), k+1), k+1);
|
|
|
|
if (is_app(new_b)) {
|
|
|
|
// (lambda (x:T) (app f ... (var 0)))
|
|
|
|
// check eta-rule applicability
|
|
|
|
unsigned n = num_args(new_b);
|
|
|
|
if (is_var(arg(new_b, n - 1), 0) &&
|
|
|
|
std::all_of(begin_args(new_b),
|
|
|
|
end_args(new_b) - 1,
|
|
|
|
[](expr const & arg) { return !has_free_var(arg, 0); })) {
|
|
|
|
if (n == 2)
|
|
|
|
return lower_free_vars(arg(new_b, 0), 1);
|
|
|
|
else
|
|
|
|
return lower_free_vars(app(n - 1, begin_args(new_b)), 1);
|
|
|
|
}
|
|
|
|
return lambda(abst_name(a), new_t, new_b);
|
2013-07-30 08:39:29 +00:00
|
|
|
} else {
|
2013-07-30 07:25:19 +00:00
|
|
|
return lambda(abst_name(a), new_t, new_b);
|
|
|
|
}
|
2013-07-25 02:36:54 +00:00
|
|
|
}
|
2013-07-30 07:25:19 +00:00
|
|
|
|
|
|
|
expr reify(value const & v, unsigned k) {
|
|
|
|
lean_trace("normalize", tout << "Reify kind: " << static_cast<unsigned>(v.kind()) << "\n";
|
|
|
|
if (v.is_bounded_var()) tout << "#" << to_bvar(v); else tout << to_expr(v); tout << "\n";);
|
|
|
|
switch (v.kind()) {
|
|
|
|
case value_kind::Expr: return to_expr(v);
|
|
|
|
case value_kind::BoundedVar: return var(k - to_bvar(v) - 1);
|
2013-07-30 08:39:29 +00:00
|
|
|
case value_kind::Closure: return reify_closure(to_expr(v), stack_of(v), k);
|
2013-07-30 07:25:19 +00:00
|
|
|
}
|
|
|
|
lean_unreachable();
|
|
|
|
return expr();
|
2013-07-26 02:13:45 +00:00
|
|
|
}
|
2013-07-25 02:36:54 +00:00
|
|
|
|
2013-07-30 08:39:29 +00:00
|
|
|
value normalize(expr const & a, stack const & c, unsigned k) {
|
2013-07-30 07:25:19 +00:00
|
|
|
lean_trace("normalize", tout << "Normalize, k: " << k << "\n" << a << "\n";);
|
|
|
|
switch (a.kind()) {
|
|
|
|
case expr_kind::Var:
|
2013-07-30 08:39:29 +00:00
|
|
|
return lookup(c, var_idx(a), k);
|
2013-07-30 07:25:19 +00:00
|
|
|
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
|
|
|
|
return value(a);
|
|
|
|
case expr_kind::App: {
|
|
|
|
value f = normalize(arg(a, 0), c, k);
|
|
|
|
unsigned i = 1;
|
|
|
|
unsigned n = num_args(a);
|
|
|
|
while (true) {
|
|
|
|
if (f.is_closure()) {
|
|
|
|
// beta reduction
|
|
|
|
expr const & fv = to_expr(f);
|
|
|
|
lean_trace("normalize", tout << "beta reduction...\n" << fv << "\n";);
|
2013-07-30 08:39:29 +00:00
|
|
|
stack new_c = extend(stack_of(f), normalize(arg(a, i), c, k));
|
2013-07-30 07:25:19 +00:00
|
|
|
f = normalize(abst_body(fv), new_c, k);
|
|
|
|
if (i == n - 1)
|
|
|
|
return f;
|
|
|
|
i++;
|
|
|
|
}
|
|
|
|
else {
|
|
|
|
// TODO: support for interpreted symbols
|
|
|
|
buffer<expr> new_args;
|
|
|
|
new_args.push_back(reify(f, k));
|
|
|
|
for (; i < n; i++)
|
|
|
|
new_args.push_back(reify(normalize(arg(a, i), c, k), k));
|
|
|
|
return value(app(new_args.size(), new_args.data()));
|
|
|
|
}
|
2013-07-26 02:13:45 +00:00
|
|
|
}
|
2013-07-25 02:36:54 +00:00
|
|
|
}
|
2013-07-30 07:25:19 +00:00
|
|
|
case expr_kind::Lambda:
|
|
|
|
return value(a, c);
|
|
|
|
case expr_kind::Pi: {
|
|
|
|
expr new_t = reify(normalize(abst_type(a), c, k), k);
|
|
|
|
expr new_b = reify(normalize(abst_body(a), extend(c, value(k)), k+1), k+1);
|
|
|
|
return value(pi(abst_name(a), new_t, new_b));
|
|
|
|
}}
|
|
|
|
lean_unreachable();
|
|
|
|
return value(a);
|
2013-07-25 02:36:54 +00:00
|
|
|
}
|
|
|
|
|
2013-07-30 07:25:19 +00:00
|
|
|
public:
|
|
|
|
normalize_fn(environment const & env, context const & ctx):
|
|
|
|
m_env(env),
|
|
|
|
m_ctx(ctx) {
|
|
|
|
}
|
|
|
|
|
|
|
|
expr operator()(expr const & e) {
|
2013-07-30 08:39:29 +00:00
|
|
|
unsigned k = length(m_ctx);
|
|
|
|
return reify(normalize(e, stack(), k), k);
|
2013-07-30 07:25:19 +00:00
|
|
|
}
|
|
|
|
};
|
|
|
|
|
|
|
|
expr normalize(expr const & e, environment const & env, context const & ctx) {
|
|
|
|
return normalize_fn(env, ctx)(e);
|
2013-07-25 02:36:54 +00:00
|
|
|
}
|
|
|
|
}
|