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

refactor(kernel): rename definition class to declaration

Browse source 
The name was misleading since not every declaration is a definition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-20 10:41:36 -07:00
parent 00b1a84051
commit 8872d4a531
15 changed files with 360 additions and 360 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/CMakeLists.txt
View file

@ -1,6 +1,6 @@
add_library(kernel level.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp
replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp
formatter.cpp definition.cpp replace_visitor.cpp environment.cpp
formatter.cpp declaration.cpp replace_visitor.cpp environment.cpp
justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp
constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp )

8
src/kernel/converter.cpp
View file

@ -165,7 +165,7 @@ struct default_converter : public converter {
D is not a theorem, nor D is in the set m_extra_opaque. To implement this feature, this class has a field
m_module_idx that is not none when this rule should be applied.
*/
bool is_opaque(definition const & d) const {
bool is_opaque(declaration const & d) const {
lean_assert(d.is_definition());
if (d.is_theorem()) return true; // theorems are always opaque
if (m_extra_opaque.contains(d.get_name())) return true; // extra_opaque set overrides opaque flag
@ -208,20 +208,20 @@ struct default_converter : public converter {
}
/** \brief Auxiliary method for \c is_delta */
optional<definition> is_delta_core(expr const & e) {
optional<declaration> is_delta_core(expr const & e) {
if (is_constant(e)) {
if (auto d = m_env.find(const_name(e)))
if (d->is_definition() && !is_opaque(*d))
return d;
}
return none_definition();
return none_declaration();
}
/**
\brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one
to be expanded.
*/
optional<definition> is_delta(expr const & e) { return is_delta_core(get_app_fn(e)); }
optional<declaration> is_delta(expr const & e) { return is_delta_core(get_app_fn(e)); }
/**
\brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with

93
src/kernel/declaration.cpp Normal file
View file

@ -0,0 +1,93 @@
/*
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/declaration.h"
#include "kernel/environment.h"
#include "kernel/for_each_fn.h"
namespace lean {
struct declaration::cell {
MK_LEAN_RC();
name m_name;
level_param_names m_params;
expr m_type;
bool m_theorem;
optional<expr> m_value; // if none, then declaration 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, level_param_names const & params, expr const & t, bool is_axiom):
m_rc(1), m_name(n), m_params(params), 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, level_param_names const & params, expr const & t, bool is_thm, expr const & v,
bool opaque, unsigned w, module_idx mod_idx, bool use_conv_opt):
m_rc(1), m_name(n), m_params(params), 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) {}
};
declaration g_dummy = mk_axiom(name(), level_param_names(), expr());
declaration::declaration():declaration(g_dummy) {}
declaration::declaration(cell * ptr):m_ptr(ptr) {}
declaration::declaration(declaration const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
declaration::declaration(declaration && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
declaration::~declaration() { if (m_ptr) m_ptr->dec_ref(); }
declaration & declaration::operator=(declaration const & s) { LEAN_COPY_REF(s); }
declaration & declaration::operator=(declaration && s) { LEAN_MOVE_REF(s); }
bool declaration::is_definition() const { return static_cast<bool>(m_ptr->m_value); }
bool declaration::is_var_decl() const { return !is_definition(); }
bool declaration::is_axiom() const { return is_var_decl() && m_ptr->m_theorem; }
bool declaration::is_theorem() const { return is_definition() && m_ptr->m_theorem; }
name declaration::get_name() const { return m_ptr->m_name; }
level_param_names const & declaration::get_params() const { return m_ptr->m_params; }
expr declaration::get_type() const { return m_ptr->m_type; }
bool declaration::is_opaque() const { return m_ptr->m_opaque; }
expr declaration::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); }
unsigned declaration::get_weight() const { return m_ptr->m_weight; }
module_idx declaration::get_module_idx() const { return m_ptr->m_module_idx; }
bool declaration::use_conv_opt() const { return m_ptr->m_use_conv_opt; }
declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) {
return declaration(new declaration::cell(n, params, t, false, v, opaque, weight, mod_idx, use_conv_opt));
}
declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque, module_idx mod_idx, bool use_conv_opt) {
unsigned w = 0;
for_each(v, [&](expr const & e, unsigned) {
if (is_constant(e)) {
auto d = env.find(const_name(e));
if (d && d->get_weight() > w)
w = d->get_weight();
}
return true;
});
return mk_definition(n, params, t, v, opaque, w+1, mod_idx, use_conv_opt);
}
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
return declaration(new declaration::cell(n, params, t, true, v, true, 0, 0, false));
}
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
return declaration(new declaration::cell(n, params, t, true));
}
declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t) {
return declaration(new declaration::cell(n, params, t, false));
}
}

90
src/kernel/declaration.h Normal file
View file

@ -0,0 +1,90 @@
/*
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 Module index. The kernel provides only basic support
for implementing a module system outside of the kernel.
We need at least the notion of module index in the kernel, because
it affects the convertability procedure.
Given an opaque definition (non-theorem) d in module m1, then d is considered
to be transparent for any other opaque definition in module m1.
*/
typedef unsigned module_idx;
/**
\brief Environment definitions, theorems, axioms and variable declarations.
*/
class declaration {
struct cell;
cell * m_ptr;
explicit declaration(cell * ptr);
friend struct cell;
public:
/**
\brief The default constructor creates a reference to a "dummy"
declaration. The actual "dummy" declaration is not relevant, and
no procedure should rely on the kind of declaration used.
We have a default constructor because some collections only work
with types that have a default constructor.
*/
declaration();
declaration(declaration const & s);
declaration(declaration && s);
~declaration();
friend void swap(declaration & a, declaration & b) { std::swap(a.m_ptr, b.m_ptr); }
declaration & operator=(declaration const & s);
declaration & operator=(declaration && s);
friend bool is_eqp(declaration const & d1, declaration const & d2) { return d1.m_ptr == d2.m_ptr; }
bool is_definition() const;
bool is_axiom() const;
bool is_theorem() const;
bool is_var_decl() const;
name get_name() const;
level_param_names const & get_params() const;
expr get_type() const;
expr get_value() const;
bool is_opaque() const;
unsigned get_weight() const;
module_idx get_module_idx() const;
bool use_conv_opt() const;
friend declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt);
friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, bool opaque,
unsigned weight, module_idx mod_idx, bool use_conv_opt);
friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
friend declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t);
};
inline optional<declaration> none_declaration() { return optional<declaration>(); }
inline optional<declaration> some_declaration(declaration const & o) { return optional<declaration>(o); }
inline optional<declaration> some_declaration(declaration && o) { return optional<declaration>(std::forward<declaration>(o)); }
declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true);
declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true);
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t);
}

