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

feat(kernel): add (optional) field m_type to expr_const, this field is useful for implementing the tactic framework

Browse source 
This field should not be visible in the external API.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-19 11:21:45 -08:00
parent 9bafa5a9e8
commit 7f088b7635
14 changed files with 167 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/CMakeLists.txt
View file

@ -1,7 +1,7 @@
add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
type_checker.cpp builtin.cpp occurs.cpp metavar.cpp justification.cpp
unification_constraint.cpp printer.cpp formatter.cpp
unification_constraint.cpp printer.cpp formatter.cpp has_cached_type.cpp
kernel_exception.cpp type_checker_justification.cpp pos_info_provider.cpp
replace_visitor.cpp)

13
src/kernel/environment.cpp
View file

@ -20,6 +20,7 @@ Author: Leonardo de Moura
#include "kernel/threadsafe_environment.h"
#include "kernel/type_checker.h"
#include "kernel/normalizer.h"
#include "kernel/has_cached_type.h"
namespace lean {
static name g_builtin_module("builtin_module");
@ -287,6 +288,11 @@ struct environment::imp {
m_uvars.emplace_back();
}
void check_no_cached_type(expr const & e, environment const & env) {
if (has_cached_type(e))
throw kernel_exception(env, "expression has a constant with a cached type, this is a bug in one of Lean tactics and/or solvers");
}
/**
\brief Throw an exception if \c t is not a type or type of \c
v is not convertible to \c t.
@ -331,6 +337,8 @@ struct environment::imp {
/** \brief Add new definition. */
void add_definition(name const & n, expr const & t, expr const & v, bool opaque, environment const & env) {
check_no_cached_type(t, env);
check_no_cached_type(v, env);
check_new_definition(n, t, v, env);
unsigned w = get_max_weight(v) + 1;
register_named_object(mk_definition(n, t, v, opaque, w));
@ -341,6 +349,7 @@ struct environment::imp {
The type of the new definition is the type of \c v.
*/
void add_definition(name const & n, expr const & v, bool opaque, environment const & env) {
check_no_cached_type(v, env);
check_name(n, env);
expr v_t = m_type_checker->infer_type(v);
unsigned w = get_max_weight(v) + 1;
@ -349,12 +358,15 @@ struct environment::imp {
/** \brief Add new theorem. */
void add_theorem(name const & n, expr const & t, expr const & v, environment const & env) {
check_no_cached_type(t, env);
check_no_cached_type(v, env);
check_new_definition(n, t, v, env);
register_named_object(mk_theorem(n, t, v));
}
/** \brief Add new axiom. */
void add_axiom(name const & n, expr const & t, environment const & env) {
check_no_cached_type(t, env);
check_name(n, env);
m_type_checker->check_type(t);
register_named_object(mk_axiom(n, t));
@ -362,6 +374,7 @@ struct environment::imp {
/** \brief Add new variable. */
void add_var(name const & n, expr const & t, environment const & env) {
check_no_cached_type(t, env);
check_name(n, env);
m_type_checker->check_type(t);
register_named_object(mk_var_decl(n, t));

15
src/kernel/expr.cpp
View file

@ -67,9 +67,14 @@ expr_var::expr_var(unsigned idx):
expr_cell(expr_kind::Var, idx, false),
m_vidx(idx) {}
expr_const::expr_const(name const & n):
expr_cell(expr_kind::Constant, n.hash(), false),
m_name(n) {}
expr_const::expr_const(name const & n, expr const & t):
expr_cell(expr_kind::Constant, n.hash(), t && t.has_metavar()),
m_name(n),
m_type(t) {}
void expr_const::dealloc(buffer<expr_cell*> & todelete) {
dec_ref(m_type, todelete);
delete(this);
}
expr_app::expr_app(unsigned num_args, bool has_mv):
expr_cell(expr_kind::App, 0, has_mv),
@ -196,10 +201,10 @@ void expr_cell::dealloc() {
lean_assert(it->get_rc() == 0);
switch (it->kind()) {
case expr_kind::Var: delete static_cast<expr_var*>(it); break;
case expr_kind::Constant: delete static_cast<expr_const*>(it); break;
case expr_kind::Value: delete static_cast<expr_value*>(it); break;
case expr_kind::MetaVar: delete static_cast<expr_metavar*>(it); break;
case expr_kind::Type: delete static_cast<expr_type*>(it); break;
case expr_kind::Constant: static_cast<expr_const*>(it)->dealloc(todo); break;
case expr_kind::Eq: static_cast<expr_eq*>(it)->dealloc(todo); break;
case expr_kind::App: static_cast<expr_app*>(it)->dealloc(todo); break;
case expr_kind::Lambda: static_cast<expr_lambda*>(it)->dealloc(todo); break;
@ -229,7 +234,7 @@ bool is_arrow(expr const & t) {
expr copy(expr const & a) {
switch (a.kind()) {
case expr_kind::Var: return mk_var(var_idx(a));
case expr_kind::Constant: return mk_constant(const_name(a));
case expr_kind::Constant: return mk_constant(const_name(a), const_type(a));
case expr_kind::Type: return mk_type(ty_level(a));
case expr_kind::Value: return mk_value(static_cast<expr_value*>(a.raw())->m_val);
case expr_kind::App: return mk_app(num_args(a), begin_args(a));

22
src/kernel/expr.h
View file

@ -125,7 +125,7 @@ public:
operator bool() const { return m_ptr != nullptr; }
friend expr mk_var(unsigned idx);
friend expr mk_constant(name const & n);
friend expr mk_constant(name const & n, expr const & t);
friend expr mk_value(value & v);
friend expr mk_app(unsigned num_args, expr const * args);
friend expr mk_eq(expr const & l, expr const & r);
@ -160,9 +160,15 @@ public:
/** \brief Constants. */
class expr_const : public expr_cell {
name m_name;
expr m_type; // (optional) cached type
// Remark: we do *not* perform destructive updates on m_type
// This field is used to efficiently implement the tactic framework
friend class expr_cell;
void dealloc(buffer<expr_cell*> & to_delete);
public:
expr_const(name const & n);
expr_const(name const & n, expr const & type);
name const & get_name() const { return m_name; }
expr const & get_type() const { return m_type; }
};
/** \brief Function Applications */
class expr_app : public expr_cell {
@ -375,7 +381,7 @@ inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); }
// Constructors
inline expr mk_var(unsigned idx) { return expr(new expr_var(idx)); }
inline expr Var(unsigned idx) { return mk_var(idx); }
inline expr mk_constant(name const & n) { return expr(new expr_const(n)); }
inline expr mk_constant(name const & n, expr const & t = expr()) { return expr(new expr_const(n, t)); }
inline expr Const(name const & n) { return mk_constant(n); }
inline expr mk_value(value & v) { return expr(new expr_value(v)); }
inline expr to_expr(value & v) { return mk_value(v); }
@ -444,6 +450,8 @@ inline bool is_shared(expr_cell * e) { return get_rc(e) > 1;
inline unsigned var_idx(expr_cell * e) { return to_var(e)->get_vidx(); }
inline bool is_var(expr_cell * e, unsigned i) { return is_var(e) && var_idx(e) == i; }
inline name const & const_name(expr_cell * e) { return to_constant(e)->get_name(); }
// Remark: the following function should not be exposed in the internal API.
inline expr const & const_type(expr_cell * e) { return to_constant(e)->get_type(); }
inline value const & to_value(expr_cell * e) { lean_assert(is_value(e)); return static_cast<expr_value*>(e)->get_value(); }
inline unsigned num_args(expr_cell * e) { return to_app(e)->get_num_args(); }
inline expr const & arg(expr_cell * e, unsigned idx) { return to_app(e)->get_arg(idx); }
@ -469,6 +477,8 @@ inline unsigned var_idx(expr const & e) { return to_var(e)->ge
/** \brief Return true iff the given expression is a variable with de Bruijn index equal to \c i. */
inline bool is_var(expr const & e, unsigned i) { return is_var(e) && var_idx(e) == i; }
inline name const & const_name(expr const & e) { return to_constant(e)->get_name(); }
// Remark: the following function should not be exposed in the internal API.
inline expr const & const_type(expr const & e) { return to_constant(e)->get_type(); }
/** \brief Return true iff the given expression is a constant with name \c n. */
inline bool is_constant(expr const & e, name const & n) {
return is_constant(e) && const_name(e) == n;
@ -647,6 +657,12 @@ inline expr update_metavar(expr const & e, local_context const & lctx) {
else
return e;
}
inline expr update_const(expr const & e, expr const & t) {
if (!is_eqp(const_type(e), t))
return mk_constant(const_name(e), t);
else
return e;
}
// =======================================
std::ostream & operator<<(std::ostream & out, expr const & e);

2
src/kernel/expr_eq.h
View file

@ -46,7 +46,7 @@ class expr_eq_fn {
}
switch (a.kind()) {
case expr_kind::Var: lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Constant: return const_name(a) == const_name(b);
case expr_kind::Constant: return const_name(a) == const_name(b) && apply(const_type(a), const_type(b));
case expr_kind::App:
if (num_args(a) != num_args(b))
return false;

15
src/kernel/for_each.h
View file

@ -40,7 +40,14 @@ class for_each_fn {
unsigned offset = p.second;
if (!CacheAtomic) {
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
case expr_kind::Constant:
if (!const_type(e)) {
// only constants without cached types are considered atomic
m_f(e, offset);
goto begin_loop;
}
break;
case expr_kind::Type: case expr_kind::Value:
case expr_kind::Var: case expr_kind::MetaVar:
m_f(e, offset);
goto begin_loop;
@ -62,7 +69,11 @@ class for_each_fn {
goto begin_loop;
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
case expr_kind::Constant:
if (const_type(e))
todo.emplace_back(const_type(e), offset);
goto begin_loop;
case expr_kind::Type: case expr_kind::Value:
case expr_kind::Var: case expr_kind::MetaVar:
goto begin_loop;
case expr_kind::App: {

24
src/kernel/free_vars.cpp
View file

@ -24,7 +24,11 @@ protected:
bool apply(expr const & e, unsigned offset) {
// handle easy cases
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
case expr_kind::Constant:
if (!const_type(e))
return false;
break;
case expr_kind::Type: case expr_kind::Value:
return false;
case expr_kind::MetaVar:
return true;
@ -58,7 +62,11 @@ protected:
bool result = false;
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
case expr_kind::Constant:
lean_assert(const_type(e));
result = apply(const_type(e), offset);
break;
case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
// easy cases were already handled
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::App:
@ -109,7 +117,11 @@ protected:
bool apply(expr const & e, unsigned offset) {
// handle easy cases
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
case expr_kind::Constant:
if (!const_type(e))
return false;
break;
case expr_kind::Type: case expr_kind::Value:
return false;
case expr_kind::MetaVar:
return true;
@ -133,7 +145,11 @@ protected:
bool result = false;
switch (e.kind()) {
case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
case expr_kind::Constant:
lean_assert(const_type(e));
result = apply(const_type(e), offset);
break;
case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar:
// easy cases were already handled
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::App:

27
src/kernel/has_cached_type.cpp Normal file
View file

@ -0,0 +1,27 @@
/*
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 "kernel/expr.h"
#include "kernel/for_each.h"
namespace lean {
bool has_cached_type(expr const & e) {
bool result = false;
auto f = [&](expr const & e, unsigned) {
if (result) {
return false; // do not continue the search
} else if (is_constant(e) && const_type(e)) {
result = true;
return false;
} else {
return true;
}
};
for_each_fn<decltype(f)> proc(f);
proc(e);
return result;
}
}

22
src/kernel/has_cached_type.h Normal file
View file

@ -0,0 +1,22 @@
/*
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 "kernel/expr.h"
namespace lean {
/**
\brief Return true iff \c e contains a constant with a cached type.
The kernel should *not* accept expressions containing cached types.
Reason: Cached types may introduce unsoundness.
For example, in the environment env, the constant x may have type T.
Now suppose we are trying to add a new definition D that contains x,
and x is associated with a cached type T'. The cached type may allow
us to accept a definition that is type incorrect with respect to env.
*/
bool has_cached_type(expr const & e);
}

6
src/kernel/replace.h
View file

@ -59,7 +59,11 @@ class replace_fn {
expr r = m_f(e, offset);
if (is_eqp(e, r)) {
switch (e.kind()) {
case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant:
case expr_kind::Constant:
if (const_type(e))
r = update_const(e, apply(const_type(e), offset));
break;
case expr_kind::Type: case expr_kind::Value:
case expr_kind::Var: case expr_kind::MetaVar:
break;
case expr_kind::App:

9
src/kernel/replace_visitor.cpp
View file

@ -10,9 +10,16 @@ Author: Leonardo de Moura
namespace lean {
expr replace_visitor::visit_type(expr const & e, context const &) { lean_assert(is_type(e)); return e; }
expr replace_visitor::visit_value(expr const & e, context const &) { lean_assert(is_value(e)); return e; }
expr replace_visitor::visit_constant(expr const & e, context const &) { lean_assert(is_constant(e)); return e; }
expr replace_visitor::visit_var(expr const & e, context const &) { lean_assert(is_var(e)); return e; }
expr replace_visitor::visit_metavar(expr const & e, context const &) { lean_assert(is_metavar(e)); return e; }
expr replace_visitor::visit_constant(expr const & e, context const & ctx) {
lean_assert(is_constant(e));
if (const_type(e)) {
return update_const(e, visit(const_type(e), ctx));
} else {
return e;
}
}
expr replace_visitor::visit_app(expr const & e, context const & ctx) {
lean_assert(is_app(e));
return update_app(e, [&](expr const & c) { return visit(c, ctx); });

14
src/kernel/type_checker.cpp
View file

@ -107,11 +107,15 @@ class type_checker::imp {
}
break;
case expr_kind::Constant: {
object const & obj = env().get_object(const_name(e));
if (obj.has_type())
r = obj.get_type();
else
throw has_no_type_exception(env(), e);
if (const_type(e)) {
r = const_type(e);
} else {
object const & obj = env().get_object(const_name(e));
if (obj.has_type())
r = obj.get_type();
else
throw has_no_type_exception(env(), e);
}
break;
}
case expr_kind::Var:

11
src/library/max_sharing.cpp
View file

@ -36,7 +36,16 @@ struct max_sharing_fn::imp {
return a;
}
switch (a.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
case expr_kind::Constant:
if (const_type(a)) {
expr r = update_const(a, apply(const_type(a)));
cache(r);
return r;
} else {
cache(a);
return a;
}
case expr_kind::Var: case expr_kind::Type: case expr_kind::Value:
cache(a);
return a;
case expr_kind::App: {

14
src/library/type_inferer.cpp
View file

@ -110,11 +110,15 @@ class type_inferer::imp {
throw unexpected_metavar_occurrence(m_env, e);
}
case expr_kind::Constant: {
object const & obj = m_env.get_object(const_name(e));
if (obj.has_type())
return obj.get_type();
else
throw has_no_type_exception(m_env, e);
if (const_type(e)) {
return const_type(e);
} else {
object const & obj = m_env.get_object(const_name(e));
if (obj.has_type())
return obj.get_type();
else
throw has_no_type_exception(m_env, e);
}
break;
}
case expr_kind::Var: {