9.6. The Lean API🔗

A tool that embeds Laurel rather than shelling out to the CLI uses the Strata.Languages.Laurel facade. parseLaurelText and readLaurelTextFile produce a Laurel.Program; readLaurelIonFiles and readLaurelIonProgram do the same from Ion; laurelToCore lowers one; and Laurel.verifyProgram translates and verifies in one step.

import Strata.Languages.Laurel

open Strata

def lower (path : System.FilePath) : IO Unit := do
  let source ← readLaurelTextFile path
  let (core?, diagnostics) ← Laurel.translate {} source
  diagnostics.forM (fun d => IO.println d.message)
  match core? with
  | some core => IO.println (Std.format core).pretty
  | none => throw (IO.userError "Laurel translation failed")

Prefer Laurel.translate over laurelToCore in tooling: it preserves the structured diagnostics instead of flattening them to strings, which is what you need to report a problem at a source location. translateWithLaurel additionally hands back the post-pass Laurel program.