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

refactor(frontends/lean/builtin_cmds): cleanup 'check' command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-14 04:25:53 +01:00
parent 5c51be4585
commit 195429611b
3 changed files with 25 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/frontends/lean/builtin_cmds.cpp
View file

@ -82,24 +82,15 @@ environment end_scoped_cmd(parser & p) {
environment check_cmd(parser & p) {
expr e = p.parse_expr();
buffer<expr> section_ps;
expr_struct_set locals;
collect_locals(e, locals);
sort_section_params(locals, p, section_ps);
e = p.lambda_abstract(section_ps, e);
buffer<expr> locals;
e = abstract_locals(e, p, locals);
level_param_names ls = to_level_param_names(collect_univ_params(e));
level_param_names new_ls;
std::tie(e, new_ls) = p.elaborate_relaxed(e);
auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen());
expr type = tc->check(e, append(ls, new_ls));
// consume sections_ps introduced with mk_section_params
for (unsigned i = 0; i < section_ps.size(); i++) {
lean_assert(is_lambda(e));
lean_assert(is_pi(type));
expr local = section_ps[i];
e = instantiate(binding_body(e), local);
type = instantiate(binding_body(type), local);
}
e = instantiate_locals(e, locals);
type = instantiate_locals(type, locals);
auto reg = p.regular_stream();
formatter const & fmt = reg.get_formatter();
options opts = p.ios().get_options();

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

@ -6,6 +6,8 @@ Author: Leonardo de Moura
*/
#include <algorithm>
#include "util/sstream.h"
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "library/scoped_ext.h"
#include "library/locals.h"
#include "frontends/lean/parser.h"
@ -56,4 +58,19 @@ void collect_section_locals(expr const & type, expr const & value, parser const
collect_locals(value, ls);
sort_section_params(ls, p, section_ps);
}
expr abstract_locals(expr const & e, parser const & p, buffer<expr> & locals) {
expr_struct_set ls;
collect_locals(e, ls);
sort_section_params(ls, p, locals);
return Fun(locals, e);
}
expr instantiate_locals(expr const & b, buffer<expr> & locals) {
expr _b = b;
unsigned sz = locals.size();
for (unsigned i = 0; i < sz; i++)
_b = binding_body(_b);
return instantiate_rev(_b, locals.size(), locals.data());
}
}

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

@ -19,4 +19,8 @@ levels collect_section_levels(level_param_names const & ls, parser & p);
void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer<expr> & section_ps);
/** \brief Copy the local parameters to \c section_ps, then sort \c section_ps (using the order in which they were declared). */
void sort_section_params(expr_struct_set const & locals, parser const & p, buffer<expr> & section_ps);
/** \brief collect all locals in \c e and store and locals, and return Fun(locals, e) */
expr abstract_locals(expr const & e, parser const & p, buffer<expr> & locals);
/** \brief 'inverse' of \c abstract_locals, given a binding \c b instantiate it using locals */
expr instantiate_locals(expr const & b, buffer<expr> & locals);
}