diff --git a/src/builtin/obj/Int.olean b/src/builtin/obj/Int.olean index 09962ad04..d648d86f1 100644 Binary files a/src/builtin/obj/Int.olean and b/src/builtin/obj/Int.olean differ diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index 5541edf69..d8d5b4879 100644 Binary files a/src/builtin/obj/Nat.olean and b/src/builtin/obj/Nat.olean differ diff --git a/src/builtin/obj/Real.olean b/src/builtin/obj/Real.olean index 03fe91b75..502ad6ec3 100644 Binary files a/src/builtin/obj/Real.olean and b/src/builtin/obj/Real.olean differ diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean index c67f10dee..b3e342dd1 100644 Binary files a/src/builtin/obj/cast.olean and b/src/builtin/obj/cast.olean differ diff --git a/src/builtin/obj/heq.olean b/src/builtin/obj/heq.olean index 3bf24218e..9ae162e52 100644 Binary files a/src/builtin/obj/heq.olean and b/src/builtin/obj/heq.olean differ diff --git a/src/builtin/obj/if_then_else.olean b/src/builtin/obj/if_then_else.olean index 202e92997..c394d4d08 100644 Binary files a/src/builtin/obj/if_then_else.olean and b/src/builtin/obj/if_then_else.olean differ diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index a3d87a9de..19d0ab9bd 100644 Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ diff --git a/src/builtin/obj/specialfn.olean b/src/builtin/obj/specialfn.olean index 18ea9a60d..b239d7032 100644 Binary files a/src/builtin/obj/specialfn.olean and b/src/builtin/obj/specialfn.olean differ diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index 4f95c602c..a04dab28e 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -649,6 +649,8 @@ std::vector const & get_implicit_arguments(ro_environment const & env, nam std::vector const & get_implicit_arguments(ro_environment const & env, expr const & n) { if (is_constant(n)) return get_implicit_arguments(env, const_name(n)); + else if (is_value(n)) + return get_implicit_arguments(env, to_value(n).get_name()); else return g_empty_vector; } diff --git a/src/frontends/lean/parser_calc.cpp b/src/frontends/lean/parser_calc.cpp index 2419f6d25..9551a8272 100644 --- a/src/frontends/lean/parser_calc.cpp +++ b/src/frontends/lean/parser_calc.cpp @@ -15,7 +15,9 @@ Author: Leonardo de Moura namespace lean { bool calc_proof_parser::supports(expr const & op1) const { return - std::find_if(m_supported_operators.begin(), m_supported_operators.end(), [&](op_data const & op2) { return op1 == op2.m_fn; }) + std::find_if(m_supported_operators.begin(), m_supported_operators.end(), [&](op_data const & op2) { + return op1 == op2.m_fn; + }) != m_supported_operators.end(); } @@ -44,18 +46,10 @@ void calc_proof_parser::add_trans_step(expr const & op1, expr const & op2, trans m_trans_ops.emplace_front(op1, op2, d); } -static expr get_value_op(expr const & op) { - if (is_value(op)) - return mk_constant(to_value(op).get_name()); - else - return op; -} - - calc_proof_parser::calc_proof_parser() { - expr imp = get_value_op(mk_implies_fn()); - expr eq = get_value_op(mk_eq_fn()); - expr neq = get_value_op(mk_neq_fn()); + expr imp = mk_implies_fn(); + expr eq = mk_eq_fn(); + expr neq = mk_neq_fn(); add_supported_operator(op_data(imp, 2)); add_supported_operator(op_data(eq, 3)); diff --git a/src/frontends/lean/parser_expr.cpp b/src/frontends/lean/parser_expr.cpp index e7ebd38cd..35a53ac4d 100644 --- a/src/frontends/lean/parser_expr.cpp +++ b/src/frontends/lean/parser_expr.cpp @@ -257,13 +257,13 @@ expr parser_imp::get_name_ref(name const & id, pos_info const & p, bool implicit name nid = *it + id; optional obj = m_env->find_object(nid); if (obj) { - object_kind k = obj->kind(); + expr f = obj->is_builtin() ? obj->get_value() : mk_constant(obj->get_name()); + object_kind k = obj->kind(); if (k == object_kind::Definition || k == object_kind::Postulate || k == object_kind::Builtin) { if (implicit_args && has_implicit_arguments(m_env, obj->get_name())) { std::vector const & imp_args = get_implicit_arguments(m_env, obj->get_name()); buffer args; pos_info p = pos(); - expr f = mk_constant(obj->get_name()); args.push_back(save(f, p)); for (unsigned i = 0; i < imp_args.size(); i++) { if (imp_args[i]) { @@ -274,7 +274,7 @@ expr parser_imp::get_name_ref(name const & id, pos_info const & p, bool implicit } return mk_app(args); } else { - return mk_constant(obj->get_name()); + return f; } } else { throw parser_error(sstream() << "invalid object reference, object '" << nid << "' is not an expression.", p); diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index f1b9765d4..01ad0318d 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -553,9 +553,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); @@ -563,6 +563,9 @@ class simplifier_fn { return simplify(e); } } + if (m_eval && obj->is_builtin()) { + return result(obj->get_value()); + } } return rewrite(e, result(e)); } diff --git a/tests/lean/simp7b.lean b/tests/lean/simp7b.lean new file mode 100644 index 000000000..29280a2c0 --- /dev/null +++ b/tests/lean/simp7b.lean @@ -0,0 +1,10 @@ +variables a b c d e f p: Bool +rewrite_set simple +add_rewrite and_assoc and_comm and_left_comm : simple +(* +local t = parse_lean("((f ∨ p) ∧ (e ∨ p)) ∧ ((p ∨ d) ∧ c) ∧ (b ∧ a)") +local t2 = simplify(t, "simple") +print(t) +print("====>") +print(t2) +*) diff --git a/tests/lean/simp7b.lean.expected.out b/tests/lean/simp7b.lean.expected.out new file mode 100644 index 000000000..0f7f222b8 --- /dev/null +++ b/tests/lean/simp7b.lean.expected.out @@ -0,0 +1,12 @@ + Set: pp::colors + Set: pp::unicode + Assumed: a + Assumed: b + Assumed: c + Assumed: d + Assumed: e + Assumed: f + Assumed: p +((f ∨ p) ∧ (e ∨ p)) ∧ ((p ∨ d) ∧ c) ∧ b ∧ a +====> +a ∧ b ∧ c ∧ (e ∨ p) ∧ (f ∨ p) ∧ (p ∨ d)