From 7492fd5a2c1c3e7708f640828ee5182edfaaa296 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Jan 2014 10:34:55 -0800 Subject: [PATCH] feat(library/simplifier): add support for simplification by evaluation Signed-off-by: Leonardo de Moura --- src/library/simplifier/simplifier.cpp | 78 +++++++++++++++++++-------- tests/lua/simp1.lua | 4 +- 2 files changed, 59 insertions(+), 23 deletions(-) diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 8ed34e7e3..cfadcfe8c 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -38,6 +38,10 @@ Author: Leonardo de Moura #define LEAN_SIMPLIFIER_ETA true #endif +#ifndef LEAN_SIMPLIFIER_EVAL +#define LEAN_SIMPLIFIER_EVAL true +#endif + #ifndef LEAN_SIMPLIFIER_UNFOLD #define LEAN_SIMPLIFIER_UNFOLD false #endif @@ -56,6 +60,7 @@ static name g_simplifier_contextual {"simplifier", "contextual"}; static name g_simplifier_single_pass {"simplifier", "single_pass"}; static name g_simplifier_beta {"simplifier", "beta"}; static name g_simplifier_eta {"simplifier", "eta"}; +static name g_simplifier_eval {"simplifier", "eval"}; static name g_simplifier_unfold {"simplifier", "unfold"}; static name g_simplifier_conditional {"simplifier", "conditional"}; static name g_simplifier_max_steps {"simplifier", "max_steps"}; @@ -65,6 +70,7 @@ RegisterBoolOption(g_simplifier_contextual, LEAN_SIMPLIFIER_CONTEXTUAL, "(simpli RegisterBoolOption(g_simplifier_single_pass, LEAN_SIMPLIFIER_SINGLE_PASS, "(simplifier) if false then the simplifier keeps applying simplifications as long as possible"); RegisterBoolOption(g_simplifier_beta, LEAN_SIMPLIFIER_BETA, "(simplifier) use beta-reduction"); RegisterBoolOption(g_simplifier_eta, LEAN_SIMPLIFIER_ETA, "(simplifier) use eta-reduction"); +RegisterBoolOption(g_simplifier_eval, LEAN_SIMPLIFIER_EVAL, "(simplifier) apply reductions based on computation"); RegisterBoolOption(g_simplifier_unfold, LEAN_SIMPLIFIER_UNFOLD, "(simplifier) unfolds non-opaque definitions"); RegisterBoolOption(g_simplifier_conditional, LEAN_SIMPLIFIER_CONDITIONAL, "(simplifier) conditional rewriting"); RegisterUnsignedOption(g_simplifier_max_steps, LEAN_SIMPLIFIER_MAX_STEPS, "(simplifier) maximum number of steps"); @@ -84,6 +90,9 @@ bool get_simplifier_beta(options const & opts) { bool get_simplifier_eta(options const & opts) { return opts.get_bool(g_simplifier_eta, LEAN_SIMPLIFIER_ETA); } +bool get_simplifier_eval(options const & opts) { + return opts.get_bool(g_simplifier_eval, LEAN_SIMPLIFIER_EVAL); +} bool get_simplifier_unfold(options const & opts) { return opts.get_bool(g_simplifier_unfold, LEAN_SIMPLIFIER_UNFOLD); } @@ -108,6 +117,7 @@ class simplifier_fn { bool m_single_pass; bool m_beta; bool m_eta; + bool m_eval; bool m_unfold; bool m_conditional; unsigned m_max_steps; @@ -329,7 +339,7 @@ class simplifier_fn { i++; } if (i == num) - return result(out); + return rewrite_app(e, result(out)); expr pr; bool heq_proof = false; if (i == 0) { @@ -369,11 +379,35 @@ class simplifier_fn { } } - result rewrite_app(expr const & e, result const & r) { - if (m_beta && is_lambda(arg(r.m_out, 0))) - return rewrite(e, result(head_beta_reduce(r.m_out), r.m_proof, r.m_heq_proof)); - else - return rewrite(e, r); + /** + \brief Given (applications) lhs and rhs s.t. lhs = rhs.m_out + with proof rhs.m_proof, this method applies rewrite rules, beta + and evaluation to \c rhs.m_out, and return a new result object + new_rhs s.t. lhs = new_rhs.m_out with proof new_rhs.m_proof + + \pre is_app(lhs) + \pre is_app(rhs.m_out) + */ + result rewrite_app(expr const & lhs, result const & rhs) { + lean_assert(is_app(rhs.m_out)); + lean_assert(is_app(lhs)); + expr f = arg(rhs.m_out, 0); + if (m_eval && is_value(f)) { + optional new_rhs = to_value(f).normalize(num_args(rhs.m_out), &arg(rhs.m_out, 0)); + if (new_rhs) { + // We don't need to create a new proof term since rhs.m_out and new_rhs are + // definitionally equal. + return rewrite(lhs, result(*new_rhs, rhs.m_proof, rhs.m_heq_proof)); + } + } + + if (m_beta && is_lambda(f)) { + expr new_rhs = head_beta_reduce(rhs.m_out); + // rhs.m_out and new_rhs are also definitionally equal + return rewrite(lhs, result(new_rhs, rhs.m_proof, rhs.m_heq_proof)); + } + + return rewrite(lhs, rhs); } expr m_target; // temp field @@ -382,17 +416,8 @@ class simplifier_fn { expr m_new_rhs; // temp field expr m_new_proof; // temp field - void reset_subst(unsigned num_args) { - if (m_subst.size() < num_args) { - m_subst.resize(num_args); - m_new_args.resize(num_args+1); - } - for (unsigned i = 0; i < num_args; i++) - m_subst[i] = none_expr(); - } - - bool found_all_args(unsigned num_args) { - for (unsigned i = 0; i < num_args; i++) { + bool found_all_args(unsigned num) { + for (unsigned i = 0; i < num; i++) { if (!m_subst[i]) return false; m_new_args[i+1] = *m_subst[i]; @@ -408,8 +433,11 @@ class simplifier_fn { */ bool match(rewrite_rule const & rule) { unsigned num = rule.get_num_args(); - reset_subst(num); - if (hop_match(rule.get_lhs(), m_target, m_subst)) { + m_subst.clear(); + m_subst.resize(num); + if (hop_match(rule.get_lhs(), m_target, m_subst, optional(m_env))) { + m_new_args.clear(); + m_new_args.resize(num+1); if (found_all_args(num)) { // easy case: all arguments found m_new_rhs = instantiate(rule.get_rhs(), num, m_new_args.data() + 1); @@ -423,7 +451,9 @@ class simplifier_fn { } return true; } - // TODO(Leo): conditional rewriting + // Conditional rewriting: we try to fill the missing + // arguments by trying to find a proof for ones that are + // propositions. } return false; } @@ -456,9 +486,9 @@ class simplifier_fn { result simplify_constant(expr const & e) { lean_assert(is_constant(e)); - if (m_unfold) { + if (m_unfold || m_eval) { auto obj = m_env->find_object(const_name(e)); - if (should_unfold(obj)) { + if (m_unfold && should_unfold(obj)) { expr e = obj->get_value(); if (m_single_pass) { return result(e); @@ -466,6 +496,9 @@ class simplifier_fn { return simplify(e); } } + if (m_eval && obj->is_builtin()) { + return result(obj->get_value()); + } } return rewrite(e, result(e)); } @@ -577,6 +610,7 @@ class simplifier_fn { m_single_pass = get_simplifier_single_pass(o); m_beta = get_simplifier_beta(o); m_eta = get_simplifier_eta(o); + m_eval = get_simplifier_eval(o); m_unfold = get_simplifier_unfold(o); m_conditional = get_simplifier_conditional(o); m_max_steps = get_simplifier_max_steps(o); diff --git a/tests/lua/simp1.lua b/tests/lua/simp1.lua index ec03a1d04..7a13b0b7f 100644 --- a/tests/lua/simp1.lua +++ b/tests/lua/simp1.lua @@ -12,9 +12,12 @@ parse_lean_cmds([[ set_opaque a true axiom f_id (x : Nat) : f x 1 = 2*x + + axiom g_g_x (x : Nat) : (not (x = 0)) -> g (g x) = 0 ]]) add_rewrite_rules("a_eq_1") add_rewrite_rules("f_id") +add_rewrite_rules("eq_id") -- set_option({"lean", "pp", "implicit"}, true) e, pr = simplify(parse_lean('fun x, f (f x (0 + a)) (g (b + 0))')) print(e) @@ -22,7 +25,6 @@ print(pr) local env = get_environment() print(env:type_check(pr)) - e, pr = simplify(parse_lean('forall x, let d := a + 1 in f x a >= d')) print(e) print(pr)