Main.lean

-- SPDX-FileCopyrightText: 2026 Christopher Lang
--
-- SPDX-License-Identifier: Apache-2.0 OR BSD-2-Clause

import Cli
import ArchSem.LitmusTest.Parse
import ArchSem.LitmusTest.Run
import ArchSem.LitmusTest.Basic
import ArchSem.TerminatingModel
import ArchSemTinyArm.Promising

open ArchSem.LitmusTest
open ArchSem.TerminatingModel (ComputationalTerminatingModel)

def modelFromStr (fuel : Nat) : String → Option ComputationalTerminatingModel
  | "tinyarm-promisefirst" =>
    ArchSemTinyArm.Promising.createPromiseFirstModel
      ArchSemTinyArm.sailTinyArmIsem fuel |> some
  | "tinyarm-promisenaive" =>
    ArchSemTinyArm.Promising.createNaiveModel
      ArchSemTinyArm.sailTinyArmIsem fuel |> some
  | _ => none

def runTests (p : Cli.Parsed) : IO UInt32 := do
  let configFname : System.FilePath ← match p.flag? "config" |>.bind (Cli.Parsed.Flag.as? · String) with
    | .some str => pure str
    | .none =>
      IO.eprintln "Config unspecified."
      return 1
  let config : LitmusTestConfig ← Config.readConfigFile configFname
  let testFnames : List System.FilePath := p.variableArgsAs! String |>.toList
  let fuel : Nat := match p.flag? "fuel" |>.bind (Cli.Parsed.Flag.as? · Nat) with
    | .some fuel => fuel
    | .none => config.defaultFuel
  let modelStr : String ← match p.flag? "model" |>.bind (Cli.Parsed.Flag.as? · String) with
    | .some str => pure str
    | .none =>
      IO.eprintln "Model unspecified."
      return 1
  let model ← match modelFromStr fuel modelStr with
    | .some m => pure m
    | .none => do
      IO.eprintln s!"Model does not exist: '{modelStr}'"
      return 1
  if testFnames.length == 0 then
    IO.eprintln s!"No tests specified."
    return 1
  let errors : List String ← testFnames.filterMapM (fun fname => do
    (← IO.getStdout).flush
    (← IO.getStderr).flush
    let testRepr ← Parse.readTestFile fname
    let finalStates ← match Run.runLitmusTest model testRepr with
      | .ok states => pure states
      | .error msg =>
        let msg := s!"[{testRepr.name}] Error: Failed to run test {msg}"
        IO.eprintln msg
        return .some msg
    let results ← match prepareTestResults config testRepr finalStates with
      | .ok results => pure results
      | .error msg =>
        let msg := s!"[{testRepr.name}] Error: Failed to prepare test results {msg}"
        IO.eprintln msg
        return .some msg
    let mcompare : String ← match MCompare.testOutput testRepr results with
      | .ok mcompare => pure mcompare
      | .error msg =>
        let msg := s!"[{testRepr.name}] Error: Failed to prepare mcompare {msg}"
        IO.eprintln msg
        return .some msg
    IO.print mcompare
    return Option.none
  )
  if errors == [] then
    pure 0
  else
    IO.eprintln "At least one test failed."
    pure 1


def litmusTestCmd : Cli.Cmd := `[Cli|
  archsem VIA runTests;
  "Run litmus tests from `.archsem.toml` format."

  FLAGS:
    model : String; "Name of model to use."
    config : String; "Config file to use."

  ARGS:
    ...tests : String; "Tests to run of the `.archsem.toml` format."
]

def main (args : List String) : IO UInt32 :=
  litmusTestCmd.validate args