Hets - the Heterogeneous Tool Set
Safe HaskellNone

PGIP.ReasoningParameters

Documentation

data ReasoningParameters Source #

Constructors

ReasoningParameters 

Fields

Instances

Instances details
Eq ReasoningParameters Source # 
Instance details

Defined in PGIP.ReasoningParameters

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

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

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

Instances

Instances details
Eq ReasonerConfiguration Source # 
Instance details

Defined in PGIP.ReasoningParameters

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

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

Instances

Instances details
Eq PremiseSelection Source # 
Instance details

Defined in PGIP.ReasoningParameters

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

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))))))