From 12a6b889d179ec600d54e307178c8e79ba45e85a Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sun, 9 May 2021 18:58:07 -0400 Subject: [PATCH 1/2] fix(checker/text_import): make leanchecker agree with external tc The change to `text_import.cpp` checks the line for parse errors after parsing, so we don't accidentally let malformed lines pass. The change to the kernel removes the check for anonymous names in lambda/let/pi. Since these are used only for pretty printing it should not affect soundness. An alternative approach would be to automatically generate a fresh name when the given name is anonymous. --- src/checker/text_import.cpp | 6 ++++++ src/kernel/type_checker.cpp | 6 ------ 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/checker/text_import.cpp b/src/checker/text_import.cpp index 8bbe6c9757..89c27e34a5 100644 --- a/src/checker/text_import.cpp +++ b/src/checker/text_import.cpp @@ -52,6 +52,7 @@ struct text_importer { while (in >> idx) { ls.push_back(m_level.at(idx)); } + in.clear(); return to_list(ls); } @@ -61,6 +62,7 @@ struct text_importer { while (in >> idx) { ls.push_back(m_name.at(idx)); } + in.clear(); return to_list(ls); } @@ -224,6 +226,10 @@ struct text_importer { } else { throw exception(sstream() << "unknown command: " << cmd); } + in >> std::ws; + if (in.fail() || !in.eof()) { + throw exception(sstream() << "parse error"); + } } }; diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index e75b2fdc8d..7f5ecaa2a8 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -111,8 +111,6 @@ expr type_checker::infer_lambda(expr const & _e, bool infer_only) { es.push_back(e); ds.push_back(binding_domain(e)); expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data()); - if (binding_name(e).is_anonymous()) - throw_kernel_exception(m_env, "invalid anonymous binder name", e); expr l = mk_local(m_name_generator.next(), binding_name(e), d, binding_info(e)); ls.push_back(l); if (!infer_only) { @@ -135,8 +133,6 @@ expr type_checker::infer_pi(expr const & _e, bool infer_only) { buffer us; expr e = _e; while (is_pi(e)) { - if (binding_name(e).is_anonymous()) - throw_kernel_exception(m_env, "invalid anonymous binder name", e); expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data()); expr t1 = ensure_sort_core(infer_type_core(d, infer_only), d); us.push_back(sort_level(t1)); @@ -189,8 +185,6 @@ expr type_checker::infer_app(expr const & e, bool infer_only) { expr type_checker::infer_let(expr const & e, bool infer_only) { if (!infer_only) { - if (let_name(e).is_anonymous()) - throw_kernel_exception(m_env, "invalid anonymous let var name", e); ensure_sort_core(infer_type_core(let_type(e), infer_only), e); expr v_type = infer_type_core(let_value(e), infer_only); // TODO(Leo): we will remove justifications in the future. From 9b2e5bc0534b69d0dca71dc419b55e4d66b6414d Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 10 May 2021 01:03:07 -0400 Subject: [PATCH 2/2] fix --- src/checker/text_import.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/checker/text_import.cpp b/src/checker/text_import.cpp index 89c27e34a5..f31f6ce7d6 100644 --- a/src/checker/text_import.cpp +++ b/src/checker/text_import.cpp @@ -226,7 +226,7 @@ struct text_importer { } else { throw exception(sstream() << "unknown command: " << cmd); } - in >> std::ws; + if (!in.eof()) in >> std::ws; if (in.fail() || !in.eof()) { throw exception(sstream() << "parse error"); }