From 30089aa4f88c65b41b022d06ebc5552e2e5bc726 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Sep 2013 16:39:29 -0700 Subject: [PATCH] test(type_checker): add example showing how to use the kernel exception formatter Signed-off-by: Leonardo de Moura --- src/tests/kernel/type_checker.cpp | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index 9535960dba..0f416ced26 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -19,6 +19,8 @@ Author: Leonardo de Moura #include "library/basic_thms.h" #include "library/arith/arith.h" #include "library/all/all.h" +#include "library/state.h" +#include "library/kernel_exception_formatter.h" using namespace lean; expr c(char const * n) { return mk_constant(n); } @@ -247,6 +249,24 @@ static void tst13() { std::cout << infer_type(f(Eq(True, False)), env) << "\n"; } +static void tst14() { + environment env; + import_all(env); + expr f = Const("f"); + expr a = Const("a"); + env.add_var("f", Int >> Int); + env.add_var("a", Real); + expr F = f(a); + type_checker checker(env); + formatter fmt = mk_simple_formatter(); + state st(options(), fmt); + try { + std::cout << checker.infer_type(F) << "\n"; + } catch (kernel_exception & ex) { + regular(st) << ex << "\n"; + } +} + int main() { tst1(); tst2(); @@ -261,5 +281,6 @@ int main() { tst11(); tst12(); tst13(); + tst14(); return has_violations() ? 1 : 0; }