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

refactor(frontends/lean/elaborator): rename choice_elaborator to choice_iterator and move to separate module

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-10 11:19:14 -07:00
parent e128610711
commit 669b1bff45
8 changed files with 131 additions and 91 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -6,6 +6,6 @@ decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp
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)
local_context.cpp choice_iterator.cpp)
target_link_libraries(lean_frontend ${LEAN_LIBS})

27
src/frontends/lean/choice_iterator.cpp Normal file
View file

@ -0,0 +1,27 @@
/*
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 "frontends/lean/choice_iterator.h"
namespace lean {
lazy_list<constraints> choose(std::shared_ptr<choice_iterator> c, bool ignore_failure) {
return mk_lazy_list<constraints>([=]() {
auto s = c->next();
if (s) {
return some(mk_pair(*s, choose(c, false)));
} else if (ignore_failure) {
// return singleton empty list of constraints, and let tactic hints try to instantiate the metavariable.
return lazy_list<constraints>::maybe_pair(constraints(), lazy_list<constraints>());
} else {
return lazy_list<constraints>::maybe_pair();
}
});
}
lazy_list<constraints> choose(std::shared_ptr<choice_iterator> c) {
return choose(c, c->ignore_failure());
}
}

28
src/frontends/lean/choice_iterator.h Normal file
View file

@ -0,0 +1,28 @@
/*
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 "util/lazy_list.h"
#include "kernel/constraint.h"
namespace lean {
/** \brief Abstract (helper) class for creating lazy_list<constraints> */
class choice_iterator {
bool m_ignore_failure;
public:
choice_iterator(bool ignore_failure = false):m_ignore_failure(ignore_failure) {}
virtual ~choice_iterator() {}
virtual optional<constraints> next() = 0;
bool ignore_failure() const { return m_ignore_failure; }
};
/** \brief Convert a choice_iterator into a lazy_list<constraints>
The lazy list is generated by invoking the method \c choice_iterator::next.
If c->ignore_failure() is true AND \c c does not produce any result,
then the singleton lazy_list is produced with an empty set of constraints.
*/
lazy_list<constraints> choose(std::shared_ptr<choice_iterator> c);
}

32
src/frontends/lean/class.cpp
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include "library/kernel_serializer.h"
#include "library/opaque_hints.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/tactic_hint.h"
namespace lean {
struct class_entry {
@ -151,4 +152,35 @@ void register_class_cmds(cmd_table & r) {
add_cmd(r, cmd_info("instance", "add a new instance", add_instance_cmd));
add_cmd(r, cmd_info("class", "add a new class", add_class_cmd));
}
/** \brief Return true iff \c type is a class or Pi that produces a class. */
optional<name> is_ext_class(type_checker & tc, expr type) {
type = tc.whnf(type).first;
if (is_pi(type)) {
return is_ext_class(tc, instantiate(binding_body(type), mk_local(tc.mk_fresh_name(), binding_domain(type))));
} else {
expr f = get_app_fn(type);
if (!is_constant(f))
return optional<name>();
name const & cls_name = const_name(f);
if (is_class(tc.env(), cls_name) || !empty(get_tactic_hints(tc.env(), cls_name)))
return optional<name>(cls_name);
else
return optional<name>();
}
}
/** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */
list<expr> get_local_instances(type_checker & tc, list<expr> const & ctx, name const & cls_name) {
buffer<expr> buffer;
for (auto const & l : ctx) {
if (!is_local(l))
continue;
expr inst_type = mlocal_type(l);
if (auto it = is_ext_class(tc, inst_type))
if (*it == cls_name)
buffer.push_back(l);
}
return to_list(buffer.begin(), buffer.end());
}
}

6
src/frontends/lean/class.h
View file

@ -21,4 +21,10 @@ bool is_class(environment const & env, name const & c);
list<name> get_class_instances(environment const & env, name const & c);
name get_class_name(environment const & env, expr const & e);
void register_class_cmds(cmd_table & r);
/** \brief Return true iff \c type is a class or Pi that produces a class. */
optional<name> is_ext_class(type_checker & tc, expr type);
/** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */
list<expr> get_local_instances(type_checker & tc, list<expr> const & ctx, name const & cls_name);
}

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

