From 341cf71fb9306f21ee604b4732e8491e2fdf7bc3 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 14 Sep 2017 09:36:40 +0200 Subject: [PATCH] fix(frontends/lean/structure_cmd): check parent expression after elaboration as well --- src/frontends/lean/structure_cmd.cpp | 10 ++++++++++ tests/lean/structure_segfault.lean | 15 +++++++++++++++ tests/lean/structure_segfault.lean.expected.out | 5 +++++ 3 files changed, 30 insertions(+) create mode 100644 tests/lean/structure_segfault.lean create mode 100644 tests/lean/structure_segfault.lean.expected.out diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index b2bb106583..8e930093b6 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -350,6 +350,15 @@ struct structure_cmd_fn { throw parser_error(sstream() << "invalid 'structure' extends, '" << S << "' is not a structure", pos); } + void check_parent(expr const & parent) { + expr const & fn = get_app_fn(parent); + if (!is_constant(fn)) + throw elaborator_exception(parent, "invalid 'structure', expression must be a 'parent' structure"); + name const & S = const_name(fn); + if (!is_structure_like(m_env, S)) + throw elaborator_exception(parent, sstream() << "invalid 'structure' extends, '" << S << "' is not a structure"); + } + /** \brief Return the universe parameters, number of parameters and introduction rule for the given parent structure */ std::tuple get_parent_info(name const & parent) { return get_structure_info(m_env, parent); @@ -589,6 +598,7 @@ struct structure_cmd_fn { for (unsigned i = 0; i < m_parents.size(); i++) { expr const & parent = m_parents[i]; + check_parent(parent); rename_vector const & renames = m_renames[i]; m_field_maps.push_back(field_map()); field_map & fmap = m_field_maps.back(); diff --git a/tests/lean/structure_segfault.lean b/tests/lean/structure_segfault.lean new file mode 100644 index 0000000000..7c0dc2a0cd --- /dev/null +++ b/tests/lean/structure_segfault.lean @@ -0,0 +1,15 @@ +universes u + +namespace hide + +structure group (α : Type u) : Type u + +structure T (α : extends group α := () + +structure ring (α : Type u) : Type u + +class T (α : Type*) extends ring x α + +class S (α : Type*) extends ((λ x, group x) α) + +end hide diff --git a/tests/lean/structure_segfault.lean.expected.out b/tests/lean/structure_segfault.lean.expected.out new file mode 100644 index 0000000000..08f32d8ee9 --- /dev/null +++ b/tests/lean/structure_segfault.lean.expected.out @@ -0,0 +1,5 @@ +structure_segfault.lean:7:17: error: invalid expression +structure_segfault.lean:7:25: error: invalid 'structure', expression must be a 'parent' structure +structure_segfault.lean:11:33: error: unknown identifier 'x' +structure_segfault.lean:11:28: error: invalid 'structure', expression must be a 'parent' structure +structure_segfault.lean:13:28: error: invalid 'structure', expression must be a 'parent' structure