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

feat(frontends/lean/elaborator): constraints associated with 'proof-qed'

Browse source 
blocks are solved independently, closes #82
This commit is contained in:
Leonardo de Moura 2014-09-13 10:21:10 -07:00
parent 8c8c9d1c4a
commit d647954f93
11 changed files with 156 additions and 50 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/CMakeLists.txt
View file

@ -7,6 +7,6 @@ dependencies.cpp parser_bindings.cpp begin_end_ext.cpp
class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
structure_cmd.cpp info_manager.cpp no_info.cpp extra_info.cpp
local_context.cpp choice_iterator.cpp placeholder_elaborator.cpp
coercion_elaborator.cpp)
coercion_elaborator.cpp proof_qed_elaborator.cpp)
target_link_libraries(lean_frontend ${LEAN_LIBS})

38
src/frontends/lean/elaborator.cpp
View file

@ -45,6 +45,7 @@ Author: Leonardo de Moura
#include "frontends/lean/choice_iterator.h"
#include "frontends/lean/placeholder_elaborator.h"
#include "frontends/lean/coercion_elaborator.h"
#include "frontends/lean/proof_qed_elaborator.h"
#ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES
#define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true
@ -153,11 +154,11 @@ class elaborator : public coercion_info_manager {
};
public:
elaborator(elaborator_context & env, list<expr> const & ctx, name_generator const & ngen):
elaborator(elaborator_context & env, name_generator const & ngen):
m_env(env),
m_ngen(ngen),
m_context(m_ngen.next(), ctx),
m_full_context(m_ngen.next(), ctx),
m_context(m_ngen.next()),
m_full_context(m_ngen.next()),
m_unifier_config(env.m_ios.get_options(), true /* use exceptions */, true /* discard */) {
m_relax_main_opaque = false;
m_no_info = false;
@ -326,10 +327,13 @@ public:
return m;
}
expr visit_proof_qed(expr const & e, optional<expr> const & /* t */, constraint_seq & cs) {
expr visit_proof_qed(expr const & e, optional<expr> const & t, constraint_seq & cs) {
lean_assert(is_proof_qed_annotation(e));
// TODO(Leo)
return visit(get_annotation_arg(e), cs);
pair<expr, constraint_seq> ecs = visit(get_annotation_arg(e));
pair<expr, constraint> mc = mk_proof_qed_elaborator(env(), m_full_context, ecs.first, t, ecs.second,
m_unifier_config, m_relax_main_opaque);
cs += mc.second;
return mc.first;
}
/** \brief Make sure \c f is really a function, if it is not, try to apply coercions.
@ -642,18 +646,7 @@ public:
constraint_seq v_cs;
expr v = visit(get_typed_expr_expr(e), v_cs);
expr v_type = infer_type(v, v_cs);
justification j = mk_justification(e, [=](formatter const & fmt, substitution const & subst) {
substitution s(subst);
format expected_fmt, given_fmt;
std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, s.instantiate(t), s.instantiate(v_type));
format r("type mismatch at term");
r += pp_indent_expr(fmt, s.instantiate(v));
r += compose(line(), format("has type"));
r += given_fmt;
r += compose(line(), format("but is expected to have type"));
r += expected_fmt;
return r;
});
justification j = mk_type_mismatch_jst(v, v_type, t, e);
auto new_vcs = ensure_has_type(v, v_type, t, j, m_relax_main_opaque);
v = new_vcs.first;
cs += t_cs + new_vcs.second + v_cs;
@ -914,7 +907,10 @@ public:
return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end()));
}
std::tuple<expr, level_param_names> operator()(expr const & e, bool _ensure_type, bool relax_main_opaque) {
std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type,
bool relax_main_opaque) {
m_context.set_ctx(ctx);
m_full_context.set_ctx(ctx);
flet<bool> set_relax(m_relax_main_opaque, relax_main_opaque && !get_hide_main_opaque(env()));
constraint_seq cs;
expr r = visit(e, cs);
@ -961,11 +957,11 @@ static name g_tmp_prefix = name::mk_internal_unique_name();
std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,
bool relax_main_opaque, bool ensure_type) {
return elaborator(env, ctx, name_generator(g_tmp_prefix))(e, ensure_type, relax_main_opaque);
return elaborator(env, name_generator(g_tmp_prefix))(ctx, e, ensure_type, relax_main_opaque);
}
std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v,
bool is_opaque) {
return elaborator(env, list<expr>(), name_generator(g_tmp_prefix))(t, v, n, is_opaque);
return elaborator(env, name_generator(g_tmp_prefix))(t, v, n, is_opaque);
}
}

1
src/frontends/lean/local_context.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "frontends/lean/local_context.h"
namespace lean {
local_context::local_context(name const & prefix):m_ngen(prefix) {}
local_context::local_context(name const & prefix, list<expr> const & ctx):
m_ngen(prefix) {
set_ctx(ctx);

1
src/frontends/lean/local_context.h
View file

@ -22,6 +22,7 @@ class local_context {
buffer<expr> m_ctx_buffer; // m_ctx as a buffer
buffer<expr> m_ctx_domain_buffer; // m_ctx_domain_buffer[i] == abstract_locals(m_ctx_buffer[i], i, m_ctx_buffer.beg
public:
local_context(name const & prefix);
local_context(name const & prefix, list<expr> const & ctx);
void set_ctx(list<expr> const & ctx);

19
src/frontends/lean/placeholder_elaborator.cpp
View file

@ -250,25 +250,6 @@ pair<expr, constraint> mk_placeholder_elaborator(std::shared_ptr<placeholder_con
return mk_pair(m, c);
}
/** \brief Given a metavariable application (?m l_1 ... l_n), apply \c s to the types of
?m and local constants l_i
Return the updated expression and a justification for all substitutions.
*/
static pair<expr, justification> update_meta(expr const & meta, substitution s) {
buffer<expr> args;
expr mvar = get_app_args(meta, args);
justification j;
auto p = s.instantiate_metavars(mlocal_type(mvar));
mvar = update_mlocal(mvar, p.first);
j = p.second;
for (expr & arg : args) {
auto p = s.instantiate_metavars(mlocal_type(arg));
arg = update_mlocal(arg, p.first);
j = mk_composite1(j, p.second);
}
return mk_pair(mk_app(mvar, args), j);
}
constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const & C, expr const & m, bool is_strict,
unifier_config const & cfg, unsigned delay_factor) {
environment const & env = C->env();

62
src/frontends/lean/proof_qed_elaborator.cpp Normal file
View file

@ -0,0 +1,62 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/unifier.h"
#include "library/opaque_hints.h"
#include "library/metavar_closure.h"
#include "frontends/lean/util.h"
#include "frontends/lean/local_context.h"
namespace lean {
constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr const & e,
constraint_seq const & cs, unifier_config const & cfg, bool relax) {
justification j = mk_failed_to_synthesize_jst(env, m);
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
name_generator const & _ngen) {
name_generator ngen(_ngen);
type_checker_ptr tc(mk_type_checker_with_hints(env, ngen.mk_child(), relax));
pair<expr, constraint_seq> tcs = tc->infer(e);
expr e_type = tcs.first;
justification new_j = mk_type_mismatch_jst(e, e_type, meta_type);
pair<bool, constraint_seq> dcs = tc->is_def_eq(e_type, meta_type, new_j);
if (!dcs.first)
throw unifier_exception(new_j, s);
constraint_seq new_cs = cs + tcs.second + dcs.second;
buffer<constraint> cs_buffer;
new_cs.linearize(cs_buffer);
cs_buffer.push_back(mk_eq_cnstr(meta, e, j, relax));
unifier_config new_cfg(cfg);
new_cfg.m_discard = false;
unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, new_cfg);
auto p = seq.pull();
lean_assert(p);
substitution new_s = p->first.first;
constraints postponed = map(p->first.second,
[&](constraint const & c) {
// we erase internal justifications
return update_justification(c, j);
});
metavar_closure cls(meta);
cls.add(meta_type);
constraints r = cls.mk_constraints(new_s, j, relax);
return append(r, postponed);
};
bool owner = false;
return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j, relax);
}
/** \brief Create a metavariable m, and attach "choice" constraint that postpone the
solving the constraints <tt>(cs union m =?= e)</tt>.
*/
pair<expr, constraint> mk_proof_qed_elaborator(
environment const & env, local_context & ctx,
expr const & e, optional<expr> const & type, constraint_seq const & cs,
unifier_config const & cfg, bool relax) {
expr m = ctx.mk_meta(type, e.get_tag());
constraint c = mk_proof_qed_cnstr(env, m, e, cs, cfg, relax);
return mk_pair(m, c);
}
}

