Zulip Chat Archive

Stream: lean4

Topic: expr pattern matching


view this post on Zulip Reid Barton (Feb 03 2021 at 16:25):

Is there syntax like `(%%a ∧ %%b) for matching against expr in Lean 4? We use this frequently in mathlib tactics, e.g., https://github.com/leanprover-community/mathlib/blob/master/src/tactic/push_neg.lean#L43

view this post on Zulip Reid Barton (Feb 03 2021 at 16:26):

This syntax seems to be used for matching syntax in Lean 4 and I couldn't figure out how to get it to match expr instead

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 16:33):

There isn't, because we had no need for it so far. I'm not actually sure if the ideal solution is to bring it back as-is. In your experience, is matching expr structurally instead of by unfication in fact the correct behavior in most cases, or is it merely that the former is easier to write down in Lean 3?

view this post on Zulip Reid Barton (Feb 03 2021 at 16:42):

Hmm, I'm not sure really. We definitely don't want to do semireducible matching usually; if prime p means 2 ≤ p ∧ ∀ m ∣ p, m = 1 ∨ m = p then we don't want push_neg to unfold that. But we don't use reducible definitions very often, so I don't know whether it would make sense to unfold them or not.

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 16:50):

Fwiw, note that match with syntax quotations is in fact a macro completely separate from "constructor match". So there's precedent showing that custom match constructs can be introduced modularly (...almost. Identification of pattern variables is currently hard-coded).

view this post on Zulip Mario Carneiro (Feb 03 2021 at 17:31):

I think the only thing expr match should do by default that it doesn't currently do is instantiate metavariables

view this post on Zulip Mario Carneiro (Feb 03 2021 at 17:31):

(and only as needed to resolve a match against a metavariable)

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 17:35):

You mean in the discriminant?

view this post on Zulip Mario Carneiro (Feb 03 2021 at 17:36):

I'm not sure what you mean. If you match against %%a /\ %%b and the expr is ?m where ?m := a /\ b then the match should work and assign a and b

view this post on Zulip Mario Carneiro (Feb 03 2021 at 17:36):

but it shouldn't do anything else to the expression like unfold definitions

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 17:38):

Yes, the expression(s) after match is called the discriminant in GHC lingo. So expr match would need to become monadic to support your case :grimacing: .

view this post on Zulip Mario Carneiro (Feb 03 2021 at 17:38):

It need not be syntactically match

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 17:39):

But it could be! :)

view this post on Zulip Mario Carneiro (Feb 03 2021 at 17:39):

I just want the ability to do that, and easily enough that I won't accidentally use match instead

view this post on Zulip Mario Carneiro (Feb 03 2021 at 17:39):

because not instantiating metavariables in that position is a recurring source of bugs

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 17:41):

We originally had a separate match_syntax syntax, but reusing match is very convenient in practice because it means you can immediately use it with macros on top of it, e.g.

fun
| `(foo) => ...

view this post on Zulip Mario Carneiro (Feb 03 2021 at 17:41):

It's not uncommon to use things like `(%%a /\ %%b) <- pure e, putting things in the monad anyway even though it's not monadic, just because the left arrow gets this pattern match sugar

view this post on Zulip Mario Carneiro (Feb 03 2021 at 17:41):

+1 to that

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 17:45):

So this match (and its RHSs) would have type m A where [MonadMCtx m]

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 17:46):

Yeah, I definitely think this would be great to have outside the stdlib :)

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 17:51):

It's funny that the situation is exactly the opposite from syntax quotations: those are monadic when used as terms (because of hygiene), but their match is non-monadic

view this post on Zulip Sebastian Ullrich (Feb 03 2021 at 18:04):

FWIW, I'd like to establish `[A|...] as the standard syntax for parsing a term of type A (using A's "standard DSL" if any) and returning its evaluation: https://twitter.com/derKha/status/1354082976456441861
So it would be `[Expr|e] , and one could also (re)introduce `[Tactic|t] as a simple macro for evalTactic (<- `(tactic|t))(though strictly speaking that term is of type TacticM Unit, not Tactic, which additionally takes a Syntax)


Last updated: May 18 2021 at 23:14 UTC