Parsing one tactic

Stream: metaprogramming / tactics

[Leni Aniva]

Why does Lean's parser consider intro n\ncases n to be a single tactic?

import Lean.Elab
open Lean

#eval show MetaM _ from do
  let input := "intro n\ncases n"
  let env ← getEnv
  let result? := Parser.runParserCategory env `tactic input
  match result? with
  | .ok s =>
    logInfo "One tactic!"
    logInfo s!"{s}"
  | .error e =>
    logError s!"Not one tactic!: {e}"

If we take this at face value and use evalTactic on this composite tactic, cases n would not run normally.

[Aaron Liu]

intro n cases n where cases is treated as the variable name to intro, I'm guessing

[Aaron Liu]

if you want a tactic seq then parse it as a tacticSeq

[Leni Aniva]

Aaron Liu said:

intro n cases n where cases is treated as the variable name to intro, I'm guessing

but in this case, there is a newline between the two tactics. If I write the tactics down in by-block they would be considered separate tactics.

[Leni Aniva]

Aaron Liu said:

if you want a tactic seq then parse it as a tacticSeq

If I set the category to tacticSeq it prints <input>:1:0: unknown parser category 'tacticSeq'.

[Kyle Miller]

It's because there's no "withPosition" set and the tactics don't know which column they're supposed to align to, so, for example, intro doesn't know it shouldn't keep consuming identifiers

[Kyle Miller]

That's what the colGt in the tactic syntax is preventing, but it only works if this bit of the parser state is enabled.

[Kyle Miller]

Leni Aniva said:

If I set the category to tacticSeq it prints <input>:1:0: unknown parser category 'tacticSeq'.

Yes, that's the expected error, since tacticSeq isn't a parser category, it's a parser.

[Kyle Miller]

You could make a new parser category and then give it one syntax definition, something like withPosition(tactic)

[Leni Aniva]

or maybe I can define my own runParserCategory analog that calls into withPosition?