parenthesize: uncaught backtrack exception

Stream: lean4

[Alexander Bentkamp]

I am trying to implement white-space sensitive syntax, but can't get the delaboration to work. Here's an MWE for the error I am getting:

import Lean

open Lean
open Lean.Parser
open Lean.PrettyPrinter.Delaborator
open SubExpr

@[termParser]
def listParser := leading_parser "List!" >>
  manyIndent (ppLine >> checkColGe >> (ident >> ":" >> termParser))

@[delab app]
partial def delabMinimization : Delab := do
  if (← getExpr).getAppFn.isConstOf ``List.cons then
    return ← `(List!
                a : 0
                b : 1
                c : 2)
  else
    failure

#check
  [("a",0), ("b",1), ("c",2)]
-- [error when printing message: parenthesize: uncaught backtrack exception]

My actual application uses a custom datatype instead of List and I have an actual implementation of the delaborator instead of this dummy.

[Alexander Bentkamp]

The function throwing the error contains some debug output: trace[PrettyPrinter.parenthesize.input] "{format stx}", but I can't enable it. The option trace.PrettyPrinter.parenthesize.input does not seem to exist.

[Henrik Böving]

You can just set trace.PrettyPrinter.parenthesize, it will include the lower levels

[Alexander Bentkamp]

I see, actually I don't get any debug output from within the delaborator.

[Sebastian Ullrich]

Most combinators like manyIndent expect the nested parser to produce exactly one syntax tree

def listParser := leading_parser "List!" >>
  manyIndent (group (ppLine >> checkColGe >> (ident >> ":" >> termParser)))

[Sebastian Ullrich]

Alexander Bentkamp said:

I see, actually I don't get any debug output from within the delaborator.

Yes, because of dependency cycles, traces from the pretty printer are currently lost unless you invoke it directly

set_option trace.PrettyPrinter.parenthesize true
#eval show Elab.TermElabM _ from do
  let stx ← `([("a",0), ("b",1), ("c",2)])
  let e ← Elab.Term.elabTerm stx none
  PrettyPrinter.ppExpr e

But the output is not terribly helpful in this case