feat(frontends/lean): nary match

library/data/list/basic.lean

@@ -461,9 +461,9 @@ theorem find_nth [decidable_eq T] {a : T} : ∀ {l}, a ∈ l → nth l (find a l
 -/
 
 definition inth [h : inhabited T] (l : list T) (n : nat) : T :=
-match nth l n with
-| some a := a
-| none   := arbitrary T
+match (nth l n) with
+| (some a) := a
+| none     := arbitrary T
 end
 
 theorem inth_zero [inhabited T] (a : T) (l : list T) : inth (a :: l) 0 = a :=

library/data/list/comb.lean

@@ -334,24 +334,24 @@ theorem exists_of_any {p : A → Prop} : ∀{l : list A}, any l p → ∃a, a
 definition decidable_all (p : A → Prop) [H : decidable_pred p] : ∀ l, decidable (all l p)
 | []       := decidable_true
 | (a :: l) :=
-  match H a with
-  | tt Hp₁ :=
-    match decidable_all l with
-    | tt Hp₂ := tt (and.intro Hp₁ Hp₂)
-    | ff Hn₂ := ff (not_and_of_not_right (p a) Hn₂)
+  match (H a) with
+  | (tt Hp₁) :=
+    match (decidable_all l) with
+    | (tt Hp₂) := tt (and.intro Hp₁ Hp₂)
+    | (ff Hn₂) := ff (not_and_of_not_right (p a) Hn₂)
     end
-  | ff Hn := ff (not_and_of_not_left (all l p) Hn)
+  | (ff Hn) := ff (not_and_of_not_left (all l p) Hn)
   end
 
 definition decidable_any (p : A → Prop) [H : decidable_pred p] : ∀ l, decidable (any l p)
 | []       := decidable_false
 | (a :: l) :=
-  match H a with
-  | tt Hp := tt (or.inl Hp)
-  | ff Hn₁ :=
-    match decidable_any l with
-    | tt Hp₂ := tt (or.inr Hp₂)
-    | ff Hn₂ := ff (not_or Hn₁ Hn₂)
+  match (H a) with
+  | (tt Hp) := tt (or.inl Hp)
+  | (ff Hn₁) :=
+    match (decidable_any l) with
+    | (tt Hp₂) := tt (or.inr Hp₂)
+    | (ff Hn₂) := ff (not_or Hn₁ Hn₂)
     end
   end
 
@@ -362,14 +362,14 @@ map₂ (λ a b, (a, b)) l₁ l₂
 definition unzip : list (A × B) → list A × list B
 | []            := ([], [])
 | ((a, b) :: l) :=
-  match unzip l with
+  match (unzip l) with
   | (la, lb) := (a :: la, b :: lb)
   end
 
 theorem unzip_nil [simp] : unzip (@nil (A × B)) = ([], []) := rfl
 
 theorem unzip_cons [simp] (a : A) (b : B) (l : list (A × B)) :
-   unzip ((a, b) :: l) = match unzip l with (la, lb) := (a :: la, b :: lb) end :=
+   unzip ((a, b) :: l) = match (unzip l) with (la, lb) := (a :: la, b :: lb) end :=
 rfl
 
 theorem zip_unzip : ∀ (l : list (A × B)), zip (pr₁ (unzip l)) (pr₂ (unzip l)) = l

library/data/list/set.lean

@@ -17,9 +17,9 @@ include H
 definition erase (a : A) : list A → list A
 | []     := []
 | (b::l) :=
-  match H a b with
-  | tt e := l
-  | ff n := b :: erase l
+  match (H a b) with
+  | (tt e) := l
+  | (ff n) := b :: erase l
   end
 
 lemma erase_nil (a : A) : erase a [] = [] :=
@@ -429,12 +429,12 @@ theorem erase_dup_eq_of_nodup [decidable_eq A] : ∀ {l : list A}, nodup l → e
 definition decidable_nodup [instance] [decidable_eq A] : ∀ (l : list A), decidable (nodup l)
 | []     := tt nodup_nil
 | (a::l) :=
-  match decidable_mem a l with
-  | tt p := ff (not_nodup_cons_of_mem p)
-  | ff n :=
-    match decidable_nodup l with
-    | tt nd := tt (nodup_cons n nd)
-    | ff d  := ff (not_nodup_cons_of_not_nodup d)
+  match (decidable_mem a l) with
+  | (tt p) := ff (not_nodup_cons_of_mem p)
+  | (ff n) :=
+    match (decidable_nodup l) with
+    | (tt nd) := tt (nodup_cons n nd)
+    | (ff d)  := ff (not_nodup_cons_of_not_nodup d)
     end
   end
 

library/data/nat/examples/fib.lean

@@ -15,7 +15,7 @@ private definition fib_fast_aux : nat → (nat × nat)
 | 0     := (0, 1)
 | 1     := (1, 1)
 | (n+2) :=
-  match fib_fast_aux (n+1) with
+  match (fib_fast_aux (n+1)) with
   | (fn, fn1) := (fn1, fn1 + fn)
   end
 

library/init/classical.lean

@@ -182,8 +182,8 @@ local attribute prop_decidable [instance]
 noncomputable definition type_decidable_eq (A : Type) : decidable_eq A := _
 
 noncomputable definition type_decidable (A : Type) : sum A (A → false) :=
-match prop_decidable (nonempty A) with
-| tt Hp := sum.inl (inhabited.value (inhabited_of_nonempty Hp))
-| ff Hn := sum.inr (λ a, absurd (nonempty.intro a) Hn)
+match (prop_decidable (nonempty A)) with
+| (tt Hp) := sum.inl (inhabited.value (inhabited_of_nonempty Hp))
+| (ff Hn) := sum.inr (λ a, absurd (nonempty.intro a) Hn)
 end
 end classical

library/init/logic.lean

@@ -709,16 +709,16 @@ take x y : A, if Hp : p x y = tt then tt (H₁ Hp)
  else ff (assume Hxy : x = y, (eq.subst Hxy Hp) (H₂ y))
 
 theorem decidable_eq_inl_refl {A : Type} [H : decidable_eq A] (a : A) : H a a = tt (eq.refl a) :=
-match H a a with
-| tt e := rfl
-| ff n := absurd rfl n
+match (H a a) with
+| (tt e) := rfl
+| (ff n) := absurd rfl n
 end
 
 theorem decidable_eq_inr_neg {A : Type} [H : decidable_eq A] {a b : A} : Π n : a ≠ b, H a b = ff n :=
 assume n,
-match H a b with
-| tt e  := absurd e n
-| ff n₁ := proof_irrel n n₁ ▸ rfl
+match (H a b) with
+| (tt e)  := absurd e n
+| (ff n₁) := proof_irrel n n₁ ▸ rfl
 end
 
 /- inhabited -/
@@ -786,15 +786,15 @@ subsingleton.intro (λa b, proof_irrel a b)
 definition subsingleton_decidable [instance] (p : Prop) : subsingleton (decidable p) :=
 subsingleton.intro (λ d₁,
   match d₁ with
-  | tt t₁ := (λ d₂,
+  | (tt t₁) := (λ d₂,
     match d₂ with
-    | tt t₂ := eq.rec_on (proof_irrel t₁ t₂) rfl
-    | ff f₂ := absurd t₁ f₂
+    | (tt t₂) := eq.rec_on (proof_irrel t₁ t₂) rfl
+    | (ff f₂) := absurd t₁ f₂
     end)
-  | ff f₁ := (λ d₂,
+  | (ff f₁) := (λ d₂,
     match d₂ with
-    | tt t₂ := absurd t₂ f₁
-    | ff f₂ := eq.rec_on (proof_irrel f₁ f₂) rfl
+    | (tt t₂) := absurd t₂ f₁
+    | (ff f₂) := eq.rec_on (proof_irrel f₁ f₂) rfl
     end)
   end)
 

library/init/meta/contradiction_tactic.lean

@@ -55,8 +55,8 @@ private meta_definition contra_constructor_eq : list expr → tactic unit
 | []        := failed
 | (H :: Hs) :=
   do t ← infer_type H,
-     match is_eq t with
-     | some (lhs_0, rhs_0) :=
+     match (is_eq t) with
+     | (some (lhs_0, rhs_0)) :=
        do env ← get_env,
           lhs ← whnf lhs_0,
           rhs ← whnf rhs_0,

library/init/meta/environment.lean

@@ -63,8 +63,8 @@ is_constant f && is_constructor env (const_name f)
 
 meta_definition is_refl_app (env : environment) (e : expr) : option (name × expr × expr) :=
 let f := get_app_fn e in
-match refl_for env (const_name f) with
-| some n :=
+match (refl_for env (const_name f)) with
+| (some n) :=
     if get_app_num_args e ≥ 2
     then some (n, app_arg (app_fn e), app_arg e)
     else none

library/init/meta/relation_tactics.lean

@@ -13,9 +13,9 @@ private meta_definition relation_tactic (op_for : environment → name → optio
 do tgt ← target,
    env ← get_env,
    r   ← return $ get_app_fn tgt,
-   match op_for env (const_name r) with
-   | some refl := mk_const refl >>= apply
-   | none      := fail $ tac_name ++ " tactic failed, target is not a relation application with the expected property."
+   match (op_for env (const_name r)) with
+   | (some refl) := mk_const refl >>= apply
+   | none        := fail $ tac_name ++ " tactic failed, target is not a relation application with the expected property."
    end
 
 meta_definition reflexivity : tactic unit :=

library/init/meta/simp_tactic.lean

@@ -62,7 +62,7 @@ simplify_goal failed Hs >> try triv
 
 private meta_definition is_equation : expr → bool
 | (expr.pi _ _ _ b) := is_equation b
-| e                 := match expr.is_eq e with some _ := tt | none := ff end
+| e                 := match (expr.is_eq e) with (some _) := tt | none := ff end
 
 private meta_definition collect_eqs : list expr → tactic (list expr)
 | []        := return []

library/init/meta/tactic.lean

@@ -111,14 +111,14 @@ repeat_at_most 100000
 
 meta_definition returnex (e : exceptional A) : tactic A :=
 λ s, match e with
-| exceptional.success a       := tactic_result.success a s
-| exceptional.exception ⌞A⌟ f := tactic_result.exception A (λ u, f options.mk) s -- TODO(Leo): extract options from environment
+| (exceptional.success a)       := tactic_result.success a s
+| (exceptional.exception ⌞A⌟ f) := tactic_result.exception A (λ u, f options.mk) s -- TODO(Leo): extract options from environment
 end
 
 meta_definition returnopt (e : option A) : tactic A :=
 λ s, match e with
-| some a     := tactic_result.success a s
-| none       := tactic_result.exception A (λ u, to_fmt "failed") s
+| (some a) := tactic_result.success a s
+| none     := tactic_result.exception A (λ u, to_fmt "failed") s
 end
 
 /- Decorate t's exceptions with msg -/
@@ -320,9 +320,9 @@ intro `_
 meta_definition intros : tactic (list expr) :=
 do t ← target,
    match t with
-   | expr.pi   _ _ _ _ := do H ← intro1, Hs ← intros, return (H :: Hs)
-   | expr.elet _ _ _ _ := do H ← intro1, Hs ← intros, return (H :: Hs)
-   | _                 := return []
+   | (expr.pi   _ _ _ _) := do H ← intro1, Hs ← intros, return (H :: Hs)
+   | (expr.elet _ _ _ _) := do H ← intro1, Hs ← intros, return (H :: Hs)
+   | _                   := return []
    end
 
 meta_definition intro_lst : list name → tactic (list expr)
@@ -349,34 +349,34 @@ meta_definition unify : expr → expr → tactic unit :=
 unify_core semireducible
 
 meta_definition match_not (e : expr) : tactic expr :=
-match expr.is_not e with
-| some a := return a
-| none   := fail "expression is not a negation"
+match (expr.is_not e) with
+| (some a) := return a
+| none     := fail "expression is not a negation"
 end
 
 meta_definition match_eq (e : expr) : tactic (expr × expr) :=
-match expr.is_eq e with
-| some (lhs, rhs) := return (lhs, rhs)
-| none            := fail "expression is not an equality"
+match (expr.is_eq e) with
+| (some (lhs, rhs)) := return (lhs, rhs)
+| none              := fail "expression is not an equality"
 end
 
 meta_definition match_ne (e : expr) : tactic (expr × expr) :=
-match expr.is_ne e with
-| some (lhs, rhs) := return (lhs, rhs)
-| none            := fail "expression is not a disequality"
+match (expr.is_ne e) with
+| (some (lhs, rhs)) := return (lhs, rhs)
+| none              := fail "expression is not a disequality"
 end
 
 meta_definition match_heq (e : expr) : tactic (expr × expr × expr × expr) :=
-do match expr.is_heq e with
-| some (A, lhs, B, rhs) := return (A, lhs, B, rhs)
-| none                  := fail "expression is not a heterogeneous equality"
+do match (expr.is_heq e) with
+| (some (A, lhs, B, rhs)) := return (A, lhs, B, rhs)
+| none                    := fail "expression is not a heterogeneous equality"
 end
 
 meta_definition match_refl_app (e : expr) : tactic (name × expr × expr) :=
 do env ← get_env,
-match environment.is_refl_app env e with
-| some (R, lhs, rhs) := return (R, lhs, rhs)
-| none               := fail "expression is not an application of a reflexive relation"
+match (environment.is_refl_app env e) with
+| (some (R, lhs, rhs)) := return (R, lhs, rhs)
+| none                 := fail "expression is not an application of a reflexive relation"
 end
 
 meta_definition get_local_type (n : name) : tactic expr :=
@@ -403,8 +403,8 @@ do { ctx ← local_context,
 meta_definition swap : tactic unit :=
 do gs ← get_goals,
    match gs with
-   | g₁ :: g₂ :: rs := set_goals (g₂ :: g₁ :: rs)
-   | _              := skip
+   | (g₁ :: g₂ :: rs) := set_goals (g₂ :: g₁ :: rs)
+   | _                := skip
    end
 
 /- Return the number of goals that need to be solved -/

library/init/nat.lean

@@ -79,9 +79,9 @@ namespace nat
   | has_decidable_eq (succ x) zero     := ff (λ H, nat.no_confusion H)
   | has_decidable_eq zero     (succ y) := ff (λ H, nat.no_confusion H)
   | has_decidable_eq (succ x) (succ y) :=
-      match has_decidable_eq x y with
-      | tt xeqy := tt (eq.subst xeqy (eq.refl (succ x)))
-      | ff xney := ff (λ H : succ x = succ y, nat.no_confusion H (λ xeqy : x = y, absurd xeqy xney))
+      match (has_decidable_eq x y) with
+      | (tt xeqy) := tt (eq.subst xeqy (eq.refl (succ x)))
+      | (ff xney) := ff (λ H : succ x = succ y, nat.no_confusion H (λ xeqy : x = y, absurd xeqy xney))
       end
 
   local attribute [instance] [priority nat.prio] nat.has_decidable_eq

library/init/option.lean

@@ -16,9 +16,9 @@ definition option_has_decidable_eq [instance] {A : Type} [H : decidable_eq A] :
 | none      (some v₂) := ff (λ H, option.no_confusion H)
 | (some v₁) none      := ff (λ H, option.no_confusion H)
 | (some v₁) (some v₂) :=
-  match H v₁ v₂ with
-  | tt e := tt (congr_arg (@some A) e)
-  | ff n := ff (λ H, option.no_confusion H (λ e, absurd e n))
+  match (H v₁ v₂) with
+  | (tt e) := tt (congr_arg (@some A) e)
+  | (ff n) := ff (λ H, option.no_confusion H (λ e, absurd e n))
   end
 
 inline definition option_fmap {A B : Type} (f : A → B) (e : option A) : option B :=

library/init/ordering.lean

@@ -32,7 +32,7 @@ variables {A B : Type} [has_ordering A] [has_ordering B]
 
 definition prod.cmp : A × B → A × B → ordering
 | (a₁, b₁) (a₂, b₂) :=
-   match has_ordering.cmp a₁ a₂ with
+   match (has_ordering.cmp a₁ a₂) with
    | ordering.lt := lt
    | ordering.eq := has_ordering.cmp b₁ b₂
    | ordering.gt := gt

library/init/prod.lean

@@ -26,11 +26,11 @@ open decidable
 
 protected definition prod.has_decidable_eq [instance] {A B : Type} [h₁ : decidable_eq A] [h₂ : decidable_eq B] : ∀ p₁ p₂ : A × B, decidable (p₁ = p₂)
 | (a, b) (a', b') :=
-  match h₁ a a' with
-  | tt e₁ :=
-    match h₂ b b' with
-    | tt e₂ := tt (eq.rec_on e₁ (eq.rec_on e₂ rfl))
-    | ff n₂ := ff (assume h, prod.no_confusion h (λ e₁' e₂', absurd e₂' n₂))
+  match (h₁ a a') with
+  | (tt e₁) :=
+    match (h₂ b b') with
+    | (tt e₂) := tt (eq.rec_on e₁ (eq.rec_on e₂ rfl))
+    | (ff n₂) := ff (assume h, prod.no_confusion h (λ e₁' e₂', absurd e₂' n₂))
     end
-  | ff n₁ := ff (assume h, prod.no_confusion h (λ e₁' e₂', absurd e₁' n₁))
+  | (ff n₁) := ff (assume h, prod.no_confusion h (λ e₁' e₂', absurd e₁' n₁))
   end

library/init/quot.lean

@@ -190,7 +190,7 @@ definition quot.has_decidable_eq [instance] {A : Type} {s : setoid A} [decR :
 λ q₁ q₂ : quot s,
   quot.rec_on_subsingleton₂ q₁ q₂
     (λ a₁ a₂,
-      match decR a₁ a₂ with
-      | tt h₁ := tt (quot.sound h₁)
-      | ff h₂ := ff (λ h, absurd (quot.exact h) h₂)
+      match (decR a₁ a₂) with
+      | (tt h₁) := tt (quot.sound h₁)
+      | (ff h₂) := ff (λ h, absurd (quot.exact h) h₂)
       end)

library/init/state.lean

@@ -12,13 +12,13 @@ section
 variables {S A B : Type}
 
 inline definition state_fmap (f : A → B) (a : state S A) : state S B :=
-λ s, match a s with (a', s') := (f a', s') end
+λ s, match (a s) with (a', s') := (f a', s') end
 
 inline definition state_return (a : A) : state S A :=
 λ s, (a, s)
 
 inline definition state_bind (a : state S A) (b : A → state S B) : state S B :=
-λ s, match a s with (a', s') := b a' s' end
+λ s, match (a s) with (a', s') := b a' s' end
 
 definition state_is_monad [instance] (S : Type) : monad (state S) :=
 monad.mk (@state_fmap S) (@state_return S) (@state_bind S)

library/init/to_string.lean

@@ -33,10 +33,10 @@ definition unit.has_to_string [instance] : has_to_string unit :=
 has_to_string.mk (λ u, "star")
 
 definition option.has_to_string [instance] {A : Type} [has_to_string A] : has_to_string (option A) :=
-has_to_string.mk (λ o, match o with | none := "none" | some a := "(some " ++ to_string a ++ ")" end)
+has_to_string.mk (λ o, match o with | none := "none" | (some a) := "(some " ++ to_string a ++ ")" end)
 
 definition sum.has_to_string [instance] {A B : Type} [has_to_string A] [has_to_string B] : has_to_string (sum A B) :=
-has_to_string.mk (λ s, match s with | inl a := "(inl " ++ to_string a ++ ")" | inr b := "(inr " ++ to_string b ++ ")" end)
+has_to_string.mk (λ s, match s with | (inl a) := "(inl " ++ to_string a ++ ")" | (inr b) := "(inr " ++ to_string b ++ ")" end)
 
 definition prod.has_to_string [instance] {A B : Type} [has_to_string A] [has_to_string B] : has_to_string (prod A B) :=
 has_to_string.mk (λ p, "(" ++ to_string (pr1 p) ++ ", " ++ to_string (pr2 p) ++ ")")

src/frontends/lean/match_expr.cpp

@@ -21,25 +21,42 @@ bool is_match_binder_name(name const & n) { return n == *g_match_name; }
 expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
     parser::local_scope scope(p);
     buffer<expr> eqns;
-    expr t;
+    buffer<expr> ts;
     try {
-        t  = p.parse_expr();
-        p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");
-        expr fn = mk_local(mk_fresh_name(), *g_match_name, mk_expr_placeholder(), binder_info());
-        if (p.curr_is_token(get_end_tk())) {
+        ts.push_back(p.parse_expr(get_max_prec()));
+        while (!p.curr_is_token(get_with_tk()) && !p.curr_is_token(get_colon_tk())) {
+            ts.push_back(p.parse_expr(get_max_prec()));
+        }
+        expr fn;
+        /* Parse optional type */
+        if (p.curr_is_token(get_colon_tk())) {
+            p.next();
+            expr type = p.parse_expr();
+            fn = mk_local(mk_fresh_name(), *g_match_name, type, binder_info());
+        } else {
+            fn = mk_local(mk_fresh_name(), *g_match_name, mk_expr_placeholder(), binder_info());
+        }
+
+        p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");
+
+        if (p.curr_is_token(get_end_tk())) {
+            /* Empty match */
             p.next();
-            // empty match-with
             eqns.push_back(Fun(fn, mk_no_equation()));
             expr f = p.save_pos(mk_equations(1, eqns.size(), eqns.data()), pos);
-            return p.mk_app(f, t, pos);
+            return p.mk_app(f, ts, pos);
         }
         if (is_eqn_prefix(p))
             p.next(); // optional '|' in the first case
         while (true) {
-            buffer<expr> locals;
             auto lhs_pos = p.pos();
-            expr lhs = p.parse_pattern(locals);
-            lhs = p.mk_app(fn, lhs, lhs_pos);
+            buffer<expr> lhs_args;
+            while (!p.curr_is_token(get_assign_tk()))
+                lhs_args.push_back(p.parse_pattern_or_expr(get_max_prec()));
+            expr lhs = p.mk_app(fn, lhs_args, lhs_pos);
+            buffer<expr> locals;
+            bool skip_main_fn = true;
+            lhs = p.patexpr_to_pattern(lhs, skip_main_fn, locals);
             auto assign_pos = p.pos();
             p.check_token_next(get_assign_tk(), "invalid 'match' expression, ':=' expected");
             {
@@ -59,7 +76,7 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
     }
     p.check_token_next(get_end_tk(), "invalid 'match' expression, 'end' expected");
     expr f = p.save_pos(mk_equations(1, eqns.size(), eqns.data()), pos);
-    return p.mk_app(f, t, pos);
+    return p.mk_app(f, ts, pos);
 }
 
 void initialize_match_expr() {

src/frontends/lean/parser.cpp

@@ -594,6 +594,14 @@ expr parser::mk_app(expr fn, expr arg, pos_info const & p) {
     return save_pos(::lean::mk_app(fn, arg), p);
 }
 
+expr parser::mk_app(expr fn, buffer<expr> const & args, pos_info const & p) {
+    expr r = fn;
+    for (expr const & arg : args) {
+        r = mk_app(r, arg, p);
+    }
+    return r;
+}
+
 expr parser::mk_app(std::initializer_list<expr> const & args, pos_info const & p) {
     lean_assert(args.size() >= 2);
     auto it = args.begin();

src/frontends/lean/parser.h

@@ -295,6 +295,7 @@ public:
     void set_line(unsigned p) { return m_scanner.set_line(p); }
 
     expr mk_app(expr fn, expr arg, pos_info const & p);
+    expr mk_app(expr fn, buffer<expr> const & args, pos_info const & p);
     expr mk_app(std::initializer_list<expr> const & args, pos_info const & p);
 
     unsigned num_threads() const { return m_num_threads; }

tests/lean/change1.lean

@@ -13,7 +13,7 @@ by do intro `Heq,
       trace_state,
       get_local `a >>= subst,
       t ← target,
-      match is_eq t with
-      | some (lhs, rhs) := do pr ← mk_app `eq.refl [lhs], exact pr
-      | none            := failed
+      match (is_eq t) with
+      | (some (lhs, rhs)) := do pr ← mk_app `eq.refl [lhs], exact pr
+      | none              := failed
       end

tests/lean/change2.lean

@@ -11,7 +11,7 @@ by do intro `Heq,
       trace "---- after dsimp ----",
       trace_state,
       t ← target,
-      match is_eq t with
-      | some (lhs, rhs) := do pr ← mk_app `eq.refl [lhs], exact pr
-      | none            := failed
+      match (is_eq t) with
+      | (some (lhs, rhs)) := do pr ← mk_app `eq.refl [lhs], exact pr
+      | none              := failed
       end

tests/lean/match_bug.lean.expected.out

@@ -1 +1 @@
-match_bug.lean:3:6: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
+match_bug.lean:3:6: error: invalid expression

tests/lean/run/assoc_flat.lean

@@ -3,13 +3,13 @@ open tactic expr
 
 meta_definition is_op_app (op : expr) (e : expr) : option (expr × expr) :=
 match e with
-| app (app fn a1) a2 := if op = fn then some (a1, a2) else none
-| _                  := none
+| (app (app fn a1) a2) := if op = fn then some (a1, a2) else none
+| _                    := none
 end
 
 meta_definition flat_with (op : expr) (assoc : expr) (e : expr) (rhs : expr) : tactic (expr × expr) :=
-match is_op_app op e with
-| some (a1, a2) :=  do
+match (is_op_app op e) with
+| (some (a1, a2)) :=  do
   -- H₁ is a proof for a2 + rhs = rhs₁
   (rhs₁, H₁)     ← flat_with op assoc a2 rhs,
   -- H₂ is a proof for a1 + rhs₁ = rhs₂
@@ -29,8 +29,8 @@ match is_op_app op e with
 end
 
 meta_definition flat (op : expr) (assoc : expr) (e : expr) : tactic (expr × expr) :=
-match is_op_app op e with
-| some (a1, a2) := do
+match (is_op_app op e) with
+| (some (a1, a2)) := do
   -- H₁ is a proof that a2 = new_a2
   (new_a2, H₁)   ← flat op assoc a2,
   -- H₂ is a proof that a1 + new_a2 = new_app
@@ -54,8 +54,8 @@ by do
   assoc : expr ← mk_const $ `nat.add_assoc,
   op : expr    ← mk_const $ `nat.add,
   tgt          ← target,
-  match is_eq tgt with
-  | some (lhs, rhs) := do
+  match (is_eq tgt) with
+  | (some (lhs, rhs)) := do
     r ← flat op assoc lhs,
     trace (prod.pr2 r),
     exact (prod.pr2 r)

tests/lean/run/match3.lean

@@ -3,8 +3,8 @@ open nat
 
 definition foo (a : nat) : nat :=
 match a with
-| zero   := zero
-| succ n := n
+| zero     := zero
+| (succ n) := n
 end
 
 example : foo 3 = 2 := rfl
@@ -16,9 +16,9 @@ protected theorem dec_eq : ∀ x y : nat, decidable (x = y)
 | dec_eq (succ x) zero     := ff (λ h, nat.no_confusion h)
 | dec_eq zero     (succ y) := ff (λ h, nat.no_confusion h)
 | dec_eq (succ x) (succ y) :=
-  match dec_eq x y with
-  | tt H := tt (eq.rec_on H rfl)
-  | ff H := ff (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
+  match (dec_eq x y) with
+  | (tt H) := tt (eq.rec_on H rfl)
+  | (ff H) := ff (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
   end
 
 section
@@ -31,9 +31,9 @@ section
   definition filter : list A → list A
   | filter nil      := nil
   | filter (a :: l) :=
-    match H a with
-    | tt h := a :: filter l
-    | ff h := filter l
+    match (H a) with
+    | (tt h) := a :: filter l
+    | (ff h) := filter l
     end
 
   theorem filter_nil : filter nil = nil :=
@@ -45,9 +45,9 @@ end
 
 definition sub2 (a : nat) : nat :=
 match a with
-| 0   := 0
-| 1   := 0
-| b+2 := b
+| 0     := 0
+| 1     := 0
+| (b+2) := b
 end
 
 example (a : nat) : sub2 (succ (succ a)) = a := rfl

tests/lean/run/match_convoy.lean

@@ -0,0 +1,50 @@
+definition foo (a b : bool) : bool :=
+match a b with
+| tt ff := tt
+| tt tt := tt
+| ff tt := tt
+| ff ff := ff
+end
+
+example : foo tt tt = tt := rfl
+example : foo tt ff = tt := rfl
+example : foo ff tt = tt := rfl
+example : foo ff ff = ff := rfl
+
+inductive vec (A : Type) : nat → Type :=
+| nil {} : vec A nat.zero
+| cons   : ∀ {n}, A → vec A n → vec A (nat.succ n)
+
+open vec
+
+definition boo (n : nat) (v : vec bool n) : vec bool n :=
+match n v : ∀ (n : _), vec bool n → _ with
+| 0      nil       := nil
+| (n+1) (cons a v) := cons (bool.bnot a) v
+end
+
+
+constant bag_setoid : ∀ A, setoid (list A)
+attribute [instance] bag_setoid
+
+definition bag (A : Type) : Type :=
+quot (bag_setoid A)
+
+constant subcount : ∀ {A}, list A → list A → bool
+constant list.count : ∀ {A}, A → list A → nat
+constant all_of_subcount_eq_tt : ∀ {A} {l₁ l₂ : list A}, subcount l₁ l₂ = tt → ∀ a, list.count a l₁ ≤ list.count a l₂
+constant ex_of_subcount_eq_ff : ∀ {A} {l₁ l₂ : list A}, subcount l₁ l₂ = ff → ∃ a, ¬ list.count a l₁ ≤ list.count a l₂
+definition count {A} (a : A) (b : bag A) : nat :=
+quot.lift_on b (λ l, list.count a l)
+  (λ l₁ l₂ h, sorry)
+definition subbag {A} (b₁ b₂ : bag A) := ∀ a, count a b₁ ≤ count a b₂
+infix ⊆ := subbag
+
+definition decidable_subbag [instance] {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) :=
+quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂,
+  match (subcount l₁ l₂) rfl : ∀ (b : _), subcount l₁ l₂ = b → _ with
+  | tt H := decidable.tt (all_of_subcount_eq_tt H)
+  | ff H := decidable.ff (λ h,
+            exists.elim (ex_of_subcount_eq_ff H)
+            (λ w hw, absurd (h w) hw))
+  end)

tests/lean/run/sigma_match.lean

@@ -7,7 +7,7 @@ definition arrow_ob [reducible] (A B : Type) : Type :=
 
 definition src1 {A B : Type} (x : arrow_ob A B) : A :=
 match x with
-  sigma.mk a (sigma.mk b h) := a
+  (sigma.mk a (sigma.mk b h)) := a
 end
 
 definition src2 {A B : Type} : arrow_ob A B → A
@@ -15,7 +15,7 @@ definition src2 {A B : Type} : arrow_ob A B → A
 
 definition src3 {A B : Type} (x : arrow_ob A B) : A :=
 match x with
-  sigma.mk a (sigma.mk _ _) := a
+  (sigma.mk a (sigma.mk _ _)) := a
 end
 
 example (A B : Type) (x : arrow_ob A B) : src1 x = src2 x :=

tests/lean/run/test_flat_assoc1.lean

@@ -7,9 +7,9 @@ meta_definition is_poly_bin_app : expr → option name
 | _  := none
 
 meta_definition is_add (e : expr) : bool  :=
-match is_poly_bin_app e with
-| some op := to_bool (op = `add)
-| none    := ff
+match (is_poly_bin_app e) with
+| (some op) := to_bool (op = `add)
+| none      := ff
 end
 
 meta_definition flat_add (e : expr) : tactic (expr × expr) :=

tests/lean/run/test_perm_ac1.lean

@@ -7,9 +7,9 @@ meta_definition is_poly_bin_app : expr → option name
 | _  := none
 
 meta_definition is_add (e : expr) : bool  :=
-match is_poly_bin_app e with
-| some op := to_bool (op = `add)
-| none    := ff
+match (is_poly_bin_app e) with
+| (some op) := to_bool (op = `add)
+| none      := ff
 end
 
 meta_definition perm_add (e1 e2 : expr) : tactic expr :=