From 5f77a2367f106013946a6e762a49fa71c7f4dc78 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 4 Aug 2013 18:26:01 -0700 Subject: [PATCH] Allow Boolean expressions (aka propositions) to be used as types. Signed-off-by: Leonardo de Moura --- src/kernel/context.h | 3 ++ src/kernel/environment.h | 18 +++++++++ src/kernel/type_check.cpp | 71 ++++++++++++++++++--------------- src/kernel/type_check.h | 1 + src/tests/kernel/type_check.cpp | 9 +++++ 5 files changed, 69 insertions(+), 33 deletions(-) diff --git a/src/kernel/context.h b/src/kernel/context.h index b25570c6a..a3bb01e26 100644 --- a/src/kernel/context.h +++ b/src/kernel/context.h @@ -32,5 +32,8 @@ inline context extend(context const & c, name const & n, expr const & t, expr co inline context extend(context const & c, name const & n, expr const & t) { return context(context_entry(n, t), c); } +inline bool empty(context const & c) { + return is_nil(c); +} std::ostream & operator<<(std::ostream & out, context const & c); } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index fd235c1f3..35b33b191 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include +#include "expr.h" #include "level.h" namespace lean { @@ -67,5 +68,22 @@ public: \pre has_parent() */ environment parent() const; + + /** + \brief Add a new definition n : t := v. + It throws an exception if v does not have type t. + If opaque == true, then definition is not used by normalizer. + */ + void add_definition(name const & n, expr const & t, expr const & v, bool opaque = false); + + /** + \brief Add a new definition n : infer_type(v) := v. + If opaque == true, then definition is not used by normalizer. + */ + void add_definition(name const & n, expr const & v, bool opaque = false); + + /** + */ + void add_fact(name const & n, expr const & t); }; } diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp index 23dda050d..7bcb0ad07 100644 --- a/src/kernel/type_check.cpp +++ b/src/kernel/type_check.cpp @@ -14,13 +14,27 @@ Author: Leonardo de Moura #include "trace.h" namespace lean { +bool is_convertible_core(expr const & expected, expr const & given, environment const & env) { + if (expected == given) + return true; + if (is_type(expected) && is_type(given)) { + if (env.is_ge(ty_level(expected), ty_level(given))) + return true; + } + return false; +} + +bool is_convertible(expr const & expected, expr const & given, environment const & env, context const & ctx) { + if (is_convertible_core(expected, given, env)) + return true; + expr e_n = normalize(expected, env, ctx); + expr g_n = normalize(given, env, ctx); + return is_convertible_core(e_n, g_n, env); +} + 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); lean_assert(length(c) >= length(def_c)); @@ -30,22 +44,30 @@ class infer_type_fn { 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); + expr u = normalize(infer_type(t, ctx), m_env, ctx); if (is_type(u)) return ty_level(u); + if (is_bool_type(u)) + return level(); std::ostringstream buffer; - buffer << "type expected, in context:\n" << ctx << "\ngiven:\n" << t; + buffer << "type expected"; + if (!empty(ctx)) + buffer << ", in context:\n" << ctx; + buffer << "\ngiven:\n" << t; throw exception(buffer.str()); } expr check_pi(expr const & e, context const & ctx) { if (is_pi(e)) return e; - expr r = normalize(e, ctx); + expr r = normalize(e, m_env, ctx); if (is_pi(r)) return r; std::ostringstream buffer; - buffer << "function expected, in context:\n" << ctx << "\ngiven:\n" << e; + buffer << "function expected"; + if (!empty(ctx)) + buffer << ", in context:\n" << ctx; + buffer << "\ngiven:\n" << e; throw exception(buffer.str()); } @@ -53,30 +75,6 @@ class infer_type_fn { return check_pi(infer_type(e, ctx), ctx); } - 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()) { @@ -93,7 +91,14 @@ class infer_type_fn { while (true) { expr const & c = arg(e, i); expr c_t = infer_type(c, ctx); - check_type(e, i, abst_domain(f_t), c_t, ctx); + if (!is_convertible(abst_domain(f_t), c_t, m_env, ctx)) { + std::ostringstream buffer; + buffer << "type mismatch at argument " << i << " of\n" << e + << "\nexpected type:\n" << abst_domain(f_t) + << "\ngiven type:\n" << c_t; + if (!empty(ctx)) + buffer << "\nin context:\n" << ctx; + } f_t = instantiate(abst_body(f_t), c); i++; if (i == num) diff --git a/src/kernel/type_check.h b/src/kernel/type_check.h index 87d038669..a7057d693 100644 --- a/src/kernel/type_check.h +++ b/src/kernel/type_check.h @@ -11,4 +11,5 @@ Author: Leonardo de Moura namespace lean { expr infer_type(expr const & e, environment const & env, context const & ctx = context()); +bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context()); } diff --git a/src/tests/kernel/type_check.cpp b/src/tests/kernel/type_check.cpp index af0a93352..020f36c4b 100644 --- a/src/tests/kernel/type_check.cpp +++ b/src/tests/kernel/type_check.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "abstract.h" #include "exception.h" #include "builtin.h" +#include "arith.h" #include "trace.h" #include "test.h" using namespace lean; @@ -73,11 +74,19 @@ static void tst3() { std::cout << infer_type(t, env) << "\n"; } +static void tst4() { + environment env; + expr a = eq(int_value(1), int_value(2)); + expr pr = lambda("x", a, var(0)); + std::cout << infer_type(pr, env) << "\n"; +} + int main() { continue_on_violation(true); enable_trace("type_check"); tst1(); tst2(); tst3(); + tst4(); return has_violations() ? 1 : 0; }