From a3554c85fe65ef39df4cb1bc26d043dbe2c2b501 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Apr 2014 10:50:41 -0700 Subject: [PATCH] fix(kernel/definition): clang compilation warning, and add module_idx typedef Signed-off-by: Leonardo de Moura --- src/kernel/definition.cpp | 5 +++-- src/kernel/definition.h | 19 ++++++++++++++++--- 2 files changed, 19 insertions(+), 5 deletions(-) diff --git a/src/kernel/definition.cpp b/src/kernel/definition.cpp index d64487499..1227a1b63 100644 --- a/src/kernel/definition.cpp +++ b/src/kernel/definition.cpp @@ -35,7 +35,7 @@ struct definition::cell { m_rc(1), m_name(n), m_params(params), m_cnstrs(cs), m_type(t), m_theorem(is_axiom), m_weight(0), m_module_idx(0), m_opaque(true), m_use_conv_opt(false) {} cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, bool is_thm, expr const & v, - bool opaque, unsigned w, unsigned mod_idx, bool use_conv_opt): + bool opaque, unsigned w, module_idx mod_idx, bool use_conv_opt): m_rc(1), m_name(n), m_params(params), m_cnstrs(cs), m_type(t), m_theorem(is_thm), m_value(v), m_weight(w), m_module_idx(mod_idx), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {} @@ -83,11 +83,12 @@ expr definition::get_type() const { return m_ptr->m_type; } bool definition::is_opaque() const { return m_ptr->m_opaque; } expr definition::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); } unsigned definition::get_weight() const { return m_ptr->m_weight; } +module_idx definition::get_module_idx() const { return m_ptr->m_module_idx; } bool definition::use_conv_opt() const { return m_ptr->m_use_conv_opt; } void definition::write(serializer & s) const { m_ptr->write(s); } -definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, unsigned weight, unsigned mod_idx, bool use_conv_opt) { +definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) { return definition(new definition::cell(n, params, cs, t, false, v, opaque, weight, mod_idx, use_conv_opt)); } definition mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v) { diff --git a/src/kernel/definition.h b/src/kernel/definition.h index 291195d79..b04efbcc5 100644 --- a/src/kernel/definition.h +++ b/src/kernel/definition.h @@ -11,6 +11,18 @@ Author: Leonardo de Moura #include "kernel/expr.h" namespace lean { +/** + \brief Module index. The kernel provides only basic support + for implementing a module system outside of the kernel. + + We need at least the notion of module index in the kernel, because + it affects the convertability procedure. + + Given an opaque definition (non-theorem) d in module m1, then d is considered + to be transparent for any other opaque definition in module m1. +*/ +typedef unsigned module_idx; + /** \brief Environment definitions, theorems, axioms and variable declarations. */ @@ -18,7 +30,7 @@ class definition { struct cell; cell * m_ptr; explicit definition(cell * ptr); - friend class cell; + friend struct cell; public: /** \brief The default constructor creates a reference to a "dummy" @@ -51,9 +63,10 @@ public: expr get_value() const; bool is_opaque() const; unsigned get_weight() const; + module_idx get_module_idx() const; bool use_conv_opt() const; - friend definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, unsigned weight, unsigned mod_idx, bool use_conv_opt); + friend definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt); friend definition mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v); friend definition mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t); friend definition mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t); @@ -65,7 +78,7 @@ inline optional none_definition() { return optional(); } inline optional some_definition(definition const & o) { return optional(o); } inline optional some_definition(definition && o) { return optional(std::forward(o)); } -definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque = false, unsigned weight = 0, unsigned mod_idx = 0, bool use_conv_opt = true); +definition mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true); definition mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v); definition mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t); definition mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);