{-# 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 { ReasoningParameters -> [GoalConfig]
goals :: [GoalConfig]
                      , ReasoningParameters -> Maybe String
format :: Maybe String
                      } deriving (Int -> ReasoningParameters -> ShowS
[ReasoningParameters] -> ShowS
ReasoningParameters -> String
(Int -> ReasoningParameters -> ShowS)
-> (ReasoningParameters -> String)
-> ([ReasoningParameters] -> ShowS)
-> Show ReasoningParameters
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ReasoningParameters] -> ShowS
$cshowList :: [ReasoningParameters] -> ShowS
show :: ReasoningParameters -> String
$cshow :: ReasoningParameters -> String
showsPrec :: Int -> ReasoningParameters -> ShowS
$cshowsPrec :: Int -> ReasoningParameters -> ShowS
Show, ReasoningParameters -> ReasoningParameters -> Bool
(ReasoningParameters -> ReasoningParameters -> Bool)
-> (ReasoningParameters -> ReasoningParameters -> Bool)
-> Eq ReasoningParameters
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ReasoningParameters -> ReasoningParameters -> Bool
$c/= :: ReasoningParameters -> ReasoningParameters -> Bool
== :: ReasoningParameters -> ReasoningParameters -> Bool
$c== :: ReasoningParameters -> ReasoningParameters -> Bool
Eq, (forall x. ReasoningParameters -> Rep ReasoningParameters x)
-> (forall x. Rep ReasoningParameters x -> ReasoningParameters)
-> Generic ReasoningParameters
forall x. Rep ReasoningParameters x -> ReasoningParameters
forall x. ReasoningParameters -> Rep ReasoningParameters x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ReasoningParameters x -> ReasoningParameters
$cfrom :: forall x. ReasoningParameters -> Rep ReasoningParameters x
Generic)
instance FromJSON ReasoningParameters

data GoalConfig = GoalConfig { GoalConfig -> String
node :: String
                             , GoalConfig -> Maybe String
conjecture :: Maybe String -- required on "prove", must be omitted on "consistency-check"
                             , GoalConfig -> ReasonerConfiguration
reasonerConfiguration :: ReasonerConfiguration
                             , GoalConfig -> Maybe PremiseSelection
premiseSelection :: Maybe PremiseSelection -- ignored on "consistency-check"
                             , GoalConfig -> Maybe String
translation :: Maybe String
                             , GoalConfig -> Maybe Bool
useTheorems :: Maybe Bool -- ignored on "consistency-check"
                             , GoalConfig -> Maybe Bool
printDetails :: Maybe Bool
                             , GoalConfig -> Maybe Bool
printProof :: Maybe Bool
                             } deriving (Int -> GoalConfig -> ShowS
[GoalConfig] -> ShowS
GoalConfig -> String
(Int -> GoalConfig -> ShowS)
-> (GoalConfig -> String)
-> ([GoalConfig] -> ShowS)
-> Show GoalConfig
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GoalConfig] -> ShowS
$cshowList :: [GoalConfig] -> ShowS
show :: GoalConfig -> String
$cshow :: GoalConfig -> String
showsPrec :: Int -> GoalConfig -> ShowS
$cshowsPrec :: Int -> GoalConfig -> ShowS
Show, GoalConfig -> GoalConfig -> Bool
(GoalConfig -> GoalConfig -> Bool)
-> (GoalConfig -> GoalConfig -> Bool) -> Eq GoalConfig
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GoalConfig -> GoalConfig -> Bool
$c/= :: GoalConfig -> GoalConfig -> Bool
== :: GoalConfig -> GoalConfig -> Bool
$c== :: GoalConfig -> GoalConfig -> Bool
Eq, (forall x. GoalConfig -> Rep GoalConfig x)
-> (forall x. Rep GoalConfig x -> GoalConfig) -> Generic GoalConfig
forall x. Rep GoalConfig x -> GoalConfig
forall x. GoalConfig -> Rep GoalConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep GoalConfig x -> GoalConfig
$cfrom :: forall x. GoalConfig -> Rep GoalConfig x
Generic)
instance FromJSON GoalConfig

data ReasonerConfiguration = ReasonerConfiguration { ReasonerConfiguration -> Int
timeLimit :: Int
                                                   , ReasonerConfiguration -> Maybe String
reasoner :: Maybe String
                                                   } deriving (Int -> ReasonerConfiguration -> ShowS
[ReasonerConfiguration] -> ShowS
ReasonerConfiguration -> String
(Int -> ReasonerConfiguration -> ShowS)
-> (ReasonerConfiguration -> String)
-> ([ReasonerConfiguration] -> ShowS)
-> Show ReasonerConfiguration
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ReasonerConfiguration] -> ShowS
$cshowList :: [ReasonerConfiguration] -> ShowS
show :: ReasonerConfiguration -> String
$cshow :: ReasonerConfiguration -> String
showsPrec :: Int -> ReasonerConfiguration -> ShowS
$cshowsPrec :: Int -> ReasonerConfiguration -> ShowS
Show, ReasonerConfiguration -> ReasonerConfiguration -> Bool
(ReasonerConfiguration -> ReasonerConfiguration -> Bool)
-> (ReasonerConfiguration -> ReasonerConfiguration -> Bool)
-> Eq ReasonerConfiguration
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ReasonerConfiguration -> ReasonerConfiguration -> Bool
$c/= :: ReasonerConfiguration -> ReasonerConfiguration -> Bool
== :: ReasonerConfiguration -> ReasonerConfiguration -> Bool
$c== :: ReasonerConfiguration -> ReasonerConfiguration -> Bool
Eq, (forall x. ReasonerConfiguration -> Rep ReasonerConfiguration x)
-> (forall x. Rep ReasonerConfiguration x -> ReasonerConfiguration)
-> Generic ReasonerConfiguration
forall x. Rep ReasonerConfiguration x -> ReasonerConfiguration
forall x. ReasonerConfiguration -> Rep ReasonerConfiguration x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ReasonerConfiguration x -> ReasonerConfiguration
$cfrom :: forall x. ReasonerConfiguration -> Rep ReasonerConfiguration x
Generic)
instance FromJSON ReasonerConfiguration

data PremiseSelection = PremiseSelection { PremiseSelection -> String
kind :: String -- One of "Manual", "SInE" (case-insensitive)
                                         , PremiseSelection -> Maybe [String]
manualPremises :: Maybe [String]
                                         , PremiseSelection -> Maybe Int
sineDepthLimit :: Maybe Int
                                         , PremiseSelection -> Maybe Double
sineTolerance :: Maybe Double
                                         , PremiseSelection -> Maybe Int
sinePremiseNumberLimit :: Maybe Int
                                         }
                        deriving (Int -> PremiseSelection -> ShowS
[PremiseSelection] -> ShowS
PremiseSelection -> String
(Int -> PremiseSelection -> ShowS)
-> (PremiseSelection -> String)
-> ([PremiseSelection] -> ShowS)
-> Show PremiseSelection
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PremiseSelection] -> ShowS
$cshowList :: [PremiseSelection] -> ShowS
show :: PremiseSelection -> String
$cshow :: PremiseSelection -> String
showsPrec :: Int -> PremiseSelection -> ShowS
$cshowsPrec :: Int -> PremiseSelection -> ShowS
Show, PremiseSelection -> PremiseSelection -> Bool
(PremiseSelection -> PremiseSelection -> Bool)
-> (PremiseSelection -> PremiseSelection -> Bool)
-> Eq PremiseSelection
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PremiseSelection -> PremiseSelection -> Bool
$c/= :: PremiseSelection -> PremiseSelection -> Bool
== :: PremiseSelection -> PremiseSelection -> Bool
$c== :: PremiseSelection -> PremiseSelection -> Bool
Eq, (forall x. PremiseSelection -> Rep PremiseSelection x)
-> (forall x. Rep PremiseSelection x -> PremiseSelection)
-> Generic PremiseSelection
forall x. Rep PremiseSelection x -> PremiseSelection
forall x. PremiseSelection -> Rep PremiseSelection x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep PremiseSelection x -> PremiseSelection
$cfrom :: forall x. PremiseSelection -> Rep PremiseSelection x
Generic)
instance FromJSON PremiseSelection

type ReasoningCacheE = [Either String ReasoningCacheGoal]
type ReasoningCache = [ReasoningCacheGoal]
data ReasoningCacheGoal = ReasoningCacheGoal
  { ReasoningCacheGoal -> ProverMode
rceProverMode :: ProverMode
  , ReasoningCacheGoal -> (Int, DGNodeLab)
rceNode :: (Int, DGNodeLab)
  , ReasoningCacheGoal -> Maybe String
rceGoalNameM :: Maybe String -- "Nothing" iff doing consistency-checking
  , ReasoningCacheGoal -> GoalConfig
rceGoalConfig :: GoalConfig
  , ReasoningCacheGoal -> G_theory
rceGTheory :: G_theory
  , ReasoningCacheGoal -> G_sublogics
rceGSublogic :: G_sublogics
  , ReasoningCacheGoal -> ProverOrConsChecker
rceReasoner :: ProverOrConsChecker
  , ReasoningCacheGoal -> AnyComorphism
rceComorphism :: AnyComorphism
  , ReasoningCacheGoal -> Int
rceTimeLimit :: Int
  , ReasoningCacheGoal -> Bool
rceUseDatabase :: Bool
  , ReasoningCacheGoal -> Maybe ReasonerConfigurationId
rceReasonerConfigurationKeyM :: Maybe DatabaseSchema.ReasonerConfigurationId -- made "Just" in the setupReasoning step if a database is used
  , ReasoningCacheGoal -> Maybe ReasoningAttemptId
rceReasoningAttemptKeyM :: Maybe DatabaseSchema.ReasoningAttemptId -- made "Just" in the preprocessReasoning step if a database is used
  } deriving Int -> ReasoningCacheGoal -> ShowS
[ReasoningCacheGoal] -> ShowS
ReasoningCacheGoal -> String
(Int -> ReasoningCacheGoal -> ShowS)
-> (ReasoningCacheGoal -> String)
-> ([ReasoningCacheGoal] -> ShowS)
-> Show ReasoningCacheGoal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ReasoningCacheGoal] -> ShowS
$cshowList :: [ReasoningCacheGoal] -> ShowS
show :: ReasoningCacheGoal -> String
$cshow :: ReasoningCacheGoal -> String
showsPrec :: Int -> ReasoningCacheGoal -> ShowS
$cshowsPrec :: Int -> ReasoningCacheGoal -> ShowS
Show