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

Add support for semantic attachments. Remove expr_numeral

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-03 16:09:21 -07:00
parent 1fec8b0d5b
commit 0a679074f0
10 changed files with 96 additions and 78 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/deep_copy.cpp
View file

@ -23,7 +23,7 @@ class deep_copy_fn {
}
expr r;
switch (a.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
r = copy(a); break; // shallow copy is equivalent to deep copy for these ones.
case expr_kind::App: {
buffer<expr> new_args;

31
src/kernel/expr.cpp
View file

@ -29,10 +29,9 @@ expr_var::expr_var(unsigned idx):
expr_cell(expr_kind::Var, idx),
m_vidx(idx) {}
expr_const::expr_const(name const & n, unsigned pos):
expr_const::expr_const(name const & n):
expr_cell(expr_kind::Constant, n.hash()),
m_name(n),
m_pos(pos) {}
m_name(n) {}
expr_app::expr_app(unsigned num_args):
expr_cell(expr_kind::App, 0),
@ -90,9 +89,15 @@ expr_type::expr_type(level const & l):
}
expr_type::~expr_type() {
}
expr_numeral::expr_numeral(mpz const & n):
expr_cell(expr_kind::Numeral, n.hash()),
m_numeral(n) {}
expr_value::expr_value(value & v):
expr_cell(expr_kind::Value, v.hash()),
m_val(v) {
m_val.inc_ref();
}
expr_value::~expr_value() {
m_val.dec_ref();
}
void expr_cell::dealloc() {
switch (kind()) {
@ -102,7 +107,7 @@ void expr_cell::dealloc() {
case expr_kind::Lambda: delete static_cast<expr_lambda*>(this); break;
case expr_kind::Pi: delete static_cast<expr_pi*>(this); break;
case expr_kind::Type: delete static_cast<expr_type*>(this); break;
case expr_kind::Numeral: delete static_cast<expr_numeral*>(this); break;
case expr_kind::Value: delete static_cast<expr_value*>(this); break;
}
}
@ -136,7 +141,7 @@ class eq_fn {
// Remark: we ignore get_abs_name because we want alpha-equivalence
return apply(abst_domain(a), abst_domain(b)) && apply(abst_body(a), abst_body(b));
case expr_kind::Type: return ty_level(a) == ty_level(b);
case expr_kind::Numeral: return num_value(a) == num_value(b);
case expr_kind::Value: return to_value(a) == to_value(b);
}
lean_unreachable();
return false;
@ -185,7 +190,7 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
out << "(Type " << ty_level(a) << ")";
break;
}
case expr_kind::Numeral: out << num_value(a); break;
case expr_kind::Value: to_value(a).display(out); break;
}
return out;
}
@ -193,9 +198,9 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
expr copy(expr const & a) {
switch (a.kind()) {
case expr_kind::Var: return var(var_idx(a));
case expr_kind::Constant: return constant(const_name(a), const_pos(a));
case expr_kind::Constant: return constant(const_name(a));
case expr_kind::Type: return type(ty_level(a));
case expr_kind::Numeral: return numeral(num_value(a));
case expr_kind::Value: return to_expr(static_cast<expr_value*>(a.raw())->m_val);
case expr_kind::App: return app(num_args(a), begin_args(a));
case expr_kind::Lambda: return lambda(abst_name(a), abst_domain(a), abst_body(a));
case expr_kind::Pi: return pi(abst_name(a), abst_domain(a), abst_body(a));
@ -212,6 +217,8 @@ lean::format pp_aux(lean::expr const & a) {
return format{format("#"), format(static_cast<int>(var_idx(a)))};
case expr_kind::Constant:
return format(const_name(a));
case expr_kind::Value:
return to_value(a).pp();
case expr_kind::App:
{
format r;
@ -247,8 +254,6 @@ lean::format pp_aux(lean::expr const & a) {
return paren(format{format("Type "),
format(ss.str())});
}
case expr_kind::Numeral:
return format(num_value(a));
}
lean_unreachable();
return format();

74
src/kernel/expr.h
View file

@ -9,21 +9,22 @@ Author: Leonardo de Moura
#include <limits>
#include "rc.h"
#include "name.h"
#include "mpz.h"
#include "level.h"
#include "hash.h"
#include "buffer.h"
#include "format.h"
namespace lean {
class value;
/* =======================================
Expressions
expr ::= Var idx
| Constant name
| App [expr]
| Lambda name expr expr
| Pi name expr expr
| Type universe
| Numeral value
expr ::= Var idx
| Constant name
| Value value
| App [expr]
| Lambda name expr expr
| Pi name expr expr
| Type universe
TODO: add meta-variables, let, constructor references and match.
@ -33,7 +34,7 @@ The main API is divided in the following sections
- Accessors
- Miscellaneous
======================================= */
enum class expr_kind { Var, Constant, App, Lambda, Pi, Type, Numeral };
enum class expr_kind { Var, Constant, Value, App, Lambda, Pi, Type };
/**
\brief Base class used to represent expressions.
@ -92,14 +93,13 @@ public:
friend expr var(unsigned idx);
friend expr constant(name const & n);
friend expr constant(name const & n, unsigned pos);
friend expr to_expr(value & v);
friend expr app(unsigned num_args, expr const * args);
friend expr app(std::initializer_list<expr> const & l);
friend expr lambda(name const & n, expr const & t, expr const & e);
friend expr pi(name const & n, expr const & t, expr const & e);
friend expr prop();
friend expr type(level const & l);
friend expr numeral(mpz const & n);
friend bool eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
@ -122,11 +122,9 @@ public:
/** \brief Constants. */
class expr_const : public expr_cell {
name m_name;
unsigned m_pos; // position in the environment.
public:
expr_const(name const & n, unsigned pos = std::numeric_limits<unsigned>::max());
expr_const(name const & n);
name const & get_name() const { return m_name; }
unsigned get_pos() const { return m_pos; }
};
/** \brief Function Applications */
class expr_app : public expr_cell {
@ -170,33 +168,55 @@ public:
~expr_type();
level const & get_level() const { return m_level; }
};
/** \brief Numerals (efficient encoding using GMP numbers) */
class expr_numeral : public expr_cell {
mpz m_numeral;
/**
\brief Base class for semantic attachment cells.
*/
class value {
void dealloc() { delete this; }
MK_LEAN_RC();
public:
expr_numeral(mpz const & n);
mpz const & get_num() const { return m_numeral; }
value():m_rc(0) {}
virtual ~value() {}
virtual char const * kind() const = 0;
virtual expr get_type() const = 0;
virtual expr normalize(unsigned num_args, expr const * args) const = 0;
virtual bool operator==(value const & other) const = 0;
virtual void display(std::ostream & out) const = 0;
virtual format pp() const = 0;
virtual unsigned hash() const = 0;
};
/** \brief Semantic attachments */
class expr_value : public expr_cell {
value & m_val;
friend expr copy(expr const & a);
public:
expr_value(value & v);
~expr_value();
value const & get_value() const { return m_val; }
};
// =======================================
// =======================================
// Testers
inline bool is_var(expr_cell * e) { return e->kind() == expr_kind::Var; }
inline bool is_constant(expr_cell * e) { return e->kind() == expr_kind::Constant; }
inline bool is_value(expr_cell * e) { return e->kind() == expr_kind::Value; }
inline bool is_app(expr_cell * e) { return e->kind() == expr_kind::App; }
inline bool is_lambda(expr_cell * e) { return e->kind() == expr_kind::Lambda; }
inline bool is_pi(expr_cell * e) { return e->kind() == expr_kind::Pi; }
inline bool is_type(expr_cell * e) { return e->kind() == expr_kind::Type; }
inline bool is_numeral(expr_cell * e) { return e->kind() == expr_kind::Numeral; }
inline bool is_abstraction(expr_cell * e) { return is_lambda(e) || is_pi(e); }
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_value(expr const & e) { return e.kind() == expr_kind::Value; }
inline bool is_app(expr const & e) { return e.kind() == expr_kind::App; }
inline bool is_lambda(expr const & e) { return e.kind() == expr_kind::Lambda; }
inline bool is_pi(expr const & e) { return e.kind() == expr_kind::Pi; }
inline bool is_type(expr const & e) { return e.kind() == expr_kind::Type; }
inline bool is_numeral(expr const & e) { return e.kind() == expr_kind::Numeral; }
inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); }
// =======================================
@ -205,7 +225,7 @@ inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); }
inline expr var(unsigned idx) { return expr(new expr_var(idx)); }
inline expr constant(name const & n) { return expr(new expr_const(n)); }
inline expr constant(char const * n) { return constant(name(n)); }
inline expr constant(name const & n, unsigned pos) { return expr(new expr_const(n, pos)); }
inline expr to_expr(value & v) { return expr(new expr_value(v)); }
expr app(unsigned num_args, expr const * args);
inline expr app(expr const & e1, expr const & e2) { expr args[2] = {e1, e2}; return app(2, args); }
inline expr app(expr const & e1, expr const & e2, expr const & e3) { expr args[3] = {e1, e2, e3}; return app(3, args); }
@ -217,8 +237,6 @@ inline expr pi(name const & n, expr const & t, expr const & e) { return expr(new
inline expr pi(char const * n, expr const & t, expr const & e) { return pi(name(n), t, e); }
inline expr arrow(expr const & t, expr const & e) { return pi(name("_"), t, e); }
inline expr type(level const & l) { return expr(new expr_type(l)); }
inline expr numeral(mpz const & n) { return expr(new expr_numeral(n)); }
inline expr numeral(int n) { return numeral(mpz(n)); }
inline expr expr::operator()(expr const & a1) const { return app(*this, a1); }
inline expr expr::operator()(expr const & a1, expr const & a2) const { return app(*this, a1, a2); }
@ -235,7 +253,6 @@ inline expr_abstraction * to_abstraction(expr_cell * e) { lean_assert(is_abstrac
inline expr_lambda * to_lambda(expr_cell * e) { lean_assert(is_lambda(e)); return static_cast<expr_lambda*>(e); }
inline expr_pi * to_pi(expr_cell * e) { lean_assert(is_pi(e)); return static_cast<expr_pi*>(e); }
inline expr_type * to_type(expr_cell * e) { lean_assert(is_type(e)); return static_cast<expr_type*>(e); }
inline expr_numeral * to_numeral(expr_cell * e) { lean_assert(is_numeral(e)); return static_cast<expr_numeral*>(e); }
inline expr_var * to_var(expr const & e) { return to_var(e.raw()); }
inline expr_const * to_constant(expr const & e) { return to_constant(e.raw()); }
@ -244,7 +261,6 @@ inline expr_abstraction * to_abstraction(expr const & e) { return to_abstraction
inline expr_lambda * to_lambda(expr const & e) { return to_lambda(e.raw()); }
inline expr_pi * to_pi(expr const & e) { return to_pi(e.raw()); }
inline expr_type * to_type(expr const & e) { return to_type(e.raw()); }
inline expr_numeral * to_numeral(expr const & e) { return to_numeral(e.raw()); }
// =======================================
// =======================================
@ -254,21 +270,20 @@ inline bool is_shared(expr_cell * e) { return get_rc(e) > 1;
inline unsigned var_idx(expr_cell * e) { return to_var(e)->get_vidx(); }
inline bool is_var(expr_cell * e, unsigned i) { return is_var(e) && var_idx(e) == i; }
inline name const & const_name(expr_cell * e) { return to_constant(e)->get_name(); }
inline unsigned const_pos(expr_cell * e) { return to_constant(e)->get_pos(); }
inline value const & to_value(expr_cell * e) { lean_assert(is_value(e)); return static_cast<expr_value*>(e)->get_value(); }
inline unsigned num_args(expr_cell * e) { return to_app(e)->get_num_args(); }
inline expr const & arg(expr_cell * e, unsigned idx) { return to_app(e)->get_arg(idx); }
inline name const & abst_name(expr_cell * e) { return to_abstraction(e)->get_name(); }
inline expr const & abst_domain(expr_cell * e) { return to_abstraction(e)->get_domain(); }
inline expr const & abst_body(expr_cell * e) { return to_abstraction(e)->get_body(); }
inline level const & ty_level(expr_cell * e) { return to_type(e)->get_level(); }
inline mpz const & num_value(expr_cell * e) { return to_numeral(e)->get_num(); }
inline unsigned get_rc(expr const & e) { return e.raw()->get_rc(); }
inline bool is_shared(expr const & e) { return get_rc(e) > 1; }
inline unsigned var_idx(expr const & e) { return to_var(e)->get_vidx(); }
inline bool is_var(expr const & e, unsigned i) { return is_var(e) && var_idx(e) == i; }
inline name const & const_name(expr const & e) { return to_constant(e)->get_name(); }
inline unsigned const_pos(expr const & e) { return to_constant(e)->get_pos(); }
inline value const & to_value(expr const & e) { return to_value(e.raw()); }
inline unsigned num_args(expr const & e) { return to_app(e)->get_num_args(); }
inline expr const & arg(expr const & e, unsigned idx) { return to_app(e)->get_arg(idx); }
inline expr const * begin_args(expr const & e) { return to_app(e)->begin_args(); }
@ -277,7 +292,6 @@ inline name const & abst_name(expr const & e) { return to_abstractio
inline expr const & abst_domain(expr const & e) { return to_abstraction(e)->get_domain(); }
inline expr const & abst_body(expr const & e) { return to_abstraction(e)->get_body(); }
inline level const & ty_level(expr const & e) { return to_type(e)->get_level(); }
inline mpz const & num_value(expr const & e) { return to_numeral(e)->get_num(); }
// =======================================
// =======================================

4
src/kernel/free_vars.cpp
View file

@ -23,7 +23,7 @@ protected:
bool apply(expr const & e, unsigned offset) {
// handle easy cases
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
return false;
case expr_kind::Var:
return process_var(e, offset);
@ -44,7 +44,7 @@ protected:
bool result = false;
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Var:
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var:
// easy cases were already handled
lean_unreachable(); return false;
case expr_kind::App:

2
src/kernel/max_sharing.cpp
View file

@ -32,7 +32,7 @@ struct max_sharing_fn::imp {
return a;
}
switch (a.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
cache(a);
return a;
case expr_kind::App: {

36
src/kernel/normalize.cpp
View file

@ -18,18 +18,18 @@ Author: Leonardo de Moura
namespace lean {
class svalue;
typedef list<svalue> stack; //!< Normalization stack
typedef list<svalue> value_stack; //!< Normalization stack
enum class svalue_kind { Expr, Closure, BoundedVar };
/** \brief Stack value: simple expressions, closures and bounded variables. */
class svalue {
svalue_kind m_kind;
unsigned m_bvar;
expr m_expr;
stack m_ctx;
value_stack m_ctx;
public:
explicit svalue(expr const & e): m_kind(svalue_kind::Expr), m_expr(e) {}
explicit svalue(unsigned k): m_kind(svalue_kind::BoundedVar), m_bvar(k) {}
svalue(expr const & e, stack const & c):m_kind(svalue_kind::Closure), m_expr(e), m_ctx(c) { lean_assert(is_lambda(e)); }
explicit svalue(expr const & e): m_kind(svalue_kind::Expr), m_expr(e) {}
explicit svalue(unsigned k): m_kind(svalue_kind::BoundedVar), m_bvar(k) {}
svalue(expr const & e, value_stack const & c):m_kind(svalue_kind::Closure), m_expr(e), m_ctx(c) { lean_assert(is_lambda(e)); }
svalue_kind kind() const { return m_kind; }
@ -38,25 +38,25 @@ public:
bool is_bounded_var() const { return kind() == svalue_kind::BoundedVar; }
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; }
value_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; }
};
svalue_kind kind(svalue const & v) { return v.kind(); }
expr const & to_expr(svalue const & v) { return v.get_expr(); }
stack const & stack_of(svalue const & v) { return v.get_ctx(); }
unsigned to_bvar(svalue const & v) { return v.get_var_idx(); }
svalue_kind kind(svalue const & v) { return v.kind(); }
expr const & to_expr(svalue const & v) { return v.get_expr(); }
value_stack const & stack_of(svalue const & v) { return v.get_ctx(); }
unsigned to_bvar(svalue const & v) { return v.get_var_idx(); }
stack extend(stack const & s, svalue const & v) { return cons(v, s); }
value_stack extend(value_stack const & s, svalue const & v) { return cons(v, s); }
/** \brief Expression normalizer. */
class normalize_fn {
environment const & m_env;
context const & m_ctx;
svalue lookup(stack const & s, unsigned i, unsigned k) {
svalue lookup(value_stack const & s, unsigned i, unsigned k) {
unsigned j = i;
stack const * it1 = &s;
value_stack const * it1 = &s;
while (*it1) {
if (j == 0)
return head(*it1);
@ -75,7 +75,7 @@ class normalize_fn {
}
/** \brief Convert the closure \c a into an expression using the given stack in a context that contains \c k binders. */
expr reify_closure(expr const & a, stack const & s, unsigned k) {
expr reify_closure(expr const & a, value_stack const & s, unsigned k) {
lean_assert(is_lambda(a));
expr new_t = reify(normalize(abst_domain(a), s, k), k);
expr new_b = reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1);
@ -126,12 +126,12 @@ class normalize_fn {
}
/** \brief Normalize the expression \c a in a context composed of stack \c s and \c k binders. */
svalue normalize(expr const & a, stack const & s, unsigned k) {
svalue normalize(expr const & a, value_stack const & s, unsigned k) {
lean_trace("normalize", tout << "Normalize, k: " << k << "\n" << a << "\n";);
switch (a.kind()) {
case expr_kind::Var:
return lookup(s, var_idx(a), k);
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
return svalue(a);
case expr_kind::App: {
svalue f = normalize(arg(a, 0), s, k);
@ -142,7 +142,7 @@ class normalize_fn {
// beta reduction
expr const & fv = to_expr(f);
lean_trace("normalize", tout << "beta reduction...\n" << fv << "\n";);
stack new_s = extend(stack_of(f), normalize(arg(a, i), s, k));
value_stack new_s = extend(stack_of(f), normalize(arg(a, i), s, k));
f = normalize(abst_body(fv), new_s, k);
if (i == n - 1)
return f;
@ -177,7 +177,7 @@ public:
expr operator()(expr const & e) {
unsigned k = length(m_ctx);
return reify(normalize(e, stack(), k), k);
return reify(normalize(e, value_stack(), k), k);
}
};

2
src/kernel/replace.h
View file

@ -39,7 +39,7 @@ class replace_fn {
expr r = m_f(e, offset);
if (eqp(e, r)) {
switch (e.kind()) {
case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Constant: case expr_kind::Var:
case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant: case expr_kind::Var:
break;
case expr_kind::App:
r = update_app(e, [=](expr const & c) { return apply(c, offset); });

5
src/kernel/type_check.cpp
View file

@ -110,9 +110,8 @@ class infer_type_fn {
level l2 = infer_universe(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
return type(max(l1, l2));
}
case expr_kind::Numeral:
// TODO
return e;
case expr_kind::Value:
return to_value(e).get_type();
}
lean_unreachable();
return e;

16
src/tests/kernel/expr.cpp
View file

@ -18,7 +18,7 @@ using namespace lean;
void tst1() {
expr a;
a = numeral(mpz(10));
a = constant("a");
expr f;
f = var(0);
expr fa = f(a);
@ -40,7 +40,7 @@ void tst1() {
void tst1_pp() {
std::cerr << "=============== PP =====================\n";
expr a;
a = numeral(mpz(10));
a = constant("a");
expr f;
f = var(0);
expr fa = f(a);
@ -66,7 +66,7 @@ expr mk_dag(unsigned depth, bool _closed = false) {
unsigned depth1(expr const & e) {
switch (e.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
return 1;
case expr_kind::App: {
unsigned m = 0;
@ -83,7 +83,7 @@ unsigned depth1(expr const & e) {
// This is the fastest depth implementation in this file.
unsigned depth2(expr const & e) {
switch (e.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
return 1;
case expr_kind::App:
return
@ -107,7 +107,7 @@ unsigned depth3(expr const & e) {
unsigned c = p.second + 1;
todo.pop_back();
switch (e.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
m = std::max(c, m);
break;
case expr_kind::App: {
@ -168,7 +168,7 @@ 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::Numeral:
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
return 1;
case expr_kind::App:
return std::accumulate(begin_args(a), end_args(a), 1,
@ -232,7 +232,7 @@ void tst8() {
expr f = constant("f");
expr x = var(0);
expr a = constant("a");
expr n = numeral(mpz(10));
expr n = constant("n");
expr p = type(level());
expr y = var(1);
lean_assert(closed(a));
@ -316,7 +316,7 @@ void tst12() {
expr a = constant("a");
expr x = var(0);
expr t = type(level());
expr F = pi("y", t, lambda("x", t, f(f(f(x,a),numeral(10)),x)));
expr F = pi("y", t, lambda("x", t, f(f(f(x,a),constant("10")),x)));
expr G = deep_copy(F);
lean_assert(F == G);
lean_assert(!eqp(F, G));

2
src/tests/kernel/normalize.cpp
View file

@ -57,7 +57,7 @@ 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::Numeral:
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
return 1;
case expr_kind::App:
return std::accumulate(begin_args(a), end_args(a), 1,