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

Add type checker. Fix normalization with non-empty context

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-07-30 01:39:29 -07:00
parent bed5f09907
commit e220d7c525
15 changed files with 377 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/CMakeLists.txt
View file

@ -1,3 +1,4 @@
add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp
instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp)
instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp
type_check.cpp context.cpp)
target_link_libraries(kernel ${EXTRA_LIBS})

35
src/kernel/context.cpp Normal file
View file

@ -0,0 +1,35 @@
/*
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 "context.h"
#include "exception.h"
namespace lean {
std::ostream & operator<<(std::ostream & out, context const & c) {
if (c) {
if (tail(c))
out << tail(c) << "\n";
context_entry const & e = head(c);
if (e.get_name().is_anonymous())
out << "_";
else
out << e.get_name();
out << " : " << e.get_type();
}
return out;
}
context const & lookup(context const & c, unsigned i) {
context const * it1 = &c;
while (*it1) {
if (i == 0)
return *it1;
--i;
it1 = &tail(*it1);
}
throw exception("unknown free variable");
}
}

25
src/kernel/context.h
View file

@ -9,19 +9,28 @@ Author: Leonardo de Moura
#include "list.h"
namespace lean {
class context_entry;
typedef list<context_entry> context;
class context_entry {
name m_name;
expr m_type;
expr m_body;
public:
name m_name;
expr m_type;
expr m_body;
friend context extend(context const & c, name const & n, expr const & t, expr const & b);
friend context extend(context const & c, name const & n, expr const & t);
context_entry(name const & n, expr const & t, expr const & b):m_name(n), m_type(t), m_body(b) {}
context_entry(expr const & t, expr const & b):m_type(t), m_body(b) {}
explicit context_entry(expr const & t):m_type(t) {}
context_entry(name const & n, expr const & t):m_name(n), m_type(t) {}
public:
~context_entry() {}
name const & get_name() const { return m_name; }
expr const & get_type() const { return m_type; }
expr const & get_body() const { return m_body; }
};
typedef list<context_entry> context;
context extend(context const & c, context_entry const & e) { return cons(e, c); }
context const & lookup(context const & c, unsigned i);
inline context extend(context const & c, name const & n, expr const & t, expr const & b) {
return context(context_entry(n, t, b), c);
}
inline context extend(context const & c, name const & n, expr const & t) {
return context(context_entry(n, t), c);
}
std::ostream & operator<<(std::ostream & out, context const & c);
}

17
src/kernel/expr.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <vector>
#include <sstream>
#include "expr.h"
#include "free_vars.h"
#include "sets.h"
#include "hash.h"
#include "format.h"
@ -164,8 +165,20 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
out << ")";
break;
case expr_kind::Lambda: out << "(fun (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")"; break;
case expr_kind::Pi: out << "(pi (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")"; break;
case expr_kind::Type: out << "(Type " << ty_level(a) << ")"; break;
case expr_kind::Pi:
if (has_free_var(abst_body(a), 0))
out << "(pi (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")";
else
out << abst_type(a) << " -> " << abst_body(a);
break;
case expr_kind::Type: {
level const & l = ty_level(a);
if (is_uvar(l) && uvar_idx(l) == 0)
out << "Type";
else
out << "(Type " << ty_level(a) << ")";
break;
}
case expr_kind::Numeral: out << num_value(a); break;
}
return out;

6
src/kernel/expr.h
View file

@ -84,10 +84,12 @@ public:
expr & operator=(expr && s) { LEAN_MOVE_REF(expr, s); }
expr_kind kind() const { return m_ptr->kind(); }
unsigned hash() const { return m_ptr->hash(); }
unsigned hash() const { return m_ptr ? m_ptr->hash() : 23; }
expr_cell * raw() const { return m_ptr; }
operator bool() const { return m_ptr != nullptr; }
friend expr var(unsigned idx);
friend expr constant(name const & n);
friend expr constant(name const & n, unsigned pos);
@ -188,7 +190,6 @@ 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_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; }
@ -214,6 +215,7 @@ inline expr lambda(name const & n, expr const & t, expr const & e) { return expr
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(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)); }

14
src/kernel/free_vars.cpp
View file

@ -105,4 +105,18 @@ expr lower_free_vars(expr const & e, unsigned d) {
return replace_fn<decltype(f)>(f)(e);
}
expr lift_free_vars(expr const & e, unsigned d) {
if (d == 0)
return e;
auto f = [=](expr const & e, unsigned offset) -> expr {
if (is_var(e) && var_idx(e) >= offset) {
return var(var_idx(e) + d);
}
else {
return e;
}
};
return replace_fn<decltype(f)>(f)(e);
}
}

5
src/kernel/free_vars.h
View file

@ -34,4 +34,9 @@ bool has_free_var(expr const & e, unsigned low, unsigned high);
\pre !has_free_var(e, 0, d)
*/
expr lower_free_vars(expr const & e, unsigned d);
/**
\brief Lift free variables in \c e by d.
*/
expr lift_free_vars(expr const & e, unsigned d);
}

