module Main (main) where

import Control.Applicative ((<**>))
import Control.Monad (unless, when)
import Control.Monad.Except (ExceptT, liftEither, runExceptT)
import Control.Monad.IO.Class (liftIO)
import Data.Aeson (FromJSON, Result (..), eitherDecodeFileStrict, fromJSON)
import Data.Aeson.Extra.Merge (lodashMerge)
import Data.Foldable (for_)
import Data.IORef (newIORef)
import Data.Text (Text)
import Data.Text qualified as T
import Data.Text.IO qualified as TextIO (putStrLn)
import Data.Version (Version, makeVersion, parseVersion, showVersion)
import Lens.Micro ((%~), (<&>))
import Options.Applicative
  ( execParser
  , fullDesc
  , header
  , helper
  , info
  , progDescDoc
  )
import Options.Applicative.Help.Pretty (text)
import Paths_horus_check (version)
import Text.ParserCombinators.ReadP (readP_to_S)

import Horus.Arguments (Arguments (..), argParser, fileArgument, specFileArgument)
import Horus.ContractDefinition (ContractDefinition, cdSpecs, cd_version)
import Horus.ContractInfo (mkContractInfo)
import Horus.Global (HorusResult (..), SolvingInfo (..), cfg_version, solveContract)
import Horus.Global.Runner qualified as Global (Env (..), run)
import Horus.SW.Std (stdSpecs)
import Horus.Util (tShow)

type EIO = ExceptT Text IO

hint :: Text
hint =
  "A result of 'Unknown' indicates that Horus was not able to prove that the \n\
  \specification holds *nor* find a counterxample. For functions yielding\n\
  \'Unknown', try increasing the solver timeout by passing '-t <milliseconds>'.\n\
  \The default is 2000ms.\n\
  \\n\
  \The timeout is per-SMT-query, which means that for a compiled contract\n\
  \containing 7 functions that requires a total of 11 queries, a 5000ms timeout\n\
  \implies a maximum running time of 55 seconds. Each function will give rise to\n\
  \at least one query, and in general, queries are in 1-1 correspondence with \n\
  \branches of control flow (so a function with a single if-then-else will require\n\
  \2 queries).\n\
  \\n\
  \Example:\n\
  \  $ horus-check -s cvc5 -t 5000 a.json"

issuesMsg :: Text
issuesMsg =
  "Horus is currently in the *alpha* stage. Please be aware of the\n\
  \known issues: -checker/issues\n"

compatibleHorusCompileVersionLower :: Version
compatibleHorusCompileVersionLower = makeVersion [0, 0, 6, 8]
compatibleHorusCompileVersionHigher :: Version
compatibleHorusCompileVersionHigher = makeVersion [0, 0, 7]

  | The main entrypoint of everything that happens in our monad stack . 
  The contract is a 1 - 1 representation of the data in the compiled JSON file . 
  The contract is then used to create a ' ContractInfo ' which is a more 
  convenient representation of the contract . 
  We run ` solveContract ` , which is the entrypoint into the * rest * of the 
  program , and gather the results for pretty - printing . 

 The contract is a 1-1 representation of the data in the compiled JSON file.
 The contract is then used to create a 'ContractInfo' which is a more
 convenient representation of the contract.
 We run `solveContract`, which is the entrypoint into the *rest* of the
 program, and gather the results for pretty-printing.
