From 4cb54ac825e8f59a018631f9e3c9d757a9acd6d1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Oct 2014 10:54:20 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): more strict test for bad universe solution --- src/frontends/lean/elaborator.cpp | 50 ++++++++++++++++++------------- src/frontends/lean/pp_options.cpp | 1 + src/frontends/lean/pp_options.h | 1 + tests/lean/run/imp2.lean | 2 +- tests/lean/univ.lean | 19 ++++++++++++ tests/lean/univ.lean.expected.out | 13 ++++++++ 6 files changed, 65 insertions(+), 21 deletions(-) create mode 100644 tests/lean/univ.lean create mode 100644 tests/lean/univ.lean.expected.out diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 17f0b695a..38e949014 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -49,6 +49,7 @@ Author: Leonardo de Moura #include "frontends/lean/placeholder_elaborator.h" #include "frontends/lean/coercion_elaborator.h" #include "frontends/lean/proof_qed_elaborator.h" +#include "frontends/lean/pp_options.h" #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true @@ -604,9 +605,20 @@ public: }); } + static bool contains_placeholder(level const & l) { + bool contains = false; + for_each(l, [&](level const & l) { + if (contains) return false; + if (is_placeholder(l)) + contains = true; + return true; + }); + return contains; + } + expr visit_sort(expr const & e) { expr r = update_sort(e, replace_univ_placeholder(sort_level(e))); - if (is_placeholder(sort_level(e))) + if (contains_placeholder(sort_level(e))) m_to_check_sorts.emplace_back(e, r); return r; } @@ -1042,25 +1054,23 @@ public: expr pre = p.first; expr post = p.second; lean_assert(is_sort(post)); - level u = sort_level(post); - lean_assert(is_meta(u)); - if (s.is_assigned(u)) { - level r = *s.get_level(u); - if (is_zero(r)) { - throw_kernel_exception(env(), pre, [=](formatter const &) { - return format("solution computed by the elaborator forces Type to be Prop"); - }); - } - if (is_explicit(r)) { - throw_kernel_exception(env(), pre, [=](formatter const &) { - unsigned u = to_explicit(r); - format r = format("solution computed by the elaborator forces Type to be Type.{"); - r += format(u); - r += format("}, (possible solution: use Type')"); - return r; - }); - } - } + for_each(sort_level(post), [&](level const & u) { + if (is_meta(u) && s.is_assigned(u)) { + level r = *s.get_level(u); + if (is_explicit(r)) { + substitution saved_s(s); + throw_kernel_exception(env(), pre, [=](formatter const & fmt) { + options o = fmt.get_options(); + o = o.update(get_pp_universes_option_name(), true); + format r("solution computed by the elaborator forces a universe placeholder" + " to be a fixed value, computed sort is"); + r += pp_indent_expr(fmt.update_options(o), substitution(saved_s).instantiate(post)); + return r; + }); + } + } + return true; + }); } } diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp index b76839ee5..80217a064 100644 --- a/src/frontends/lean/pp_options.cpp +++ b/src/frontends/lean/pp_options.cpp @@ -119,6 +119,7 @@ void finalize_pp_options() { name const & get_pp_coercions_option_name() { return *g_pp_coercions; } name const & get_pp_full_names_option_name() { return *g_pp_full_names; } +name const & get_pp_universes_option_name() { return *g_pp_universes; } unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); } unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); } diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h index 1c118ed84..47de14641 100644 --- a/src/frontends/lean/pp_options.h +++ b/src/frontends/lean/pp_options.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura namespace lean { name const & get_pp_coercions_option_name(); name const & get_pp_full_names_option_name(); +name const & get_pp_universes_option_name(); unsigned get_pp_max_depth(options const & opts); unsigned get_pp_max_steps(options const & opts); diff --git a/tests/lean/run/imp2.lean b/tests/lean/run/imp2.lean index 48f2d027a..e097a0106 100644 --- a/tests/lean/run/imp2.lean +++ b/tests/lean/run/imp2.lean @@ -1,4 +1,4 @@ import data.num -check (λ {A : Type'} (a : A), a) 10 +check (λ {A : Type.{1}} (a : A), a) 10 check (λ {A} a, a) 10 check (λ a, a) 10 diff --git a/tests/lean/univ.lean b/tests/lean/univ.lean new file mode 100644 index 000000000..eab8b2385 --- /dev/null +++ b/tests/lean/univ.lean @@ -0,0 +1,19 @@ +import data.num + +definition id (A : Type) (a : A) := a + +check id Type num + +check id Type' num + +check id Type.{1} num + +check id _ num + +check id Type.{_+1} num + +check id Type.{0+1} num + +check id Type Type.{1} + +check id Type' Type.{1} diff --git a/tests/lean/univ.lean.expected.out b/tests/lean/univ.lean.expected.out new file mode 100644 index 000000000..ba9e87446 --- /dev/null +++ b/tests/lean/univ.lean.expected.out @@ -0,0 +1,13 @@ +univ.lean:5:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is + Type.{1} +univ.lean:7:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is + Type.{1} +id Type num : Type +id Type num : Type +univ.lean:13:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is + Type.{1} +id Type num : Type +univ.lean:17:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is + Type.{2} +univ.lean:19:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is + Type.{2}