Main.lean

import Lean.Data.AssocList
import Lean.Data.Json
import Std.Data.HashSet

import LambdaLifting
import Examples.Literature

/-!
# Main executable

Runs lambda lifting algorithms on examples from the literature and on generated
examples, and checks the results satisfy the specifications.
-/

open Lean (AssocList)
open LambdaLifting.LeanUtil (assert')
open scoped LambdaLifting.LeanUtil -- for `↑` (CoeExplicit)
open LambdaLifting.Core
open LambdaLifting.Util
open LambdaLifting.Generate
open LambdaLifting.FischbachHannan
open LambdaLifting.Johnsson
open LambdaLifting.CompleteLifting


/-! ## Checks for `enumExpr'` -/

/--
Basic correctness checks for `Generate.enumExpr'`.

* The expression should be well-typed.
* Elements should have the correct size.
* The elements should be unique.
* The enumeration should be exhaustive (tested using `randExpr'`).
-/
def checkEnumExpr : IO Unit := do
  let _ : Hashable Exprₜ := ⟨hash ∘ reprStr⟩ -- Hack to avoid a global `deriving instance Hashable for Ty, Exprₜ`
  let seed := 0
  let gen := mkStdGen (s := seed)
  let baseTypes : List Ty := [.base "Int" /-, .base "Bool"-/]
  let _ : NeZero baseTypes.length := ⟨by decide⟩
  let sig : Sig := {("0", Ty.base "Int"), ("succ", Ty.arrow (.base "Int") (.base "Int"))}
  let τ : Ty := .base "Int" -- The type of the expressions we generate.
  IO.eprintln "\nGenerating random expressions to check exhaustiveness of enumExpr'..."
  let mut (rand, ⟨gen⟩) ← StateT.run (s := ⟨gen⟩) do
    let mut rand : Array (Std.HashSet Exprₜ) := .replicate (4+1) ∅
    for s in [0:rand.size] do
      for i in [0:100000] do
        let r ← randExpr' baseTypes sig {} s τ
        let s' := exprSize sig {} r -- `randExpr'` does not guarantee an exact size.
        if s' < rand.size then
          let r' ← .ofExcept $ Exprₜ_canon r
          rand := rand.modify s' (·.insert r')
    pure rand
  IO.eprintln "\nChecking enumExpr'..."
  for s in [0:4+1] do
    let mut h : Std.HashSet Exprₜ := ∅
    for e in enumExpr' baseTypes sig {} s τ do
      -- Check that `e` is well-typed.
      _ ← .ofExcept $ (e.checkType sig {} τ).mapError (s!"enumExpr' error: expression is not well-typed: {·}\n{ppStr e}")
      -- Check the size.
      let s' := exprSize sig {} e
      if s' != s then
        throw (.userError s!"enumExpr' error: requested size was {s} but size of generated expression was {s'}:\n{ppStr e}")
      -- Check uniqueness.
      let e' ← .ofExcept $ Exprₜ_canon e
      if h.contains e' then
        throw (.userError s!"enumExpr' error: duplicate expression with size {s}:\n{ppStr e}")
      h := h.insert e'
      rand := rand.modify s (·.erase e')
    IO.eprintln s!"size={s} ok"
  for hs : s in [0:rand.size] do
    if !rand[s].isEmpty then
      throw (.userError s!"enumExpr' error: the following expressions of size {s} were missed:\n{"\n".intercalate (rand[s].toList.map ppStr)}")


/-! ## Checks for lifting algorithms -/

/-- Checks that the output of an algorithm satisfies the specifications. -/
def check (S : Sig) (e : Expr)
    (τ : Ty) (h_TJ : TypeJudgement S {} e τ)
    (h_no_shadow : Expr.NoShadow [] e)
    (eₐ : Exprₐ) (globals := false) :
    Except String Unit := do
  have h_closed := Expr.Closed.of_TypeJudgement h_TJ
  -- Check that the algorithm's output is valid.
  let ⟨heq⟩ ← assert' (↑eₐ = e) s!"the output does not match the input expression"
  let ⟨h_closed_ep⟩ ← Exprₐ.checkStrictClosedEP [] eₐ
  -- Prove that the output satisfies `JohnssonLiftJudgement`.
  have : ∃ e', JohnssonLiftJudgement {} eₐ e' := JohnssonLiftJudgement_exists eₐ (heq ▸ h_closed) (heq ▸ h_no_shadow) h_closed_ep
  -- Insert the extraneous parameters (and again prove the output satisfies `JohnssonLiftJudgement`).
  let ⟨e', h_JLJ⟩ := performJohnssonTranslation eₐ (heq ▸ h_closed) (heq ▸ h_no_shadow) h_closed_ep
  -- Prove that the result satisfies `FischbachHannan.LiftJudgement`.
  have : LiftJudgement S {} e ↑τ e' := heq ▸ h_JLJ.to_LiftJudgement (heq ▸ h_TJ)
  -- We could also dynamically check that `e'` satisfies `FischbachHannan.LiftJudgement` using our decision procedure:
  --let ⟨τ', (_h_LJ : LiftJudgement S {} e τ' e')⟩ ← computeLiftJudgement e τ h_TJ {} e'
  --assert (τ' = ↑τ) s!"computeLiftJudgement produced an unexpected type: {ppStr τ'} ≠ {ppStr τ}"
  -- Check that the result satisfies `CompleteLifting`.
  if globals then
    let ⟨(_ : CompleteProgramLifting e')⟩ ← (checkCompleteProgramLifting e').mapError (s!"not a complete program lifting: {·}")
  else
    let ⟨(_ : CompleteLifting {} e')⟩ ← (checkCompleteLifting {} e').mapError (s!"not a complete lifting: {·}")

/-- Counts the number of extraneous parameters. -/
def countEP (e : Exprₐ) : Nat :=
  match e with
  | .const _c => 0
  | .var _x => 0
  | .abs θ _x b => θ.length + countEP b
  | .app e₁ e₂ => countEP e₁ + countEP e₂
  | .letrec bindings b =>
    let rec go
      | [] => 0
      | (_fᵢ, eᵢ) :: bindings' => countEP eᵢ + go bindings'
    go bindings + countEP b

/-- Checks that two `Exprₐ` have the same extraneous parameters (up to reordering). -/
def checkSameEP (eₗ eᵣ : Exprₐ) : Except String Unit :=
  -- We assume eₗ and eᵣ are equal apart from the extraneous parameters.
  -- If they are not, we may or may not report an error.
  match eₗ, eᵣ with
  | .const _, .const _ => .ok ()
  | .var _, .var _ => .ok ()
  | .abs θₗ x bₗ, .abs θᵣ _ bᵣ => do
    if θₗ.mergeSort != θᵣ.mergeSort then
      .error s!"extraneous parameters of `.abs {reprStr x}` are different: {reprStr θₗ} ≁ {reprStr θᵣ}"
    checkSameEP bₗ bᵣ
  | .app l₁ l₂, .app r₁ r₂ => do
    checkSameEP l₁ r₁
    checkSameEP l₂ r₂
  | .letrec bindingsₗ bₗ, .letrec bindingsᵣ bᵣ => do
    let rec go
      | [], [] => .ok ()
      | (fᵢ, eₗᵢ) :: bindingsₗ', (_, eᵣᵢ) :: bindingsᵣ' => do
        match eₗᵢ, eᵣᵢ with
        | .abs θₗ x bₗ, .abs θᵣ _ bᵣ =>
          -- Copied from the `.abs` case to give a better error message.
          if θₗ.mergeSort != θᵣ.mergeSort then
            .error s!"extraneous parameters of {reprStr fᵢ} are different: {reprStr θₗ} ≁ {reprStr θᵣ}"
          checkSameEP bₗ bᵣ
        | eₗᵢ, eᵣᵢ =>
          checkSameEP eₗᵢ eᵣᵢ
        go bindingsₗ' bindingsᵣ'
      | _, _ => .error s!"expressions have different structure"
    go bindingsₗ bindingsᵣ
    checkSameEP bₗ bᵣ
  | _, _ =>
    .error s!"expressions have different structure"
termination_by structural eₗ


/-!
## Support for external (subprocess-based) implementations

An external implementation is a program (written in any programming language)
that reads lines from standard input, each containing a representation of an
`Expr`, and outputs a representation of an annotated expression `Exprₐ`
containing extraneous parameters.

Different representations can be used for different programs; any
representation can be used as long as conversion can be implemented in Lean.

* The standard representation (used by `mkExprSubprocess`) is direct JSON-based
  encoding of the Lean types. For convenience, `.var` nodes are represented as
  either "var" or "fun" depending on whether they refer to variables or
  functions. See `Expr_toJson`, `Expr_toJsonDis`, and `Exprₐ_fromJson`.

* `mkFischbachAlg` uses a the same representation but eliminates variable
  bindings and anonymous functions, for algorithms that don't support them.

* `mkJohnssonSubprocess` uses a representation tailored to the Haskell
  translation of Johnsson's algorithm. It performs several preprocessing and
  postprocessing transformations.

Note: The external program must flush standard output after each line, because
the Lean code waits for a response before sending the next expression.
-/

-- We write our own JSON converters, because the format used by Lean's default
-- converter (`deriving instance Lean.ToJson, Lean.FromJson for ...`) is
-- "pretty" but awkward to parse (see `Lean.Json.parseTagged`).

-- Convert an `Expr` to JSON. Some examples to illustrate the format:
--
--     ["const","0"]
--     ["letrec",[["x",["const","0"]]],["var","x"]]
--     ["letrec",[["f",["abs","x",["var","x"]]]],["app",["var","f"],["const","0"]]]
def Expr_toJson : Expr → Lean.Json
  | .const c => .arr #["const", c]
  | .var x => .arr #["var", x]
  | .abs x b => .arr #["abs", x, Expr_toJson b]
  | .app e₁ e₂ => .arr #["app", Expr_toJson e₁, Expr_toJson e₂]
  | .letrec bindings b =>
    let rec go : _ → List Lean.Json
      | [] => []
      | (fᵢ, eᵢ) :: bindings' =>
        .arr #[fᵢ, Expr_toJson eᵢ] :: go bindings'
    .arr #["letrec", .arr (go bindings).toArray, Expr_toJson b]

-- Like `Expr_toJson`, but the returned JSON representation has separate node
-- types for variable references and function references. This is useful
-- because some algorithms require this distinction. We implement this in Lean
-- rather than in the external programs so that the identifier resolution logic
-- will only need to be implemented once. Example:
--
--     ["letrec",[["f",["abs","x",["var","x"]]]],["app",["fun","f"],["const","0"]]]
def Expr_toJsonDis (e : Expr) : Lean.Json :=
  -- We abuse `Ident.idx` to track whether an identifier is a variable or a function.
  let (json, s) := StateT.run (go e) IdentStack.empty
  checkEmpty s json
where
  idxVar := 0
  idxFun := 1
  idxTags := ["var", "fun"]
  go (e : Expr) : StateM IdentStack Lean.Json := do
    match e with
    | .const c => pure (.arr #["const", c])
    | .var x =>
      match (← .get).find? x with
      | .some ⟨_, idx⟩ => pure (.arr #[idxTags[idx]!, x])
      | .none => panic s!"invalid expression: {reprStr x} is not in scope"
    | .abs x b =>
      .modifyGet ((), ·.push ⟨x, idxVar⟩)
      let b' ← go b
      .modifyGet ((), ·.pop ⟨x, idxVar⟩)
      pure (.arr #["abs", x, b'])
    | .app e₁ e₂ =>
      let e₁' ← go e₁
      let e₂' ← go e₂
      pure (.arr #["app", e₁', e₂'])
    | .letrec bindings b =>
      for (fᵢ, eᵢ) in bindings do -- Push all the identifier bindings.
        .modifyGet ((), ·.push ⟨fᵢ, if eᵢ.isAbs then idxFun else idxVar⟩)
      let rec go' bindings : StateM IdentStack (List Lean.Json) := do
        match bindings with
        | [] => pure []
        | (fᵢ, eᵢ) :: bindings =>
          let eᵢ' ← go eᵢ
          let bindings' ← go' bindings
          pure (.arr #[fᵢ, eᵢ'] :: bindings')
      let bindings' ← go' bindings
      let b' ← go b
      for (fᵢ, eᵢ) in bindings.reverse do -- We must remove the bindings in reverse order in case of duplicates.
        .modifyGet ((), ·.pop ⟨fᵢ, if eᵢ.isAbs then idxFun else idxVar⟩)
      pure (.arr #["letrec", .arr bindings'.toArray, b'])
  checkEmpty s json : Lean.Json := -- Panics if there are any identifiers in scope (because we didn't pop them correctly).
    if s.trie.values.all (·.isEmpty) then json
    else panic! s!"internal error: the stack was expected to be empty, but contained identifier bindings: {reprStr (s.trie.values.toList.filter (!·.isEmpty))}"

-- The representation is the same as `Expr_toJson`, except that "abs" nodes are
-- of the form `["abs", θ, x, e]` where θ is a list of extraneous parameters.
open Lean (fromJson?) in
def Exprₐ_fromJson? (json : Lean.Json) : Except String Exprₐ := do
  let .arr ⟨a⟩ := json | throw "array expected"
  let tag :: args := a | throw "tag missing"
  match ← fromJson? tag with
  | "const" =>
    let [c] := args | throw "wrong number of arguments"
    .ok (.const (← fromJson? c))
  | "var" =>
    let [x] := args | throw "wrong number of arguments"
    .ok (.var (← fromJson? x))
  | "fun" => -- Allowed for compatibility; translated to "var" without any verification.
    let [x] := args | throw "wrong number of arguments"
    .ok (.var (← fromJson? x))
  | "abs" =>
    let [θ, x, b] := args | throw "wrong number of arguments"
    .ok (.abs (← fromJson? θ) (← fromJson? x) (← Exprₐ_fromJson? b))
  | "app" =>
    let [e₁, e₂] := args | throw "wrong number of arguments"
    .ok (.app (← Exprₐ_fromJson? e₁) (← Exprₐ_fromJson? e₂))
  | "letrec" =>
    let [bindings, b] := args | throw "wrong number of arguments"
    let .arr ⟨bindings⟩ := bindings | throw "array expected"
    let rec go : List Lean.Json → Except String _
      | [] => .ok []
      | binding :: bindings' => do
        let .arr ⟨[fᵢ, eᵢ]⟩ := binding | throw "pair expected"
        .ok ((← fromJson? fᵢ, ← Exprₐ_fromJson? eᵢ) :: (← go bindings'))
    .ok (.letrec (← go bindings) (← Exprₐ_fromJson? b))
  | tag => throw s!"invalid tag: {reprStr tag}"

-- Line-based interactive process.
def mkSubprocess (cmd : String) (args : Array String := #[]) :
    IO (String → IO (Except String String)) := do
  let reprCmd := fun () => reprStr (" ".intercalate (cmd :: args.toList))
  let child ← IO.Process.spawn {
    cmd := cmd, args := args,
    stdin := .piped, stdout := .piped, stderr := .inherit,
  }
  pure fun (query : String) => do
    let response ← try
      child.stdin.putStrLn query
      child.stdin.flush
      --IO.eprintln s!"Waiting for reply from subprocess {reprCmd ()}"
      child.stdout.getLine
    catch err =>
      throw (.userError s!"error communicating with subprocess {reprCmd ()}: {err.toString}")
    if response == "" then -- EOF (almost always because the subprocess crashed).
      return .error s!"subprocess {reprCmd ()} died" -- We return the error using `Except` so the caller will give a better error message.
    pure (.ok response)

-- JSON-based interactive process.
def mkJsonSubprocess {α β} [Lean.ToJson α] [Lean.FromJson β] (cmd : String) (args : Array String := #[]) :
    IO (α → IO (Except String β)) := do
  let reprCmd := fun () => reprStr (" ".intercalate (cmd :: args.toList))
  let subproc ← mkSubprocess cmd args
  pure fun (a : α) => do
    let response? ← subproc (Lean.Json.compress (Lean.toJson a))
    -- In the following code, we return errors using `Except` rather than
    -- `IO.Error` so the caller will give a better error message.
    pure do -- Now we are in the `Except` monad (no `IO`).
      let response ← response?
      let json ← (Lean.Json.parse response).mapError (s!"subprocess {reprCmd ()} produced invalid JSON ({·}), received line:\n{response}")
      (Lean.fromJson? json).mapError (s!"subprocess {reprCmd ()} produced invalid JSON ({·}), received line:\n{response}")

-- `Expr`-based interactive process.
def mkExprSubprocess (cmd : String) (args : Array String := #[]) :
    IO (Expr → IO (Except String Exprₐ)) := do
  let _ : Lean.ToJson Expr := ⟨Expr_toJsonDis⟩
  let _ : Lean.FromJson Exprₐ := ⟨Exprₐ_fromJson?⟩
  mkJsonSubprocess cmd args

open Lean (fromJson?) in
/--
Support for running Johnsson's algorithm externally.

This uses the traslation functions from `LambdaLifting/Johnsson/Algorithm.lean`
but runs the algorithm itself as a subprocess instead of using the Lean
translation.
-/
def mkJohnssonSubprocess (cmd : String) (args : Array String := #[]) :
    IO (Expr → IO (Except String Exprₐ)) := do
  let reprCmd := fun () => reprStr (" ".intercalate (cmd :: args.toList))
  let subproc ← mkSubprocess cmd args
  pure fun (e : Expr) => ExceptT.run do
    -- Based on `LambdaLifting.Johnsson.lambdaLiftExpr`.
    -- Eliminate non-identifier function operands and anonymous functions.
    let e' := elimAnonFuncs' (elimNonIdentFuncOperands e)
    -- Make the identifiers unique (including the identifiers inserted in the previous step).
    let (_n, e') ← Exprᵣ.of e'
    let e' := e'.toExprUniq
    -- Convert to Haskell.
    let hask := String.join (toHaskell (← Expr_.of e')).toList
    -- Run Johnsson's algorithm.
    let response ← ExceptT.mk (subproc hask)
    -- Parse JSON.
    let json ← (Lean.Json.parse response).mapError (s!"subprocess {reprCmd ()} produced invalid JSON ({·}), received line:\n{response}")
    -- Convert from JSON.
    let r ← (JExpr_fromJson? json).mapError (s!"subprocess {reprCmd ()} produced invalid JSON ({·}), received line:\n{response}")
    let r := r.toExpr
    -- Undo the block-floating step.
    let r' := undoBlockFloating e' r
    -- Reverse all the transformations.
    pure (undoElimFuncsₐ (undoUniqₐ r'))

where

  toHaskell : Expr_ → GList String
    -- We must not use `reprStr` because it wraps long lines.
    | .LETREC defs b =>
      let rec go_defs : List Def_ → List (GList String)
        | [] => []
        | .VAR x e :: defs =>
          (.ofList ["VAR (", reprStr1 x, ", "] ++ toHaskell e ++ .ofList [")"]) :: go_defs defs
        | .FUN f params e :: defs =>
          (.ofList ["FUN (", reprStr1 f, ", ", reprStr1 params, ", "] ++ toHaskell e ++ .ofList [")"]) :: go_defs defs
      let defs' := .flatMap' ((go_defs defs).intersperse (.ofList [", "])) id
      .ofList ["LETREC (["] ++ defs' ++ .ofList ["], "] ++ toHaskell b ++ .ofList [")"]
    | .APPL f args =>
      let rec go_args
        | [] => []
        | arg :: args => toHaskell arg :: go_args args
      let args' := .flatMap' ((go_args args).intersperse (.ofList [", "])) id
      .ofList ["APPL (", reprStr1 f, ", ["] ++ args' ++ .ofList ["])"]

  JExpr_fromJson? (json : Lean.Json) : Except String Expr_ := do
    let .arr ⟨a⟩ := json | throw "array expected"
    let tag :: args := a | throw "tag missing"
    match ← fromJson? tag with
    | "LETREC" =>
      let [defs, b] := args | throw "wrong number of arguments"
      let .arr ⟨defs⟩ := defs | throw "array expected"
      let rec go_defs : List Lean.Json → Except String _
        | [] => .ok []
        | d :: defs => do
          let .arr ⟨a⟩ := d | throw "array expected"
          let tag :: args := a | throw "tag missing"
          let d' ← match ← fromJson? tag with
            | "VAR" =>
              let [x, e] := args | throw "wrong number of arguments"
              .ok (Def_.VAR (← fromJson? x) (← JExpr_fromJson? e))
            | "FUN" =>
              let [f, params, e] := args | throw "wrong number of arguments"
              .ok (Def_.FUN (← fromJson? f) (← fromJson? params) (← JExpr_fromJson? e))
            | tag => throw s!"invalid tag: {reprStr tag}"
          .ok (d' :: (← go_defs defs))
      .ok (.LETREC (← go_defs defs) (← JExpr_fromJson? b))
    | "APPL" =>
      let [f, args] := args | throw "wrong number of arguments"
      let .arr ⟨args⟩ := args | throw "array expected"
      let rec go_args : List Lean.Json → Except String (List Expr_)
        | [] => .ok []
        | arg :: args => do .ok ((← JExpr_fromJson? arg) :: (← go_args args))
      .ok (.APPL (← fromJson? f) (← go_args args))
    | tag => throw s!"invalid tag: {reprStr tag}"

/--
Support for running the Fischbach–Hannan algorithm externally.

The Fischbach–Hannan algorithm doesn't support variable bindings and doesn't
eliminate free variables from anonymous functions.
-/
def mkFischbachAlg (alg : Expr → IO (Except String Exprₐ)) : Expr → IO (Except String Exprₐ) :=
  fun e => do
    let e' := elimAnonFuncs (elimVarBindings e)
    let eₐ ← alg e'
    pure (undoElimVarBindingsₐ <$> undoElimAnonFuncsₐ <$> eₐ)

def mkDanvyAlg := mkFischbachAlg -- It so happens that they require the same transformation.


/-! ## `main` -/

def main : IO Unit := do

  -- For each algorithm, we check that:
  --  * The output satisfies `JohnssonLiftJudgement` (and hence also
  --    `FischbachHannan.LiftJudgement`).
  --  * The output satisfies `CompleteLifting`.
  --  * The number of extraneous parameters is the same as the other
  --    algorithms, as a proxy for checking minimality.
  --  * The extraneous parameters are the same as the other algorithms (up to
  --    reordering).
  --
  -- These checks are very strict -- they check that the algorithm computes the
  -- minimal* complete Johnsson-style lifting. (*We don't check minimality
  -- directly -- we only check that the algorithms agree with each other.)
  --
  -- For lifting algorithms that are *not* intended to compute the minimal
  -- complete Johnsson-style lifting, these checks are *too* strict. To check
  -- such algorithms, the unwanted checks should be commented out manually.
  -- (Also see the commented-out code in the function `check` that uses
  -- `FischbachHannan.computeLiftJudgement`; that allows checking a somewhat
  -- more general class of liftings than Johnsson-style lifting.)

  -- As a special case, we support checking algorithms that are minimal except
  -- in the presence of dead code. The following variable can be set to `true`
  -- to enable dead code elimination, ensuring that examples tested don't
  -- contain dead code. This flag applies to *all* the algorithms (having a
  -- per-algorithm flag would make it difficult to compare the results to the
  -- other algorithms).
  let enableDeadCodeElim := false

  -- Flag to enable progress indication.
  let enableProgress := true
  -- Flag to include the current test case in progress indication (verbose).
  let enableProgressTestCases := false

  -- We allow the algorithms to use `IO` to support external (subprocess-based) implementations.
  let algs : AssocList String (Expr → IO (Except String Exprₐ)) := {
    ("simple", pure ∘ LambdaLifting.Algorithm.lambdaLift')
    ,("johnsson-fixed", pure ∘ LambdaLifting.Johnsson.lambdaLiftExpr (useOrigAlg := false))
    --,("johnsson-orig", pure ∘ LambdaLifting.Johnsson.lambdaLiftExpr (useOrigAlg := true)) -- Not minimal in the presence of dead code.
    -- External (non-Lean) implementations
    --,("johnsson-haskell-fixed", ← mkJohnssonSubprocess "foreign/johnsson_fixed" #[])
    --,("johnsson-haskell-orig", ← mkJohnssonSubprocess "foreign/johnsson" #[]) -- Not minimal in the presence of dead code.
    --,("fischbach-fixed", mkFischbachAlg (← mkExprSubprocess "python3" #["foreign/fischbach.py"]))
    --,("fischbach-orig", mkFischbachAlg (← mkExprSubprocess "python3" #["foreign/fischbach.py", "--original"])) -- Not minimal in the presence of dead code.
    --,("danvy", mkDanvyAlg (← mkExprSubprocess "python3" #["foreign/danvy.py"])) -- Fixed to produce a complete lifting, but not minimal in the presence of dead code.
  }

  --checkEnumExpr -- There is no need to run this every time, only after changing `enumExpr'`.

  IO.eprintln s!"\nChecking algorithms {algs.keys}{if enableDeadCodeElim then " with dead code elimination enabled" else ""}"

  -- Examples from literature.
  IO.eprintln s!"\nRunning on examples from literature..."
  for (id, eₜ) in Examples.literatureExamples do
    let eₜ := if enableDeadCodeElim then elimDeadCode eₜ else eₜ
    -- Check that the input is valid.
    let ⟨e, τ, h_TJ⟩ ← .ofExcept $ (eₜ.computeType Examples.S {}).mapError (s!"example '{id}' is invalid: {·}")
    let ⟨h_no_shadow⟩ ← .ofExcept $ (Expr.checkNoShadow [] e).mapError (s!"example '{id}' is invalid: {·}")
    let .some expectedEPCount := Examples.expectedEPCounts[id]? | throw (.userError s!"missing expected EP count for '{id}'")
    let mut expected? := none -- We treat the output of the first algorithm in `algs` as the expected output.
    for (algName, alg) in algs do
      -- Run the algorithm.
      let eₐ ← .ofExcept $ (← alg e).mapError (s!"algorithm '{algName}' failed on example '{id}': {·}")
      -- Check that the output satisfies the specifications.
      .ofExcept $ (check Examples.S e τ h_TJ h_no_shadow eₐ).mapError (s!"algorithm '{algName}' failed on example '{id}': {·}\n{ppStr e}\n=>\n{ppStr eₐ}")
      -- Check that the number of extraneous parameters is correct.
      if !enableDeadCodeElim && countEP eₐ != expectedEPCount then -- We can't check when dead code elimination is enabled.
        throw (.userError s!"algorithm '{algName}' failed on example '{id}': expected {expectedEPCount} extraneous parameter(s), but algorithm inserted {countEP eₐ}\n{ppStr e}\n=>\n{ppStr eₐ}")
      match expected? with
      | .none => expected? := .some eₐ
      | .some eₓ =>
        -- Compare to the expected output.
        .ofExcept $ (checkSameEP eₐ eₓ).mapError (s!"algorithm '{algName}' failed on example '{id}': extraneous parameters do not match reference output: {·}\n{ppStr e}\n=>\n{ppStr eₐ}")
  IO.eprintln s!"All {Examples.literatureExamples.length} examples from literature passed"

  let run (sig : Sig) (eₜ : Exprₜ) (name : Unit → String) : IO Unit := do
    -- Check that the input is valid.
    let ⟨e, τ, h_TJ⟩ ← .ofExcept $ (eₜ.computeType sig {}).mapError (s!"{name ()} is invalid: {·}\n{ppStr eₜ}")
    let ⟨h_no_shadow⟩ ← .ofExcept $ (Expr.checkNoShadow [] e).mapError (s!"{name ()} is invalid: {·}\n{ppStr e}")
    let mut expected? := none
    for (algName, alg) in algs do
      -- Run the algorithm.
      let eₐ ← .ofExcept $ (← alg e).mapError (s!"algorithm '{algName}' failed on {name ()}: {·}\n{ppStr e}")
      -- Check that the output satisfies the specifications.
      .ofExcept $ (check sig e τ h_TJ h_no_shadow eₐ).mapError (s!"algorithm '{algName}' failed on {name ()}: {·}\n{ppStr e}\n=>\n{ppStr eₐ}")
      match expected? with
      | .none => expected? := .some (eₐ, countEP eₐ)
      | .some (eₓ, countₓ) =>
        -- Compare to the expected output.
        if countEP eₐ != countₓ then
          throw (.userError s!"algorithm '{algName}' failed on {name ()}: expected {countₓ} extraneous parameter(s), but algorithm inserted {countEP eₐ}\n{ppStr e}\n=>\n{ppStr eₐ}")
        .ofExcept $ (checkSameEP eₐ eₓ).mapError (s!"algorithm '{algName}' failed on {name ()}: extraneous parameters do not match reference output: {·}\n{ppStr e}\n=>\n{ppStr eₐ}")

  -- Random examples.

  let seed := 0
  let gen := mkStdGen (s := seed)
  let baseTypes : List Ty := [.base "Int", .base "Bool"]
  let _ : NeZero baseTypes.length := ⟨by decide⟩
  let sig : Sig := {("0", Ty.base "Int"), ("succ", Ty.arrow (.base "Int") (.base "Int"))}

  let n := 5000
  let maxSize := 1000
  IO.eprintln s!"\nRunning on {n} randomly-generated examples..."
  let ((), ⟨gen⟩) ← StateT.run (s := ⟨gen⟩) do
    for i in [0:n] do
      let eₜ ← randExpr baseTypes sig {} (min i maxSize) (.base "Int")
      let eₜ := if enableDeadCodeElim then elimDeadCode eₜ else eₜ
      if enableProgress && i % 500 == 0 then IO.eprintln s!"{i}/{n}{if enableProgressTestCases then " " ++ ppStr eₜ.toExpr else ""}" -- We omit the type annotations to reduce verbosity.
      run sig eₜ fun () => s!"randomly-generated example #{i}"
  IO.eprintln s!"All {n} randomly-generated examples passed"

  let n := 20
  let size := 5000
  IO.eprintln s!"\nRunning on {n} extra-large randomly-generated examples..."
  let ((), ⟨gen⟩) ← StateT.run (s := ⟨gen⟩) do
    for i in [0:n] do
      let eₜ ← randExpr' baseTypes sig {} size (.base "Int")
      let eₜ := if enableDeadCodeElim then elimDeadCode eₜ else eₜ
      if enableProgress && i % 5 == 0 then IO.eprintln s!"{i}/{n}{if enableProgressTestCases then " " ++ ppStr eₜ.toExpr else ""}" -- We omit the type annotations to reduce verbosity.
      run sig eₜ fun () => s!"extra-large randomly-generated example #{i}"
  IO.eprintln s!"All {n} extra-large randomly-generated examples passed"

  -- Exhaustively-enumerated examples.

  let size := 5
  IO.eprintln s!"\nRunning on exhaustively-enumerated examples up to size {size} with two pre-defined constants..."
  let baseTypes : List Ty := [.base "Int" /-, .base "Bool"-/]
  let sig : Sig := {("0", Ty.base "Int"), ("succ", Ty.arrow (.base "Int") (.base "Int"))}
  let exprs := enumExpr baseTypes sig {} size (.base "Int")
  let mut i := 0
  for eₜ in exprs do
    let eₜ := if enableDeadCodeElim then elimDeadCode eₜ else eₜ
    if enableProgress && i % 100000 == 0 then IO.eprintln s!"{i}/?{if enableProgressTestCases then " " ++ ppStr eₜ else ""}" -- Give some sense of progress. (We print "/?" because we don't know the number of expressions in advance.)
    run sig eₜ fun () => s!"exhaustively-enumerated example #{i}"
    i := i + 1
  IO.eprintln s!"All {i} exhaustively-enumerated examples up to size {size} with two pre-defined constants passed"

  let size := 6
  IO.eprintln s!"\nRunning on exhaustively-enumerated examples up to size {size} with no pre-defined constants..."
  let baseTypes : List Ty := [.base "Int" /-, .base "Bool"-/]
  let sig : Sig := {}
  let exprs := enumExpr baseTypes sig {} size (.base "Int")
  i := 0
  for eₜ in exprs do
    let eₜ := if enableDeadCodeElim then elimDeadCode eₜ else eₜ
    if enableProgress && i % 100000 == 0 then IO.eprintln s!"{i}/? {if enableProgressTestCases then " " ++ ppStr eₜ else ""}" -- Give some sense of progress. (We print "/?" because we don't know the number of expressions in advance.)
    run sig eₜ fun () => s!"exhaustively-enumerated example #{i}"
    i := i + 1
  IO.eprintln s!"All {i} exhaustively-enumerated examples up to size {size} with no pre-defined constants passed"

  -- The size limit of the exhaustively-enumerated examples must be 6 or higher
  -- to catch the dead code issue (both with and without pre-defined
  -- constants).