Adding syntax for commands🔗

Contributors: ajay-k-nair, Siddhartha Gadgil

Lean allows you to define custom syntax for a command. As with terms, this can be done in a simple way with macro, or in a more complex way with elab. The elab approach is more powerful, since it allows you to generate an expression from the syntax and perform checks during elaboration. In this recipe, we will show how to define custom syntax for commands using elab, which lets you specify both the syntax and its elaboration in one place.

"Hello World" command🔗

We start with a simple example of a command that prints "Hello World". The following elab declaration tells Lean to parse #helloWorld as a command and explains what that command should do.

elab "#helloWorld" : command => do
    logInfo "Hello World!"

Hello World!#helloWorld

Here, logInfo s prints the string s in the InfoView.

Command for checking whether a proposition is solved by grind🔗

We define a custom command that tests whether a proposition can be solved automatically by the grind tactic. The goal is to provide a small command-line-style tool that reports whether grind can close a goal.

Again, we can define the command directly with elab. In the declaration below, Lean parses inputs of the form #grindable? <term> as a command, and the elaborator says how that command should behave.

elab "#grindable?" t:term : command => do
    Command.liftTermElabM do
      try
        withoutErrToSorry do
          let tExpr ← elabTerm t none
          let goal ← mkFreshExprMVar tExpr
          Term.synthesizeSyntheticMVarsNoPostponing
          let (goals,_) ← Elab.runTactic goal.mvarId!
                                (← `(tactic|grind))
          if goals.isEmpty then
            logInfo m!"{t} is grindable"
          else
            logInfo m!"grind failed with goals: {goals}"
      catch _ =>
        logInfo m!"{t} is not grindable"

∀ n : Nat, n + 0 = n is grindable#grindable? ∀ n : Nat, n + 0 = n -- grindable
∃ x : Nat, x > 100 is not grindable#grindable? ∃ x : Nat, x > 100 -- not grindable

Let's break down the specific metaprogramming functions used in the elaborator above:

The call to Command.liftTermElabM is needed because command elaboration happens in the CommandElabM monad, while elaborating terms and running tactics uses the term elaboration machinery in the TermElabM monad.
Lean's elaborator sometimes turns elaboration errors into sorries. withoutErrToSorry prevents that from happening, so we can catch the exceptions thrown while elaborating.
We write a try … catch block and place withoutErrToSorry inside the try block.
Lean.Elab.Term.elabTerm elaborates the user-provided proposition (i.e., t) into an expression.
Then mkFreshExprMVar creates a fresh metavariable goal whose type is given as an expression (i.e., tExpr).
Elab.runTactic runs the tactic grind on that fresh goal and returns a tuple of type List MVarId × Term.State. In this example, the first component is exactly the list of goals left open after grind, while the second component is the updated state of the TermElabM monad, which we ignore with _.
Finally, we inspect the remaining goals. If the list is empty, then grind managed to prove the proposition completely.

If you prefer to separate the syntax declaration from the elaboration logic, Lean also lets you define the syntax first with syntax and then add elaboration rules with elab_rules.

syntax "#grindable'?" term : command

elab_rules : command
|`(command| #grindable'? $t:term ) => do
    Command.liftTermElabM do
      try
        withoutErrToSorry do
          let tExpr ← elabTerm t none
          let goal ← mkFreshExprMVar tExpr
          Term.synthesizeSyntheticMVarsNoPostponing
          let (goals,_) ← Elab.runTactic goal.mvarId!
                                (← `(tactic|grind))
          if goals.isEmpty then
            logInfo m!"{t} is grindable"
          else
            logInfo m!"grind failed with goals: {goals}"
      catch _ =>
        logInfo m!"{t} is not grindable"

The elab_rules command lets us define elaboration rules by pattern matching on the command syntax that was parsed. Both styles are useful, but the direct elab form is often a good starting point for a compact one-off command, while syntax plus elab_rules is helpful when you want to separate the parser and elaborator more explicitly.