How to write custom patterns

Stream: new members

[MrQubo]

I couldn't find any information on how to write custom patterns. I only found about @[match_pattern], but it is not applicable in many cases.

Is it possible to implement for example something similar to that haskell code?

{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}

data Foo = Foo Int Int

add :: Foo -> Int
add (Foo a b) = a + b

pattern FooAdd :: Int -> Foo
pattern FooAdd x <- (add -> x)

foo :: Foo -> Bool
foo (FooAdd 5) = True
foo _ = False

-- |
-- >>> foo (Foo 2 3)
-- True
-- >>> foo (Foo 4 1)
-- True
-- >>> foo (Foo 2 2)
-- False

And, another MWE more in line with my actual problem, is how to make this Foo.succ pattern work, like in m₁. I.e. it should match x on pattern { val := Nat.succ i, prop }, and then it should construct y from matched values (i and prop), as y = { val := i, prop := by injection prop }.

set_option pp.proofs true

structure Foo (n : Nat) where
  val : Nat
  prop : val = n

def m₁ {n} (x : Foo n.succ) : Foo n :=
  match x with
  | { val := Nat.succ i, prop } => { val := i, prop := by injection prop }

@[match_pattern]
def Foo.succ {n} (v : Foo n) : Foo n.succ := { val := v.val.succ, prop := congrArg Nat.succ v.prop }

def m₂ {n} (x : Foo n.succ) : Foo n :=
  match x with
  | Foo.succ y => y

[Kyle Miller]

The only options right now are @[match_pattern] or writing a completely custom match command, sorry.

[Kyle Miller]

Maybe there's an unexplored hack where you make a term that elaborates differently when it's used in a pattern context... but I haven't tried it.

[Kyle Miller]

Hmm, Nat.succ (Foo.val y) isn't a valid match pattern due to the Foo.val projection.

[MrQubo]

Yes, it is not. y requires to also specify value of prop, which cannot be infered from that pattern. In math terms, it's like asking for an inverse of a projection.

[Kyle Miller]

Yeah, I guess fundamentally the problem is that Foo.succ v =?= x needs to somehow solve for v. I'm not sure how it could unify congrArg Nat.succ v.prop =?= x.prop to solve for v without some ad hoc method.

[Kyle Miller]

(Just checking that the unifier has no tricks up its sleeve:

variable {n : Nat} {x : Foo n.succ}
#check (rfl : Foo.succ _ = x)
/-
type mismatch
  rfl
has type
  ?m.2499 = ?m.2499 : Prop
but is expected to have type
  Foo.succ ?m.2471 = x : Prop
-/

)

[MrQubo]

So with the macro approach you suggested, I would probably need to write a macro that rewrites | Foo.succ $y:ident => $t:term in match to something like | { val := Nat.succ _i, prop := _prop } => let $y = { val := _i, prop := by injection _prop }; $t?

I will try to implement that.

[MrQubo]

I've tried like this, but that doesn't work. I think that the error "invalid pattern" comes from here: https://github.com/leanprover/lean4/blob/b81dd3e7adb5252a89afb5d9abfc14ee54e59881/src/Lean/Elab/PatternVar.lean#L270.
Seems like my macro isn't being run at all.

import Lean

structure Foo (n : Nat) where
  val : Nat
  prop : val = n

open Lean Parser.Term

syntax "foo_succ" ident : term

@[macro Lean.Parser.Term.matchAlt]
def foo_succ_impl : Macro
  | `(matchAltExpr| | foo_succ $y:ident => $t:term ) =>
    `(matchAltExpr|
      | { val := Nat.succ _i, prop := _prop } =>
        --match { val := i, prop := by injection _prop } with
        --  | $y => $t
        let $y := { val := i, prop := by injection _prop }; $t
    )
  | _ => Macro.throwUnsupported

def m₂ {n} (x : Foo n.succ) : Foo n :=
  match x with
  | foo_succ y => y

[Kyle Miller]

A macro gotcha is that macros don't indiscriminately expand, but instead they expand in particular places. For example, terms and macros get macro expanded in their entirety.

We can simulate this with match alts by adding a macro for match that expands matchAlt macros.

import Lean

structure Foo (n : Nat) where
  val : Nat
  prop : val = n

open Lean Parser.Term

syntax "foo_succ" ident : term

@[macro Lean.Parser.Term.matchAlt]
def foo_succ_impl : Macro
  | `(matchAltExpr| | foo_succ $y:ident => $t:term ) =>
    `(matchAltExpr|
      | { val := Nat.succ _i, prop := _prop } =>
        let $y := { val := _i, prop := by injection _prop }; $t
    )
  | _ => Macro.throwUnsupported

@[macro Lean.Parser.Term.match]
def expandMatchAlts : Macro := fun stx => do
  /-
  @[builtin_term_parser] def «match» := leading_parser:leadPrec
    "match " >> optional generalizingParam >> optional motive >> sepBy1 matchDiscr ", " >>
    " with" >> ppDedent matchAlts
  -/
  let mut alts := stx[5][0].getArgs
  let mut changed := false
  for i in [0:alts.size] do
    if let some alt ← expandMacro? alts[i]! then
      alts := alts.set! i alt
      changed := true
  if changed then
    return stx.setArg 5 <| stx[5].setArg 0 <| stx[5][0].setArgs alts
  else
    Macro.throwUnsupported

def m₂ {n} (x : Foo n.succ) : Foo n :=
  match x with
  | foo_succ y => y

[MrQubo]

Thanks!
Though, I still don't understand, why match gets expanded, and matchAlt doesn't?
Is it because match term is already expanded using some internal function, and that function doesn't expand macros?

[MrQubo]

Looking at the code for elabMatch it seems like it might expand Lean.Parser.Term.matchAlts, but not Lean.Parser.Term.matchAlt. nvm

[Kyle Miller]

It's because the term elaborator's steps are

1. see if the current term has a macro expansion, if so expand and go back to 1.
2. see if there is an elaborator for this term. if so, apply it, and return the result.
3. otherwise, thrown a 'no such elaborator' error

Macro expansion isn't applied to subterms before we're actually considering them for elaboration.

There's a similar flow for commands and tactics, but tactics have a backtracking version of macro expansion, where if the macro expansion leads to a tactic error, it backtracks and tries the next applicable macro.

[Kyle Miller]

match is a term, so its macros get applied, matchAlt is just some syntax that goes into a match, so macros don't get applied unless we explicitly create our own macro driver (like I did)