From cfeb426cd76b842b660f306c009716d312249ff6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 13 Mar 2015 18:58:34 -0700
Subject: [PATCH] fix(frontends/lean): pretty print numeral notation from
 algebra

---
 src/frontends/lean/pp.cpp                     | 18 +++++++++++-------
 src/library/head_map.cpp                      | 11 ++++++++++-
 tests/lean/pp_algebra_num_bug.lean            | 19 +++++++++++++++++++
 .../lean/pp_algebra_num_bug.lean.expected.out |  4 ++++
 4 files changed, 44 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/pp_algebra_num_bug.lean
 create mode 100644 tests/lean/pp_algebra_num_bug.lean.expected.out

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index a4ff85771..4aad0d09c 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -767,12 +767,14 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & a
         return match(sort_level(p), sort_level(e));
     } else if (is_app(e)) {
         buffer<expr> p_args, e_args;
-        expr const & p_fn = get_app_args(p, p_args);
-        expr const & e_fn = get_app_args(e, e_args);
+        expr p_fn    = get_app_args(p, p_args);
+        bool consume = is_consume_args(p_fn);
+        if (consume)
+            p_fn     = get_consume_args_arg(p_fn);
+        expr e_fn    = get_app_args(e, e_args);
         if (!match(p_fn, e_fn, args))
             return false;
-        bool expl   = is_explicit(p);
-        if (expl) {
+        if (is_explicit(p)) {
             if (p_args.size() != e_args.size())
                 return false;
             for (unsigned i = 0; i < p_args.size(); i++) {
@@ -785,15 +787,17 @@ bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & a
                 expr fn_type = m_tc.infer(e_fn).first;
                 unsigned j = 0;
                 for (unsigned i = 0; i < e_args.size(); i++) {
-                    fn_type = m_tc.ensure_pi(fn_type).first;
-                    if (is_explicit(binding_info(fn_type))) {
+                    fn_type                  = m_tc.ensure_pi(fn_type).first;
+                    expr const & body        = binding_body(fn_type);
+                    binder_info const & info = binding_info(fn_type);
+                    if ((!consume || closed(body)) && is_explicit(info)) {
                         if (j >= p_args.size())
                             return false;
                         if (!match(p_args[j], e_args[i], args))
                             return false;
                         j++;
                     }
-                    fn_type = instantiate(binding_body(fn_type), e_args[i]);
+                    fn_type = instantiate(body, e_args[i]);
                 }
                 return j == p_args.size();
             } catch (exception&) {
diff --git a/src/library/head_map.cpp b/src/library/head_map.cpp
index 0dc7adbda..99e9eb0b7 100644
--- a/src/library/head_map.cpp
+++ b/src/library/head_map.cpp
@@ -5,10 +5,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/head_map.h"
+#include "library/explicit.h"
 
 namespace lean {
 head_index::head_index(expr const & e) {
-    expr const & f = get_app_fn(e);
+    expr f = get_app_fn(e);
+    while (true) {
+        if (is_explicit(f))
+            f = get_explicit_arg(f);
+        else if (is_consume_args(f))
+            f = get_consume_args_arg(f);
+        else
+            break;
+    }
     m_kind = f.kind();
     if (is_constant(f))
         m_const_name = const_name(f);
diff --git a/tests/lean/pp_algebra_num_bug.lean b/tests/lean/pp_algebra_num_bug.lean
new file mode 100644
index 000000000..d59087ba6
--- /dev/null
+++ b/tests/lean/pp_algebra_num_bug.lean
@@ -0,0 +1,19 @@
+import algebra.group
+open algebra
+
+variable {A : Type}
+variable [s : group A]
+variable (a : A)
+
+check 1 * 1 * a
+set_option pp.notation false
+check 1 * a
+
+variable [s2 : add_comm_group A]
+
+set_option pp.notation true
+
+check 0 + a
+
+set_option pp.notation false
+check 0 + a
diff --git a/tests/lean/pp_algebra_num_bug.lean.expected.out b/tests/lean/pp_algebra_num_bug.lean.expected.out
new file mode 100644
index 000000000..c0ec37250
--- /dev/null
+++ b/tests/lean/pp_algebra_num_bug.lean.expected.out
@@ -0,0 +1,4 @@
+1 * 1 * a : A
+has_mul.mul (has_one.one A) a : A
+0 + a : A
+has_add.add (has_zero.zero A) a : A