diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 5d8039fbf..2d93a1785 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,4 +1,5 @@ add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp printer.cpp formatter.cpp context_to_lambda.cpp - state.cpp metavar.cpp update_expr.cpp kernel_exception_formatter.cpp) + state.cpp metavar.cpp update_expr.cpp kernel_exception_formatter.cpp + reduce.cpp light_checker.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/light_checker.cpp b/src/library/light_checker.cpp new file mode 100644 index 000000000..473b9ab88 --- /dev/null +++ b/src/library/light_checker.cpp @@ -0,0 +1,164 @@ +/* +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 "light_checker.h" +#include "environment.h" +#include "reduce.h" +#include "scoped_map.h" +#include "normalizer.h" +#include "builtin.h" +#include "kernel_exception.h" +#include "instantiate.h" +#include "free_vars.h" + +namespace lean { +class light_checker::imp { + typedef scoped_map cache; + + environment m_env; + cache m_cache; + normalizer m_normalizer; + volatile bool m_interrupted; + + level infer_universe(expr const & t, context const & ctx) { + expr u = m_normalizer(infer_type(t, ctx), ctx); + if (is_type(u)) + return ty_level(u); + if (u == Bool) + return level(); + throw type_expected_exception(m_env, ctx, t); + } + + expr get_range(expr t, expr const & e, context const & ctx) { + unsigned num = num_args(e) - 1; + while (num > 0) { + --num; + if (is_pi(t)) { + t = abst_body(t); + } else { + t = m_normalizer(t, ctx); + if (is_pi(t)) { + t = abst_body(t); + } else { + throw function_expected_exception(m_env, ctx, e); + } + } + } + if (closed(t)) + return t; + else + return instantiate(t, num_args(e)-1, &arg(e, 1)); + } + +public: + imp(environment const & env): + m_env(env), + m_normalizer(env) { + m_interrupted = false; + } + + expr infer_type(expr const & e, context const & ctx) { + // cheap cases, we do not cache results + switch (e.kind()) { + case expr_kind::Constant: { + object const & obj = m_env.get_object(const_name(e)); + if (obj.has_type()) + return obj.get_type(); + else + throw exception("type incorrect expression"); + break; + } + case expr_kind::Var: { + context_entry const & ce = lookup(ctx, var_idx(e)); + if (ce.get_domain()) + return ce.get_domain(); + // Remark: the case where ce.get_domain() is not + // available is not considered cheap. + break; + } + case expr_kind::Eq: + return mk_bool_type(); + case expr_kind::Value: + return to_value(e).get_type(); + case expr_kind::Type: + return mk_type(ty_level(e) + 1); + case expr_kind::App: case expr_kind::Lambda: + case expr_kind::Pi: case expr_kind::Let: + break; // expensive cases + } + + check_interrupted(m_interrupted); + bool shared = false; + if (is_shared(e)) { + shared = true; + auto it = m_cache.find(e); + if (it != m_cache.end()) + return it->second; + } + + expr r; + switch (e.kind()) { + case expr_kind::Constant: case expr_kind::Eq: + case expr_kind::Value: case expr_kind::Type: + lean_unreachable(); + break; + case expr_kind::Var: { + auto p = lookup_ext(ctx, var_idx(e)); + context_entry const & ce = p.first; + context const & ce_ctx = p.second; + lean_assert(!ce.get_domain()); + r = lift_free_vars(infer_type(ce.get_body(), ce_ctx), ctx.size() - ce_ctx.size()); + break; + } + case expr_kind::App: { + expr const & f = arg(e, 0); + expr f_t = infer_type(f, ctx); + r = get_range(f_t, e, ctx); + break; + } + case expr_kind::Lambda: { + cache::mk_scope sc(m_cache); + r = mk_pi(abst_name(e), abst_domain(e), infer_type(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)))); + break; + } + case expr_kind::Pi: { + level l1 = infer_universe(abst_domain(e), ctx); + level l2; + { + cache::mk_scope sc(m_cache); + l2 = infer_universe(abst_body(e), extend(ctx, abst_name(e), abst_domain(e))); + } + r = mk_type(max(l1, l2)); + break; + } + case expr_kind::Let: { + cache::mk_scope sc(m_cache); + r = infer_type(let_body(e), extend(ctx, let_name(e), let_type(e), let_value(e))); + break; + }} + + if (shared) { + m_cache.insert(e, r); + } + return r; + } + + void set_interrupt(bool flag) { + m_interrupted = flag; + m_normalizer.set_interrupt(flag); + } + + void clear() { + m_cache.clear(); + m_normalizer.clear(); + } +}; +light_checker::light_checker(environment const & env):m_ptr(new imp(env)) {} +light_checker::~light_checker() {} +expr light_checker::operator()(expr const & e, context const & ctx) { return m_ptr->infer_type(e, ctx); } +void light_checker::clear() { m_ptr->clear(); } +void light_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } +} diff --git a/src/library/light_checker.h b/src/library/light_checker.h new file mode 100644 index 000000000..c872a52f3 --- /dev/null +++ b/src/library/light_checker.h @@ -0,0 +1,39 @@ +/* +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 +#include "expr.h" +#include "context.h" + +namespace lean { +class environment; +/** + \brief Functional object for "quickly" inferring the type of expressions. + It does not check whether the input expression is type correct or not. + The contract is: IF the input expression is type correct, then the inferred + type is correct. + + \remark The exceptions produced by this class are not informative. + That is, they are not meant for external users, but to sign that the + type could not be inferred. +*/ +class light_checker { + class imp; + std::unique_ptr m_ptr; +public: + light_checker(environment const & env); + ~light_checker(); + + expr operator()(expr const & e, context const & ctx = context()); + + void clear(); + + void set_interrupt(bool flag); + void interrupt() { set_interrupt(true); } + void reset_interrupt() { set_interrupt(false); } +}; +} diff --git a/src/library/reduce.cpp b/src/library/reduce.cpp new file mode 100644 index 000000000..28ab44a25 --- /dev/null +++ b/src/library/reduce.cpp @@ -0,0 +1,81 @@ +/* +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 "instantiate.h" +#include "environment.h" +#include "name_set.h" +#include "update_expr.h" +#include "free_vars.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 args; + args.push_back(r); + m++; + for (; m < num; m++) + args.push_back(arg(t, m)); + return mk_app(args.size(), args.data()); + } + } +} + +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(); + } + } else { + return t; + } +} +} diff --git a/src/library/reduce.h b/src/library/reduce.h new file mode 100644 index 000000000..2fe1620e3 --- /dev/null +++ b/src/library/reduce.h @@ -0,0 +1,16 @@ +/* +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 "context.h" +#include "environment.h" +#include "name_set.h" + +namespace lean { +bool is_head_beta(expr const & t); +expr head_beta_reduce(expr const & t); +expr head_reduce(expr const & t, environment const & e, context const & c = context(), name_set const * defs = nullptr); +} diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt index 17647867f..26e57af5f 100644 --- a/src/tests/library/CMakeLists.txt +++ b/src/tests/library/CMakeLists.txt @@ -1,3 +1,6 @@ add_executable(metavar metavar.cpp) target_link_libraries(metavar ${EXTRA_LIBS}) add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar) +add_executable(light_checker light_checker.cpp) +target_link_libraries(light_checker ${EXTRA_LIBS}) +add_test(light_checker ${CMAKE_CURRENT_BINARY_DIR}/light_checker) diff --git a/src/tests/library/light_checker.cpp b/src/tests/library/light_checker.cpp new file mode 100644 index 000000000..4331bd289 --- /dev/null +++ b/src/tests/library/light_checker.cpp @@ -0,0 +1,74 @@ +/* +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 "test.h" +#include "light_checker.h" +#include "type_checker.h" +#include "environment.h" +#include "arithlibs.h" +#include "import_all.h" +#include "abstract.h" +#include "printer.h" +#include "timeit.h" +using namespace lean; + +static void tst1() { + environment env = mk_toplevel(); + light_checker type_of(env); + expr f = Const("f"); + expr g = Const("g"); + expr a = Const("a"); + expr b = Const("b"); + expr A = Const("A"); + env.add_var("f", Int >> (Int >> Int)); + lean_assert(type_of(f(a,a)) == Int); + lean_assert(type_of(f(a)) == Int >> Int); + lean_assert(type_of(And(a, f(a))) == Bool); + lean_assert(type_of(Fun({a, Int}, iAdd(a,iVal(1)))) == Int >> Int); + lean_assert(type_of(Let({a, iVal(10)}, iAdd(a, b))) == Int); + lean_assert(type_of(Type()) == Type(level() + 1)); + lean_assert(type_of(Bool) == Type()); + lean_assert(type_of(Pi({a, Type()}, Type(level() + 2))) == Type(level() + 3)); + lean_assert(type_of(Pi({a, Type(level()+4)}, Type(level() + 2))) == Type(level() + 5)); + lean_assert(type_of(Pi({a, Int}, Bool)) == Type()); + env.add_var("g", Pi({A, Type()}, A >> A)); + lean_assert(type_of(g(Int, a)) == Int); + lean_assert(type_of(g(Fun({a, Type()}, a)(Int), a)) == Fun({a, Type()}, a)(Int)); +} + +static expr mk_big(unsigned val, unsigned depth) { + if (depth == 0) + return iVal(val); + else + return iAdd(mk_big(val*2, depth-1), mk_big(val*2 + 1, depth-1)); +} + +static void tst2() { + environment env = mk_toplevel(); + light_checker type_of(env); + type_checker type_of_slow(env); + expr t = mk_big(0, 10); + { + timeit timer(std::cout, "light checker 10000 calls"); + for (unsigned i = 0; i < 10000; i++) { + type_of(t); + type_of.clear(); + } + } + { + timeit timer(std::cout, "type checker 300 calls"); + for (unsigned i = 0; i < 300; i++) { + type_of_slow.infer_type(t); + type_of_slow.clear(); + } + } +} + +int main() { + tst1(); + tst2(); + return has_violations() ? 1 : 0; +} diff --git a/src/util/timeit.h b/src/util/timeit.h new file mode 100644 index 000000000..86bfeb657 --- /dev/null +++ b/src/util/timeit.h @@ -0,0 +1,28 @@ +/* +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 +#include + +namespace lean { +/** + \brief Low tech timer for used for testing. +*/ +class timeit { + std::ostream & m_out; + std::string m_msg; + clock_t m_start; +public: + timeit(std::ostream & out, char const * msg):m_out(out), m_msg(msg) { + m_start = clock(); + } + ~timeit() { + clock_t end = clock(); + std::cout << m_msg << " " << ((static_cast(end) - static_cast(m_start)) / CLOCKS_PER_SEC) << " secs\n"; + } +}; +}