17
src/frontends/lean/proof_qed_elaborator.h Normal file
View file

@ -0,0 +1,17 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/unifier.h"
namespace lean {
/** \brief Create a metavariable m, and attach "choice" constraint that postpone the
solving the constraints <tt>(cs union m =?= e)</tt>.
*/
pair<expr, constraint> mk_proof_qed_elaborator(environment const & env, local_context & ctx,
expr const & e, optional<expr> const & type, constraint_seq const & cs,
unifier_config const & cfg, bool relax);
}

31
src/frontends/lean/util.cpp
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/replace_fn.h"
#include "kernel/error_msgs.h"
#include "kernel/for_each_fn.h"
#include "library/scoped_ext.h"
#include "library/locals.h"
@ -226,4 +227,34 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const &
return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
});
}
justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr const & t, expr const & src) {
return mk_justification(src, [=](formatter const & fmt, substitution const & subst) {
substitution s(subst);
format expected_fmt, given_fmt;
std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, s.instantiate(t), s.instantiate(v_type));
format r("type mismatch at term");
r += pp_indent_expr(fmt, s.instantiate(v));
r += compose(line(), format("has type"));
r += given_fmt;
r += compose(line(), format("but is expected to have type"));
r += expected_fmt;
return r;
});
}
pair<expr, justification> update_meta(expr const & meta, substitution s) {
buffer<expr> args;
expr mvar = get_app_args(meta, args);
justification j;
auto p = s.instantiate_metavars(mlocal_type(mvar));
mvar = update_mlocal(mvar, p.first);
j = p.second;
for (expr & arg : args) {
auto p = s.instantiate_metavars(mlocal_type(arg));
arg = update_mlocal(arg, p.first);
j = mk_composite1(j, p.second);
}
return mk_pair(mk_app(mvar, args), j);
}
}

