michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel): parametric kernel objects

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-23 14:41:44 -08:00
parent 54801bbd05
commit 916301bdfb
9 changed files with 190 additions and 105 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/kernel/constraint.h
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <algorithm>
#include "kernel/expr.h"
#include "kernel/justification.h"
namespace lean {

40
src/kernel/environment.cpp
View file

@ -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) {

19
src/kernel/environment.h
View file

@ -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<object> 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<std::string> 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.

15
src/kernel/expr.cpp
View file

@ -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<level> 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<expr, expr_hash_alloc, expr_eqp> {
typedef object_serializer<expr, expr_hash_alloc, expr_eqp> super;
max_sharing_fn m_max_sharing_fn;

1
src/kernel/expr.h
View file

@ -25,7 +25,6 @@ Author: Leonardo de Moura
namespace lean {
class expr;
typedef list<level> levels;
/* =======================================
Expressions
expr ::= Var idx

55
src/kernel/level.cpp
View file

@ -394,6 +394,61 @@ level read_level(deserializer & d) {
return d.get_extension<level_deserializer>(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<level> 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<level_cnstr> 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) {

21
src/kernel/level.h
View file

@ -7,9 +7,11 @@ Author: Leonardo de Moura
#pragma once
#include <iostream>
#include <algorithm>
#include <utility>
#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<level> levels;
/**
\brief Simpler version of the constraint class.
We use in the definition of objects.
*/
typedef std::pair<level, level> level_cnstr;
typedef list<level_cnstr> 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. */

117
src/kernel/object.cpp
View file

@ -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)); }
}

26
src/kernel/object.h
View file

@ -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<object> none_object() { return optional<object>(); }
inline optional<object> some_object(object const & o) { return optional<object>(o); }
inline optional<object> some_object(object && o) { return optional<object>(std::forward<object>(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);