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

refactor(kernel/expr): adding suport for universe polymorphism, and simplify metavariable representation

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-14 19:55:02 -08:00
parent 13cfd60622
commit 02413d7c44
4 changed files with 233 additions and 288 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/CMakeLists.txt
View file

@ -1,5 +1,4 @@
add_library(kernel level.cpp diff_cnstrs.cpp
# expr.cpp
add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp
# free_vars.cpp abstract.cpp instantiate.cpp
# normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
# type_checker.cpp kernel.cpp occurs.cpp metavar.cpp

10
src/kernel/expr.cpp
View file

@ -13,12 +13,13 @@ Author: Leonardo de Moura
#include "util/buffer.h"
#include "util/object_serializer.h"
#include "kernel/expr.h"
#include "kernel/free_vars.h"
#include "kernel/expr_eq.h"
#include "kernel/metavar.h"
#include "kernel/max_sharing.h"
// #include "kernel/free_vars.h"
// #include "kernel/expr_eq.h"
// #include "kernel/metavar.h"
// #include "kernel/max_sharing.h"
namespace lean {
#if 0
static expr g_dummy(mk_var(0));
expr::expr():expr(g_dummy) {}
@ -576,4 +577,5 @@ serializer & operator<<(serializer & s, expr const & n) {
expr read_expr(deserializer & d) {
return d.get_extension<expr_deserializer>(g_expr_sd.m_d_extid).read();
}
#endif
}

469
src/kernel/expr.h
View file

@ -24,52 +24,26 @@ Author: Leonardo de Moura
#include "kernel/level.h"
namespace lean {
class value;
class expr;
/* =======================================
Expressions
expr ::= Var idx
| Constant name
| Value value
| App [expr]
| Sort level
| Constant name [levels]
| Meta name expr
| Local name expr
| App expr expr
| Pair expr expr expr
| Proj bool expr The Boolean flag indicates whether is the first/second projection
| Fst expr
| Snd expr
| Lambda name expr expr
| Pi name expr expr
| Sigma name expr expr
| Type universe
| Let name expr expr expr
| HEq expr expr Heterogeneous equality
| Metavar name local_context
| Let name expr? expr expr
local_context ::= [local_entry]
local_entry ::= lift idx idx
| inst idx expr
TODO(Leo): match expressions.
The main API is divided in the following sections
- Testers
- Constructors
- Accessors
- Miscellaneous
======================================= */
class expr;
enum class expr_kind { Value, Var, Constant, App, Pair, Proj, Lambda, Pi, Sigma, Type, Let, HEq, MetaVar };
class local_entry;
/**
\brief A metavariable local context is just a list of local_entries.
\see local_entry
*/
typedef list<local_entry> local_context;
/**
\brief Base class used to represent expressions.
In principle, the expr_cell class and subclasses should be located in the .cpp file.
However, this is performance critical code, and we want to be able to have
inline definitions.
| Macro macro
*/
enum class expr_kind { Var, Sort, Constant, Meta, Local, App, Pair, Fst, Snd, Lambda, Pi, Sigma, Let, Macro };
class expr_cell {
protected:
unsigned short m_kind;
@ -105,6 +79,9 @@ public:
unsigned hash_alloc() const { return m_hash_alloc; }
bool has_metavar() const { return (m_flags & 4) != 0; }
};
class macro;
/**
\brief Exprs for encoding formulas/expressions, types and proofs.
*/
@ -142,18 +119,19 @@ public:
expr_cell * raw() const { return m_ptr; }
friend expr mk_var(unsigned idx);
friend expr mk_constant(name const & n, optional<expr> const & t);
friend expr mk_value(value & v);
friend expr mk_sort(level const & l);
friend expr mk_constant(name const & n, list<level> const & ls);
friend expr mk_metavar(name const & n, expr const & t);
friend expr mk_local(name const & n, expr const & t);
friend expr mk_app(expr const & f, expr const & a);
friend expr mk_pair(expr const & f, expr const & s, expr const & t);
friend expr mk_proj(bool f, expr const & t);
friend expr mk_app(unsigned num_args, expr const * args);
friend expr mk_fst(expr const & p);
friend expr mk_snd(expr const & p);
friend expr mk_lambda(name const & n, expr const & t, expr const & e);
friend expr mk_pi(name const & n, expr const & t, expr const & e);
friend expr mk_sigma(name const & n, expr const & t, expr const & e);
friend expr mk_type(level const & l);
friend expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e);
friend expr mk_heq(expr const & lhs, expr const & rhs);
friend expr mk_metavar(name const & n, local_context const & ctx);
friend expr mk_macro(macro * m);
friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
// Overloaded operator() can be used to create applications
@ -163,8 +141,10 @@ public:
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6, expr const & a7) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6, expr const & a7, expr const & a8) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6,
expr const & a7) const;
expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6,
expr const & a7, expr const & a8) const;
};
// =======================================
@ -183,115 +163,104 @@ inline bool is_eqp(optional<expr> const & a, optional<expr> const & b) {
return static_cast<bool>(a) == static_cast<bool>(b) && (!a || is_eqp(*a, *b));
}
// =======================================
// Expr (internal) Representation
/** \brief Free variables. They are encoded using de Bruijn's indices. */
/** \brief Bounded variables. They are encoded using de Bruijn's indices. */
class expr_var : public expr_cell {
unsigned m_vidx; // de Bruijn index
public:
expr_var(unsigned idx);
unsigned get_vidx() const { return m_vidx; }
};
/** \brief Constants. */
/** \brief (parametric) Constants. */
class expr_const : public expr_cell {
name m_name;
optional<expr> m_type;
// Remark: we do *not* perform destructive updates on m_type
// This field is used to efficiently implement the tactic framework
list<level> m_levels;
friend class expr_cell;
void dealloc(buffer<expr_cell*> & to_delete);
public:
expr_const(name const & n, optional<expr> const & type);
expr_const(name const & n, list<level> const & ls);
name const & get_name() const { return m_name; }
optional<expr> const & get_type() const { return m_type; }
list<level> const & get_level_params() const { return m_levels; }
};
/** \brief Function Applications */
class expr_app : public expr_cell {
/** \brief Metavariables and local constants */
class expr_meta_local : public expr_cell {
name m_name;
expr m_type;
public:
expr_meta_local(bool is_meta, name const & n, expr const & t);
name const & get_name() const { return m_name; }
expr const & get_type() const { return m_type; }
};
/** \brief Composite expressions */
class expr_composite : public expr_cell {
unsigned m_depth;
unsigned m_num_args;
expr m_args[0];
friend expr mk_app(unsigned num_args, expr const * args);
friend expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
friend unsigned get_depth(expr const & e);
public:
expr_app(unsigned size, bool has_mv);
unsigned get_num_args() const { return m_num_args; }
expr const & get_arg(unsigned idx) const { lean_assert(idx < m_num_args); return m_args[idx]; }
expr const * begin_args() const { return m_args; }
expr const * end_args() const { return m_args + m_num_args; }
expr_composite(expr_kind k, unsigned h, bool has_mv, unsigned d);
};
/** \brief Applications */
class expr_app : public expr_composite {
expr m_fn;
expr m_arg;
friend expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
public:
expr_app(expr const & fn, expr const & arg);
expr const & get_fn() const { return m_fn; }
expr const & get_arg() const { return m_arg; }
};
/** \brief dependent pairs */
class expr_dep_pair : public expr_cell {
class expr_dep_pair : public expr_composite {
expr m_first;
expr m_second;
expr m_type;
unsigned m_depth;
friend expr_cell;
friend expr mk_pair(expr const & f, expr const & s, expr const & t);
void dealloc(buffer<expr_cell*> & todelete);
friend unsigned get_depth(expr const & e);
public:
expr_dep_pair(expr const & f, expr const & s, expr const & t);
expr const & get_first() const { return m_first; }
expr const & get_second() const { return m_second; }
expr const & get_type() const { return m_type; }
};
/** \brief dependent pair projection */
class expr_proj : public expr_cell {
bool m_first; // first/second projection
unsigned m_depth;
class expr_proj : public expr_composite {
expr m_expr;
friend expr_cell;
friend expr mk_proj(unsigned idx, expr const & t);
void dealloc(buffer<expr_cell*> & todelete);
friend unsigned get_depth(expr const & e);
public:
expr_proj(bool first, expr const & e);
bool first() const { return m_first; }
bool second() const { return !m_first; }
expr const & get_arg() const { return m_expr; }
};
/** \brief Super class for lambda abstraction and pi (functional spaces). */
class expr_abstraction : public expr_cell {
unsigned m_depth;
/** \brief Super class for lambda, pi and sigma */
class expr_binder : public expr_composite {
name m_name;
expr m_domain;
expr m_body;
friend class expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
friend unsigned get_depth(expr const & e);
public:
expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & e);
expr_binder(expr_kind k, name const & n, expr const & t, expr const & e);
name const & get_name() const { return m_name; }
expr const & get_domain() const { return m_domain; }
expr const & get_body() const { return m_body; }
};
/** \brief Lambda abstractions */
class expr_lambda : public expr_abstraction {
public:
expr_lambda(name const & n, expr const & t, expr const & e);
};
/** \brief (dependent) Functional spaces */
class expr_pi : public expr_abstraction {
public:
expr_pi(name const & n, expr const & t, expr const & e);
};
/** \brief Sigma types (aka the type of dependent pairs) */
class expr_sigma : public expr_abstraction {
public:
expr_sigma(name const & n, expr const & t, expr const & e);
};
/** \brief Let expressions */
class expr_let : public expr_cell {
unsigned m_depth;
class expr_let : public expr_composite {
name m_name;
optional<expr> m_type;
expr m_value;
expr m_body;
friend class expr_cell;
void dealloc(buffer<expr_cell*> & todelete);
friend unsigned get_depth(expr const & e);
public:
expr_let(name const & n, optional<expr> const & t, expr const & v, expr const & b);
~expr_let();
@ -300,261 +269,196 @@ public:
expr const & get_value() const { return m_value; }
expr const & get_body() const { return m_body; }
};
/** \brief Type */
class expr_type : public expr_cell {
/** \brief Sort */
class expr_sort : public expr_cell {
level m_level;
public:
expr_type(level const & l);
~expr_type();
expr_sort(level const & l);
~expr_sort();
level const & get_level() const { return m_level; }
};
/** \brief Base class for semantic attachment cells. */
class value {
class formatter;
/** \brief Base class for macro attachments */
class macro {
void dealloc() { delete this; }
MK_LEAN_RC();
protected:
/**
\brief Auxiliary method used for implementing a total order on semantic
\brief Auxiliary method used for implementing a total order on macro
attachments. It is invoked by operator<, and it is only invoked when
<tt>get_name() == other.get_name()</tt>
*/
virtual bool lt(value const &) const { return false; }
virtual bool lt(macro const &) const { return false; }
public:
value():m_rc(0) {}
virtual ~value() {}
virtual expr get_type() const = 0;
macro():m_rc(0) {}
virtual ~macro() {}
virtual name get_name() const = 0;
virtual name get_unicode_name() const;
virtual optional<expr> normalize(unsigned num_args, expr const * args) const;
virtual bool operator==(value const & other) const;
bool operator<(value const & other) const;
virtual void display(std::ostream & out) const;
virtual format pp() const;
virtual format pp(bool unicode, bool coercion) const;
virtual bool is_atomic_pp(bool unicode, bool coercion) const = 0;
virtual expr get_type(buffer<expr> const & arg_types) const = 0;
virtual expr expand1(buffer<expr> const & args) const = 0;
virtual expr expand(buffer<expr> const & args) const = 0;
virtual int push_lua(lua_State * L) const;
virtual bool operator==(macro const & other) const;
bool operator<(macro const & other) const;
virtual void display(std::ostream & out) const;
virtual format pp(formatter const & fmt, options const & opts) const;
virtual bool is_atomic_pp(bool unicode, bool coercion) const;
virtual unsigned hash() const;
virtual void write(serializer & s) const = 0;
typedef std::function<expr(deserializer&)> reader;
static void register_deserializer(std::string const & k, reader rd);
struct register_deserializer_fn {
register_deserializer_fn(std::string const & k, value::reader rd) { value::register_deserializer(k, rd); }
register_deserializer_fn(std::string const & k, macro::reader rd) { macro::register_deserializer(k, rd); }
};
};
/** \brief Semantic attachments */
class expr_value : public expr_cell {
value & m_val;
/** \brief Macro attachments */
class expr_macro : public expr_cell {
macro * m_macro;
friend expr copy(expr const & a);
public:
expr_value(value & v);
~expr_value();
expr_macro(macro * v);
~expr_macro();
value const & get_value() const { return m_val; }
macro const & get_macro() const { return *m_macro; }
};
/** \brief Heterogeneous equality */
class expr_heq : public expr_cell {
expr m_lhs;
expr m_rhs;
unsigned m_depth;
friend expr_cell;
friend expr mk_heq(expr const & lhs, expr const & rhs);
void dealloc(buffer<expr_cell*> & todelete);
friend unsigned get_depth(expr const & e);
public:
expr_heq(expr const & lhs, expr const & rhs);
expr const & get_lhs() const { return m_lhs; }
expr const & get_rhs() const { return m_rhs; }
};
/**
\see local_entry
*/
enum class local_entry_kind { Lift, Inst };
/**
\brief An entry in a metavariable context.
It represents objects of the form:
<code>
| Lift s n
| Inst s v
</code>
where \c s and \c n are unsigned integers, and
\c v is an expression
The meaning of <tt>Lift s n</tt> is: lift the free variables greater than or equal to \c s by \c n.
The meaning of <tt>Inst s v</tt> is: instantiate free variable \c s with the expression \c v, and
lower free variables greater than \c s.
The metavariable context records operations that must be applied
whenever we substitute a metavariable with an actual expression.
For example, let ?M be a metavariable with context
<code>
[ Inst 0 a, Lift 1 2 ]
</code>
Now, assume we want to instantiate \c ?M with <tt>f #0 (g #2)</tt>.
Then, we apply the metavariable entries from right to left.
Thus, first we apply <tt>(Lift 1 2)</tt> and obtain the term
<code>
f #0 (g #4)
</code>
Then, we apply <tt>(Inst 0 a)</tt> and produce
<code>
f a (g #3)
</code>
*/
class local_entry {
local_entry_kind m_kind;
unsigned m_s;
unsigned m_n;
optional<expr> m_v;
local_entry(unsigned s, unsigned n);
local_entry(unsigned s, expr const & v);
public:
~local_entry();
friend local_entry mk_lift(unsigned s, unsigned n);
friend local_entry mk_inst(unsigned s, expr const & v);
local_entry_kind kind() const { return m_kind; }
bool is_inst() const { return kind() == local_entry_kind::Inst; }
bool is_lift() const { return kind() == local_entry_kind::Lift; }
unsigned s() const { return m_s; }
unsigned n() const { lean_assert(is_lift()); return m_n; }
bool operator==(local_entry const & e) const;
bool operator!=(local_entry const & e) const { return !operator==(e); }
expr const & v() const { lean_assert(is_inst()); return *m_v; }
};
inline local_entry mk_lift(unsigned s, unsigned n) { return local_entry(s, n); }
inline local_entry mk_inst(unsigned s, expr const & v) { return local_entry(s, v); }
/** \brief Metavariables */
class expr_metavar : public expr_cell {
name m_name;
local_context m_lctx;
public:
expr_metavar(name const & n, local_context const & lctx);
~expr_metavar();
name const & get_name() const { return m_name; }
local_context const & get_lctx() const { return m_lctx; }
};
// =======================================
// =======================================
// Testers
inline bool is_var(expr_cell * e) { return e->kind() == expr_kind::Var; }
inline bool is_constant(expr_cell * e) { return e->kind() == expr_kind::Constant; }
inline bool is_value(expr_cell * e) { return e->kind() == expr_kind::Value; }
inline bool is_local(expr_cell * e) { return e->kind() == expr_kind::Local; }
inline bool is_metavar(expr_cell * e) { return e->kind() == expr_kind::Meta; }
inline bool is_macro(expr_cell * e) { return e->kind() == expr_kind::Macro; }
inline bool is_dep_pair(expr_cell * e) { return e->kind() == expr_kind::Pair; }
inline bool is_proj(expr_cell * e) { return e->kind() == expr_kind::Proj; }
inline bool is_fst(expr_cell * e) { return e->kind() == expr_kind::Fst; }
inline bool is_snd(expr_cell * e) { return e->kind() == expr_kind::Snd; }
inline bool is_app(expr_cell * e) { return e->kind() == expr_kind::App; }
inline bool is_lambda(expr_cell * e) { return e->kind() == expr_kind::Lambda; }
inline bool is_pi(expr_cell * e) { return e->kind() == expr_kind::Pi; }
inline bool is_sigma(expr_cell * e) { return e->kind() == expr_kind::Sigma; }
inline bool is_type(expr_cell * e) { return e->kind() == expr_kind::Type; }
inline bool is_sort(expr_cell * e) { return e->kind() == expr_kind::Sort; }
inline bool is_let(expr_cell * e) { return e->kind() == expr_kind::Let; }
inline bool is_heq(expr_cell * e) { return e->kind() == expr_kind::HEq; }
inline bool is_metavar(expr_cell * e) { return e->kind() == expr_kind::MetaVar; }
inline bool is_abstraction(expr_cell * e) { return is_lambda(e) || is_pi(e) || is_sigma(e); }
inline bool is_binder(expr_cell * e) { return is_lambda(e) || is_pi(e) || is_sigma(e); }
inline bool is_proj(expr_cell * e) { return is_fst(e) || is_snd(e); }
inline bool is_meta_local(expr_cell * e) { return is_metavar(e) || is_local(e); }
inline bool is_var(expr const & e) { return e.kind() == expr_kind::Var; }
inline bool is_constant(expr const & e) { return e.kind() == expr_kind::Constant; }
inline bool is_value(expr const & e) { return e.kind() == expr_kind::Value; }
inline bool is_dep_pair(expr const & e) { return e.kind() == expr_kind::Pair; }
inline bool is_proj(expr const & e) { return e.kind() == expr_kind::Proj; }
inline bool is_app(expr const & e) { return e.kind() == expr_kind::App; }
inline bool is_lambda(expr const & e) { return e.kind() == expr_kind::Lambda; }
inline bool is_pi(expr const & e) { return e.kind() == expr_kind::Pi; }
bool is_arrow(expr const & e);
bool is_cartesian(expr const & e);
inline bool is_sigma(expr const & e) { return e.kind() == expr_kind::Sigma; }
inline bool is_type(expr const & e) { return e.kind() == expr_kind::Type; }
inline bool is_let(expr const & e) { return e.kind() == expr_kind::Let; }
inline bool is_heq(expr const & e) { return e.kind() == expr_kind::HEq; }
inline bool is_metavar(expr const & e) { return e.kind() == expr_kind::MetaVar; }
inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e) || is_sigma(e); }
inline bool is_var(expr const & e) { return e.kind() == expr_kind::Var; }
inline bool is_constant(expr const & e) { return e.kind() == expr_kind::Constant; }
inline bool is_local(expr const & e) { return e.kind() == expr_kind::Local; }
inline bool is_metavar(expr const & e) { return e.kind() == expr_kind::Meta; }
inline bool is_macro(expr const & e) { return e.kind() == expr_kind::Macro; }
inline bool is_dep_pair(expr const & e) { return e.kind() == expr_kind::Pair; }
inline bool is_fst(expr const & e) { return e.kind() == expr_kind::Fst; }
inline bool is_snd(expr const & e) { return e.kind() == expr_kind::Snd; }
inline bool is_app(expr const & e) { return e.kind() == expr_kind::App; }
inline bool is_lambda(expr const & e) { return e.kind() == expr_kind::Lambda; }
inline bool is_pi(expr const & e) { return e.kind() == expr_kind::Pi; }
inline bool is_sigma(expr const & e) { return e.kind() == expr_kind::Sigma; }
inline bool is_sort(expr const & e) { return e.kind() == expr_kind::Sort; }
inline bool is_let(expr const & e) { return e.kind() == expr_kind::Let; }
inline bool is_binder(expr const & e) { return is_lambda(e) || is_pi(e) || is_sigma(e); }
inline bool is_proj(expr const & e) { return is_fst(e) || is_snd(e); }
inline bool is_meta_local(expr const & e) { return is_metavar(e) || is_local(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, optional<expr> const & t) { return expr(new expr_const(n, t)); }
inline expr mk_constant(name const & n, expr const & t) { return mk_constant(n, some_expr(t)); }
inline expr mk_constant(name const & n) { return mk_constant(n, none_expr()); }
inline expr mk_constant(name const & n, list<level> const & ls) { return expr(new expr_const(n, ls)); }
inline expr mk_constant(name const & n) { return mk_constant(n, list<level>()); }
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); }
inline expr mk_macro(macro * m) { return expr(new expr_macro(m)); }
inline expr mk_metavar(name const & n, expr const & t) { return expr(new expr_meta_local(true, n, t)); }
inline expr mk_local(name const & n, expr const & t) { return expr(new expr_meta_local(false, n, t)); }
inline expr mk_pair(expr const & f, expr const & s, expr const & t) { return expr(new expr_dep_pair(f, s, t)); }
inline expr mk_proj(bool f, expr const & e) { return expr(new expr_proj(f, e)); }
inline expr mk_proj1(expr const & e) { return mk_proj(true, e); }
inline expr mk_proj2(expr const & e) { return mk_proj(false, e); }
inline expr mk_fst(expr const & a) { return expr(new expr_proj(true, a)); }
inline expr mk_snd(expr const & a) { return expr(new expr_proj(false, a)); }
inline expr mk_app(expr const & f, expr const & a) { return expr(new expr_app(f, a)); }
expr mk_app(unsigned num_args, expr const * args);
inline expr mk_app(std::initializer_list<expr> const & l) { return mk_app(l.size(), l.begin()); }
template<typename T> expr mk_app(T const & args) { return mk_app(args.size(), args.data()); }
inline expr mk_app(expr const & e1, expr const & e2) { return mk_app({e1, e2}); }
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { return mk_app({e1, e2, e3}); }
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({e1, e2, e3, e4}); }
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) { return mk_app({e1, e2, e3, e4, e5}); }
inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); }
inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
inline expr mk_sigma(name const & n, expr const & t, expr const & e) { return expr(new expr_sigma(n, t, e)); }
inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Lambda, n, t, e)); }
inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Pi, n, t, e)); }
inline expr mk_sigma(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Sigma, n, t, e)); }
inline bool is_default_arrow_var_name(name const & n) { return n == "a"; }
inline expr mk_arrow(expr const & t, expr const & e) { return mk_pi(name("a"), t, e); }
inline expr mk_cartesian_product(expr const & t, expr const & e) { return mk_sigma(name("a"), t, e); }
inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); }
inline expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); }
inline expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e) {
return expr(new expr_let(n, t, v, e));
}
inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return mk_let(n, some_expr(t), v, e); }
inline expr mk_let(name const & n, expr const & v, expr const & e) { return mk_let(n, none_expr(), v, e); }
inline expr mk_type(level const & l) { return expr(new expr_type(l)); }
expr mk_type();
inline expr Type(level const & l) { return mk_type(l); }
inline expr Type() { return mk_type(); }
inline expr mk_heq(expr const & lhs, expr const & rhs) { return expr(new expr_heq(lhs, rhs)); }
inline expr mk_metavar(name const & n, local_context const & ctx = local_context()) {
return expr(new expr_metavar(n, ctx));
}
inline expr mk_sort(level const & l) { return expr(new expr_sort(l)); }
expr mk_Bool();
expr mk_Type();
extern expr Type;
extern expr Bool;
// Auxiliary
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3) { return mk_app({e1, e2, e3}); }
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({e1, e2, e3, e4}); }
inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5) {
return mk_app({e1, e2, e3, e4, e5});
}
inline expr expr::operator()(expr const & a1) const { return mk_app({*this, a1}); }
inline expr expr::operator()(expr const & a1, expr const & a2) const { return mk_app({*this, a1, a2}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3) const { return mk_app({*this, a1, a2, a3}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const { return mk_app({*this, a1, a2, a3, a4}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const { return mk_app({*this, a1, a2, a3, a4, a5}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6) const { return mk_app({*this, a1, a2, a3, a4, a5, a6}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6, expr const & a7) const { return mk_app({*this, a1, a2, a3, a4, a5, a6, a7}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5, expr const & a6, expr const & a7, expr const & a8) const { return mk_app({*this, a1, a2, a3, a4, a5, a6, a7, a8}); }
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
return mk_app({*this, a1, a2, a3, a4});
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
return mk_app({*this, a1, a2, a3, a4, a5});
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5,
expr const & a6) const {
return mk_app({*this, a1, a2, a3, a4, a5, a6});
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5,
expr const & a6, expr const & a7) const {
return mk_app({*this, a1, a2, a3, a4, a5, a6, a7});
}
inline expr expr::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5,
expr const & a6, expr const & a7, expr const & a8) const {
return mk_app({*this, a1, a2, a3, a4, a5, a6, a7, a8});
}
// =======================================
// =======================================
// Casting (these functions are only needed for low-level code)
inline expr_var * to_var(expr_cell * e) { lean_assert(is_var(e)); return static_cast<expr_var*>(e); }
inline expr_const * to_constant(expr_cell * e) { lean_assert(is_constant(e)); return static_cast<expr_const*>(e); }
inline expr_dep_pair * to_pair(expr_cell * e) { lean_assert(is_dep_pair(e)); return static_cast<expr_dep_pair*>(e); }
inline expr_proj * to_proj(expr_cell * e) { lean_assert(is_proj(e)); return static_cast<expr_proj*>(e); }
inline expr_app * to_app(expr_cell * e) { lean_assert(is_app(e)); return static_cast<expr_app*>(e); }
inline expr_abstraction * to_abstraction(expr_cell * e) { lean_assert(is_abstraction(e)); return static_cast<expr_abstraction*>(e); }
inline expr_lambda * to_lambda(expr_cell * e) { lean_assert(is_lambda(e)); return static_cast<expr_lambda*>(e); }
inline expr_pi * to_pi(expr_cell * e) { lean_assert(is_pi(e)); return static_cast<expr_pi*>(e); }
inline expr_sigma * to_sigma(expr_cell * e) { lean_assert(is_sigma(e)); return static_cast<expr_sigma*>(e); }
inline expr_type * to_type(expr_cell * e) { lean_assert(is_type(e)); return static_cast<expr_type*>(e); }
inline expr_let * to_let(expr_cell * e) { lean_assert(is_let(e)); return static_cast<expr_let*>(e); }
inline expr_heq * to_heq(expr_cell * e) { lean_assert(is_heq(e)); return static_cast<expr_heq*>(e); }
inline expr_metavar * to_metavar(expr_cell * e) { lean_assert(is_metavar(e)); return static_cast<expr_metavar*>(e); }
inline expr_var * to_var(expr_cell * e) { lean_assert(is_var(e)); return static_cast<expr_var*>(e); }
inline expr_const * to_constant(expr_cell * e) { lean_assert(is_constant(e)); return static_cast<expr_const*>(e); }
inline expr_dep_pair * to_pair(expr_cell * e) { lean_assert(is_dep_pair(e)); return static_cast<expr_dep_pair*>(e); }
inline expr_proj * to_proj(expr_cell * e) { lean_assert(is_proj(e)); return static_cast<expr_proj*>(e); }
inline expr_app * to_app(expr_cell * e) { lean_assert(is_app(e)); return static_cast<expr_app*>(e); }
inline expr_binder * to_binder(expr_cell * e) { lean_assert(is_binder(e)); return static_cast<expr_binder*>(e); }
inline expr_let * to_let(expr_cell * e) { lean_assert(is_let(e)); return static_cast<expr_let*>(e); }
inline expr_sort * to_sort(expr_cell * e) { lean_assert(is_sort(e)); return static_cast<expr_sort*>(e); }
inline expr_meta_local * to_meta_local(expr_cell * e) { lean_assert(is_meta_local(e)); return static_cast<expr_meta_local*>(e); }
inline expr_meta_local * to_local(expr_cell * e) { lean_assert(is_local(e)); return static_cast<expr_meta_local*>(e); }
inline expr_meta_local * to_metavar(expr_cell * e) { lean_assert(is_metavar(e)); return static_cast<expr_meta_local*>(e); }
inline expr_var * to_var(expr const & e) { return to_var(e.raw()); }
inline expr_const * to_constant(expr const & e) { return to_constant(e.raw()); }
inline expr_dep_pair * to_pair(expr const & e) { return to_pair(e.raw()); }
inline expr_proj * to_proj(expr const & e) { return to_proj(e.raw()); }
inline expr_app * to_app(expr const & e) { return to_app(e.raw()); }
inline expr_abstraction * to_abstraction(expr const & e) { return to_abstraction(e.raw()); }
inline expr_lambda * to_lambda(expr const & e) { return to_lambda(e.raw()); }
inline expr_pi * to_pi(expr const & e) { return to_pi(e.raw()); }
inline expr_sigma * to_sigma(expr const & e) { return to_sigma(e.raw()); }
inline expr_binder * to_binder(expr const & e) { return to_binder(e.raw()); }
inline expr_let * to_let(expr const & e) { return to_let(e.raw()); }
inline expr_type * to_type(expr const & e) { return to_type(e.raw()); }
inline expr_heq * to_heq(expr const & e) { return to_heq(e.raw()); }
inline expr_metavar * to_metavar(expr const & e) { return to_metavar(e.raw()); }
inline expr_sort * to_sort(expr const & e) { return to_sort(e.raw()); }
inline expr_meta_local * to_meta_local(expr const & e) { return to_meta_local(e.raw()); }
inline expr_meta_local * to_metavar(expr const & e) { return to_metavar(e.raw()); }
inline expr_meta_local * to_local(expr const & e) { return to_local(e.raw()); }
// =======================================
#if 0
// =======================================
// Accessors
inline unsigned get_rc(expr_cell * e) { return e->get_rc(); }
@ -810,4 +714,5 @@ inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d);
// =======================================
std::ostream & operator<<(std::ostream & out, expr const & e);
#endif
}

39
src/kernel/level.h
View file

@ -129,5 +129,44 @@ inline deserializer & operator>>(deserializer & d, level & l) { l = read_level(d
format pp(level l, bool unicode, unsigned indent);
/** \brief Pretty print the given level expression using the given configuration options. */
format pp(level const & l, options const & opts = options());
/**
\brief Auxiliary class used to manage universe constraints.
*/
class universe_context {
struct imp;
std::unique_ptr<imp> m_ptr;
public:
universe_context();
universe_context(universe_context const & s);
~universe_context();
/**
\brief Add the universe level constraint l1 <= l2.
*/
void add_le(level const & l1, level const & l2);
/**
\brief Quick check wether l1 <= l2. No backtracking search is performed.
If the result is true, then l1 <= l2 is implied. The result is false,
if we could not establish that.
*/
bool is_implied_cheap(level const & l1, level const & l2) const;
/**
\brief Expensive l1 <= l2 test. It performs a backtracking search.
*/
bool is_implied(level const & l1, level const & l2);
/**
\brief Create a backtracking point.
*/
void push();
/**
\brief Backtrack.
*/
void pop(unsigned num_scopes);
};
}
void print(lean::level const & l);