Custom errors from macro-elaborated code?

Stream: lean4

[David Thrane Christiansen]

I just wrote a little macro that programming-minded people might enjoy. It's to allow simple tests to be embedded in a file:

syntax "test" term:60 "=" term:60 ":" term:60 : command
syntax "test" term:60 "=" term:60 : command

macro_rules
  | `(test $x:term = $y:term : $type:term) => `(def someTest : ($x : $type) = ($y : $type) := rfl)
  | `(test $x:term = $y:term) => `(def someTest : $x = $y := rfl)

test 1 = 1 : Nat
test 1 = 1
test 1 + 1 = 2

Unfortunately , failing tests get a pretty unhelpful error message, phrased in terms of the macro's expansion to rfl:

test 1 + 1 = 3

type mismatch
   rfl
 has type
   1 + 1 = 1 + 1 : Prop
 but is expected to have type
   1 + 1 = 3 : Prop

Is there a nice way to catch and rewrite that error message? Or perhaps I need to expand to a tactic script instead, to get more control of what's going on?

[David Thrane Christiansen]

In particular, I'd like the error message for this example to be something like:

Expected 3, but got 2

[Simon Hudon]

Nice macro!

I don't think a macro will let you do that but if you use elab_rules instead of macro_rules, you can use tactic-like code and check that the two expressions are definitionally equal and throw the exact error message that you want if they're not

[Simon Hudon]

I'm surprised that you don't get a name clash between your test cases. I expected that the name hygiene was just for local declarations

[David Thrane Christiansen]

Thanks!

RE hygiene, it seems to work here, which is what the Schemer in me expected. Also, I checked whether I could refer to someTest afterwards, and I could not, which is what I'd expect with hygiene. It's quite common for Racket macros to emit helper definitions, after all, and hygiene makes this work predictably.

Do you know any code in the wild with some examples of elab_rules? As far as I can see, it is used only once in the Lean 4 repository, and that's a fairly minimal test.

[Mario Carneiro]

there are 6 occurrences in mathlib4

[Mario Carneiro]

it looks like the main use is when we want to write an elab tactic but only for some subset or special case of the actual syntax of the tactic

[Arthur Paulino]

You may be able to find more examples of elaboration functions in the Lean 4 source code. Organizing the code along these lines might help:

syntax (name := testStx) "#test " term:60 " = " term:60 (" : " term:60)? : command

open Lean.Elab.Command in
@[commandElab testStx] def elabTest : CommandElab := fun stx =>
  dbg_trace stx
  match stx with
  | `(#test $x:term = $y:term $[: $t:term]?) => do
    dbg_trace x
    dbg_trace y
    dbg_trace t
  | _ => Elab.throwUnsupportedSyntax

#test 1 = 1 : Nat
-- (testStx "#test" (numLit "1") "=" (numLit "1") [":" `Nat])
-- (numLit "1")
-- (numLit "1")
-- (some `Nat)

#test 1 = 2
-- (testStx "#test" (numLit "1") "=" (numLit "1") [])
-- (numLit "1")
-- (numLit "2")
-- none

Your code will run in the Lean.Elab.Command.CommandElabM monad

[Arthur Paulino]

You can search for functions tagged with @[commandElab ⋯] for examples

[David Thrane Christiansen]

Thanks, this is really helpful! I think it's time to hit the sack, but I'll revisit this next time I get a moment.

[Arthur Paulino]

And I forgot to mention that you can use try/catch/finally routines there. Or even throw errors with customized messages: throwError "my error message"

[Leonardo de Moura]

@David Thrane Christiansen Here is an example

import Lean

syntax "test" term:60 "=" term:60 : command

elab_rules : command
  | `(test $x:term = $y:term) =>
    open Lean.Elab.Command in
    open Lean.Elab.Term in
    open Lean.Meta in liftTermElabM `test do
      let x ← elabTerm x none
      let y ← elabTerm y none
      synthesizeSyntheticMVarsNoPostponing
      unless (← isDefEq x y) do
        throwError "Expected {y}, but got {← reduce x}"

test 1 = 1
test 1 + 1 = 2
test 1 + 1 = 3 -- error: Expected 3, but got 2

[Arthur Paulino]

@Leonardo de Moura It got me thinking... would it be possible to code it in the CommandElabM monad? What would be an alternative solution to elabTerm?

[Leonardo de Moura]

The code after => is in the CommandElabM monad, but I immediately used liftTermElabM to move to TermElabM.

[Arthur Paulino]

Oh, right! Thanks

[Leonardo de Moura]

The TermElabM tracks a lot of extra information: pending elaboration problems, pending tactics to be executed, etc.

[Arthur Paulino]

Is there a place from where I can learn more about these monads roles, hierarchies and transitions?
In your code you went from the CommandElabM to the TermElabM and I didn't know that was possible. And then you talked about the TermElabMonadM and I don't know where it fits in the context of this conversation

[Mario Carneiro]

I recall a diagram of the relation between the monads in Leo's lean 4 presentation from Lean Together 2021

[Leonardo de Moura]

Unfortunately, the only place right now is the Lean source code itself :( TermElabMonadM was typo. Sorry about that.

[Mario Carneiro]

Page 5 of https://leanprover-community.github.io/lt2021/slides/leo-LT2021-meta.pdf

[Leonardo de Moura]

We are currently overwhelmed. I think we will be able to greatly improve the documentation for end-users in the next few months, but we currently do not have a plan for documenting the Lean internals.

[Arthur Paulino]

Leonardo de Moura said:

We are currently overwhelmed. I think we will be able to greatly improve the documentation for end-users in the next few months, but we currently do not have a plan for documenting the Lean internals.

Np, I just wanted to know about already existing sources

[Arthur Paulino]

Mario Carneiro said:

Page 5 of https://leanprover-community.github.io/lt2021/slides/leo-LT2021-meta.pdf

So, I've seen that diagram but I don't understand it. I'll open a dedicated thread to ask questions about it

[David Thrane Christiansen]

This is great, thanks Leo!