Syntax of tactic sequence

Stream: lean4

[Jon Eugster]

I'm trying to understand lean's Syntax better, in particular tacticSeq1Indented.

In particular this is a Syntax.node info `tacticSeq1Indented args where args is an Array Syntax containing a single null-node Syntax.node info `null args2. Now args2 is another Array Syntax containing the tactics of the sequence, but also another null-node Syntax.node info `null #[] between any two tactics.

Can anybody explain what the function of these null-nodes is? I don't understand either use case and naively have the impression that everything would work just as well if they didn't exist.

below is a #mwe that matches the syntax of args for demonstration

MWE

import Lean

open Lean

partial
def modifySyntax (tacs : Syntax) : Syntax :=
  match tacs with
  | Syntax.node info kind ⟨args⟩ =>
    match kind with
    | `Lean.Parser.Tactic.tacticSeq1Indented =>
      dbg_trace s!"args for tacticSeq1Indented:\n{args}\n"

      match args with
      -- The `args` of `tacticSeq1Indented`. What's the purpose of the two different null-nodes?
      | Syntax.node info `null ⟨_ :: (Syntax.node _ `null #[]) :: _⟩ :: [] =>
        dbg_trace s!"yes"
        Syntax.node info kind ⟨args.map modifySyntax⟩
      | _ =>
        dbg_trace "nope"
        Syntax.node info kind ⟨args.map modifySyntax⟩
    | _ => Syntax.node info kind ⟨args.map modifySyntax⟩
  | _ => tacs

elab "MyTactic" tacs:tacticSeq : tactic => do
  let out := modifySyntax tacs.raw
  let x ← PrettyPrinter.ppCategory `Lean.Parser.Tactic.tacticSeq out

example : 100 > 99 := by
  MyTactic
    simp
    assumption
  decide

[Mario Carneiro]

the null nodes are the separators between tactics, they are actually optional ";"

[Mario Carneiro]

check out what happens if you use simp; instead of simp

[Jon Eugster]

Then you get a Syntax.atom info ";" in between the two tactics instead, yes.

[Jon Eugster]

And the first null-node wrapping the list?

[Mario Carneiro]

that's the list itself

[Mario Carneiro]

it gets packed up as one argument because tacticSeq1Indented itself has one argument, which is a tactic;* (more or less)

[Jon Eugster]

ah and it would be impossible in lean to define tacticSeq1Indented with arbitrary number of arguments, I guess?

and likewise I assume it would be more effort to find out if the next entry was a ";" or a new tactic, so it just inserts a null-node and then assumes that every other node is just a separator?

Thanks for the explanation!

[Mario Carneiro]

not impossible, just irregular

[Mario Carneiro]

it helps to have some standardized structure in syntax so that stuff like syntax-match works properly

[Mario Carneiro]

basically the only variadic syntaxes are many,many1, sepBy, sepBy1 and they all produce null nodes

[Mario Carneiro]

and "regular" syntax node constructors all have a statically known number of arguments

[Mario Carneiro]

(this was not always the case, but exceptions usually ended up as bug reports because something wouldn't handle them correctly)

[Jon Eugster]

I see, that makes sense!

I was a bit confused because I tried to parse a tactic sequence removing all occurences of a tactic Hint and I thought it looked a bit cumbersome:

  match args with
    | [] => []
    -- delete all `Hint` occurences in the middle of the sequence.
    | Syntax.node _ `GameServer.Tactic.Hint _ :: _ :: r
      filterArgs r
    -- delete `Hint` occurence at the end of the sequence
    | Syntax.node _ `GameServer.Tactic.Hint _ :: []
        []
    -- just recurse over any other type of syntax
    | a :: rest =>
      replaceHoles a :: filterArgs rest

(where replaceHoles and filterArgs are the recursive functions containing this snippet)

[Sebastian Ullrich]

Was there some part that did not work out with syntax quotation patterns?

[Jon Eugster]

probably only that I don't know how to use them...

[Jon Eugster]

I want to take a sequence of tactics and execute it, but also store it as a string ("template") where I delete my custom tactics that appear within that tactic block:
roughly this non-mwe

def replaceHoles (tacs : Syntax) : Syntax :=
  match tacs with
  | Syntax.node info kind ⟨args⟩ => Syntax.node info kind ⟨filterArgs args⟩
  | other => other
where filterArgs (args : List Syntax) : List Syntax :=
  match args with
    | [] => []
    -- replace `Hole` with `sorry`.
    | Syntax.node info `GameServer.Tactic.Hole _ :: r =>
      Syntax.node info `Lean.Parser.Tactic.tacticSorry #[Syntax.atom info "sorry"] :: filterArgs r
    -- delete all `Hint` and `Branch` occurences in the middle.
    | Syntax.node _ `GameServer.Tactic.Hint _ :: _ :: r
    | Syntax.node _ `GameServer.Tactic.Branch _ :: _ :: r =>
      filterArgs r
    -- delete `Hint` and `Branch` occurence at the end of the tactic sequence.
    | Syntax.node _ `GameServer.Tactic.Hint _ :: []
    | Syntax.node _ `GameServer.Tactic.Branch _ :: [] =>
        []
    -- Recurse on all other Syntax.
    | a :: rest =>
      replaceHoles a :: filterArgs rest

elab "Template" tacs:tacticSeq : tactic => do
  -- evaluate the tactic sequence
  Tactic.evalTactic tacs
  -- now save a string version of this tactic block
  let newTacs : TSyntax `Lean.Parser.Tactic.tacticSeq := ⟨replaceHoles tacs.raw⟩
  let template ← PrettyPrinter.ppCategory `Lean.Parser.Tactic.tacticSeq newTacs
  pure () -- more stuff

is this the wrong approach? (i.e. is there a higher level way of doing this?)