Extending match forms

Stream: lean4

[Kiran]

Hi yall!! Been playing aroud more with Lean and metaprogramming, and I've been trying recently to "extend" match with custom behaviours.

My situation is , that I have a opaque type that contains external data in C and can't be matched on.
Now I have a function to convert this opaque type into a lean representation, but most of my API calls use the opaque type directly.

To provide an ergonomic interface for the user, I'd like to make it such that the user can write code that matches on values of this type, but implicitly things are converted to the lean representation automatically (this I guess is kinda like how Int is handled in Lean, but for my custom type).

I've manageed to kinda get it working by defining my own elab rules for match, which will try to infer the type of the discriminant, and insert the conversion function automatically:

opaque Symbol: Type
inductive Repr | ...
opaque Symbol.Repr : Symbol -> Repr

elab_rules : term
| `(term| match $x:term with $m:matchAlts) => do
   let x_stx <- Term.elabTerm x (some (mkConst ``Symbol))
   let ty <- Meta.inferType x_stx
   let is_sym <- Meta.isDefEq ty (mkConst ``Symbol)
   if not is_sym then throwUnsupportedSyntax
   Term.elabTerm (<- `(term| match Symbol.repr $x:term with $m:matchAlts)) none

def f (n : Symbol) :=
 match n with
 | Repr.Infimum => 0
 | Repr.Supremum => 0
 | Repr.Function name args positive => 0
 | Repr.String s => 0
 | Repr.Number n => 0

I found this super nifty, but also seemed like a little bit of a hack.

As such, I'd like to ask the lean developers, what would be the idiomatic way of doing this?

[Eric Wieser]

Is there a reason you don't want to write match n.Repr with?

[Kiran]

Sure, that would work, but maybe out of academic curiousity, I'd like to try extending the match either way.

I guess kinda like the same reason that Lean doesn't make it's users call .repr on its ints before matching on them, like ease of use

[Kyle Miller]

I'm not sure how many examples there are of overriding match out there. The two that come to mind: (1) in core Lean, there's match syntax for matching against Syntax in https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Quotation.lean and (2) in Qq, there's match syntax for ~q(...) patterns for Expr in https://github.com/leanprover-community/quote4/blob/master/Qq/Match.lean

Both of these completely take over match elaboration.

[Kiran]

Ah, yep! I had seen quotation's approach, of overriding the match elaborator, but for some reason, when I try to use the annotation @[builtin_term_elab ...] it doesn't seem to work the same:

import Lean
open Lean
open Meta Elab

@[builtin_term_elab «match»] def elabMatchSyntax : Elab.Term.TermElab := Term.adaptExpander fun _stx _oexpr => do
  dbg_trace "running custom match {_stx}"
  throwUnsupportedSyntax

#eval match (1 - 2) with | 0 => true | _ => false

Prints 'true' and nothing else.

[Kyle Miller]

Anything with builtin_ is for boostrapping issues in core -- there's @[term_elab] for user notations

[Kiran]

Ahhh, awesome! Thanks I changed it, and now it works! So I overriding the elaborator is the best way of implementing this kind of functionality (most idiomatic way maybe?):

import Lean
open Lean
open Meta Elab

opaque Symbol : Type
inductive SymbolRepr where | Infinimum | Supremum | Number (n : Nat)
deriving Inhabited
opaque Symbol.repr : Symbol -> SymbolRepr

@[term_elab «match»] def elabMatchSyntax : Elab.Term.TermElab := fun _stx _oexpr =>
   match _stx with
   | `(term| match $x:term with $m:matchAlts) => do
      let x_stx <- Term.elabTerm x (some (mkConst ``Symbol))
      let ty <- Meta.inferType x_stx
      let is_sym <- Meta.isDefEq ty (mkConst ``Symbol)
      if not is_sym then throwUnsupportedSyntax
      Term.elabTerm (<- `(term| match Symbol.repr $x:term with $m:matchAlts)) none
   | _ => throwUnsupportedSyntax

#check fun (s : Symbol) => match s with | SymbolRepr.Infinimum => 0 | _ => 1

[Eric Wieser]

I think maybe this is _maybe_ an #xy problem; is your question actually

If I have a type

inductive SymbolRepr where | Infinimum | Supremum | Number (n : Nat)

how can I use implemented_by to give it a custom C in-memory implementation?

[Kiran]

Oh, if there's a solution to that problem that would be great as well!

(my question here was just about prompting for how Lean envisions the story for extending macros (in a programming context I guess, tactics being extensible is something well known from Rocq even))

[Kyle Miller]

For match, I think a long-term ideal is to be able to reconfigure what the constructors are for a type (this might be RFC lean4#2716) rather than solving the problem using just syntax transformations.

[Kyle Miller]

You'd want to be able to use these patterns everywhere patterns can be matched, and you want to be sure you're not accidentally getting in the way of any match features. An issue with your match macro is that it won't generalize the expected type and substitute in each match case, which is important for dependent types. But if the return type never depends on the variable you're matching against, this doesn't matter.