-- editorconfig-checker-disable-file
{-# LANGUAGE OverloadedStrings #-}

module Opts where

import Data.Semigroup ((<>))
import Data.Text qualified as T
import Data.Text.IO qualified as T

import Data.Foldable (asum)
import Options.Applicative hiding (asum)

import PlutusCore.Executable.Common
import PlutusCore.Executable.Parsers

import System.Exit (exitFailure)
import System.IO (stderr)

import PlutusCore.Evaluation.Machine.ExBudgetingDefaults (defaultCekMachineCostsForTesting)
import PlutusCore.Evaluation.Machine.SimpleBuiltinCostModel
import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts (CekMachineCosts)


-- the different budget modes of plc-agda
data BudgetMode a = Silent
                 | Counting a
                 | Tallying a
      deriving (forall a b. (a -> b) -> BudgetMode a -> BudgetMode b)
-> (forall a b. a -> BudgetMode b -> BudgetMode a)
-> Functor BudgetMode
forall a b. a -> BudgetMode b -> BudgetMode a
forall a b. (a -> b) -> BudgetMode a -> BudgetMode b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> BudgetMode a -> BudgetMode b
fmap :: forall a b. (a -> b) -> BudgetMode a -> BudgetMode b
$c<$ :: forall a b. a -> BudgetMode b -> BudgetMode a
<$ :: forall a b. a -> BudgetMode b -> BudgetMode a
Functor

countingbudget :: Parser (BudgetMode ())
countingbudget :: Parser (BudgetMode ())
countingbudget = BudgetMode ()
-> Mod FlagFields (BudgetMode ()) -> Parser (BudgetMode ())
forall a. a -> Mod FlagFields a -> Parser a
flag' (() -> BudgetMode ()
forall a. a -> BudgetMode a
Counting ())
                 (  String -> Mod FlagFields (BudgetMode ())
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"counting"
                 Mod FlagFields (BudgetMode ())
-> Mod FlagFields (BudgetMode ()) -> Mod FlagFields (BudgetMode ())
forall a. Semigroup a => a -> a -> a
<> Char -> Mod FlagFields (BudgetMode ())
forall (f :: * -> *) a. HasName f => Char -> Mod f a
short Char
'c'
                 Mod FlagFields (BudgetMode ())
-> Mod FlagFields (BudgetMode ()) -> Mod FlagFields (BudgetMode ())
forall a. Semigroup a => a -> a -> a
<> String -> Mod FlagFields (BudgetMode ())
forall (f :: * -> *) a. String -> Mod f a
help String
"Run machine in counting mode and report results" )

tallyingbudget :: Parser (BudgetMode ())
tallyingbudget :: Parser (BudgetMode ())
tallyingbudget = BudgetMode ()
-> Mod FlagFields (BudgetMode ()) -> Parser (BudgetMode ())
forall a. a -> Mod FlagFields a -> Parser a
flag' (() -> BudgetMode ()
forall a. a -> BudgetMode a
Tallying ())
                 (  String -> Mod FlagFields (BudgetMode ())
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"tallying"
                 Mod FlagFields (BudgetMode ())
-> Mod FlagFields (BudgetMode ()) -> Mod FlagFields (BudgetMode ())
forall a. Semigroup a => a -> a -> a
<> Char -> Mod FlagFields (BudgetMode ())
forall (f :: * -> *) a. HasName f => Char -> Mod f a
short Char
't'
                 Mod FlagFields (BudgetMode ())
-> Mod FlagFields (BudgetMode ()) -> Mod FlagFields (BudgetMode ())
forall a. Semigroup a => a -> a -> a
<> String -> Mod FlagFields (BudgetMode ())
forall (f :: * -> *) a. String -> Mod f a
help String
"Run machine in tallying mode and report results" )

budgetmode :: Parser (BudgetMode ())
budgetmode :: Parser (BudgetMode ())
budgetmode = [Parser (BudgetMode ())] -> Parser (BudgetMode ())
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum
    [ Parser (BudgetMode ())
countingbudget
    , Parser (BudgetMode ())
tallyingbudget
    , BudgetMode () -> Parser (BudgetMode ())
forall a. a -> Parser a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BudgetMode ()
forall a. BudgetMode a
Silent
    ]

