michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/printer): include de Bruijn index in the debug printer

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-16 16:56:46 -08:00
parent 91f4ced83b
commit f09fd0fc04
3 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/printer.cpp
View file

@ -102,7 +102,7 @@ struct print_expr_fn {
case expr_kind::Var: {
auto e = find(c, var_idx(a));
if (e)
out() << e->get_name();
out() << e->get_name() << "#" << var_idx(a);
else
out() << "#" << var_idx(a);
break;

10
src/tests/kernel/type_checker.cpp
View file

@ -315,11 +315,11 @@ static void tst16() {
expr a = Const("a");
expr x = Var(0);
ctx = extend(ctx, "x", Const("N"));
check_justification_msg(mk_function_expected_justification(ctx, f(a, x)), "Function expected at\n f a x");
check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n N -> x");
check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1)(a))), "Type expected at\n Pi a : N, (x a)");
check_justification_msg(mk_app_type_match_justification(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_justification_msg(mk_max_type_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n N -> x");
check_justification_msg(mk_function_expected_justification(ctx, f(a, x)), "Function expected at\n f a x#0");
check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n N -> x#1");
check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1)(a))), "Type expected at\n Pi a : N, (x#1 a#0)");
check_justification_msg(mk_app_type_match_justification(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#0");
check_justification_msg(mk_max_type_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n N -> x#1");
check_justification_msg(mk_def_type_match_justification(ctx, "foo", f(a, x)), "Type of definition 'foo' must be convertible to expected type.");
}

8
src/tests/library/formatter.cpp
View file

@ -30,15 +30,15 @@ static void tst1() {
expr y = Const("y");
expr N = Const("N");
expr F = Fun({x, Pi({x, N}, x >> x)}, Let({y, f(a)}, f(Eq(x, f(y, a)))));
check(fmt(F), "fun x : (Pi x : N, (x -> x)), (let y := f a in (f (x == (f y a))))");
check(fmt(F), "fun x : (Pi x : N, (x#0 -> x#1)), (let y := f a in (f (x#1 == (f y#0 a))))");
check(fmt(env->get_object("N")), "Variable N : Type");
context ctx;
ctx = extend(ctx, "x", f(a));
ctx = extend(ctx, "y", f(Var(0), N >> N));
ctx = extend(ctx, "z", N, Eq(Var(0), Var(1)));
check(fmt(ctx), "[x : f a; y : f x (N -> N); z : N := y == x]");
check(fmt(ctx, f(Var(0), Var(2))), "f z x");
check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x (N -> N); z : N := y == x] |- f z x");
check(fmt(ctx), "[x : f a; y : f x#0 (N -> N); z : N := y#0 == x#1]");
check(fmt(ctx, f(Var(0), Var(2))), "f z#0 x#2");
check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x#0 (N -> N); z : N := y#0 == x#1] |- f z#0 x#2");
}
int main() {