From 876a2bee46dc274e9df06e6776d9b0fcef9b1f8a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 3 Mar 2017 18:23:57 +0100 Subject: [PATCH] feat(frontends/lean/elaborator): flag expr quotes containing universe params --- src/frontends/lean/elaborator.cpp | 12 ++++++++---- tests/lean/expr_quote.lean | 6 ++++++ tests/lean/expr_quote.lean.expected.out | 3 +++ 3 files changed, 17 insertions(+), 4 deletions(-) create mode 100644 tests/lean/expr_quote.lean create mode 100644 tests/lean/expr_quote.lean.expected.out diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 19dccd0d79..7a6a80e1ba 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2643,7 +2643,7 @@ expr elaborate_quote(expr e, environment const &env, options const &opts, bool i } return none_expr(); }); - e = Fun(locals, e); + e = copy_tag(e, Fun(locals, e)); metavar_context ctx; local_context lctx; @@ -2651,12 +2651,16 @@ expr elaborate_quote(expr e, environment const &env, options const &opts, bool i e = elab.elaborate(e); e = elab.finalize(e, true, true).first; + expr body = e; + for (unsigned i = 0; i < aqs.size(); i++) + body = binding_body(body); + if (in_pattern) { - for (unsigned i = 0; i < aqs.size(); i++) - e = binding_body(e); - e = instantiate_rev(e, aqs.size(), aqs.data()); + e = instantiate_rev(body, aqs.size(), aqs.data()); e = quote(e); } else { + if (has_param_univ(body)) + throw elaborator_exception(e, "invalid quotation, contains universe parameter"); e = mk_quote_core(e, true); expr subst = mk_constant(get_expr_subst_name()); for (expr aq : aqs) diff --git a/tests/lean/expr_quote.lean b/tests/lean/expr_quote.lean new file mode 100644 index 0000000000..2592276138 --- /dev/null +++ b/tests/lean/expr_quote.lean @@ -0,0 +1,6 @@ +meta def f (α a : expr) := ```(@id %%α %%a) + +meta def f (α a : expr) := ```(@id (%%α : Type 2) %%a) + +set_option pp.universes true +print f diff --git a/tests/lean/expr_quote.lean.expected.out b/tests/lean/expr_quote.lean.expected.out new file mode 100644 index 0000000000..c0aa21bf4a --- /dev/null +++ b/tests/lean/expr_quote.lean.expected.out @@ -0,0 +1,3 @@ +expr_quote.lean:1:32: error: invalid quotation, contains universe parameter +meta def f : expr → expr → expr := +λ (α a : expr), expr.subst (expr.subst ```(λ (_x_1 : Type 2) (_x_2 : _x_1), id.{3} _x_2) α) a