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

refactor(kernel): rename trace to justification

Browse source 
Motivations:

- We have been writing several comments of the form "... trace/justification..." and "this trace object justify ...".
- Avoid confusion with util/trace.h

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-23 13:42:14 -07:00
parent 8e1a75ce1c
commit 13531b7d3e
22 changed files with 859 additions and 859 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
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 trace.cpp
type_checker.cpp builtin.cpp occurs.cpp metavar.cpp justification.cpp
unification_constraint.cpp printer.cpp formatter.cpp
kernel_exception.cpp type_checker_trace.cpp pos_info_provider.cpp)
kernel_exception.cpp type_checker_justification.cpp pos_info_provider.cpp)
target_link_libraries(kernel ${LEAN_LIBS})

26
src/kernel/trace.cpp → src/kernel/justification.cpp
View file

@ -6,10 +6,10 @@ Author: Leonardo de Moura
*/
#include <set>
#include "util/buffer.h"
#include "kernel/trace.h"
#include "kernel/justification.h"
namespace lean {
void trace_cell::add_pos_info(format & r, expr const & e, pos_info_provider const * p) {
void justification_cell::add_pos_info(format & r, expr const & e, pos_info_provider const * p) {
if (!p || !e)
return;
format f = p->pp(e);
@ -19,41 +19,41 @@ void trace_cell::add_pos_info(format & r, expr const & e, pos_info_provider cons
r += space();
}
format trace_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const {
format justification_cell::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const {
format r;
add_pos_info(r, get_main_expr(), p);
r += pp_header(fmt, opts);
if (display_children) {
buffer<trace_cell *> children;
buffer<justification_cell *> children;
get_children(children);
unsigned indent = get_pp_indent(opts);
for (trace_cell * child : children) {
for (justification_cell * child : children) {
r += nest(indent, compose(line(), child->pp(fmt, opts, p, display_children)));
}
}
return r;
}
bool trace::has_children() const {
buffer<trace_cell *> r;
bool justification::has_children() const {
buffer<justification_cell *> r;
get_children(r);
return !r.empty();
}
bool depends_on(trace const & t, trace const & d) {
buffer<trace_cell *> todo;
std::set<trace_cell *> visited;
buffer<trace_cell *> children;
bool depends_on(justification const & t, justification const & d) {
buffer<justification_cell *> todo;
std::set<justification_cell *> visited;
buffer<justification_cell *> children;
todo.push_back(t.raw());
while (!todo.empty()) {
trace_cell * curr = todo.back();
justification_cell * curr = todo.back();
todo.pop_back();
if (curr == d.raw()) {
return true;
} else {
children.clear();
curr->get_children(children);
for (trace_cell * child : children) {
for (justification_cell * child : children) {
if (child->is_shared()) {
if (visited.find(child) == visited.end()) {
visited.insert(child);

46
src/kernel/trace.h → src/kernel/justification.h
View file

@ -15,54 +15,54 @@ Author: Leonardo de Moura
#include "kernel/pos_info_provider.h"
namespace lean {
class trace;
class justification;
/**
\brief Base class used to represent trace objects.
These objects are used to trace the execution of different engines in Lean.
The traces may help users understanding why something did not work.
The traces are particularly important for the elaborator.
\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 trace_cell {
class justification_cell {
MK_LEAN_RC();
void dealloc() { delete this; }
protected:
static void add_pos_info(format & r, expr const & e, pos_info_provider const * p);
public:
trace_cell():m_rc(0) {}
virtual ~trace_cell() {}
justification_cell():m_rc(0) {}
virtual ~justification_cell() {}
virtual format pp_header(formatter const & fmt, options const & opts) const = 0;
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
virtual void get_children(buffer<trace_cell*> & r) const = 0;
virtual void get_children(buffer<justification_cell*> & r) const = 0;
virtual expr const & get_main_expr() const { return expr::null(); }
bool is_shared() const { return get_rc() > 1; }
};
/**
\brief Smart pointer for trace_cell's
\brief Smart pointer for justification_cell's
*/
class trace {
trace_cell * m_ptr;
class justification {
justification_cell * m_ptr;
public:
trace():m_ptr(nullptr) {}
trace(trace_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
trace(trace const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
trace(trace && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~trace() { if (m_ptr) m_ptr->dec_ref(); }
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(); }
operator bool() const { return m_ptr != nullptr; }
trace_cell * raw() const { return m_ptr; }
justification_cell * raw() const { return m_ptr; }
friend void swap(trace & a, trace & b) { std::swap(a.m_ptr, b.m_ptr); }
friend void swap(justification & a, justification & b) { std::swap(a.m_ptr, b.m_ptr); }
trace & operator=(trace const & s) { LEAN_COPY_REF(trace, s); }
trace & operator=(trace && s) { LEAN_MOVE_REF(trace, s); }
justification & operator=(justification const & s) { LEAN_COPY_REF(justification, s); }
justification & operator=(justification && s) { LEAN_MOVE_REF(justification, s); }
format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool display_children = true) const {
lean_assert(m_ptr);
return m_ptr->pp(fmt, opts, p, display_children);
}
expr const & get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : expr::null(); }
void get_children(buffer<trace_cell*> & r) const { if (m_ptr) m_ptr->get_children(r); }
void get_children(buffer<justification_cell*> & r) const { if (m_ptr) m_ptr->get_children(r); }
bool has_children() const;
};
@ -70,5 +70,5 @@ public:
\brief Return true iff \c t depends on \c d.
That is \c t is a descendant of \c d.
*/
bool depends_on(trace const & t, trace const & d);
bool depends_on(justification const & t, justification const & d);
}

32
src/kernel/metavar.cpp
View file

@ -87,12 +87,12 @@ expr substitution::get_subst(expr const & m) const {
static name g_unique_name = name::mk_internal_unique_name();
void swap(metavar_env & a, metavar_env & b) {
swap(a.m_name_generator, b.m_name_generator);
swap(a.m_substitution, b.m_substitution);
swap(a.m_metavar_types, b.m_metavar_types);
swap(a.m_metavar_contexts, b.m_metavar_contexts);
swap(a.m_metavar_traces, b.m_metavar_traces);
std::swap(a.m_timestamp, b.m_timestamp);
swap(a.m_name_generator, b.m_name_generator);
swap(a.m_substitution, b.m_substitution);
swap(a.m_metavar_types, b.m_metavar_types);
swap(a.m_metavar_contexts, b.m_metavar_contexts);
swap(a.m_metavar_justifications, b.m_metavar_justifications);
std::swap(a.m_timestamp, b.m_timestamp);
}
void metavar_env::inc_timestamp() {
@ -173,17 +173,17 @@ bool metavar_env::has_type(expr const & m) const {
}
trace metavar_env::get_trace(expr const & m) const {
justification metavar_env::get_justification(expr const & m) const {
lean_assert(is_metavar(m));
return get_trace(metavar_name(m));
return get_justification(metavar_name(m));
}
trace metavar_env::get_trace(name const & m) const {
auto e = const_cast<metavar_env*>(this)->m_metavar_traces.splay_find(m);
justification metavar_env::get_justification(name const & m) const {
auto e = const_cast<metavar_env*>(this)->m_metavar_justifications.splay_find(m);
if (e) {
return e->second;
} else {
return trace();
return justification();
}
}
@ -196,18 +196,18 @@ bool metavar_env::is_assigned(expr const & m) const {
return is_assigned(metavar_name(m));
}
void metavar_env::assign(name const & m, expr const & t, trace const & tr) {
void metavar_env::assign(name const & m, expr const & t, justification const & j) {
lean_assert(!is_assigned(m));
inc_timestamp();
m_substitution.assign(m, t);
if (tr)
m_metavar_traces.insert(m, tr);
if (j)
m_metavar_justifications.insert(m, j);
}
void metavar_env::assign(expr const & m, expr const & t, trace const & tr) {
void metavar_env::assign(expr const & m, expr const & t, justification const & j) {
lean_assert(is_metavar(m));
lean_assert(!has_local_context(m));
assign(metavar_name(m), t, tr);
assign(metavar_name(m), t, j);
}
struct found_unassigned{};

30
src/kernel/metavar.h
View file

@ -10,7 +10,7 @@ Author: Leonardo de Moura
#include "util/name_generator.h"
#include "kernel/expr.h"
#include "kernel/context.h"
#include "kernel/trace.h"
#include "kernel/justification.h"
namespace lean {
/**
@ -89,16 +89,16 @@ void swap(substitution & s1, substitution & s2);
4- Collecting constraints
*/
class metavar_env {
typedef splay_map<name, expr, name_cmp> name2expr;
typedef splay_map<name, context, name_cmp> name2context;
typedef splay_map<name, trace, name_cmp> name2trace;
typedef splay_map<name, expr, name_cmp> name2expr;
typedef splay_map<name, context, name_cmp> name2context;
typedef splay_map<name, justification, name_cmp> name2justification;
name_generator m_name_generator;
substitution m_substitution;
name2expr m_metavar_types;
name2context m_metavar_contexts;
name2trace m_metavar_traces;
unsigned m_timestamp;
name_generator m_name_generator;
substitution m_substitution;
name2expr m_metavar_types;
name2context m_metavar_contexts;
name2justification m_metavar_justifications;
unsigned m_timestamp;
void inc_timestamp();
public:
@ -146,12 +146,12 @@ public:
bool has_type(name const & m) const;
/**
\brief Return the trace/justification for an assigned metavariable.
\brief Return the justification for an assigned metavariable.
\pre is_metavar(m)
\pre is_assigned(m)
*/
trace get_trace(expr const & m) const;
trace get_trace(name const & m) const;
justification get_justification(expr const & m) const;
justification get_justification(name const & m) const;
/**
@ -172,7 +172,7 @@ public:
\pre !is_assigned(m)
*/
void assign(name const & m, expr const & t, trace const & tr = trace());
void assign(name const & m, expr const & t, justification const & j = justification());
/**
\brief Assign metavariable \c m to \c t.
@ -181,7 +181,7 @@ public:
\pre !has_meta_context(m)
\pre !is_assigned(m)
*/
void assign(expr const & m, expr const & t, trace const & tr = trace());
void assign(expr const & m, expr const & t, justification const & j = justification());
/**
\brief Return the set of substitutions.

32
src/kernel/type_checker.cpp
View file

@ -13,7 +13,7 @@ Author: Leonardo de Moura
#include "kernel/instantiate.h"
#include "kernel/builtin.h"
#include "kernel/free_vars.h"
#include "kernel/type_checker_trace.h"
#include "kernel/type_checker_justification.h"
namespace lean {
static name g_x_name("x");
@ -55,8 +55,8 @@ class type_checker::imp {
expr A = m_menv->mk_metavar(ctx);
expr B = m_menv->mk_metavar(ctx);
expr p = mk_pi(g_x_name, A, B(Var(0)));
trace tr = mk_function_expected_trace(ctx, s);
m_uc->push_back(mk_eq_constraint(ctx, r, p, tr));
justification jst = mk_function_expected_justification(ctx, s);
m_uc->push_back(mk_eq_constraint(ctx, r, p, jst));
return p;
}
throw function_expected_exception(m_env, ctx, s);
@ -73,8 +73,8 @@ class type_checker::imp {
if (u == Bool)
return Type();
if (has_metavar(u) && m_menv) {
trace tr = mk_type_expected_trace(ctx, s);
m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, tr));
justification jst = mk_type_expected_justification(ctx, s);
m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, jst));
return u;
}
throw type_expected_exception(m_env, ctx, s);
@ -123,8 +123,8 @@ class type_checker::imp {
while (true) {
expr const & c = arg(e, i);
expr const & c_t = arg_types[i];
auto mk_trace = [&](){ return mk_app_type_match_trace(ctx, e, i); }; // thunk for creating trace object if needed
if (!is_convertible(c_t, abst_domain(f_t), ctx, mk_trace))
auto mk_justification = [&](){ return mk_app_type_match_justification(ctx, e, i); }; // thunk for creating justification object if needed
if (!is_convertible(c_t, abst_domain(f_t), ctx, mk_justification))
throw app_type_mismatch_exception(m_env, ctx, e, arg_types.size(), arg_types.data());
if (closed(abst_body(f_t)))
f_t = abst_body(f_t);
@ -169,9 +169,9 @@ class type_checker::imp {
r = mk_type(max(ty_level(t1), ty_level(t2)));
} else {
lean_assert(m_uc);
trace tr = mk_max_type_trace(ctx, e);
justification jst = mk_max_type_justification(ctx, e);
r = m_menv->mk_metavar(ctx);
m_uc->push_back(mk_max_constraint(ctx, t1, t2, r, tr));
m_uc->push_back(mk_max_constraint(ctx, t1, t2, r, jst));
}
break;
}
@ -180,8 +180,8 @@ class type_checker::imp {
if (let_type(e)) {
expr ty = infer_type_core(let_type(e), ctx);
check_type(ty, let_type(e), ctx); // check if it is really a type
auto mk_trace = [&](){ return mk_def_type_match_trace(ctx, let_name(e), let_value(e)); }; // thunk for creating trace object if needed
if (!is_convertible(lt, let_type(e), ctx, mk_trace))
auto mk_justification = [&](){ return mk_def_type_match_justification(ctx, let_name(e), let_value(e)); }; // thunk for creating justification object if needed
if (!is_convertible(lt, let_type(e), ctx, mk_justification))
throw def_type_mismatch_exception(m_env, ctx, let_name(e), let_type(e), let_value(e), lt);
}
{
@ -235,8 +235,8 @@ class type_checker::imp {
}
}
template<typename MkTrace>
bool is_convertible(expr const & given, expr const & expected, context const & ctx, MkTrace const & mk_trace) {
template<typename MkJustification>
bool is_convertible(expr const & given, expr const & expected, context const & ctx, MkJustification const & mk_justification) {
if (is_convertible_core(given, expected))
return true;
expr new_given = normalize(given, ctx);
@ -244,7 +244,7 @@ class type_checker::imp {
if (is_convertible_core(new_given, new_expected))
return true;
if (m_menv && (has_metavar(new_given) || has_metavar(new_expected))) {
m_uc->push_back(mk_convertible_constraint(ctx, new_given, new_expected, mk_trace()));
m_uc->push_back(mk_convertible_constraint(ctx, new_given, new_expected, mk_justification()));
return true;
}
return false;
@ -292,8 +292,8 @@ public:
bool is_convertible(expr const & t1, expr const & t2, context const & ctx) {
set_ctx(ctx);
set_menv(nullptr);
auto mk_trace = [](){ lean_unreachable(); return trace(); };
return is_convertible(t1, t2, ctx, mk_trace);
auto mk_justification = [](){ lean_unreachable(); return justification(); };
return is_convertible(t1, t2, ctx, mk_justification);
}
void check_type(expr const & e, context const & ctx) {

34
src/kernel/type_checker_trace.cpp → src/kernel/type_checker_justification.cpp
View file

@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/type_checker_trace.h"
#include "kernel/type_checker_justification.h"
namespace lean {
function_expected_trace_cell::~function_expected_trace_cell() {
function_expected_justification_cell::~function_expected_justification_cell() {
}
format function_expected_trace_cell::pp_header(formatter const & fmt, options const & opts) const {
format function_expected_justification_cell::pp_header(formatter const & fmt, options const & opts) const {
unsigned indent = get_pp_indent(opts);
format expr_fmt = fmt(m_ctx, m_app, false, opts);
format r;
@ -20,17 +20,17 @@ format function_expected_trace_cell::pp_header(formatter const & fmt, options co
return r;
}
void function_expected_trace_cell::get_children(buffer<trace_cell*> &) const {
void function_expected_justification_cell::get_children(buffer<justification_cell*> &) const {
}
expr const & function_expected_trace_cell::get_main_expr() const {
expr const & function_expected_justification_cell::get_main_expr() const {
return m_app;
}
app_type_match_trace_cell::~app_type_match_trace_cell() {
app_type_match_justification_cell::~app_type_match_justification_cell() {
}
format app_type_match_trace_cell::pp_header(formatter const & fmt, options const & opts) const {
format app_type_match_justification_cell::pp_header(formatter const & fmt, options const & opts) const {
unsigned indent = get_pp_indent(opts);
format r;
r += format("Type of argument ");
@ -48,17 +48,17 @@ format app_type_match_trace_cell::pp_header(formatter const & fmt, options const
return r;
}
void app_type_match_trace_cell::get_children(buffer<trace_cell*> &) const {
void app_type_match_justification_cell::get_children(buffer<justification_cell*> &) const {
}
expr const & app_type_match_trace_cell::get_main_expr() const {
expr const & app_type_match_justification_cell::get_main_expr() const {
return m_app;
}
type_expected_trace_cell::~type_expected_trace_cell() {
type_expected_justification_cell::~type_expected_justification_cell() {
}
format type_expected_trace_cell::pp_header(formatter const & fmt, options const & opts) const {
format type_expected_justification_cell::pp_header(formatter const & fmt, options const & opts) const {
unsigned indent = get_pp_indent(opts);
format expr_fmt = fmt(m_ctx, m_type, false, opts);
format r;
@ -67,17 +67,17 @@ format type_expected_trace_cell::pp_header(formatter const & fmt, options const
return r;
}
void type_expected_trace_cell::get_children(buffer<trace_cell*> &) const {
void type_expected_justification_cell::get_children(buffer<justification_cell*> &) const {
}
expr const & type_expected_trace_cell::get_main_expr() const {
expr const & type_expected_justification_cell::get_main_expr() const {
return m_type;
}
def_type_match_trace_cell::~def_type_match_trace_cell() {
def_type_match_justification_cell::~def_type_match_justification_cell() {
}
format def_type_match_trace_cell::pp_header(formatter const &, options const &) const {
format def_type_match_justification_cell::pp_header(formatter const &, options const &) const {
format r;
r += format("Type of definition '");
r += format(get_name());
@ -85,10 +85,10 @@ format def_type_match_trace_cell::pp_header(formatter const &, options const &)
return r;
}
void def_type_match_trace_cell::get_children(buffer<trace_cell*> &) const {
void def_type_match_justification_cell::get_children(buffer<justification_cell*> &) const {
}
expr const & def_type_match_trace_cell::get_main_expr() const {
expr const & def_type_match_justification_cell::get_main_expr() const {
return m_value;
}
}

128
src/kernel/type_checker_justification.h Normal file
View file

@ -0,0 +1,128 @@
/*
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/justification.h"
#include "kernel/expr.h"
#include "kernel/context.h"
namespace lean {
/**
\brief Justification produced by the type checker when the application \c m_app
is an application <tt>(f ...)</tt>, the type \c T of \c f contains metavariables, and
it is not clear whether it is a Pi or not. In this case, the type checker adds
the constraint
<tt>ctx |- T == Pi (x : ?A), ?B x</tt>
where, \c ?A and \c ?B are fresh metavariables.
This justification cell is used to justify the new constraint.
*/
class function_expected_justification_cell : public justification_cell {
context m_ctx;
expr m_app;
public:
function_expected_justification_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {}
virtual ~function_expected_justification_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual expr const & get_main_expr() const;
context const & get_context() const { return m_ctx; }
expr const & get_app() const { return m_app; }
};
/**
\brief Justification produced by the type checker for application argument type matching.
When checking an application <tt>(f a_1 ... a_i ...)</tt>, the type
\c T_inferred of \c a_i must be convertible to the expected type \c T_expected. If
\c T_expected or \c T_inferred contain metavariables, and it is not clear whether
\c T_inferred is convertible to \c T_expected, then the type checker adds the constraint
<tt>ctx |- T_inferred << T_expected</tt>
This justification cell is used to justify this constraint.
*/
class app_type_match_justification_cell : public justification_cell {
context m_ctx;
expr m_app;
unsigned m_i;
public:
app_type_match_justification_cell(context const & c, expr const & a, unsigned i):m_ctx(c), m_app(a), m_i(i) {}
virtual ~app_type_match_justification_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual expr const & get_main_expr() const;
context const & get_context() const { return m_ctx; }
expr const & get_app() const { return m_app; }
unsigned get_arg_pos() const { return m_i; }
};
/**
\brief Justification produced by the type checker when the type \c T of \c type must be of the form
<tt>Type l</tt>, and \c T constains metavariables, and it is not of this form.
The type checker adds the following constraint
<tt>ctx |- T << Type U</tt>
This justification cell is used to justify these constraints.
*/
class type_expected_justification_cell : public justification_cell {
context m_ctx;
expr m_type;
public:
type_expected_justification_cell(context const & c, expr const & t):m_ctx(c), m_type(t) {}
virtual ~type_expected_justification_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual expr const & get_main_expr() const;
context const & get_context() const { return m_ctx; }
expr const & get_type() const { return m_type; }
};
/**
\brief If \c type is of the form <tt>Pi x : A, B</tt>, where \c A has type \c T1 and \c B has type \c T2,
and \c T1 or \c T2 have metavariables, then the type checker adds the following constraint
<tt>ctx |- max(T1, T2) == ?T
where ?T is a new metavariable, and this justification cell is used to justify the new constraint.
*/
class max_type_justification_cell : public type_expected_justification_cell {
public:
max_type_justification_cell(context const & c, expr const & t):type_expected_justification_cell(c, t) {}
};
/**
\brief Justification produced by the type checker when checking whether the type \c T_inferred of \c value
is convertible to the expected type \c T_expected. If \c T_expected or \c T_inferred contain
metavariables, and it is not clear whether \c T_inferred is convertible to \c T_expected,
then the type checker adds the constraint
<tt>ctx |- T_inferred << T_expected</tt>
This justification cell is used to justify this constraint.
*/
class def_type_match_justification_cell : public justification_cell {
context m_ctx;
name m_name;
expr m_value;
public:
def_type_match_justification_cell(context const & c, name const & n, expr const & v):m_ctx(c), m_name(n), m_value(v) {}
virtual ~def_type_match_justification_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<justification_cell*> &) const;
virtual expr const & get_main_expr() const;
context const & get_context() const { return m_ctx; }
name const & get_name() const { return m_name; }
expr const & get_value() const { return m_value; }
};
inline justification mk_function_expected_justification(context const & ctx, expr const & app) { return justification(new function_expected_justification_cell(ctx, app)); }
inline justification mk_app_type_match_justification(context const & ctx, expr const & app, unsigned i) { return justification(new app_type_match_justification_cell(ctx, app, i)); }
inline justification mk_type_expected_justification(context const & ctx, expr const & type) { return justification(new type_expected_justification_cell(ctx, type)); }
inline justification mk_max_type_justification(context const & ctx, expr const & type) { return justification(new max_type_justification_cell(ctx, type)); }
inline justification mk_def_type_match_justification(context const & ctx, name const & n, expr const & v) { return justification(new def_type_match_justification_cell(ctx, n, v)); }
}

128
src/kernel/type_checker_trace.h
View file

@ -1,128 +0,0 @@
/*
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/trace.h"
#include "kernel/expr.h"
#include "kernel/context.h"
namespace lean {
/**
\brief Trace produced by the type checker when the application \c m_app
is an application <tt>(f ...)</tt>, the type \c T of \c f contains metavariables, and
it is not clear whether it is a Pi or not. In this case, the type checker adds
the constraint
<tt>ctx |- T == Pi (x : ?A), ?B x</tt>
where, \c ?A and \c ?B are fresh metavariables.
This trace cell is used to justify/trace the new constraint.
*/
class function_expected_trace_cell : public trace_cell {
context m_ctx;
expr m_app;
public:
function_expected_trace_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {}
virtual ~function_expected_trace_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<trace_cell*> &) const;
virtual expr const & get_main_expr() const;
context const & get_context() const { return m_ctx; }
expr const & get_app() const { return m_app; }
};
/**
\brief Trace produced by the type checker for application argument type matching.
When checking an application <tt>(f a_1 ... a_i ...)</tt>, the type
\c T_inferred of \c a_i must be convertible to the expected type \c T_expected. If
\c T_expected or \c T_inferred contain metavariables, and it is not clear whether
\c T_inferred is convertible to \c T_expected, then the type checker adds the constraint
<tt>ctx |- T_inferred << T_expected</tt>
This trace cell is used to justify this constraint.
*/
class app_type_match_trace_cell : public trace_cell {
context m_ctx;
expr m_app;
unsigned m_i;
public:
app_type_match_trace_cell(context const & c, expr const & a, unsigned i):m_ctx(c), m_app(a), m_i(i) {}
virtual ~app_type_match_trace_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<trace_cell*> &) const;
virtual expr const & get_main_expr() const;
context const & get_context() const { return m_ctx; }
expr const & get_app() const { return m_app; }
unsigned get_arg_pos() const { return m_i; }
};
/**
\brief Trace produced by the type checker when the type \c T of \c type must be of the form
<tt>Type l</tt>, and \c T constains metavariables, and it is not of this form.
The type checker adds the following constraint
<tt>ctx |- T << Type U</tt>
This trace cell is used to justify these constraints.
*/
class type_expected_trace_cell : public trace_cell {
context m_ctx;
expr m_type;
public:
type_expected_trace_cell(context const & c, expr const & t):m_ctx(c), m_type(t) {}
virtual ~type_expected_trace_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<trace_cell*> &) const;
virtual expr const & get_main_expr() const;
context const & get_context() const { return m_ctx; }
expr const & get_type() const { return m_type; }
};
/**
\brief If \c type is of the form <tt>Pi x : A, B</tt>, where \c A has type \c T1 and \c B has type \c T2,
and \c T1 or \c T2 have metavariables, then the type checker adds the following constraint
<tt>ctx |- max(T1, T2) == ?T
where ?T is a new metavariable, and this trace cell is used to justify the new constraint.
*/
class max_type_trace_cell : public type_expected_trace_cell {
public:
max_type_trace_cell(context const & c, expr const & t):type_expected_trace_cell(c, t) {}
};
/**
\brief Trace produced by the type checker when checking whether the type \c T_inferred of \c value
is convertible to the expected type \c T_expected. If \c T_expected or \c T_inferred contain
metavariables, and it is not clear whether \c T_inferred is convertible to \c T_expected,
then the type checker adds the constraint
<tt>ctx |- T_inferred << T_expected</tt>
This trace cell is used to justify this constraint.
*/
class def_type_match_trace_cell : public trace_cell {
context m_ctx;
name m_name;
expr m_value;
public:
def_type_match_trace_cell(context const & c, name const & n, expr const & v):m_ctx(c), m_name(n), m_value(v) {}
virtual ~def_type_match_trace_cell();
virtual format pp_header(formatter const & fmt, options const & opts) const;
virtual void get_children(buffer<trace_cell*> &) const;
virtual expr const & get_main_expr() const;
context const & get_context() const { return m_ctx; }
name const & get_name() const { return m_name; }
expr const & get_value() const { return m_value; }
};
inline trace mk_function_expected_trace(context const & ctx, expr const & app) { return trace(new function_expected_trace_cell(ctx, app)); }
inline trace mk_app_type_match_trace(context const & ctx, expr const & app, unsigned i) { return trace(new app_type_match_trace_cell(ctx, app, i)); }
inline trace mk_type_expected_trace(context const & ctx, expr const & type) { return trace(new type_expected_trace_cell(ctx, type)); }
inline trace mk_max_type_trace(context const & ctx, expr const & type) { return trace(new max_type_trace_cell(ctx, type)); }
inline trace mk_def_type_match_trace(context const & ctx, name const & n, expr const & v) { return trace(new def_type_match_trace_cell(ctx, n, v)); }
}

62
src/kernel/unification_constraint.cpp
View file

@ -7,8 +7,8 @@ Author: Leonardo de Moura
#include "kernel/unification_constraint.h"
namespace lean {
unification_constraint_cell::unification_constraint_cell(unification_constraint_kind k, context const & c, trace const & t):
m_kind(k), m_ctx(c), m_trace(t), m_rc(1) {
unification_constraint_cell::unification_constraint_cell(unification_constraint_kind k, context const & c, justification const & j):
m_kind(k), m_ctx(c), m_justification(j), m_rc(1) {
}
unification_constraint_cell::~unification_constraint_cell() {
}
@ -23,10 +23,10 @@ static format add_context(formatter const & fmt, options const & opts, context c
return group(format{ctx_fmt, space(), turnstile, line(), body});
}
static format add_trace(formatter const & fmt, options const & opts, format const & body, trace const & tr, pos_info_provider const * p, bool include_trace) {
if (tr && include_trace) {
static format add_justification(formatter const & fmt, options const & opts, format const & body, justification const & jst, pos_info_provider const * p, bool include_justification) {
if (jst && include_justification) {
unsigned indent = get_pp_indent(opts);
return format{body, line(), format("Trace:"), nest(indent, compose(line(), tr.pp(fmt, opts, p)))};
return format{body, line(), format("Justification:"), nest(indent, compose(line(), jst.pp(fmt, opts, p)))};
} else {
return body;
}
@ -43,8 +43,8 @@ static format mk_unification_op(options const & opts) {
return unicode ? format("\u2248") /* ≈ */ : format("=?=");
}
unification_constraint_eq::unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, trace const & t):
unification_constraint_cell(unification_constraint_kind::Eq, c, t),
unification_constraint_eq::unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, justification const & j):
unification_constraint_cell(unification_constraint_kind::Eq, c, j),
m_lhs(lhs),
m_rhs(rhs) {
}
@ -52,15 +52,15 @@ unification_constraint_eq::unification_constraint_eq(context const & c, expr con
unification_constraint_eq::~unification_constraint_eq() {
}
format unification_constraint_eq::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const {
format unification_constraint_eq::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const {
format op = mk_unification_op(opts);
format body = mk_binary(fmt, opts, m_ctx, m_lhs, m_rhs, op);
body = add_context(fmt, opts, m_ctx, body);
return add_trace(fmt, opts, body, m_trace, p, include_trace);
return add_justification(fmt, opts, body, m_justification, p, include_justification);
}
unification_constraint_convertible::unification_constraint_convertible(context const & c, expr const & from, expr const & to, trace const & t):
unification_constraint_cell(unification_constraint_kind::Convertible, c, t),
unification_constraint_convertible::unification_constraint_convertible(context const & c, expr const & from, expr const & to, justification const & j):
unification_constraint_cell(unification_constraint_kind::Convertible, c, j),
m_from(from),
m_to(to) {
}
@ -68,16 +68,16 @@ unification_constraint_convertible::unification_constraint_convertible(context c
unification_constraint_convertible::~unification_constraint_convertible() {
}
format unification_constraint_convertible::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const {
format unification_constraint_convertible::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const {
bool unicode = get_pp_unicode(opts);
format op = unicode ? format("\u227A") /* ≺ */ : format("<<");
format body = mk_binary(fmt, opts, m_ctx, m_from, m_to, op);
body = add_context(fmt, opts, m_ctx, body);
return add_trace(fmt, opts, body, m_trace, p, include_trace);
return add_justification(fmt, opts, body, m_justification, p, include_justification);
}
unification_constraint_max::unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t):
unification_constraint_cell(unification_constraint_kind::Max, c, t),
unification_constraint_max::unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j):
unification_constraint_cell(unification_constraint_kind::Max, c, j),
m_lhs1(lhs1),
m_lhs2(lhs2),
m_rhs(rhs) {
@ -86,18 +86,18 @@ unification_constraint_max::unification_constraint_max(context const & c, expr c
unification_constraint_max::~unification_constraint_max() {
}
format unification_constraint_max::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const {
format unification_constraint_max::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const {
format op = mk_unification_op(opts);
format lhs1_fmt = fmt(m_ctx, m_lhs1, false, opts);
format lhs2_fmt = fmt(m_ctx, m_lhs2, false, opts);
format rhs_fmt = fmt(m_ctx, m_rhs, false, opts);
format body = group(format{format("max"), lp(), lhs1_fmt, comma(), nest(4, compose(line(), lhs2_fmt)), rp(), space(), op, line(), rhs_fmt});
body = add_context(fmt, opts, m_ctx, body);
return add_trace(fmt, opts, body, m_trace, p, include_trace);
return add_justification(fmt, opts, body, m_justification, p, include_justification);
}
unification_constraint_choice::unification_constraint_choice(context const & c, expr const & mvar, unsigned num, trace const & t):
unification_constraint_cell(unification_constraint_kind::Choice, c, t),
unification_constraint_choice::unification_constraint_choice(context const & c, expr const & mvar, unsigned num, justification const & j):
unification_constraint_cell(unification_constraint_kind::Choice, c, j),
m_mvar(mvar),
m_num_choices(num) {
}
@ -105,7 +105,7 @@ unification_constraint_choice::unification_constraint_choice(context const & c,
unification_constraint_choice::~unification_constraint_choice() {
}
format unification_constraint_choice::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const {
format unification_constraint_choice::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const {
bool unicode = get_pp_unicode(opts);
format m_fmt = fmt(m_ctx, m_mvar, false, opts);
format eq_op = mk_unification_op(opts);
@ -118,31 +118,31 @@ format unification_constraint_choice::pp(formatter const & fmt, options const &
}
body = group(body);
body = add_context(fmt, opts, m_ctx, body);
return add_trace(fmt, opts, body, m_trace, p, include_trace);
return add_justification(fmt, opts, body, m_justification, p, include_justification);
}
unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t) {
return unification_constraint(new unification_constraint_eq(c, lhs, rhs, t));
unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j) {
return unification_constraint(new unification_constraint_eq(c, lhs, rhs, j));
}
unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, trace const & t) {
return unification_constraint(new unification_constraint_convertible(c, from, to, t));
unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j) {
return unification_constraint(new unification_constraint_convertible(c, from, to, j));
}
unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t) {
return unification_constraint(new unification_constraint_max(c, lhs1, lhs2, rhs, t));
unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j) {
return unification_constraint(new unification_constraint_max(c, lhs1, lhs2, rhs, j));
}
unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t) {
unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j) {
char * mem = new char[sizeof(unification_constraint_choice) + num*sizeof(expr)];
unification_constraint r(new (mem) unification_constraint_choice(c, mvar, num, t));
unification_constraint r(new (mem) unification_constraint_choice(c, mvar, num, j));
expr * m_choices = to_choice(r)->m_choices;
for (unsigned i = 0; i < num; i++)
new (m_choices+i) expr(choices[i]);
return r;
}
unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list<expr> const & choices, trace const & t) {
return mk_choice_constraint(c, mvar, choices.size(), choices.begin(), t);
unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list<expr> const & choices, justification const & j) {
return mk_choice_constraint(c, mvar, choices.size(), choices.begin(), j);
}
}

58
src/kernel/unification_constraint.h
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include <algorithm>
#include "kernel/expr.h"
#include "kernel/context.h"
#include "kernel/trace.h"
#include "kernel/justification.h"
namespace lean {
/**
@ -37,17 +37,17 @@ class unification_constraint_cell {
protected:
unification_constraint_kind m_kind;
context m_ctx;
trace m_trace; //!< justification for this constraint
justification m_justification; //!< justification for this constraint
MK_LEAN_RC();
void dealloc();
public:
unification_constraint_cell(unification_constraint_kind k, context const & c, trace const & t);
unification_constraint_cell(unification_constraint_kind k, context const & c, justification const & j);
virtual ~unification_constraint_cell();
unification_constraint_kind kind() const { return m_kind; }
trace const & get_trace() const { return m_trace; }
justification const & get_justification() const { return m_justification; }
context const & get_context() const { return m_ctx; }
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const = 0;
void set_trace(trace const & t) { lean_assert(!m_trace); m_trace = t; }
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const = 0;
void set_justification(justification const & j) { lean_assert(!m_justification); m_justification = j; }
};
class unification_constraint {
@ -70,18 +70,18 @@ public:
operator bool() const { return m_ptr != nullptr; }
format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool include_trace = false) const {
format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool include_justification = false) const {
lean_assert(m_ptr);
return m_ptr->pp(fmt, opts, p, include_trace);
return m_ptr->pp(fmt, opts, p, include_justification);
}
trace const & get_trace() const { lean_assert(m_ptr); return m_ptr->get_trace(); }
void set_trace(trace const & t) { lean_assert(!get_trace()); lean_assert(m_ptr); m_ptr->set_trace(t); }
justification const & get_justification() const { lean_assert(m_ptr); return m_ptr->get_justification(); }
void set_justification(justification const & j) { lean_assert(!get_justification()); lean_assert(m_ptr); m_ptr->set_justification(j); }
friend unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t);
friend unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, trace const & t);
friend unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t);
friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t);
friend unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j);
friend unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j);
friend unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j);
friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j);
};
/**
@ -91,11 +91,11 @@ class unification_constraint_eq : public unification_constraint_cell {
expr m_lhs;
expr m_rhs;
public:
unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, trace const & t);
unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, justification const & j);
virtual ~unification_constraint_eq();
expr const & get_lhs() const { return m_lhs; }
expr const & get_rhs() const { return m_rhs; }
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const;
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const;
};
/**
@ -107,11 +107,11 @@ class unification_constraint_convertible : public unification_constraint_cell {
expr m_from;
expr m_to;
public:
unification_constraint_convertible(context const & c, expr const & from, expr const & to, trace const & t);
unification_constraint_convertible(context const & c, expr const & from, expr const & to, justification const & j);
virtual ~unification_constraint_convertible();
expr const & get_from() const { return m_from; }
expr const & get_to() const { return m_to; }
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const;
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const;
};
/**
@ -122,12 +122,12 @@ class unification_constraint_max : public unification_constraint_cell {
expr m_lhs2;
expr m_rhs;
public:
unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t);
unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j);
virtual ~unification_constraint_max();
expr const & get_lhs1() const { return m_lhs1; }
expr const & get_lhs2() const { return m_lhs2; }
expr const & get_rhs() const { return m_rhs; }
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const;
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const;
};
/**
@ -137,23 +137,23 @@ class unification_constraint_choice : public unification_constraint_cell {
expr m_mvar;
unsigned m_num_choices;
expr m_choices[0];
friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t);
friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j);
public:
unification_constraint_choice(context const & c, expr const & mvar, unsigned num, trace const & t);
unification_constraint_choice(context const & c, expr const & mvar, unsigned num, justification const & j);
virtual ~unification_constraint_choice();
expr const & get_mvar() const { return m_mvar; }
unsigned get_num_choices() const { return m_num_choices; }
expr const & get_choice(unsigned idx) const { lean_assert(idx < m_num_choices); return m_choices[idx]; }
expr const * begin_choices() const { return m_choices; }
expr const * end_choices() const { return m_choices + m_num_choices; }
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_trace) const;
virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const;
};
unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, trace const & t);
unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, trace const & t);
unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, trace const & t);
unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, trace const & t);
unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list<expr> const & choices, trace const & t);
unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j);
unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j);
unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j);
unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j);
unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list<expr> const & choices, justification const & j);
inline bool is_eq(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Eq; }
inline bool is_convertible(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Convertible; }
@ -166,7 +166,7 @@ inline unification_constraint_max * to_max(unification_constraint const
inline unification_constraint_choice * to_choice(unification_constraint const & c) { lean_assert(is_choice(c)); return static_cast<unification_constraint_choice*>(c.raw()); }
inline context const & get_context(unification_constraint const & c) { return c.raw()->get_context(); }
inline trace const & get_trace(unification_constraint const & c) { return c.raw()->get_trace(); }
inline justification const & get_justification(unification_constraint const & c) { return c.raw()->get_justification(); }
inline expr const & eq_lhs(unification_constraint const & c) { return to_eq(c)->get_lhs(); }
inline expr const & eq_rhs(unification_constraint const & c) { return to_eq(c)->get_rhs(); }
inline expr const & convertible_from(unification_constraint const & c) { return to_convertible(c)->get_from(); }

2
src/library/elaborator/CMakeLists.txt
View file

@ -1,2 +1,2 @@
add_library(elaborator elaborator.cpp elaborator_trace.cpp)
add_library(elaborator elaborator.cpp elaborator_justification.cpp)
target_link_libraries(elaborator ${LEAN_LIBS})

234
src/library/elaborator/elaborator.cpp
View file

@ -18,7 +18,7 @@ Author: Leonardo de Moura
#include "library/update_expr.h"
#include "library/reduce.h"
#include "library/elaborator/elaborator.h"
#include "library/elaborator/elaborator_trace.h"
#include "library/elaborator/elaborator_justification.h"
namespace lean {
static name g_x_name("x");
@ -46,9 +46,9 @@ class elaborator::imp {
\brief Base class for case splits performed by the elaborator.
*/
struct case_split {
trace m_curr_assumption; // trace object used to justify current split
state m_prev_state;
std::vector<trace> m_failed_traces; // traces/justifications for failed branches
justification m_curr_assumption; // object used to justify current split
state m_prev_state;
std::vector<justification> m_failed_justifications; // justifications for failed branches
case_split(state const & prev_state):m_prev_state(prev_state) {}
virtual ~case_split() {}
@ -80,10 +80,10 @@ class elaborator::imp {
\brief General purpose case split object
*/
struct generic_case_split : public case_split {
unification_constraint m_constraint;
unsigned m_idx; // current alternative
std::vector<state> m_states; // alternatives
std::vector<trace> m_assumptions; // assumption for each alternative
unification_constraint m_constraint;
unsigned m_idx; // current alternative
std::vector<state> m_states; // alternatives
std::vector<justification> m_assumptions; // assumption for each alternative
generic_case_split(unification_constraint const & cnstr, state const & prev_state):
case_split(prev_state),
@ -97,7 +97,7 @@ class elaborator::imp {
return owner.next_generic_case(*this);
}
void push_back(state const & s, trace const & tr) {
void push_back(state const & s, justification const & tr) {
m_states.push_back(s);
m_assumptions.push_back(tr);
}
@ -142,28 +142,28 @@ class elaborator::imp {
std::shared_ptr<elaborator_plugin> m_plugin;
unsigned m_next_id;
int m_quota;
trace m_conflict;
justification m_conflict;
bool m_first;
bool m_interrupted;
// options
bool m_use_traces;
bool m_use_justifications;
bool m_use_normalizer;
void set_options(options const &) {
m_use_traces = true;
m_use_normalizer = true;
m_use_justifications = true;
m_use_normalizer = true;
}
void reset_quota() {
m_quota = m_state.m_queue.size();
}
trace mk_assumption() {
justification mk_assumption() {
unsigned id = m_next_id;
m_next_id++;
return trace(new assumption_trace(id));
return justification(new assumption_justification(id));
}
/** \brief Add given constraint to the front of the current constraint queue */
@ -190,11 +190,11 @@ class elaborator::imp {
return m_state.m_menv.get_subst(m);
}
/** \brief Return the trace/justification for an assigned metavariable */
trace get_mvar_trace(expr const & m) const {
/** \brief Return the justification/justification for an assigned metavariable */
justification get_mvar_justification(expr const & m) const {
lean_assert(is_metavar(m));
lean_assert(is_assigned(m));
return m_state.m_menv.get_trace(m);
return m_state.m_menv.get_justification(m);
}
/** \brief Return the type of an metavariable */
@ -286,59 +286,59 @@ class elaborator::imp {
\brief Auxiliary method for pushing a new constraint to the given constraint queue.
If \c is_eq is true, then a equality constraint is created, otherwise a convertability constraint is created.
*/
void push_new_constraint(cnstr_queue & q, bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, trace const & new_tr) {
void push_new_constraint(cnstr_queue & q, bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) {
if (is_eq)
q.push_front(mk_eq_constraint(new_ctx, new_a, new_b, new_tr));
q.push_front(mk_eq_constraint(new_ctx, new_a, new_b, new_jst));
else
q.push_front(mk_convertible_constraint(new_ctx, new_a, new_b, new_tr));
q.push_front(mk_convertible_constraint(new_ctx, new_a, new_b, new_jst));
}
void push_new_eq_constraint(cnstr_queue & q, context const & new_ctx, expr const & new_a, expr const & new_b, trace const & new_tr) {
push_new_constraint(q, true, new_ctx, new_a, new_b, new_tr);
void push_new_eq_constraint(cnstr_queue & q, context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) {
push_new_constraint(q, true, new_ctx, new_a, new_b, new_jst);
}
/**
\brief Auxiliary method for pushing a new constraint to the current constraint queue.
If \c is_eq is true, then a equality constraint is created, otherwise a convertability constraint is created.
*/
void push_new_constraint(bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, trace const & new_tr) {
void push_new_constraint(bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) {
reset_quota();
push_new_constraint(m_state.m_queue, is_eq, new_ctx, new_a, new_b, new_tr);
push_new_constraint(m_state.m_queue, is_eq, new_ctx, new_a, new_b, new_jst);
}
/**
\brief Auxiliary method for pushing a new constraint to the current constraint queue.
The new constraint is based on the constraint \c c. The constraint \c c may be a equality or convertability constraint.
The update is justified by \c new_tr.
The update is justified by \c new_jst.
*/
void push_updated_constraint(unification_constraint const & c, expr const & new_a, expr const & new_b, trace const & new_tr) {
void push_updated_constraint(unification_constraint const & c, expr const & new_a, expr const & new_b, justification const & new_jst) {
lean_assert(is_eq(c) || is_convertible(c));
context const & ctx = get_context(c);
if (is_eq(c))
push_front(mk_eq_constraint(ctx, new_a, new_b, new_tr));
push_front(mk_eq_constraint(ctx, new_a, new_b, new_jst));
else
push_front(mk_convertible_constraint(ctx, new_a, new_b, new_tr));
push_front(mk_convertible_constraint(ctx, new_a, new_b, new_jst));
}
/**
\brief Auxiliary method for pushing a new constraint to the current constraint queue.
The new constraint is based on the constraint \c c. The constraint \c c may be a equality or convertability constraint.
The flag \c is_lhs says if the left-hand-side or right-hand-side are being updated with \c new_a.
The update is justified by \c new_tr.
The update is justified by \c new_jst.
*/
void push_updated_constraint(unification_constraint const & c, bool is_lhs, expr const & new_a, trace const & new_tr) {
void push_updated_constraint(unification_constraint const & c, bool is_lhs, expr const & new_a, justification const & new_jst) {
lean_assert(is_eq(c) || is_convertible(c));
context const & ctx = get_context(c);
if (is_eq(c)) {
if (is_lhs)
push_front(mk_eq_constraint(ctx, new_a, eq_rhs(c), new_tr));
push_front(mk_eq_constraint(ctx, new_a, eq_rhs(c), new_jst));
else
push_front(mk_eq_constraint(ctx, eq_lhs(c), new_a, new_tr));
push_front(mk_eq_constraint(ctx, eq_lhs(c), new_a, new_jst));
} else {
if (is_lhs)
push_front(mk_convertible_constraint(ctx, new_a, convertible_to(c), new_tr));
push_front(mk_convertible_constraint(ctx, new_a, convertible_to(c), new_jst));
else
push_front(mk_convertible_constraint(ctx, convertible_from(c), new_a, new_tr));
push_front(mk_convertible_constraint(ctx, convertible_from(c), new_a, new_jst));
}
}
@ -347,13 +347,13 @@ class elaborator::imp {
The new constraint is obtained from \c c by one or more normalization steps that produce \c new_a and \c new_b
*/
void push_normalized_constraint(unification_constraint const & c, expr const & new_a, expr const & new_b) {
push_updated_constraint(c, new_a, new_b, trace(new normalize_trace(c)));
push_updated_constraint(c, new_a, new_b, justification(new normalize_justification(c)));
}
/**
\brief Assign \c v to \c m with justification \c tr in the current state.
*/
void assign(expr const & m, expr const & v, context const & ctx, trace const & tr) {
void assign(expr const & m, expr const & v, context const & ctx, justification const & tr) {
lean_assert(is_metavar(m));
metavar_env & menv = m_state.m_menv;
m_state.m_menv.assign(m, v, tr);
@ -362,8 +362,8 @@ class elaborator::imp {
expr tv = m_type_inferer(v, ctx, &menv, ucs);
for (auto c : ucs)
push_front(c);
trace new_trace(new typeof_mvar_trace(ctx, m, menv.get_type(m), tv, tr));
push_front(mk_convertible_constraint(ctx, tv, menv.get_type(m), new_trace));
justification new_jst(new typeof_mvar_justification(ctx, m, menv.get_type(m), tv, tr));
push_front(mk_convertible_constraint(ctx, tv, menv.get_type(m), new_jst));
}
}
@ -400,16 +400,16 @@ class elaborator::imp {
if (is_metavar(a)) {
if (is_assigned(a)) {
// Case 1
trace new_tr(new substitution_trace(c, get_mvar_trace(a)));
push_updated_constraint(c, is_lhs, get_mvar_subst(a), new_tr);
justification new_jst(new substitution_justification(c, get_mvar_justification(a)));
push_updated_constraint(c, is_lhs, get_mvar_subst(a), new_jst);
return Processed;
} else if (!has_local_context(a)) {
// Case 2
if (has_metavar(b, a)) {
m_conflict = trace(new unification_failure_trace(c));
m_conflict = justification(new unification_failure_justification(c));
return Failed;
} else if (allow_assignment) {
assign(a, b, get_context(c), trace(new assignment_trace(c)));
assign(a, b, get_context(c), justification(new assignment_justification(c)));
reset_quota();
return Processed;
}
@ -418,18 +418,18 @@ class elaborator::imp {
if (me.is_lift()) {
if (!has_free_var(b, me.s(), me.s() + me.n())) {
// Case 3
trace new_tr(new normalize_trace(c));
justification new_jst(new normalize_justification(c));
expr new_a = pop_meta_context(a);
expr new_b = lower_free_vars(b, me.s() + me.n(), me.n());
context new_ctx = get_context(c).remove(me.s(), me.n());
if (!is_lhs)
swap(new_a, new_b);
push_new_constraint(is_eq(c), new_ctx, new_a, new_b, new_tr);
push_new_constraint(is_eq(c), new_ctx, new_a, new_b, new_jst);
return Processed;
} else if (is_var(b)) {
// Failure, there is no way to unify
// ?m[lift:s:n, ...] with a variable in [s, s+n]
m_conflict = trace(new unification_failure_trace(c));
m_conflict = justification(new unification_failure_justification(c));
return Failed;
}
}
@ -438,34 +438,34 @@ class elaborator::imp {
if (is_app(a) && is_metavar(arg(a, 0)) && is_assigned(arg(a, 0))) {
// Case 4
trace new_tr(new substitution_trace(c, get_mvar_trace(arg(a, 0))));
justification new_jst(new substitution_justification(c, get_mvar_justification(arg(a, 0))));
expr new_a = update_app(a, 0, get_mvar_subst(arg(a, 0)));
push_updated_constraint(c, is_lhs, new_a, new_tr);
push_updated_constraint(c, is_lhs, new_a, new_jst);
return Processed;
}
return Continue;
}
trace mk_subst_trace(unification_constraint const & c, buffer<trace> const & subst_traces) {
if (subst_traces.size() == 1) {
return trace(new substitution_trace(c, subst_traces[0]));
justification mk_subst_justification(unification_constraint const & c, buffer<justification> const & subst_justifications) {
if (subst_justifications.size() == 1) {
return justification(new substitution_justification(c, subst_justifications[0]));
} else {
return trace(new multi_substitution_trace(c, subst_traces.size(), subst_traces.data()));
return justification(new multi_substitution_justification(c, subst_justifications.size(), subst_justifications.data()));
}
}
/**
\brief Instantiate the assigned metavariables in \c a, and store the justification
in \c traces.
\brief Instantiate the assigned metavariables in \c a, and store the justifications
in \c jsts.
*/
expr instantiate_metavars(expr const & a, buffer<trace> & traces) {
expr instantiate_metavars(expr const & a, buffer<justification> & jsts) {
lean_assert(has_assigned_metavar(a));
metavar_env & menv = m_state.m_menv;
auto f = [&](expr const & m, unsigned) -> expr {
if (is_metavar(m) && menv.is_assigned(m)) {
trace t = menv.get_trace(m);
justification t = menv.get_justification(m);
if (t)
traces.push_back(t);
jsts.push_back(t);
return menv.get_subst(m);
} else {
return m;
@ -488,10 +488,10 @@ class elaborator::imp {
lean_assert(!is_convertible(c) || !is_lhs || is_eqp(convertible_from(c), a));
lean_assert(!is_convertible(c) || is_lhs || is_eqp(convertible_to(c), a));
if (has_assigned_metavar(a)) {
buffer<trace> traces;
expr new_a = instantiate_metavars(a, traces);
trace new_tr = mk_subst_trace(c, traces);
push_updated_constraint(c, is_lhs, new_a, new_tr);
buffer<justification> jsts;
expr new_a = instantiate_metavars(a, jsts);
justification new_jst = mk_subst_justification(c, jsts);
push_updated_constraint(c, is_lhs, new_a, new_jst);
return true;
} else {
return false;
@ -679,11 +679,11 @@ class elaborator::imp {
buffer<expr> types;
for (unsigned i = 1; i < num_args(a); i++)
types.push_back(lookup(ctx, var_idx(arg(a, i))).get_domain());
trace new_trace(new destruct_trace(c));
justification new_jst(new destruct_justification(c));
expr s = mk_lambda(types, b);
if (!is_lhs)
swap(m, s);
push_front(mk_eq_constraint(ctx, m, s, new_trace));
push_front(mk_eq_constraint(ctx, m, s, new_jst));
return true;
} else {
return false;
@ -711,7 +711,7 @@ class elaborator::imp {
for (unsigned i = 1; i < num_a; i++) {
// Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), x_i
state new_state(m_state);
trace new_assumption = mk_assumption();
justification new_assumption = mk_assumption();
expr proj = mk_lambda(arg_types, mk_var(num_a - i - 1));
expr new_a = arg(a, i);
expr new_b = b;
@ -723,7 +723,7 @@ class elaborator::imp {
}
// Add imitation
state new_state(m_state);
trace new_assumption = mk_assumption();
justification new_assumption = mk_assumption();
expr imitation;
if (is_app(b)) {
// Imitation for applications
@ -829,7 +829,7 @@ class elaborator::imp {
{
// Case 1
state new_state(m_state);
trace new_assumption = mk_assumption();
justification new_assumption = mk_assumption();
// add ?m[...] == #1
push_new_eq_constraint(new_state.m_queue, ctx, pop_meta_context(a), mk_var(i), new_assumption);
// add t == b (t << b)
@ -843,7 +843,7 @@ class elaborator::imp {
{
// Case 2
state new_state(m_state);
trace new_assumption = mk_assumption();
justification new_assumption = mk_assumption();
expr imitation;
if (is_app(b)) {
// Imitation for applications b == f(s_1, ..., s_k)
@ -911,8 +911,8 @@ class elaborator::imp {
// See comment at process_metavar_inst
expr imitation = update_abstraction(b, h_1, h_2);
expr ma = mk_metavar(metavar_name(a));
trace new_tr(new imitation_trace(c));
push_new_constraint(true, ctx, ma, imitation, new_tr);
justification new_jst(new imitation_justification(c));
push_new_constraint(true, ctx, ma, imitation, new_jst);
return true;
} else {
return false;
@ -934,14 +934,14 @@ class elaborator::imp {
if (is_lower(c)) {
// Remark: in principle, there are infinite number of choices.
// We approximate and only consider the most useful ones.
trace new_tr(new destruct_trace(c));
justification new_jst(new destruct_justification(c));
unification_constraint new_c;
if (a == Bool) {
expr choices[5] = { Bool, Type(), Type(level() + 1), TypeM, TypeU };
new_c = mk_choice_constraint(get_context(c), b, 5, choices, new_tr);
new_c = mk_choice_constraint(get_context(c), b, 5, choices, new_jst);
} else {
expr choices[5] = { a, Type(ty_level(a) + 1), Type(ty_level(a) + 2), TypeM, TypeU };
new_c = mk_choice_constraint(get_context(c), b, 5, choices, new_tr);
new_c = mk_choice_constraint(get_context(c), b, 5, choices, new_jst);
}
push_front(new_c);
return true;
@ -997,17 +997,17 @@ class elaborator::imp {
// and just check if the upper bound is satisfied.
//
// Remark: we also give preference to lower bounds
trace new_tr(new destruct_trace(c));
justification new_jst(new destruct_justification(c));
unification_constraint new_c;
if (b == Type()) {
expr choices[2] = { Type(), Bool };
new_c = mk_choice_constraint(get_context(c), a, 2, choices, new_tr);
new_c = mk_choice_constraint(get_context(c), a, 2, choices, new_jst);
} else if (b == TypeU) {
expr choices[5] = { TypeU, TypeM, Type(level() + 1), Type(), Bool };
new_c = mk_choice_constraint(get_context(c), a, 5, choices, new_tr);
new_c = mk_choice_constraint(get_context(c), a, 5, choices, new_jst);
} else if (b == TypeM) {
expr choices[4] = { TypeM, Type(level() + 1), Type(), Bool };
new_c = mk_choice_constraint(get_context(c), a, 4, choices, new_tr);
new_c = mk_choice_constraint(get_context(c), a, 4, choices, new_jst);
} else {
level const & lvl = ty_level(b);
lean_assert(!lvl.is_bottom());
@ -1026,10 +1026,10 @@ class elaborator::imp {
if (!L.is_bottom())
choices.push_back(Type());
choices.push_back(Bool);
new_c = mk_choice_constraint(get_context(c), a, choices.size(), choices.data(), new_tr);
new_c = mk_choice_constraint(get_context(c), a, choices.size(), choices.data(), new_jst);
} else if (is_uvar(lvl)) {
expr choices[4] = { Type(level() + 1), Type(), b, Bool };
new_c = mk_choice_constraint(get_context(c), a, 4, choices, new_tr);
new_c = mk_choice_constraint(get_context(c), a, 4, choices, new_jst);
} else {
lean_assert(is_max(lvl));
// TODO(Leo)
@ -1076,45 +1076,45 @@ class elaborator::imp {
if (a == b) {
return true;
} else {
m_conflict = trace(new unification_failure_trace(c));
m_conflict = justification(new unification_failure_justification(c));
return false;
}
case expr_kind::Type:
if ((!eq && m_env.is_ge(ty_level(b), ty_level(a))) || (eq && a == b)) {
return true;
} else {
m_conflict = trace(new unification_failure_trace(c));
m_conflict = justification(new unification_failure_justification(c));
return false;
}
case expr_kind::Eq: {
trace new_trace(new destruct_trace(c));
push_front(mk_eq_constraint(ctx, eq_lhs(a), eq_lhs(b), new_trace));
push_front(mk_eq_constraint(ctx, eq_rhs(a), eq_rhs(b), new_trace));
justification new_jst(new destruct_justification(c));
push_front(mk_eq_constraint(ctx, eq_lhs(a), eq_lhs(b), new_jst));
push_front(mk_eq_constraint(ctx, eq_rhs(a), eq_rhs(b), new_jst));
return true;
}
case expr_kind::Pi: {
trace new_trace(new destruct_trace(c));
push_front(mk_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_trace));
justification new_jst(new destruct_justification(c));
push_front(mk_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst));
context new_ctx = extend(ctx, abst_name(a), abst_domain(a));
if (eq)
push_front(mk_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_trace));
push_front(mk_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_jst));
else
push_front(mk_convertible_constraint(new_ctx, abst_body(a), abst_body(b), new_trace));
push_front(mk_convertible_constraint(new_ctx, abst_body(a), abst_body(b), new_jst));
return true;
}
case expr_kind::Lambda: {
trace new_trace(new destruct_trace(c));
push_front(mk_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_trace));
justification new_jst(new destruct_justification(c));
push_front(mk_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst));
context new_ctx = extend(ctx, abst_name(a), abst_domain(a));
push_front(mk_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_trace));
push_front(mk_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_jst));
return true;
}
case expr_kind::App:
if (!is_meta_app(a) && !is_meta_app(b)) {
if (num_args(a) == num_args(b)) {
trace new_trace(new destruct_trace(c));
justification new_jst(new destruct_justification(c));
for (unsigned i = 0; i < num_args(a); i++)
push_front(mk_eq_constraint(ctx, arg(a, i), arg(b, i), new_trace));
push_front(mk_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst));
return true;
} else {
return false;
@ -1135,7 +1135,7 @@ class elaborator::imp {
}
if (a.kind() != b.kind() && !has_metavar(a) && !has_metavar(b)) {
m_conflict = trace(new unification_failure_trace(c));
m_conflict = justification(new unification_failure_justification(c));
return false;
}
@ -1170,26 +1170,26 @@ class elaborator::imp {
expr const & lhs1 = max_lhs1(c);
expr const & lhs2 = max_lhs2(c);
expr const & rhs = max_rhs(c);
buffer<trace> traces;
buffer<justification> jsts;
bool modified = false;
expr new_lhs1 = lhs1;
expr new_lhs2 = lhs2;
expr new_rhs = rhs;
if (has_assigned_metavar(lhs1)) {
new_lhs1 = instantiate_metavars(lhs1, traces);
new_lhs1 = instantiate_metavars(lhs1, jsts);
modified = true;
}
if (has_assigned_metavar(lhs2)) {
new_lhs2 = instantiate_metavars(lhs2, traces);
new_lhs2 = instantiate_metavars(lhs2, jsts);
modified = true;
}
if (has_assigned_metavar(rhs)) {
new_rhs = instantiate_metavars(rhs, traces);
new_rhs = instantiate_metavars(rhs, jsts);
modified = true;
}
if (modified) {
trace new_tr = mk_subst_trace(c, traces);
push_front(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_tr));
justification new_jst = mk_subst_justification(c, jsts);
push_front(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_jst));
return true;
}
if (!is_metavar(lhs1) && !is_type(lhs1)) {
@ -1205,35 +1205,35 @@ class elaborator::imp {
modified = (rhs != new_rhs);
}
if (modified) {
trace new_tr(new normalize_trace(c));
push_front(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_tr));
justification new_jst(new normalize_justification(c));
push_front(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_jst));
return true;
}
if (is_type(lhs1) && is_type(lhs2)) {
trace new_tr(new normalize_trace(c));
justification new_jst(new normalize_justification(c));
expr new_lhs = mk_type(max(ty_level(lhs1), ty_level(lhs2)));
push_front(mk_eq_constraint(get_context(c), new_lhs, rhs, new_tr));
push_front(mk_eq_constraint(get_context(c), new_lhs, rhs, new_jst));
return true;
}
if (lhs1 == rhs) {
// ctx |- max(lhs1, lhs2) == rhs
// ==> IF lhs1 = rhs
// ctx |- lhs2 << rhs
trace new_tr(new normalize_trace(c));
push_front(mk_convertible_constraint(get_context(c), lhs2, rhs, new_tr));
justification new_jst(new normalize_justification(c));
push_front(mk_convertible_constraint(get_context(c), lhs2, rhs, new_jst));
return true;
} else if (lhs2 == rhs) {
// ctx |- max(lhs1, lhs2) == rhs
// ==> IF lhs1 = rhs
// ctx |- lhs2 << rhs
trace new_tr(new normalize_trace(c));
push_front(mk_convertible_constraint(get_context(c), lhs1, rhs, new_tr));
justification new_jst(new normalize_justification(c));
push_front(mk_convertible_constraint(get_context(c), lhs1, rhs, new_jst));
return true;
}
if ((!has_metavar(lhs1) && !is_type(lhs1)) ||
(!has_metavar(lhs2) && !is_type(lhs2))) {
m_conflict = trace(new unification_failure_trace(c));
m_conflict = justification(new unification_failure_justification(c));
return false;
}
@ -1261,9 +1261,9 @@ class elaborator::imp {
std::unique_ptr<case_split> & d = m_case_splits.back();
// std::cout << "Assumption " << d->m_curr_assumption.pp(fmt, options(), nullptr, true) << "\n";
if (depends_on(m_conflict, d->m_curr_assumption)) {
d->m_failed_traces.push_back(m_conflict);
d->m_failed_justifications.push_back(m_conflict);
if (d->next(*this)) {
m_conflict = trace();
m_conflict = justification();
reset_quota();
return;
}
@ -1283,7 +1283,7 @@ class elaborator::imp {
push_front(mk_eq_constraint(get_context(choice), choice_mvar(choice), choice_ith(choice, idx), s.m_curr_assumption));
return true;
} else {
m_conflict = trace(new unification_failure_by_cases_trace(choice, s.m_failed_traces.size(), s.m_failed_traces.data()));
m_conflict = justification(new unification_failure_by_cases_justification(choice, s.m_failed_justifications.size(), s.m_failed_justifications.data()));
return false;
}
}
@ -1297,7 +1297,7 @@ class elaborator::imp {
m_state = s.m_states[sz - idx - 1];
return true;
} else {
m_conflict = trace(new unification_failure_by_cases_trace(s.m_constraint, s.m_failed_traces.size(), s.m_failed_traces.data()));
m_conflict = justification(new unification_failure_by_cases_justification(s.m_constraint, s.m_failed_justifications.size(), s.m_failed_justifications.data()));
return false;
}
}
@ -1313,7 +1313,7 @@ class elaborator::imp {
}
return true;
} catch (exception & ex) {
m_conflict = trace(new unification_failure_by_cases_trace(s.m_constraint, s.m_failed_traces.size(), s.m_failed_traces.data()));
m_conflict = justification(new unification_failure_by_cases_justification(s.m_constraint, s.m_failed_justifications.size(), s.m_failed_justifications.data()));
return false;
}
}
@ -1340,16 +1340,16 @@ public:
if (m_conflict)
throw elaborator_exception(m_conflict);
if (!m_case_splits.empty()) {
buffer<trace> assumptions;
buffer<justification> assumptions;
for (std::unique_ptr<case_split> const & cs : m_case_splits)
assumptions.push_back(cs->m_curr_assumption);
m_conflict = trace(new next_solution_trace(assumptions.size(), assumptions.data()));
m_conflict = justification(new next_solution_justification(assumptions.size(), assumptions.data()));
resolve_conflict();
} else if (m_first) {
m_first = false;
} else {
// this is not the first run, and there are no case-splits
m_conflict = trace(new next_solution_trace(0, nullptr));
m_conflict = justification(new next_solution_justification(0, nullptr));
throw elaborator_exception(m_conflict);
}
reset_quota();
@ -1410,7 +1410,7 @@ elaborator::elaborator(environment const & env,
elaborator::elaborator(environment const & env,
metavar_env const & menv,
context const & ctx, expr const & lhs, expr const & rhs):
elaborator(env, menv, { mk_eq_constraint(ctx, lhs, rhs, trace()) }) {
elaborator(env, menv, { mk_eq_constraint(ctx, lhs, rhs, justification()) }) {
}
elaborator::~elaborator() {

10
src/library/elaborator/elaborator_exception.h
View file

@ -6,20 +6,20 @@ Author: Leonardo de Moura
*/
#pragma once
#include "util/exception.h"
#include "kernel/trace.h"
#include "kernel/justification.h"
namespace lean {
/**
\brief Elaborator and related components store the reason for
failure in trace objects.
failure in justification objects.
*/
class elaborator_exception : public exception {
trace m_trace;
justification m_justification;
public:
elaborator_exception(trace const & tr):m_trace(tr) {}
elaborator_exception(justification const & j):m_justification(j) {}
virtual ~elaborator_exception() {}
virtual char const * what() const noexcept { return "elaborator exception"; }
trace const & get_trace() const { return m_trace; }
justification const & get_justification() const { return m_justification; }
};

187
src/library/elaborator/elaborator_justification.cpp Normal file
View file

@ -0,0 +1,187 @@
/*
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 "library/elaborator/elaborator_justification.h"
namespace lean {
static void push_back(buffer<justification_cell*> & r, justification const & t) {
if (t)
r.push_back(t.raw());
}
template<typename T>
static void append(buffer<justification_cell*> & r, T const & s) {
for (auto t : s)
push_back(r, t);
}
// -------------------------
// Assumptions
// -------------------------
assumption_justification::assumption_justification(unsigned idx):m_idx(idx) {
}
void assumption_justification::get_children(buffer<justification_cell*> &) const {
}
expr const & assumption_justification::get_main_expr() const {
return expr::null();
}
format assumption_justification::pp_header(formatter const &, options const &) const {
return format{format("assumption"), space(), format(m_idx)};
}
// -------------------------
// Propagation justification
// -------------------------
propagation_justification::propagation_justification(unification_constraint const & c):
m_constraint(c) {
}
propagation_justification::~propagation_justification() {
}
void propagation_justification::get_children(buffer<justification_cell*> & r) const {
push_back(r, m_constraint.get_justification());
}
expr const & propagation_justification::get_main_expr() const {
return expr::null();
}
format propagation_justification::pp_header(formatter const & fmt, options const & opts) const {
format r;
r += format(get_prop_name());
r += compose(line(), get_constraint().pp(fmt, opts, nullptr, false));
return r;
}
// -------------------------
// Unification failure (by cases)
// -------------------------
unification_failure_by_cases_justification::unification_failure_by_cases_justification(unification_constraint const & c, unsigned num, justification const * cs):
unification_failure_justification(c),
m_cases(cs, cs + num) {
}
unification_failure_by_cases_justification::~unification_failure_by_cases_justification() {
}
void unification_failure_by_cases_justification::get_children(buffer<justification_cell*> & r) const {
push_back(r, get_constraint().get_justification());
append(r, m_cases);
}
// -------------------------
// Substitution justification
// -------------------------
substitution_justification::substitution_justification(unification_constraint const & c, justification const & t):
propagation_justification(c),
m_assignment_justification(t) {
}
substitution_justification::~substitution_justification() {
}
void substitution_justification::get_children(buffer<justification_cell*> & r) const {
propagation_justification::get_children(r);
push_back(r, m_assignment_justification);
}
multi_substitution_justification::multi_substitution_justification(unification_constraint const & c, unsigned num, justification const * ts):
propagation_justification(c),
m_assignment_justifications(ts, ts + num) {
}
multi_substitution_justification::~multi_substitution_justification() {
}
void multi_substitution_justification::get_children(buffer<justification_cell*> & r) const {
propagation_justification::get_children(r);
append(r, m_assignment_justifications);
}
// -------------------------
// typeof metavar justification
// -------------------------
typeof_mvar_justification::typeof_mvar_justification(context const & ctx, expr const & m, expr const & tm, expr const & t, justification const & tr):
m_context(ctx),
m_mvar(m),
m_typeof_mvar(tm),
m_type(t),
m_justification(tr) {
}
typeof_mvar_justification::~typeof_mvar_justification() {
}
format typeof_mvar_justification::pp_header(formatter const & fmt, options const & opts) const {
format r;
unsigned indent = get_pp_indent(opts);
r += format("Propagate type,");
{
format body;
body += fmt(m_context, m_mvar, false, opts);
body += space();
body += colon();
body += nest(indent, compose(line(), fmt(m_context, m_typeof_mvar, false, opts)));
r += nest(indent, compose(line(), body));
}
return group(r);
}
void typeof_mvar_justification::get_children(buffer<justification_cell*> & r) const {
push_back(r, m_justification);
}
// -------------------------
// Synthesis justification objects
// -------------------------
synthesis_justification::synthesis_justification(context const & ctx, expr const & mvar, expr const & type, unsigned num, justification const * substs):
m_context(ctx),
m_mvar(mvar),
m_type(type),
m_substitution_justifications(substs, substs + num) {
}
synthesis_justification::~synthesis_justification() {
}
format synthesis_justification::pp_header(formatter const & fmt, options const & opts) const {
format r;
r += format(get_label());
r += space();
r += fmt(m_context, m_mvar, false, opts);
unsigned indent = get_pp_indent(opts);
r += nest(indent, compose(line(), fmt(m_context, m_type, true, opts)));
return r;
}
void synthesis_justification::get_children(buffer<justification_cell*> & r) const {
append(r, m_substitution_justifications);
}
expr const & synthesis_justification::get_main_expr() const {
return m_mvar;
}
char const * synthesis_failure_justification::get_label() const {
return "Failed to synthesize expression of type for";
}
synthesis_failure_justification::synthesis_failure_justification(context const & ctx, expr const & mvar, expr const & type, justification const & tr, unsigned num, justification const * substs):
synthesis_justification(ctx, mvar, type, num, substs),
m_justification(tr) {
}
synthesis_failure_justification::~synthesis_failure_justification() {
}
void synthesis_failure_justification::get_children(buffer<justification_cell*> & r) const {
synthesis_justification::get_children(r);
push_back(r, m_justification);
}
char const * synthesized_assignment_justification::get_label() const {
return "Synthesized assignment for";
}
// -------------------------
// Next solution justification
// -------------------------
next_solution_justification::next_solution_justification(unsigned num, justification const * as):
m_assumptions(as, as + num) {
}
next_solution_justification::~next_solution_justification() {
}
format next_solution_justification::pp_header(formatter const &, options const &) const {
return format("next solution");
}
void next_solution_justification::get_children(buffer<justification_cell*> & r) const {
append(r, m_assumptions);
}
expr const & next_solution_justification::get_main_expr() const {
return expr::null();
}
}

229
src/library/elaborator/elaborator_justification.h Normal file
View file

@ -0,0 +1,229 @@
/*
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 <vector>
#include "kernel/justification.h"
#include "kernel/unification_constraint.h"
namespace lean {
/**
\brief Base class for justification objects used to justify case-splits.
*/
class assumption_justification : public justification_cell {
unsigned m_idx;
public:
assumption_justification(unsigned idx);
virtual void get_children(buffer<justification_cell*> &) const;
virtual expr const & get_main_expr() const;
virtual format pp_header(formatter const &, options const &) const;
};
/**
\brief Base class for justifying propagations and failures
*/
class propagation_justification : public justification_cell {
unification_constraint m_constraint;
protected:
/** \brief Auxiliary method used by pp_header to label a propagation step, subclasses must redefine it. */
virtual char const * get_prop_name() const = 0;
public:
propagation_justification(unification_constraint const & c);
virtual ~propagation_justification();
virtual void get_children(buffer<justification_cell*> & r) const;
virtual expr const & get_main_expr() const;
virtual format pp_header(formatter const &, options const &) const;
unification_constraint const & get_constraint() const { return m_constraint; }
};
/**
\brief Justification object used to mark that a particular unification constraint could not be solved.
*/
class unification_failure_justification : public propagation_justification {
protected:
virtual char const * get_prop_name() const { return "Failed to solve"; }
public:
unification_failure_justification(unification_constraint const & c):propagation_justification(c) {}
};
/**
\brief Justification object created for justifying that a constraint that
generated a case-split does not have a solution. Each case-split
corresponds to a different way of solving the constraint.
*/
class unification_failure_by_cases_justification : public unification_failure_justification {
std::vector<justification> m_cases; // why each case failed
public:
unification_failure_by_cases_justification(unification_constraint const & c, unsigned num, justification const * cs);
virtual ~unification_failure_by_cases_justification();
virtual void get_children(buffer<justification_cell*> & r) const;
};
/**
\brief Justification object used to justify a metavar assignment.
*/
class assignment_justification : public propagation_justification {
protected:
virtual char const * get_prop_name() const { return "Assignment"; }
public:
assignment_justification(unification_constraint const & c):propagation_justification(c) {}
};
/**
\brief Justification object used to justify simple structural steps when processing unification
constraints. For example, given the constraint
<tt>ctx |- (f a) == (f b)</tt>
where \c f is a variable, we must have
<tt>ctx |- a == b</tt>
The justification for the latter is a destruct justification based on the former.
*/
class destruct_justification : public propagation_justification {
protected:
virtual char const * get_prop_name() const { return "Destruct/Decompose"; }
public:
destruct_justification(unification_constraint const & c):propagation_justification(c) {}
};
/**
\brief Justification object used to justify a normalization step such as.
<tt>ctx |- (fun x : T, x) a == b</tt>
==>
<tt>ctx |- a == b</tt>
*/
class normalize_justification : public propagation_justification {
protected:
virtual char const * get_prop_name() const { return "Normalize"; }
public:
normalize_justification(unification_constraint const & c):propagation_justification(c) {}
};
/**
\brief Justification object used to justify an imitation step.
An imitation step is used when solving constraints such as:
<tt>ctx |- ?m[lift:s:n, ...] == Pi (x : A), B x</tt>
In this case, ?m must be a Pi. We make progress, by adding the constraint
<tt>ctx |- ?m == Pi (x : ?M1), (?M2 x)</tt>
where ?M1 and ?M2 are fresh metavariables.
*/
class imitation_justification : public propagation_justification {
protected:
virtual char const * get_prop_name() const { return "Imitation"; }
public:
imitation_justification(unification_constraint const & c):propagation_justification(c) {}
};
/**
\brief Justification object used to justify a new constraint obtained by substitution.
*/
class substitution_justification : public propagation_justification {
justification m_assignment_justification;
protected:
virtual char const * get_prop_name() const { return "Substitution"; }
public:
substitution_justification(unification_constraint const & c, justification const & t);
virtual ~substitution_justification();
virtual void get_children(buffer<justification_cell*> & r) const;
};
/**
\brief Justification object used to justify a new constraint obtained by multiple substitution.
*/
class multi_substitution_justification : public propagation_justification {
std::vector<justification> m_assignment_justifications;
protected:
virtual char const * get_prop_name() const { return "Substitution"; }
public:
multi_substitution_justification(unification_constraint const & c, unsigned num, justification const * ts);
virtual ~multi_substitution_justification();
virtual void get_children(buffer<justification_cell*> & r) const;
};
/**
\brief Justification object used to justify a <tt>typeof(m) == t</tt> constraint generated when
we assign a metavariable \c m.
*/
class typeof_mvar_justification : public justification_cell {
context m_context;
expr m_mvar;
expr m_typeof_mvar;
expr m_type;
justification m_justification;
public:
typeof_mvar_justification(context const & ctx, expr const & m, expr const & mt, expr const & t, justification const & tr);
virtual ~typeof_mvar_justification();
virtual format pp_header(formatter const &, options const &) const;
virtual void get_children(buffer<justification_cell*> & r) const;
};
/**
\brief Base class for synthesis_failure_justification and synthesized_assignment_justification
*/
class synthesis_justification : public justification_cell {
context m_context;
expr m_mvar;
expr m_type;
std::vector<justification> m_substitution_justifications; // justification objects justifying the assignments used to instantiate \c m_type and \c m_context.
protected:
virtual char const * get_label() const = 0;
public:
synthesis_justification(context const & ctx, expr const & mvar, expr const & type, unsigned num, justification const * substs);
virtual ~synthesis_justification();
virtual format pp_header(formatter const &, options const &) const;
virtual void get_children(buffer<justification_cell*> & r) const;
virtual expr const & get_main_expr() const;
};
/**
\brief Justification object for justifying why a synthesis step failed.
A synthesis step is of the form
<tt>ctx |- ?mvar : type</tt>
Before invoking the synthesizer, the elaborator substitutes the
metavariables in \c ctx and \c type with their corresponding assignments.
*/
class synthesis_failure_justification : public synthesis_justification {
justification m_justification; // justification object produced by the synthesizer
protected:
virtual char const * get_label() const;
public:
synthesis_failure_justification(context const & ctx, expr const & mvar, expr const & type, justification const & tr, unsigned num, justification const * substs);
virtual ~synthesis_failure_justification();
virtual void get_children(buffer<justification_cell*> & r) const;
};
/**
\brief Justification object used to justify a metavar assignment produced by a synthesizer.
*/
class synthesized_assignment_justification : public synthesis_justification {
protected:
virtual char const * get_label() const;
public:
synthesized_assignment_justification(context const & ctx, expr const & mvar, expr const & type, unsigned num, justification const * substs):
synthesis_justification(ctx, mvar, type, num, substs) {
}
};
/**
\brief Justification object used to justify that we are moving to the next solution.
*/
class next_solution_justification : public justification_cell {
std::vector<justification> m_assumptions; // Set of assumptions used to derive last solution
public:
next_solution_justification(unsigned num, justification const * as);
virtual ~next_solution_justification();
virtual format pp_header(formatter const &, options const &) const;
virtual void get_children(buffer<justification_cell*> & r) const;
virtual expr const & get_main_expr() const;
};
};

2
src/library/elaborator/elaborator_plugin.h
View file

@ -27,7 +27,7 @@ public:
Each result is represented by a pair: the new metavariable
environment and a new list of constraints to be solved.
*/
virtual std::pair<metavar_env, list<unification_constraint>> next(trace const & assumption) = 0;
virtual std::pair<metavar_env, list<unification_constraint>> next(justification const & assumption) = 0;
/** \brief Interrupt the computation for the next solution. */
virtual void interrupt() = 0;
};

187
src/library/elaborator/elaborator_trace.cpp
View file

@ -1,187 +0,0 @@
/*
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 "library/elaborator/elaborator_trace.h"
namespace lean {
static void push_back(buffer<trace_cell*> & r, trace const & t) {
if (t)
r.push_back(t.raw());
}
template<typename T>
static void append(buffer<trace_cell*> & r, T const & s) {
for (auto t : s)
push_back(r, t);
}
// -------------------------
// Assumptions
// -------------------------
assumption_trace::assumption_trace(unsigned idx):m_idx(idx) {
}
void assumption_trace::get_children(buffer<trace_cell*> &) const {
}
expr const & assumption_trace::get_main_expr() const {
return expr::null();
}
format assumption_trace::pp_header(formatter const &, options const &) const {
return format{format("assumption"), space(), format(m_idx)};
}
// -------------------------
// Propagation trace
// -------------------------
propagation_trace::propagation_trace(unification_constraint const & c):
m_constraint(c) {
}
propagation_trace::~propagation_trace() {
}
void propagation_trace::get_children(buffer<trace_cell*> & r) const {
push_back(r, m_constraint.get_trace());
}
expr const & propagation_trace::get_main_expr() const {
return expr::null();
}
format propagation_trace::pp_header(formatter const & fmt, options const & opts) const {
format r;
r += format(get_prop_name());
r += compose(line(), get_constraint().pp(fmt, opts, nullptr, false));
return r;
}
// -------------------------
// Unification failure (by cases)
// -------------------------
unification_failure_by_cases_trace::unification_failure_by_cases_trace(unification_constraint const & c, unsigned num, trace const * cs):
unification_failure_trace(c),
m_cases(cs, cs + num) {
}
unification_failure_by_cases_trace::~unification_failure_by_cases_trace() {
}
void unification_failure_by_cases_trace::get_children(buffer<trace_cell*> & r) const {
push_back(r, get_constraint().get_trace());
append(r, m_cases);
}
// -------------------------
// Substitution trace
// -------------------------
substitution_trace::substitution_trace(unification_constraint const & c, trace const & t):
propagation_trace(c),
m_assignment_trace(t) {
}
substitution_trace::~substitution_trace() {
}
void substitution_trace::get_children(buffer<trace_cell*> & r) const {
propagation_trace::get_children(r);
push_back(r, m_assignment_trace);
}
multi_substitution_trace::multi_substitution_trace(unification_constraint const & c, unsigned num, trace const * ts):
propagation_trace(c),
m_assignment_traces(ts, ts + num) {
}
multi_substitution_trace::~multi_substitution_trace() {
}
void multi_substitution_trace::get_children(buffer<trace_cell*> & r) const {
propagation_trace::get_children(r);
append(r, m_assignment_traces);
}
// -------------------------
// typeof metavar trace
// -------------------------
typeof_mvar_trace::typeof_mvar_trace(context const & ctx, expr const & m, expr const & tm, expr const & t, trace const & tr):
m_context(ctx),
m_mvar(m),
m_typeof_mvar(tm),
m_type(t),
m_trace(tr) {
}
typeof_mvar_trace::~typeof_mvar_trace() {
}
format typeof_mvar_trace::pp_header(formatter const & fmt, options const & opts) const {
format r;
unsigned indent = get_pp_indent(opts);
r += format("Propagate type,");
{
format body;
body += fmt(m_context, m_mvar, false, opts);
body += space();
body += colon();
body += nest(indent, compose(line(), fmt(m_context, m_typeof_mvar, false, opts)));
r += nest(indent, compose(line(), body));
}
return group(r);
}
void typeof_mvar_trace::get_children(buffer<trace_cell*> & r) const {
push_back(r, m_trace);
}
// -------------------------
// Synthesis trace objects
// -------------------------
synthesis_trace::synthesis_trace(context const & ctx, expr const & mvar, expr const & type, unsigned num, trace const * substs):
m_context(ctx),
m_mvar(mvar),
m_type(type),
m_substitution_traces(substs, substs + num) {
}
synthesis_trace::~synthesis_trace() {
}
format synthesis_trace::pp_header(formatter const & fmt, options const & opts) const {
format r;
r += format(get_label());
r += space();
r += fmt(m_context, m_mvar, false, opts);
unsigned indent = get_pp_indent(opts);
r += nest(indent, compose(line(), fmt(m_context, m_type, true, opts)));
return r;
}
void synthesis_trace::get_children(buffer<trace_cell*> & r) const {
append(r, m_substitution_traces);
}
expr const & synthesis_trace::get_main_expr() const {
return m_mvar;
}
char const * synthesis_failure_trace::get_label() const {
return "Failed to synthesize expression of type for";
}
synthesis_failure_trace::synthesis_failure_trace(context const & ctx, expr const & mvar, expr const & type, trace const & tr, unsigned num, trace const * substs):
synthesis_trace(ctx, mvar, type, num, substs),
m_trace(tr) {
}
synthesis_failure_trace::~synthesis_failure_trace() {
}
void synthesis_failure_trace::get_children(buffer<trace_cell*> & r) const {
synthesis_trace::get_children(r);
push_back(r, m_trace);
}
char const * synthesized_assignment_trace::get_label() const {
return "Synthesized assignment for";
}
// -------------------------
// Next solution trace
// -------------------------
next_solution_trace::next_solution_trace(unsigned num, trace const * as):
m_assumptions(as, as + num) {
}
next_solution_trace::~next_solution_trace() {
}
format next_solution_trace::pp_header(formatter const &, options const &) const {
return format("next solution");
}
void next_solution_trace::get_children(buffer<trace_cell*> & r) const {
append(r, m_assumptions);
}
expr const & next_solution_trace::get_main_expr() const {
return expr::null();
}
}

229
src/library/elaborator/elaborator_trace.h
View file

@ -1,229 +0,0 @@
/*
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 <vector>
#include "kernel/trace.h"
#include "kernel/unification_constraint.h"
namespace lean {
/**
\brief Base class for trace objects used to justify case-splits.
*/
class assumption_trace : public trace_cell {
unsigned m_idx;
public:
assumption_trace(unsigned idx);
virtual void get_children(buffer<trace_cell*> &) const;
virtual expr const & get_main_expr() const;
virtual format pp_header(formatter const &, options const &) const;
};
/**
\brief Base class for justifying propagations and failures
*/
class propagation_trace : public trace_cell {
unification_constraint m_constraint;
protected:
/** \brief Auxiliary method used by pp_header to label a propagation step, subclasses must redefine it. */
virtual char const * get_prop_name() const = 0;
public:
propagation_trace(unification_constraint const & c);
virtual ~propagation_trace();
virtual void get_children(buffer<trace_cell*> & r) const;
virtual expr const & get_main_expr() const;
virtual format pp_header(formatter const &, options const &) const;
unification_constraint const & get_constraint() const { return m_constraint; }
};
/**
\brief Trace object used to mark that a particular unification constraint could not be solved.
*/
class unification_failure_trace : public propagation_trace {
protected:
virtual char const * get_prop_name() const { return "Failed to solve"; }
public:
unification_failure_trace(unification_constraint const & c):propagation_trace(c) {}
};
/**
\brief Trace object created for justifying that a constraint that
generated a case-split does not have a solution. Each case-split
corresponds to a different way of solving the constraint.
*/
class unification_failure_by_cases_trace : public unification_failure_trace {
std::vector<trace> m_cases; // why each case failed
public:
unification_failure_by_cases_trace(unification_constraint const & c, unsigned num, trace const * cs);
virtual ~unification_failure_by_cases_trace();
virtual void get_children(buffer<trace_cell*> & r) const;
};
/**
\brief Trace object used to justify a metavar assignment.
*/
class assignment_trace : public propagation_trace {
protected:
virtual char const * get_prop_name() const { return "Assignment"; }
public:
assignment_trace(unification_constraint const & c):propagation_trace(c) {}
};
/**
\brief Trace object used to justify simple structural steps when processing unification
constraints. For example, given the constraint
<tt>ctx |- (f a) == (f b)</tt>
where \c f is a variable, we must have
<tt>ctx |- a == b</tt>
The justification for the latter is a destruct trace based on the former.
*/
class destruct_trace : public propagation_trace {
protected:
virtual char const * get_prop_name() const { return "Destruct/Decompose"; }
public:
destruct_trace(unification_constraint const & c):propagation_trace(c) {}
};
/**
\brief Trace object used to justify a normalization step such as.
<tt>ctx |- (fun x : T, x) a == b</tt>
==>
<tt>ctx |- a == b</tt>
*/
class normalize_trace : public propagation_trace {
protected:
virtual char const * get_prop_name() const { return "Normalize"; }
public:
normalize_trace(unification_constraint const & c):propagation_trace(c) {}
};
/**
\brief Trace object used to justify an imitation step.
An imitation step is used when solving constraints such as:
<tt>ctx |- ?m[lift:s:n, ...] == Pi (x : A), B x</tt>
In this case, ?m must be a Pi. We make progress, by adding the constraint
<tt>ctx |- ?m == Pi (x : ?M1), (?M2 x)</tt>
where ?M1 and ?M2 are fresh metavariables.
*/
class imitation_trace : public propagation_trace {
protected:
virtual char const * get_prop_name() const { return "Imitation"; }
public:
imitation_trace(unification_constraint const & c):propagation_trace(c) {}
};
/**
\brief Trace object used to justify a new constraint obtained by substitution.
*/
class substitution_trace : public propagation_trace {
trace m_assignment_trace;
protected:
virtual char const * get_prop_name() const { return "Substitution"; }
public:
substitution_trace(unification_constraint const & c, trace const & t);
virtual ~substitution_trace();
virtual void get_children(buffer<trace_cell*> & r) const;
};
/**
\brief Trace object used to justify a new constraint obtained by multiple substitution.
*/
class multi_substitution_trace : public propagation_trace {
std::vector<trace> m_assignment_traces;
protected:
virtual char const * get_prop_name() const { return "Substitution"; }
public:
multi_substitution_trace(unification_constraint const & c, unsigned num, trace const * ts);
virtual ~multi_substitution_trace();
virtual void get_children(buffer<trace_cell*> & r) const;
};
/**
\brief Trace object used to justify a <tt>typeof(m) == t</tt> constraint generated when
we assign a metavariable \c m.
*/
class typeof_mvar_trace : public trace_cell {
context m_context;
expr m_mvar;
expr m_typeof_mvar;
expr m_type;
trace m_trace;
public:
typeof_mvar_trace(context const & ctx, expr const & m, expr const & mt, expr const & t, trace const & tr);
virtual ~typeof_mvar_trace();
virtual format pp_header(formatter const &, options const &) const;
virtual void get_children(buffer<trace_cell*> & r) const;
};
/**
\brief Base class for synthesis_failure_trace and synthesized_assignment_trace
*/
class synthesis_trace : public trace_cell {
context m_context;
expr m_mvar;
expr m_type;
std::vector<trace> m_substitution_traces; // trace objects justifying the assignments used to instantiate \c m_type and \c m_context.
protected:
virtual char const * get_label() const = 0;
public:
synthesis_trace(context const & ctx, expr const & mvar, expr const & type, unsigned num, trace const * substs);
virtual ~synthesis_trace();
virtual format pp_header(formatter const &, options const &) const;
virtual void get_children(buffer<trace_cell*> & r) const;
virtual expr const & get_main_expr() const;
};
/**
\brief Trace object for justifying why a synthesis step failed.
A synthesis step is of the form
<tt>ctx |- ?mvar : type</tt>
Before invoking the synthesizer, the elaborator substitutes the
metavariables in \c ctx and \c type with their corresponding assignments.
*/
class synthesis_failure_trace : public synthesis_trace {
trace m_trace; // trace object produced by the synthesizer
protected:
virtual char const * get_label() const;
public:
synthesis_failure_trace(context const & ctx, expr const & mvar, expr const & type, trace const & tr, unsigned num, trace const * substs);
virtual ~synthesis_failure_trace();
virtual void get_children(buffer<trace_cell*> & r) const;
};
/**
\brief Trace object used to justify a metavar assignment produced by a synthesizer.
*/
class synthesized_assignment_trace : public synthesis_trace {
protected:
virtual char const * get_label() const;
public:
synthesized_assignment_trace(context const & ctx, expr const & mvar, expr const & type, unsigned num, trace const * substs):
synthesis_trace(ctx, mvar, type, num, substs) {
}
};
/**
\brief Trace object used to justify that we are moving to the next solution.
*/
class next_solution_trace : public trace_cell {
std::vector<trace> m_assumptions; // Set of assumptions used to derive last solution
public:
next_solution_trace(unsigned num, trace const * as);
virtual ~next_solution_trace();
virtual format pp_header(formatter const &, options const &) const;
virtual void get_children(buffer<trace_cell*> & r) const;
virtual expr const & get_main_expr() const;
};
};

14
src/library/type_inferer.cpp
View file

@ -10,7 +10,7 @@ Author: Leonardo de Moura
#include "kernel/normalizer.h"
#include "kernel/builtin.h"
#include "kernel/kernel_exception.h"
#include "kernel/type_checker_trace.h"
#include "kernel/type_checker_justification.h"
#include "kernel/instantiate.h"
#include "kernel/free_vars.h"
#include "kernel/metavar.h"
@ -47,8 +47,8 @@ class type_inferer::imp {
if (u == Bool)
return Type();
if (has_metavar(u) && m_menv) {
trace tr = mk_type_expected_trace(ctx, s);
m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, tr));
justification jst = mk_type_expected_justification(ctx, s);
m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, jst));
return u;
}
throw type_expected_exception(m_env, ctx, s);
@ -70,8 +70,8 @@ class type_inferer::imp {
expr A = m_menv->mk_metavar(ctx);
expr B = m_menv->mk_metavar(ctx);
expr p = mk_pi(g_x_name, A, B(Var(0)));
trace tr = mk_function_expected_trace(ctx, e);
m_uc->push_back(mk_eq_constraint(ctx, t, p, tr));
justification jst = mk_function_expected_justification(ctx, e);
m_uc->push_back(mk_eq_constraint(ctx, t, p, jst));
t = abst_body(p);
} else {
throw function_expected_exception(m_env, ctx, e);
@ -186,9 +186,9 @@ class type_inferer::imp {
r = mk_type(max(ty_level(t1), ty_level(t2)));
} else {
lean_assert(m_uc);
trace tr = mk_max_type_trace(ctx, e);
justification jst = mk_max_type_justification(ctx, e);
r = m_menv->mk_metavar(ctx);
m_uc->push_back(mk_max_constraint(ctx, t1, t2, r, tr));
m_uc->push_back(mk_max_constraint(ctx, t1, t2, r, jst));
}
break;
}

18
src/tests/kernel/type_checker.cpp
View file

@ -18,7 +18,7 @@ Author: Leonardo de Moura
#include "kernel/normalizer.h"
#include "kernel/printer.h"
#include "kernel/kernel_exception.h"
#include "kernel/type_checker_trace.h"
#include "kernel/type_checker_justification.h"
#include "library/basic_thms.h"
#include "library/arith/arith.h"
#include "library/all/all.h"
@ -297,7 +297,7 @@ static void tst15() {
lean_assert(is_eqp(r, checker.infer_type(F, ctx1)));
}
static void check_trace_msg(trace const & t, char const * expected) {
static void check_justification_msg(justification const & t, char const * expected) {
formatter fmt = mk_simple_formatter();
options opts;
opts = opts.update({"pp", "indent"}, 2);
@ -309,18 +309,18 @@ static void check_trace_msg(trace const & t, char const * expected) {
}
static void tst16() {
std::cout << "Testing type checker trace objects\n";
std::cout << "Testing type checker justification objects\n";
context ctx;
expr f = Const("f");
expr a = Const("a");
expr x = Var(0);
ctx = extend(ctx, "x", Const("N"));
check_trace_msg(mk_function_expected_trace(ctx, f(a, x)), "Function expected at\n f a x");
check_trace_msg(mk_type_expected_trace(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n N -> x");
check_trace_msg(mk_type_expected_trace(ctx, Pi({a, Const("N")}, Var(1)(a))), "Type expected at\n Pi a : N, (x a)");
check_trace_msg(mk_app_type_match_trace(ctx, f(a, x), 1), "Type of argument 1 must be convertible to the expected type in the application of\n f\nwith arguments:\n a\n x");
check_trace_msg(mk_max_type_trace(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n N -> x");
check_trace_msg(mk_def_type_match_trace(ctx, "foo", f(a, x)), "Type of definition 'foo' must be convertible to expected type.");
check_justification_msg(mk_function_expected_justification(ctx, f(a, x)), "Function expected at\n f a x");
check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n N -> x");
check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1)(a))), "Type expected at\n Pi a : N, (x a)");
check_justification_msg(mk_app_type_match_justification(ctx, f(a, x), 1), "Type of argument 1 must be convertible to the expected type in the application of\n f\nwith arguments:\n a\n x");
check_justification_msg(mk_max_type_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n N -> x");
check_justification_msg(mk_def_type_match_justification(ctx, "foo", f(a, x)), "Type of definition 'foo' must be convertible to expected type.");
}
int main() {

26
src/tests/library/elaborator/elaborator.cpp
View file

@ -51,9 +51,9 @@ static void tst1() {
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
expr int_id = Fun({a, Int}, a);
expr nat_id = Fun({a, Nat}, a);
ucs.push_back(mk_choice_constraint(context(), m1, { int_id, mk_int_to_real_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m2, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m1, { int_id, mk_int_to_real_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m2, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
substitution s = elb.next();
}
@ -93,9 +93,9 @@ static void tst2() {
expr F = m1(g(m2, m3(a)), m4(nVal(0)));
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m1, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m1, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
substitution s = elb.next();
}
@ -136,9 +136,9 @@ static void tst3() {
expr F = Fun({x, m1}, m2(f(m3, x), m4(nVal(10))))(m5(a));
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m2, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m5, { int_id, mk_int_to_real_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m2, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m5, { int_id, mk_int_to_real_fn() }, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
substitution s = elb.next();
}
@ -181,8 +181,8 @@ static void tst4() {
expr F = Fun({{x, m1}, {y, m2}}, m3(f(m4, x), f(m5, y)))(m6(a), b);
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m3, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m6, { int_id, mk_int_to_real_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m3, { mk_nat_le_fn(), mk_int_le_fn(), mk_real_le_fn() }, justification()));
ucs.push_back(mk_choice_constraint(context(), m6, { int_id, mk_int_to_real_fn() }, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
substitution s = elb.next();
}
@ -223,7 +223,7 @@ static void tst5() {
expr F = Fun({{x, m1}, {y, m2}}, f(m3, x, y))(m4(a), b);
std::cout << F << "\n";
std::cout << checker.infer_type(F, context(), &menv, ucs) << "\n";
ucs.push_back(mk_choice_constraint(context(), m4, { int_id, mk_int_to_real_fn() }, trace()));
ucs.push_back(mk_choice_constraint(context(), m4, { int_id, mk_int_to_real_fn() }, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
substitution s = elb.next();
}
@ -260,7 +260,7 @@ static void tst6() {
expr V = Subst(m1, m2, m3, m4, H1, H2);
expr expected = Eq(f(a, f(b, b)), a);
expr given = checker.infer_type(V, context(), &menv, ucs);
ucs.push_back(mk_eq_constraint(context(), expected, given, trace()));
ucs.push_back(mk_eq_constraint(context(), expected, given, justification()));
elaborator elb(env, menv, ucs.size(), ucs.data());
substitution s = elb.next();
std::cout << beta_reduce(instantiate_metavars(V, s)) << "\n";