syntax subdefinitions, elaboration function for …

Stream: lean4

[Joachim Breitner]

I have

syntax (name := find_theorems)
  withPosition("#find_theorems" (colGt (strLit <|> ident <|> conclusion_pattern <|> term:max))+) : comman

and it works, but I’d like to make this prettier and name the syntax for the arguments. If I write

syntax find_pattern :=
  strLit <|> ident <|> conclusion_pattern <|> term:max

syntax (name := find_theorems)
  withPosition("#find_theorems" (colGt find_pattern)+) : comman

instead, however, I get

elaboration function for 'find_pattern' has not been implemented
  "all"

when trying to use it. I tried some unstructured cargo-culting, but couldn’t get it to work. Why do I need an elaboration function here when I am parsing the syntax in the elaboration function for the command?

(I should try to come up with a #mwe)

[Joachim Breitner]

Ok, got it to work somehow. The problem was that abstracting out definitions like this wraps the syntax in a new node, with the definition names as the “syntax node“ of the things parsed, and if I pass them to Lean.Elab.Term.elabTerm that functions complains. But the real problem was these extra wrappers, that I ought to remove before passing to Lean.Elab.Term.elabTerm. I now have this code:

syntax name_pattern := strLit
syntax ident_pattern := ident
syntax turnstyle := "⊢ " <|> "|- "
syntax conclusion_pattern := turnstyle term:max
syntax term_pattern := term:max
syntax find_pattern := name_pattern <|> ident_pattern <|> conclusion_pattern <|> term_pattern
syntax (name := find_theorems) withPosition("#find_theorems" (colGt find_pattern)+) : command

which I process with this fragment:

    match stx with
      | `(command|#find_theorems $args:find_pattern*) =>
      for arg in args do
        match arg with
        | `(find_pattern|$ss:str) => do
          let str := Lean.TSyntax.getString ss
          name_pats := name_pats.push str
        | `(find_pattern|$i:ident) => do
          let n := Lean.TSyntax.getId i
          unless (← getEnv).contains n do
            throwErrorAt i "Name {n} not in scope"
          idents := idents.push n
        | `(find_pattern| $_:turnstyle $s) => do
          let t ← Lean.Elab.Term.elabTerm s none
          terms := terms.push (true, t)
        | `(find_pattern| $s) => do
          let t ← Lean.Elab.Term.elabTerm s.raw[0][0] none
          terms := terms.push (false, t)
      | _ => return -- unreachable?

which I fear is rather non-idiomatic, but at least it works :)

[Mac Malone]

Joachim Breitner said:

      | _ => return -- unreachable?

Note that this is reachable if another macro (accidently) produces an ill-formed find_pattern node. So, ideally, you should error here. The standard error is Elab.throwUnsupportedSyntax or Macro.throwUnsupported, but a more informative error using throwErrorAt or Macro.throwErrorAt is usually much nicer for the downstream debugger.

[Sebastian Ullrich]

Use $s:term to select the nested term node. Also, you should be able to use i.getId etc

[Sebastian Ullrich]

Joachim Breitner said:

      | _ => return -- unreachable?

Perhaps in some far future we will actually get an exhaustiveness checker for TSyntax matches :)

[Joachim Breitner]

Thanks. So a $s:termpattern will look inside syntax nodes, searching for a neated one with the right tag? Neat!
(The fog slowly retreats :-))

[Mario Carneiro]

Mac Malone said:

Joachim Breitner said:

      | _ => return -- unreachable?

Note that this is reachable if another macro (accidently) produces an ill-formed find_pattern node. So, ideally, you should error here. The standard error is Elab.throwUnsupportedSyntax or Macro.throwUnsupported, but a more informative error using throwErrorAt or Macro.throwErrorAt is usually much nicer for the downstream debugger.

@Sebastian Ullrich is it still the case that the unreachable case is also hit if the syntax is incomplete or ill-formed and the parser produces .missing nodes?

[Sebastian Ullrich]

If it is sufficiently ill-formed or incomplete not to match the previous patterns, then certainly, yes. How missing should interact with TSyntax is an interesting but likely complex question that I don't have an answer for currently.

[Scott Morrison]

Is there a reason you made the synonyms syntax name_pattern := strLit, etc? Seems better just to skip these and use the existing names.

[Joachim Breitner]

I tried, but somehow I then got errors I didn't understand, or the types of the TSyntax variables further below changed in ways I didn't understand! I'd be grateful if someone could show me how I can avoid these extra definitions.