Add light_checker: module for extracting the type of (fully elaborated) expressions. It is much faster than type_checker, which infers the type but also check whether the input is type correct or not.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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})

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<expr, expr, expr_hash, expr_eqp> 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); }
+}

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 <memory>
+#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<imp> 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); }
+};
+}

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<expr> 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;
+    }
+}
+}

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);
+}

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)

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;
+}

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 <iostream>
+#include <time.h>
+
+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<double>(end) - static_cast<double>(m_start)) / CLOCKS_PER_SEC) << " secs\n";
+    }
+};
+}