Safe Haskell	None

PGIP.ReasoningParameters

Documentation

data ReasoningParameters Source #

Constructors

ReasoningParameters
Fields goals :: [GoalConfig] format :: Maybe String

Instances

Instances details

Eq ReasoningParameters Source #
Instance details Defined in PGIP.ReasoningParameters Methods (==) :: ReasoningParameters -> ReasoningParameters -> Bool (/=) :: ReasoningParameters -> ReasoningParameters -> Bool
Show ReasoningParameters Source #
Instance details Defined in PGIP.ReasoningParameters Methods showsPrec :: Int -> ReasoningParameters -> ShowS show :: ReasoningParameters -> String showList :: [ReasoningParameters] -> ShowS
Generic ReasoningParameters Source #
Instance details Defined in PGIP.ReasoningParameters Associated Types type Rep ReasoningParameters :: Type -> Type Methods from :: ReasoningParameters -> Rep ReasoningParameters x to :: Rep ReasoningParameters x -> ReasoningParameters
FromJSON ReasoningParameters Source #
Instance details Defined in PGIP.ReasoningParameters Methods parseJSON :: Value -> Parser ReasoningParameters parseJSONList :: Value -> Parser [ReasoningParameters]
type Rep ReasoningParameters Source #
Instance details Defined in PGIP.ReasoningParameters type Rep ReasoningParameters = D1 ('MetaData "ReasoningParameters" "PGIP.ReasoningParameters" "main" 'False) (C1 ('MetaCons "ReasoningParameters" 'PrefixI 'True) (S1 ('MetaSel ('Just "goals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GoalConfig]) :*: S1 ('MetaSel ('Just "format") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String))))

data GoalConfig Source #

Constructors

GoalConfig
Fields node :: String conjecture :: Maybe String reasonerConfiguration :: ReasonerConfiguration premiseSelection :: Maybe PremiseSelection translation :: Maybe String useTheorems :: Maybe Bool printDetails :: Maybe Bool printProof :: Maybe Bool

Instances

Instances details

Eq GoalConfig Source #
Instance details Defined in PGIP.ReasoningParameters Methods (==) :: GoalConfig -> GoalConfig -> Bool (/=) :: GoalConfig -> GoalConfig -> Bool
Show GoalConfig Source #
Instance details Defined in PGIP.ReasoningParameters Methods showsPrec :: Int -> GoalConfig -> ShowS show :: GoalConfig -> String showList :: [GoalConfig] -> ShowS
Generic GoalConfig Source #
Instance details Defined in PGIP.ReasoningParameters Associated Types type Rep GoalConfig :: Type -> Type Methods from :: GoalConfig -> Rep GoalConfig x to :: Rep GoalConfig x -> GoalConfig
FromJSON GoalConfig Source #
Instance details Defined in PGIP.ReasoningParameters Methods parseJSON :: Value -> Parser GoalConfig parseJSONList :: Value -> Parser [GoalConfig]
type Rep GoalConfig Source #
Instance details Defined in PGIP.ReasoningParameters type Rep GoalConfig = D1 ('MetaData "GoalConfig" "PGIP.ReasoningParameters" "main" 'False) (C1 ('MetaCons "GoalConfig" 'PrefixI 'True) (((S1 ('MetaSel ('Just "node") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: S1 ('MetaSel ('Just "conjecture") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String))) :: (S1 ('MetaSel ('Just "reasonerConfiguration") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ReasonerConfiguration) :: S1 ('MetaSel ('Just "premiseSelection") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe PremiseSelection)))) :: ((S1 ('MetaSel ('Just "translation") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)) :: S1 ('MetaSel ('Just "useTheorems") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool))) :: (S1 ('MetaSel ('Just "printDetails") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: S1 ('MetaSel ('Just "printProof") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool))))))

data ReasonerConfiguration Source #

Constructors

ReasonerConfiguration
Fields timeLimit :: Int reasoner :: Maybe String

Instances

Instances details

Eq ReasonerConfiguration Source #
Instance details Defined in PGIP.ReasoningParameters Methods (==) :: ReasonerConfiguration -> ReasonerConfiguration -> Bool (/=) :: ReasonerConfiguration -> ReasonerConfiguration -> Bool
Show ReasonerConfiguration Source #
Instance details Defined in PGIP.ReasoningParameters Methods showsPrec :: Int -> ReasonerConfiguration -> ShowS show :: ReasonerConfiguration -> String showList :: [ReasonerConfiguration] -> ShowS
Generic ReasonerConfiguration Source #
Instance details Defined in PGIP.ReasoningParameters Associated Types type Rep ReasonerConfiguration :: Type -> Type Methods from :: ReasonerConfiguration -> Rep ReasonerConfiguration x to :: Rep ReasonerConfiguration x -> ReasonerConfiguration
FromJSON ReasonerConfiguration Source #
Instance details Defined in PGIP.ReasoningParameters Methods parseJSON :: Value -> Parser ReasonerConfiguration parseJSONList :: Value -> Parser [ReasonerConfiguration]
type Rep ReasonerConfiguration Source #
Instance details Defined in PGIP.ReasoningParameters type Rep ReasonerConfiguration = D1 ('MetaData "ReasonerConfiguration" "PGIP.ReasoningParameters" "main" 'False) (C1 ('MetaCons "ReasonerConfiguration" 'PrefixI 'True) (S1 ('MetaSel ('Just "timeLimit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "reasoner") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String))))

data PremiseSelection Source #

Constructors

PremiseSelection
Fields kind :: String manualPremises :: Maybe [String] sineDepthLimit :: Maybe Int sineTolerance :: Maybe Double sinePremiseNumberLimit :: Maybe Int

Instances

Instances details

Eq PremiseSelection Source #
Instance details Defined in PGIP.ReasoningParameters Methods (==) :: PremiseSelection -> PremiseSelection -> Bool (/=) :: PremiseSelection -> PremiseSelection -> Bool
Show PremiseSelection Source #
Instance details Defined in PGIP.ReasoningParameters Methods showsPrec :: Int -> PremiseSelection -> ShowS show :: PremiseSelection -> String showList :: [PremiseSelection] -> ShowS
Generic PremiseSelection Source #
Instance details Defined in PGIP.ReasoningParameters Associated Types type Rep PremiseSelection :: Type -> Type Methods from :: PremiseSelection -> Rep PremiseSelection x to :: Rep PremiseSelection x -> PremiseSelection
FromJSON PremiseSelection Source #
Instance details Defined in PGIP.ReasoningParameters Methods parseJSON :: Value -> Parser PremiseSelection parseJSONList :: Value -> Parser [PremiseSelection]
type Rep PremiseSelection Source #
Instance details Defined in PGIP.ReasoningParameters type Rep PremiseSelection = D1 ('MetaData "PremiseSelection" "PGIP.ReasoningParameters" "main" 'False) (C1 ('MetaCons "PremiseSelection" 'PrefixI 'True) ((S1 ('MetaSel ('Just "kind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: S1 ('MetaSel ('Just "manualPremises") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [String]))) :: (S1 ('MetaSel ('Just "sineDepthLimit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)) :: (S1 ('MetaSel ('Just "sineTolerance") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Double)) :: S1 ('MetaSel ('Just "sinePremiseNumberLimit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int))))))

type ReasoningCacheE = [Either String ReasoningCacheGoal] Source #

type ReasoningCache = [ReasoningCacheGoal] Source #

data ReasoningCacheGoal Source #

Constructors

ReasoningCacheGoal

Fields

rceProverMode :: ProverMode
rceNode :: (Int, DGNodeLab)
rceGoalNameM :: Maybe String
rceGoalConfig :: GoalConfig
rceGTheory :: G_theory
rceGSublogic :: G_sublogics
rceReasoner :: ProverOrConsChecker
rceComorphism :: AnyComorphism
rceTimeLimit :: Int
rceUseDatabase :: Bool
rceReasonerConfigurationKeyM :: Maybe ReasonerConfigurationId
rceReasoningAttemptKeyM :: Maybe ReasoningAttemptId

Instances

Instances details

Show ReasoningCacheGoal Source #
Instance details Defined in PGIP.ReasoningParameters Methods showsPrec :: Int -> ReasoningCacheGoal -> ShowS show :: ReasoningCacheGoal -> String showList :: [ReasoningCacheGoal] -> ShowS