93
src/kernel/definition.cpp
View file

@ -1,93 +0,0 @@
/*
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"
#include "kernel/environment.h"
#include "kernel/for_each_fn.h"
namespace lean {
struct definition::cell {
MK_LEAN_RC();
name m_name;
level_param_names m_params;
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, level_param_names const & params, expr const & t, bool is_axiom):
m_rc(1), m_name(n), m_params(params), 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, level_param_names const & params, expr const & t, bool is_thm, expr const & v,
bool opaque, unsigned w, module_idx mod_idx, bool use_conv_opt):
m_rc(1), m_name(n), m_params(params), 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) {}
};
definition g_dummy = mk_axiom(name(), level_param_names(), expr());
definition::definition():definition(g_dummy) {}
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; }
level_param_names const & definition::get_params() const { return m_ptr->m_params; }
expr definition::get_type() const { return m_ptr->m_type; }
bool definition::is_opaque() const { return m_ptr->m_opaque; }
expr definition::get_value() const { lean_assert(is_definition()); return *(m_ptr->m_value); }
unsigned definition::get_weight() const { return m_ptr->m_weight; }
module_idx definition::get_module_idx() const { return m_ptr->m_module_idx; }
bool definition::use_conv_opt() const { return m_ptr->m_use_conv_opt; }
definition mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) {
return definition(new definition::cell(n, params, t, false, v, opaque, weight, mod_idx, use_conv_opt));
}
definition mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque, module_idx mod_idx, bool use_conv_opt) {
unsigned w = 0;
for_each(v, [&](expr const & e, unsigned) {
if (is_constant(e)) {
auto d = env.find(const_name(e));
if (d && d->get_weight() > w)
w = d->get_weight();
}
return true;
});
return mk_definition(n, params, t, v, opaque, w+1, mod_idx, use_conv_opt);
}
definition mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
return definition(new definition::cell(n, params, t, true, v, true, 0, 0, false));
}
definition mk_axiom(name const & n, level_param_names const & params, expr const & t) {
return definition(new definition::cell(n, params, t, true));
}
definition mk_var_decl(name const & n, level_param_names const & params, expr const & t) {
return definition(new definition::cell(n, params, t, false));
}
}

90
src/kernel/definition.h
View file

@ -1,90 +0,0 @@
/*
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 Module index. The kernel provides only basic support
for implementing a module system outside of the kernel.
We need at least the notion of module index in the kernel, because
it affects the convertability procedure.
Given an opaque definition (non-theorem) d in module m1, then d is considered
to be transparent for any other opaque definition in module m1.
*/
typedef unsigned module_idx;
/**
\brief Environment definitions, theorems, axioms and variable declarations.
*/
class definition {
struct cell;
cell * m_ptr;
explicit definition(cell * ptr);
friend struct cell;
public:
/**
\brief The default constructor creates a reference to a "dummy"
definition. The actual "dummy" definition is not relevant, and
no procedure should rely on the kind of definition used.
We have a default constructor because some collections only work
with types that have a default constructor.
*/
definition();
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);
friend bool is_eqp(definition const & d1, definition const & d2) { return d1.m_ptr == d2.m_ptr; }
bool is_definition() const;
bool is_axiom() const;
bool is_theorem() const;
bool is_var_decl() const;
name get_name() const;
level_param_names const & get_params() const;
expr get_type() const;
expr get_value() const;
bool is_opaque() const;
unsigned get_weight() const;
module_idx get_module_idx() const;
bool use_conv_opt() const;
friend definition mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t,
expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt);
friend definition mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, bool opaque,
unsigned weight, module_idx mod_idx, bool use_conv_opt);
friend definition mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
friend definition mk_axiom(name const & n, level_param_names const & params, expr const & t);
friend definition mk_var_decl(name const & n, level_param_names const & params, expr const & t);
};
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, level_param_names const & params, expr const & t, expr const & v,
bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true);
definition mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true);
definition mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
definition mk_axiom(name const & n, level_param_names const & params, expr const & t);
definition mk_var_decl(name const & n, level_param_names const & params, expr const & t);
}

40
src/kernel/environment.cpp
View file

