feat(frontends/lean): add 'match' expressions

We reuse the equations infrastructure to compile them.

src/emacs/lean-syntax.el

@@ -13,7 +13,7 @@
     "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "example"
     "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "record" "universe" "universes"
     "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
-    "calc_trans" "calc_subst" "calc_refl" "calc_symm"
+    "calc_trans" "calc_subst" "calc_refl" "calc_symm" "match"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
     "using" "namespace" "instance" "class" "multiple_instances" "section" "fields" "find_decl"
     "set_option" "add_rewrite" "extends" "include" "omit" "classes" "instances" "coercions" "raw")

src/frontends/lean/builtin_exprs.cpp

@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "library/let.h"
 #include "library/definitional/equations.h"
 #include "frontends/lean/builtin_exprs.h"
+#include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/calc.h"
 #include "frontends/lean/begin_end_ext.h"
@@ -509,6 +510,7 @@ parse_table init_nud_table() {
     r = r.add({transition("begin", mk_ext_action_core(parse_begin_end))}, x0);
     r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, x0);
     r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0);
+    r = r.add({transition("match", mk_ext_action(parse_match))}, x0);
     return r;
 }
 

src/frontends/lean/decl_cmds.cpp

@@ -462,6 +462,45 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
     }
 }
 
+/** \brief Use equations compiler infrastructure to implement match-with */
+expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
+    expr t  = p.parse_expr();
+    p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");
+    buffer<expr> eqns;
+    expr fn = mk_local(p.mk_fresh_name(), "match", mk_expr_placeholder(), binder_info());
+    while (true) {
+        expr lhs;
+        unsigned prev_num_undef_ids = p.get_num_undef_ids();
+        buffer<expr> locals;
+        {
+            parser::undef_id_to_local_scope scope2(p);
+            auto lhs_pos = p.pos();
+            lhs = p.parse_expr();
+            lhs = p.mk_app(fn, lhs, lhs_pos);
+            unsigned num_undef_ids = p.get_num_undef_ids();
+            for (unsigned i = prev_num_undef_ids; i < num_undef_ids; i++) {
+                locals.push_back(p.get_undef_id(i));
+            }
+        }
+        validate_equation_lhs(p, lhs, locals);
+        lhs = merge_equation_lhs_vars(lhs, locals);
+        auto assign_pos = p.pos();
+        p.check_token_next(get_assign_tk(), "invalid 'match' expression, ':=' expected");
+        {
+            parser::local_scope scope2(p);
+            for (expr const & local : locals)
+                p.add_local(local);
+            expr rhs = p.parse_expr();
+            eqns.push_back(Fun(fn, Fun(locals, p.save_pos(mk_equation(lhs, rhs), assign_pos), p)));
+        }
+        if (!p.curr_is_token(get_comma_tk()))
+            break;
+        p.next();
+    }
+    expr f = p.save_pos(mk_equations(1, eqns.size(), eqns.data()), pos);
+    return p.mk_app(f, t, pos);
+}
+
 // An Lean example is not really a definition, but we use the definition infrastructure to simulate it.
 enum def_cmd_kind { Theorem, Definition, Example };
 

src/frontends/lean/decl_cmds.h

@@ -16,6 +16,7 @@ class parser;
     Return true when levels were provided.
 */
 bool parse_univ_params(parser & p, buffer<name> & ps);
+expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos);
 /**
    \brief Add universe levels from \c found_ls to \c ls_buffer (only the levels that do not already occur in \c ls_buffer are added).
    Then sort \c ls_buffer (using the order in which the universe levels were declared).

src/frontends/lean/token_table.cpp

@@ -80,7 +80,7 @@ void init_token_table(token_table & t) {
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
-         {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0},
+         {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},
          {"<d", g_decreasing_prec}, {"local", 0}, {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
 
     char const * commands[] =

tests/lean/run/match3.lean

@@ -0,0 +1,49 @@
+import data.list
+open nat
+
+definition foo (a : nat) : nat :=
+match a with
+ zero   := zero,
+ succ n := n
+
+example : foo 3 = 2 := rfl
+
+open decidable
+
+protected theorem dec_eq : ∀ x y : nat, decidable (x = y),
+dec_eq zero     zero     := inl rfl,
+dec_eq (succ x) zero     := inr (λ h, nat.no_confusion h),
+dec_eq zero     (succ y) := inr (λ h, nat.no_confusion h),
+dec_eq (succ x) (succ y) :=
+  match dec_eq x y with
+    inl H := inl (eq.rec_on H rfl),
+    inr H := inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
+
+context
+  open list
+  parameter {A : Type}
+  parameter (p : A → Prop)
+  parameter [H : decidable_pred p]
+  include H
+
+  definition filter : list A → list A,
+  filter nil      := nil,
+  filter (a :: l) :=
+    match H a with
+     inl h := a :: filter l,
+     inr h := filter l
+
+  theorem filter_nil : filter nil = nil :=
+  rfl
+
+  theorem filter_cons (a : A) (l : list A) : filter (a :: l) = if p a then a :: filter l else filter l :=
+  rfl
+end
+
+definition sub2 (a : nat) : nat :=
+match a with
+ 0   := 0,
+ 1   := 0,
+ b+2 := b
+
+example (a : nat) : sub2 (succ (succ a)) = a := rfl