2
src/kernel/level.cpp
View file

@ -92,7 +92,7 @@ bool operator==(level const & l1, level const & l2) {
std::ostream & operator<<(std::ostream & out, level const & l) {
switch (kind(l)) {
case level_kind::UVar: out << uvar_name(l); return out;
case level_kind::Lift: out << lift_of(l) << "+" << lift_offset(l); return out;
case level_kind::Lift: out << lift_of(l) << "+" << lift_offset(l); return out;
case level_kind::Max: out << "(max " << max_level1(l) << " " << max_level2(l) << ")"; return out;
}
return out;

87
src/kernel/normalize.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include "normalize.h"
#include "expr.h"
#include "context.h"
#include "environment.h"
@ -17,70 +18,61 @@ Author: Leonardo de Moura
namespace lean {
class value;
typedef list<value> local_context;
typedef list<value> stack; //!< Normalization stack
enum class value_kind { Expr, Closure, BoundedVar };
class value {
unsigned m_kind:2;
unsigned m_bvar:30;
expr m_expr;
local_context m_ctx;
value_kind m_kind;
unsigned m_bvar;
expr m_expr;
stack m_ctx;
public:
value() {}
explicit value(expr const & e):m_kind(static_cast<unsigned>(value_kind::Expr)), m_expr(e) {}
explicit value(unsigned k):m_kind(static_cast<unsigned>(value_kind::BoundedVar)), m_bvar(k) {}
value(expr const & e, local_context const & c):
m_kind(static_cast<unsigned>(value_kind::Closure)),
m_expr(e),
m_ctx(c) {
lean_assert(is_lambda(e));
}
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)); }
value_kind kind() const { return static_cast<value_kind>(m_kind); }
value_kind kind() const { return m_kind; }
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; }
expr const & get_expr() const { lean_assert(is_expr() || is_closure()); return m_expr; }
local_context const & get_ctx() const { lean_assert(is_closure()); return m_ctx; }
unsigned get_var_idx() const { lean_assert(is_bounded_var()); return m_bvar; }
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; }
};
value_kind kind(value const & v) { return v.kind(); }
expr const & to_expr(value const & v) { return v.get_expr(); }
local_context const & ctx_of(value const & v) { return v.get_ctx(); }
unsigned to_bvar(value const & v) { return v.get_var_idx(); }
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(); }
local_context extend(local_context const & c, value const & v) { return cons(v, c); }
stack extend(stack const & s, value const & v) { return cons(v, s); }
class normalize_fn {
environment const & m_env;
context const & m_ctx;
value lookup(local_context const & c, unsigned i) {
local_context const * it1 = &c;
while (!is_nil(*it1)) {
if (i == 0)
value lookup(stack const & s, unsigned i, unsigned k) {
unsigned j = i;
stack const * it1 = &s;
while (*it1) {
if (j == 0)
return head(*it1);
--i;
--j;
it1 = &tail(*it1);
}
context const * it2 = &m_ctx;
while (!is_nil(*it2)) {
if (i == 0) {
expr const & b = head(*it2).get_body();
if (!is_null(b))
return value(b);
else break;
}
--i;
it2 = &tail(*it2);
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);
}
throw exception("unknown free variable");
}
expr reify_closure(expr const & a, local_context const & c, unsigned k) {
expr reify_closure(expr const & a, stack const & c, unsigned k) {
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);
@ -98,8 +90,7 @@ class normalize_fn {
return lower_free_vars(app(n - 1, begin_args(new_b)), 1);
}
return lambda(abst_name(a), new_t, new_b);
}
else {
} else {
return lambda(abst_name(a), new_t, new_b);
}
}
@ -110,17 +101,17 @@ class normalize_fn {
switch (v.kind()) {
case value_kind::Expr: return to_expr(v);
case value_kind::BoundedVar: return var(k - to_bvar(v) - 1);
case value_kind::Closure: return reify_closure(to_expr(v), ctx_of(v), k);
case value_kind::Closure: return reify_closure(to_expr(v), stack_of(v), k);
}
lean_unreachable();
return expr();
}
value normalize(expr const & a, local_context const & c, unsigned k) {
value normalize(expr const & a, stack const & c, unsigned k) {
lean_trace("normalize", tout << "Normalize, k: " << k << "\n" << a << "\n";);
switch (a.kind()) {
case expr_kind::Var:
return lookup(c, var_idx(a));
return lookup(c, var_idx(a), k);
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
return value(a);
case expr_kind::App: {
@ -132,7 +123,7 @@ class normalize_fn {
// beta reduction
expr const & fv = to_expr(f);
lean_trace("normalize", tout << "beta reduction...\n" << fv << "\n";);
local_context new_c = extend(ctx_of(f), normalize(arg(a, i), c, k));
stack new_c = extend(stack_of(f), normalize(arg(a, i), c, k));
f = normalize(abst_body(fv), new_c, k);
if (i == n - 1)
return f;
@ -166,12 +157,12 @@ public:
}
expr operator()(expr const & e) {
return reify(normalize(e, local_context(), 0), 0);
unsigned k = length(m_ctx);
return reify(normalize(e, stack(), k), k);
}
};
expr normalize(expr const & e, environment const & env, context const & ctx) {
return normalize_fn(env, ctx)(e);
}
}

126
src/kernel/type_check.cpp Normal file
View file

@ -0,0 +1,126 @@
/*
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 <sstream>
#include "type_check.h"
#include "normalize.h"
#include "free_vars.h"
#include "exception.h"
#include "trace.h"
namespace lean {
class infer_type_fn {
environment const & m_env;
expr normalize(expr const & e, context const & ctx) {
return ::lean::normalize(e, m_env, ctx);
}
expr lookup(context const & c, unsigned i) {
context const & def_c = ::lean::lookup(c, i);
return lift_free_vars(head(def_c).get_type(), length(c) - length(def_c));
}
level infer_universe(expr const & t, context const & ctx) {
lean_trace("type_check", tout << "infer universe\n" << t << "\n";);
expr u = normalize(infer_type(t, ctx), ctx);
if (is_type(u))
return ty_level(u);
std::ostringstream buffer;
buffer << "type expected, in context:\n" << ctx << "\ngiven:\n" << t;
throw exception(buffer.str());
}
expr infer_pi(expr const & e, context const & ctx) {
lean_trace("type_check", tout << "infer pi\n" << e << "\n";);
expr p = normalize(infer_type(e, ctx), ctx);
if (is_pi(p))
return p;
std::ostringstream buffer;
buffer << "function expected, in context:\n" << ctx << "\ngiven:\n" << e;
throw exception(buffer.str());
}
bool check_type_core(expr const & expected, expr const & given) {
if (expected == given)
return true;
if (is_type(expected) && is_type(given)) {
if (m_env.is_ge(ty_level(expected), ty_level(given)))
return true;
}
return false;
}
void check_type(expr const & e, unsigned i, expr const & expected, expr const & given, context const & ctx) {
if (check_type_core(expected, given))
return;
expr e_n = normalize(expected, ctx);
expr g_n = normalize(given, ctx);
if (check_type_core(e_n, g_n))
return;
std::ostringstream buffer;
buffer << "type mismatch at argument " << i << " of\n" << e
<< "\nexpected type:\n" << expected
<< "\ngiven type:\n" << given << "\nin context:\n" << ctx;;
throw exception(buffer.str());
}
expr infer_type(expr const & e, context const & ctx) {
lean_trace("type_check", tout << "infer type\n" << e << "\n" << ctx << "\n";);
switch (e.kind()) {
case expr_kind::Constant:
// TODO
return e;
case expr_kind::Var: return lookup(ctx, var_idx(e));
case expr_kind::Type: return type(ty_level(e) + 1);
case expr_kind::App: {
expr f_t = infer_pi(arg(e, 0), ctx);
unsigned i = 1;
unsigned num = num_args(e);
lean_assert(num >= 2);
while (true) {
expr const & c = arg(e, i);
expr c_t = infer_type(c, ctx);
check_type(e, i, abst_type(f_t), c_t, ctx);
f_t = normalize(abst_body(f_t), extend(ctx, abst_name(f_t), c_t));
i++;
if (i == num)
return f_t;
if (!is_pi(f_t))
throw exception("function expected");
}
}
case expr_kind::Lambda: {
infer_universe(abst_type(e), ctx);
expr t = infer_type(abst_body(e), extend(ctx, abst_name(e), abst_type(e)));
return pi(abst_name(e), abst_type(e), t);
}
case expr_kind::Pi: {
level l1 = infer_universe(abst_type(e), ctx);
level l2 = infer_universe(abst_body(e), extend(ctx, abst_name(e), abst_type(e)));
return type(max(l1, l2));
}
case expr_kind::Numeral:
// TODO
return e;
}
lean_unreachable();
return e;
}
public:
infer_type_fn(environment const & env):
m_env(env) {
}
expr operator()(expr const & e, context const & ctx) {
return infer_type(e, ctx);
}
};
expr infer_type(expr const & e, environment const & env, context const & ctx) {
return infer_type_fn(env)(e, ctx);
}
}

14
src/kernel/type_check.h Normal file
View file

@ -0,0 +1,14 @@
/*
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"
#include "environment.h"
#include "context.h"
namespace lean {
expr infer_type(expr const & e, environment const & env, context const & ctx = context());
}

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

@ -16,3 +16,6 @@ add_test(level ${CMAKE_CURRENT_BINARY_DIR}/level)
add_executable(replace replace.cpp)
target_link_libraries(replace ${EXTRA_LIBS})
add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace)
add_executable(type_check type_check.cpp)
target_link_libraries(type_check ${EXTRA_LIBS})
add_test(type_check ${CMAKE_CURRENT_BINARY_DIR}/type_check)

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

@ -21,7 +21,6 @@ static expr t() { return constant("t"); }
static expr lam(expr const & e) { return lambda("_", t(), e); }
static expr lam(expr const & t, expr const & e) { return lambda("_", t, e); }
static expr v(unsigned i) { return var(i); }
static expr arrow(expr const & d, expr const & r) { return pi("_", d, r); }
static expr zero() {
// fun (t : T) (s : t -> t) (z : t) z
return lam(t(), lam(arrow(v(0), v(0)), lam(v(1), v(0))));
@ -94,10 +93,10 @@ static void tst_church_numbers() {
expr big = normalize(app(app(power(), two(), app(power(), two(), three())), N, s, z));
std::cout << count(big) << "\n";
lean_assert(count(big) == 256 + 2);
// expr three = app(plus(), two(), one());
// lean_assert(count(normalize(app(app(power(), three, three), N, s, z))) == 27 + 2);
// expr big = normalize(app(app(power(), two(), app(times(), app(plus(), four(), one()), four())), N, s, z));
// std::cout << count(big) << "\n";
expr three = app(plus(), two(), one());
lean_assert(count(normalize(app(app(power(), three, three), N, s, z))) == 27 + 2);
// expr big2 = normalize(app(app(power(), two(), app(times(), app(plus(), four(), one()), four())), N, s, z));
// std::cout << count(big2) << "\n";
std::cout << normalize(lam(lam(app(app(times(), four(), four()), N, var(0), z)))) << "\n";
}
@ -126,12 +125,38 @@ static void tst1() {
static void tst2() {
environment env;
expr f = constant("f");
expr h = constant("h");
expr a = constant("a");
expr b = constant("b");
expr x = var(0);
expr y = var(1);
expr t = type(level());
std::cout << normalize(f(x,x), env, extend(context(), context_entry(t, f(a)))) << "\n";
lean_assert(normalize(f(x,x), env, extend(context(), name("f"), t, f(a))) == f(f(a), f(a)));
context c1 = extend(extend(context(), name("f"), t, f(a)), name("h"), t, h(x));
expr F1 = normalize(f(x,f(x)), env, c1);
lean_assert(F1 == f(h(f(a)), f(h(f(a)))));
std::cout << F1 << "\n";
expr F2 = normalize(lambda("x", t, f(x, f(y))), env, c1);
std::cout << F2 << "\n";
lean_assert(F2 == lambda("x", t, f(x, f(h(f(a))))));
expr F3 = normalize(lambda("y", t, lambda("x", t, f(x, f(y)))), env, c1);
std::cout << F3 << "\n";
lean_assert(F3 == lambda("y", t, lambda("x", t, f(x, f(y)))));
context c2 = extend(extend(context(), name("foo"), t, lambda("x", t, f(x, a))), name("bla"), t, lambda("z", t, h(x,y)));
expr F4 = normalize(lambda("x", t, f(x, f(y))), env, c2);
std::cout << F4 << "\n";
lean_assert(F4 == lambda("x", t, f(x, f(lambda("z", t, h(x,lambda("x", t, f(x, a))))))));
context c3 = extend(context(), name("x"), t);
expr f5 = app(lambda("f", t, lambda("z", t, var(1))), lambda("y", t, var(1)));
expr F5 = normalize(f5, env, c3);
std::cout << f5 << "\n---->\n";
std::cout << F5 << "\n";
lean_assert(F5 == lambda("z", t, lambda("y", t, var(2))));
context c4 = extend(extend(context(), name("x"), t), name("x2"), t);
expr F6 = normalize(app(lambda("f", t, lambda("z1", t, lambda("z2", t, app(var(2), constant("a"))))),
lambda("y", t, app(var(1), var(2), var(0)))), env, c4);
std::cout << F6 << "\n";
lean_assert(F6 == lambda("z1", t, lambda("z2", t, app(var(2), var(3), constant("a")))));
}
int main() {

51
src/tests/kernel/type_check.cpp Normal file
View file

@ -0,0 +1,51 @@
/*
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 <iostream>
#include "type_check.h"
#include "exception.h"
#include "trace.h"
#include "test.h"
using namespace lean;
static void tst1() {
environment env;
expr t0 = type(level());
std::cout << infer_type(t0, env) << "\n";
lean_assert(infer_type(t0, env) == type(level()+1));
expr t1 = pi("_", t0, t0);
std::cout << infer_type(t1, env) << "\n";
}
static void tst2() {
try{
environment env;
level l1 = env.define_uvar("l1", level() + 1);
expr t0 = type(level());
expr t1 = type(l1);
expr F =
lambda("Nat", t0,
lambda("Vec", arrow(var(0), t0),
lambda("n", var(1),
lambda("len", arrow(app(var(1), var(0)), var(2)),
lambda("v", app(var(2), var(1)),
app(var(1), var(0)))))));
std::cout << F << "\n";
std::cout << infer_type(F, env) << "\n";
}
catch (exception ex) {
std::cout << "Error: " << ex.what() << "\n";
}
}
int main() {
// continue_on_violation(true);
enable_trace("type_check");
tst1();
return 0;
tst2();
return has_violations() ? 1 : 0;
}

21
src/util/list.h
View file

@ -31,11 +31,20 @@ public:
list(T const & h, list const & t):m_ptr(new cell(h, t)) {}
list(list const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
list(list&& s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
list(std::initializer_list<T> const & l):list() {
auto it = l.end();
while (it != l.begin()) {
--it;
*this = list(*it, *this);
}
}
~list() { if (m_ptr) m_ptr->dec_ref(); }
list & operator=(list const & s) { LEAN_COPY_REF(list, s); }
list & operator=(list && s) { LEAN_MOVE_REF(list, s); }
operator bool() const { return m_ptr != nullptr; }
friend bool is_nil(list const & l) { return l.m_ptr == nullptr; }
friend T const & head(list const & l) { lean_assert(!is_nil(l)); return l.m_ptr->m_head; }
friend list const & tail(list const & l) { lean_assert(!is_nil(l)); return l.m_ptr->m_tail; }
@ -51,7 +60,7 @@ template<typename T> inline std::ostream & operator<<(std::ostream & out, list<T
out << "(";
bool first = true;
list<T> const * ptr = &l;
while (!is_nil(*ptr)) {
while (*ptr) {
if (first)
first = false;
else
@ -62,4 +71,14 @@ template<typename T> inline std::ostream & operator<<(std::ostream & out, list<T
out << ")";
return out;
}
template<typename T> unsigned length(list<T> const & l) {
unsigned r = 0;
list<T> const * it = &l;
while (*it) {
r++;
it = &tail(*it);
}
return r;
}
}