diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h index ebd0e2879..d1a8a66d2 100644 --- a/src/kernel/constraint.h +++ b/src/kernel/constraint.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include "kernel/expr.h" #include "kernel/justification.h" namespace lean { diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 2b3f006cd..d123a442f 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -199,6 +199,13 @@ void environment_cell::check_name(name const & n) { check_name_core(n); } +void environment_cell::check_level_cnstrs(unsigned num_param, level_cnstrs const & ls) { + if (get_meta_range(ls) > 0) + throw_kernel_exception(env(), "invalid level constraint, it contains level placeholders (aka meta-parameters that must be synthesized by Lean's elaborator"); + if (get_param_range(ls) > num_param) + throw_kernel_exception(env(), "invalid level constraints, it contains undefined parameters"); +} + /** \brief Store new named object inside internal data-structures */ void environment_cell::register_named_object(object const & new_obj) { m_objects.push_back(new_obj); @@ -263,27 +270,26 @@ void environment_cell::check_type(expr const & t) { } /** \brief Throw exception if it is not a valid new definition */ -void environment_cell::check_new_definition(name const & n, expr const & t, expr const & v) { +void environment_cell::check_new_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v) { check_name(n); + check_level_cnstrs(num_param, cs); check_type(n, t, v); } /** \brief Add new definition. */ -void environment_cell::add_definition(name const & n, expr const & t, expr const & v, bool opaque) { +void environment_cell::add_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v) { check_no_mlocal(t); check_no_mlocal(v); - check_new_definition(n, t, v); + check_new_definition(n, num_param, cs, t, v); unsigned w = get_max_weight(v) + 1; - register_named_object(mk_definition(n, t, v, w)); - if (opaque) - set_opaque(n, opaque); + register_named_object(mk_definition(n, num_param, cs, t, v, w)); } /** \brief Add new definition. The type of the new definition is the type of \c v. */ -void environment_cell::add_definition(name const & n, expr const & v, bool opaque) { +void environment_cell::add_definition(name const & n, expr const & v) { check_no_mlocal(v); check_name(n); expr v_t; @@ -294,17 +300,15 @@ void environment_cell::add_definition(name const & n, expr const & v, bool opaqu v_t = m_type_checker->infer_type(v); #endif unsigned w = get_max_weight(v) + 1; - register_named_object(mk_definition(n, v_t, v, w)); - if (opaque) - set_opaque(n, opaque); + register_named_object(mk_definition(n, 0, level_cnstrs(), v_t, v, w)); } /** \brief Add new theorem. */ -void environment_cell::add_theorem(name const & n, expr const & t, expr const & v) { +void environment_cell::add_theorem(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v) { check_no_mlocal(t); check_no_mlocal(v); - check_new_definition(n, t, v); - register_named_object(mk_theorem(n, t, v)); + check_new_definition(n, num_param, cs, t, v); + register_named_object(mk_theorem(n, num_param, cs, t, v)); } void environment_cell::set_opaque(name const & n, bool opaque) { @@ -316,19 +320,21 @@ void environment_cell::set_opaque(name const & n, bool opaque) { } /** \brief Add new axiom. */ -void environment_cell::add_axiom(name const & n, expr const & t) { +void environment_cell::add_axiom(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t) { check_no_mlocal(t); check_name(n); + check_level_cnstrs(num_param, cs); check_type(t); - register_named_object(mk_axiom(n, t)); + register_named_object(mk_axiom(n, num_param, cs, t)); } /** \brief Add new variable. */ -void environment_cell::add_var(name const & n, expr const & t) { +void environment_cell::add_var(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t) { check_no_mlocal(t); check_name(n); + check_level_cnstrs(num_param, cs); check_type(t); - register_named_object(mk_var_decl(n, t)); + register_named_object(mk_var_decl(n, num_param, cs, t)); } void environment_cell::add_neutral_object(neutral_object_cell * o) { diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 9cf1e8e36..5bdafbe03 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -62,13 +62,15 @@ class environment_cell { void check_name_core(name const & n); void check_name(name const & n); + void check_level_cnstrs(unsigned num_param, level_cnstrs const & ls); + void register_named_object(object const & new_obj); optional get_object_core(name const & n) const; void check_no_mlocal(expr const & e); void check_type(name const & n, expr const & t, expr const & v); void check_type(expr const & t); - void check_new_definition(name const & n, expr const & t, expr const & v); + void check_new_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v); bool mark_imported_core(name n); bool load_core(std::string const & fname, io_state const & ios, optional const & mod_name); @@ -106,15 +108,16 @@ public: It throws an exception if v does not have type t. It throws an exception if there is already an object with the given name. */ - void add_definition(name const & n, expr const & t, expr const & v, bool opaque = false); - void add_opaque_definition(name const & n, expr const & t, expr const & v) { add_definition(n, t, v, true); } - void add_theorem(name const & n, expr const & t, expr const & v); + void add_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v); + void add_theorem(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v); + void add_definition(name const & n, expr const & t, expr const & v) { add_definition(n, 0, level_cnstrs(), t, v); } + void add_theorem(name const & n, expr const & t, expr const & v) { add_theorem(n, 0, level_cnstrs(), t, v); } /** \brief Add a new definition n : infer_type(v) := v. It throws an exception if there is already an object with the given name. */ - void add_definition(name const & n, expr const & v, bool opaque = false); + void add_definition(name const & n, expr const & v); /** \brief Set the given definition as opaque (or not) @@ -127,8 +130,10 @@ public: \brief Add a new fact (Axiom or Fact) to the environment. It throws an exception if there is already an object with the given name. */ - void add_axiom(name const & n, expr const & t); - void add_var(name const & n, expr const & t); + void add_axiom(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t); + void add_var(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t); + void add_axiom(name const & n, expr const & t) { add_axiom(n, 0, level_cnstrs(), t); } + void add_var(name const & n, expr const & t) { add_var(n, 0, level_cnstrs(), t); }; /** \brief Register the given unanymous object in this environment. diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 1aec509ba..a88ff56ea 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -420,21 +420,6 @@ expr copy(expr const & a) { lean_unreachable(); // LCOV_EXCL_LINE } -serializer & operator<<(serializer & s, levels const & ls) { - s << length(ls); - for (auto const & l : ls) - s << l; - return s; -} - -levels read_levels(deserializer & d) { - unsigned num = d.read_unsigned(); - buffer ls; - for (unsigned i = 0; i < num; i++) - ls.push_back(read_level(d)); - return to_list(ls.begin(), ls.end()); -} - class expr_serializer : public object_serializer { typedef object_serializer super; max_sharing_fn m_max_sharing_fn; diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 6c5daf3b9..54962cd3d 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -25,7 +25,6 @@ Author: Leonardo de Moura namespace lean { class expr; -typedef list levels; /* ======================================= Expressions expr ::= Var idx diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 136b9145b..d3f347ece 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -394,6 +394,61 @@ level read_level(deserializer & d) { return d.get_extension(g_level_sd.m_d_extid).read(); } +serializer & operator<<(serializer & s, levels const & ls) { + s << length(ls); + for (auto const & l : ls) + s << l; + return s; +} + +levels read_levels(deserializer & d) { + unsigned num = d.read_unsigned(); + buffer ls; + for (unsigned i = 0; i < num; i++) + ls.push_back(read_level(d)); + return to_list(ls.begin(), ls.end()); +} + +serializer & operator<<(serializer & s, level_cnstrs const & cs) { + s << length(cs); + for (auto const & p : cs) + s << p.first << p.second; + return s; +} + +level_cnstrs read_level_cnstrs(deserializer & d) { + unsigned num = d.read_unsigned(); + buffer cs; + for (unsigned i = 0; i < num; i++) { + level lhs = read_level(d); + level rhs = read_level(d); + cs.push_back(level_cnstr(lhs, rhs)); + } + return to_list(cs.begin(), cs.end()); +} + +unsigned get_param_range(level_cnstr const & c) { + return std::max(get_param_range(c.first), get_param_range(c.second)); +} + +unsigned get_param_range(level_cnstrs const & cs) { + unsigned r = 0; + for (auto const & c : cs) + r = std::max(r, get_param_range(c)); + return r; +} + +unsigned get_meta_range(level_cnstr const & c) { + return std::max(get_meta_range(c.first), get_meta_range(c.second)); +} + +unsigned get_meta_range(level_cnstrs const & cs) { + unsigned r = 0; + for (auto const & c : cs) + r = std::max(r, get_meta_range(c)); + return r; +} + static void print(std::ostream & out, level l); static void print_child(std::ostream & out, level const & l) { diff --git a/src/kernel/level.h b/src/kernel/level.h index 3b56663ba..77cbbbacb 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -7,9 +7,11 @@ Author: Leonardo de Moura #pragma once #include #include +#include #include "util/name.h" #include "util/optional.h" #include "util/serializer.h" +#include "util/list.h" #include "util/sexpr/format.h" #include "util/sexpr/options.h" @@ -119,6 +121,19 @@ inline bool has_meta(level const & l) { return get_meta_range(l) > 0; } */ bool is_trivial(level const & lhs, level const & rhs); +typedef list levels; + +/** + \brief Simpler version of the constraint class. + We use in the definition of objects. +*/ +typedef std::pair level_cnstr; +typedef list level_cnstrs; + +unsigned get_param_range(level_cnstr const & c); +unsigned get_param_range(level_cnstrs const & cs); +unsigned get_meta_range(level_cnstr const & c); +unsigned get_meta_range(level_cnstrs const & cs); /** \brief Printer for debugging purposes @@ -135,6 +150,12 @@ serializer & operator<<(serializer & s, level const & l); level read_level(deserializer & d); inline deserializer & operator>>(deserializer & d, level & l) { l = read_level(d); return d; } +serializer & operator<<(serializer & s, levels const & ls); +levels read_levels(deserializer & d); + +serializer & operator<<(serializer & s, level_cnstrs const & cs); +level_cnstrs read_level_cnstrs(deserializer & d); + /** \brief Pretty print the given level expression, unicode characters are used if \c unicode is \c true. */ format pp(level l, bool unicode, unsigned indent); /** \brief Pretty print the given level expression using the given configuration options. */ diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp index e0f04c407..107cb0180 100644 --- a/src/kernel/object.cpp +++ b/src/kernel/object.cpp @@ -32,41 +32,32 @@ void read_object(environment const & env, io_state const & ios, std::string cons neutral_object_cell::neutral_object_cell():object_cell(object_kind::Neutral) {} /** - \brief Named kernel objects. - - \remark All nonneutral objects have names. + \brief Parametric kernel objects. */ -class named_object_cell : public object_cell { - name m_name; +class parametric_object_cell : public object_cell { + name m_name; + unsigned m_num_params; + level_cnstrs m_cnstrs; + expr m_type; public: - named_object_cell(object_kind k, name const & n):object_cell(k), m_name(n) {} - virtual ~named_object_cell() {} + parametric_object_cell(object_kind k, name const & n, unsigned num_params, level_cnstrs const & cs, expr const & t): + object_cell(k), m_name(n), m_num_params(num_params), m_cnstrs(cs), m_type(t) {} + virtual ~parametric_object_cell() {} virtual bool has_name() const { return true; } virtual name get_name() const { return m_name; } -}; - -/** - \brief Named (and typed) kernel objects. -*/ -class named_typed_object_cell : public named_object_cell { - expr m_type; -public: - named_typed_object_cell(object_kind k, name const & n, expr const & t): - named_object_cell(k, n), m_type(t) {} - virtual ~named_typed_object_cell() {} - - virtual bool has_type() const { return true; } virtual expr get_type() const { return m_type; } + virtual unsigned get_num_level_params() const { return m_num_params; } + level_cnstrs const & get_level_cnstrs() const { return m_cnstrs; } }; /** \brief Base class for Axioms and Variable declarations. */ -class postulate_object_cell : public named_typed_object_cell { +class postulate_object_cell : public parametric_object_cell { public: - postulate_object_cell(name const & n, expr const & t): - named_typed_object_cell(object_kind::Postulate, n, t) {} + postulate_object_cell(name const & n, unsigned num_params, level_cnstrs const & cs, expr const & t): + parametric_object_cell(object_kind::Postulate, n, num_params, cs, t) {} }; /** @@ -74,15 +65,18 @@ public: */ class axiom_object_cell : public postulate_object_cell { public: - axiom_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {} + axiom_object_cell(name const & n, unsigned num_params, level_cnstrs const & cs, expr const & t): + postulate_object_cell(n, num_params, cs, t) {} virtual char const * keyword() const { return "axiom"; } virtual bool is_axiom() const { return true; } - virtual void write(serializer & s) const { s << "ax" << get_name() << get_type(); } + virtual void write(serializer & s) const { s << "ax" << get_name() << get_num_level_params() << get_level_cnstrs() << get_type(); } }; static void read_axiom(environment const & env, io_state const &, deserializer & d) { - name n = read_name(d); - expr t = read_expr(d); - env->add_axiom(n, t); + name n = read_name(d); + unsigned num = d.read_unsigned(); + level_cnstrs cs = read_level_cnstrs(d); + expr t = read_expr(d); + env->add_axiom(n, num, cs, t); } static object_cell::register_deserializer_fn axiom_ds("ax", read_axiom); @@ -92,28 +86,31 @@ static object_cell::register_deserializer_fn axiom_ds("ax", read_axiom); */ class variable_decl_object_cell : public postulate_object_cell { public: - variable_decl_object_cell(name const & n, expr const & t):postulate_object_cell(n, t) {} + variable_decl_object_cell(name const & n, unsigned num_params, level_cnstrs const & cs, expr const & t): + postulate_object_cell(n, num_params, cs, t) {} virtual char const * keyword() const { return "variable"; } virtual bool is_var_decl() const { return true; } - virtual void write(serializer & s) const { s << "var" << get_name() << get_type(); } + virtual void write(serializer & s) const { s << "var" << get_name() << get_num_level_params() << get_level_cnstrs() << get_type(); } }; static void read_variable(environment const & env, io_state const &, deserializer & d) { - name n = read_name(d); - expr t = read_expr(d); - env->add_var(n, t); + name n = read_name(d); + unsigned num = d.read_unsigned(); + level_cnstrs cs = read_level_cnstrs(d); + expr t = read_expr(d); + env->add_var(n, num, cs, t); } static object_cell::register_deserializer_fn var_decl_ds("var", read_variable); /** \brief Base class for definitions: theorems and definitions. */ -class definition_object_cell : public named_typed_object_cell { +class definition_object_cell : public parametric_object_cell { expr m_value; bool m_opaque; unsigned m_weight; public: - definition_object_cell(name const & n, expr const & t, expr const & v, unsigned weight): - named_typed_object_cell(object_kind::Definition, n, t), m_value(v), m_opaque(false), m_weight(weight) {} + definition_object_cell(name const & n, unsigned num_params, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight): + parametric_object_cell(object_kind::Definition, n, num_params, cs, t), m_value(v), m_opaque(false), m_weight(weight) {} virtual ~definition_object_cell() {} virtual bool is_definition() const { return true; } @@ -122,13 +119,17 @@ public: virtual expr get_value() const { return m_value; } virtual char const * keyword() const { return "definition"; } virtual unsigned get_weight() const { return m_weight; } - virtual void write(serializer & s) const { s << "def" << get_name() << get_type() << get_value(); } + virtual void write(serializer & s) const { + s << "def" << get_name() << get_num_level_params() << get_level_cnstrs() << get_type() << get_value(); + } }; static void read_definition(environment const & env, io_state const &, deserializer & d) { - name n = read_name(d); - expr t = read_expr(d); - expr v = read_expr(d); - env->add_definition(n, t, v); + name n = read_name(d); + unsigned num = d.read_unsigned(); + level_cnstrs cs = read_level_cnstrs(d); + expr t = read_expr(d); + expr v = read_expr(d); + env->add_definition(n, num, cs, t, v); } static object_cell::register_deserializer_fn definition_ds("def", read_definition); @@ -137,26 +138,36 @@ static object_cell::register_deserializer_fn definition_ds("def", read_definitio */ class theorem_object_cell : public definition_object_cell { public: - theorem_object_cell(name const & n, expr const & t, expr const & v): - definition_object_cell(n, t, v, 0) { + theorem_object_cell(name const & n, unsigned num_params, level_cnstrs const & cs, expr const & t, expr const & v): + definition_object_cell(n, num_params, cs, t, v, 0) { set_opaque(true); } virtual char const * keyword() const { return "theorem"; } virtual bool is_theorem() const { return true; } - virtual void write(serializer & s) const { s << "th" << get_name() << get_type() << get_value(); } + virtual void write(serializer & s) const { + s << "th" << get_name() << get_num_level_params() << get_level_cnstrs() << get_type() << get_value(); + } }; static void read_theorem(environment const & env, io_state const &, deserializer & d) { - name n = read_name(d); - expr t = read_expr(d); - expr v = read_expr(d); - env->add_theorem(n, t, v); + name n = read_name(d); + unsigned num = d.read_unsigned(); + level_cnstrs cs = read_level_cnstrs(d); + expr t = read_expr(d); + expr v = read_expr(d); + env->add_theorem(n, num, cs, t, v); } static object_cell::register_deserializer_fn theorem_ds("th", read_theorem); -object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight) { - return object(new definition_object_cell(n, t, v, weight)); +object mk_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight) { + return object(new definition_object_cell(n, num_param, cs, t, v, weight)); +} +object mk_theorem(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v) { + return object(new theorem_object_cell(n, num_param, cs, t, v)); +} +object mk_axiom(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t) { + return object(new axiom_object_cell(n, num_param, cs, t)); +} +object mk_var_decl(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t) { + return object(new variable_decl_object_cell(n, num_param, cs, t)); } -object mk_theorem(name const & n, expr const & t, expr const & v) { return object(new theorem_object_cell(n, t, v)); } -object mk_axiom(name const & n, expr const & t) { return object(new axiom_object_cell(n, t)); } -object mk_var_decl(name const & n, expr const & t) { return object(new variable_decl_object_cell(n, t)); } } diff --git a/src/kernel/object.h b/src/kernel/object.h index e42617ca9..e1bf033e1 100644 --- a/src/kernel/object.h +++ b/src/kernel/object.h @@ -44,12 +44,13 @@ public: virtual bool has_name() const { return false; } /** \brief Return object name. \pre has_name() */ virtual name get_name() const { lean_unreachable(); } // LCOV_EXCL_LINE + /** \brief Return number of level parameters */ + virtual unsigned get_num_level_params() const { lean_unreachable(); } + /** \brief Return the level constraints associated with a definition/postulate. */ + virtual level_cnstrs const & get_level_cnstrs() const { lean_unreachable(); } - /** \brief Return true iff object has a type. */ - virtual bool has_type() const { return false; } /** \brief Return object type. \pre has_type() */ virtual expr get_type() const { lean_unreachable(); } // LCOV_EXCL_LINE - /** \brief Return true iff object is a definition */ virtual bool is_definition() const { return false; } /** \brief Return true iff the definition is opaque. \pre is_definition() */ @@ -102,16 +103,17 @@ public: object_kind kind() const { return m_ptr->kind(); } - friend object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight); - friend object mk_theorem(name const & n, expr const & t, expr const & v); - friend object mk_axiom(name const & n, expr const & t); - friend object mk_var_decl(name const & n, expr const & t); + friend object mk_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight); + friend object mk_theorem(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v); + friend object mk_axiom(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t); + friend object mk_var_decl(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t); friend object mk_neutral(neutral_object_cell * c); char const * keyword() const { return m_ptr->keyword(); } bool has_name() const { return m_ptr->has_name(); } name get_name() const { return m_ptr->get_name(); } - bool has_type() const { return m_ptr->has_type(); } + unsigned get_num_level_params() const { return m_ptr->get_num_level_params(); } + level_cnstrs const & get_level_cnstrs() const { return m_ptr->get_level_cnstrs(); } expr get_type() const { return m_ptr->get_type(); } bool is_definition() const { return m_ptr->is_definition(); } bool is_opaque() const { return m_ptr->is_opaque(); } @@ -130,10 +132,10 @@ inline optional none_object() { return optional(); } inline optional some_object(object const & o) { return optional(o); } inline optional some_object(object && o) { return optional(std::forward(o)); } -object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight); -object mk_theorem(name const & n, expr const & t, expr const & v); -object mk_axiom(name const & n, expr const & t); -object mk_var_decl(name const & n, expr const & t); +object mk_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight); +object mk_theorem(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v); +object mk_axiom(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t); +object mk_var_decl(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t); inline object mk_neutral(neutral_object_cell * c) { lean_assert(c->get_rc() == 1); return object(c); } void read_object(environment const & env, io_state const & ios, std::string const & k, deserializer & d);