From 11a9cac5d6d0fbafd12dae6ab02decab17317140 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Aug 2013 15:13:54 -0700 Subject: [PATCH] Refactor kernel objects Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 2 +- src/kernel/environment.cpp | 238 +++++++++++++++++-------------- src/kernel/environment.h | 88 +----------- src/kernel/expr.cpp | 7 + src/kernel/expr.h | 13 ++ src/kernel/normalize.cpp | 6 +- src/kernel/object.cpp | 74 ++++++++++ src/kernel/object.h | 171 ++++++++++++++++++++++ src/tests/kernel/environment.cpp | 3 +- src/util/name.cpp | 7 + src/util/name.h | 1 + 11 files changed, 413 insertions(+), 197 deletions(-) create mode 100644 src/kernel/object.cpp create mode 100644 src/kernel/object.h diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index f90a54348..e65a3c6a8 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp type_check.cpp context.cpp builtin.cpp basic_thms.cpp toplevel.cpp - pp.cpp) + object.cpp pp.cpp) target_link_libraries(kernel ${LEAN_LIBS}) diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 30ae0316c..9065ec59c 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -17,51 +17,10 @@ Author: Leonardo de Moura #include "debug.h" namespace lean { -constexpr unsigned uninit = std::numeric_limits::max(); - -environment::definition::definition(name const & n, expr const & t, expr const & v, bool opaque): - m_name(n), - m_type(t), - m_value(v), - m_opaque(opaque) { -} - -environment::definition::~definition() { -} - -void environment::definition::display(std::ostream & out) const { - out << header() << " " << m_name << " : " << m_type << " := " << m_value << "\n"; -} - -format pp_object_kind(char const * n) { return highlight(format(n), format::format_color::BLUE); } -constexpr unsigned indentation = 2; // TODO: must be option - -format environment::definition::pp(environment const & env) const { - return nest(indentation, - format{pp_object_kind(header()), format(" "), format(m_name), format(" : "), ::lean::pp(m_type, env), format(" :="), - line(), ::lean::pp(m_value), format(".")}); -} - -environment::fact::fact(name const & n, expr const & t): - m_name(n), - m_type(t) { -} - -environment::fact::~fact() { -} - -format environment::fact::pp(environment const & env) const { - return nest(indentation, - format{pp_object_kind(header()), format(" "), format(m_name), format(" : "), ::lean::pp(m_type, env), format(".")}); -} - -void environment::fact::display(std::ostream & out) const { - out << header() << " " << m_name << " : " << m_type << "\n"; -} - /** \brief Implementation of the Lean environment. */ struct environment::imp { - typedef std::unordered_map object_dictionary; + // Remark: only named objects are stored in the dictionary. + typedef std::unordered_map object_dictionary; typedef std::tuple constraint; // Universe variable management std::vector m_constraints; @@ -73,25 +32,33 @@ struct environment::imp { std::vector m_objects; object_dictionary m_object_dictionary; + /** + \brief Return true iff this environment has children. + + \remark If an environment has children than it cannot be + updated. That is, it is read-only. + */ bool has_children() const { return m_num_children > 0; } void inc_children() { m_num_children++; } void dec_children() { m_num_children--; } + /** \brief Return true iff this environment has a parent environment */ bool has_parent() const { return m_parent != nullptr; } - /** \brief Return true if l1 >= l2 + k is implied by constraints - \pre is_uvar(l1) && is_uvar(l2) - */ - bool is_implied(level const & l1, level const & l2, int k) { - lean_assert(is_uvar(l1) && is_uvar(l2)); - if (l1 == l2) + /** + \brief Return true if u >= v + k is implied by constraints + \pre is_uvar(u) && is_uvar(v) + */ + bool is_implied(level const & u, level const & v, int k) { + lean_assert(is_uvar(u) && is_uvar(v)); + if (u == v) return k <= 0; else return std::any_of(m_constraints.begin(), m_constraints.end(), - [&](constraint const & c) { return std::get<0>(c) == l1 && std::get<1>(c) == l2 && std::get<2>(c) >= k; }); + [&](constraint const & c) { return std::get<0>(c) == u && std::get<1>(c) == v && std::get<2>(c) >= k; }); } - /** \brief Return true iff l1 >= l2 + k */ + /** \brief Return true iff l1 >= l2 + k by asserted universe constraints. */ bool is_ge(level const & l1, level const & l2, int k) { if (l1 == l2) return k == 0; @@ -109,6 +76,7 @@ struct environment::imp { return false; } + /** \brief Return true iff l1 >= l2 is implied by asserted universe constraints. */ bool is_ge(level const & l1, level const & l2) { if (has_parent()) return m_parent->is_ge(l1, l2); @@ -116,6 +84,7 @@ struct environment::imp { return is_ge(l1, l2, 0); } + /** \brief Add a new universe variable */ level add_var(name const & n) { if (std::any_of(m_uvars.begin(), m_uvars.end(), [&](level const & l){ return uvar_name(l) == n; })) throw exception("invalid universe variable declaration, it has already been declared"); @@ -124,24 +93,37 @@ struct environment::imp { return r; } - void add_constraint(level const & l1, level const & l2, int d) { - if (is_implied(l1, l2, d)) + /** + \brief Add basic constraint u >= v + d, and all basic + constraints implied by transitivity. + + \pre is_uvar(u) && is_uvar(v) + */ + void add_constraint(level const & u, level const & v, int d) { + lean_assert(is_uvar(u) && is_uvar(v)); + if (is_implied(u, v, d)) return; // redundant buffer to_add; for (constraint const & c : m_constraints) { - if (std::get<0>(c) == l2) { + if (std::get<0>(c) == v) { level const & l3 = std::get<1>(c); - int l1_l3_d = safe_add(d, std::get<2>(c)); - if (!is_implied(l1, l3, l1_l3_d)) - to_add.push_back(constraint(l1, l3, l1_l3_d)); + int u_l3_d = safe_add(d, std::get<2>(c)); + if (!is_implied(u, l3, u_l3_d)) + to_add.push_back(constraint(u, l3, u_l3_d)); } } - m_constraints.push_back(constraint(l1, l2, d)); + m_constraints.push_back(constraint(u, v, d)); for (constraint const & c: to_add) { m_constraints.push_back(c); } } + /** + \brief Add all basic constraints implied by n >= l + k + + A basic constraint is a constraint of the form u >= v + k + where u and v are universe variables. + */ void add_constraints(level const & n, level const & l, int k) { lean_assert(is_uvar(n)); switch (kind(l)) { @@ -152,6 +134,7 @@ struct environment::imp { lean_unreachable(); } + /** \brief Add a new universe variable with constraint n >= l */ level add_uvar(name const & n, level const & l) { if (has_parent()) throw exception("invalid universe declaration, universe variables can only be declared in top-level environments"); @@ -162,6 +145,11 @@ struct environment::imp { return r; } + /** + \brief Return the universe variable with given name. Throw an + exception if the environment and its ancestors do not + contain a universe variable named \c n. + */ level get_uvar(name const & n) const { if (has_parent()) { return m_parent->get_uvar(n); @@ -177,10 +165,14 @@ struct environment::imp { } } + /** + \brief Initialize the set of universe variables with bottom + */ void init_uvars() { m_uvars.push_back(level()); } + /** \brief Display universe variable constraints */ void display_uvars(std::ostream & out) const { for (constraint const & c : m_constraints) { out << uvar_name(std::get<0>(c)) << " >= " << uvar_name(std::get<1>(c)); @@ -190,12 +182,16 @@ struct environment::imp { } } + /** \brief Throw exception if environment has children. */ void check_no_children() { if (has_children()) throw exception("invalid object declaration, environment has children environments"); } - void check_name(name const & n) { + /** \brief Throw exception if environment or its ancestors already have an object with the given name. */ + void check_name_core(name const & n) { + if (has_parent()) + m_parent->check_name_core(n); if (m_object_dictionary.find(n) != m_object_dictionary.end()) { std::ostringstream s; s << "environment already contains an object with name '" << n << "'"; @@ -203,32 +199,84 @@ struct environment::imp { } } - void check_add(name const & n) { + void check_name(name const & n) { check_no_children(); + check_name_core(n); + } + + /** + \brief Throw an exception if \c t is not a type or type of \c + v is not convertible to \c t. + + \remark env is the smart pointer of imp. We need it because + infer_universe and infer_type expect an environment instead of environment::imp. + */ + void check_type(name const & n, expr const & t, expr const & v, environment const & env) { + infer_universe(t, env); + expr v_t = infer_type(v, env); + if (!is_convertible(t, v_t, env)) { + std::ostringstream buffer; + buffer << "type mismatch when defining '" << n << "'\n" + << "expected type:\n" << t << "\n" + << "given type:\n" << v_t; + throw exception(buffer.str()); + } + } + + /** \brief Throw exception if it is not a valid new definition */ + void check_new_definition(name const & n, expr const & t, expr const & v, environment const & env) { check_name(n); + check_type(n, t, v, env); } - void add_definition(name const & n, expr const & t, expr const & v, bool opaque) { - m_objects.push_back(new definition(n, t, v, opaque)); - m_object_dictionary.insert(std::make_pair(n, m_objects.back())); + /** \brief Store new named object inside internal data-structures */ + void register_named_object(named_object * new_obj) { + m_objects.push_back(new_obj); + m_object_dictionary.insert(std::make_pair(new_obj->get_name(), new_obj)); } - void add_theorem(name const & n, expr const & t, expr const & v) { - m_objects.push_back(new theorem(n, t, v)); - m_object_dictionary.insert(std::make_pair(n, m_objects.back())); + /** \brief Add new definition. */ + void add_definition(name const & n, expr const & t, expr const & v, bool opaque, environment const & env) { + check_new_definition(n, t, v, env); + register_named_object(new definition(n, t, v, opaque)); } - void add_axiom(name const & n, expr const & t) { - m_objects.push_back(new axiom(n, t)); - m_object_dictionary.insert(std::make_pair(n, m_objects.back())); + /** + \brief Add new definition. + The type of the new definition is the type of \c v. + */ + void add_definition(name const & n, expr const & v, bool opaque, environment const & env) { + check_name(n); + expr v_t = infer_type(v, env); + register_named_object(new definition(n, v_t, v, opaque)); } - void add_var(name const & n, expr const & t) { - m_objects.push_back(new variable(n, t)); - m_object_dictionary.insert(std::make_pair(n, m_objects.back())); + /** \brief Add new theorem. */ + void add_theorem(name const & n, expr const & t, expr const & v, environment const & env) { + check_new_definition(n, t, v, env); + register_named_object(new theorem(n, t, v)); } - object const * get_object_ptr(name const & n) const { + /** \brief Add new axiom. */ + void add_axiom(name const & n, expr const & t, environment const & env) { + check_name(n); + infer_universe(t, env); + register_named_object(new axiom(n, t)); + } + + /** \brief Add new variable. */ + void add_var(name const & n, expr const & t, environment const & env) { + check_name(n); + infer_universe(t, env); + register_named_object(new variable(n, t)); + } + + /** + \brief Return the object named \c n in the environment or its + ancestors. Return nullptr if there is not object with the + given name. + */ + named_object const * get_object_ptr(name const & n) const { auto it = m_object_dictionary.find(n); if (it == m_object_dictionary.end()) { if (has_parent()) @@ -240,8 +288,8 @@ struct environment::imp { } } - object const & get_object(name const & n) const { - object const * ptr = get_object_ptr(n); + named_object const & get_object(name const & n) const { + named_object const * ptr = get_object_ptr(n); if (ptr) { return *ptr; } else { @@ -331,55 +379,31 @@ level environment::get_uvar(name const & n) const { return m_imp->get_uvar(n); } -void environment::check_type(name const & n, expr const & t, expr const & v) { - infer_universe(t, *this); - expr v_t = infer_type(v, *this); - if (!is_convertible(t, v_t, *this)) { - std::ostringstream buffer; - buffer << "type mismatch when defining '" << n << "'\n" - << "expected type:\n" << t << "\n" - << "given type:\n" << v_t; - throw exception(buffer.str()); - } -} - void environment::add_definition(name const & n, expr const & t, expr const & v, bool opaque) { - m_imp->check_no_children(); - m_imp->check_name(n); - check_type(n, t, v); - m_imp->add_definition(n, t, v, opaque); + m_imp->add_definition(n, t, v, opaque, *this); } void environment::add_theorem(name const & n, expr const & t, expr const & v) { - m_imp->check_no_children(); - m_imp->check_name(n); - check_type(n, t, v); - m_imp->add_theorem(n, t, v); + m_imp->add_theorem(n, t, v, *this); } void environment::add_definition(name const & n, expr const & v, bool opaque) { - m_imp->check_add(n); - expr v_t = infer_type(v, *this); - m_imp->add_definition(n, v_t, v, opaque); + m_imp->add_definition(n, v, opaque, *this); } void environment::add_axiom(name const & n, expr const & t) { - m_imp->check_add(n); - infer_universe(t, *this); - m_imp->add_axiom(n, t); + m_imp->add_axiom(n, t, *this); } void environment::add_var(name const & n, expr const & t) { - m_imp->check_add(n); - infer_universe(t, *this); - m_imp->add_var(n, t); + m_imp->add_var(n, t, *this); } -environment::object const & environment::get_object(name const & n) const { +named_object const & environment::get_object(name const & n) const { return m_imp->get_object(n); } -environment::object const * environment::get_object_ptr(name const & n) const { +named_object const * environment::get_object_ptr(name const & n) const { return m_imp->get_object_ptr(n); } @@ -387,7 +411,7 @@ unsigned environment::get_num_objects() const { return m_imp->m_objects.size(); } -environment::object const & environment::get_object(unsigned i) const { +object const & environment::get_object(unsigned i) const { return *(m_imp->m_objects[i]); } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 2d91dd059..ed51d9e54 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -7,7 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include -#include "expr.h" +#include "object.h" #include "level.h" namespace lean { @@ -16,8 +16,6 @@ namespace lean { datatypes, universe variables, et.c */ class environment { -public: - class object; private: struct imp; std::shared_ptr m_imp; @@ -80,86 +78,6 @@ public: // ======================================= // Environment Objects - enum class object_kind { Definition, Theorem, Var, Axiom }; - /** - \brief Base class for environment objects - It is just a place holder at this point. - */ - class object { - protected: - public: - object() {} - object(object const & o) = delete; - object & operator=(object const & o) = delete; - - virtual ~object() {} - virtual object_kind kind() const = 0; - virtual void display(std::ostream & out) const = 0; - virtual format pp(environment const &) const = 0; - virtual expr const & get_type() const = 0; - virtual char const * header() const = 0; - }; - - class definition : public object { - name m_name; - expr m_type; - expr m_value; - bool m_opaque; - public: - definition(name const & n, expr const & t, expr const & v, bool opaque); - virtual ~definition(); - virtual object_kind kind() const { return object_kind::Definition; } - name const & get_name() const { return m_name; } - virtual expr const & get_type() const { return m_type; } - expr const & get_value() const { return m_value; } - bool is_opaque() const { return m_opaque; } - virtual void display(std::ostream & out) const; - virtual format pp(environment const & env) const; - virtual char const * header() const { return "Definition"; } - }; - - class theorem : public definition { - public: - theorem(name const & n, expr const & t, expr const & v):definition(n, t, v, true) {} - virtual object_kind kind() const { return object_kind::Theorem; } - virtual char const * header() const { return "Theorem"; } - }; - - class fact : public object { - protected: - name m_name; - expr m_type; - public: - fact(name const & n, expr const & t); - virtual ~fact(); - name const & get_name() const { return m_name; } - virtual expr const & get_type() const { return m_type; } - virtual void display(std::ostream & out) const; - virtual format pp(environment const &) const; - }; - - class axiom : public fact { - public: - axiom(name const & n, expr const & t):fact(n, t) {} - virtual object_kind kind() const { return object_kind::Axiom; } - virtual char const * header() const { return "Axiom"; } - }; - - class variable : public fact { - public: - variable(name const & n, expr const & t):fact(n, t) {} - virtual object_kind kind() const { return object_kind::Var; } - virtual char const * header() const { return "Variable"; } - }; - - friend bool is_definition(object const & o) { return o.kind() == object_kind::Definition; } - friend bool is_axiom(object const & o) { return o.kind() == object_kind::Axiom; } - friend bool is_var(object const & o) { return o.kind() == object_kind::Var; } - friend bool is_fact(object const & o) { return is_axiom(o) || is_var(o); } - - friend definition const & to_definition(object const & o) { lean_assert(is_definition(o)); return static_cast(o); } - friend fact const & to_fact(object const & o) { lean_assert(is_fact(o)); return static_cast(o); } - /** \brief Add a new definition n : t := v. It throws an exception if v does not have type t. @@ -187,13 +105,13 @@ public: \brief Return the object with the given name. It throws an exception if the environment does not have an object with the given name. */ - object const & get_object(name const & n) const; + named_object const & get_object(name const & n) const; /** \brief Return the object with the given name. Return nullptr if there is no object with the given name. */ - object const * get_object_ptr(name const & n) const; + named_object const * get_object_ptr(name const & n) const; /** \brief Iterator for Lean environment objects. */ class object_iterator { diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index dd5c8b90b..caced6aca 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -19,6 +19,13 @@ unsigned hash_args(unsigned size, expr const * args) { return hash(size, [&args](unsigned i){ return args[i].hash(); }); } +static expr g_null; + +expr const & expr::null() { + lean_assert(!g_null); + return g_null; +} + expr_cell::expr_cell(expr_kind k, unsigned h): m_kind(static_cast(k)), m_flags(0), diff --git a/src/kernel/expr.h b/src/kernel/expr.h index c5293e671..8b33cd1d1 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -79,6 +79,8 @@ public: expr(expr && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } ~expr() { if (m_ptr) m_ptr->dec_ref(); } + static expr const & null(); + friend void swap(expr & a, expr & b) { std::swap(a.m_ptr, b.m_ptr); } void release() { if (m_ptr) m_ptr->dec_ref(); m_ptr = nullptr; } @@ -410,6 +412,17 @@ struct args { expr copy(expr const & e); // ======================================= +// ======================================= +// Expression formatter +class expr_formatter { +public: + virtual ~expr_formatter() {} + virtual format operator()(expr const & e) = 0; + virtual options const & get_options() const = 0; +}; +// ======================================= + + // ======================================= // Update template expr update_app(expr const & e, F f) { diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp index b1d208123..fdf13d190 100644 --- a/src/kernel/normalize.cpp +++ b/src/kernel/normalize.cpp @@ -133,9 +133,9 @@ class normalize_fn { case expr_kind::Var: return lookup(s, var_idx(a), k); case expr_kind::Constant: { - environment::object const & obj = m_env.get_object(const_name(a)); - if (is_definition(obj) && !to_definition(obj).is_opaque()) { - return normalize(to_definition(obj).get_value(), value_stack(), 0); + named_object const & obj = m_env.get_object(const_name(a)); + if (obj.is_definition() && !obj.is_opaque()) { + return normalize(obj.get_value(), value_stack(), 0); } else { return svalue(a); diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp new file mode 100644 index 000000000..2f31512ac --- /dev/null +++ b/src/kernel/object.cpp @@ -0,0 +1,74 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "object.h" +#include "environment.h" +#include "pp.h" // TODO: move to front-end + +namespace lean { +// TODO: delete hardcoded +format pp_object_kind(char const * n) { return highlight(format(n), format::format_color::BLUE); } +constexpr unsigned indentation = 2; // TODO: must be option +// + +object::~object() {} +void object::display(std::ostream & out, environment const & env) const { out << pp(env); } + +anonymous_object::~anonymous_object() {} +bool anonymous_object::has_name() const { return false; } +name const & anonymous_object::get_name() const { lean_unreachable(); return name::anonymous(); } +bool anonymous_object::has_type() const { return false; } +expr const & anonymous_object::get_type() const { lean_unreachable(); return expr::null(); } +bool anonymous_object::is_definition() const { return false; } +bool anonymous_object::is_opaque() const { lean_unreachable(); return false; } +expr const & anonymous_object::get_value() const { lean_unreachable(); return expr::null(); } + +named_object::named_object(name const & n, expr const & t):m_name(n), m_type(t) {} +named_object::~named_object() {} +bool named_object::has_name() const { return true; } +name const & named_object::get_name() const { return m_name; } +bool named_object::has_type() const { return true; } +expr const & named_object::get_type() const { return m_type; } + +char const * definition::g_keyword = "Definition"; +definition::definition(name const & n, expr const & t, expr const & v, bool opaque):named_object(n, t), m_value(v), m_opaque(opaque) {} +definition::~definition() {} +char const * definition::keyword() const { return g_keyword; } +bool definition::is_definition() const { return true; } +bool definition::is_opaque() const { return m_opaque; } +expr const & definition::get_value() const { return m_value; } +format definition::pp(environment const & env) const { + return nest(indentation, + format{pp_object_kind(keyword()), format(" "), format(get_name()), format(" : "), ::lean::pp(get_type(), env), format(" :="), + line(), ::lean::pp(get_value()), format(".")}); +} + +char const * theorem::g_keyword = "Theorem"; +theorem::theorem(name const & n, expr const & t, expr const & v):definition(n, t, v, true) {} +theorem::~theorem() {} +char const * theorem::keyword() const { return g_keyword; } + +fact::fact(name const & n, expr const & t):named_object(n, t) {} +fact::~fact() {} +bool fact::is_definition() const { return false; } +bool fact::is_opaque() const { lean_unreachable(); return false; } +expr const & fact::get_value() const { lean_unreachable(); return expr::null(); } +format fact::pp(environment const & env) const { + return nest(indentation, + format{pp_object_kind(keyword()), format(" "), format(get_name()), format(" : "), ::lean::pp(get_type(), env), format(".")}); +} + +char const * axiom::g_keyword = "Axiom"; +axiom::axiom(name const & n, expr const & t):fact(n, t) {} +axiom::~axiom() {} +char const * axiom::keyword() const { return g_keyword; } + +char const * variable::g_keyword = "Variable"; +variable::variable(name const & n, expr const & t):fact(n, t) {} +variable::~variable() {} +char const * variable::keyword() const { return g_keyword; } +} + diff --git a/src/kernel/object.h b/src/kernel/object.h new file mode 100644 index 000000000..45a0c91b3 --- /dev/null +++ b/src/kernel/object.h @@ -0,0 +1,171 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "expr.h" + +/* + Kernel objects. + + We use abstract classes and virtual methods because a kernel + frontend may need to create new objects for bookkeeping. +*/ +namespace lean { +class environment; + +/** + \brief Abstract class used to represent kernel objects (i.e., + definitions, theorems, axioms, recursive definitions, etc) +*/ +class object { +protected: +public: + object() {} + object(object const & o) = delete; + object & operator=(object const & o) = delete; + virtual ~object(); + + /** + \brief Return the keyword used to define this object in a Lean + file. The keyword is also used to identify the class of an object. + */ + virtual char const * keyword() const = 0; + + /** \brief Pretty print this object. */ + virtual format pp(environment const &) const = 0; + + /** \brief Display the object in the standard output. */ + virtual void display(std::ostream & out, environment const &) const; + + /** \brief Return true iff object has a name. */ + virtual bool has_name() const = 0; + + /** \brief Return object name. \pre has_name() */ + virtual name const & get_name() const = 0; + + /** \brief Return true iff object has a type. */ + virtual bool has_type() const = 0; + + /** \brief Return object type. \pre has_type() */ + virtual expr const & get_type() const = 0; + + /** \brief Return true iff object is a definition */ + virtual bool is_definition() const = 0; + + /** \brief Return true iff the definition is opaque. \pre is_definition() */ + virtual bool is_opaque() const = 0; + + /** \brief Return object value. \pre is_definition() */ + virtual expr const & get_value() const = 0; +}; + +/** + \brief Anonymous objects are mainly used for bookkeeping. +*/ +class anonymous_object : public object { +public: + virtual ~anonymous_object(); + + virtual bool has_name() const; + virtual name const & get_name() const; + + virtual bool has_type() const; + virtual expr const & get_type() const; + + virtual bool is_definition() const; + virtual bool is_opaque() const; + virtual expr const & get_value() const; +}; + +/** + \brief Named (and typed) kernel objects. +*/ +class named_object : public object { + name m_name; + expr m_type; +public: + named_object(name const & n, expr const & t); + virtual ~named_object(); + + virtual bool has_name() const; + virtual name const & get_name() const; + + virtual bool has_type() const; + virtual expr const & get_type() const; +}; + +/** + \brief Non-recursive definitions. +*/ +class definition : public named_object { + expr m_value; + bool m_opaque; // Opaque definitions are ignored by definitional equality. +public: + definition(name const & n, expr const & t, expr const & v, bool opaque); + virtual ~definition(); + + static char const * g_keyword; + virtual char const * keyword() const; + + virtual bool is_definition() const; + virtual bool is_opaque() const; + virtual expr const & get_value() const; + + virtual format pp(environment const & env) const; +}; + +/** + \brief A theorem is essentially an opaque definition. +*/ +class theorem : public definition { +public: + theorem(name const & n, expr const & t, expr const & v); + virtual ~theorem(); + + static char const * g_keyword; + virtual char const * keyword() const; +}; + +/** + \brief Base class for named objects that are not definitions. +*/ +class fact : public named_object { +public: + fact(name const & n, expr const & t); + virtual ~fact(); + + virtual bool is_definition() const; + virtual bool is_opaque() const; + virtual expr const & get_value() const; + + virtual format pp(environment const & env) const; +}; + +/** + \brief Axioms +*/ +class axiom : public fact { +public: + axiom(name const & n, expr const & t); + virtual ~axiom(); + + static char const * g_keyword; + virtual char const * keyword() const; +}; + +/** + \brief Variable postulate. It is like an axiom since we are + essentially postulating that a type is inhabited. +*/ +class variable : public fact { +public: + variable(name const & n, expr const & t); + virtual ~variable(); + + static char const * g_keyword; + virtual char const * keyword() const; +}; +} diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 5d55f9c0f..297a0e764 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -68,6 +68,7 @@ static void tst3() { std::cout << "expected error: " << ex.what() << "\n"; } env.add_definition("a", Int, iAdd(iVal(1), iVal(2))); + std::cout << env << "\n"; expr t = iAdd(Const("a"), iVal(1)); std::cout << t << " --> " << normalize(t, env) << "\n"; lean_assert(normalize(t, env) == iVal(4)); @@ -169,7 +170,7 @@ static void tst7() { int main() { enable_trace("is_convertible"); - continue_on_violation(true); + // continue_on_violation(true); tst1(); tst2(); tst3(); diff --git a/src/util/name.cpp b/src/util/name.cpp index 22fa0e8f9..d6315614e 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -140,6 +140,13 @@ name::~name() { m_ptr->dec_ref(); } +static name g_anonymous; + +name const & name::anonymous() { + lean_assert(g_anonymous.is_anonymous()); + return g_anonymous; +} + name & name::operator=(name const & other) { LEAN_COPY_REF(name, other); } name & name::operator=(name && other) { LEAN_MOVE_REF(name, other); } diff --git a/src/util/name.h b/src/util/name.h index fcb2ba570..fdb5d57d0 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -28,6 +28,7 @@ public: name(name && other); name(std::initializer_list const & l); ~name(); + static name const & anonymous(); name & operator=(name const & other); name & operator=(name && other); friend bool operator==(name const & a, name const & b);