-- The different evaluation modes of plc-agda
data EvalMode = U | TL | TCK | TCEK deriving stock (Int -> EvalMode -> ShowS
[EvalMode] -> ShowS
EvalMode -> String
(Int -> EvalMode -> ShowS)
-> (EvalMode -> String) -> ([EvalMode] -> ShowS) -> Show EvalMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> EvalMode -> ShowS
showsPrec :: Int -> EvalMode -> ShowS
$cshow :: EvalMode -> String
show :: EvalMode -> String
$cshowList :: [EvalMode] -> ShowS
showList :: [EvalMode] -> ShowS
Show, ReadPrec [EvalMode]
ReadPrec EvalMode
Int -> ReadS EvalMode
ReadS [EvalMode]
(Int -> ReadS EvalMode)
-> ReadS [EvalMode]
-> ReadPrec EvalMode
-> ReadPrec [EvalMode]
-> Read EvalMode
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS EvalMode
readsPrec :: Int -> ReadS EvalMode
$creadList :: ReadS [EvalMode]
readList :: ReadS [EvalMode]
$creadPrec :: ReadPrec EvalMode
readPrec :: ReadPrec EvalMode
$creadListPrec :: ReadPrec [EvalMode]
readListPrec :: ReadPrec [EvalMode]
Read)

data EvalOptions a = EvalOpts Input Format EvalMode (BudgetMode a)
  deriving (forall a b. (a -> b) -> EvalOptions a -> EvalOptions b)
-> (forall a b. a -> EvalOptions b -> EvalOptions a)
-> Functor EvalOptions
forall a b. a -> EvalOptions b -> EvalOptions a
forall a b. (a -> b) -> EvalOptions a -> EvalOptions b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> EvalOptions a -> EvalOptions b
fmap :: forall a b. (a -> b) -> EvalOptions a -> EvalOptions b
$c<$ :: forall a b. a -> EvalOptions b -> EvalOptions a
<$ :: forall a b. a -> EvalOptions b -> EvalOptions a
Functor

evalMode :: Parser EvalMode
evalMode :: Parser EvalMode
evalMode = ReadM EvalMode -> Mod OptionFields EvalMode -> Parser EvalMode
forall a. ReadM a -> Mod OptionFields a -> Parser a
option ReadM EvalMode
forall a. Read a => ReadM a
auto
  (  String -> Mod OptionFields EvalMode
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"mode"
  Mod OptionFields EvalMode
-> Mod OptionFields EvalMode -> Mod OptionFields EvalMode
forall a. Semigroup a => a -> a -> a
<> Char -> Mod OptionFields EvalMode
forall (f :: * -> *) a. HasName f => Char -> Mod f a
short Char
'm'
  Mod OptionFields EvalMode
-> Mod OptionFields EvalMode -> Mod OptionFields EvalMode
forall a. Semigroup a => a -> a -> a
<> String -> Mod OptionFields EvalMode
forall (f :: * -> *) a. HasMetavar f => String -> Mod f a
metavar String
"MODE"
  Mod OptionFields EvalMode
-> Mod OptionFields EvalMode -> Mod OptionFields EvalMode
forall a. Semigroup a => a -> a -> a
<> EvalMode -> Mod OptionFields EvalMode
forall (f :: * -> *) a. HasValue f => a -> Mod f a
value EvalMode
TL
  Mod OptionFields EvalMode
-> Mod OptionFields EvalMode -> Mod OptionFields EvalMode
forall a. Semigroup a => a -> a -> a
<> Mod OptionFields EvalMode
forall a (f :: * -> *). Show a => Mod f a
showDefault
  Mod OptionFields EvalMode
-> Mod OptionFields EvalMode -> Mod OptionFields EvalMode
forall a. Semigroup a => a -> a -> a
<> String -> Mod OptionFields EvalMode
forall (f :: * -> *) a. String -> Mod f a
help String
"Evaluation mode (U , TL, TCK, TCEK)" )