14
src/frontends/lean/util.h
View file

@ -49,4 +49,18 @@ expr instantiate_meta(expr const & meta, substitution & subst);
/** \brief Return a 'failed to synthesize placholder' justification for the given
metavariable application \c m of the form (?m l_1 ... l_k) */
justification mk_failed_to_synthesize_jst(environment const & env, expr const & m);
/** \brief Return a justification for \c v_type being definitionally equal to \c t,
<tt> v : v_type</tt>, the expressiong \c src is used to extract position information.
*/
justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr const & t, expr const & src);
inline justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr const & t) {
return mk_type_mismatch_jst(v, v_type, t, v);
}
/** \brief Given a metavariable application (?m l_1 ... l_n), apply \c s to the types of
?m and local constants l_i
Return the updated expression and a justification for all substitutions.
*/
pair<expr, justification> update_meta(expr const & meta, substitution s);
}

6
src/library/unifier.cpp
View file

@ -245,9 +245,9 @@ unify_status unify_simple(substitution & s, constraint const & c) {
}
static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification(), false);
static unsigned g_group_size = 1u << 29;
constexpr unsigned g_num_groups = 7;
static unsigned g_cnstr_group_first_index[g_num_groups] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size, 6*g_group_size};
static unsigned g_group_size = 1u << 28;
constexpr unsigned g_num_groups = 8;
static unsigned g_cnstr_group_first_index[g_num_groups] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size, 6*g_group_size, 7*g_group_size};
static unsigned get_group_first_index(cnstr_group g) {
return g_cnstr_group_first_index[static_cast<unsigned>(g)];
}

15
src/library/unifier.h
View file

@ -53,7 +53,8 @@ unify_result_seq unify(environment const & env, expr const & lhs, expr const & r
substitution const & s = substitution(), unifier_config const & c = unifier_config());
/**
The unifier divides the constraints in 8 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, FlexFlex, MaxDelayed
The unifier divides the constraints in 9 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance,
Epilogue, FlexFlex, MaxDelayed
1) Simple: constraints that never create case-splits. Example: pattern matching constraints (?M l_1 ... l_n) =?= t.
The are not even inserted in the constraint priority queue.
@ -71,13 +72,15 @@ unify_result_seq unify(environment const & env, expr const & lhs, expr const & r
6) ClassInstance: for delayed choice constraints (we use this group for class-instance).
7) FlexFlex: (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other
ones instantiate ?m1 or ?m2. If this kind of constraint is the next to be processed in the queue, then
we simply discard it.
7) Epilogue: constraints that must be solved before FlexFlex are discarded/postponed.
8) MaxDelayed: maximally delayed constraint group
8) FlexFlex: (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other
ones instantiate ?m1 or ?m2. If this kind of constraint is the next to be processed in the queue, then
we simply discard it (or save it and return to the caller as residue).
9) MaxDelayed: maximally delayed constraint group
*/
enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, FlexFlex, MaxDelayed };
enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, Epilogue, FlexFlex, MaxDelayed };
inline unsigned to_delay_factor(cnstr_group g) { return static_cast<unsigned>(g); }
class unifier_exception : public exception {