{-# LANGUAGE CPP #-}

-- Copyright (c) 2020-2026, Chris Pressey, Cat's Eye Technologies.
-- This file is distributed under a 2-clause BSD license, see LICENSES/ dir.
-- SPDX-License-Identifier: LicenseRef-BSD-2-Clause-X-Burro

module Main where

import System.Environment
import System.Exit (exitFailure)

import Language.Burro.Definition
import qualified Language.Burro.Debugger as Debugger
import qualified Language.Kondey.Compiler as KondeyCompiler
import Language.Turmac.Parser (parseRules)
import Language.Turmac.Model (TMRule, initConfiguration)
import Language.Turmac.Simulator (execute)
import Language.Turmac.Renderer (renderConfig)

#ifdef ENABLE_CLAUDE_PROOF
import Language.Burro.TCProof.TM2Kondey (compileToKondey)
import Language.Burro.TCProof.Bisimulator (BisimResult(..), runBisim)
import Language.Burro.TCProof.Configuration (decodeConfiguration)
#endif


data Flags = Flags {
    tapeChunkSize :: Int,
    tapeDisplayWidth :: Int
} deriving (Show, Ord, Eq)

defaultFlags = Flags{
    tapeChunkSize = 1,
    tapeDisplayWidth = 20
}

parseFlags flags ("--tape-chunk-size":n:rest) =
    parseFlags flags{ tapeChunkSize = read n } rest
parseFlags flags ("--tape-display-width":n:rest) =
    parseFlags flags{ tapeDisplayWidth = read n } rest
parseFlags flags other = (flags, other)


main = do
    args <- getArgs
    let (flags, args') = parseFlags defaultFlags args
    case args' of
        ["parse", fileName] -> do
            burroText <- readFile fileName
            putStrLn $ show $ parse burroText
        ["run", fileName] -> do
            burroText <- readFile fileName
            putStrLn $ show $ interpret burroText
        ["debug", fileName] -> do
            burroText <- readFile fileName
            state <- Debugger.interpret (parse burroText) (tapeChunkSize flags) (tapeDisplayWidth flags)
            putStrLn $ show $ state
        ["compile-kondey", fileName] -> do
            kondeyText <- readFile fileName
            let burroProg = KondeyCompiler.compile kondeyText
            putStrLn $ show $ burroProg
        ["run-kondey", fileName] -> do
            kondeyText <- readFile fileName
            let burroProg = KondeyCompiler.compile kondeyText
            putStrLn $ show $ run burroProg newstate
        ["debug-kondey", fileName] -> do
            kondeyText <- readFile fileName
            let burroProg = KondeyCompiler.compile kondeyText
            state <- Debugger.interpret burroProg (tapeChunkSize flags) (tapeDisplayWidth flags)
            putStrLn $ show $ state
#ifdef ENABLE_CLAUDE_PROOF
        ["compile-turmac", fileName] -> do
            turmacText <- readFile fileName
            let tmRules = parseRules turmacText
            let kondeyText = compileToKondey tmRules
            putStr $ kondeyText
        ["run-turmac", fileName] -> do
            turmacText <- readFile fileName
            let tmRules = parseRules turmacText
            let kondeyText = compileToKondey tmRules
            let burroProg = KondeyCompiler.compile kondeyText
            putStrLn $ show $ run burroProg newstate
        ["run-and-compare-turmac", fileName] -> do
            turmacText <- readFile fileName
            let tmRules = parseRules turmacText
            let tmResult = execute tmRules initConfiguration
            let tmRendered = renderConfig (-1) tmResult
            let kondeyText = compileToKondey tmRules
            let burroProg = KondeyCompiler.compile kondeyText
            let burroState = run burroProg newstate
            let burroResult = decodeConfiguration tmRules True burroState
            let burroRendered = renderConfig (-1) burroResult
            if tmRendered == burroRendered
                then do
                    putStrLn "MATCH"
                    putStrLn tmRendered
                else do
                    putStrLn "MISMATCH"
                    putStrLn "--- Turmac simulator result ---"
                    putStrLn tmRendered
                    putStrLn "--- Burro (via Turmac-to-Kondey-to-Burro) result ---"
                    putStrLn burroRendered
                    exitFailure
        ["bisim-check-turmac", fileName, nStr] -> do
            turmacText <- readFile fileName
            let tmRules = parseRules turmacText
            let kondeyText = compileToKondey tmRules
            let burroProg = KondeyCompiler.compile kondeyText
            case runBisim tmRules burroProg (read nStr) of
                BisimMatch steps halted -> do
                    putStrLn "MATCH"
                    putStrLn $ show steps ++
                        (if halted then " steps, halted" else " steps, still running")
                BisimMismatch step tmCfg burroCfg -> do
                    putStrLn $ "MISMATCH at step " ++ show step
                    putStrLn "--- Turmac simulator result ---"
                    putStrLn $ renderConfig step tmCfg
                    putStrLn "--- Burro (via Turmac-to-Kondey-to-Burro) result ---"
                    putStrLn $ renderConfig step burroCfg
                    exitFailure
        ["debug-turmac", fileName] -> do
            turmacText <- readFile fileName
            let tmRules = parseRules turmacText
            let kondeyText = compileToKondey tmRules
            let burroProg = KondeyCompiler.compile kondeyText
            state <- Debugger.interpret burroProg (tapeChunkSize flags) (tapeDisplayWidth flags)
            putStrLn $ show $ state
#endif
        _ -> do
            putStrLn $
              "Usage:\n" ++
              "  burro run <filename.burro>\n" ++
              "  burro debug <filename.burro>\n" ++
              "  burro compile-kondey <filename.kondey>\n" ++
              "  burro run-kondey <filename.kondey>\n" ++
              "  burro debug-kondey <filename.kondey>\n" ++
#ifdef ENABLE_CLAUDE_PROOF
              "  burro compile-turmac <filename.turmac>\n" ++
              "  burro run-turmac <filename.turmac>\n" ++
              "  burro run-and-compare-turmac <filename.turmac>\n" ++
              "  burro bisim-check-turmac <filename.turmac> <n>\n" ++
              "  burro debug-turmac <filename.turmac>" ++
#endif
              "\n"