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

perf(library/unifier): improve check_imitation performance

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-07 18:28:23 -07:00
parent f6ba6da4b5
commit 969afa8245
1 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/unifier.cpp
View file

@ -1232,7 +1232,15 @@ struct unifier_fn {
/** \brief Check if term \c e (produced by an imitation step) is /** \brief Check if term \c e (produced by an imitation step) is
type correct, and store generated constraints in \c cs. type correct, and store generated constraints in \c cs.
Include \c j in all generated constraints */ Include \c j in all generated constraints */
bool check_imitation(expr const & e, justification const & j, bool relax, buffer<constraint> & cs) { bool check_imitation(expr e, justification const & j, bool relax, buffer<constraint> & cs) {
buffer<expr> ls;
while (is_lambda(e)) {
expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
expr l = mk_local(m_ngen.next(), binding_name(e), d, binding_info(e));
ls.push_back(l);
e = binding_body(e);
}
e = instantiate_rev(e, ls.size(), ls.data());;
try { try {
buffer<constraint> aux; buffer<constraint> aux;
m_tc[relax]->check(e, aux); m_tc[relax]->check(e, aux);