Parenthesizer error when creating do-blocks using TSyntax

Stream: metaprogramming / tactics

[Ernest Ng]

Hi! I'm trying to programmatically create a monadic do-block using TSyntax terms, but I keep running into a parenthesize: uncaught backtrack exception error when pretty-printing the do-block I've generated.

Here's a MWE -- I've defined a dummy command elaborator that triggers the issue:

import Lean
open Lean Elab Command Meta Term Parser

/-- `mkLetBind lhs rhsTerms` constructs a monadic let-bind expression of the form
    `let lhs ← e0 e1 … en`, where `rhsTerms := #[e0, e1, …, en]`.
    - Note: `rhsTerms` cannot be empty, otherwise this function throws an exception -/
def mkLetBind (lhs : Ident) (rhsTerms : TSyntaxArray `term) : MetaM (TSyntax ``Term.doSeq) := do
  let rhsList := rhsTerms.toList
  match rhsList with
  | f :: args =>
    let argTerms := args.toArray
    `(doSeq| let $lhs:term ← $f:term $argTerms* )
  | [] => throwError "rhsTerms can't be empty"


/-- Constructs a Lean monadic `do` block out of an array of `doSeq`s
    (expressions that appear in the `do` block) -/
def mkDoBlock (doBlockExprs : TSyntaxArray ``Term.doSeq) : MetaM (TSyntax `term) := do
  let doSeqElems := TSyntaxArray.mk doBlockExprs
  let doBlockBody ← `(doSeq| $doSeqElems*)
  `(do $doBlockBody)

-- Dummy monadic function for example purposes
def dummyMonadicFunc (n : Nat) : Option Nat := pure (n * 2)

-- Print the raw expr when the command elaborator below fails
set_option pp.rawOnError true


/- Example command elaborator that triggers the issue:
   In this example, we are trying to create the do-block
  ```
  do
     let x ← dummyMonadicFunc 1
     let y ← dummyMonadicFunc 2
     return (x, y)
  ```
-/
elab "#test_doblock" : command => do
  let mut doBlockExprs := #[]

  -- Creates `let x ← dummyMonadicFunc 1`
  let x := mkIdent $ Name.mkStr1 "x"
  let rhs1 := #[← `(dummyMonadicFunc), ← `(1)]
  let bind1 ← liftTermElabM $ mkLetBind x rhs1
  doBlockExprs := doBlockExprs.push bind1

  -- Creates `let y ← dummyMonadicFunc 2`
  let y := mkIdent $ Name.mkStr1 "y"
  let rhs2 := #[← `(dummyMonadicFunc), ← `(2)]
  let bind2 ← liftTermElabM $ mkLetBind y rhs2
  doBlockExprs := doBlockExprs.push bind2

  -- Creates `return (x, y)`
  let returnExpr ← `(doSeq| return ($x, $y))
  doBlockExprs := doBlockExprs.push returnExpr

  -- Creates the offending do-block
  -- This causes the exception `parenthesize: uncaught backtrack exception`
  let doBlock ← liftTermElabM $ mkDoBlock doBlockExprs
  logInfo m!"{doBlock}"

#test_doblock

I suspect the issue is that I am creating nested doSeqs, which causes the parenthesizer to complain, although I'm not sure how else to programmatically create do-blocks with let-bind expressions in them. Any advice would be much appreciated, thanks!

[Kyle Miller]

You diagnosed the problem correctly, you are creating invalid syntax, that's why it doesn't work :wink:

Any code that uses constructors like TSyntax.mk or TSyntaxArray.mk (like in mkDoBlock) must be done with a lot of care (or, better, be avoided!) since that circumvents the small amount of typechecking that the TSyntax system provides. In particular, there should always at least be a type ascription (otherwise you're at the mercy of the syntax quotations assigning types; here it comes up with TSyntaxArray `Lean.Parser.Term.doSeqItem) and then verify that the conversion is actually valid. Converting a Term.doSeq to a Lean.Parser.Term.doSeqItem is definitely not valid, since they have different internal Syntax structures. (doSeq has kind doSeqIndent or doSeqBracketed, but doSeqItem has kind doSeqItem)

The right kind of syntax to work with here is the syntax category doElem, since the body of a do is ultimately a list of them.

import Lean
open Lean Elab Command Meta Term Parser

/-- `mkLetBind lhs rhsTerms` constructs a monadic let-bind expression of the form
    `let lhs ← e0 e1 … en`, where `rhsTerms := #[e0, e1, …, en]`.
    - Note: `rhsTerms` cannot be empty, otherwise this function throws an exception -/
def mkLetBind (lhs : Ident) (rhsTerms : TSyntaxArray `term) : MetaM (TSyntax `doElem) := do
  let rhsList := rhsTerms.toList
  match rhsList with
  | f :: args =>
    let argTerms := args.toArray
    `(doElem| let $lhs:term ← $f:term $argTerms* )
  | [] => throwError "rhsTerms can't be empty"


/-- Constructs a Lean monadic `do` block out of an array of `doSeq`s
    (expressions that appear in the `do` block) -/
def mkDoBlock (doElems : TSyntaxArray `doElem) : MetaM (TSyntax `term) := do
  `(do $[$doElems:doElem]*)

-- Dummy monadic function for example purposes
def dummyMonadicFunc (n : Nat) : Option Nat := pure (n * 2)

-- Print the raw expr when the command elaborator below fails
set_option pp.rawOnError true


/- Example command elaborator that triggers the issue:
   In this example, we are trying to create the do-block
  ```
  do
     let x ← dummyMonadicFunc 1
     let y ← dummyMonadicFunc 2
     return (x, y)
  ```
-/
elab "#test_doblock" : command => do
  let mut doBlockExprs := #[]

  -- Creates `let x ← dummyMonadicFunc 1`
  let x := mkIdent $ Name.mkStr1 "x"
  let rhs1 := #[← `(dummyMonadicFunc), ← `(1)]
  let bind1 ← liftTermElabM $ mkLetBind x rhs1
  doBlockExprs := doBlockExprs.push bind1

  -- Creates `let y ← dummyMonadicFunc 2`
  let y := mkIdent $ Name.mkStr1 "y"
  let rhs2 := #[← `(dummyMonadicFunc), ← `(2)]
  let bind2 ← liftTermElabM $ mkLetBind y rhs2
  doBlockExprs := doBlockExprs.push bind2

  -- Creates `return (x, y)`
  let returnExpr ← `(doElem| return ($x, $y))
  doBlockExprs := doBlockExprs.push returnExpr

  -- Creates the offending do-block
  -- This causes the exception `parenthesize: uncaught backtrack exception`
  let doBlock ← liftTermElabM $ mkDoBlock doBlockExprs
  logInfo m!"{doBlock}"

#test_doblock
/-
do
  let x ← dummyMonadicFunc✝ 1
  let y ← dummyMonadicFunc✝ 2
  return (x, y)
-/

[Ernest Ng]

Thanks a lot! This was very helpful & informative!

I was looking at the section in the language reference on the grammar for do-expressions and mistakenly thought that doElem only described let mut expressions (since the page only mentions doElem in the context of local mutability). However, looking at the source code for the Lean parser, it seems like doElem is the most primitive construct and should be preferred during metaprogramming (since the parser for doElems is a built-in).