From 04e92e1e96159423716731a24975e75a40f6ff6e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Feb 2015 16:25:06 -0800 Subject: [PATCH] feat(frontends/lean/parser): reject explicit universe levels in variables and parameters This modification was motivated by issue #427 --- src/frontends/lean/parser.cpp | 5 ++++- tests/lean/sec3.lean | 6 ++++++ tests/lean/sec3.lean.expected.out | 1 + 3 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 tests/lean/sec3.lean create mode 100644 tests/lean/sec3.lean.expected.out diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index f8db029236..4f17f6196b 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1079,7 +1079,10 @@ expr parser::id_to_expr(name const & id, pos_info const & p) { // locals if (auto it1 = m_local_decls.find(id)) { - auto r = copy_with_new_pos(propagate_levels(*it1, ls), p); + if (ls && m_undef_id_behavior != undef_id_behavior::AssumeConstant) + throw parser_error("invalid use of explicit universe parameter, identifier is a variable, " + "parameter or a constant bound to parameters in a section/context", p); + auto r = copy_with_new_pos(*it1, p); save_type_info(r); save_identifier_info(p, id); return r; diff --git a/tests/lean/sec3.lean b/tests/lean/sec3.lean new file mode 100644 index 0000000000..ad8f9f7493 --- /dev/null +++ b/tests/lean/sec3.lean @@ -0,0 +1,6 @@ +context + parameter A : Type + definition tst (a : A) := a + set_option pp.universes true + check tst.{1} +end diff --git a/tests/lean/sec3.lean.expected.out b/tests/lean/sec3.lean.expected.out new file mode 100644 index 0000000000..79c5acc7a1 --- /dev/null +++ b/tests/lean/sec3.lean.expected.out @@ -0,0 +1 @@ +sec3.lean:5:8: error: invalid use of explicit universe parameter, identifier is a variable, parameter or a constant bound to parameters in a section/context