-}
main' :: Arguments -> FilePath -> FilePath -> EIO ()
main' Arguments{..} filename specFileName = do
  contract <- eioDecodeFileStrict filename specFileName <&> cdSpecs %~ (<> stdSpecs)
  guardVersion contract
  contractInfo <- mkContractInfo contract
  configRef <- liftIO (newIORef arg_config)
  let env = Global.Env{e_config = configRef, e_contractInfo = contractInfo}
  infos <- liftIO (Global.run env solveContract) >>= liftEither
  for_ infos $ \si -> liftIO $ do
    TextIO.putStrLn (ppSolvingInfo si)
  let unknowns = [res | res@(Timeout{}) <- map si_result infos]
  unless (null unknowns) $ liftIO (TextIO.putStrLn hint')
 where
  hint' = "\ESC[33m" <> (T.strip . T.unlines . map ("hint: " <>) . T.lines) hint <> "\ESC[0m"
  guardVersion :: ContractDefinition -> EIO ()
  guardVersion cd = do
    compilerVersion <- case [ x
                            | x@(_, lst) <- readP_to_S parseVersion (cd_version cd)
                            , null lst
                            ] of
      [(v, [])] -> pure v
      _ -> fail $ "Wrong version format: " <> cd_version cd
    when
      ( compilerVersion < compatibleHorusCompileVersionLower
          || compilerVersion >= compatibleHorusCompileVersionHigher
      )
      . fail
      . concat
      $ [ "The *.json on input has been compiled with an incompatible version of Horus-compile.\nExpected: "
        , ">="
        , showVersion compatibleHorusCompileVersionLower
        , ", <"
        , showVersion compatibleHorusCompileVersionHigher
        , " but got: "
        , showVersion compilerVersion
        ]

eioDecodeFileStrict :: FromJSON a => FilePath -> FilePath -> EIO a
eioDecodeFileStrict contractFile specFile = do
  mbContract <- liftIO (eitherDecodeFileStrict contractFile)
  mbSpecs <- liftIO (eitherDecodeFileStrict specFile)
  case (mbContract, mbSpecs) of
    (Left err, _) -> fail ("Malformed contract *.json. Cause: " ++ err)
    (_, Left err) -> fail ("Malformed specification *.json. Cause: " ++ err)
    (Right contract, Right specifications) -> do
      let mbRes = fromJSON $ lodashMerge contract specifications
      case mbRes of
        Error err -> fail ("Malformed contract *.json. Cause: " ++ err)
        Success res -> pure res

ppSolvingInfo :: SolvingInfo -> Text
ppSolvingInfo SolvingInfo{..} =
  si_moduleName <> inlinedIndicator <> "\n" <> tShow si_result <> "\n"
 where
  inlinedIndicator = if si_inlinable then " [inlined]" else ""

{- | Main entrypoint of the program.
 Cases
 =====
 1. No arguments are passed. In this case, we print the help message.
 2. The `--version` flag is passed. In this case, we print the version number.
 3. No file is passed. In this case, we print an error.
 4. A file is passed. In this case, we run `main'`.
-}
main :: IO ()
main = do
  TextIO.putStrLn issuesMsg'
  arguments <- execParser opts
  if cfg_version (arg_config arguments)
    then
      putStrLn . concat $
        [ "Horus version: "
        , showVersion version
        , "\nHorus-compile (required): "
        , ">="
        , showVersion compatibleHorusCompileVersionLower
        , ", <"
        , showVersion compatibleHorusCompileVersionHigher
        ]
    else case (arg_fileName arguments, arg_specFile arguments) of
      (Nothing, _) -> putStrLn "Missing compiled JSON file. Use --help for more information."
      (_, Nothing) -> putStrLn "Missing specification JSON file. Use --help for more information."
      (Just filename, Just specFileName) -> do
        runExceptT (main' arguments filename specFileName) >>= either (fail . T.unpack) pure
 where
  issuesMsg' =
    "\ESC[33m" <> (T.strip . T.unlines . map ("Warning: " <>) . T.lines) issuesMsg <> "\ESC[0m\n"
  opts =
    info
      (argParser <**> helper)
      ( fullDesc
          <> progDescDoc
            ( Just $
                text "Verifies "
                  <> text (T.unpack fileArgument)
                  <> text " (a JSON contract compiled with horus-compile) with the specification file "
                  <> text (T.unpack specFileArgument)
                  <> text " provided by horus-compile \n\n"
                  <> text "Example using solver cvc5 (default):\n"
                  <> text "  $ horus-check a.json spec.json\n\n"
                  <> text "Example using solver mathsat:\n"
                  <> text "  $ horus-check -s mathsat a.json spec.json\n\n"
                  <> text "Example using solvers z3, mathsat:\n"
                  <> text "  $ horus-check -s z3 -s mathsat a.json spec.json\n"
            )
          <> header "horus-check: an SMT-based checker for StarkNet contracts"
      )

 | Main entrypoint of the program.
 Cases
 =====
 1. No arguments are passed. In this case, we print the help message.
 2. The `--version` flag is passed. In this case, we print the version number.
 3. No file is passed. In this case, we print an error.
 4. A file is passed. In this case, we run `main'`.

module Main (main) where

import Control.Applicative ((<**>))
import Control.Monad (unless, when)
import Control.Monad.Except (ExceptT, liftEither, runExceptT)
import Control.Monad.IO.Class (liftIO)
import Data.Aeson (FromJSON, Result (..), eitherDecodeFileStrict, fromJSON)
import Data.Aeson.Extra.Merge (lodashMerge)
import Data.Foldable (for_)
import Data.IORef (newIORef)
import Data.Text (Text)
import Data.Text qualified as T
import Data.Text.IO qualified as TextIO (putStrLn)
import Data.Version (Version, makeVersion, parseVersion, showVersion)
import Lens.Micro ((%~), (<&>))
import Options.Applicative
  ( execParser
  , fullDesc
  , header
  , helper
  , info
  , progDescDoc
  )
import Options.Applicative.Help.Pretty (text)
import Paths_horus_check (version)
import Text.ParserCombinators.ReadP (readP_to_S)

import Horus.Arguments (Arguments (..), argParser, fileArgument, specFileArgument)
import Horus.ContractDefinition (ContractDefinition, cdSpecs, cd_version)
import Horus.ContractInfo (mkContractInfo)
import Horus.Global (HorusResult (..), SolvingInfo (..), cfg_version, solveContract)
import Horus.Global.Runner qualified as Global (Env (..), run)
import Horus.SW.Std (stdSpecs)
import Horus.Util (tShow)

type EIO = ExceptT Text IO

hint :: Text
hint =
  "A result of 'Unknown' indicates that Horus was not able to prove that the \n\
  \specification holds *nor* find a counterxample. For functions yielding\n\
  \'Unknown', try increasing the solver timeout by passing '-t <milliseconds>'.\n\
  \The default is 2000ms.\n\
  \\n\
  \The timeout is per-SMT-query, which means that for a compiled contract\n\
  \containing 7 functions that requires a total of 11 queries, a 5000ms timeout\n\
  \implies a maximum running time of 55 seconds. Each function will give rise to\n\
  \at least one query, and in general, queries are in 1-1 correspondence with \n\
  \branches of control flow (so a function with a single if-then-else will require\n\
  \2 queries).\n\
  \\n\
  \Example:\n\
  \  $ horus-check -s cvc5 -t 5000 a.json"

issuesMsg :: Text
issuesMsg =
  "Horus is currently in the *alpha* stage. Please be aware of the\n\
  \known issues: -checker/issues\n"

compatibleHorusCompileVersionLower :: Version
compatibleHorusCompileVersionLower = makeVersion [0, 0, 6, 8]
compatibleHorusCompileVersionHigher :: Version
compatibleHorusCompileVersionHigher = makeVersion [0, 0, 7]

  | The main entrypoint of everything that happens in our monad stack . 
  The contract is a 1 - 1 representation of the data in the compiled JSON file . 
  The contract is then used to create a ' ContractInfo ' which is a more 
  convenient representation of the contract . 
  We run ` solveContract ` , which is the entrypoint into the * rest * of the 
  program , and gather the results for pretty - printing . 

 The contract is a 1-1 representation of the data in the compiled JSON file.
 The contract is then used to create a 'ContractInfo' which is a more
 convenient representation of the contract.
 We run `solveContract`, which is the entrypoint into the *rest* of the
 program, and gather the results for pretty-printing.
-}
main' :: Arguments -> FilePath -> FilePath -> EIO ()
main' Arguments{..} filename specFileName = do
  contract <- eioDecodeFileStrict filename specFileName <&> cdSpecs %~ (<> stdSpecs)
  guardVersion contract
  contractInfo <- mkContractInfo contract
  configRef <- liftIO (newIORef arg_config)
  let env = Global.Env{e_config = configRef, e_contractInfo = contractInfo}
  infos <- liftIO (Global.run env solveContract) >>= liftEither
  for_ infos $ \si -> liftIO $ do
    TextIO.putStrLn (ppSolvingInfo si)
  let unknowns = [res | res@(Timeout{}) <- map si_result infos]
  unless (null unknowns) $ liftIO (TextIO.putStrLn hint')
 where
  hint' = "\ESC[33m" <> (T.strip . T.unlines . map ("hint: " <>) . T.lines) hint <> "\ESC[0m"
  guardVersion :: ContractDefinition -> EIO ()
  guardVersion cd = do
    compilerVersion <- case [ x
                            | x@(_, lst) <- readP_to_S parseVersion (cd_version cd)
                            , null lst
                            ] of
      [(v, [])] -> pure v
      _ -> fail $ "Wrong version format: " <> cd_version cd
    when
      ( compilerVersion < compatibleHorusCompileVersionLower
          || compilerVersion >= compatibleHorusCompileVersionHigher
      )
      . fail
      . concat
      $ [ "The *.json on input has been compiled with an incompatible version of Horus-compile.\nExpected: "
        , ">="
        , showVersion compatibleHorusCompileVersionLower
        , ", <"
        , showVersion compatibleHorusCompileVersionHigher
        , " but got: "
        , showVersion compilerVersion
        ]

eioDecodeFileStrict :: FromJSON a => FilePath -> FilePath -> EIO a
eioDecodeFileStrict contractFile specFile = do
  mbContract <- liftIO (eitherDecodeFileStrict contractFile)
  mbSpecs <- liftIO (eitherDecodeFileStrict specFile)
  case (mbContract, mbSpecs) of
    (Left err, _) -> fail ("Malformed contract *.json. Cause: " ++ err)
    (_, Left err) -> fail ("Malformed specification *.json. Cause: " ++ err)
    (Right contract, Right specifications) -> do
      let mbRes = fromJSON $ lodashMerge contract specifications
      case mbRes of
        Error err -> fail ("Malformed contract *.json. Cause: " ++ err)
        Success res -> pure res

ppSolvingInfo :: SolvingInfo -> Text
ppSolvingInfo SolvingInfo{..} =
  si_moduleName <> inlinedIndicator <> "\n" <> tShow si_result <> "\n"
 where
  inlinedIndicator = if si_inlinable then " [inlined]" else ""

main :: IO ()
main = do
  TextIO.putStrLn issuesMsg'
  arguments <- execParser opts
  if cfg_version (arg_config arguments)
    then
      putStrLn . concat $
        [ "Horus version: "
        , showVersion version
        , "\nHorus-compile (required): "
        , ">="
        , showVersion compatibleHorusCompileVersionLower
        , ", <"
        , showVersion compatibleHorusCompileVersionHigher
        ]
    else case (arg_fileName arguments, arg_specFile arguments) of
      (Nothing, _) -> putStrLn "Missing compiled JSON file. Use --help for more information."
      (_, Nothing) -> putStrLn "Missing specification JSON file. Use --help for more information."
      (Just filename, Just specFileName) -> do
        runExceptT (main' arguments filename specFileName) >>= either (fail . T.unpack) pure
 where
  issuesMsg' =
    "\ESC[33m" <> (T.strip . T.unlines . map ("Warning: " <>) . T.lines) issuesMsg <> "\ESC[0m\n"
  opts =
    info
      (argParser <**> helper)
      ( fullDesc
          <> progDescDoc
            ( Just $
                text "Verifies "
                  <> text (T.unpack fileArgument)
                  <> text " (a JSON contract compiled with horus-compile) with the specification file "
                  <> text (T.unpack specFileArgument)
                  <> text " provided by horus-compile \n\n"
                  <> text "Example using solver cvc5 (default):\n"
                  <> text "  $ horus-check a.json spec.json\n\n"
                  <> text "Example using solver mathsat:\n"
                  <> text "  $ horus-check -s mathsat a.json spec.json\n\n"
                  <> text "Example using solvers z3, mathsat:\n"
                  <> text "  $ horus-check -s z3 -s mathsat a.json spec.json\n"
            )
          <> header "horus-check: an SMT-based checker for StarkNet contracts"
      )
