Main.lean

/-
  Main.lean

  CLI entry point for PythonOfLean.
  Parses Python files using Racket and executes them with the Lean interpreter.
-/

import PythonOfLean
import PythonOfLean.Parser.Racket
import PythonOfLean.Semantics.Interp
import PythonOfLean.Examples.Utils

open PythonOfLean

/-- Print usage information -/
def printUsage : IO Unit := do
  IO.println "PythonOfLean: λπ semantics in Lean 4"
  IO.println ""
  IO.println "Usage:"
  IO.println "  python-of-lean --run <file.py>         Parse and execute a Python file"
  IO.println "  python-of-lean --parse <file.py>       Parse Python and print the Expr"
  IO.println "  python-of-lean --parse-sexp <file>     Parse an S-expression file"
  IO.println "  python-of-lean --eval <python-code>    Parse and execute Python code string"
  IO.println "  python-of-lean --help                  Show this help message"

/-- Parse and run a Python file -/
def runPythonFile (path : String) : IO Unit := do
  IO.println s!"Parsing {path}..."
  let result ← parsePythonFileDefault path
  match result with
  | .error msg => IO.println s!"Error: {msg}"
  | .ok expr => do
    IO.println "Running..."
    let result := run expr
    IO.println (Examples.showResult result)

/-- Parse a Python file and print the Expr -/
def parsePythonFileAndPrint (path : String) : IO Unit := do
  let result ← parsePythonFileDefault path
  match result with
  | .error msg => IO.println s!"Error: {msg}"
  | .ok expr => IO.println (repr expr)

/-- Parse a Python code string and run it -/
def evalPythonString (code : String) : IO Unit := do
  let result ← parsePython code
  match result with
  | .error msg => IO.println s!"Error: {msg}"
  | .ok expr => do
    let result := run expr
    IO.println (Examples.showResult result)

/-- Parse an S-expression file and convert to Expr -/
def parseSexpFile (path : String) : IO Unit := do
  let contents ← IO.FS.readFile path
  match parseAndConvert contents with
  | .error msg => IO.println s!"Error: {msg}"
  | .ok expr => IO.println (repr expr)

/-- Main entry point -/
def main (args : List String) : IO Unit := do
  match args with
  | ["--help"] | ["-h"] => printUsage
  | ["--run", path] => runPythonFile path
  | ["--parse", path] => parsePythonFileAndPrint path
  | ["--parse-sexp", path] => parseSexpFile path
  | ["--eval", code] => evalPythonString code
  | [] => printUsage
  | _ => do
    IO.println "Unknown command"
    printUsage