From 96d7d9c8d97f979ce22d5c17a08c18e010d183ee Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Oct 2014 09:19:58 -0700 Subject: [PATCH] feat(library/tactic/elaborate): do not invoke unifier if no constraints were generated during elaboration --- src/library/tactic/elaborate.cpp | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp index 15bf45a472..023cbb6ca5 100644 --- a/src/library/tactic/elaborate.cpp +++ b/src/library/tactic/elaborate.cpp @@ -19,17 +19,23 @@ optional elaborate_with_respect_to(environment const & env, io_state const expr new_e = ecs.first; buffer cs; to_buffer(ecs.second, cs); - to_buffer(s.get_postponed(), cs); - unifier_config cfg(ios.get_options()); - unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), subst, cfg); - if (auto p = rseq.pull()) { - substitution new_subst = p->first.first; - constraints new_postponed = p->first.second; - new_e = new_subst.instantiate(new_e); - s = proof_state(gs, new_subst, ngen, new_postponed); + if (cs.empty()) { + // easy case: no constraints to be solved + s = proof_state(s, ngen); return some_expr(new_e); } else { - return none_expr(); + to_buffer(s.get_postponed(), cs); + unifier_config cfg(ios.get_options()); + unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), subst, cfg); + if (auto p = rseq.pull()) { + substitution new_subst = p->first.first; + constraints new_postponed = p->first.second; + new_e = new_subst.instantiate(new_e); + s = proof_state(gs, new_subst, ngen, new_postponed); + return some_expr(new_e); + } else { + return none_expr(); + } } } }