Hets - the Heterogeneous Tool Set

Safe HaskellNone

PGIP.ReasoningParameters

Documentation

data ReasoningParameters Source #

Constructors

ReasoningParameters 

Fields

Instances

Eq ReasoningParameters Source # 
Show ReasoningParameters Source # 

Methods

showsPrec :: Int -> ReasoningParameters -> ShowS

show :: ReasoningParameters -> String

showList :: [ReasoningParameters] -> ShowS

Generic ReasoningParameters Source # 

Associated Types

type Rep ReasoningParameters :: * -> *

FromJSON ReasoningParameters Source # 

Methods

parseJSON :: Value -> Parser ReasoningParameters

parseJSONList :: Value -> Parser [ReasoningParameters]

type Rep ReasoningParameters Source # 
type Rep ReasoningParameters = D1 (MetaData "ReasoningParameters" "PGIP.ReasoningParameters" "main" False) (C1 (MetaCons "ReasoningParameters" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "goals") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [GoalConfig])) (S1 (MetaSel (Just Symbol "format") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String)))))

data GoalConfig Source #

Constructors

GoalConfig 

Fields

Instances

Eq GoalConfig Source # 

Methods

(==) :: GoalConfig -> GoalConfig -> Bool

(/=) :: GoalConfig -> GoalConfig -> Bool

Show GoalConfig Source # 

Methods

showsPrec :: Int -> GoalConfig -> ShowS

show :: GoalConfig -> String

showList :: [GoalConfig] -> ShowS

Generic GoalConfig Source # 

Associated Types

type Rep GoalConfig :: * -> *

Methods

from :: GoalConfig -> Rep GoalConfig x

to :: Rep GoalConfig x -> GoalConfig

FromJSON GoalConfig Source # 

Methods

parseJSON :: Value -> Parser GoalConfig

parseJSONList :: Value -> Parser [GoalConfig]

type Rep GoalConfig Source # 
type Rep GoalConfig = D1 (MetaData "GoalConfig" "PGIP.ReasoningParameters" "main" False) (C1 (MetaCons "GoalConfig" PrefixI True) ((:*:) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "node") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) (S1 (MetaSel (Just Symbol "conjecture") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String)))) ((:*:) (S1 (MetaSel (Just Symbol "reasonerConfiguration") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ReasonerConfiguration)) (S1 (MetaSel (Just Symbol "premiseSelection") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe PremiseSelection))))) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "translation") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String))) (S1 (MetaSel (Just Symbol "useTheorems") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Bool)))) ((:*:) (S1 (MetaSel (Just Symbol "printDetails") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Bool))) (S1 (MetaSel (Just Symbol "printProof") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Bool)))))))

data ReasonerConfiguration Source #

Constructors

ReasonerConfiguration 

Fields

Instances

Eq ReasonerConfiguration Source # 
Show ReasonerConfiguration Source # 

Methods

showsPrec :: Int -> ReasonerConfiguration -> ShowS

show :: ReasonerConfiguration -> String

showList :: [ReasonerConfiguration] -> ShowS

Generic ReasonerConfiguration Source # 
FromJSON ReasonerConfiguration Source # 

Methods

parseJSON :: Value -> Parser ReasonerConfiguration

parseJSONList :: Value -> Parser [ReasonerConfiguration]

type Rep ReasonerConfiguration Source # 
type Rep ReasonerConfiguration = D1 (MetaData "ReasonerConfiguration" "PGIP.ReasoningParameters" "main" False) (C1 (MetaCons "ReasonerConfiguration" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "timeLimit") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) (S1 (MetaSel (Just Symbol "reasoner") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String)))))

data PremiseSelection Source #

Constructors

PremiseSelection 

Fields

Instances

Eq PremiseSelection Source # 
Show PremiseSelection Source # 

Methods

showsPrec :: Int -> PremiseSelection -> ShowS

show :: PremiseSelection -> String

showList :: [PremiseSelection] -> ShowS

Generic PremiseSelection Source # 

Associated Types

type Rep PremiseSelection :: * -> *

FromJSON PremiseSelection Source # 

Methods

parseJSON :: Value -> Parser PremiseSelection

parseJSONList :: Value -> Parser [PremiseSelection]

type Rep PremiseSelection Source # 
type Rep PremiseSelection = D1 (MetaData "PremiseSelection" "PGIP.ReasoningParameters" "main" False) (C1 (MetaCons "PremiseSelection" PrefixI True) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "kind") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 String)) (S1 (MetaSel (Just Symbol "manualPremises") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe [String])))) ((:*:) (S1 (MetaSel (Just Symbol "sineDepthLimit") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int))) ((:*:) (S1 (MetaSel (Just Symbol "sineTolerance") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Double))) (S1 (MetaSel (Just Symbol "sinePremiseNumberLimit") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Int)))))))