evalOpts :: Parser (EvalOptions ())
evalOpts :: Parser (EvalOptions ())
evalOpts = Input -> Format -> EvalMode -> BudgetMode () -> EvalOptions ()
forall a.
Input -> Format -> EvalMode -> BudgetMode a -> EvalOptions a
EvalOpts (Input -> Format -> EvalMode -> BudgetMode () -> EvalOptions ())
-> Parser Input
-> Parser (Format -> EvalMode -> BudgetMode () -> EvalOptions ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Input
input Parser (Format -> EvalMode -> BudgetMode () -> EvalOptions ())
-> Parser Format
-> Parser (EvalMode -> BudgetMode () -> EvalOptions ())
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Format
inputformat Parser (EvalMode -> BudgetMode () -> EvalOptions ())
-> Parser EvalMode -> Parser (BudgetMode () -> EvalOptions ())
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser EvalMode
evalMode Parser (BudgetMode () -> EvalOptions ())
-> Parser (BudgetMode ()) -> Parser (EvalOptions ())
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (BudgetMode ())
budgetmode

data TypecheckOptions = TCOpts Input Format

typecheckOpts :: Parser TypecheckOptions
typecheckOpts :: Parser TypecheckOptions
typecheckOpts = Input -> Format -> TypecheckOptions
TCOpts (Input -> Format -> TypecheckOptions)
-> Parser Input -> Parser (Format -> TypecheckOptions)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Input
input Parser (Format -> TypecheckOptions)
-> Parser Format -> Parser TypecheckOptions
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Format
inputformat

data Command a = Eval (EvalOptions a)
             | Typecheck TypecheckOptions
          deriving (forall a b. (a -> b) -> Command a -> Command b)
-> (forall a b. a -> Command b -> Command a) -> Functor Command
forall a b. a -> Command b -> Command a
forall a b. (a -> b) -> Command a -> Command b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Command a -> Command b
fmap :: forall a b. (a -> b) -> Command a -> Command b
$c<$ :: forall a b. a -> Command b -> Command a
<$ :: forall a b. a -> Command b -> Command a
Functor

commands :: Parser (Command ())
commands :: Parser (Command ())
commands = Mod CommandFields (Command ()) -> Parser (Command ())
forall a. Mod CommandFields a -> Parser a
hsubparser (
         String -> ParserInfo (Command ()) -> Mod CommandFields (Command ())
forall a. String -> ParserInfo a -> Mod CommandFields a
command String
"evaluate"
          (Parser (Command ())
-> InfoMod (Command ()) -> ParserInfo (Command ())
forall a. Parser a -> InfoMod a -> ParserInfo a
info (EvalOptions () -> Command ()
forall a. EvalOptions a -> Command a
Eval (EvalOptions () -> Command ())
-> Parser (EvalOptions ()) -> Parser (Command ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (EvalOptions ())
evalOpts)
          (InfoMod (Command ())
forall a. InfoMod a
fullDesc InfoMod (Command ())
-> InfoMod (Command ()) -> InfoMod (Command ())
forall a. Semigroup a => a -> a -> a
<> String -> InfoMod (Command ())
forall a. String -> InfoMod a
progDesc String
"run a Plutus Core program"))
      Mod CommandFields (Command ())
-> Mod CommandFields (Command ()) -> Mod CommandFields (Command ())
forall a. Semigroup a => a -> a -> a
<> String -> ParserInfo (Command ()) -> Mod CommandFields (Command ())
forall a. String -> ParserInfo a -> Mod CommandFields a
command String
"typecheck"
          (Parser (Command ())
-> InfoMod (Command ()) -> ParserInfo (Command ())
forall a. Parser a -> InfoMod a -> ParserInfo a
info (TypecheckOptions -> Command ()
forall a. TypecheckOptions -> Command a
Typecheck (TypecheckOptions -> Command ())
-> Parser TypecheckOptions -> Parser (Command ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser TypecheckOptions
typecheckOpts)
          (InfoMod (Command ())
forall a. InfoMod a
fullDesc InfoMod (Command ())
-> InfoMod (Command ()) -> InfoMod (Command ())
forall a. Semigroup a => a -> a -> a
<> String -> InfoMod (Command ())
forall a. String -> InfoMod a
progDesc String
"typecheck a Plutus Core program")))

-- A CostModel has all the information to run the Agda machine
-- with cost reporting
type CostModel = (CekMachineCosts , BuiltinCostMap)

addJSONParameters :: Command a -> Command CostModel
addJSONParameters :: forall a. Command a -> Command CostModel
addJSONParameters = (a -> CostModel) -> Command a -> Command CostModel
forall a b. (a -> b) -> Command a -> Command b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CostModel -> a -> CostModel
forall a b. a -> b -> a
const (CekMachineCosts
defaultCekMachineCostsForTesting, BuiltinCostMap
defaultSimpleBuiltinCostModel))

execP :: IO (Command CostModel)
execP :: IO (Command CostModel)
execP = Command () -> Command CostModel
forall a. Command a -> Command CostModel
addJSONParameters (Command () -> Command CostModel)
-> IO (Command ()) -> IO (Command CostModel)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParserInfo (Command ()) -> IO (Command ())
forall a. ParserInfo a -> IO a
execParser (Parser (Command ())
-> InfoMod (Command ()) -> ParserInfo (Command ())
forall a. Parser a -> InfoMod a -> ParserInfo a
info (Parser (Command ())
commands Parser (Command ())
-> Parser (Command () -> Command ()) -> Parser (Command ())
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**> Parser (Command () -> Command ())
forall a. Parser (a -> a)
helper)
                    (InfoMod (Command ())
forall a. InfoMod a
fullDesc
                     InfoMod (Command ())
-> InfoMod (Command ()) -> InfoMod (Command ())
forall a. Semigroup a => a -> a -> a
<> String -> InfoMod (Command ())
forall a. String -> InfoMod a
progDesc String
"Plutus Core tool"
                     InfoMod (Command ())
-> InfoMod (Command ()) -> InfoMod (Command ())
forall a. Semigroup a => a -> a -> a
<> String -> InfoMod (Command ())
forall a. String -> InfoMod a
header String
"plc-agda - a Plutus Core implementation written in Agda"))