refactor(kernel): justification objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
50300126a5
commit
2a73389ed3
6 changed files with 314 additions and 118 deletions
|
|
@ -2,10 +2,10 @@ add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
|
|||
for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
|
||||
instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp
|
||||
object.cpp environment.cpp replace_visitor.cpp io_state.cpp
|
||||
normalizer.cpp
|
||||
# type_checker.cpp kernel.cpp
|
||||
# justification.cpp unification_constraint.cpp
|
||||
# type_checker_justification.cpp pos_info_provider.cpp
|
||||
normalizer.cpp justification.cpp pos_info_provider.cpp
|
||||
# type_checker.cpp
|
||||
# unification_constraint.cpp
|
||||
# type_checker_justification.cpp
|
||||
)
|
||||
|
||||
target_link_libraries(kernel ${LEAN_LIBS})
|
||||
|
|
|
|||
|
|
@ -6,76 +6,232 @@ Author: Leonardo de Moura
|
|||
*/
|
||||
#include <vector>
|
||||
#include "util/buffer.h"
|
||||
#include "util/int64.h"
|
||||
#include "kernel/justification.h"
|
||||
#include "kernel/metavar.h"
|
||||
|
||||
namespace lean {
|
||||
void justification_cell::add_pos_info(format & r, optional<expr> const & e, pos_info_provider const * p) {
|
||||
format to_pos(optional<expr> const & e, pos_info_provider const * p) {
|
||||
if (!p || !e)
|
||||
return;
|
||||
return format();
|
||||
format f = p->pp(*e);
|
||||
if (!f)
|
||||
return;
|
||||
r += f;
|
||||
r += space();
|
||||
return format();
|
||||
return f + space();
|
||||
}
|
||||
|
||||
format justification_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children,
|
||||
optional<metavar_env> const & menv) const {
|
||||
format r;
|
||||
add_pos_info(r, get_main_expr(), p);
|
||||
r += pp_header(fmt, opts, menv);
|
||||
if (display_children) {
|
||||
buffer<justification_cell *> children;
|
||||
get_children(children);
|
||||
unsigned indent = get_pp_indent(opts);
|
||||
for (justification_cell * child : children) {
|
||||
r += nest(indent, compose(line(), child->pp(fmt, opts, p, display_children, menv)));
|
||||
typedef uint64 approx_set;
|
||||
static approx_set mk_empty_set() { return 0; }
|
||||
static approx_set mk_union(approx_set s1, approx_set s2) { return s1 | s2; }
|
||||
static approx_set mk_intersection(approx_set s1, approx_set s2) { return s1 & s2; }
|
||||
static approx_set mk_singleton(unsigned i) { return static_cast<uint64>(1) << (i % 64); }
|
||||
static approx_set may_contain(approx_set s, unsigned i) { return mk_intersection(s, mk_singleton(i)) != 0ull; }
|
||||
|
||||
enum class justification_kind { Asserted, Composite, ExtComposite, Assumption, ExtAssumption };
|
||||
|
||||
approx_set get_approx_assumption_set(justification const & j);
|
||||
|
||||
struct justification_cell {
|
||||
MK_LEAN_RC();
|
||||
justification_kind m_kind;
|
||||
void dealloc();
|
||||
justification_cell(justification_kind k):m_rc(0), m_kind(k) {}
|
||||
bool is_asserted() const { return m_kind == justification_kind::Asserted; }
|
||||
bool is_assumption() const { return m_kind == justification_kind::Assumption || m_kind == justification_kind::ExtAssumption; }
|
||||
bool is_composite() const { return m_kind == justification_kind::Composite || m_kind == justification_kind::ExtComposite; }
|
||||
bool is_ext_assumption() const { return m_kind == justification_kind::ExtAssumption; }
|
||||
bool is_ext_composite() const { return m_kind == justification_kind::ExtComposite; }
|
||||
};
|
||||
|
||||
struct asserted_cell : public justification_cell {
|
||||
pp_jst_fn m_fn;
|
||||
optional<expr> m_expr;
|
||||
asserted_cell(pp_jst_fn const & fn, optional<expr> const & e):
|
||||
justification_cell(justification_kind::Asserted),
|
||||
m_fn(fn), m_expr(e) {}
|
||||
};
|
||||
|
||||
struct composite_cell : public justification_cell {
|
||||
approx_set m_assumption_set; // approximated set of assumptions contained in child1 and child2
|
||||
justification m_child[2];
|
||||
composite_cell(justification_kind k, justification const & j1, justification const & j2):
|
||||
justification_cell(k) {
|
||||
m_child[0] = j1;
|
||||
m_child[1] = j2;
|
||||
m_assumption_set = mk_union(get_approx_assumption_set(j1), get_approx_assumption_set(j2));
|
||||
}
|
||||
composite_cell(justification const & j1, justification const & j2):
|
||||
composite_cell(justification_kind::Composite, j1, j2) {}
|
||||
};
|
||||
|
||||
struct ext_composite_cell : public composite_cell {
|
||||
pp_jst_fn m_fn;
|
||||
optional<expr> m_expr;
|
||||
ext_composite_cell(justification const & j1, justification const & j2, pp_jst_fn const & fn, optional<expr> const & e):
|
||||
composite_cell(justification_kind::ExtComposite, j1, j2),
|
||||
m_fn(fn),
|
||||
m_expr(e) {}
|
||||
};
|
||||
|
||||
struct assumption_cell : public justification_cell {
|
||||
unsigned m_idx;
|
||||
assumption_cell(justification_kind k, unsigned idx):
|
||||
justification_cell(k), m_idx(idx) {}
|
||||
assumption_cell(unsigned idx):
|
||||
assumption_cell(justification_kind::Assumption, idx) {}
|
||||
};
|
||||
|
||||
struct ext_assumption_cell : public assumption_cell {
|
||||
pp_jst_fn m_fn;
|
||||
optional<expr> m_expr;
|
||||
ext_assumption_cell(unsigned idx, pp_jst_fn const & fn, optional<expr> const & e):
|
||||
assumption_cell(justification_kind::ExtAssumption, idx),
|
||||
m_fn(fn),
|
||||
m_expr(e) {}
|
||||
};
|
||||
|
||||
asserted_cell * to_asserted(justification_cell * j) { lean_assert(j && j->is_asserted()); return static_cast<asserted_cell*>(j); }
|
||||
assumption_cell * to_assumption(justification_cell * j) { lean_assert(j && j->is_assumption()); return static_cast<assumption_cell*>(j); }
|
||||
ext_assumption_cell * to_ext_assumption(justification_cell * j) { lean_assert(j && j->is_ext_assumption()); return static_cast<ext_assumption_cell*>(j); }
|
||||
composite_cell * to_composite(justification_cell * j) { lean_assert(j && j->is_composite()); return static_cast<composite_cell*>(j); }
|
||||
ext_composite_cell * to_ext_composite(justification_cell * j) { lean_assert(j && j->is_composite()); return static_cast<ext_composite_cell*>(j); }
|
||||
|
||||
approx_set get_approx_assumption_set(justification const & j) {
|
||||
justification_cell * it = j.raw();
|
||||
if (!it)
|
||||
return mk_empty_set();
|
||||
switch (it->m_kind) {
|
||||
case justification_kind::Asserted:
|
||||
return mk_empty_set();
|
||||
case justification_kind::Assumption: case justification_kind::ExtAssumption:
|
||||
return mk_singleton(to_assumption(it)->m_idx);
|
||||
case justification_kind::Composite: case justification_kind::ExtComposite:
|
||||
return to_composite(it)->m_assumption_set;
|
||||
}
|
||||
return r;
|
||||
lean_unreachable(); // LCOV_EXCL_LINE
|
||||
}
|
||||
|
||||
bool justification::has_children() const {
|
||||
buffer<justification_cell *> r;
|
||||
get_children(r);
|
||||
return !r.empty();
|
||||
void justification_cell::dealloc() {
|
||||
switch (m_kind) {
|
||||
case justification_kind::Asserted: delete to_asserted(this); break;
|
||||
case justification_kind::Assumption: delete to_assumption(this); break;
|
||||
case justification_kind::ExtAssumption: delete to_ext_assumption(this); break;
|
||||
case justification_kind::Composite: delete to_composite(this); break;
|
||||
case justification_kind::ExtComposite: delete to_ext_composite(this); break;
|
||||
}
|
||||
format justification::pp(formatter const & fmt, options const & opts, pos_info_provider const * p,
|
||||
bool display_children, optional<metavar_env> const & menv) const {
|
||||
lean_assert(m_ptr);
|
||||
return m_ptr->pp(fmt, opts, p, display_children, menv);
|
||||
}
|
||||
format justification::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const {
|
||||
lean_assert(m_ptr);
|
||||
return m_ptr->pp(fmt, opts, p, display_children, optional<metavar_env>());
|
||||
}
|
||||
|
||||
assumption_justification::assumption_justification(unsigned idx):m_idx(idx) {}
|
||||
void assumption_justification::get_children(buffer<justification_cell*> &) const {}
|
||||
optional<expr> assumption_justification::get_main_expr() const { return none_expr(); }
|
||||
format assumption_justification::pp_header(formatter const &, options const &, optional<metavar_env> const &) const {
|
||||
return format{format("Assumption"), space(), format(m_idx)};
|
||||
}
|
||||
|
||||
|
||||
bool depends_on(justification const & t, justification const & d) {
|
||||
bool depends_on(justification const & j, unsigned i) {
|
||||
if (!may_contain(get_approx_assumption_set(j), i))
|
||||
return false;
|
||||
buffer<justification_cell *> todo;
|
||||
buffer<justification_cell *> children;
|
||||
todo.push_back(t.raw());
|
||||
todo.push_back(j.raw());
|
||||
while (!todo.empty()) {
|
||||
justification_cell * curr = todo.back();
|
||||
todo.pop_back();
|
||||
if (curr == d.raw()) {
|
||||
switch (curr->m_kind) {
|
||||
case justification_kind::Asserted:
|
||||
break;
|
||||
case justification_kind::Assumption: case justification_kind::ExtAssumption:
|
||||
if (to_assumption(curr)->m_idx == i)
|
||||
return true;
|
||||
} else {
|
||||
children.clear();
|
||||
curr->get_children(children);
|
||||
for (justification_cell * child : children) {
|
||||
todo.push_back(child);
|
||||
break;
|
||||
case justification_kind::Composite: case justification_kind::ExtComposite:
|
||||
for (unsigned i = 0; i < 2; i++) {
|
||||
justification c = to_composite(curr)->m_child[i];
|
||||
if (may_contain(get_approx_assumption_set(c), i))
|
||||
todo.push_back(c.raw());
|
||||
}
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
justification const & composite_child1(justification const & j) {
|
||||
lean_assert(j.is_composite());
|
||||
return to_composite(j.raw())->m_child[0];
|
||||
}
|
||||
|
||||
justification const & composite_child2(justification const & j) {
|
||||
lean_assert(j.is_composite());
|
||||
return to_composite(j.raw())->m_child[0];
|
||||
}
|
||||
|
||||
unsigned assumption_idx(justification const & j) {
|
||||
lean_assert(j.is_assumption());
|
||||
return to_assumption(j.raw())->m_idx;
|
||||
}
|
||||
|
||||
justification::justification():m_ptr(nullptr) {}
|
||||
justification::justification(justification_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
||||
justification::justification(justification const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
||||
justification::justification(justification && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
|
||||
justification::~justification() { if (m_ptr) m_ptr->dec_ref(); }
|
||||
bool justification::is_none() const { return m_ptr == nullptr; }
|
||||
bool justification::is_asserted() const { return m_ptr && m_ptr->is_asserted(); }
|
||||
bool justification::is_assumption() const { return m_ptr && m_ptr->is_assumption(); }
|
||||
bool justification::is_composite() const { return m_ptr && m_ptr->is_composite(); }
|
||||
justification & justification::operator=(justification const & s) { LEAN_COPY_REF(s); }
|
||||
justification & justification::operator=(justification && s) { LEAN_MOVE_REF(s); }
|
||||
optional<expr> justification::get_main_expr() const {
|
||||
justification_cell * it = m_ptr;
|
||||
while (true) {
|
||||
if (!it)
|
||||
return none_expr();
|
||||
switch (it->m_kind) {
|
||||
case justification_kind::Asserted:
|
||||
return to_asserted(it)->m_expr;
|
||||
case justification_kind::ExtAssumption:
|
||||
return to_ext_assumption(it)->m_expr;
|
||||
case justification_kind::ExtComposite:
|
||||
return to_ext_composite(it)->m_expr;
|
||||
case justification_kind::Assumption:
|
||||
return none_expr();
|
||||
case justification_kind::Composite:
|
||||
it = to_composite(it)->m_child[0].raw();
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
format justification::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & s) {
|
||||
justification_cell * it = m_ptr;
|
||||
while (true) {
|
||||
if (!it)
|
||||
return format();
|
||||
switch (it->m_kind) {
|
||||
case justification_kind::Asserted:
|
||||
return to_asserted(it)->m_fn(fmt, opts, p, s);
|
||||
case justification_kind::ExtAssumption:
|
||||
return to_ext_assumption(it)->m_fn(fmt, opts, p, s);
|
||||
case justification_kind::ExtComposite:
|
||||
return to_ext_composite(it)->m_fn(fmt, opts, p, s);
|
||||
case justification_kind::Assumption:
|
||||
return format(format("Assumption "), format(to_assumption(it)->m_idx));
|
||||
case justification_kind::Composite:
|
||||
it = to_composite(it)->m_child[0].raw();
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
justification mk_composite(justification const & j1, justification const & j2, pp_jst_fn const & fn, optional<expr> const & s) {
|
||||
return justification(new ext_composite_cell(j1, j2, fn, s));
|
||||
}
|
||||
justification mk_composite1(justification const & j1, justification const & j2) {
|
||||
return justification(new composite_cell(j1, j2));
|
||||
}
|
||||
justification mk_assumption_justification(unsigned idx, pp_jst_fn const & fn, optional<expr> const & s) {
|
||||
return justification(new ext_assumption_cell(idx, fn, s));
|
||||
}
|
||||
justification mk_assumption_justification(unsigned idx) {
|
||||
return justification(new assumption_cell(idx));
|
||||
}
|
||||
justification mk_justification(pp_jst_fn const & fn, optional<expr> const & s) {
|
||||
return justification(new asserted_cell(fn, s));
|
||||
}
|
||||
justification mk_justification(pp_jst_sfn const & fn, optional<expr> const & s) {
|
||||
return mk_justification([=](formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & subst) {
|
||||
return compose(to_pos(s, p), fn(fmt, opts, subst));
|
||||
}, s);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -15,87 +15,121 @@ Author: Leonardo de Moura
|
|||
#include "kernel/pos_info_provider.h"
|
||||
|
||||
namespace lean {
|
||||
class metavar_env;
|
||||
class justification;
|
||||
/**
|
||||
\brief Base class used to represent justification objects.
|
||||
These objects are used to justification the execution of different engines in Lean.
|
||||
The justifications may help users understanding why something did not work.
|
||||
The justifications are particularly important for the elaborator.
|
||||
*/
|
||||
class justification_cell {
|
||||
MK_LEAN_RC();
|
||||
void dealloc() { delete this; }
|
||||
protected:
|
||||
static void add_pos_info(format & r, optional<expr> const & e, pos_info_provider const * p);
|
||||
public:
|
||||
justification_cell():m_rc(0) {}
|
||||
virtual ~justification_cell() {}
|
||||
virtual format pp_header(formatter const & fmt, options const & opts, optional<metavar_env> const & menv) const = 0;
|
||||
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p,
|
||||
bool display_children, optional<metavar_env> const & menv) const;
|
||||
virtual void get_children(buffer<justification_cell*> & r) const = 0;
|
||||
virtual optional<expr> get_main_expr() const { return none_expr(); }
|
||||
bool is_shared() const { return get_rc() > 1; }
|
||||
};
|
||||
class substitution;
|
||||
struct justification_cell;
|
||||
|
||||
/**
|
||||
\brief Base class for justification objects used to justify case-splits.
|
||||
\brief When a set of constraints cannot be solved, we must print some "error" message to the user.
|
||||
The pp_jst_fn is a generic funciton that produces these messages. We can associate these functions
|
||||
to justification objects.
|
||||
*/
|
||||
class assumption_justification : public justification_cell {
|
||||
unsigned m_idx;
|
||||
public:
|
||||
assumption_justification(unsigned idx);
|
||||
virtual void get_children(buffer<justification_cell*> &) const;
|
||||
virtual optional<expr> get_main_expr() const;
|
||||
virtual format pp_header(formatter const &, options const &, optional<metavar_env> const & menv) const;
|
||||
};
|
||||
typedef std::function<format(formatter const &, options const &, pos_info_provider const *, substitution const &)> pp_jst_fn;
|
||||
|
||||
/**
|
||||
\brief Smart pointer for justification_cell's
|
||||
\brief Objects used to justify unification (and level) constraints and metavariable assignments.
|
||||
|
||||
There are 4 basic kinds of justification:
|
||||
- None: the null justification.
|
||||
- Asserted: a justification produced by the type checker.
|
||||
- Assumption: for case-splits inside the elaborator and other constraint solvers.
|
||||
- Composite: the combination of two other justification objects.
|
||||
|
||||
A composite justification is used, for example, to justify a constraint produced by
|
||||
replacing a metavariable ?M by its assignment in a constraint C.
|
||||
*/
|
||||
class justification {
|
||||
justification_cell * m_ptr;
|
||||
justification(justification_cell * ptr);
|
||||
public:
|
||||
justification():m_ptr(nullptr) {}
|
||||
justification(justification_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
||||
justification(justification const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
|
||||
justification(justification && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
|
||||
~justification() { if (m_ptr) m_ptr->dec_ref(); }
|
||||
|
||||
explicit operator bool() const { return m_ptr != nullptr; }
|
||||
|
||||
justification_cell * raw() const { return m_ptr; }
|
||||
justification();
|
||||
justification(justification const & s);
|
||||
justification(justification && s);
|
||||
~justification();
|
||||
|
||||
friend void swap(justification & a, justification & b) { std::swap(a.m_ptr, b.m_ptr); }
|
||||
|
||||
justification & operator=(justification const & s) { LEAN_COPY_REF(s); }
|
||||
justification & operator=(justification && s) { LEAN_MOVE_REF(s); }
|
||||
format pp(formatter const & fmt, options const & opts, pos_info_provider const * p,
|
||||
bool display_children, optional<metavar_env> const & menv) const;
|
||||
format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool display_children = true) const;
|
||||
optional<expr> get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : none_expr(); }
|
||||
void get_children(buffer<justification_cell*> & r) const { if (m_ptr) m_ptr->get_children(r); }
|
||||
bool has_children() const;
|
||||
bool is_none() const;
|
||||
bool is_asserted() const;
|
||||
bool is_assumption() const;
|
||||
bool is_composite() const;
|
||||
|
||||
justification_cell * raw() const { return m_ptr; }
|
||||
|
||||
justification & operator=(justification const & s);
|
||||
justification & operator=(justification && s);
|
||||
/**
|
||||
\brief Convert this justification into a format object. This method is usually used to report
|
||||
"error" messages to users.
|
||||
*/
|
||||
format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & s);
|
||||
/**
|
||||
\brief Return an expression associated with the justification object.
|
||||
*/
|
||||
optional<expr> get_main_expr() const;
|
||||
|
||||
friend justification mk_composite(justification const & j1, justification const & j2, pp_jst_fn const & fn, optional<expr> const & s);
|
||||
friend justification mk_composite1(justification const & j1, justification const & j2);
|
||||
friend justification mk_assumption_justification(unsigned idx, pp_jst_fn const & fn, optional<expr> const & s);
|
||||
friend justification mk_assumption_justification(unsigned idx);
|
||||
friend justification mk_justification(pp_jst_fn const & fn, optional<expr> const & s);
|
||||
};
|
||||
|
||||
inline justification mk_assumption_justification(unsigned idx) { return justification(new assumption_justification(idx)); }
|
||||
/**
|
||||
\brief Simplifer version of pp_jst_fn
|
||||
*/
|
||||
typedef std::function<format(formatter const &, options const &, substitution const &)> pp_jst_sfn;
|
||||
|
||||
/** \brief Return a format object containing position information for the given expression (if available) */
|
||||
format to_pos(optional<expr> const & e, pos_info_provider const * p);
|
||||
|
||||
/**
|
||||
\brief Return true iff \c t depends on \c d.
|
||||
That is \c t is a descendant of \c d.
|
||||
\brief Combine the two given justifications into a new justification object, and use
|
||||
the given function to convert the justification into a format object.
|
||||
*/
|
||||
bool depends_on(justification const & t, justification const & d);
|
||||
justification mk_composite(justification const & j1, justification const & j2, pp_jst_fn const & fn, optional<expr> const & s);
|
||||
/**
|
||||
\brief Similar to \c mk_composite, but uses \c j1.pp to convert the
|
||||
resulting justification into a format object.
|
||||
*/
|
||||
justification mk_composite1(justification const & j1, justification const & j2);
|
||||
/**
|
||||
\brief Alias for \c mk_composite1
|
||||
*/
|
||||
justification mk_substitution_justification(justification const & j1, justification const & j2);
|
||||
/**
|
||||
\brief Create a "case-split" justification with the given \c idx.
|
||||
*/
|
||||
justification mk_assumption_justification(unsigned idx, pp_jst_fn const & fn, optional<expr> const & s);
|
||||
/**
|
||||
\brief Similar to the previous function, but fn just returns the format object "assumption idx", and s is the none.
|
||||
*/
|
||||
justification mk_assumption_justification(unsigned idx);
|
||||
/**
|
||||
\brief Create a justification for constraints produced by the type checker.
|
||||
*/
|
||||
justification mk_justification(pp_jst_fn const & fn, optional<expr> const & s);
|
||||
/**
|
||||
\brief Create a justification for constraints produced by the type checker.
|
||||
It is similar to the previous function, but the position of \c s will be automatically included.
|
||||
*/
|
||||
justification mk_justification(pp_jst_sfn const & fn, optional<expr> const & s);
|
||||
|
||||
/** \brief Add \c t to \c r */
|
||||
inline void push_back(buffer<justification_cell*> & r, justification const & t) {
|
||||
if (t) r.push_back(t.raw());
|
||||
}
|
||||
/**
|
||||
\brief Return the first child of a composite justification.
|
||||
\pre j.is_composite()
|
||||
*/
|
||||
justification const & composite_child1(justification const & j);
|
||||
/**
|
||||
\brief Return the second child of a composite justification.
|
||||
\pre j.is_composite()
|
||||
*/
|
||||
justification const & composite_child2(justification const & j);
|
||||
/**
|
||||
\brief Return the index of an assumption justification.
|
||||
\pre j.is_assumption()
|
||||
*/
|
||||
unsigned assumption_idx(justification const & j);
|
||||
|
||||
/** \brief Add justifications in the collection \c s into r. */
|
||||
template<typename T>
|
||||
void append(buffer<justification_cell*> & r, T const & s) {
|
||||
for (auto t : s)
|
||||
push_back(r, t);
|
||||
}
|
||||
/** \brief Return true iff \c j depends on the assumption with index \c i. */
|
||||
bool depends_on(justification const & j, unsigned i);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ Author: Leonardo de Moura
|
|||
|
||||
namespace lean {
|
||||
/**
|
||||
\brief Abstract class for providing expression position information (line number and position).
|
||||
\brief Abstract class for providing expression position information (line number and column).
|
||||
*/
|
||||
class pos_info_provider {
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -419,6 +419,7 @@ int main() {
|
|||
std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n";
|
||||
std::cout << "sizeof(optional<expr>): " << sizeof(optional<expr>) << "\n";
|
||||
std::cout << "sizeof(optional<sexpr>): " << sizeof(optional<sexpr>) << "\n";
|
||||
std::cout << "sizeof(std::function): " << sizeof(std::function<expr(expr const &, optional<expr> const &)>) << "\n";
|
||||
std::cout << "done" << "\n";
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -116,11 +116,16 @@ static void tst4() {
|
|||
lean_assert_eq(s.str(), "() (foo bar) nil \"test\" (100 1/2)");
|
||||
}
|
||||
|
||||
static void tst5() {
|
||||
std::cout << "{" << format() << "}" << "\n";
|
||||
}
|
||||
|
||||
int main() {
|
||||
save_stack_info();
|
||||
tst1();
|
||||
tst2();
|
||||
tst3();
|
||||
tst4();
|
||||
tst5();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue