content: {-# LANGUAGE DeriveGeneric #-}
  
  module PGIP.ReasoningParameters where
  
  import PGIP.Shared (ProverMode)
  
  import Logic.Comorphism (AnyComorphism)
  import Logic.Grothendieck (G_sublogics)
  import Proofs.AbstractState (ProverOrConsChecker)
  import Static.DevGraph (DGNodeLab)
  import Static.GTheory (G_theory)
  import qualified Persistence.Schema as DatabaseSchema
  
  import Data.Aeson
  import GHC.Generics
  
  data ReasoningParameters =
    ReasoningParameters { goals :: [GoalConfig]
                        , format :: Maybe String
                        } deriving (Show, Eq, Generic)
  instance FromJSON ReasoningParameters
  
  data GoalConfig = GoalConfig { node :: String
                               , conjecture :: Maybe String -- required on "prove", must be omitted on "consistency-check"
                               , reasonerConfiguration :: ReasonerConfiguration
                               , premiseSelection :: Maybe PremiseSelection -- ignored on "consistency-check"
                               , translation :: Maybe String
                               , useTheorems :: Maybe Bool -- ignored on "consistency-check"
                               , printDetails :: Maybe Bool
                               , printProof :: Maybe Bool
                               } deriving (Show, Eq, Generic)
  instance FromJSON GoalConfig
  
  data ReasonerConfiguration = ReasonerConfiguration { timeLimit :: Int
                                                     , reasoner :: Maybe String
                                                     } deriving (Show, Eq, Generic)
  instance FromJSON ReasonerConfiguration
  
  data PremiseSelection = PremiseSelection { kind :: String -- One of "Manual", "SInE" (case-insensitive)
                                           , manualPremises :: Maybe [String]
                                           , sineDepthLimit :: Maybe Int
                                           , sineTolerance :: Maybe Double
                                           , sinePremiseNumberLimit :: Maybe Int
                                           }
                          deriving (Show, Eq, Generic)
  instance FromJSON PremiseSelection
  
  type ReasoningCacheE = [Either String ReasoningCacheGoal]
  type ReasoningCache = [ReasoningCacheGoal]
  data ReasoningCacheGoal = ReasoningCacheGoal
    { rceProverMode :: ProverMode
    , rceNode :: (Int, DGNodeLab)
    , rceGoalNameM :: Maybe String -- "Nothing" iff doing consistency-checking
    , rceGoalConfig :: GoalConfig
    , rceGTheory :: G_theory
    , rceGSublogic :: G_sublogics
    , rceReasoner :: ProverOrConsChecker
    , rceComorphism :: AnyComorphism
    , rceTimeLimit :: Int
    , rceUseDatabase :: Bool
    , rceReasonerConfigurationKeyM :: Maybe DatabaseSchema.ReasonerConfigurationId -- made "Just" in the setupReasoning step if a database is used
    , rceReasoningAttemptKeyM :: Maybe DatabaseSchema.ReasoningAttemptId -- made "Just" in the preprocessReasoning step if a database is used
    } deriving Show
  