@ -44,8 +44,8 @@ bool environment_id::is_descendant(environment_id const & id) const {
return false;
}
environment::environment(header const & h, environment_id const & ancestor, definitions const & d, name_set const & g, extensions const & exts):
m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_definitions(d), m_global_levels(g), m_extensions(exts) {}
environment::environment(header const & h, environment_id const & ancestor, declarations const & d, name_set const & g, extensions const & exts):
m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_declarations(d), m_global_levels(g), m_extensions(exts) {}
environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list<name> const & cls_proof_irrel):
environment(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel, std::unique_ptr<normalizer_extension>(new noop_normalizer_extension()))
@ -59,13 +59,13 @@ environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bo
environment::~environment() {}
optional<definition> environment::find(name const & n) const {
definition const * r = m_definitions.find(n);
return r ? some_definition(*r) : none_definition();
optional<declaration> environment::find(name const & n) const {
declaration const * r = m_declarations.find(n);
return r ? some_declaration(*r) : none_declaration();
}
definition environment::get(name const & n) const {
definition const * r = m_definitions.find(n);
declaration environment::get(name const & n) const {
declaration const * r = m_declarations.find(n);
if (!r)
throw_unknown_declaration(*this, n);
return *r;
@ -75,44 +75,44 @@ definition environment::get(name const & n) const {
throw_kernel_exception(env, "invalid declaration, it was checked/certified in an incompatible environment");
}
environment environment::add(certified_definition const & d) const {
environment environment::add(certified_declaration const & d) const {
if (!m_id.is_descendant(d.get_id()))
throw_incompatible_environment(*this);
name const & n = d.get_definition().get_name();
name const & n = d.get_declaration().get_name();
if (find(n))
throw_already_declared(*this, n);
return environment(m_header, m_id, insert(m_definitions, n, d.get_definition()), m_global_levels, m_extensions);
return environment(m_header, m_id, insert(m_declarations, n, d.get_declaration()), m_global_levels, m_extensions);
}
environment environment::add_global_level(name const & n) const {
if (m_global_levels.contains(n))
throw_kernel_exception(*this,
"invalid global universe level declaration, environment already contains a universe level with the given name");
return environment(m_header, m_id, m_definitions, insert(m_global_levels, n), m_extensions);
return environment(m_header, m_id, m_declarations, insert(m_global_levels, n), m_extensions);
}
bool environment::is_global_level(name const & n) const {
return m_global_levels.contains(n);
}
environment environment::replace(certified_definition const & t) const {
environment environment::replace(certified_declaration const & t) const {
if (!m_id.is_descendant(t.get_id()))
throw_incompatible_environment(*this);
name const & n = t.get_definition().get_name();
name const & n = t.get_declaration().get_name();
auto ax = find(n);
if (!ax)
throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the environment does not have an axiom with the given name");
if (!ax->is_axiom())
throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the current declaration in the environment is not an axiom");
if (!t.get_definition().is_theorem())
if (!t.get_declaration().is_theorem())
throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the new declaration is not a theorem");
if (ax->get_type() != t.get_definition().get_type())
if (ax->get_type() != t.get_declaration().get_type())
throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the 'replace' operation can only be used when the axiom and theorem have the same type");
return environment(m_header, m_id, insert(m_definitions, n, t.get_definition()), m_global_levels, m_extensions);
return environment(m_header, m_id, insert(m_declarations, n, t.get_declaration()), m_global_levels, m_extensions);
}
environment environment::forget() const {
return environment(m_header, environment_id(), m_definitions, m_global_levels, m_extensions);
return environment(m_header, environment_id(), m_declarations, m_global_levels, m_extensions);
}
class extension_manager {
@ -165,10 +165,10 @@ environment environment::update(unsigned id, std::shared_ptr<environment_extensi
if (id >= new_exts->size())
new_exts->resize(id+1);
(*new_exts)[id] = ext;
return environment(m_header, m_id, m_definitions, m_global_levels, new_exts);
return environment(m_header, m_id, m_declarations, m_global_levels, new_exts);
}
void environment::for_each(std::function<void(definition const & d)> const & f) const {
m_definitions.for_each([&](name const &, definition const & d) { return f(d); });
void environment::for_each(std::function<void(declaration const & d)> const & f) const {
m_declarations.for_each([&](name const &, declaration const & d) { return f(d); });
}
}

52
src/kernel/environment.h
View file

@ -15,12 +15,12 @@ Author: Leonardo de Moura
#include "util/name_set.h"
#include "kernel/expr.h"
#include "kernel/constraint.h"
#include "kernel/definition.h"
#include "kernel/declaration.h"
namespace lean {
class type_checker;
class environment;
class certified_definition;
class certified_declaration;
/**
\brief The Lean kernel can be instantiated with different normalization extensions.
@ -98,16 +98,16 @@ public:
*/
class environment {
typedef std::shared_ptr<environment_header const> header;
typedef rb_map<name, definition, name_quick_cmp> definitions;
typedef rb_map<name, declaration, name_quick_cmp> declarations;
typedef std::shared_ptr<environment_extensions const> extensions;
header m_header;
environment_id m_id;
definitions m_definitions;
declarations m_declarations;
name_set m_global_levels;
extensions m_extensions;
environment(header const & h, environment_id const & id, definitions const & d, name_set const & global_levels, extensions const & ext);
environment(header const & h, environment_id const & id, declarations const & d, name_set const & global_levels, extensions const & ext);
public:
environment(unsigned trust_lvl = 0, bool prop_proof_irrel = true, bool eta = true, bool impredicative = true,
@ -140,11 +140,11 @@ public:
/** \brief Return reference to the normalizer extension associatied with this environment. */
normalizer_extension const & norm_ext() const { return m_header->norm_ext(); }
/** \brief Return definition with name \c n (if it is defined in this environment). */
optional<definition> find(name const & n) const;
/** \brief Return declaration with name \c n (if it is defined in this environment). */
optional<declaration> find(name const & n) const;
/** \brief Return definition with name \c n. Throws and exception if definition does not exist in this environment. */
definition get(name const & n) const;
/** \brief Return declaration with name \c n. Throws and exception if declaration does not exist in this environment. */
declaration get(name const & n) const;
/**
\brief Add a new global universe level with name \c n
@ -156,20 +156,20 @@ public:
bool is_global_level(name const & n) const;
/**
\brief Extends the current environment with the given (certified) definition
\brief Extends the current environment with the given (certified) declaration
This method throws an exception if:
- The definition was certified in an environment which is not an ancestor of this one.
- The environment already contains a definition with the given name.
- The declaration was certified in an environment which is not an ancestor of this one.
- The environment already contains a declaration with the given name.
*/
environment add(certified_definition const & d) const;
environment add(certified_declaration const & d) const;
/**
\brief Replace the axiom with name <tt>t.get_definition().get_name()</tt> with the theorem t.get_definition().
\brief Replace the axiom with name <tt>t.get_declaration().get_name()</tt> with the theorem t.get_declaration().
This method throws an exception if:
- The theorem was certified in an environment which is not an ancestor of this one.
- The environment does not contain an axiom named <tt>t.get_definition().get_name()</tt>
- The environment does not contain an axiom named <tt>t.get_declaration().get_name()</tt>
*/
environment replace(certified_definition const & t) const;
environment replace(certified_declaration const & t) const;
/**
\brief Register an environment extension. Every environment
@ -197,24 +197,24 @@ public:
*/
environment forget() const;
/** \brief Apply the function \c f to each definition */
void for_each(std::function<void(definition const & d)> const & f) const;
/** \brief Apply the function \c f to each declaration */
void for_each(std::function<void(declaration const & d)> const & f) const;
};
class name_generator;
/**
\brief A certified definition is one that has been type checked.
Only the type_checker class can create certified definitions.
\brief A certified declaration is one that has been type checked.
Only the type_checker class can create certified declarations.
*/
class certified_definition {
friend certified_definition check(environment const & env, definition const & d, name_generator const & g, name_set const & extra_opaque, bool memoize);
class certified_declaration {
friend certified_declaration check(environment const & env, declaration const & d, name_generator const & g, name_set const & extra_opaque, bool memoize);
environment_id m_id;
definition m_definition;
certified_definition(environment_id const & id, definition const & d):m_id(id), m_definition(d) {}
declaration m_declaration;
certified_declaration(environment_id const & id, declaration const & d):m_id(id), m_declaration(d) {}
public:
/** \brief Return the id of the environment that was used to type check this definition. */
/** \brief Return the id of the environment that was used to type check this declaration. */
environment_id const & get_id() const { return m_id; }
definition const & get_definition() const { return m_definition; }
declaration const & get_declaration() const { return m_declaration; }
};
}

8
src/kernel/type_checker.cpp
View file

@ -307,7 +307,7 @@ struct type_checker::imp {
r = mk_sort(mk_succ(sort_level(e)));
break;
case expr_kind::Constant: {
definition d = m_env.get(const_name(e));
declaration d = m_env.get(const_name(e));
auto const & ps = d.get_params();
auto const & ls = const_levels(e);
if (length(ps) != length(ls))
@ -445,7 +445,7 @@ static void check_name(environment const & env, name const & n) {
throw_already_declared(env, n);
}
certified_definition check(environment const & env, definition const & d, name_generator const & g, name_set const & extra_opaque, bool memoize) {
certified_declaration check(environment const & env, declaration const & d, name_generator const & g, name_set const & extra_opaque, bool memoize) {
check_no_mlocal(env, d.get_type());
if (d.is_definition())
check_no_mlocal(env, d.get_value());
@ -466,10 +466,10 @@ certified_definition check(environment const & env, definition const & d, name_g
});
}
}
return certified_definition(env.get_id(), d);
return certified_declaration(env.get_id(), d);
}
certified_definition check(environment const & env, definition const & d, name_set const & extra_opaque, bool memoize) {
certified_declaration check(environment const & env, declaration const & d, name_set const & extra_opaque, bool memoize) {
return check(env, d, name_generator(g_tmp_prefix), extra_opaque, memoize);
}
}

10
src/kernel/type_checker.h
View file

@ -101,10 +101,10 @@ public:
};
/**
\brief Type check the given definition, and return a certified definition if it is type correct.
Throw an exception if the definition is type incorrect.
\brief Type check the given declaration, and return a certified declaration if it is type correct.
Throw an exception if the declaration is type incorrect.
*/
certified_definition check(environment const & env, definition const & d,
name_generator const & g, name_set const & extra_opaque = name_set(), bool memoize = true);
certified_definition check(environment const & env, definition const & d, name_set const & extra_opaque = name_set(), bool memoize = true);
certified_declaration check(environment const & env, declaration const & d,
name_generator const & g, name_set const & extra_opaque = name_set(), bool memoize = true);
certified_declaration check(environment const & env, declaration const & d, name_set const & extra_opaque = name_set(), bool memoize = true);
}

176
src/library/kernel_bindings.cpp
View file

@ -830,25 +830,25 @@ static void open_macro_definition(lua_State * L) {
SET_GLOBAL_FUN(macro_definition_pred, "is_macro_definition");
}
// definition
DECL_UDATA(definition)
int push_optional_definition(lua_State * L, optional<definition> const & e) { return e ? push_definition(L, *e) : push_nil(L); }
#define DEFINITION_PRED(P) static int definition_ ## P(lua_State * L) { return push_boolean(L, to_definition(L, 1).P()); }
DEFINITION_PRED(is_definition)
DEFINITION_PRED(is_theorem)
DEFINITION_PRED(is_axiom)
DEFINITION_PRED(is_var_decl)
DEFINITION_PRED(is_opaque)
DEFINITION_PRED(use_conv_opt)
static int definition_get_name(lua_State * L) { return push_name(L, to_definition(L, 1).get_name()); }
static int definition_get_params(lua_State * L) { return push_list_name(L, to_definition(L, 1).get_params()); }
static int definition_get_type(lua_State * L) { return push_expr(L, to_definition(L, 1).get_type()); }
static int definition_get_value(lua_State * L) {
if (to_definition(L, 1).is_definition())
return push_expr(L, to_definition(L, 1).get_value());
throw exception("arg #1 must be a definition");
// declaration
DECL_UDATA(declaration)
int push_optional_declaration(lua_State * L, optional<declaration> const & e) { return e ? push_declaration(L, *e) : push_nil(L); }
#define DECLARATION_PRED(P) static int declaration_ ## P(lua_State * L) { return push_boolean(L, to_declaration(L, 1).P()); }
DECLARATION_PRED(is_definition)
DECLARATION_PRED(is_theorem)
DECLARATION_PRED(is_axiom)
DECLARATION_PRED(is_var_decl)
DECLARATION_PRED(is_opaque)
DECLARATION_PRED(use_conv_opt)
static int declaration_get_name(lua_State * L) { return push_name(L, to_declaration(L, 1).get_name()); }
static int declaration_get_params(lua_State * L) { return push_list_name(L, to_declaration(L, 1).get_params()); }
static int declaration_get_type(lua_State * L) { return push_expr(L, to_declaration(L, 1).get_type()); }
static int declaration_get_value(lua_State * L) {
if (to_declaration(L, 1).is_definition())
return push_expr(L, to_declaration(L, 1).get_value());
throw exception("arg #1 must be a declaration");
}
static int definition_get_weight(lua_State * L) { return push_integer(L, to_definition(L, 1).get_weight()); }
static int declaration_get_weight(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_weight()); }
static list<name> to_level_param_names(lua_State * L, int _idx) {
return table_to_list<name>(L, _idx, [](lua_State * L, int idx) -> name {
if (is_level(L, idx)) {
@ -864,27 +864,27 @@ static list<name> to_level_param_names(lua_State * L, int _idx) {
}
});
}
static int definition_get_module_idx(lua_State * L) { return push_integer(L, to_definition(L, 1).get_module_idx()); }
static int declaration_get_module_idx(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_module_idx()); }
static int mk_var_decl(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 2)
return push_definition(L, mk_var_decl(to_name_ext(L, 1), level_param_names(), to_expr(L, 2)));
return push_declaration(L, mk_var_decl(to_name_ext(L, 1), level_param_names(), to_expr(L, 2)));
else
return push_definition(L, mk_var_decl(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
return push_declaration(L, mk_var_decl(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
}
static int mk_axiom(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 2)
return push_definition(L, mk_axiom(to_name_ext(L, 1), level_param_names(), to_expr(L, 2)));
return push_declaration(L, mk_axiom(to_name_ext(L, 1), level_param_names(), to_expr(L, 2)));
else
return push_definition(L, mk_axiom(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
return push_declaration(L, mk_axiom(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3)));
}
static int mk_theorem(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 3)
return push_definition(L, mk_theorem(to_name_ext(L, 1), level_param_names(), to_expr(L, 2), to_expr(L, 3)));
return push_declaration(L, mk_theorem(to_name_ext(L, 1), level_param_names(), to_expr(L, 2), to_expr(L, 3)));
else
return push_definition(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4)));
return push_declaration(L, mk_theorem(to_name_ext(L, 1), to_level_param_names(L, 2), to_expr(L, 3), to_expr(L, 4)));
}
static void get_definition_args(lua_State * L, int idx, bool & opaque, unsigned & weight, module_idx & mod_idx, bool & use_conv_opt) {
opaque = get_bool_named_param(L, idx, "opaque", opaque);
@ -896,60 +896,60 @@ static int mk_definition(lua_State * L) {
int nargs = lua_gettop(L);
bool opaque = true; unsigned weight = 0; module_idx mod_idx = 0; bool use_conv_opt = true;
if (nargs < 3) {
throw exception("mk_definition must have at least 3 arguments");
throw exception("mk_declaration must have at least 3 arguments");
} else if (is_environment(L, 1)) {
if (nargs < 4) {
throw exception("mk_definition must have at least 4 arguments, when the first argument is an environment");
throw exception("mk_declaration must have at least 4 arguments, when the first argument is an environment");
} else if (is_expr(L, 3)) {
get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), level_param_names(),
return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), level_param_names(),
to_expr(L, 3), to_expr(L, 4), opaque, mod_idx, use_conv_opt));
} else {
get_definition_args(L, 6, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_level_param_names(L, 3),
return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_level_param_names(L, 3),
to_expr(L, 4), to_expr(L, 5), opaque, mod_idx, use_conv_opt));
}
} else {
if (is_expr(L, 2)) {
get_definition_args(L, 4, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_name_ext(L, 1), level_param_names(), to_expr(L, 2),
return push_declaration(L, mk_definition(to_name_ext(L, 1), level_param_names(), to_expr(L, 2),
to_expr(L, 3), opaque, weight, mod_idx, use_conv_opt));
} else {
get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_name_ext(L, 1), to_level_param_names(L, 2),
return push_declaration(L, mk_definition(to_name_ext(L, 1), to_level_param_names(L, 2),
to_expr(L, 3), to_expr(L, 4), opaque, weight, mod_idx, use_conv_opt));
}
}
}
static const struct luaL_Reg definition_m[] = {
{"__gc", definition_gc}, // never throws
{"is_definition", safe_function<definition_is_definition>},
{"is_theorem", safe_function<definition_is_theorem>},
{"is_axiom", safe_function<definition_is_axiom>},
{"is_var_decl", safe_function<definition_is_var_decl>},
{"opaque", safe_function<definition_is_opaque>},
{"use_conv_opt", safe_function<definition_use_conv_opt>},
{"name", safe_function<definition_get_name>},
{"univ_params", safe_function<definition_get_params>},
{"type", safe_function<definition_get_type>},
{"value", safe_function<definition_get_value>},
{"weight", safe_function<definition_get_weight>},
{"module_idx", safe_function<definition_get_module_idx>},
static const struct luaL_Reg declaration_m[] = {
{"__gc", declaration_gc}, // never throws
{"is_definition", safe_function<declaration_is_definition>},
{"is_theorem", safe_function<declaration_is_theorem>},
{"is_axiom", safe_function<declaration_is_axiom>},
{"is_var_decl", safe_function<declaration_is_var_decl>},
{"opaque", safe_function<declaration_is_opaque>},
{"use_conv_opt", safe_function<declaration_use_conv_opt>},
{"name", safe_function<declaration_get_name>},
{"univ_params", safe_function<declaration_get_params>},
{"type", safe_function<declaration_get_type>},
{"value", safe_function<declaration_get_value>},
{"weight", safe_function<declaration_get_weight>},
{"module_idx", safe_function<declaration_get_module_idx>},
{0, 0}
};
static void open_definition(lua_State * L) {
luaL_newmetatable(L, definition_mt);
static void open_declaration(lua_State * L) {
luaL_newmetatable(L, declaration_mt);
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, definition_m, 0);
setfuncs(L, declaration_m, 0);
SET_GLOBAL_FUN(definition_pred, "is_definition");
SET_GLOBAL_FUN(mk_var_decl, "mk_var_decl");
SET_GLOBAL_FUN(mk_axiom, "mk_axiom");
SET_GLOBAL_FUN(mk_theorem, "mk_theorem");
SET_GLOBAL_FUN(mk_definition, "mk_definition");
SET_GLOBAL_FUN(declaration_pred, "is_declaration");
SET_GLOBAL_FUN(mk_var_decl, "mk_var_decl");
SET_GLOBAL_FUN(mk_axiom, "mk_axiom");
SET_GLOBAL_FUN(mk_theorem, "mk_theorem");
SET_GLOBAL_FUN(mk_definition, "mk_definition");
}
// Formatter
@ -1059,33 +1059,33 @@ static void open_environment_id(lua_State * L) {
SET_GLOBAL_FUN(environment_id_pred, "is_environment_id");
}
// certified_definition
DECL_UDATA(certified_definition)
static int certified_definition_get_definition(lua_State * L) { return push_definition(L, to_certified_definition(L, 1).get_definition()); }
static int certified_definition_get_id(lua_State * L) { return push_environment_id(L, to_certified_definition(L, 1). get_id()); }
// certified_declaration
DECL_UDATA(certified_declaration)
static int certified_declaration_get_declaration(lua_State * L) { return push_declaration(L, to_certified_declaration(L, 1).get_declaration()); }
static int certified_declaration_get_id(lua_State * L) { return push_environment_id(L, to_certified_declaration(L, 1). get_id()); }
static const struct luaL_Reg certified_definition_m[] = {
{"__gc", certified_definition_gc}, // never throws
{"definition", safe_function<certified_definition_get_definition>},
{"environment_id", safe_function<certified_definition_get_id>},
static const struct luaL_Reg certified_declaration_m[] = {
{"__gc", certified_declaration_gc}, // never throws
{"declaration", safe_function<certified_declaration_get_declaration>},
{"environment_id", safe_function<certified_declaration_get_id>},
{0, 0}
};
static void certified_definition_migrate(lua_State * src, int i, lua_State * tgt) {
push_certified_definition(tgt, to_certified_definition(src, i));
static void certified_declaration_migrate(lua_State * src, int i, lua_State * tgt) {
push_certified_declaration(tgt, to_certified_declaration(src, i));
}
static void open_certified_definition(lua_State * L) {
luaL_newmetatable(L, certified_definition_mt);
set_migrate_fn_field(L, -1, certified_definition_migrate);
static void open_certified_declaration(lua_State * L) {
luaL_newmetatable(L, certified_declaration_mt);
set_migrate_fn_field(L, -1, certified_declaration_migrate);
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, certified_definition_m, 0);
setfuncs(L, certified_declaration_m, 0);
SET_GLOBAL_FUN(certified_definition_pred, "is_certified_definition");
SET_GLOBAL_FUN(certified_declaration_pred, "is_certified_declaration");
}
static bool operator!=(certified_definition const &, certified_definition const &) { return true; }
DEFINE_LUA_LIST(certified_definition, push_certified_definition, to_certified_definition)
static bool operator!=(certified_declaration const &, certified_declaration const &) { return true; }
DEFINE_LUA_LIST(certified_declaration, push_certified_declaration, to_certified_declaration)
// Environment
DECL_UDATA(environment)
@ -1097,10 +1097,10 @@ static int environment_eta(lua_State * L) { return push_boolean(L, to_environmen
static int environment_impredicative(lua_State * L) { return push_boolean(L, to_environment(L, 1).impredicative()); }
static int environment_add_global_level(lua_State * L) { return push_environment(L, to_environment(L, 1).add_global_level(to_name_ext(L, 2))); }
static int environment_is_global_level(lua_State * L) { return push_boolean(L, to_environment(L, 1).is_global_level(to_name_ext(L, 2))); }
static int environment_find(lua_State * L) { return push_optional_definition(L, to_environment(L, 1).find(to_name_ext(L, 2))); }
static int environment_get(lua_State * L) { return push_definition(L, to_environment(L, 1).get(to_name_ext(L, 2))); }
static int environment_add(lua_State * L) { return push_environment(L, to_environment(L, 1).add(to_certified_definition(L, 2))); }
static int environment_replace(lua_State * L) { return push_environment(L, to_environment(L, 1).replace(to_certified_definition(L, 2))); }
static int environment_find(lua_State * L) { return push_optional_declaration(L, to_environment(L, 1).find(to_name_ext(L, 2))); }
static int environment_get(lua_State * L) { return push_declaration(L, to_environment(L, 1).get(to_name_ext(L, 2))); }
static int environment_add(lua_State * L) { return push_environment(L, to_environment(L, 1).add(to_certified_declaration(L, 2))); }
static int environment_replace(lua_State * L) { return push_environment(L, to_environment(L, 1).replace(to_certified_declaration(L, 2))); }
static int mk_empty_environment(lua_State * L) {
unsigned trust_lvl = get_uint_named_param(L, 1, "trust_lvl", 0);
trust_lvl = get_uint_named_param(L, 1, "trust_level", trust_lvl);
@ -1125,9 +1125,9 @@ static int environment_type_check(lua_State * L) { return push_expr(L, type_chec
static int environment_for_each(lua_State * L) {
environment const & env = to_environment(L, 1);
luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
env.for_each([&](definition const & d) {
env.for_each([&](declaration const & d) {
lua_pushvalue(L, 2); // push user-fun
push_definition(L, d);
push_declaration(L, d);
pcall(L, 1, 0, 0);
});
return 0;
@ -1758,27 +1758,27 @@ static const struct luaL_Reg type_checker_ref_m[] = {
static int type_check(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 2)
return push_certified_definition(L, check(to_environment(L, 1), to_definition(L, 2)));
return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2)));
else if (nargs == 3)
return push_certified_definition(L, check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3)));
return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3)));
else if (nargs == 4)
return push_certified_definition(L, check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3), to_name_set(L, 4)));
return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4)));
else
return push_certified_definition(L, check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3), to_name_set(L, 4),
return push_certified_declaration(L, check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4),
lua_toboolean(L, 5)));
}
static int add_declaration(lua_State * L) {
int nargs = lua_gettop(L);
optional<certified_definition> d;
optional<certified_declaration> d;
if (nargs == 2)
d = check(to_environment(L, 1), to_definition(L, 2));
d = check(to_environment(L, 1), to_declaration(L, 2));
else if (nargs == 3)
d = check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3));
d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3));
else if (nargs == 4)
d = check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3), to_name_set(L, 4));
d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4));
else
d = check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3), to_name_set(L, 4), lua_toboolean(L, 5));
d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), to_name_set(L, 4), lua_toboolean(L, 5));
return push_environment(L, to_environment(L, 1).add(*d));
}
@ -1876,11 +1876,11 @@ void open_kernel_module(lua_State * L) {
open_expr(L);
open_list_expr(L);
open_macro_definition(L);
open_definition(L);
open_declaration(L);
open_formatter(L);
open_environment_id(L);
open_certified_definition(L);
open_list_certified_definition(L);
open_certified_declaration(L);
open_list_certified_declaration(L);
open_environment(L);
open_io_state(L);
open_justification(L);

10
src/library/kernel_serializer.cpp
View file

@ -7,11 +7,11 @@ Author: Leonardo de Moura
#include <string>
#include "util/object_serializer.h"
#include "kernel/expr.h"
#include "kernel/definition.h"
#include "kernel/declaration.h"
#include "library/max_sharing.h"
#include "library/kernel_serializer.h"
// Procedures for serializing and deserializing kernel objects (levels, exprs, definitions)
// Procedures for serializing and deserializing kernel objects (levels, exprs, declarations)
namespace lean {
// Universe level serialization
class level_serializer : public object_serializer<level, level::ptr_hash, level::ptr_eq> {
@ -254,10 +254,10 @@ expr read_expr(deserializer & d) {
return d.get_extension<expr_deserializer>(g_expr_sd.m_d_extid).read();
}
// Definition serialization
// Declaration serialization
static serializer & operator<<(serializer & s, level_param_names const & ps) { return write_list<name>(s, ps); }
static level_param_names read_level_params(deserializer & d) { return read_list<name>(d); }
serializer & operator<<(serializer & s, definition const & d) {
serializer & operator<<(serializer & s, declaration const & d) {
char k = 0;
if (d.is_definition()) {
k |= 1;
@ -277,7 +277,7 @@ serializer & operator<<(serializer & s, definition const & d) {
return s;
}
definition read_definition(deserializer & d, unsigned module_idx) {
declaration read_declaration(deserializer & d, unsigned module_idx) {
char k = d.read_char();
bool has_value = (k & 1) != 0;
bool is_theorem = (k & 8) != 0;

6
src/library/kernel_serializer.h
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include <string>
#include "util/serializer.h"
#include "kernel/definition.h"
#include "kernel/declaration.h"
namespace lean {
serializer & operator<<(serializer & s, level const & l);
@ -21,8 +21,8 @@ serializer & operator<<(serializer & s, expr const & e);
expr read_expr(deserializer & d);
inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); return d; }
serializer & operator<<(serializer & s, definition const & d);
definition read_definition(deserializer & d, unsigned module_idx);
serializer & operator<<(serializer & s, declaration const & d);
declaration read_declaration(deserializer & d, unsigned module_idx);
void register_macro_deserializer(std::string const & k, macro_definition_cell::reader rd);
struct register_macro_deserializer_fn {

38
src/tests/kernel/environment.cpp
View file

@ -13,52 +13,52 @@ Author: Leonardo de Moura
#include "kernel/kernel_exception.h"
using namespace lean;
static environment add_def(environment const & env, definition const & d) {
static environment add_decl(environment const & env, declaration const & d) {
auto cd = check(env, d, name_generator("test"));
return env.add(cd);
}
static void tst1() {
environment env1;
auto env2 = add_def(env1, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool()));
auto env2 = add_decl(env1, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool()));
lean_assert(!env1.find("Bool"));
lean_assert(env2.find("Bool"));
lean_assert(env2.find("Bool")->get_value() == mk_Bool());
try {
auto env3 = add_def(env2, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool()));
auto env3 = add_decl(env2, mk_definition("Bool", level_param_names(), mk_Type(), mk_Bool()));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
try {
auto env4 = add_def(env2, mk_definition("BuggyBool", level_param_names(), mk_Bool(), mk_Bool()));
auto env4 = add_decl(env2, mk_definition("BuggyBool", level_param_names(), mk_Bool(), mk_Bool()));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
try {
auto env5 = add_def(env2, mk_definition("Type1", level_param_names(), mk_metavar("T", mk_sort(mk_meta_univ("l"))), mk_Type()));
auto env5 = add_decl(env2, mk_definition("Type1", level_param_names(), mk_metavar("T", mk_sort(mk_meta_univ("l"))), mk_Type()));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
try {
auto env6 = add_def(env2, mk_definition("Type1", level_param_names(), mk_Type(), mk_metavar("T", mk_sort(mk_meta_univ("l")))));
auto env6 = add_decl(env2, mk_definition("Type1", level_param_names(), mk_Type(), mk_metavar("T", mk_sort(mk_meta_univ("l")))));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
try {
auto env7 = add_def(env2, mk_definition("foo", level_param_names(), mk_Type() >> mk_Type(), mk_Bool()));
auto env7 = add_decl(env2, mk_definition("foo", level_param_names(), mk_Type() >> mk_Type(), mk_Bool()));
lean_unreachable();
} catch (kernel_exception & ex) {
std::cout << "expected error: " << ex.pp(mk_simple_formatter(), options()) << "\n";
}
expr A = Const("A");
expr x = Const("x");
auto env3 = add_def(env2, mk_definition("id", level_param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
auto env3 = add_decl(env2, mk_definition("id", level_param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
expr c = mk_local("c", "c", Bool);
expr id = Const("id");
type_checker checker(env3, name_generator("tmp"));
@ -73,18 +73,18 @@ static void tst1() {
static void tst2() {
environment env;
name base("base");
env = add_def(env, mk_var_decl(name(base, 0u), level_param_names(), Bool >> (Bool >> Bool)));
env = add_decl(env, mk_var_decl(name(base, 0u), level_param_names(), Bool >> (Bool >> Bool)));
expr x = Const("x");
expr y = Const("y");
for (unsigned i = 1; i <= 100; i++) {
expr prev = Const(name(base, i-1));
env = add_def(env, mk_definition(env, name(base, i), level_param_names(), Bool >> (Bool >> Bool),
Fun({{x, Bool}, {y, Bool}}, prev(prev(x, y), prev(y, x)))));
env = add_decl(env, mk_definition(env, name(base, i), level_param_names(), Bool >> (Bool >> Bool),
Fun({{x, Bool}, {y, Bool}}, prev(prev(x, y), prev(y, x)))));
}
expr A = Const("A");
env = add_def(env, mk_definition("id", level_param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
env = add_decl(env, mk_definition("id", level_param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
type_checker checker(env, name_generator("tmp"));
expr f96 = Const(name(base, 96));
expr f97 = Const(name(base, 97));
@ -129,9 +129,9 @@ static void tst3() {
expr A = Const("A");
expr x = Const("x");
expr id = Const("id");
env = add_def(env, mk_definition("id", level_param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
env = add_decl(env, mk_definition("id", level_param_names(),
Pi(A, mk_Type(), A >> A),
Fun({{A, mk_Type()}, {x, A}}, x)));
expr mk = Const("mk");
expr proj1 = Const("proj1");
expr a = Const("a");

4
tests/lua/threads/th2.lua
View file

@ -2,9 +2,9 @@ S1 = State()
S2 = State()
code = [[
function f(env, prefix, num, type)
local r = list_certified_definition()
local r = list_certified_declaration()
for i = 1, num do
r = list_certified_definition(type_check(env, mk_var_decl(prefix .. "_" .. i, type)), r)
r = list_certified_declaration(type_check(env, mk_var_decl(prefix .. "_" .. i, type)), r)
end
return r
end