refactor(*): semantic attachment parsing and simplification

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/frontend.cpp

@@ -649,6 +649,8 @@ std::vector<bool> const & get_implicit_arguments(ro_environment const & env, nam
 std::vector<bool> 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;
 }

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));

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<object> 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<bool> const & imp_args = get_implicit_arguments(m_env, obj->get_name());
                         buffer<expr> 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);

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));
     }

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)
+*)

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)