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

Rename type to domain in contexts (aka telescopes). Reason: make name convention consistent with the one used for abstractions (lambdas and pis).

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-14 12:11:08 -07:00
parent 338ce88ea0
commit e5b8c45b3f
4 changed files with 15 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/context.cpp
View file

@ -19,7 +19,7 @@ format pp(expr_formatter & fmt, context const & c) {
r += format("_");
else
r += format(e.get_name());
r += format{space(), colon(), space(), fmt(e.get_type(), tail(c))};
r += format{space(), colon(), space(), fmt(e.get_domain(), tail(c))};
return r;
} else {
return format();

24
src/kernel/context.h
View file

@ -13,24 +13,24 @@ class context_entry;
typedef list<context_entry> context;
class context_entry {
name m_name;
expr m_type;
expr m_domain;
expr m_body;
friend context extend(context const & c, name const & n, expr const & t, expr const & b);
friend context extend(context const & c, name const & n, expr const & t);
context_entry(name const & n, expr const & t, expr const & b):m_name(n), m_type(t), m_body(b) {}
context_entry(name const & n, expr const & t):m_name(n), m_type(t) {}
friend context extend(context const & c, name const & n, expr const & d, expr const & b);
friend context extend(context const & c, name const & n, expr const & d);
context_entry(name const & n, expr const & d, expr const & b):m_name(n), m_domain(d), m_body(b) {}
context_entry(name const & n, expr const & d):m_name(n), m_domain(d) {}
public:
~context_entry() {}
name const & get_name() const { return m_name; }
expr const & get_type() const { return m_type; }
expr const & get_body() const { return m_body; }
name const & get_name() const { return m_name; }
expr const & get_domain() const { return m_domain; }
expr const & get_body() const { return m_body; }
};
context const & lookup(context const & c, unsigned i);
inline context extend(context const & c, name const & n, expr const & t, expr const & b) {
return context(context_entry(n, t, b), c);
inline context extend(context const & c, name const & n, expr const & d, expr const & b) {
return context(context_entry(n, d, b), c);
}
inline context extend(context const & c, name const & n, expr const & t) {
return context(context_entry(n, t), c);
inline context extend(context const & c, name const & n, expr const & d) {
return context(context_entry(n, d), c);
}
inline bool empty(context const & c) {
return is_nil(c);

2
src/kernel/occurs.cpp
View file

@ -13,7 +13,7 @@ void for_each(F & f, context const * c, unsigned sz, expr const * es) {
for_each_fn<F> visitor(f);
if (c) {
for (auto const & e : *c) {
visitor(e.get_type());
visitor(e.get_domain());
if (e.get_body())
visitor(e.get_body());
}

2
src/kernel/type_check.cpp
View file

@ -53,7 +53,7 @@ struct infer_type_fn {
context const & def_c = ::lean::lookup(c, i);
lean_assert(length(c) >= length(def_c));
lean_assert(length(def_c) > 0);
return lift_free_vars(head(def_c).get_type(), length(c) - (length(def_c) - 1));
return lift_free_vars(head(def_c).get_domain(), length(c) - (length(def_c) - 1));
}
expr_formatter & fmt() { return m_env.get_formatter(); }