From 026c5ee50935ddfde429487c36d45dcd6060be7d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 10 Apr 2017 15:56:18 +0200 Subject: [PATCH] fix(library/init/meta/expr,library/vm/vm_expr): fix macro args --- library/init/meta/expr.lean | 2 +- src/library/vm/vm_expr.cpp | 2 +- tests/lean/macro_args.lean | 1 + tests/lean/macro_args.lean.expected.out | 1 + 4 files changed, 4 insertions(+), 2 deletions(-) create mode 100644 tests/lean/macro_args.lean create mode 100644 tests/lean/macro_args.lean.expected.out diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean index 525871af5f..0076970a55 100644 --- a/library/init/meta/expr.lean +++ b/library/init/meta/expr.lean @@ -334,7 +334,7 @@ private meta def macro_args_to_list_aux (n : nat) (args : fin n → expr) : Π ( | (i+1) h := args ⟨i, h⟩ :: macro_args_to_list_aux i (nat.le_trans (nat.le_succ _) h) meta def macro_args_to_list (n : nat) (args : fin n → expr) : list expr := -macro_args_to_list_aux n args n (nat.le_refl _) +(macro_args_to_list_aux n args n (nat.le_refl _)).reverse meta def to_raw_fmt : expr → format | (var n) := p ["var", to_fmt n] diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index 12c6025400..e54983e5bb 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -204,7 +204,7 @@ unsigned expr_cases_on(vm_obj const & o, buffer & data) { break; case expr_kind::Macro: data.push_back(to_obj(macro_def(e))); - data.push_back(to_obj(macro_num_args(e))); + data.push_back(mk_vm_nat(macro_num_args(e))); data.push_back(mk_vm_closure(g_expr_macro_arg_fun_idx, 1, &o)); break; } diff --git a/tests/lean/macro_args.lean b/tests/lean/macro_args.lean new file mode 100644 index 0000000000..7532724c6c --- /dev/null +++ b/tests/lean/macro_args.lean @@ -0,0 +1 @@ +#eval ``({pos . line := zero, col := 1}).to_raw_expr.to_raw_fmt diff --git a/tests/lean/macro_args.lean.expected.out b/tests/lean/macro_args.lean.expected.out new file mode 100644 index 0000000000..10bbc77be7 --- /dev/null +++ b/tests/lean/macro_args.lean.expected.out @@ -0,0 +1 @@ +[macro structure instance (const zero []) [macro prenum]]