From 1f0eab7a145e06ce41ef02875f81a5a8b293de5d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 1 Oct 2013 10:52:17 -0700
Subject: [PATCH] test(type_checker): add new tests for type_checker trace
 objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/type_checker_trace.cpp | 23 +++++++++++++++--------
 src/tests/kernel/type_checker.cpp | 29 +++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+), 8 deletions(-)

diff --git a/src/kernel/type_checker_trace.cpp b/src/kernel/type_checker_trace.cpp
index 113b12d44e..ed4899fc4b 100644
--- a/src/kernel/type_checker_trace.cpp
+++ b/src/kernel/type_checker_trace.cpp
@@ -15,7 +15,7 @@ format function_expected_trace_cell::pp(formatter const & fmt, options const & o
     unsigned indent = get_pp_indent(opts);
     format expr_fmt = fmt(m_ctx, m_app, false, opts);
     format r;
-    r += format("function expected at");
+    r += format("Function expected at");
     r += nest(indent, compose(line(), expr_fmt));
     return r;
 }
@@ -32,12 +32,19 @@ app_type_match_trace_cell::~app_type_match_trace_cell() {
 
 format app_type_match_trace_cell::pp(formatter const & fmt, options const & opts) const {
     unsigned indent = get_pp_indent(opts);
-    format app_fmt  = fmt(m_ctx, m_app, false, opts);
     format r;
-    r += format("type of argument ");
+    r += format("Type of argument ");
     r += format(m_i);
-    r += format(" of application");
-    r += nest(indent, compose(line(), app_fmt));
+    r += format(" must be convertible to the expected type in the application of");
+    r += nest(indent, compose(line(), fmt(m_ctx, arg(m_app, 0), false, opts)));
+    unsigned num = num_args(m_app);
+    r += line();
+    if (num == 2)
+        r += format("with argument:");
+    else
+        r += format("with arguments:");
+    for (unsigned i = 1; i < num; i++)
+        r += nest(indent, compose(line(), fmt(m_ctx, arg(m_app, i), false, opts)));
     return r;
 }
 
@@ -55,7 +62,7 @@ format type_expected_trace_cell::pp(formatter const & fmt, options const & opts)
     unsigned indent = get_pp_indent(opts);
     format expr_fmt = fmt(m_ctx, m_type, false, opts);
     format r;
-    r += format("type expected at");
+    r += format("Type expected at");
     r += nest(indent, compose(line(), expr_fmt));
     return r;
 }
@@ -72,9 +79,9 @@ def_type_match_trace_cell::~def_type_match_trace_cell() {
 
 format def_type_match_trace_cell::pp(formatter const &, options const &) const {
     format r;
-    r += format("type of definition of '");
+    r += format("Type of definition '");
     r += format(get_name());
-    r += format("'");
+    r += format("' must be convertible to expected type.");
     return r;
 }
 
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index 49ae26f47e..70799328bd 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 #include "kernel/printer.h"
 #include "kernel/kernel_exception.h"
+#include "kernel/type_checker_trace.h"
 #include "library/basic_thms.h"
 #include "library/arith/arith.h"
 #include "library/all/all.h"
@@ -295,7 +296,34 @@ static void tst15() {
     lean_assert(is_eqp(r, checker.infer_type(F, ctx1)));
 }
 
+static void check_trace_msg(trace const & t, char const * expected) {
+    formatter fmt = mk_simple_formatter();
+    options   opts;
+    opts = opts.update({"pp", "indent"}, 2);
+    format    r = t.pp(fmt, opts);
+    std::cout << r << "\n";
+    std::ostringstream strm;
+    strm << r;
+    lean_assert_eq(strm.str(), std::string(expected));
+}
+
+static void tst16() {
+    std::cout << "Testing type checker trace objects\n";
+    context ctx;
+    expr f = Const("f");
+    expr a = Const("a");
+    expr x = Var(0);
+    ctx = extend(ctx, "x", Const("N"));
+    check_trace_msg(mk_function_expected_trace(ctx, f(a, x)), "Function expected at\n  f a x");
+    check_trace_msg(mk_type_expected_trace(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n  N -> x");
+    check_trace_msg(mk_type_expected_trace(ctx, Pi({a, Const("N")}, Var(1)(a))), "Type expected at\n  Pi a : N, (x a)");
+    check_trace_msg(mk_app_type_match_trace(ctx, f(a, x), 1), "Type of argument 1 must be convertible to the expected type in the application of\n  f\nwith arguments:\n  a\n  x");
+    check_trace_msg(mk_max_type_trace(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n  N -> x");
+    check_trace_msg(mk_def_type_match_trace(ctx, "foo", f(a, x)), "Type of definition 'foo' must be convertible to expected type.");
+}
+
 int main() {
+    tst15(); return 0;
     tst1();
     tst2();
     tst3();
@@ -311,5 +339,6 @@ int main() {
     tst13();
     tst14();
     tst15();
+    tst16();
     return has_violations() ? 1 : 0;
 }