Lean4
/-- `extractSymbols expr` takes as input an `Expr`ession `expr`, assuming that it is the `value`
of a "parser".
It returns the array of all subterms of `expr` that are the `Expr.lit` argument to
`Lean.ParserDescr.symbol` and `Lean.ParserDescr.nonReservedSymbol` applications.
The output array serves as a way of regenerating what the syntax tree of the input parser is.
-/
def extractSymbols : Expr → Array Expr
| .app a b =>
let rest := extractSymbols a ++ extractSymbols b
match a.constName with
| ``Lean.ParserDescr.symbol | ``Lean.ParserDescr.nonReservedSymbol => rest.push b
| _ => rest
| .letE _ a b c _ => extractSymbols a ++ extractSymbols b ++ extractSymbols c
| .lam _ a b _ => extractSymbols a ++ extractSymbols b
| .forallE _ a b _ => extractSymbols a ++ extractSymbols b
| .mdata _ a => extractSymbols a
| .proj _ _ a => extractSymbols a
| _ => #[]
