refactor(kernel): replace kernel object with definition, disable affected files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
cb479a75ae
commit
984ac03ac7
11 changed files with 200 additions and 364 deletions
|
|
@ -1,8 +1,8 @@
|
|||
add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
|
||||
for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
|
||||
instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp
|
||||
object.cpp environment.cpp replace_visitor.cpp io_state.cpp
|
||||
normalizer.cpp justification.cpp pos_info_provider.cpp metavar.cpp
|
||||
instantiate.cpp context.cpp formatter.cpp max_sharing.cpp
|
||||
definition.cpp replace_visitor.cpp
|
||||
justification.cpp pos_info_provider.cpp metavar.cpp
|
||||
constraint.cpp type_checker.cpp error_msgs.cpp
|
||||
)
|
||||
|
||||
|
|
|
|||
125
src/kernel/definition.cpp
Normal file
125
src/kernel/definition.cpp
Normal file
|
|
@ -0,0 +1,125 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "kernel/definition.h"
|
||||
|
||||
namespace lean {
|
||||
static serializer & operator<<(serializer & s, param_names const & ps) { return write_list<name>(s, ps); }
|
||||
static param_names read_params(deserializer & d) { return read_list<name>(d); }
|
||||
|
||||
struct definition::cell {
|
||||
MK_LEAN_RC();
|
||||
name m_name;
|
||||
param_names m_params;
|
||||
level_cnstrs m_cnstrs;
|
||||
expr m_type;
|
||||
bool m_theorem;
|
||||
optional<expr> m_value; // if none, then definition is actually a postulate
|
||||
// The following fields are only meaningful for definitions (which are not theorems)
|
||||
unsigned m_weight;
|
||||
unsigned m_module_idx; // module idx where it was defined
|
||||
bool m_opaque;
|
||||
// The following field affects the convertability checker.
|
||||
// Let f be this definition, then if the following field is true,
|
||||
// then whenever we are checking whether
|
||||
// (f a) is convertible to (f b)
|
||||
// we will first check whether a is convertible to b.
|
||||
// If the test fails, then we perform the full check.
|
||||
bool m_use_conv_opt;
|
||||
void dealloc() { delete this; }
|
||||
|
||||
cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, bool is_axiom):
|
||||
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):
|
||||
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) {}
|
||||
|
||||
void write(serializer & s) const {
|
||||
char k = 0;
|
||||
if (m_value) {
|
||||
k |= 1;
|
||||
if (m_opaque)
|
||||
k |= 2;
|
||||
if (m_use_conv_opt)
|
||||
k |= 4;
|
||||
}
|
||||
if (m_theorem)
|
||||
k |= 8;
|
||||
s << k << m_name << m_params << m_cnstrs << m_type;
|
||||
if (m_value) {
|
||||
s << *m_value;
|
||||
if (!m_theorem)
|
||||
s << m_weight;
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
definition::definition(cell * ptr):m_ptr(ptr) {}
|
||||
definition::definition(definition const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
||||
definition::definition(definition && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
|
||||
definition::~definition() { if (m_ptr) m_ptr->dec_ref(); }
|
||||
|
||||
definition & definition::operator=(definition const & s) { LEAN_COPY_REF(s); }
|
||||
definition & definition::operator=(definition && s) { LEAN_MOVE_REF(s); }
|
||||
|
||||
bool definition::is_definition() const { return static_cast<bool>(m_ptr->m_value); }
|
||||
bool definition::is_var_decl() const { return !is_definition(); }
|
||||
bool definition::is_axiom() const { return is_var_decl() && m_ptr->m_theorem; }
|
||||
bool definition::is_theorem() const { return is_definition() && m_ptr->m_theorem; }
|
||||
|
||||
name definition::get_name() const { return m_ptr->m_name; }
|
||||
param_names const & definition::get_params() const { return m_ptr->m_params; }
|
||||
level_cnstrs const & definition::get_level_cnstrs() const { return m_ptr->m_cnstrs; }
|
||||
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; }
|
||||
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) {
|
||||
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) {
|
||||
return definition(new definition::cell(n, params, cs, t, true, v, true, 0, 0, false));
|
||||
}
|
||||
definition mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t) {
|
||||
return definition(new definition::cell(n, params, cs, t, true));
|
||||
}
|
||||
definition mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t) {
|
||||
return definition(new definition::cell(n, params, cs, t, false));
|
||||
}
|
||||
|
||||
definition read_definition(deserializer & d, unsigned module_idx) {
|
||||
char k = d.read_char();
|
||||
bool has_value = (k & 1) != 0;
|
||||
bool is_theorem = (k & 8) != 0;
|
||||
name n = read_name(d);
|
||||
param_names ps = read_params(d);
|
||||
level_cnstrs cs = read_level_cnstrs(d);
|
||||
expr t = read_expr(d);
|
||||
if (has_value) {
|
||||
expr v = read_expr(d);
|
||||
if (is_theorem) {
|
||||
return mk_theorem(n, ps, cs, t, v);
|
||||
} else {
|
||||
unsigned w = d.read_unsigned();
|
||||
bool is_opaque = (k & 2) != 0;
|
||||
bool use_conv_opt = (k & 4) != 0;
|
||||
return mk_definition(n, ps, cs, t, v, is_opaque, w, module_idx, use_conv_opt);
|
||||
}
|
||||
} else {
|
||||
if (is_theorem)
|
||||
return mk_axiom(n, ps, cs, t);
|
||||
else
|
||||
return mk_var_decl(n, ps, cs, t);
|
||||
}
|
||||
}
|
||||
}
|
||||
63
src/kernel/definition.h
Normal file
63
src/kernel/definition.h
Normal file
|
|
@ -0,0 +1,63 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <algorithm>
|
||||
#include <string>
|
||||
#include "util/rc.h"
|
||||
#include "kernel/expr.h"
|
||||
|
||||
namespace lean {
|
||||
/**
|
||||
\brief Environment definitions, theorems, axioms and variable declarations.
|
||||
*/
|
||||
class definition {
|
||||
struct cell;
|
||||
cell * m_ptr;
|
||||
explicit definition(cell * ptr);
|
||||
friend class cell;
|
||||
public:
|
||||
definition(definition const & s);
|
||||
definition(definition && s);
|
||||
~definition();
|
||||
|
||||
friend void swap(definition & a, definition & b) { std::swap(a.m_ptr, b.m_ptr); }
|
||||
|
||||
definition & operator=(definition const & s);
|
||||
definition & operator=(definition && s);
|
||||
|
||||
bool is_definition() const;
|
||||
bool is_axiom() const;
|
||||
bool is_theorem() const;
|
||||
bool is_var_decl() const;
|
||||
|
||||
name get_name() const;
|
||||
param_names const & get_params() const;
|
||||
level_cnstrs const & get_level_cnstrs() const;
|
||||
expr get_type() const;
|
||||
|
||||
expr get_value() const;
|
||||
bool is_opaque() const;
|
||||
unsigned get_weight() 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_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);
|
||||
|
||||
void write(serializer & s) const;
|
||||
};
|
||||
|
||||
inline optional<definition> none_definition() { return optional<definition>(); }
|
||||
inline optional<definition> some_definition(definition const & o) { return optional<definition>(o); }
|
||||
inline optional<definition> some_definition(definition && o) { return optional<definition>(std::forward<definition>(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_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);
|
||||
}
|
||||
|
|
@ -9,6 +9,7 @@ Author: Leonardo de Moura
|
|||
#include <sstream>
|
||||
#include <string>
|
||||
#include <algorithm>
|
||||
#include <limits>
|
||||
#include "util/list_fn.h"
|
||||
#include "util/hash.h"
|
||||
#include "util/buffer.h"
|
||||
|
|
|
|||
|
|
@ -132,12 +132,6 @@ public:
|
|||
virtual format operator()(expr const & e, options const &) {
|
||||
std::ostringstream s; s << e; return format(s.str());
|
||||
}
|
||||
virtual format operator()(object const & /* obj */, options const & /* opts */) {
|
||||
return format(); // TODO(Leo)
|
||||
}
|
||||
virtual format operator()(ro_environment const & /* env */, options const & /* opts */) {
|
||||
return format(); // TODO(Leo)
|
||||
}
|
||||
};
|
||||
formatter mk_simple_formatter() {
|
||||
return mk_formatter(simple_formatter_cell());
|
||||
|
|
|
|||
|
|
@ -7,28 +7,17 @@ Author: Leonardo de Moura
|
|||
#pragma once
|
||||
#include <memory>
|
||||
#include "util/sexpr/options.h"
|
||||
#include "kernel/environment.h"
|
||||
#include "kernel/expr.h"
|
||||
|
||||
namespace lean {
|
||||
/**
|
||||
\brief API for formatting expressions, contexts and environments.
|
||||
\brief API for formatting expressions
|
||||
*/
|
||||
class formatter_cell {
|
||||
public:
|
||||
virtual ~formatter_cell() {}
|
||||
/** \brief Format the given expression. */
|
||||
virtual format operator()(expr const & e, options const & opts) = 0;
|
||||
/** \brief Format the given object */
|
||||
virtual format operator()(object const & obj, options const & opts) = 0;
|
||||
/** \brief Format the given environment */
|
||||
virtual format operator()(ro_environment const & env, options const & opts) = 0;
|
||||
|
||||
/**
|
||||
\brief Return environment object associated with this formatter.
|
||||
Not every formatter has an associated environment object.
|
||||
*/
|
||||
virtual optional<ro_environment> get_environment() const { return optional<ro_environment>(); }
|
||||
};
|
||||
/**
|
||||
\brief Smart-pointer for the actual formatter object (aka \c formatter_cell).
|
||||
|
|
@ -38,9 +27,6 @@ class formatter {
|
|||
formatter(formatter_cell * c):m_cell(c) {}
|
||||
public:
|
||||
format operator()(expr const & e, options const & opts = options()) const { return (*m_cell)(e, opts); }
|
||||
format operator()(object const & obj, options const & opts = options()) const { return (*m_cell)(obj, opts); }
|
||||
format operator()(ro_environment const & env, options const & opts = options()) const { return (*m_cell)(env, opts); }
|
||||
optional<ro_environment> get_environment() { return m_cell->get_environment(); }
|
||||
template<typename FCell> friend formatter mk_formatter(FCell && fcell);
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -1,181 +0,0 @@
|
|||
/*
|
||||
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 <string>
|
||||
#include "kernel/object.h"
|
||||
#include "kernel/environment.h"
|
||||
|
||||
namespace lean {
|
||||
typedef std::unordered_map<std::string, object_cell::reader> object_readers;
|
||||
static std::unique_ptr<object_readers> g_object_readers;
|
||||
object_readers & get_object_readers() {
|
||||
if (!g_object_readers)
|
||||
g_object_readers.reset(new object_readers());
|
||||
return *(g_object_readers.get());
|
||||
}
|
||||
|
||||
void object_cell::register_deserializer(std::string const & k, reader rd) {
|
||||
object_readers & readers = get_object_readers();
|
||||
lean_assert(readers.find(k) == readers.end());
|
||||
readers[k] = rd;
|
||||
}
|
||||
void read_object(environment const & env, io_state const & ios, std::string const & k, deserializer & d) {
|
||||
object_readers & readers = get_object_readers();
|
||||
auto it = readers.find(k);
|
||||
lean_assert(it != readers.end());
|
||||
it->second(env, ios, d);
|
||||
}
|
||||
|
||||
neutral_object_cell::neutral_object_cell():object_cell(object_kind::Neutral) {}
|
||||
|
||||
serializer & operator<<(serializer & s, param_names const & ps) {
|
||||
return write_list<name>(s, ps);
|
||||
}
|
||||
|
||||
param_names read_params(deserializer & d) {
|
||||
return read_list<name>(d);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Parametric kernel objects.
|
||||
*/
|
||||
class parametric_object_cell : public object_cell {
|
||||
name m_name;
|
||||
param_names m_params;
|
||||
level_cnstrs m_cnstrs;
|
||||
expr m_type;
|
||||
public:
|
||||
parametric_object_cell(object_kind k, name const & n, param_names const & params, level_cnstrs const & cs, expr const & t):
|
||||
object_cell(k), m_name(n), m_params(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; }
|
||||
virtual expr get_type() const { return m_type; }
|
||||
virtual param_names const & get_params() const { return m_params; }
|
||||
virtual level_cnstrs const & get_level_cnstrs() const { return m_cnstrs; }
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Base class for Axioms and Variable declarations.
|
||||
*/
|
||||
class postulate_object_cell : public parametric_object_cell {
|
||||
public:
|
||||
postulate_object_cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t):
|
||||
parametric_object_cell(object_kind::Postulate, n, params, cs, t) {}
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Axioms
|
||||
*/
|
||||
class axiom_object_cell : public postulate_object_cell {
|
||||
public:
|
||||
axiom_object_cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t):
|
||||
postulate_object_cell(n, 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_params() << get_level_cnstrs() << get_type(); }
|
||||
};
|
||||
static void read_axiom(environment const & env, io_state const &, deserializer & d) {
|
||||
name n = read_name(d);
|
||||
param_names ps = read_params(d);
|
||||
level_cnstrs cs = read_level_cnstrs(d);
|
||||
expr t = read_expr(d);
|
||||
env->add_axiom(n, ps, cs, t);
|
||||
}
|
||||
static object_cell::register_deserializer_fn axiom_ds("ax", read_axiom);
|
||||
|
||||
|
||||
/**
|
||||
\brief Variable (aka constant) declaration
|
||||
*/
|
||||
class variable_decl_object_cell : public postulate_object_cell {
|
||||
public:
|
||||
variable_decl_object_cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t):
|
||||
postulate_object_cell(n, 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_params() << get_level_cnstrs() << get_type(); }
|
||||
};
|
||||
static void read_variable(environment const & env, io_state const &, deserializer & d) {
|
||||
name n = read_name(d);
|
||||
param_names ps = read_params(d);
|
||||
level_cnstrs cs = read_level_cnstrs(d);
|
||||
expr t = read_expr(d);
|
||||
env->add_var(n, ps, 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 parametric_object_cell {
|
||||
expr m_value;
|
||||
bool m_opaque;
|
||||
unsigned m_weight;
|
||||
public:
|
||||
definition_object_cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight):
|
||||
parametric_object_cell(object_kind::Definition, n, params, cs, t), m_value(v), m_opaque(false), m_weight(weight) {}
|
||||
virtual ~definition_object_cell() {}
|
||||
|
||||
virtual bool is_definition() const { return true; }
|
||||
virtual bool is_opaque() const { return m_opaque; }
|
||||
virtual void set_opaque(bool f) { m_opaque = f; }
|
||||
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_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);
|
||||
param_names ps = read_params(d);
|
||||
level_cnstrs cs = read_level_cnstrs(d);
|
||||
expr t = read_expr(d);
|
||||
expr v = read_expr(d);
|
||||
env->add_definition(n, ps, cs, t, v);
|
||||
}
|
||||
static object_cell::register_deserializer_fn definition_ds("def", read_definition);
|
||||
|
||||
/**
|
||||
\brief Theorems
|
||||
*/
|
||||
class theorem_object_cell : public definition_object_cell {
|
||||
public:
|
||||
theorem_object_cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v):
|
||||
definition_object_cell(n, 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_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);
|
||||
param_names ps = read_params(d);
|
||||
level_cnstrs cs = read_level_cnstrs(d);
|
||||
expr t = read_expr(d);
|
||||
expr v = read_expr(d);
|
||||
env->add_theorem(n, ps, cs, t, v);
|
||||
}
|
||||
static object_cell::register_deserializer_fn theorem_ds("th", read_theorem);
|
||||
|
||||
object mk_definition(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight) {
|
||||
return object(new definition_object_cell(n, ps, cs, t, v, weight));
|
||||
}
|
||||
object mk_theorem(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v) {
|
||||
return object(new theorem_object_cell(n, ps, cs, t, v));
|
||||
}
|
||||
object mk_axiom(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t) {
|
||||
return object(new axiom_object_cell(n, ps, cs, t));
|
||||
}
|
||||
object mk_var_decl(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t) {
|
||||
return object(new variable_decl_object_cell(n, ps, cs, t));
|
||||
}
|
||||
}
|
||||
|
|
@ -1,151 +0,0 @@
|
|||
/*
|
||||
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 <algorithm>
|
||||
#include <string>
|
||||
#include "util/rc.h"
|
||||
#include "kernel/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 io_state;
|
||||
class object;
|
||||
enum class object_kind { Definition, Postulate, Neutral };
|
||||
|
||||
class object_cell {
|
||||
protected:
|
||||
friend class object;
|
||||
void dealloc() { delete this; }
|
||||
MK_LEAN_RC();
|
||||
object_kind m_kind;
|
||||
/** \brief Set the opaque flag */
|
||||
virtual void set_opaque(bool ) { lean_unreachable(); } // LCOV_EXCL_LINE
|
||||
public:
|
||||
object_cell(object_kind k):m_rc(1), m_kind(k) {}
|
||||
virtual ~object_cell() {}
|
||||
|
||||
object_kind kind() const { return m_kind; }
|
||||
|
||||
/**
|
||||
\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 Return true iff object has a name. */
|
||||
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 param_names const & get_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 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() */
|
||||
virtual bool is_opaque() const { lean_unreachable(); } // LCOV_EXCL_LINE
|
||||
/** \brief Return object value. \pre is_definition() */
|
||||
virtual expr get_value() const { lean_unreachable(); } // LCOV_EXCL_LINE
|
||||
|
||||
virtual bool is_axiom() const { return false; }
|
||||
virtual bool is_theorem() const { return false; }
|
||||
virtual bool is_var_decl() const { return false; }
|
||||
|
||||
virtual unsigned get_weight() const { return 0; }
|
||||
|
||||
virtual void write(serializer & ) const = 0;
|
||||
typedef void (*reader)(environment const & env, io_state const & ios, deserializer & d);
|
||||
static void register_deserializer(std::string const & k, reader rd);
|
||||
struct register_deserializer_fn {
|
||||
register_deserializer_fn(std::string const & k, reader rd) { register_deserializer(k, rd); }
|
||||
};
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Neutral objects are mainly used for bookkeeping in
|
||||
frontends built on top of the kernel.
|
||||
The kernel does *not* create neutral objects.
|
||||
*/
|
||||
class neutral_object_cell : public object_cell {
|
||||
public:
|
||||
neutral_object_cell();
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Environment objects: definitions, theorems, axioms, universe
|
||||
variable declarations, etc.
|
||||
*/
|
||||
class object {
|
||||
object_cell * m_ptr;
|
||||
explicit object(object_cell * ptr):m_ptr(ptr) {}
|
||||
friend class environment_cell;
|
||||
void set_opaque(bool f) { m_ptr->set_opaque(f); }
|
||||
public:
|
||||
object(object const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
||||
object(object && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
|
||||
~object() { if (m_ptr) m_ptr->dec_ref(); }
|
||||
|
||||
friend void swap(object & a, object & b) { std::swap(a.m_ptr, b.m_ptr); }
|
||||
|
||||
object & operator=(object const & s) { LEAN_COPY_REF(s); }
|
||||
object & operator=(object && s) { LEAN_MOVE_REF(s); }
|
||||
|
||||
object_kind kind() const { return m_ptr->kind(); }
|
||||
|
||||
friend object mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight);
|
||||
friend object mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v);
|
||||
friend object mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);
|
||||
friend object mk_var_decl(name const & n, param_names const & params, 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(); }
|
||||
param_names const & get_params() const { return m_ptr->get_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(); }
|
||||
expr get_value() const { return m_ptr->get_value(); }
|
||||
unsigned get_weight() const { return m_ptr->get_weight(); }
|
||||
|
||||
bool is_axiom() const { return m_ptr->is_axiom(); }
|
||||
bool is_theorem() const { return m_ptr->is_theorem(); }
|
||||
bool is_var_decl() const { return m_ptr->is_var_decl(); }
|
||||
|
||||
void write(serializer & s) const { m_ptr->write(s); }
|
||||
object_cell const * cell() const { return m_ptr; }
|
||||
};
|
||||
|
||||
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, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight);
|
||||
object mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v);
|
||||
object mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);
|
||||
object mk_var_decl(name const & n, param_names const & params, 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);
|
||||
|
||||
/**
|
||||
\brief Helper function whether we should unfold an definition or not.
|
||||
|
||||
1- We unfold non-opaque definitions.
|
||||
2- We never unfold theorems.
|
||||
*/
|
||||
inline bool should_unfold(object const & obj) { return obj.is_definition() && !obj.is_theorem() && !obj.is_opaque(); }
|
||||
inline bool should_unfold(optional<object> const & obj) { return obj && should_unfold(*obj); }
|
||||
}
|
||||
|
|
@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#if 0
|
||||
#include "util/freset.h"
|
||||
#include "util/flet.h"
|
||||
#include "util/interrupt.h"
|
||||
|
|
@ -66,7 +67,6 @@ class type_checker::imp {
|
|||
throw_kernel_exception(env(), s, [=](formatter const & fmt, options const & o) { return pp_type_expected(fmt, o, e); });
|
||||
}
|
||||
|
||||
#if 0
|
||||
expr check_pi(expr const & e, expr const & s, context const & ctx) {
|
||||
if (is_pi(e))
|
||||
return e;
|
||||
|
|
@ -85,10 +85,8 @@ class type_checker::imp {
|
|||
}
|
||||
throw function_expected_exception(env(), ctx, s);
|
||||
}
|
||||
#endif
|
||||
};
|
||||
|
||||
#if 0
|
||||
static name g_x_name("x");
|
||||
/** \brief Auxiliary functional object used to implement infer_type. */
|
||||
class type_checker::imp {
|
||||
|
|
@ -635,5 +633,5 @@ bool is_proposition(expr const & e, ro_environment const & env, context const &
|
|||
bool is_proposition(expr const & e, ro_environment const & env, context const & ctx) {
|
||||
return is_proposition(e, env, ctx, none_ro_menv());
|
||||
}
|
||||
#endif
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -1,4 +1,5 @@
|
|||
add_library(library deep_copy.cpp expr_lt.cpp io_state_stream.cpp)
|
||||
add_library(library deep_copy.cpp expr_lt.cpp)
|
||||
# io_state_stream.cpp
|
||||
# kernel_bindings.cpp
|
||||
# context_to_lambda.cpp placeholder.cpp
|
||||
# fo_unify.cpp bin_op.cpp equality.cpp
|
||||
|
|
|
|||
|
|
@ -7,9 +7,9 @@ add_test(diff_cnstrs ${CMAKE_CURRENT_BINARY_DIR}/diff_cnstrs)
|
|||
add_executable(expr expr.cpp)
|
||||
target_link_libraries(expr ${EXTRA_LIBS})
|
||||
add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr)
|
||||
add_executable(normalizer normalizer.cpp)
|
||||
target_link_libraries(normalizer ${EXTRA_LIBS})
|
||||
add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer)
|
||||
# add_executable(normalizer normalizer.cpp)
|
||||
# target_link_libraries(normalizer ${EXTRA_LIBS})
|
||||
# add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer)
|
||||
# add_executable(threads threads.cpp)
|
||||
# target_link_libraries(threads ${EXTRA_LIBS})
|
||||
# add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads)
|
||||
|
|
|
|||
Loading…
Reference in a new issue