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

perf(library/unifier): improve performance of instantiate_meta method

Browse source 
It provides a significant performance boost in some files.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-22 15:44:54 -07:00
parent 5ad6d5cbc4
commit 697bcf4b4f
1 changed files with 14 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/library/unifier.cpp
View file

@ -552,17 +552,20 @@ struct unifier_fn {
return Continue;
}
expr instantiate_meta(expr const & e, justification & j) {
expr const & f = get_app_fn(e);
if (!is_metavar(f))
return e;
auto r = m_subst.d_instantiate_metavars(f);
if (is_metavar(r.first))
return e;
buffer<expr> args;
get_app_rev_args(e, args);
j = mk_composite1(j, r.second);
return apply_beta(r.first, args.size(), args.data());
expr instantiate_meta(expr e, justification & j) {
while (true) {
expr const & f = get_app_fn(e);
if (!is_metavar(f))
return e;
name const & f_name = mlocal_name(f);
auto f_value = m_subst.get_expr(f_name);
if (!f_value)
return e;
j = mk_composite1(j, m_subst.get_expr_jst(f_name));
buffer<expr> args;
get_app_rev_args(e, args);
e = apply_beta(*f_value, args.size(), args.data());
}
}
expr instantiate_meta_args(expr const & e, justification & j) {