From 8eb4bbd0cbb34e4490c23c139799a487eafc9813 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 7 Nov 2016 12:39:48 -0500 Subject: [PATCH] fix(kernel/declaration): allow introspection of declarations in GDB If the declaration::cell struct is not defined in the same header file as declaration, GDB will show the cells as . --- src/kernel/declaration.cpp | 24 ------------------------ src/kernel/declaration.h | 24 ++++++++++++++++++++++++ 2 files changed, 24 insertions(+), 24 deletions(-) diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 973afa639a..affc5ded43 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -37,30 +37,6 @@ int compare(reducibility_hints const & h1, reducibility_hints const & h2) { } } -struct declaration::cell { - MK_LEAN_RC(); - name m_name; - level_param_names m_params; - expr m_type; - bool m_theorem; - optional m_value; // if none, then declaration is actually a postulate - reducibility_hints m_hints; - /* Definitions are trusted by default, and nested macros are expanded when kernel is instantiated with - trust level 0. When this flag is false, then we do not expand nested macros. We say the - associated definitions are "untrusted". We use this feature to define tactical-definitions. - The kernel type checker ensures trusted definitions do not use untrusted ones. */ - bool m_trusted; - void dealloc() { delete this; } - - cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom, bool trusted): - m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom), - m_hints(reducibility_hints::mk_opaque()), m_trusted(trusted) {} - cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v, - reducibility_hints const & h, bool trusted): - m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm), - m_value(v), m_hints(h), m_trusted(trusted) {} -}; - static declaration * g_dummy = nullptr; declaration::declaration():declaration(*g_dummy) {} diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index f62290dbec..c620a810ec 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -118,6 +118,30 @@ public: friend declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted); }; +struct declaration::cell { + MK_LEAN_RC(); + name m_name; + level_param_names m_params; + expr m_type; + bool m_theorem; + optional m_value; // if none, then declaration is actually a postulate + reducibility_hints m_hints; + /* Definitions are trusted by default, and nested macros are expanded when kernel is instantiated with + trust level 0. When this flag is false, then we do not expand nested macros. We say the + associated definitions are "untrusted". We use this feature to define tactical-definitions. + The kernel type checker ensures trusted definitions do not use untrusted ones. */ + bool m_trusted; + void dealloc() { delete this; } + + cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom, bool trusted): + m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom), + m_hints(reducibility_hints::mk_opaque()), m_trusted(trusted) {} + cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v, + reducibility_hints const & h, bool trusted): + m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm), + m_value(v), m_hints(h), m_trusted(trusted) {} +}; + inline optional none_declaration() { return optional(); } inline optional some_declaration(declaration const & o) { return optional(o); } inline optional some_declaration(declaration && o) { return optional(std::forward(o)); }