From a23df570fc20e5a221d0efd32f255b85191d6ea0 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 17 Jan 2019 19:19:01 +0100
Subject: [PATCH] fix(library/init/lean/elaborator): match

---
 library/init/lean/elaborator.lean    | 10 +++++++---
 library/init/lean/expander.lean      |  2 +-
 src/frontends/lean/vm_elaborator.cpp |  7 +++++--
 3 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index 353ac7d3c3..dde002fd03 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -318,8 +318,12 @@ def to_pexpr : syntax → elaborator_m expr
       pure (`_match_fn, lhs, rhs)
     },
     type ← to_pexpr $ get_opt_type v.type,
-    pure $ mk_eqns type eqns
-  | _ := error stx $ "unexpected node: " ++ to_string k.name,
+    let eqns := mk_eqns type eqns,
+    expr.mdata mdata e ← pure eqns
+      | error stx "to_pexpr: unreachable",
+    let eqns := expr.mdata (mdata.set_bool `match tt) e,
+    expr.mk_app eqns <$> v.scrutinees.mmap (λ scr, to_pexpr scr.item)
+  | _ := error stx $ "to_pexpr: unexpected node: " ++ to_string k.name,
   (match k with
   | @app := pure e -- no position
   | _ := do
@@ -329,7 +333,7 @@ def to_pexpr : syntax → elaborator_m expr
       let pos := cfg.file_map.to_position pos in
       pure $ expr.mdata ((kvmap.set_nat {} `column pos.column).set_nat `row pos.line) e
     | none := pure e)
-| stx := error stx $ "unexpected: " ++ to_string stx
+| stx := error stx $ "to_pexpr: unexpected: " ++ to_string stx
 
 /-- Returns the active namespace, that is, the concatenation of all active `namespace` commands. -/
 def get_namespace : elaborator_m name := do
diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean
index 08719a45fd..75ec95c057 100644
--- a/library/init/lean/expander.lean
+++ b/library/init/lean/expander.lean
@@ -274,7 +274,7 @@ def expand_binders (mk_binding : binders.view → syntax → syntax) (bnders : b
     -- anonymous constructor binding ~> binding + match
     | mixed_binder.view.bracketed (bracketed_binder.view.anonymous_constructor ctor) :=
       pure $ mk_binding (mk_simple_binder "x" binder_info.default (review hole {})) $ review «match» {
-        scrutinees := [syntax.ident "x"],
+        scrutinees := [review ident_univs ↑"x"],
         equations := [{item := {lhs := [review anonymous_constructor ctor], rhs := r}}]
       }
     -- local notation: should have been handled by caller, erase
diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp
index 3062429d50..849ee64a79 100644
--- a/src/frontends/lean/vm_elaborator.cpp
+++ b/src/frontends/lean/vm_elaborator.cpp
@@ -65,7 +65,8 @@ struct resolve_names_fn : public replace_visitor {
 
     expr visit_pre_equations(expr const & e) {
         equations_header header;
-        if (get_bool(mdata_data(e), "match")) {
+        bool is_match = get_bool(mdata_data(e), "match").value_or(false);
+        if (is_match) {
             parser::local_scope scope1(m_p);
             match_definition_scope scope2(m_p.env());
             header = mk_match_header(scope2.get_name(), scope2.get_actual_name());
@@ -87,12 +88,14 @@ struct resolve_names_fn : public replace_visitor {
                 buffer<expr> new_locals;
                 bool skip_main_fn = true;
                 lhs = m_p.patexpr_to_pattern(lhs, skip_main_fn, new_locals);
-                names locals;
+                names locals = m_locals;
                 // NOTE: appends `new_locals` to `locals` in reverse
                 for (auto const & l : new_locals)
                     locals = cons(local_name_p(l), locals);
                 flet<names> _(m_locals, locals);
                 rhs = visit(rhs);
+                if (is_match)
+                    new_locals.insert(0, mk_local("_match_fn", mk_expr_placeholder()));
                 eqn = Fun(new_locals, mk_equation(lhs, rhs), m_p);
             }
         }