{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
module Proof.Assistant.Settings where

import Dhall
import Data.HashMap.Strict (HashMap)

data Settings = Settings
  { Settings -> Text
botName :: !Text -- ^ Telegram bot name. Used to parse @/command\@botname@.
  , Settings -> Text
botToken :: !Text -- ^ Bot token.
  , Settings -> Natural
outputSize :: !Natural -- ^ output size in bytes.
  , Settings -> Text
help :: Text -- ^ Help message.
  , Settings -> HashMap Text Text
helpMessages :: HashMap Text Text -- ^ Help messages for sub-commands.
  , Settings -> Text
version :: Text -- ^ Version message.
  , Settings -> InterpretersSettings
interpretersSettings :: !InterpretersSettings -- ^ Settings for backend interpreters.
  } deriving ((forall x. Settings -> Rep Settings x)
-> (forall x. Rep Settings x -> Settings) -> Generic Settings
forall x. Rep Settings x -> Settings
forall x. Settings -> Rep Settings x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Settings x -> Settings
$cfrom :: forall x. Settings -> Rep Settings x
Generic, InputNormalizer -> Decoder Settings
(InputNormalizer -> Decoder Settings) -> FromDhall Settings
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder Settings
$cautoWith :: InputNormalizer -> Decoder Settings
FromDhall)

data ExternalInterpreterSettings = ExternalInterpreterSettings
  { ExternalInterpreterSettings -> CmdArgs
args :: !CmdArgs -- ^ CLI arguments.
  , ExternalInterpreterSettings -> Executable
executable :: !Executable -- ^ Path to executable.
  , ExternalInterpreterSettings -> Time
time :: !Time -- ^ Time, in seconds.
  , ExternalInterpreterSettings -> Priority
priority :: !Priority -- ^ Priority for the thread.
  , ExternalInterpreterSettings -> ResourceSettings
resources :: !ResourceSettings -- ^ Different resources.
  , ExternalInterpreterSettings -> FilePath
tempFilePrefix :: !FilePath -- ^ Prefix to filepath to avoid confusion between different interpreters.
  , ExternalInterpreterSettings -> FilePath
fileExtension :: !FilePath -- ^ File extension used by interpreter.
  , ExternalInterpreterSettings -> Natural
inputSize :: !Natural -- ^ input size in bytes.
  } deriving ((forall x.
 ExternalInterpreterSettings -> Rep ExternalInterpreterSettings x)
-> (forall x.
    Rep ExternalInterpreterSettings x -> ExternalInterpreterSettings)
-> Generic ExternalInterpreterSettings
forall x.
Rep ExternalInterpreterSettings x -> ExternalInterpreterSettings
forall x.
ExternalInterpreterSettings -> Rep ExternalInterpreterSettings x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x.
Rep ExternalInterpreterSettings x -> ExternalInterpreterSettings
$cfrom :: forall x.
ExternalInterpreterSettings -> Rep ExternalInterpreterSettings x
Generic, InputNormalizer -> Decoder ExternalInterpreterSettings
(InputNormalizer -> Decoder ExternalInterpreterSettings)
-> FromDhall ExternalInterpreterSettings
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder ExternalInterpreterSettings
$cautoWith :: InputNormalizer -> Decoder ExternalInterpreterSettings
FromDhall)

data InternalInterpreterSettings = InternalInterpreterSettings
  { InternalInterpreterSettings -> Natural
timeout :: !Natural -- ^ Timeout in seconds.
  , InternalInterpreterSettings -> Natural
allocations :: !Natural -- ^ Max number of GHC allocations for the interpreter thread.
  , InternalInterpreterSettings -> Natural
inputSize :: !Natural -- ^ input size in bytes.
  , InternalInterpreterSettings -> FilePath
sourceFilePrefix :: !FilePath -- ^ Prefix to filepath to avoid confusion between different interpreters.
  , InternalInterpreterSettings -> FilePath
sourceFileExtension :: !FilePath -- ^ File extension used by interpreter.
  } deriving ((forall x.
 InternalInterpreterSettings -> Rep InternalInterpreterSettings x)
-> (forall x.
    Rep InternalInterpreterSettings x -> InternalInterpreterSettings)
-> Generic InternalInterpreterSettings
forall x.
Rep InternalInterpreterSettings x -> InternalInterpreterSettings
forall x.
InternalInterpreterSettings -> Rep InternalInterpreterSettings x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x.
Rep InternalInterpreterSettings x -> InternalInterpreterSettings
$cfrom :: forall x.
InternalInterpreterSettings -> Rep InternalInterpreterSettings x
Generic, InputNormalizer -> Decoder InternalInterpreterSettings
(InputNormalizer -> Decoder InternalInterpreterSettings)
-> FromDhall InternalInterpreterSettings
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder InternalInterpreterSettings
$cautoWith :: InputNormalizer -> Decoder InternalInterpreterSettings
FromDhall)

data AgdaSettings = AgdaSettings
  { AgdaSettings -> InternalInterpreterSettings
internal :: !InternalInterpreterSettings 
  } deriving ((forall x. AgdaSettings -> Rep AgdaSettings x)
-> (forall x. Rep AgdaSettings x -> AgdaSettings)
-> Generic AgdaSettings
forall x. Rep AgdaSettings x -> AgdaSettings
forall x. AgdaSettings -> Rep AgdaSettings x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep AgdaSettings x -> AgdaSettings
$cfrom :: forall x. AgdaSettings -> Rep AgdaSettings x
Generic, InputNormalizer -> Decoder AgdaSettings
(InputNormalizer -> Decoder AgdaSettings) -> FromDhall AgdaSettings
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder AgdaSettings
$cautoWith :: InputNormalizer -> Decoder AgdaSettings
FromDhall)

data LeanSettings = LeanSettings
  { LeanSettings -> FilePath
projectDir :: !FilePath -- ^ Lean requires project where to store source files for typechecking.
  , LeanSettings -> ExternalInterpreterSettings
externalLean   :: !ExternalInterpreterSettings
  } deriving ((forall x. LeanSettings -> Rep LeanSettings x)
-> (forall x. Rep LeanSettings x -> LeanSettings)
-> Generic LeanSettings
forall x. Rep LeanSettings x -> LeanSettings
forall x. LeanSettings -> Rep LeanSettings x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep LeanSettings x -> LeanSettings
$cfrom :: forall x. LeanSettings -> Rep LeanSettings x
Generic, InputNormalizer -> Decoder LeanSettings
(InputNormalizer -> Decoder LeanSettings) -> FromDhall LeanSettings
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder LeanSettings
$cautoWith :: InputNormalizer -> Decoder LeanSettings
FromDhall)

data ArendSettings = ArendSettings
  { ArendSettings -> FilePath
arendRootProjectDir :: !FilePath -- ^ Arend requires different directories to work correctly. One of them used to store libraries, settings, user projects. We call it "root directory".
  , ArendSettings -> FilePath
arendYamlFilename :: !FilePath -- ^ For each project Arend requires yaml file with a specific name.
  , ArendSettings -> Text
arendYamlContent :: !Text -- ^ For each project Arend requires yaml file to store specific settings inside.
  , ArendSettings -> FilePath
arendModuleName :: !FilePath -- ^ Since Arend requires project per chat, it will have a single module inside and we want to give it a common specific configurable name.
  , ArendSettings -> ExternalInterpreterSettings
externalArend :: !ExternalInterpreterSettings
  } deriving ((forall x. ArendSettings -> Rep ArendSettings x)
-> (forall x. Rep ArendSettings x -> ArendSettings)
-> Generic ArendSettings
forall x. Rep ArendSettings x -> ArendSettings
forall x. ArendSettings -> Rep ArendSettings x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ArendSettings x -> ArendSettings
$cfrom :: forall x. ArendSettings -> Rep ArendSettings x
Generic, InputNormalizer -> Decoder ArendSettings
(InputNormalizer -> Decoder ArendSettings)
-> FromDhall ArendSettings
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder ArendSettings
$cautoWith :: InputNormalizer -> Decoder ArendSettings
FromDhall)

newtype IdrisSettings = IdrisSettings ExternalInterpreterSettings
  deriving newtype (InputNormalizer -> Decoder IdrisSettings
(InputNormalizer -> Decoder IdrisSettings)
-> FromDhall IdrisSettings
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder IdrisSettings
$cautoWith :: InputNormalizer -> Decoder IdrisSettings
FromDhall, IdrisSettings -> Natural
(IdrisSettings -> Natural) -> ToInterpreterState IdrisSettings
forall settings.
(settings -> Natural) -> ToInterpreterState settings
getQueueSize :: IdrisSettings -> Natural
$cgetQueueSize :: IdrisSettings -> Natural
ToInterpreterState)
  deriving stock (forall x. IdrisSettings -> Rep IdrisSettings x)
-> (forall x. Rep IdrisSettings x -> IdrisSettings)
-> Generic IdrisSettings
forall x. Rep IdrisSettings x -> IdrisSettings
forall x. IdrisSettings -> Rep IdrisSettings x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep IdrisSettings x -> IdrisSettings
$cfrom :: forall x. IdrisSettings -> Rep IdrisSettings x
Generic

newtype CmdArgs = CmdArgs [Text]
  deriving stock (forall x. CmdArgs -> Rep CmdArgs x)
-> (forall x. Rep CmdArgs x -> CmdArgs) -> Generic CmdArgs
forall x. Rep CmdArgs x -> CmdArgs
forall x. CmdArgs -> Rep CmdArgs x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CmdArgs x -> CmdArgs
$cfrom :: forall x. CmdArgs -> Rep CmdArgs x
Generic
  deriving newtype InputNormalizer -> Decoder CmdArgs
(InputNormalizer -> Decoder CmdArgs) -> FromDhall CmdArgs
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder CmdArgs
$cautoWith :: InputNormalizer -> Decoder CmdArgs
FromDhall

newtype Packages = Packages Text
  deriving stock (forall x. Packages -> Rep Packages x)
-> (forall x. Rep Packages x -> Packages) -> Generic Packages
forall x. Rep Packages x -> Packages
forall x. Packages -> Rep Packages x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Packages x -> Packages
$cfrom :: forall x. Packages -> Rep Packages x
Generic
  deriving newtype InputNormalizer -> Decoder Packages
(InputNormalizer -> Decoder Packages) -> FromDhall Packages
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder Packages
$cautoWith :: InputNormalizer -> Decoder Packages
FromDhall

newtype Executable = Executable Text
  deriving stock (forall x. Executable -> Rep Executable x)
-> (forall x. Rep Executable x -> Executable) -> Generic Executable
forall x. Rep Executable x -> Executable
forall x. Executable -> Rep Executable x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Executable x -> Executable
$cfrom :: forall x. Executable -> Rep Executable x
Generic
  deriving newtype InputNormalizer -> Decoder Executable
(InputNormalizer -> Decoder Executable) -> FromDhall Executable
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder Executable
$cautoWith :: InputNormalizer -> Decoder Executable
FromDhall

newtype Time = Time Natural
  deriving stock (forall x. Time -> Rep Time x)
-> (forall x. Rep Time x -> Time) -> Generic Time
forall x. Rep Time x -> Time
forall x. Time -> Rep Time x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Time x -> Time
$cfrom :: forall x. Time -> Rep Time x
Generic
  deriving newtype InputNormalizer -> Decoder Time
(InputNormalizer -> Decoder Time) -> FromDhall Time
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder Time
$cautoWith :: InputNormalizer -> Decoder Time
FromDhall

newtype Priority = Priority Natural
  deriving stock (forall x. Priority -> Rep Priority x)
-> (forall x. Rep Priority x -> Priority) -> Generic Priority
forall x. Rep Priority x -> Priority
forall x. Priority -> Rep Priority x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Priority x -> Priority
$cfrom :: forall x. Priority -> Rep Priority x
Generic
  deriving newtype InputNormalizer -> Decoder Priority
(InputNormalizer -> Decoder Priority) -> FromDhall Priority
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder Priority
$cautoWith :: InputNormalizer -> Decoder Priority
FromDhall

-- | Resource settings.
data ResourceSettings = ResourceSettings
  { ResourceSettings -> Limit
totalMemory :: !Limit
  , ResourceSettings -> Limit
dataSize    :: !Limit
  , ResourceSettings -> Limit
openFiles   :: !Limit
  , ResourceSettings -> Limit
fileSize    :: !Limit
  , ResourceSettings -> Limit
cpuTime     :: !Limit
  } deriving ((forall x. ResourceSettings -> Rep ResourceSettings x)
-> (forall x. Rep ResourceSettings x -> ResourceSettings)
-> Generic ResourceSettings
forall x. Rep ResourceSettings x -> ResourceSettings
forall x. ResourceSettings -> Rep ResourceSettings x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ResourceSettings x -> ResourceSettings
$cfrom :: forall x. ResourceSettings -> Rep ResourceSettings x
Generic, InputNormalizer -> Decoder ResourceSettings
(InputNormalizer -> Decoder ResourceSettings)
-> FromDhall ResourceSettings
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder ResourceSettings
$cautoWith :: InputNormalizer -> Decoder ResourceSettings
FromDhall)

-- | Limits.
data Limit = Limit
  { Limit -> Natural
soft :: !Natural
  , Limit -> Natural
hard :: !Natural
  } deriving ((forall x. Limit -> Rep Limit x)
-> (forall x. Rep Limit x -> Limit) -> Generic Limit
forall x. Rep Limit x -> Limit
forall x. Limit -> Rep Limit x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Limit x -> Limit
$cfrom :: forall x. Limit -> Rep Limit x
Generic, InputNormalizer -> Decoder Limit
(InputNormalizer -> Decoder Limit) -> FromDhall Limit
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder Limit
$cautoWith :: InputNormalizer -> Decoder Limit
FromDhall)

-- | Combination of all supported interpreters settings.
data InterpretersSettings = InterpretersSettings
  { InterpretersSettings -> AgdaSettings
agda  :: !AgdaSettings
  , InterpretersSettings -> ArendSettings
arend :: !ArendSettings
  , InterpretersSettings -> IdrisSettings
idris :: !IdrisSettings
  , InterpretersSettings -> ExternalInterpreterSettings
coq   :: !ExternalInterpreterSettings
  , InterpretersSettings -> LeanSettings
lean  :: !LeanSettings
  , InterpretersSettings -> InternalInterpreterSettings
rzk   :: !InternalInterpreterSettings
  } deriving ((forall x. InterpretersSettings -> Rep InterpretersSettings x)
-> (forall x. Rep InterpretersSettings x -> InterpretersSettings)
-> Generic InterpretersSettings
forall x. Rep InterpretersSettings x -> InterpretersSettings
forall x. InterpretersSettings -> Rep InterpretersSettings x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep InterpretersSettings x -> InterpretersSettings
$cfrom :: forall x. InterpretersSettings -> Rep InterpretersSettings x
Generic, InputNormalizer -> Decoder InterpretersSettings
(InputNormalizer -> Decoder InterpretersSettings)
-> FromDhall InterpretersSettings
forall a. (InputNormalizer -> Decoder a) -> FromDhall a
autoWith :: InputNormalizer -> Decoder InterpretersSettings
$cautoWith :: InputNormalizer -> Decoder InterpretersSettings
FromDhall)

-- | Load settings from file.
loadSettings :: Text -> IO Settings
loadSettings :: Text -> IO Settings
loadSettings = Decoder Settings -> Text -> IO Settings
forall a. Decoder a -> Text -> IO a
input Decoder Settings
forall a. FromDhall a => Decoder a
auto

-- | Load default settings.
loadDefaultSettings :: IO Settings
loadDefaultSettings :: IO Settings
loadDefaultSettings = Text -> IO Settings
loadSettings Text
"./config/settings.dhall"

-- | Helper to get queue size (communication model between bot and backend worker).
class ToInterpreterState settings where
  getQueueSize :: settings -> Natural

instance ToInterpreterState InternalInterpreterSettings where
  getQueueSize :: InternalInterpreterSettings -> Natural
getQueueSize = InternalInterpreterSettings -> Natural
inputSize

instance ToInterpreterState ExternalInterpreterSettings where
  getQueueSize :: ExternalInterpreterSettings -> Natural
getQueueSize = ExternalInterpreterSettings -> Natural
inputSize

instance ToInterpreterState AgdaSettings where
  getQueueSize :: AgdaSettings -> Natural
getQueueSize = InternalInterpreterSettings -> Natural
forall settings. ToInterpreterState settings => settings -> Natural
getQueueSize (InternalInterpreterSettings -> Natural)
-> (AgdaSettings -> InternalInterpreterSettings)
-> AgdaSettings
-> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AgdaSettings -> InternalInterpreterSettings
internal

instance ToInterpreterState LeanSettings where
  getQueueSize :: LeanSettings -> Natural
getQueueSize = ExternalInterpreterSettings -> Natural
forall settings. ToInterpreterState settings => settings -> Natural
getQueueSize (ExternalInterpreterSettings -> Natural)
-> (LeanSettings -> ExternalInterpreterSettings)
-> LeanSettings
-> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LeanSettings -> ExternalInterpreterSettings
externalLean

instance ToInterpreterState ArendSettings where
  getQueueSize :: ArendSettings -> Natural
getQueueSize = ExternalInterpreterSettings -> Natural
forall settings. ToInterpreterState settings => settings -> Natural
getQueueSize (ExternalInterpreterSettings -> Natural)
-> (ArendSettings -> ExternalInterpreterSettings)
-> ArendSettings
-> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArendSettings -> ExternalInterpreterSettings
externalArend