Application: Tracking Undefined Identifiers with RBTree🔗

The following example implements a simple "linter" that finds all undefined identifiers in a piece of syntax. Because RBTree is persistent, we can simply pass the set down to nested expressions. When we "insert" a new variable into the set for a let body, the original set remains unchanged for other branches of the syntax tree.

/-- A simple linter that finds undefined variables 
    in a piece of syntax. -/
partial def findUndefined (stx : Syntax) 
    (defined : NameSet := {}) : List Name :=
  match stx with
  | `($id:ident) => 
    let n := id.getId.eraseMacroScopes
    if defined.contains n then [] else [n]
  | `(let $id:ident := $v; $body) =>
    let errs1 := findUndefined v defined
    -- Shadowing is handled automatically by the tree.
    let errs2 := findUndefined body 
      (defined.insert id.getId.eraseMacroScopes)
    errs1 ++ errs2
  | `($e1 + $e2) => 
    findUndefined e1 defined ++ findUndefined e2 defined
  | _ => 
    -- Recursively check all other syntax components
    stx.getArgs.toList.flatMap (findUndefined · defined)

def runLinterExample : CoreM Unit := do
  let expr ← `(let y := 2; let z := x + 3; z * y)
  let undef := findUndefined expr
  IO.println s!"Undefined: {undef}"

Undefined: [x]
#eval show CoreM Unit from runLinterExample