Copyright | (c) Rene Wagner Heng Jiang Uni Bremen 2007 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | luecke@informatik.uni-bremen.de |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Data structures representing SPASS signatures. Refer to http://spass.mpi-sb.mpg.de/webspass/help/syntax/dfgsyntax.html for the SPASS syntax documentation.
Synopsis
- type SoftFOLMorphism = DefaultMorphism Sign
- type SortMap = Map SPIdentifier (Maybe Generated)
- type FuncMap = Map SPIdentifier (Set ([SPIdentifier], SPIdentifier))
- type PredMap = Map SPIdentifier (Set [SPIdentifier])
- data Sign = Sign {
- sortRel :: Rel SPIdentifier
- sortMap :: SortMap
- funcMap :: FuncMap
- predMap :: PredMap
- singleSorted :: Bool
- data Generated = Generated {
- freely :: Bool
- byFunctions :: [SPIdentifier]
- emptySign :: Sign
- type Sentence = SPTerm
- type SPIdentifier = Token
- singleSortNotGen :: Sign -> Bool
- data SFSymbol = SFSymbol {}
- data SFSymbType
- sfSymbKind :: SFSymbType -> String
- data SPProblem = SPProblem {
- identifier :: String
- description :: SPDescription
- logicalPart :: SPLogicalPart
- settings :: [SPSetting]
- data SPLogicalPart = SPLogicalPart {
- symbolList :: Maybe SPSymbolList
- declarationList :: Maybe [SPDeclaration]
- formulaLists :: [SPFormulaList]
- clauseLists :: [SPClauseList]
- proofLists :: [SPProofList]
- emptySPLogicalPart :: SPLogicalPart
- data SPSymbolList = SPSymbolList {}
- emptySymbolList :: SPSymbolList
- data SPSignSym
- = SPSignSym {
- sym :: SPIdentifier
- arity :: Int
- | SPSimpleSignSym SPIdentifier
- = SPSignSym {
- data SPSortSym = SPSortSym SPIdentifier
- data SPDeclaration
- = SPSubsortDecl { }
- | SPTermDecl {
- termDeclTermList :: [SPTerm]
- termDeclTerm :: SPTerm
- | SPSimpleTermDecl SPTerm
- | SPPredDecl {
- predSym :: SPIdentifier
- sortSyms :: [SPIdentifier]
- | SPGenDecl {
- sortSym :: SPIdentifier
- freelyGenerated :: Bool
- funcList :: [SPIdentifier]
- data SPFormulaList = SPFormulaList {
- originType :: SPOriginType
- formulae :: [SPFormula]
- isAxiomFormula :: SPFormulaList -> Bool
- data SPClauseList = SPClauseList {}
- data SPOriginType
- data SPClauseType
- type SPClause = Named NSPClause
- data NSPClause
- data NSPClauseBody = NSPClauseBody SPClauseType [SPLiteral]
- data TermWsList = TWL [SPTerm] Bool
- data SPTerm
- = SPQuantTerm {
- quantSym :: SPQuantSym
- variableList :: [SPTerm]
- qFormula :: SPTerm
- | SPComplexTerm { }
- = SPQuantTerm {
- data FileName = FileName String
- data FormKind
- data Role
- data Name = Name String
- data Annos = Annos Source (Maybe Info)
- data Source = Source GenTerm
- data AWord = AWord String
- data GenTerm
- = GenTerm GenData (Maybe GenTerm)
- | GenTermList [GenTerm]
- data GenData
- = GenData AWord [GenTerm]
- | OtherGenData String
- | GenFormData FormData
- data FormData = FormData FormKind SPTerm
- data Info = Info [GenTerm]
- data TPTP
- data SPLiteral = SPLiteral Bool SPSymbol
- toLiteral :: MonadFail m => SPTerm -> m SPLiteral
- data SPQuantSym
- data SPSymbol
- mkSPCustomSymbol :: String -> SPSymbol
- showSPSymbol :: SPSymbol -> String
- data SPProofList = SPProofList {
- proofType :: Maybe SPProofType
- plAssocList :: SPAssocList
- step :: [SPProofStep]
- type SPProofType = SPIdentifier
- data SPProofStep = SPProofStep {}
- data SPReference = PRefTerm SPTerm
- data SPResult = PResTerm SPTerm
- data SPRuleAppl
- data SPUserRuleAppl
- data SPParent = PParTerm SPTerm
- type SPAssocList = Map SPKey SPValue
- data SPKey = PKeyTerm SPTerm
- data SPValue = PValTerm SPTerm
- type SPFormula = Named SPTerm
- typedVarTerm :: SPIdentifier -> SPIdentifier -> SPTerm
- spTerms :: [SPIdentifier] -> [SPTerm]
- spSym :: SPIdentifier -> SPSymbol
- compTerm :: SPSymbol -> [SPTerm] -> SPTerm
- simpTerm :: SPSymbol -> SPTerm
- mkConj :: SPTerm -> SPTerm -> SPTerm
- mkDisj :: SPTerm -> SPTerm -> SPTerm
- mkEq :: SPTerm -> SPTerm -> SPTerm
- data SPDescription = SPDescription {}
- data SPLogState
- data SPSetting
- = SPGeneralSettings {
- entries :: [SPHypothesis]
- | SPSettings { }
- = SPGeneralSettings {
- data SPSettingBody
- = SPClauseRelation [SPCRBIND]
- | SPFlag String [String]
- data SPHypothesis = SPHypothesis [SPIdentifier]
- data SPSettingLabel
- showSettingLabel :: SPSettingLabel -> String
- data SPCRBIND = SPCRBIND {
- clauseSPR :: String
- formulaSPR :: String
- negateSentence :: SPTerm -> Maybe SPTerm
Externally used data structures
type SoftFOLMorphism = DefaultMorphism Sign Source #
We use the DefaultMorphism for SPASS.
type SortMap = Map SPIdentifier (Maybe Generated) Source #
type FuncMap = Map SPIdentifier (Set ([SPIdentifier], SPIdentifier)) Source #
type PredMap = Map SPIdentifier (Set [SPIdentifier]) Source #
This Signature data type will be translated to the SoftFOL data types internally.
sortRel contains the sorts relation. For each sort we need to know if it is a generated sort and if so by which functions it is possibly freely generated (sortMap).
For each function the types of all arguments and the return type must be known (funcMap). The same goes for the arguments of a predicate (predMap).
Sign | |
|
Instances
Sorts can be (freely) generated by a set of functions.
Generated | |
|
Instances
Eq Generated Source # | |
Data Generated Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Generated -> c Generated gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Generated toConstr :: Generated -> Constr dataTypeOf :: Generated -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Generated) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Generated) gmapT :: (forall b. Data b => b -> b) -> Generated -> Generated gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Generated -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Generated -> r gmapQ :: (forall d. Data d => d -> u) -> Generated -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Generated -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Generated -> m Generated gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Generated -> m Generated gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Generated -> m Generated | |
Ord Generated Source # | |
Defined in SoftFOL.Sign | |
Show Generated Source # | |
Generic Generated | |
FromJSON Generated | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser Generated parseJSONList :: Value -> Parser [Generated] | |
ToJSON Generated | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: Generated -> Encoding toJSONList :: [Generated] -> Value toEncodingList :: [Generated] -> Encoding | |
ShATermConvertible Generated | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> Generated -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Generated] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Generated) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Generated]) | |
type Rep Generated | |
Defined in SoftFOL.ATC_SoftFOL type Rep Generated = D1 ('MetaData "Generated" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "Generated" 'PrefixI 'True) (S1 ('MetaSel ('Just "freely") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "byFunctions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPIdentifier]))) |
type SPIdentifier = Token Source #
A SPASS Identifier is a String for now.
singleSortNotGen :: Sign -> Bool Source #
Check a Sign if it is single sorted (and the sort is non-generated).
Symbol related datatypes
Symbols of SoftFOL.
Instances
data SFSymbType Source #
Symbol types of SoftFOL. (not related to CASL)
Instances
Eq SFSymbType Source # | |
Defined in SoftFOL.Sign (==) :: SFSymbType -> SFSymbType -> Bool (/=) :: SFSymbType -> SFSymbType -> Bool | |
Data SFSymbType Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SFSymbType -> c SFSymbType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SFSymbType toConstr :: SFSymbType -> Constr dataTypeOf :: SFSymbType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SFSymbType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SFSymbType) gmapT :: (forall b. Data b => b -> b) -> SFSymbType -> SFSymbType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SFSymbType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SFSymbType -> r gmapQ :: (forall d. Data d => d -> u) -> SFSymbType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SFSymbType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SFSymbType -> m SFSymbType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SFSymbType -> m SFSymbType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SFSymbType -> m SFSymbType | |
Ord SFSymbType Source # | |
Defined in SoftFOL.Sign compare :: SFSymbType -> SFSymbType -> Ordering (<) :: SFSymbType -> SFSymbType -> Bool (<=) :: SFSymbType -> SFSymbType -> Bool (>) :: SFSymbType -> SFSymbType -> Bool (>=) :: SFSymbType -> SFSymbType -> Bool max :: SFSymbType -> SFSymbType -> SFSymbType min :: SFSymbType -> SFSymbType -> SFSymbType | |
Show SFSymbType Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SFSymbType -> ShowS show :: SFSymbType -> String showList :: [SFSymbType] -> ShowS | |
Generic SFSymbType | |
Defined in SoftFOL.ATC_SoftFOL type Rep SFSymbType :: Type -> Type from :: SFSymbType -> Rep SFSymbType x to :: Rep SFSymbType x -> SFSymbType | |
FromJSON SFSymbType | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SFSymbType parseJSONList :: Value -> Parser [SFSymbType] | |
ToJSON SFSymbType | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SFSymbType -> Value toEncoding :: SFSymbType -> Encoding toJSONList :: [SFSymbType] -> Value toEncodingList :: [SFSymbType] -> Encoding | |
ShATermConvertible SFSymbType | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SFSymbType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SFSymbType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SFSymbType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SFSymbType]) | |
Pretty SFSymbType Source # | |
Defined in SoftFOL.Print pretty :: SFSymbType -> Doc Source # pretties :: [SFSymbType] -> Doc Source # | |
type Rep SFSymbType | |
Defined in SoftFOL.ATC_SoftFOL type Rep SFSymbType = D1 ('MetaData "SFSymbType" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SFOpType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPIdentifier]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPIdentifier)) :+: (C1 ('MetaCons "SFPredType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPIdentifier])) :+: C1 ('MetaCons "SFSortType" 'PrefixI 'False) (U1 :: Type -> Type))) |
sfSymbKind :: SFSymbType -> String Source #
Internal data structures
SPASS Problems
A SPASS problem consists of a description and a logical part. The optional settings part hasn't been implemented yet.
SPProblem | |
|
Instances
Eq SPProblem Source # | |
Data SPProblem Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPProblem -> c SPProblem gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPProblem toConstr :: SPProblem -> Constr dataTypeOf :: SPProblem -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPProblem) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPProblem) gmapT :: (forall b. Data b => b -> b) -> SPProblem -> SPProblem gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPProblem -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPProblem -> r gmapQ :: (forall d. Data d => d -> u) -> SPProblem -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPProblem -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPProblem -> m SPProblem gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPProblem -> m SPProblem gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPProblem -> m SPProblem | |
Ord SPProblem Source # | |
Defined in SoftFOL.Sign | |
Show SPProblem Source # | |
Generic SPProblem | |
FromJSON SPProblem | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPProblem parseJSONList :: Value -> Parser [SPProblem] | |
ToJSON SPProblem | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: SPProblem -> Encoding toJSONList :: [SPProblem] -> Value toEncodingList :: [SPProblem] -> Encoding | |
ShATermConvertible SPProblem | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPProblem -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPProblem] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPProblem) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPProblem]) | |
Pretty SPProblem Source # | Creates a Doc from a SPASS Problem. |
PrintTPTP SPProblem Source # | Creates a Doc from a SoftFOL Problem. |
type Rep SPProblem | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPProblem = D1 ('MetaData "SPProblem" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPProblem" 'PrefixI 'True) ((S1 ('MetaSel ('Just "identifier") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "description") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPDescription)) :*: (S1 ('MetaSel ('Just "logicalPart") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPLogicalPart) :*: S1 ('MetaSel ('Just "settings") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPSetting])))) |
SPASS Logical Parts
data SPLogicalPart Source #
A SPASS logical part consists of a symbol list, a declaration list, and a set of formula lists. Support for clause lists and proof lists hasn't been implemented yet.
SPLogicalPart | |
|
Instances
Eq SPLogicalPart Source # | |
Defined in SoftFOL.Sign (==) :: SPLogicalPart -> SPLogicalPart -> Bool (/=) :: SPLogicalPart -> SPLogicalPart -> Bool | |
Data SPLogicalPart Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPLogicalPart -> c SPLogicalPart gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPLogicalPart toConstr :: SPLogicalPart -> Constr dataTypeOf :: SPLogicalPart -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPLogicalPart) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPLogicalPart) gmapT :: (forall b. Data b => b -> b) -> SPLogicalPart -> SPLogicalPart gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPLogicalPart -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPLogicalPart -> r gmapQ :: (forall d. Data d => d -> u) -> SPLogicalPart -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPLogicalPart -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPLogicalPart -> m SPLogicalPart gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPLogicalPart -> m SPLogicalPart gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPLogicalPart -> m SPLogicalPart | |
Ord SPLogicalPart Source # | |
Defined in SoftFOL.Sign compare :: SPLogicalPart -> SPLogicalPart -> Ordering (<) :: SPLogicalPart -> SPLogicalPart -> Bool (<=) :: SPLogicalPart -> SPLogicalPart -> Bool (>) :: SPLogicalPart -> SPLogicalPart -> Bool (>=) :: SPLogicalPart -> SPLogicalPart -> Bool max :: SPLogicalPart -> SPLogicalPart -> SPLogicalPart min :: SPLogicalPart -> SPLogicalPart -> SPLogicalPart | |
Show SPLogicalPart Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPLogicalPart -> ShowS show :: SPLogicalPart -> String showList :: [SPLogicalPart] -> ShowS | |
Generic SPLogicalPart | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPLogicalPart :: Type -> Type from :: SPLogicalPart -> Rep SPLogicalPart x to :: Rep SPLogicalPart x -> SPLogicalPart | |
FromJSON SPLogicalPart | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPLogicalPart parseJSONList :: Value -> Parser [SPLogicalPart] | |
ToJSON SPLogicalPart | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPLogicalPart -> Value toEncoding :: SPLogicalPart -> Encoding toJSONList :: [SPLogicalPart] -> Value toEncodingList :: [SPLogicalPart] -> Encoding | |
ShATermConvertible SPLogicalPart | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPLogicalPart -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPLogicalPart] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPLogicalPart) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPLogicalPart]) | |
Pretty SPLogicalPart Source # | Creates a Doc from a SPASS Logical Part. |
Defined in SoftFOL.Print pretty :: SPLogicalPart -> Doc Source # pretties :: [SPLogicalPart] -> Doc Source # | |
PrintTPTP SPLogicalPart Source # | Creates a Doc from a SoftFOL Logical Part. |
Defined in SoftFOL.PrintTPTP printTPTP :: SPLogicalPart -> Doc Source # | |
type Rep SPLogicalPart | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPLogicalPart = D1 ('MetaData "SPLogicalPart" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPLogicalPart" 'PrefixI 'True) ((S1 ('MetaSel ('Just "symbolList") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe SPSymbolList)) :*: S1 ('MetaSel ('Just "declarationList") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [SPDeclaration]))) :*: (S1 ('MetaSel ('Just "formulaLists") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPFormulaList]) :*: (S1 ('MetaSel ('Just "clauseLists") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPClauseList]) :*: S1 ('MetaSel ('Just "proofLists") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPProofList]))))) |
Symbol Lists
data SPSymbolList Source #
All non-predefined signature symbols must be declared as part of a SPASS symbol list.
Instances
Eq SPSymbolList Source # | |
Defined in SoftFOL.Sign (==) :: SPSymbolList -> SPSymbolList -> Bool (/=) :: SPSymbolList -> SPSymbolList -> Bool | |
Data SPSymbolList Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPSymbolList -> c SPSymbolList gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPSymbolList toConstr :: SPSymbolList -> Constr dataTypeOf :: SPSymbolList -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPSymbolList) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPSymbolList) gmapT :: (forall b. Data b => b -> b) -> SPSymbolList -> SPSymbolList gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPSymbolList -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPSymbolList -> r gmapQ :: (forall d. Data d => d -> u) -> SPSymbolList -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPSymbolList -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPSymbolList -> m SPSymbolList gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSymbolList -> m SPSymbolList gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSymbolList -> m SPSymbolList | |
Ord SPSymbolList Source # | |
Defined in SoftFOL.Sign compare :: SPSymbolList -> SPSymbolList -> Ordering (<) :: SPSymbolList -> SPSymbolList -> Bool (<=) :: SPSymbolList -> SPSymbolList -> Bool (>) :: SPSymbolList -> SPSymbolList -> Bool (>=) :: SPSymbolList -> SPSymbolList -> Bool max :: SPSymbolList -> SPSymbolList -> SPSymbolList min :: SPSymbolList -> SPSymbolList -> SPSymbolList | |
Show SPSymbolList Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPSymbolList -> ShowS show :: SPSymbolList -> String showList :: [SPSymbolList] -> ShowS | |
Generic SPSymbolList | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPSymbolList :: Type -> Type from :: SPSymbolList -> Rep SPSymbolList x to :: Rep SPSymbolList x -> SPSymbolList | |
FromJSON SPSymbolList | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPSymbolList parseJSONList :: Value -> Parser [SPSymbolList] | |
ToJSON SPSymbolList | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPSymbolList -> Value toEncoding :: SPSymbolList -> Encoding toJSONList :: [SPSymbolList] -> Value toEncodingList :: [SPSymbolList] -> Encoding | |
ShATermConvertible SPSymbolList | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPSymbolList -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPSymbolList] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSymbolList) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPSymbolList]) | |
Pretty SPSymbolList Source # | Creates a Doc from a SPASS Symbol List. |
Defined in SoftFOL.Print pretty :: SPSymbolList -> Doc Source # pretties :: [SPSymbolList] -> Doc Source # | |
type Rep SPSymbolList | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPSymbolList = D1 ('MetaData "SPSymbolList" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPSymbolList" 'PrefixI 'True) (S1 ('MetaSel ('Just "functions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPSignSym]) :*: (S1 ('MetaSel ('Just "predicates") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPSignSym]) :*: S1 ('MetaSel ('Just "sorts") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPSignSym])))) |
emptySymbolList :: SPSymbolList Source #
Creates an empty SPASS Symbol List.
A common data type used for all signature symbols.
SPSignSym | |
| |
SPSimpleSignSym SPIdentifier |
Instances
Eq SPSignSym Source # | |
Data SPSignSym Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPSignSym -> c SPSignSym gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPSignSym toConstr :: SPSignSym -> Constr dataTypeOf :: SPSignSym -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPSignSym) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPSignSym) gmapT :: (forall b. Data b => b -> b) -> SPSignSym -> SPSignSym gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPSignSym -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPSignSym -> r gmapQ :: (forall d. Data d => d -> u) -> SPSignSym -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPSignSym -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPSignSym -> m SPSignSym gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSignSym -> m SPSignSym gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSignSym -> m SPSignSym | |
Ord SPSignSym Source # | |
Defined in SoftFOL.Sign | |
Show SPSignSym Source # | |
Generic SPSignSym | |
FromJSON SPSignSym | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPSignSym parseJSONList :: Value -> Parser [SPSignSym] | |
ToJSON SPSignSym | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: SPSignSym -> Encoding toJSONList :: [SPSignSym] -> Value toEncodingList :: [SPSignSym] -> Encoding | |
ShATermConvertible SPSignSym | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPSignSym -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPSignSym] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSignSym) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPSignSym]) | |
Pretty SPSignSym Source # | Helper function. Creates a Doc from a Signature Symbol. |
type Rep SPSignSym | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPSignSym = D1 ('MetaData "SPSignSym" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPSignSym" 'PrefixI 'True) (S1 ('MetaSel ('Just "sym") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPIdentifier) :*: S1 ('MetaSel ('Just "arity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "SPSimpleSignSym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPIdentifier))) |
Instances
Eq SPSortSym Source # | |
Data SPSortSym Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPSortSym -> c SPSortSym gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPSortSym toConstr :: SPSortSym -> Constr dataTypeOf :: SPSortSym -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPSortSym) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPSortSym) gmapT :: (forall b. Data b => b -> b) -> SPSortSym -> SPSortSym gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPSortSym -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPSortSym -> r gmapQ :: (forall d. Data d => d -> u) -> SPSortSym -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPSortSym -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPSortSym -> m SPSortSym gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSortSym -> m SPSortSym gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSortSym -> m SPSortSym | |
Ord SPSortSym Source # | |
Defined in SoftFOL.Sign | |
Show SPSortSym Source # | |
Generic SPSortSym | |
FromJSON SPSortSym | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPSortSym parseJSONList :: Value -> Parser [SPSortSym] | |
ToJSON SPSortSym | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: SPSortSym -> Encoding toJSONList :: [SPSortSym] -> Value toEncodingList :: [SPSortSym] -> Encoding | |
ShATermConvertible SPSortSym | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPSortSym -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPSortSym] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSortSym) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPSortSym]) | |
type Rep SPSortSym | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPSortSym = D1 ('MetaData "SPSortSym" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPSortSym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPIdentifier))) |
Declarations
data SPDeclaration Source #
SPASS Declarations allow the introduction of sorts.
SPSubsortDecl | |
SPTermDecl | |
| |
SPSimpleTermDecl SPTerm | |
SPPredDecl | |
| |
SPGenDecl | |
|
Instances
Eq SPDeclaration Source # | |
Defined in SoftFOL.Sign (==) :: SPDeclaration -> SPDeclaration -> Bool (/=) :: SPDeclaration -> SPDeclaration -> Bool | |
Data SPDeclaration Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPDeclaration -> c SPDeclaration gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPDeclaration toConstr :: SPDeclaration -> Constr dataTypeOf :: SPDeclaration -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPDeclaration) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPDeclaration) gmapT :: (forall b. Data b => b -> b) -> SPDeclaration -> SPDeclaration gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPDeclaration -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPDeclaration -> r gmapQ :: (forall d. Data d => d -> u) -> SPDeclaration -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPDeclaration -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPDeclaration -> m SPDeclaration gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPDeclaration -> m SPDeclaration gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPDeclaration -> m SPDeclaration | |
Ord SPDeclaration Source # | |
Defined in SoftFOL.Sign compare :: SPDeclaration -> SPDeclaration -> Ordering (<) :: SPDeclaration -> SPDeclaration -> Bool (<=) :: SPDeclaration -> SPDeclaration -> Bool (>) :: SPDeclaration -> SPDeclaration -> Bool (>=) :: SPDeclaration -> SPDeclaration -> Bool max :: SPDeclaration -> SPDeclaration -> SPDeclaration min :: SPDeclaration -> SPDeclaration -> SPDeclaration | |
Show SPDeclaration Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPDeclaration -> ShowS show :: SPDeclaration -> String showList :: [SPDeclaration] -> ShowS | |
Generic SPDeclaration | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPDeclaration :: Type -> Type from :: SPDeclaration -> Rep SPDeclaration x to :: Rep SPDeclaration x -> SPDeclaration | |
FromJSON SPDeclaration | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPDeclaration parseJSONList :: Value -> Parser [SPDeclaration] | |
ToJSON SPDeclaration | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPDeclaration -> Value toEncoding :: SPDeclaration -> Encoding toJSONList :: [SPDeclaration] -> Value toEncodingList :: [SPDeclaration] -> Encoding | |
ShATermConvertible SPDeclaration | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPDeclaration -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPDeclaration] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPDeclaration) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPDeclaration]) | |
Pretty SPDeclaration Source # | Creates a Doc from a SPASS Declaration |
Defined in SoftFOL.Print pretty :: SPDeclaration -> Doc Source # pretties :: [SPDeclaration] -> Doc Source # | |
PrintTPTP SPDeclaration Source # | Creates a Doc from a SoftFOL Declaration. A subsort declaration will be rewritten as a special SPQuantTerm. |
Defined in SoftFOL.PrintTPTP printTPTP :: SPDeclaration -> Doc Source # | |
type Rep SPDeclaration | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPDeclaration = D1 ('MetaData "SPDeclaration" "SoftFOL.Sign" "main" 'False) ((C1 ('MetaCons "SPSubsortDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "sortSymA") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPIdentifier) :*: S1 ('MetaSel ('Just "sortSymB") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPIdentifier)) :+: C1 ('MetaCons "SPTermDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "termDeclTermList") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPTerm]) :*: S1 ('MetaSel ('Just "termDeclTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPTerm))) :+: (C1 ('MetaCons "SPSimpleTermDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPTerm)) :+: (C1 ('MetaCons "SPPredDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "predSym") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPIdentifier) :*: S1 ('MetaSel ('Just "sortSyms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPIdentifier])) :+: C1 ('MetaCons "SPGenDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "sortSym") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPIdentifier) :*: (S1 ('MetaSel ('Just "freelyGenerated") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "funcList") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPIdentifier])))))) |
Formula List
data SPFormulaList Source #
SPASS Formula List
Instances
Eq SPFormulaList Source # | |
Defined in SoftFOL.Sign (==) :: SPFormulaList -> SPFormulaList -> Bool (/=) :: SPFormulaList -> SPFormulaList -> Bool | |
Data SPFormulaList Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPFormulaList -> c SPFormulaList gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPFormulaList toConstr :: SPFormulaList -> Constr dataTypeOf :: SPFormulaList -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPFormulaList) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPFormulaList) gmapT :: (forall b. Data b => b -> b) -> SPFormulaList -> SPFormulaList gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPFormulaList -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPFormulaList -> r gmapQ :: (forall d. Data d => d -> u) -> SPFormulaList -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPFormulaList -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPFormulaList -> m SPFormulaList gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPFormulaList -> m SPFormulaList gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPFormulaList -> m SPFormulaList | |
Ord SPFormulaList Source # | |
Defined in SoftFOL.Sign compare :: SPFormulaList -> SPFormulaList -> Ordering (<) :: SPFormulaList -> SPFormulaList -> Bool (<=) :: SPFormulaList -> SPFormulaList -> Bool (>) :: SPFormulaList -> SPFormulaList -> Bool (>=) :: SPFormulaList -> SPFormulaList -> Bool max :: SPFormulaList -> SPFormulaList -> SPFormulaList min :: SPFormulaList -> SPFormulaList -> SPFormulaList | |
Show SPFormulaList Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPFormulaList -> ShowS show :: SPFormulaList -> String showList :: [SPFormulaList] -> ShowS | |
Generic SPFormulaList | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPFormulaList :: Type -> Type from :: SPFormulaList -> Rep SPFormulaList x to :: Rep SPFormulaList x -> SPFormulaList | |
FromJSON SPFormulaList | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPFormulaList parseJSONList :: Value -> Parser [SPFormulaList] | |
ToJSON SPFormulaList | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPFormulaList -> Value toEncoding :: SPFormulaList -> Encoding toJSONList :: [SPFormulaList] -> Value toEncodingList :: [SPFormulaList] -> Encoding | |
ShATermConvertible SPFormulaList | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPFormulaList -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPFormulaList] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPFormulaList) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPFormulaList]) | |
Pretty SPFormulaList Source # | Creates a Doc from a SPASS Formula List |
Defined in SoftFOL.Print pretty :: SPFormulaList -> Doc Source # pretties :: [SPFormulaList] -> Doc Source # | |
PrintTPTP SPFormulaList Source # | Creates a Doc from a SoftFOL Formula List. |
Defined in SoftFOL.PrintTPTP printTPTP :: SPFormulaList -> Doc Source # | |
type Rep SPFormulaList | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPFormulaList = D1 ('MetaData "SPFormulaList" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPFormulaList" 'PrefixI 'True) (S1 ('MetaSel ('Just "originType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPOriginType) :*: S1 ('MetaSel ('Just "formulae") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPFormula]))) |
isAxiomFormula :: SPFormulaList -> Bool Source #
test the origin type of the formula list
Clause List
data SPClauseList Source #
SPASS Clause List
Instances
Eq SPClauseList Source # | |
Defined in SoftFOL.Sign (==) :: SPClauseList -> SPClauseList -> Bool (/=) :: SPClauseList -> SPClauseList -> Bool | |
Data SPClauseList Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPClauseList -> c SPClauseList gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPClauseList toConstr :: SPClauseList -> Constr dataTypeOf :: SPClauseList -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPClauseList) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPClauseList) gmapT :: (forall b. Data b => b -> b) -> SPClauseList -> SPClauseList gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPClauseList -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPClauseList -> r gmapQ :: (forall d. Data d => d -> u) -> SPClauseList -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPClauseList -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPClauseList -> m SPClauseList gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPClauseList -> m SPClauseList gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPClauseList -> m SPClauseList | |
Ord SPClauseList Source # | |
Defined in SoftFOL.Sign compare :: SPClauseList -> SPClauseList -> Ordering (<) :: SPClauseList -> SPClauseList -> Bool (<=) :: SPClauseList -> SPClauseList -> Bool (>) :: SPClauseList -> SPClauseList -> Bool (>=) :: SPClauseList -> SPClauseList -> Bool max :: SPClauseList -> SPClauseList -> SPClauseList min :: SPClauseList -> SPClauseList -> SPClauseList | |
Show SPClauseList Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPClauseList -> ShowS show :: SPClauseList -> String showList :: [SPClauseList] -> ShowS | |
Generic SPClauseList | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPClauseList :: Type -> Type from :: SPClauseList -> Rep SPClauseList x to :: Rep SPClauseList x -> SPClauseList | |
FromJSON SPClauseList | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPClauseList parseJSONList :: Value -> Parser [SPClauseList] | |
ToJSON SPClauseList | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPClauseList -> Value toEncoding :: SPClauseList -> Encoding toJSONList :: [SPClauseList] -> Value toEncodingList :: [SPClauseList] -> Encoding | |
ShATermConvertible SPClauseList | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPClauseList -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPClauseList] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPClauseList) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPClauseList]) | |
Pretty SPClauseList Source # | |
Defined in SoftFOL.Print pretty :: SPClauseList -> Doc Source # pretties :: [SPClauseList] -> Doc Source # | |
type Rep SPClauseList | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPClauseList = D1 ('MetaData "SPClauseList" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPClauseList" 'PrefixI 'True) (S1 ('MetaSel ('Just "coriginType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPOriginType) :*: (S1 ('MetaSel ('Just "clauseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPClauseType) :*: S1 ('MetaSel ('Just "clauses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPClause])))) |
data SPOriginType Source #
There are axiom formulae and conjecture formulae.
Instances
Eq SPOriginType Source # | |
Defined in SoftFOL.Sign (==) :: SPOriginType -> SPOriginType -> Bool (/=) :: SPOriginType -> SPOriginType -> Bool | |
Data SPOriginType Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPOriginType -> c SPOriginType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPOriginType toConstr :: SPOriginType -> Constr dataTypeOf :: SPOriginType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPOriginType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPOriginType) gmapT :: (forall b. Data b => b -> b) -> SPOriginType -> SPOriginType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPOriginType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPOriginType -> r gmapQ :: (forall d. Data d => d -> u) -> SPOriginType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPOriginType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPOriginType -> m SPOriginType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPOriginType -> m SPOriginType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPOriginType -> m SPOriginType | |
Ord SPOriginType Source # | |
Defined in SoftFOL.Sign compare :: SPOriginType -> SPOriginType -> Ordering (<) :: SPOriginType -> SPOriginType -> Bool (<=) :: SPOriginType -> SPOriginType -> Bool (>) :: SPOriginType -> SPOriginType -> Bool (>=) :: SPOriginType -> SPOriginType -> Bool max :: SPOriginType -> SPOriginType -> SPOriginType min :: SPOriginType -> SPOriginType -> SPOriginType | |
Show SPOriginType Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPOriginType -> ShowS show :: SPOriginType -> String showList :: [SPOriginType] -> ShowS | |
Generic SPOriginType | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPOriginType :: Type -> Type from :: SPOriginType -> Rep SPOriginType x to :: Rep SPOriginType x -> SPOriginType | |
FromJSON SPOriginType | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPOriginType parseJSONList :: Value -> Parser [SPOriginType] | |
ToJSON SPOriginType | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPOriginType -> Value toEncoding :: SPOriginType -> Encoding toJSONList :: [SPOriginType] -> Value toEncodingList :: [SPOriginType] -> Encoding | |
ShATermConvertible SPOriginType | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPOriginType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPOriginType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPOriginType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPOriginType]) | |
Pretty SPOriginType Source # | Creates a Doc from a SPASS Origin Type |
Defined in SoftFOL.Print pretty :: SPOriginType -> Doc Source # pretties :: [SPOriginType] -> Doc Source # | |
PrintTPTP SPOriginType Source # | Creates a Doc from a SoftFOL Origin Type. |
Defined in SoftFOL.PrintTPTP printTPTP :: SPOriginType -> Doc Source # | |
type Rep SPOriginType | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPOriginType = D1 ('MetaData "SPOriginType" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPOriginAxioms" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SPOriginConjectures" 'PrefixI 'False) (U1 :: Type -> Type)) |
data SPClauseType Source #
Formulae can be in cnf or dnf
Instances
Eq SPClauseType Source # | |
Defined in SoftFOL.Sign (==) :: SPClauseType -> SPClauseType -> Bool (/=) :: SPClauseType -> SPClauseType -> Bool | |
Data SPClauseType Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPClauseType -> c SPClauseType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPClauseType toConstr :: SPClauseType -> Constr dataTypeOf :: SPClauseType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPClauseType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPClauseType) gmapT :: (forall b. Data b => b -> b) -> SPClauseType -> SPClauseType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPClauseType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPClauseType -> r gmapQ :: (forall d. Data d => d -> u) -> SPClauseType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPClauseType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPClauseType -> m SPClauseType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPClauseType -> m SPClauseType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPClauseType -> m SPClauseType | |
Ord SPClauseType Source # | |
Defined in SoftFOL.Sign compare :: SPClauseType -> SPClauseType -> Ordering (<) :: SPClauseType -> SPClauseType -> Bool (<=) :: SPClauseType -> SPClauseType -> Bool (>) :: SPClauseType -> SPClauseType -> Bool (>=) :: SPClauseType -> SPClauseType -> Bool max :: SPClauseType -> SPClauseType -> SPClauseType min :: SPClauseType -> SPClauseType -> SPClauseType | |
Show SPClauseType Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPClauseType -> ShowS show :: SPClauseType -> String showList :: [SPClauseType] -> ShowS | |
Generic SPClauseType | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPClauseType :: Type -> Type from :: SPClauseType -> Rep SPClauseType x to :: Rep SPClauseType x -> SPClauseType | |
FromJSON SPClauseType | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPClauseType parseJSONList :: Value -> Parser [SPClauseType] | |
ToJSON SPClauseType | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPClauseType -> Value toEncoding :: SPClauseType -> Encoding toJSONList :: [SPClauseType] -> Value toEncodingList :: [SPClauseType] -> Encoding | |
ShATermConvertible SPClauseType | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPClauseType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPClauseType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPClauseType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPClauseType]) | |
Pretty SPClauseType Source # | |
Defined in SoftFOL.Print pretty :: SPClauseType -> Doc Source # pretties :: [SPClauseType] -> Doc Source # | |
type Rep SPClauseType | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPClauseType = D1 ('MetaData "SPClauseType" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPCNF" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SPDNF" 'PrefixI 'False) (U1 :: Type -> Type)) |
QuanClause [SPTerm] NSPClauseBody | |
SimpleClause NSPClauseBody | |
BriefClause TermWsList TermWsList TermWsList |
Instances
Eq NSPClause Source # | |
Data NSPClause Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NSPClause -> c NSPClause gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NSPClause toConstr :: NSPClause -> Constr dataTypeOf :: NSPClause -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NSPClause) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NSPClause) gmapT :: (forall b. Data b => b -> b) -> NSPClause -> NSPClause gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NSPClause -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NSPClause -> r gmapQ :: (forall d. Data d => d -> u) -> NSPClause -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> NSPClause -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> NSPClause -> m NSPClause gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NSPClause -> m NSPClause gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NSPClause -> m NSPClause | |
Ord NSPClause Source # | |
Defined in SoftFOL.Sign | |
Show NSPClause Source # | |
Generic NSPClause | |
FromJSON NSPClause | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser NSPClause parseJSONList :: Value -> Parser [NSPClause] | |
ToJSON NSPClause | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: NSPClause -> Encoding toJSONList :: [NSPClause] -> Value toEncodingList :: [NSPClause] -> Encoding | |
ShATermConvertible NSPClause | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> NSPClause -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [NSPClause] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, NSPClause) fromShATermList' :: Int -> ATermTable -> (ATermTable, [NSPClause]) | |
Pretty NSPClause Source # | |
type Rep NSPClause | |
Defined in SoftFOL.ATC_SoftFOL type Rep NSPClause = D1 ('MetaData "NSPClause" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "QuanClause" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPTerm]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NSPClauseBody)) :+: (C1 ('MetaCons "SimpleClause" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NSPClauseBody)) :+: C1 ('MetaCons "BriefClause" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TermWsList) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TermWsList) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TermWsList))))) |
data NSPClauseBody Source #
a true boolean indicates the cnf
Instances
Eq NSPClauseBody Source # | |
Defined in SoftFOL.Sign (==) :: NSPClauseBody -> NSPClauseBody -> Bool (/=) :: NSPClauseBody -> NSPClauseBody -> Bool | |
Data NSPClauseBody Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NSPClauseBody -> c NSPClauseBody gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NSPClauseBody toConstr :: NSPClauseBody -> Constr dataTypeOf :: NSPClauseBody -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c NSPClauseBody) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NSPClauseBody) gmapT :: (forall b. Data b => b -> b) -> NSPClauseBody -> NSPClauseBody gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NSPClauseBody -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NSPClauseBody -> r gmapQ :: (forall d. Data d => d -> u) -> NSPClauseBody -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> NSPClauseBody -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> NSPClauseBody -> m NSPClauseBody gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NSPClauseBody -> m NSPClauseBody gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NSPClauseBody -> m NSPClauseBody | |
Ord NSPClauseBody Source # | |
Defined in SoftFOL.Sign compare :: NSPClauseBody -> NSPClauseBody -> Ordering (<) :: NSPClauseBody -> NSPClauseBody -> Bool (<=) :: NSPClauseBody -> NSPClauseBody -> Bool (>) :: NSPClauseBody -> NSPClauseBody -> Bool (>=) :: NSPClauseBody -> NSPClauseBody -> Bool max :: NSPClauseBody -> NSPClauseBody -> NSPClauseBody min :: NSPClauseBody -> NSPClauseBody -> NSPClauseBody | |
Show NSPClauseBody Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> NSPClauseBody -> ShowS show :: NSPClauseBody -> String showList :: [NSPClauseBody] -> ShowS | |
Generic NSPClauseBody | |
Defined in SoftFOL.ATC_SoftFOL type Rep NSPClauseBody :: Type -> Type from :: NSPClauseBody -> Rep NSPClauseBody x to :: Rep NSPClauseBody x -> NSPClauseBody | |
FromJSON NSPClauseBody | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser NSPClauseBody parseJSONList :: Value -> Parser [NSPClauseBody] | |
ToJSON NSPClauseBody | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: NSPClauseBody -> Value toEncoding :: NSPClauseBody -> Encoding toJSONList :: [NSPClauseBody] -> Value toEncodingList :: [NSPClauseBody] -> Encoding | |
ShATermConvertible NSPClauseBody | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> NSPClauseBody -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [NSPClauseBody] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, NSPClauseBody) fromShATermList' :: Int -> ATermTable -> (ATermTable, [NSPClauseBody]) | |
type Rep NSPClauseBody | |
Defined in SoftFOL.ATC_SoftFOL type Rep NSPClauseBody = D1 ('MetaData "NSPClauseBody" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "NSPClauseBody" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPClauseType) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPLiteral]))) |
data TermWsList Source #
Instances
Eq TermWsList Source # | |
Defined in SoftFOL.Sign (==) :: TermWsList -> TermWsList -> Bool (/=) :: TermWsList -> TermWsList -> Bool | |
Data TermWsList Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TermWsList -> c TermWsList gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TermWsList toConstr :: TermWsList -> Constr dataTypeOf :: TermWsList -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TermWsList) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TermWsList) gmapT :: (forall b. Data b => b -> b) -> TermWsList -> TermWsList gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TermWsList -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TermWsList -> r gmapQ :: (forall d. Data d => d -> u) -> TermWsList -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TermWsList -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TermWsList -> m TermWsList gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TermWsList -> m TermWsList gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TermWsList -> m TermWsList | |
Ord TermWsList Source # | |
Defined in SoftFOL.Sign compare :: TermWsList -> TermWsList -> Ordering (<) :: TermWsList -> TermWsList -> Bool (<=) :: TermWsList -> TermWsList -> Bool (>) :: TermWsList -> TermWsList -> Bool (>=) :: TermWsList -> TermWsList -> Bool max :: TermWsList -> TermWsList -> TermWsList min :: TermWsList -> TermWsList -> TermWsList | |
Show TermWsList Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> TermWsList -> ShowS show :: TermWsList -> String showList :: [TermWsList] -> ShowS | |
Generic TermWsList | |
Defined in SoftFOL.ATC_SoftFOL type Rep TermWsList :: Type -> Type from :: TermWsList -> Rep TermWsList x to :: Rep TermWsList x -> TermWsList | |
FromJSON TermWsList | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser TermWsList parseJSONList :: Value -> Parser [TermWsList] | |
ToJSON TermWsList | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: TermWsList -> Value toEncoding :: TermWsList -> Encoding toJSONList :: [TermWsList] -> Value toEncodingList :: [TermWsList] -> Encoding | |
ShATermConvertible TermWsList | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> TermWsList -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TermWsList] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TermWsList) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TermWsList]) | |
Pretty TermWsList Source # | |
Defined in SoftFOL.Print pretty :: TermWsList -> Doc Source # pretties :: [TermWsList] -> Doc Source # | |
type Rep TermWsList | |
Defined in SoftFOL.ATC_SoftFOL type Rep TermWsList = D1 ('MetaData "TermWsList" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "TWL" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPTerm]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) |
A SPASS Term.
Instances
FileName String |
Instances
Data FileName Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FileName -> c FileName gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FileName toConstr :: FileName -> Constr dataTypeOf :: FileName -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FileName) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FileName) gmapT :: (forall b. Data b => b -> b) -> FileName -> FileName gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FileName -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FileName -> r gmapQ :: (forall d. Data d => d -> u) -> FileName -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FileName -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FileName -> m FileName gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FileName -> m FileName gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FileName -> m FileName | |
Show FileName Source # | |
Generic FileName | |
FromJSON FileName | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser FileName parseJSONList :: Value -> Parser [FileName] | |
ToJSON FileName | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: FileName -> Encoding toJSONList :: [FileName] -> Value toEncodingList :: [FileName] -> Encoding | |
ShATermConvertible FileName | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> FileName -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FileName] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FileName) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FileName]) | |
type Rep FileName | |
Defined in SoftFOL.ATC_SoftFOL type Rep FileName = D1 ('MetaData "FileName" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "FileName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |
Instances
Data FormKind Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FormKind -> c FormKind gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FormKind toConstr :: FormKind -> Constr dataTypeOf :: FormKind -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FormKind) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FormKind) gmapT :: (forall b. Data b => b -> b) -> FormKind -> FormKind gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FormKind -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FormKind -> r gmapQ :: (forall d. Data d => d -> u) -> FormKind -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FormKind -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FormKind -> m FormKind gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FormKind -> m FormKind gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FormKind -> m FormKind | |
Show FormKind Source # | |
Generic FormKind | |
FromJSON FormKind | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser FormKind parseJSONList :: Value -> Parser [FormKind] | |
ToJSON FormKind | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: FormKind -> Encoding toJSONList :: [FormKind] -> Value toEncodingList :: [FormKind] -> Encoding | |
ShATermConvertible FormKind | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> FormKind -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FormKind] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FormKind) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FormKind]) | |
type Rep FormKind | |
Defined in SoftFOL.ATC_SoftFOL type Rep FormKind = D1 ('MetaData "FormKind" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "FofKind" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CnfKind" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FotKind" 'PrefixI 'False) (U1 :: Type -> Type))) |
Axiom | |
Hypothesis | |
Definition | |
Assumption | |
Lemma | |
Theorem | |
Conjecture | |
Negated_conjecture | |
Plain | |
Fi_domain | |
Fi_functors | |
Fi_predicates | |
Type | |
Unknown |
Instances
Data Role Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role dataTypeOf :: Role -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Role) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role) gmapT :: (forall b. Data b => b -> b) -> Role -> Role gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r gmapQ :: (forall d. Data d => d -> u) -> Role -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Role -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Role -> m Role gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role | |
Show Role Source # | |
Generic Role | |
FromJSON Role | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser Role parseJSONList :: Value -> Parser [Role] | |
ToJSON Role | |
Defined in SoftFOL.ATC_SoftFOL | |
ShATermConvertible Role | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> Role -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Role] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Role) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Role]) | |
type Rep Role | |
Defined in SoftFOL.ATC_SoftFOL type Rep Role = D1 ('MetaData "Role" "SoftFOL.Sign" "main" 'False) (((C1 ('MetaCons "Axiom" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Hypothesis" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Definition" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Assumption" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Lemma" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Theorem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Conjecture" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Negated_conjecture" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Plain" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Fi_domain" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Fi_functors" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Fi_predicates" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Type" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Unknown" 'PrefixI 'False) (U1 :: Type -> Type))))) |
Name String |
Instances
Data Name Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Name -> c Name gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Name dataTypeOf :: Name -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Name) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name) gmapT :: (forall b. Data b => b -> b) -> Name -> Name gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r gmapQ :: (forall d. Data d => d -> u) -> Name -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Name -> m Name gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Name -> m Name | |
Show Name Source # | |
Generic Name | |
FromJSON Name | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser Name parseJSONList :: Value -> Parser [Name] | |
ToJSON Name | |
Defined in SoftFOL.ATC_SoftFOL | |
ShATermConvertible Name | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> Name -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Name] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Name) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Name]) | |
type Rep Name | |
Defined in SoftFOL.ATC_SoftFOL type Rep Name = D1 ('MetaData "Name" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "Name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |
Instances
Data Annos Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Annos -> c Annos gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Annos dataTypeOf :: Annos -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Annos) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annos) gmapT :: (forall b. Data b => b -> b) -> Annos -> Annos gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Annos -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Annos -> r gmapQ :: (forall d. Data d => d -> u) -> Annos -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Annos -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Annos -> m Annos gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Annos -> m Annos gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Annos -> m Annos | |
Show Annos Source # | |
Generic Annos | |
FromJSON Annos | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser Annos parseJSONList :: Value -> Parser [Annos] | |
ToJSON Annos | |
Defined in SoftFOL.ATC_SoftFOL | |
ShATermConvertible Annos | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> Annos -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Annos] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Annos) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Annos]) | |
type Rep Annos | |
Defined in SoftFOL.ATC_SoftFOL type Rep Annos = D1 ('MetaData "Annos" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "Annos" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Source) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Info)))) |
Instances
Data Source Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Source -> c Source gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Source dataTypeOf :: Source -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Source) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Source) gmapT :: (forall b. Data b => b -> b) -> Source -> Source gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Source -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Source -> r gmapQ :: (forall d. Data d => d -> u) -> Source -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Source -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Source -> m Source gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Source -> m Source gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Source -> m Source | |
Show Source Source # | |
Generic Source | |
FromJSON Source | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser Source parseJSONList :: Value -> Parser [Source] | |
ToJSON Source | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: Source -> Encoding toJSONList :: [Source] -> Value toEncodingList :: [Source] -> Encoding | |
ShATermConvertible Source | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> Source -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Source] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Source) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Source]) | |
type Rep Source | |
Defined in SoftFOL.ATC_SoftFOL |
AWord String |
Instances
Data AWord Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AWord -> c AWord gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AWord dataTypeOf :: AWord -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AWord) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AWord) gmapT :: (forall b. Data b => b -> b) -> AWord -> AWord gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AWord -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AWord -> r gmapQ :: (forall d. Data d => d -> u) -> AWord -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> AWord -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> AWord -> m AWord gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AWord -> m AWord gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AWord -> m AWord | |
Show AWord Source # | |
Generic AWord | |
FromJSON AWord | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser AWord parseJSONList :: Value -> Parser [AWord] | |
ToJSON AWord | |
Defined in SoftFOL.ATC_SoftFOL | |
ShATermConvertible AWord | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> AWord -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [AWord] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, AWord) fromShATermList' :: Int -> ATermTable -> (ATermTable, [AWord]) | |
type Rep AWord | |
Defined in SoftFOL.ATC_SoftFOL type Rep AWord = D1 ('MetaData "AWord" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "AWord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |
GenTerm GenData (Maybe GenTerm) | |
GenTermList [GenTerm] |
Instances
Data GenTerm Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GenTerm -> c GenTerm gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GenTerm dataTypeOf :: GenTerm -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GenTerm) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GenTerm) gmapT :: (forall b. Data b => b -> b) -> GenTerm -> GenTerm gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GenTerm -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GenTerm -> r gmapQ :: (forall d. Data d => d -> u) -> GenTerm -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> GenTerm -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> GenTerm -> m GenTerm gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GenTerm -> m GenTerm gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GenTerm -> m GenTerm | |
Show GenTerm Source # | |
Generic GenTerm | |
FromJSON GenTerm | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser GenTerm parseJSONList :: Value -> Parser [GenTerm] | |
ToJSON GenTerm | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: GenTerm -> Encoding toJSONList :: [GenTerm] -> Value toEncodingList :: [GenTerm] -> Encoding | |
ShATermConvertible GenTerm | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> GenTerm -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [GenTerm] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, GenTerm) fromShATermList' :: Int -> ATermTable -> (ATermTable, [GenTerm]) | |
type Rep GenTerm | |
Defined in SoftFOL.ATC_SoftFOL type Rep GenTerm = D1 ('MetaData "GenTerm" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "GenTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GenData) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe GenTerm))) :+: C1 ('MetaCons "GenTermList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GenTerm]))) |
GenData AWord [GenTerm] | |
OtherGenData String | |
GenFormData FormData |
Instances
Data GenData Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GenData -> c GenData gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GenData dataTypeOf :: GenData -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GenData) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GenData) gmapT :: (forall b. Data b => b -> b) -> GenData -> GenData gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GenData -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GenData -> r gmapQ :: (forall d. Data d => d -> u) -> GenData -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> GenData -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> GenData -> m GenData gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GenData -> m GenData gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GenData -> m GenData | |
Show GenData Source # | |
Generic GenData | |
FromJSON GenData | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser GenData parseJSONList :: Value -> Parser [GenData] | |
ToJSON GenData | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: GenData -> Encoding toJSONList :: [GenData] -> Value toEncodingList :: [GenData] -> Encoding | |
ShATermConvertible GenData | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> GenData -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [GenData] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, GenData) fromShATermList' :: Int -> ATermTable -> (ATermTable, [GenData]) | |
type Rep GenData | |
Defined in SoftFOL.ATC_SoftFOL type Rep GenData = D1 ('MetaData "GenData" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "GenData" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 AWord) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GenTerm])) :+: (C1 ('MetaCons "OtherGenData" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "GenFormData" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FormData)))) |
Instances
Data FormData Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FormData -> c FormData gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FormData toConstr :: FormData -> Constr dataTypeOf :: FormData -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FormData) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FormData) gmapT :: (forall b. Data b => b -> b) -> FormData -> FormData gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FormData -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FormData -> r gmapQ :: (forall d. Data d => d -> u) -> FormData -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> FormData -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> FormData -> m FormData gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FormData -> m FormData gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FormData -> m FormData | |
Show FormData Source # | |
Generic FormData | |
FromJSON FormData | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser FormData parseJSONList :: Value -> Parser [FormData] | |
ToJSON FormData | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: FormData -> Encoding toJSONList :: [FormData] -> Value toEncodingList :: [FormData] -> Encoding | |
ShATermConvertible FormData | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> FormData -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [FormData] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, FormData) fromShATermList' :: Int -> ATermTable -> (ATermTable, [FormData]) | |
type Rep FormData | |
Defined in SoftFOL.ATC_SoftFOL type Rep FormData = D1 ('MetaData "FormData" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "FormData" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FormKind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPTerm))) |
Instances
Data Info Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Info -> c Info gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Info dataTypeOf :: Info -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Info) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Info) gmapT :: (forall b. Data b => b -> b) -> Info -> Info gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Info -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Info -> r gmapQ :: (forall d. Data d => d -> u) -> Info -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Info -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Info -> m Info gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Info -> m Info gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Info -> m Info | |
Show Info Source # | |
Generic Info | |
FromJSON Info | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser Info parseJSONList :: Value -> Parser [Info] | |
ToJSON Info | |
Defined in SoftFOL.ATC_SoftFOL | |
ShATermConvertible Info | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> Info -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Info] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Info) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Info]) | |
type Rep Info | |
Defined in SoftFOL.ATC_SoftFOL |
FormAnno FormKind Name Role SPTerm (Maybe Annos) | |
Include FileName [Name] | |
CommentLine String | |
EmptyLine |
Instances
Literals for SPASS CNF and DNF (the boolean indicates a negated literal).
Instances
Eq SPLiteral Source # | |
Data SPLiteral Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPLiteral -> c SPLiteral gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPLiteral toConstr :: SPLiteral -> Constr dataTypeOf :: SPLiteral -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPLiteral) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPLiteral) gmapT :: (forall b. Data b => b -> b) -> SPLiteral -> SPLiteral gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPLiteral -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPLiteral -> r gmapQ :: (forall d. Data d => d -> u) -> SPLiteral -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPLiteral -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPLiteral -> m SPLiteral gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPLiteral -> m SPLiteral gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPLiteral -> m SPLiteral | |
Ord SPLiteral Source # | |
Defined in SoftFOL.Sign | |
Show SPLiteral Source # | |
Generic SPLiteral | |
FromJSON SPLiteral | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPLiteral parseJSONList :: Value -> Parser [SPLiteral] | |
ToJSON SPLiteral | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: SPLiteral -> Encoding toJSONList :: [SPLiteral] -> Value toEncodingList :: [SPLiteral] -> Encoding | |
ShATermConvertible SPLiteral | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPLiteral -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPLiteral] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPLiteral) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPLiteral]) | |
type Rep SPLiteral | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPLiteral = D1 ('MetaData "SPLiteral" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPLiteral" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPSymbol))) |
data SPQuantSym Source #
SPASS Quantifier Symbols.
Instances
Eq SPQuantSym Source # | |
Defined in SoftFOL.Sign (==) :: SPQuantSym -> SPQuantSym -> Bool (/=) :: SPQuantSym -> SPQuantSym -> Bool | |
Data SPQuantSym Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPQuantSym -> c SPQuantSym gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPQuantSym toConstr :: SPQuantSym -> Constr dataTypeOf :: SPQuantSym -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPQuantSym) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPQuantSym) gmapT :: (forall b. Data b => b -> b) -> SPQuantSym -> SPQuantSym gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPQuantSym -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPQuantSym -> r gmapQ :: (forall d. Data d => d -> u) -> SPQuantSym -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPQuantSym -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPQuantSym -> m SPQuantSym gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPQuantSym -> m SPQuantSym gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPQuantSym -> m SPQuantSym | |
Ord SPQuantSym Source # | |
Defined in SoftFOL.Sign compare :: SPQuantSym -> SPQuantSym -> Ordering (<) :: SPQuantSym -> SPQuantSym -> Bool (<=) :: SPQuantSym -> SPQuantSym -> Bool (>) :: SPQuantSym -> SPQuantSym -> Bool (>=) :: SPQuantSym -> SPQuantSym -> Bool max :: SPQuantSym -> SPQuantSym -> SPQuantSym min :: SPQuantSym -> SPQuantSym -> SPQuantSym | |
Show SPQuantSym Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPQuantSym -> ShowS show :: SPQuantSym -> String showList :: [SPQuantSym] -> ShowS | |
Generic SPQuantSym | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPQuantSym :: Type -> Type from :: SPQuantSym -> Rep SPQuantSym x to :: Rep SPQuantSym x -> SPQuantSym | |
FromJSON SPQuantSym | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPQuantSym parseJSONList :: Value -> Parser [SPQuantSym] | |
ToJSON SPQuantSym | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPQuantSym -> Value toEncoding :: SPQuantSym -> Encoding toJSONList :: [SPQuantSym] -> Value toEncodingList :: [SPQuantSym] -> Encoding | |
ShATermConvertible SPQuantSym | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPQuantSym -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPQuantSym] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPQuantSym) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPQuantSym]) | |
Pretty SPQuantSym Source # | Creates a Doc from a SPASS Quantifier Symbol. |
Defined in SoftFOL.Print pretty :: SPQuantSym -> Doc Source # pretties :: [SPQuantSym] -> Doc Source # | |
PrintTPTP SPQuantSym Source # | Creates a Doc from a SoftFOL Quantifier Symbol. |
Defined in SoftFOL.PrintTPTP printTPTP :: SPQuantSym -> Doc Source # | |
type Rep SPQuantSym | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPQuantSym = D1 ('MetaData "SPQuantSym" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPForall" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SPExists" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SPCustomQuantSym" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPIdentifier)))) |
SPASS Symbols.
SPEqual | |
SPTrue | |
SPFalse | |
SPOr | |
SPAnd | |
SPNot | |
SPImplies | |
SPImplied | |
SPEquiv | |
SPID | |
SPDiv | |
SPComp | |
SPSum | |
SPConv | |
SPCustomSymbol SPIdentifier |
Instances
Eq SPSymbol Source # | |
Data SPSymbol Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPSymbol -> c SPSymbol gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPSymbol toConstr :: SPSymbol -> Constr dataTypeOf :: SPSymbol -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPSymbol) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPSymbol) gmapT :: (forall b. Data b => b -> b) -> SPSymbol -> SPSymbol gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPSymbol -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPSymbol -> r gmapQ :: (forall d. Data d => d -> u) -> SPSymbol -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPSymbol -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPSymbol -> m SPSymbol gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSymbol -> m SPSymbol gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSymbol -> m SPSymbol | |
Ord SPSymbol Source # | |
Show SPSymbol Source # | |
Generic SPSymbol | |
FromJSON SPSymbol | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPSymbol parseJSONList :: Value -> Parser [SPSymbol] | |
ToJSON SPSymbol | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: SPSymbol -> Encoding toJSONList :: [SPSymbol] -> Value toEncodingList :: [SPSymbol] -> Encoding | |
ShATermConvertible SPSymbol | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPSymbol -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPSymbol] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSymbol) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPSymbol]) | |
Pretty SPSymbol Source # | Creates a Doc from a SPASS Symbol. printSymbol :: SPSymbol-> Doc |
PrintTPTP SPSymbol Source # | Creates a Doc from a SoftFOL Symbol. |
type Rep SPSymbol | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPSymbol = D1 ('MetaData "SPSymbol" "SoftFOL.Sign" "main" 'False) (((C1 ('MetaCons "SPEqual" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SPTrue" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SPFalse" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "SPOr" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SPAnd" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SPNot" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SPImplies" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "SPImplied" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SPEquiv" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SPID" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SPDiv" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "SPComp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SPSum" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SPConv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SPCustomSymbol" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPIdentifier)))))) |
mkSPCustomSymbol :: String -> SPSymbol Source #
showSPSymbol :: SPSymbol -> String Source #
Proof List
data SPProofList Source #
SPASS Proof List
SPProofList | |
|
Instances
Eq SPProofList Source # | |
Defined in SoftFOL.Sign (==) :: SPProofList -> SPProofList -> Bool (/=) :: SPProofList -> SPProofList -> Bool | |
Data SPProofList Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPProofList -> c SPProofList gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPProofList toConstr :: SPProofList -> Constr dataTypeOf :: SPProofList -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPProofList) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPProofList) gmapT :: (forall b. Data b => b -> b) -> SPProofList -> SPProofList gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPProofList -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPProofList -> r gmapQ :: (forall d. Data d => d -> u) -> SPProofList -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPProofList -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPProofList -> m SPProofList gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPProofList -> m SPProofList gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPProofList -> m SPProofList | |
Ord SPProofList Source # | |
Defined in SoftFOL.Sign compare :: SPProofList -> SPProofList -> Ordering (<) :: SPProofList -> SPProofList -> Bool (<=) :: SPProofList -> SPProofList -> Bool (>) :: SPProofList -> SPProofList -> Bool (>=) :: SPProofList -> SPProofList -> Bool max :: SPProofList -> SPProofList -> SPProofList min :: SPProofList -> SPProofList -> SPProofList | |
Show SPProofList Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPProofList -> ShowS show :: SPProofList -> String showList :: [SPProofList] -> ShowS | |
Generic SPProofList | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPProofList :: Type -> Type from :: SPProofList -> Rep SPProofList x to :: Rep SPProofList x -> SPProofList | |
FromJSON SPProofList | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPProofList parseJSONList :: Value -> Parser [SPProofList] | |
ToJSON SPProofList | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPProofList -> Value toEncoding :: SPProofList -> Encoding toJSONList :: [SPProofList] -> Value toEncodingList :: [SPProofList] -> Encoding | |
ShATermConvertible SPProofList | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPProofList -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPProofList] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPProofList) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPProofList]) | |
Pretty SPProofList Source # | |
Defined in SoftFOL.Print pretty :: SPProofList -> Doc Source # pretties :: [SPProofList] -> Doc Source # | |
type Rep SPProofList | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPProofList = D1 ('MetaData "SPProofList" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPProofList" 'PrefixI 'True) (S1 ('MetaSel ('Just "proofType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe SPProofType)) :*: (S1 ('MetaSel ('Just "plAssocList") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPAssocList) :*: S1 ('MetaSel ('Just "step") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPProofStep])))) |
type SPProofType = SPIdentifier Source #
data SPProofStep Source #
SPProofStep | |
|
Instances
Eq SPProofStep Source # | |
Defined in SoftFOL.Sign (==) :: SPProofStep -> SPProofStep -> Bool (/=) :: SPProofStep -> SPProofStep -> Bool | |
Data SPProofStep Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPProofStep -> c SPProofStep gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPProofStep toConstr :: SPProofStep -> Constr dataTypeOf :: SPProofStep -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPProofStep) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPProofStep) gmapT :: (forall b. Data b => b -> b) -> SPProofStep -> SPProofStep gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPProofStep -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPProofStep -> r gmapQ :: (forall d. Data d => d -> u) -> SPProofStep -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPProofStep -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPProofStep -> m SPProofStep gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPProofStep -> m SPProofStep gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPProofStep -> m SPProofStep | |
Ord SPProofStep Source # | |
Defined in SoftFOL.Sign compare :: SPProofStep -> SPProofStep -> Ordering (<) :: SPProofStep -> SPProofStep -> Bool (<=) :: SPProofStep -> SPProofStep -> Bool (>) :: SPProofStep -> SPProofStep -> Bool (>=) :: SPProofStep -> SPProofStep -> Bool max :: SPProofStep -> SPProofStep -> SPProofStep min :: SPProofStep -> SPProofStep -> SPProofStep | |
Show SPProofStep Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPProofStep -> ShowS show :: SPProofStep -> String showList :: [SPProofStep] -> ShowS | |
Generic SPProofStep | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPProofStep :: Type -> Type from :: SPProofStep -> Rep SPProofStep x to :: Rep SPProofStep x -> SPProofStep | |
FromJSON SPProofStep | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPProofStep parseJSONList :: Value -> Parser [SPProofStep] | |
ToJSON SPProofStep | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPProofStep -> Value toEncoding :: SPProofStep -> Encoding toJSONList :: [SPProofStep] -> Value toEncodingList :: [SPProofStep] -> Encoding | |
ShATermConvertible SPProofStep | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPProofStep -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPProofStep] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPProofStep) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPProofStep]) | |
type Rep SPProofStep | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPProofStep = D1 ('MetaData "SPProofStep" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPProofStep" 'PrefixI 'True) ((S1 ('MetaSel ('Just "reference") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPReference) :*: S1 ('MetaSel ('Just "result") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPResult)) :*: (S1 ('MetaSel ('Just "ruleAppl") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPRuleAppl) :*: (S1 ('MetaSel ('Just "parentList") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPParent]) :*: S1 ('MetaSel ('Just "stepAssocList") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPAssocList))))) |
data SPReference Source #
Instances
Eq SPReference Source # | |
Defined in SoftFOL.Sign (==) :: SPReference -> SPReference -> Bool (/=) :: SPReference -> SPReference -> Bool | |
Data SPReference Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPReference -> c SPReference gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPReference toConstr :: SPReference -> Constr dataTypeOf :: SPReference -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPReference) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPReference) gmapT :: (forall b. Data b => b -> b) -> SPReference -> SPReference gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPReference -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPReference -> r gmapQ :: (forall d. Data d => d -> u) -> SPReference -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPReference -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPReference -> m SPReference gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPReference -> m SPReference gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPReference -> m SPReference | |
Ord SPReference Source # | |
Defined in SoftFOL.Sign compare :: SPReference -> SPReference -> Ordering (<) :: SPReference -> SPReference -> Bool (<=) :: SPReference -> SPReference -> Bool (>) :: SPReference -> SPReference -> Bool (>=) :: SPReference -> SPReference -> Bool max :: SPReference -> SPReference -> SPReference min :: SPReference -> SPReference -> SPReference | |
Show SPReference Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPReference -> ShowS show :: SPReference -> String showList :: [SPReference] -> ShowS | |
Generic SPReference | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPReference :: Type -> Type from :: SPReference -> Rep SPReference x to :: Rep SPReference x -> SPReference | |
FromJSON SPReference | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPReference parseJSONList :: Value -> Parser [SPReference] | |
ToJSON SPReference | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPReference -> Value toEncoding :: SPReference -> Encoding toJSONList :: [SPReference] -> Value toEncodingList :: [SPReference] -> Encoding | |
ShATermConvertible SPReference | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPReference -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPReference] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPReference) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPReference]) | |
Pretty SPReference Source # | |
Defined in SoftFOL.Print pretty :: SPReference -> Doc Source # pretties :: [SPReference] -> Doc Source # | |
type Rep SPReference | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPReference = D1 ('MetaData "SPReference" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "PRefTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPTerm))) |
Instances
Eq SPResult Source # | |
Data SPResult Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPResult -> c SPResult gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPResult toConstr :: SPResult -> Constr dataTypeOf :: SPResult -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPResult) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPResult) gmapT :: (forall b. Data b => b -> b) -> SPResult -> SPResult gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPResult -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPResult -> r gmapQ :: (forall d. Data d => d -> u) -> SPResult -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPResult -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPResult -> m SPResult gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPResult -> m SPResult gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPResult -> m SPResult | |
Ord SPResult Source # | |
Show SPResult Source # | |
Generic SPResult | |
FromJSON SPResult | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPResult parseJSONList :: Value -> Parser [SPResult] | |
ToJSON SPResult | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: SPResult -> Encoding toJSONList :: [SPResult] -> Value toEncodingList :: [SPResult] -> Encoding | |
ShATermConvertible SPResult | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPResult -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPResult] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPResult) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPResult]) | |
Pretty SPResult Source # | |
type Rep SPResult | |
Defined in SoftFOL.ATC_SoftFOL |
data SPRuleAppl Source #
Instances
Eq SPRuleAppl Source # | |
Defined in SoftFOL.Sign (==) :: SPRuleAppl -> SPRuleAppl -> Bool (/=) :: SPRuleAppl -> SPRuleAppl -> Bool | |
Data SPRuleAppl Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPRuleAppl -> c SPRuleAppl gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPRuleAppl toConstr :: SPRuleAppl -> Constr dataTypeOf :: SPRuleAppl -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPRuleAppl) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPRuleAppl) gmapT :: (forall b. Data b => b -> b) -> SPRuleAppl -> SPRuleAppl gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPRuleAppl -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPRuleAppl -> r gmapQ :: (forall d. Data d => d -> u) -> SPRuleAppl -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPRuleAppl -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPRuleAppl -> m SPRuleAppl gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPRuleAppl -> m SPRuleAppl gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPRuleAppl -> m SPRuleAppl | |
Ord SPRuleAppl Source # | |
Defined in SoftFOL.Sign compare :: SPRuleAppl -> SPRuleAppl -> Ordering (<) :: SPRuleAppl -> SPRuleAppl -> Bool (<=) :: SPRuleAppl -> SPRuleAppl -> Bool (>) :: SPRuleAppl -> SPRuleAppl -> Bool (>=) :: SPRuleAppl -> SPRuleAppl -> Bool max :: SPRuleAppl -> SPRuleAppl -> SPRuleAppl min :: SPRuleAppl -> SPRuleAppl -> SPRuleAppl | |
Show SPRuleAppl Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPRuleAppl -> ShowS show :: SPRuleAppl -> String showList :: [SPRuleAppl] -> ShowS | |
Generic SPRuleAppl | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPRuleAppl :: Type -> Type from :: SPRuleAppl -> Rep SPRuleAppl x to :: Rep SPRuleAppl x -> SPRuleAppl | |
FromJSON SPRuleAppl | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPRuleAppl parseJSONList :: Value -> Parser [SPRuleAppl] | |
ToJSON SPRuleAppl | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPRuleAppl -> Value toEncoding :: SPRuleAppl -> Encoding toJSONList :: [SPRuleAppl] -> Value toEncodingList :: [SPRuleAppl] -> Encoding | |
ShATermConvertible SPRuleAppl | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPRuleAppl -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPRuleAppl] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPRuleAppl) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPRuleAppl]) | |
Pretty SPRuleAppl Source # | |
Defined in SoftFOL.Print pretty :: SPRuleAppl -> Doc Source # pretties :: [SPRuleAppl] -> Doc Source # | |
type Rep SPRuleAppl | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPRuleAppl = D1 ('MetaData "SPRuleAppl" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "PRuleTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPTerm)) :+: C1 ('MetaCons "PRuleUser" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPUserRuleAppl))) |
data SPUserRuleAppl Source #
Instances
Eq SPUserRuleAppl Source # | |
Defined in SoftFOL.Sign (==) :: SPUserRuleAppl -> SPUserRuleAppl -> Bool (/=) :: SPUserRuleAppl -> SPUserRuleAppl -> Bool | |
Data SPUserRuleAppl Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPUserRuleAppl -> c SPUserRuleAppl gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPUserRuleAppl toConstr :: SPUserRuleAppl -> Constr dataTypeOf :: SPUserRuleAppl -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPUserRuleAppl) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPUserRuleAppl) gmapT :: (forall b. Data b => b -> b) -> SPUserRuleAppl -> SPUserRuleAppl gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPUserRuleAppl -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPUserRuleAppl -> r gmapQ :: (forall d. Data d => d -> u) -> SPUserRuleAppl -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPUserRuleAppl -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPUserRuleAppl -> m SPUserRuleAppl gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPUserRuleAppl -> m SPUserRuleAppl gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPUserRuleAppl -> m SPUserRuleAppl | |
Ord SPUserRuleAppl Source # | |
Defined in SoftFOL.Sign compare :: SPUserRuleAppl -> SPUserRuleAppl -> Ordering (<) :: SPUserRuleAppl -> SPUserRuleAppl -> Bool (<=) :: SPUserRuleAppl -> SPUserRuleAppl -> Bool (>) :: SPUserRuleAppl -> SPUserRuleAppl -> Bool (>=) :: SPUserRuleAppl -> SPUserRuleAppl -> Bool max :: SPUserRuleAppl -> SPUserRuleAppl -> SPUserRuleAppl min :: SPUserRuleAppl -> SPUserRuleAppl -> SPUserRuleAppl | |
Show SPUserRuleAppl Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPUserRuleAppl -> ShowS show :: SPUserRuleAppl -> String showList :: [SPUserRuleAppl] -> ShowS | |
Generic SPUserRuleAppl | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPUserRuleAppl :: Type -> Type from :: SPUserRuleAppl -> Rep SPUserRuleAppl x to :: Rep SPUserRuleAppl x -> SPUserRuleAppl | |
FromJSON SPUserRuleAppl | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPUserRuleAppl parseJSONList :: Value -> Parser [SPUserRuleAppl] | |
ToJSON SPUserRuleAppl | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPUserRuleAppl -> Value toEncoding :: SPUserRuleAppl -> Encoding toJSONList :: [SPUserRuleAppl] -> Value toEncodingList :: [SPUserRuleAppl] -> Encoding | |
ShATermConvertible SPUserRuleAppl | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPUserRuleAppl -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPUserRuleAppl] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPUserRuleAppl) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPUserRuleAppl]) | |
Pretty SPUserRuleAppl Source # | |
Defined in SoftFOL.Print pretty :: SPUserRuleAppl -> Doc Source # pretties :: [SPUserRuleAppl] -> Doc Source # | |
type Rep SPUserRuleAppl | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPUserRuleAppl = D1 ('MetaData "SPUserRuleAppl" "SoftFOL.Sign" "main" 'False) ((((C1 ('MetaCons "GeR" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SpL" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SpR" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "EqF" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Rew" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Obv" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "EmS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SoR" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "EqR" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Mpm" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SPm" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OPm" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "SHy" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "OHy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "URR" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Fac" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Spt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Inp" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Con" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RRE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SSi" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "ClR" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UnC" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Ter" 'PrefixI 'False) (U1 :: Type -> Type)))))) |
Instances
Eq SPParent Source # | |
Data SPParent Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPParent -> c SPParent gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPParent toConstr :: SPParent -> Constr dataTypeOf :: SPParent -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPParent) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPParent) gmapT :: (forall b. Data b => b -> b) -> SPParent -> SPParent gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPParent -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPParent -> r gmapQ :: (forall d. Data d => d -> u) -> SPParent -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPParent -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPParent -> m SPParent gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPParent -> m SPParent gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPParent -> m SPParent | |
Ord SPParent Source # | |
Show SPParent Source # | |
Generic SPParent | |
FromJSON SPParent | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPParent parseJSONList :: Value -> Parser [SPParent] | |
ToJSON SPParent | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: SPParent -> Encoding toJSONList :: [SPParent] -> Value toEncodingList :: [SPParent] -> Encoding | |
ShATermConvertible SPParent | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPParent -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPParent] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPParent) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPParent]) | |
Pretty SPParent Source # | |
type Rep SPParent | |
Defined in SoftFOL.ATC_SoftFOL |
type SPAssocList = Map SPKey SPValue Source #
Instances
Eq SPKey Source # | |
Data SPKey Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPKey -> c SPKey gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPKey dataTypeOf :: SPKey -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPKey) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPKey) gmapT :: (forall b. Data b => b -> b) -> SPKey -> SPKey gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPKey -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPKey -> r gmapQ :: (forall d. Data d => d -> u) -> SPKey -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPKey -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPKey -> m SPKey gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPKey -> m SPKey gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPKey -> m SPKey | |
Ord SPKey Source # | |
Show SPKey Source # | |
Generic SPKey | |
FromJSON SPKey | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPKey parseJSONList :: Value -> Parser [SPKey] | |
ToJSON SPKey | |
Defined in SoftFOL.ATC_SoftFOL | |
ShATermConvertible SPKey | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPKey -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPKey] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPKey) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPKey]) | |
Pretty SPKey Source # | |
type Rep SPKey | |
Defined in SoftFOL.ATC_SoftFOL |
Instances
Eq SPValue Source # | |
Data SPValue Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPValue -> c SPValue gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPValue dataTypeOf :: SPValue -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPValue) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPValue) gmapT :: (forall b. Data b => b -> b) -> SPValue -> SPValue gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPValue -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPValue -> r gmapQ :: (forall d. Data d => d -> u) -> SPValue -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPValue -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPValue -> m SPValue gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPValue -> m SPValue gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPValue -> m SPValue | |
Ord SPValue Source # | |
Show SPValue Source # | |
Generic SPValue | |
FromJSON SPValue | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPValue parseJSONList :: Value -> Parser [SPValue] | |
ToJSON SPValue | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: SPValue -> Encoding toJSONList :: [SPValue] -> Value toEncodingList :: [SPValue] -> Encoding | |
ShATermConvertible SPValue | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPValue -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPValue] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPValue) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPValue]) | |
Pretty SPValue Source # | |
type Rep SPValue | |
Defined in SoftFOL.ATC_SoftFOL |
Formulae And Terms
type SPFormula = Named SPTerm Source #
A SPASS Formula is modelled as a Named SPTerm for now. This doesn't reflect the fact that the SPASS syntax lists both term and label as optional.
helpers for generating SoftFOL formulas
:: SPIdentifier | Variable symbol: v |
-> SPIdentifier | Sort symbol: s |
-> SPTerm | Term: s(v) |
spTerms :: [SPIdentifier] -> [SPTerm] Source #
spSym :: SPIdentifier -> SPSymbol Source #
SPASS Desciptions
data SPDescription Source #
A description is mandatory for a SPASS problem. It has to specify
at least a name
, the name of the author
, the status
(see also
SPLogState
below), and a (verbose) description.
Instances
Eq SPDescription Source # | |
Defined in SoftFOL.Sign (==) :: SPDescription -> SPDescription -> Bool (/=) :: SPDescription -> SPDescription -> Bool | |
Data SPDescription Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPDescription -> c SPDescription gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPDescription toConstr :: SPDescription -> Constr dataTypeOf :: SPDescription -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPDescription) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPDescription) gmapT :: (forall b. Data b => b -> b) -> SPDescription -> SPDescription gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPDescription -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPDescription -> r gmapQ :: (forall d. Data d => d -> u) -> SPDescription -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPDescription -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPDescription -> m SPDescription gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPDescription -> m SPDescription gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPDescription -> m SPDescription | |
Ord SPDescription Source # | |
Defined in SoftFOL.Sign compare :: SPDescription -> SPDescription -> Ordering (<) :: SPDescription -> SPDescription -> Bool (<=) :: SPDescription -> SPDescription -> Bool (>) :: SPDescription -> SPDescription -> Bool (>=) :: SPDescription -> SPDescription -> Bool max :: SPDescription -> SPDescription -> SPDescription min :: SPDescription -> SPDescription -> SPDescription | |
Show SPDescription Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPDescription -> ShowS show :: SPDescription -> String showList :: [SPDescription] -> ShowS | |
Generic SPDescription | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPDescription :: Type -> Type from :: SPDescription -> Rep SPDescription x to :: Rep SPDescription x -> SPDescription | |
FromJSON SPDescription | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPDescription parseJSONList :: Value -> Parser [SPDescription] | |
ToJSON SPDescription | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPDescription -> Value toEncoding :: SPDescription -> Encoding toJSONList :: [SPDescription] -> Value toEncodingList :: [SPDescription] -> Encoding | |
ShATermConvertible SPDescription | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPDescription -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPDescription] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPDescription) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPDescription]) | |
Pretty SPDescription Source # | Creates a Doc from a SPASS description. |
Defined in SoftFOL.Print pretty :: SPDescription -> Doc Source # pretties :: [SPDescription] -> Doc Source # | |
PrintTPTP SPDescription Source # | Creates a Doc from a SoftFOL description. |
Defined in SoftFOL.PrintTPTP printTPTP :: SPDescription -> Doc Source # | |
type Rep SPDescription | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPDescription = D1 ('MetaData "SPDescription" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPDescription" 'PrefixI 'True) ((S1 ('MetaSel ('Just "name") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "author") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "version") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))) :*: ((S1 ('MetaSel ('Just "logic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)) :*: S1 ('MetaSel ('Just "status") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPLogState)) :*: (S1 ('MetaSel ('Just "desc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "date") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))))) |
data SPLogState Source #
The state of a SPASS problem can be satisfiable, unsatisfiable, or unknown.
Instances
Eq SPLogState Source # | |
Defined in SoftFOL.Sign (==) :: SPLogState -> SPLogState -> Bool (/=) :: SPLogState -> SPLogState -> Bool | |
Data SPLogState Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPLogState -> c SPLogState gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPLogState toConstr :: SPLogState -> Constr dataTypeOf :: SPLogState -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPLogState) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPLogState) gmapT :: (forall b. Data b => b -> b) -> SPLogState -> SPLogState gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPLogState -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPLogState -> r gmapQ :: (forall d. Data d => d -> u) -> SPLogState -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPLogState -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPLogState -> m SPLogState gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPLogState -> m SPLogState gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPLogState -> m SPLogState | |
Ord SPLogState Source # | |
Defined in SoftFOL.Sign compare :: SPLogState -> SPLogState -> Ordering (<) :: SPLogState -> SPLogState -> Bool (<=) :: SPLogState -> SPLogState -> Bool (>) :: SPLogState -> SPLogState -> Bool (>=) :: SPLogState -> SPLogState -> Bool max :: SPLogState -> SPLogState -> SPLogState min :: SPLogState -> SPLogState -> SPLogState | |
Show SPLogState Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPLogState -> ShowS show :: SPLogState -> String showList :: [SPLogState] -> ShowS | |
Generic SPLogState | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPLogState :: Type -> Type from :: SPLogState -> Rep SPLogState x to :: Rep SPLogState x -> SPLogState | |
FromJSON SPLogState | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPLogState parseJSONList :: Value -> Parser [SPLogState] | |
ToJSON SPLogState | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPLogState -> Value toEncoding :: SPLogState -> Encoding toJSONList :: [SPLogState] -> Value toEncodingList :: [SPLogState] -> Encoding | |
ShATermConvertible SPLogState | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPLogState -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPLogState] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPLogState) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPLogState]) | |
Pretty SPLogState Source # | Creates a Doc from an |
Defined in SoftFOL.Print pretty :: SPLogState -> Doc Source # pretties :: [SPLogState] -> Doc Source # | |
PrintTPTP SPLogState Source # | Creates a Doc from an |
Defined in SoftFOL.PrintTPTP printTPTP :: SPLogState -> Doc Source # | |
type Rep SPLogState | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPLogState = D1 ('MetaData "SPLogState" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPStateSatisfiable" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SPStateUnsatisfiable" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SPStateUnknown" 'PrefixI 'False) (U1 :: Type -> Type))) |
SPASS Settings
New impelmentation of Settings. See spass input syntax Version 1.5.
Instances
Eq SPSetting Source # | |
Data SPSetting Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPSetting -> c SPSetting gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPSetting toConstr :: SPSetting -> Constr dataTypeOf :: SPSetting -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPSetting) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPSetting) gmapT :: (forall b. Data b => b -> b) -> SPSetting -> SPSetting gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPSetting -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPSetting -> r gmapQ :: (forall d. Data d => d -> u) -> SPSetting -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPSetting -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPSetting -> m SPSetting gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSetting -> m SPSetting gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSetting -> m SPSetting | |
Ord SPSetting Source # | |
Defined in SoftFOL.Sign | |
Show SPSetting Source # | |
Generic SPSetting | |
FromJSON SPSetting | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPSetting parseJSONList :: Value -> Parser [SPSetting] | |
ToJSON SPSetting | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: SPSetting -> Encoding toJSONList :: [SPSetting] -> Value toEncodingList :: [SPSetting] -> Encoding | |
ShATermConvertible SPSetting | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPSetting -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPSetting] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSetting) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPSetting]) | |
Pretty SPSetting Source # | |
PrintTPTP SPSetting Source # | |
type Rep SPSetting | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPSetting = D1 ('MetaData "SPSetting" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPGeneralSettings" 'PrefixI 'True) (S1 ('MetaSel ('Just "entries") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPHypothesis])) :+: C1 ('MetaCons "SPSettings" 'PrefixI 'True) (S1 ('MetaSel ('Just "settingName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPSettingLabel) :*: S1 ('MetaSel ('Just "settingBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPSettingBody]))) |
data SPSettingBody Source #
SPClauseRelation [SPCRBIND] | |
SPFlag String [String] |
Instances
Eq SPSettingBody Source # | |
Defined in SoftFOL.Sign (==) :: SPSettingBody -> SPSettingBody -> Bool (/=) :: SPSettingBody -> SPSettingBody -> Bool | |
Data SPSettingBody Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPSettingBody -> c SPSettingBody gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPSettingBody toConstr :: SPSettingBody -> Constr dataTypeOf :: SPSettingBody -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPSettingBody) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPSettingBody) gmapT :: (forall b. Data b => b -> b) -> SPSettingBody -> SPSettingBody gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPSettingBody -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPSettingBody -> r gmapQ :: (forall d. Data d => d -> u) -> SPSettingBody -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPSettingBody -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPSettingBody -> m SPSettingBody gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSettingBody -> m SPSettingBody gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSettingBody -> m SPSettingBody | |
Ord SPSettingBody Source # | |
Defined in SoftFOL.Sign compare :: SPSettingBody -> SPSettingBody -> Ordering (<) :: SPSettingBody -> SPSettingBody -> Bool (<=) :: SPSettingBody -> SPSettingBody -> Bool (>) :: SPSettingBody -> SPSettingBody -> Bool (>=) :: SPSettingBody -> SPSettingBody -> Bool max :: SPSettingBody -> SPSettingBody -> SPSettingBody min :: SPSettingBody -> SPSettingBody -> SPSettingBody | |
Show SPSettingBody Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPSettingBody -> ShowS show :: SPSettingBody -> String showList :: [SPSettingBody] -> ShowS | |
Generic SPSettingBody | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPSettingBody :: Type -> Type from :: SPSettingBody -> Rep SPSettingBody x to :: Rep SPSettingBody x -> SPSettingBody | |
FromJSON SPSettingBody | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPSettingBody parseJSONList :: Value -> Parser [SPSettingBody] | |
ToJSON SPSettingBody | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPSettingBody -> Value toEncoding :: SPSettingBody -> Encoding toJSONList :: [SPSettingBody] -> Value toEncodingList :: [SPSettingBody] -> Encoding | |
ShATermConvertible SPSettingBody | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPSettingBody -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPSettingBody] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSettingBody) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPSettingBody]) | |
Pretty SPSettingBody Source # | |
Defined in SoftFOL.Print pretty :: SPSettingBody -> Doc Source # pretties :: [SPSettingBody] -> Doc Source # | |
PrintTPTP SPSettingBody Source # | |
Defined in SoftFOL.PrintTPTP printTPTP :: SPSettingBody -> Doc Source # | |
type Rep SPSettingBody | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPSettingBody = D1 ('MetaData "SPSettingBody" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPClauseRelation" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPCRBIND])) :+: C1 ('MetaCons "SPFlag" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]))) |
data SPHypothesis Source #
Instances
Eq SPHypothesis Source # | |
Defined in SoftFOL.Sign (==) :: SPHypothesis -> SPHypothesis -> Bool (/=) :: SPHypothesis -> SPHypothesis -> Bool | |
Data SPHypothesis Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPHypothesis -> c SPHypothesis gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPHypothesis toConstr :: SPHypothesis -> Constr dataTypeOf :: SPHypothesis -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPHypothesis) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPHypothesis) gmapT :: (forall b. Data b => b -> b) -> SPHypothesis -> SPHypothesis gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPHypothesis -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPHypothesis -> r gmapQ :: (forall d. Data d => d -> u) -> SPHypothesis -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPHypothesis -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPHypothesis -> m SPHypothesis gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPHypothesis -> m SPHypothesis gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPHypothesis -> m SPHypothesis | |
Ord SPHypothesis Source # | |
Defined in SoftFOL.Sign compare :: SPHypothesis -> SPHypothesis -> Ordering (<) :: SPHypothesis -> SPHypothesis -> Bool (<=) :: SPHypothesis -> SPHypothesis -> Bool (>) :: SPHypothesis -> SPHypothesis -> Bool (>=) :: SPHypothesis -> SPHypothesis -> Bool max :: SPHypothesis -> SPHypothesis -> SPHypothesis min :: SPHypothesis -> SPHypothesis -> SPHypothesis | |
Show SPHypothesis Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPHypothesis -> ShowS show :: SPHypothesis -> String showList :: [SPHypothesis] -> ShowS | |
Generic SPHypothesis | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPHypothesis :: Type -> Type from :: SPHypothesis -> Rep SPHypothesis x to :: Rep SPHypothesis x -> SPHypothesis | |
FromJSON SPHypothesis | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPHypothesis parseJSONList :: Value -> Parser [SPHypothesis] | |
ToJSON SPHypothesis | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPHypothesis -> Value toEncoding :: SPHypothesis -> Encoding toJSONList :: [SPHypothesis] -> Value toEncodingList :: [SPHypothesis] -> Encoding | |
ShATermConvertible SPHypothesis | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPHypothesis -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPHypothesis] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPHypothesis) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPHypothesis]) | |
Pretty SPHypothesis Source # | |
Defined in SoftFOL.Print pretty :: SPHypothesis -> Doc Source # pretties :: [SPHypothesis] -> Doc Source # | |
type Rep SPHypothesis | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPHypothesis = D1 ('MetaData "SPHypothesis" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPHypothesis" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPIdentifier]))) |
data SPSettingLabel Source #
Instances
Eq SPSettingLabel Source # | |
Defined in SoftFOL.Sign (==) :: SPSettingLabel -> SPSettingLabel -> Bool (/=) :: SPSettingLabel -> SPSettingLabel -> Bool | |
Data SPSettingLabel Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPSettingLabel -> c SPSettingLabel gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPSettingLabel toConstr :: SPSettingLabel -> Constr dataTypeOf :: SPSettingLabel -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPSettingLabel) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPSettingLabel) gmapT :: (forall b. Data b => b -> b) -> SPSettingLabel -> SPSettingLabel gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPSettingLabel -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPSettingLabel -> r gmapQ :: (forall d. Data d => d -> u) -> SPSettingLabel -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPSettingLabel -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPSettingLabel -> m SPSettingLabel gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSettingLabel -> m SPSettingLabel gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPSettingLabel -> m SPSettingLabel | |
Ord SPSettingLabel Source # | |
Defined in SoftFOL.Sign compare :: SPSettingLabel -> SPSettingLabel -> Ordering (<) :: SPSettingLabel -> SPSettingLabel -> Bool (<=) :: SPSettingLabel -> SPSettingLabel -> Bool (>) :: SPSettingLabel -> SPSettingLabel -> Bool (>=) :: SPSettingLabel -> SPSettingLabel -> Bool max :: SPSettingLabel -> SPSettingLabel -> SPSettingLabel min :: SPSettingLabel -> SPSettingLabel -> SPSettingLabel | |
Show SPSettingLabel Source # | |
Defined in SoftFOL.Sign showsPrec :: Int -> SPSettingLabel -> ShowS show :: SPSettingLabel -> String showList :: [SPSettingLabel] -> ShowS | |
Generic SPSettingLabel | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPSettingLabel :: Type -> Type from :: SPSettingLabel -> Rep SPSettingLabel x to :: Rep SPSettingLabel x -> SPSettingLabel | |
FromJSON SPSettingLabel | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPSettingLabel parseJSONList :: Value -> Parser [SPSettingLabel] | |
ToJSON SPSettingLabel | |
Defined in SoftFOL.ATC_SoftFOL toJSON :: SPSettingLabel -> Value toEncoding :: SPSettingLabel -> Encoding toJSONList :: [SPSettingLabel] -> Value toEncodingList :: [SPSettingLabel] -> Encoding | |
ShATermConvertible SPSettingLabel | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPSettingLabel -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPSettingLabel] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPSettingLabel) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPSettingLabel]) | |
Pretty SPSettingLabel Source # | |
Defined in SoftFOL.Print pretty :: SPSettingLabel -> Doc Source # pretties :: [SPSettingLabel] -> Doc Source # | |
type Rep SPSettingLabel | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPSettingLabel = D1 ('MetaData "SPSettingLabel" "SoftFOL.Sign" "main" 'False) (((C1 ('MetaCons "KIV" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LEM" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "OTTER" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PROTEIN" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "SATURATE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ThreeTAP" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SETHEO" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SPASS" 'PrefixI 'False) (U1 :: Type -> Type)))) |
showSettingLabel :: SPSettingLabel -> String Source #
A Tupel of the Clause Relation
SPCRBIND | |
|
Instances
Eq SPCRBIND Source # | |
Data SPCRBIND Source # | |
Defined in SoftFOL.Sign gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPCRBIND -> c SPCRBIND gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPCRBIND toConstr :: SPCRBIND -> Constr dataTypeOf :: SPCRBIND -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPCRBIND) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPCRBIND) gmapT :: (forall b. Data b => b -> b) -> SPCRBIND -> SPCRBIND gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPCRBIND -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPCRBIND -> r gmapQ :: (forall d. Data d => d -> u) -> SPCRBIND -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPCRBIND -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPCRBIND -> m SPCRBIND gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPCRBIND -> m SPCRBIND gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPCRBIND -> m SPCRBIND | |
Ord SPCRBIND Source # | |
Show SPCRBIND Source # | |
Generic SPCRBIND | |
FromJSON SPCRBIND | |
Defined in SoftFOL.ATC_SoftFOL parseJSON :: Value -> Parser SPCRBIND parseJSONList :: Value -> Parser [SPCRBIND] | |
ToJSON SPCRBIND | |
Defined in SoftFOL.ATC_SoftFOL toEncoding :: SPCRBIND -> Encoding toJSONList :: [SPCRBIND] -> Value toEncodingList :: [SPCRBIND] -> Encoding | |
ShATermConvertible SPCRBIND | |
Defined in SoftFOL.ATC_SoftFOL toShATermAux :: ATermTable -> SPCRBIND -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPCRBIND] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPCRBIND) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPCRBIND]) | |
Pretty SPCRBIND Source # | |
type Rep SPCRBIND | |
Defined in SoftFOL.ATC_SoftFOL type Rep SPCRBIND = D1 ('MetaData "SPCRBIND" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPCRBIND" 'PrefixI 'True) (S1 ('MetaSel ('Just "clauseSPR") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "formulaSPR") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |
negateSentence :: SPTerm -> Maybe SPTerm Source #
negate a sentence