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

Add some overloads

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-07-23 09:37:32 -07:00
parent 17834d531c
commit 90f498994a
3 changed files with 11 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/expr.cpp
View file

@ -184,7 +184,7 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
out << ")"; out << ")";
break; break;
case expr_kind::Lambda: out << "(fun (" << get_abs_name(a) << " : " << get_abs_type(a) << ") " << get_abs_expr(a) << ")"; break; case expr_kind::Lambda: out << "(fun (" << get_abs_name(a) << " : " << get_abs_type(a) << ") " << get_abs_expr(a) << ")"; break;
case expr_kind::Pi: out << "(forall (" << get_abs_name(a) << " : " << get_abs_type(a) << ") " << get_abs_expr(a) << ")"; break; case expr_kind::Pi: out << "(pi (" << get_abs_name(a) << " : " << get_abs_type(a) << ") " << get_abs_expr(a) << ")"; break;
case expr_kind::Prop: out << "Prop"; break; case expr_kind::Prop: out << "Prop"; break;
case expr_kind::Type: out << "Type"; break; case expr_kind::Type: out << "Type"; break;
case expr_kind::Numeral: out << get_numeral(a); break; case expr_kind::Numeral: out << get_numeral(a); break;

3
src/kernel/expr.h
View file

@ -229,6 +229,7 @@ inline bool is_sort(expr const & e) { return is_prop(e) || is_type(e); }
// Constructors // Constructors
inline expr var(unsigned idx) { return expr(new expr_var(idx)); } 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(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 constant(name const & n, unsigned pos) { return expr(new expr_const(n, pos)); }
expr app(unsigned num_args, expr const * args); 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 args[2] = {e1, e2}; return app(2, args); }
@ -236,7 +237,9 @@ inline expr app(expr const & e1, expr const & e2, expr const & e3) { expr args[3
inline expr app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { expr args[4] = {e1, e2, e3, e4}; return app(4, args); } inline expr app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { expr args[4] = {e1, e2, e3, e4}; return app(4, args); }
inline expr app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { expr args[5] = {e1, e2, e3, e4, e5}; return app(5, args); } inline expr app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { expr args[5] = {e1, e2, e3, e4, e5}; return app(5, args); }
inline expr lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); } inline expr lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); }
inline expr lambda(char const * n, expr const & t, expr const & e) { return lambda(name(n), t, e); }
inline expr pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); } inline expr pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
inline expr pi(char const * n, expr const & t, expr const & e) { return pi(name(n), t, e); }
inline expr prop() { return expr(new expr_prop()); } inline expr prop() { return expr(new expr_prop()); }
expr type(unsigned size, uvar const * vars); expr type(unsigned size, uvar const * vars);
inline expr type(uvar const & uv) { return type(1, &uv); } inline expr type(uvar const & uv) { return type(1, &uv); }

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

@ -24,13 +24,13 @@ void tst1() {
lean_assert(!eqp(fa, app(f, a))); lean_assert(!eqp(fa, app(f, a)));
lean_assert(app(fa, a) == app(f, a, a)); lean_assert(app(fa, a) == app(f, a, a));
std::cout << app(fa, fa, fa) << "\n"; std::cout << app(fa, fa, fa) << "\n";
std::cout << lambda(name("x"), prop(), var(0)) << "\n"; std::cout << lambda("x", prop(), var(0)) << "\n";
lean_assert(app(app(f, a), a) == app(f, a, a)); lean_assert(app(app(f, a), a) == app(f, a, a));
lean_assert(app(f, app(a, a)) != app(f, a, a)); lean_assert(app(f, app(a, a)) != app(f, a, a));
} }
expr mk_dag(unsigned depth) { expr mk_dag(unsigned depth) {
expr f = constant(name("f")); expr f = constant("f");
expr a = var(0); expr a = var(0);
while (depth > 0) { while (depth > 0) {
depth--; depth--;
@ -116,14 +116,14 @@ expr mk_big(expr f, unsigned depth, unsigned val) {
} }
void tst3() { void tst3() {
expr f = constant(name("f")); expr f = constant("f");
expr r1 = mk_big(f, 18, 0); expr r1 = mk_big(f, 18, 0);
expr r2 = mk_big(f, 18, 0); expr r2 = mk_big(f, 18, 0);
lean_verify(r1 == r2); lean_verify(r1 == r2);
} }
void tst4() { void tst4() {
expr f = constant(name("f")); expr f = constant("f");
expr a = var(0); expr a = var(0);
for (unsigned i = 0; i < 10000; i++) { for (unsigned i = 0; i < 10000; i++) {
a = app(f, a); a = app(f, a);
@ -160,7 +160,7 @@ unsigned count(expr const & a) {
} }
void tst5() { void tst5() {
expr f = constant(name("f")); expr f = constant("f");
{ {
expr r1 = mk_redundant_dag(f, 5); expr r1 = mk_redundant_dag(f, 5);
expr r2 = max_sharing(r1); expr r2 = max_sharing(r1);
@ -176,7 +176,7 @@ void tst5() {
} }
void tst6() { void tst6() {
expr f = constant(name("f")); expr f = constant("f");
expr r = mk_redundant_dag(f, 12); expr r = mk_redundant_dag(f, 12);
for (unsigned i = 0; i < 1000; i++) { for (unsigned i = 0; i < 1000; i++) {
r = max_sharing(r); r = max_sharing(r);
@ -188,7 +188,7 @@ void tst6() {
} }
void tst7() { void tst7() {
expr f = constant(name("f")); expr f = constant("f");
expr v = var(0); expr v = var(0);
expr a1 = max_sharing(app(f, v, v)); expr a1 = max_sharing(app(f, v, v));
expr a2 = max_sharing(app(f, v, v)); expr a2 = max_sharing(app(f, v, v));