@ -41,6 +41,7 @@ Author: Leonardo de Moura
#include "frontends/lean/no_info.h"
#include "frontends/lean/extra_info.h"
#include "frontends/lean/local_context.h"
#include "frontends/lean/choice_iterator.h"
#ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES
#define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true
@ -62,37 +63,6 @@ elaborator_context::elaborator_context(environment const & env, io_state const &
m_use_local_instances = get_elaborator_local_instances(ios.get_options());
}
/** \brief Return true iff \c type is a class or Pi that produces a class. */
optional<name> is_ext_class(type_checker & tc, expr type) {
type = tc.whnf(type).first;
if (is_pi(type)) {
return is_ext_class(tc, instantiate(binding_body(type), mk_local(tc.mk_fresh_name(), binding_domain(type))));
} else {
expr f = get_app_fn(type);
if (!is_constant(f))
return optional<name>();
name const & cls_name = const_name(f);
if (is_class(tc.env(), cls_name) || !empty(get_tactic_hints(tc.env(), cls_name)))
return optional<name>(cls_name);
else
return optional<name>();
}
}
/** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */
list<expr> get_local_instances(type_checker & tc, list<expr> const & ctx, name const & cls_name) {
buffer<expr> buffer;
for (auto const & l : ctx) {
if (!is_local(l))
continue;
expr inst_type = mlocal_type(l);
if (auto it = is_ext_class(tc, inst_type))
if (*it == cls_name)
buffer.push_back(l);
}
return to_list(buffer.begin(), buffer.end());
}
typedef std::unique_ptr<type_checker> type_checker_ptr;
/** \brief Helper class for implementing the \c elaborate functions. */
@ -162,19 +132,13 @@ class elaborator {
}
};
struct choice_elaborator {
bool m_ignore_failure;
choice_elaborator(bool ignore_failure = false):m_ignore_failure(ignore_failure) {}
virtual optional<constraints> next() = 0;
};
/** \brief 'Choice' expressions <tt>(choice e_1 ... e_n)</tt> are mapped into a metavariable \c ?m
and a choice constraints <tt>(?m in fn)</tt> where \c fn is a choice function.
The choice function produces a stream of alternatives. In this case, it produces a stream of
size \c n, one alternative for each \c e_i.
This is a helper class for implementing this choice functions.
*/
struct choice_expr_elaborator : public choice_elaborator {
struct choice_expr_elaborator : public choice_iterator {
elaborator & m_elab;
expr m_mvar;
expr m_choice;
@ -221,7 +185,7 @@ class elaborator {
This is a helper class for implementing this choice function.
*/
struct placeholder_elaborator : public choice_elaborator {
struct placeholder_elaborator : public choice_iterator {
elaborator & m_elab;
expr m_meta;
expr m_meta_type; // elaborated type of the metavariable
@ -238,7 +202,7 @@ class elaborator {
placeholder_elaborator(elaborator & elab, expr const & meta, expr const & meta_type,
list<expr> const & local_insts, list<name> const & instances, list<tactic_hint_entry> const & tacs,
saved_state const & s, justification const & j, bool ignore_failure, bool relax):
choice_elaborator(ignore_failure),
choice_iterator(ignore_failure),
m_elab(elab), m_meta(meta), m_meta_type(meta_type), m_local_instances(local_insts), m_instances(instances),
m_tactics(tacs), m_state(s), m_jst(j), m_relax_main_opaque(relax) {
collect_metavars(meta_type, m_mvars_in_meta_type);
@ -337,20 +301,6 @@ class elaborator {
}
};
lazy_list<constraints> choose(std::shared_ptr<choice_elaborator> c) {
return mk_lazy_list<constraints>([=]() {
auto s = c->next();
if (s) {
return some(mk_pair(*s, choose(c)));
} else if (c->m_ignore_failure) {
// return singleton empty list of constraints, and let tactic hints try to instantiate the metavariable.
return lazy_list<constraints>::maybe_pair(constraints(), lazy_list<constraints>());
} else {
return lazy_list<constraints>::maybe_pair();
}
});
}
public:
elaborator(elaborator_context & env, list<expr> const & ctx, name_generator const & ngen):
m_env(env),
@ -453,36 +403,16 @@ public:
m_pre_info_data.clear();
}
static expr instantiate_meta(expr const & meta, substitution & subst) {
buffer<expr> locals;
expr mvar = get_app_args(meta, locals);
mvar = update_mlocal(mvar, subst.instantiate_all(mlocal_type(mvar)));
for (auto & local : locals) local = subst.instantiate_all(local);
return ::lean::mk_app(mvar, locals);
}
/** \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(expr const & m) {
environment _env = env();
return mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
substitution tmp(subst);
expr new_m = instantiate_meta(m, tmp);
expr new_type = type_checker(_env).infer(new_m).first;
proof_state ps(goals(goal(new_m, new_type)), substitution(), name_generator("dontcare"));
return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
});
}
/** \brief Create a metavariable, and attach choice constraint for generating
solutions using class-instances and tactic-hints.
*/
expr mk_placeholder_meta(optional<expr> const & type, tag g, bool is_strict, constraint_seq & cs) {
expr m = m_context.mk_meta(type, g);
saved_state st(*this);
justification j = mk_failed_to_synthesize_jst(m);
justification j = mk_failed_to_synthesize_jst(env(), m);
bool relax = m_relax_main_opaque;
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, name_generator const & /* ngen */) {
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
name_generator const & /* ngen */) {
expr const & mvar = get_app_fn(meta);
if (auto cls_name_it = is_ext_class(*m_tc[relax], meta_type)) {
name cls_name = *cls_name_it;
@ -633,7 +563,7 @@ public:
return a;
}
struct coercion_case_split {
struct coercion_case_split : public choice_iterator {
elaborator & m_elab;
expr m_arg;
bool m_id; // true if identity was not tried yet
@ -662,21 +592,11 @@ public:
}
};
lazy_list<constraints> choose(std::shared_ptr<coercion_case_split> c) {
return mk_lazy_list<constraints>([=]() {
auto s = c->next();
if (s) {
return some(mk_pair(*s, choose(c)));
} else {
return lazy_list<constraints>::maybe_pair();
}
});
}
constraint mk_delayed_coercion_cnstr(expr const & m, expr const & a, expr const & a_type,
justification const & j, unsigned delay_factor) {
bool relax = m_relax_main_opaque;
auto choice_fn = [=](expr const & mvar, expr const & d_type, substitution const & s, name_generator const & /* ngen */) {
auto choice_fn = [=](expr const & mvar, expr const & d_type, substitution const & s,
name_generator const & /* ngen */) {
type_checker & tc = *m_tc[relax];
expr new_a_type;
justification new_a_type_jst;

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

@ -205,4 +205,24 @@ expr univ_metavars_to_params(environment const & env, local_decls<level> const &
name_set & ps, buffer<name> & new_ps, expr const & e) {
return univ_metavars_to_params_fn(env, lls, s, ps, new_ps)(e);
}
expr instantiate_meta(expr const & meta, substitution & subst) {
lean_assert(is_meta(meta));
buffer<expr> locals;
expr mvar = get_app_args(meta, locals);
mvar = update_mlocal(mvar, subst.instantiate_all(mlocal_type(mvar)));
for (auto & local : locals)
local = subst.instantiate_all(local);
return mk_app(mvar, locals);
}
justification mk_failed_to_synthesize_jst(environment const & env, expr const & m) {
return mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
substitution tmp(subst);
expr new_m = instantiate_meta(m, tmp);
expr new_type = type_checker(env).infer(new_m).first;
proof_state ps(goals(goal(new_m, new_type)), substitution(), name_generator("dontcare"));
return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
});
}
}

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

@ -40,4 +40,11 @@ bool occurs(level const & u, level const & l);
*/
expr univ_metavars_to_params(environment const & env, local_decls<level> const & lls, substitution & s,
name_set & ps, buffer<name> & new_ps, expr const & e);
/** \brief Instantiate metavariable application \c meta (?M ...) using \c subst */
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);
}