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

SoftFOL.Sign

Contents

Externally used data structures
- Symbol related datatypes
Internal data structures

Description

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 {
- sym_ident :: SPIdentifier
- sym_type :: SFSymbType
}
data SFSymbType
- = SFOpType [SPIdentifier] SPIdentifier
- | SFPredType [SPIdentifier]
- | SFSortType
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 {
- functions :: [SPSignSym]
- predicates :: [SPSignSym]
- sorts :: [SPSignSym]
}
emptySymbolList :: SPSymbolList
data SPSignSym
- = SPSignSym {
  - sym :: SPIdentifier
  - arity :: Int
  }
- | SPSimpleSignSym SPIdentifier
data SPSortSym = SPSortSym SPIdentifier
data SPDeclaration
- = SPSubsortDecl {
  - sortSymA :: SPIdentifier
  - sortSymB :: SPIdentifier
  }
- | 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 {
- coriginType :: SPOriginType
- clauseType :: SPClauseType
- clauses :: [SPClause]
}
data SPOriginType
- = SPOriginAxioms
- | SPOriginConjectures
data SPClauseType
- = SPCNF
- | SPDNF
type SPClause = Named NSPClause
data NSPClause
- = QuanClause [SPTerm] NSPClauseBody
- | SimpleClause NSPClauseBody
- | BriefClause TermWsList TermWsList TermWsList
data NSPClauseBody = NSPClauseBody SPClauseType [SPLiteral]
data TermWsList = TWL [SPTerm] Bool
data SPTerm
- = SPQuantTerm {
  - quantSym :: SPQuantSym
  - variableList :: [SPTerm]
  - qFormula :: SPTerm
  }
- | SPComplexTerm {
  - symbol :: SPSymbol
  - arguments :: [SPTerm]
  }
data FileName = FileName String
data FormKind
- = FofKind
- | CnfKind
- | FotKind
data Role
- = Axiom
- | Hypothesis
- | Definition
- | Assumption
- | Lemma
- | Theorem
- | Conjecture
- | Negated_conjecture
- | Plain
- | Fi_domain
- | Fi_functors
- | Fi_predicates
- | Type
- | Unknown
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
- = FormAnno FormKind Name Role SPTerm (Maybe Annos)
- | Include FileName [Name]
- | CommentLine String
- | EmptyLine
data SPLiteral = SPLiteral Bool SPSymbol
toLiteral :: MonadFail m => SPTerm -> m SPLiteral
data SPQuantSym
- = SPForall
- | SPExists
- | SPCustomQuantSym SPIdentifier
data SPSymbol
- = SPEqual
- | SPTrue
- | SPFalse
- | SPOr
- | SPAnd
- | SPNot
- | SPImplies
- | SPImplied
- | SPEquiv
- | SPID
- | SPDiv
- | SPComp
- | SPSum
- | SPConv
- | SPCustomSymbol SPIdentifier
mkSPCustomSymbol :: String -> SPSymbol
showSPSymbol :: SPSymbol -> String
data SPProofList = SPProofList {
- proofType :: Maybe SPProofType
- plAssocList :: SPAssocList
- step :: [SPProofStep]
}
type SPProofType = SPIdentifier
data SPProofStep = SPProofStep {
- reference :: SPReference
- result :: SPResult
- ruleAppl :: SPRuleAppl
- parentList :: [SPParent]
- stepAssocList :: SPAssocList
}
data SPReference = PRefTerm SPTerm
data SPResult = PResTerm SPTerm
data SPRuleAppl
- = PRuleTerm SPTerm
- | PRuleUser SPUserRuleAppl
data SPUserRuleAppl
- = GeR
- | SpL
- | SpR
- | EqF
- | Rew
- | Obv
- | EmS
- | SoR
- | EqR
- | Mpm
- | SPm
- | OPm
- | SHy
- | OHy
- | URR
- | Fac
- | Spt
- | Inp
- | Con
- | RRE
- | SSi
- | ClR
- | UnC
- | Ter
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 {
- name :: String
- author :: String
- version :: Maybe String
- logic :: Maybe String
- status :: SPLogState
- desc :: String
- date :: Maybe String
}
data SPLogState
- = SPStateSatisfiable
- | SPStateUnsatisfiable
- | SPStateUnknown
data SPSetting
- = SPGeneralSettings {
  - entries :: [SPHypothesis]
  }
- | SPSettings {
  - settingName :: SPSettingLabel
  - settingBody :: [SPSettingBody]
  }
data SPSettingBody
- = SPClauseRelation [SPCRBIND]
- | SPFlag String [String]
data SPHypothesis = SPHypothesis [SPIdentifier]
data SPSettingLabel
- = KIV
- | LEM
- | OTTER
- | PROTEIN
- | SATURATE
- | ThreeTAP
- | SETHEO
- | SPASS
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 #

data Sign 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).

Constructors

Sign
Fields sortRel :: Rel SPIdentifier sortMap :: SortMap funcMap :: FuncMap predMap :: PredMap singleSorted :: Bool

Instances

Instances details

Eq Sign Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: Sign -> Sign -> Bool (/=) :: Sign -> Sign -> Bool
Data Sign Source #
Instance details Defined in SoftFOL.Sign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sign -> c Sign gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sign toConstr :: Sign -> Constr dataTypeOf :: Sign -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sign) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign) gmapT :: (forall b. Data b => b -> b) -> Sign -> Sign gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r gmapQ :: (forall d. Data d => d -> u) -> Sign -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Sign -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sign -> m Sign gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign
Ord Sign Source #
Instance details Defined in SoftFOL.Sign Methods compare :: Sign -> Sign -> Ordering (<) :: Sign -> Sign -> Bool (<=) :: Sign -> Sign -> Bool (>) :: Sign -> Sign -> Bool (>=) :: Sign -> Sign -> Bool max :: Sign -> Sign -> Sign min :: Sign -> Sign -> Sign
Show Sign Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> Sign -> ShowS show :: Sign -> String showList :: [Sign] -> ShowS
Generic Sign
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep Sign :: Type -> Type Methods from :: Sign -> Rep Sign x to :: Rep Sign x -> Sign
FromJSON Sign
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser Sign parseJSONList :: Value -> Parser [Sign]
ToJSON Sign
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: Sign -> Value toEncoding :: Sign -> Encoding toJSONList :: [Sign] -> Value toEncodingList :: [Sign] -> Encoding
ShATermConvertible Sign
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sign] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sign])
Pretty Sign Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods pretty :: Sign -> Doc Source # pretties :: [Sign] -> Doc Source #
PrintTPTP Sign Source #
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: Sign -> Doc Source #
Sentences SoftFOL Sentence Sign SoftFOLMorphism SFSymbol Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods map_sen :: SoftFOL -> SoftFOLMorphism -> Sentence -> Result Sentence Source # simplify_sen :: SoftFOL -> Sign -> Sentence -> Sentence Source # negation :: SoftFOL -> Sentence -> Maybe Sentence Source # print_sign :: SoftFOL -> Sign -> Doc Source # print_named :: SoftFOL -> Named Sentence -> Doc Source # sym_of :: SoftFOL -> Sign -> [Set SFSymbol] Source # mostSymsOf :: SoftFOL -> Sign -> [SFSymbol] Source # symmap_of :: SoftFOL -> SoftFOLMorphism -> EndoMap SFSymbol Source # sym_name :: SoftFOL -> SFSymbol -> Id Source # sym_label :: SoftFOL -> SFSymbol -> Maybe String Source # fullSymName :: SoftFOL -> SFSymbol -> String Source # symKind :: SoftFOL -> SFSymbol -> String Source # symsOfSen :: SoftFOL -> Sign -> Sentence -> [SFSymbol] Source # pair_symbols :: SoftFOL -> SFSymbol -> SFSymbol -> Result SFSymbol Source #
Comorphism SoftFOL2CommonLogic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.SoftFOL2CommonLogic Methods sourceLogic :: SoftFOL2CommonLogic -> SoftFOL Source # sourceSublogic :: SoftFOL2CommonLogic -> () Source # sourceSublogicLossy :: SoftFOL2CommonLogic -> () Source # minSourceTheory :: SoftFOL2CommonLogic -> Maybe (LibName, String) Source # targetLogic :: SoftFOL2CommonLogic -> CommonLogic Source # mapSublogic :: SoftFOL2CommonLogic -> () -> Maybe CommonLogicSL Source # map_theory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source # mapMarkedTheory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source # map_morphism :: SoftFOL2CommonLogic -> SoftFOLMorphism -> Result Morphism Source # map_sentence :: SoftFOL2CommonLogic -> Sign -> Sentence -> Result TEXT_META Source # map_symbol :: SoftFOL2CommonLogic -> Sign -> SFSymbol -> Set Symbol Source # extractModel :: SoftFOL2CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: SoftFOL2CommonLogic -> Bool Source # has_model_expansion :: SoftFOL2CommonLogic -> Bool Source # is_weakly_amalgamable :: SoftFOL2CommonLogic -> Bool Source # constituents :: SoftFOL2CommonLogic -> [String] Source # isInclusionComorphism :: SoftFOL2CommonLogic -> Bool Source # rps :: SoftFOL2CommonLogic -> Bool Source # eps :: SoftFOL2CommonLogic -> Bool Source # isGTC :: SoftFOL2CommonLogic -> Bool Source #
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods parse_basic_sen :: SoftFOL -> Maybe ([TPTP] -> AParser st Sentence) Source # stability :: SoftFOL -> Stability Source # data_logic :: SoftFOL -> Maybe AnyLogic Source # top_sublogic :: SoftFOL -> () Source # all_sublogics :: SoftFOL -> [()] Source # bottomSublogic :: SoftFOL -> Maybe () Source # sublogicDimensions :: SoftFOL -> [[()]] Source # parseSublogic :: SoftFOL -> String -> Maybe () Source # proj_sublogic_epsilon :: SoftFOL -> () -> Sign -> SoftFOLMorphism Source # provers :: SoftFOL -> [Prover Sign Sentence SoftFOLMorphism () ProofTree] Source # default_prover :: SoftFOL -> String Source # cons_checkers :: SoftFOL -> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree] Source # conservativityCheck :: SoftFOL -> [ConservativityChecker Sign Sentence SoftFOLMorphism] Source # empty_proof_tree :: SoftFOL -> ProofTree Source # syntaxTable :: SoftFOL -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: SoftFOL -> Maybe OMCD Source # export_symToOmdoc :: SoftFOL -> NameMap SFSymbol -> SFSymbol -> String -> Result TCElement Source # export_senToOmdoc :: SoftFOL -> NameMap SFSymbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: SoftFOL -> SigMap SFSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result SFSymbol Source # omdocToSen :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source # addOmdocToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source # sublogicOfTheo :: SoftFOL -> (Sign, [Sentence]) -> () Source #
StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods basic_analysis :: SoftFOL -> Maybe (([TPTP], Sign, GlobalAnnos) -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])) Source # sen_analysis :: SoftFOL -> Maybe (([TPTP], Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: SoftFOL -> IRI -> LibName -> [TPTP] -> Sign -> GlobalAnnos -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]) Source # stat_symb_map_items :: SoftFOL -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: SoftFOL -> Sign -> [()] -> Result [()] Source # convertTheory :: SoftFOL -> Maybe ((Sign, [Named Sentence]) -> [TPTP]) Source # ensures_amalgamability :: SoftFOL -> ([CASLAmalgOpt], Gr Sign (Int, SoftFOLMorphism), [(Int, SoftFOLMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: SoftFOL -> SoftFOLMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: SoftFOL -> Gr Sign (Int, SoftFOLMorphism) -> Result (Sign, Map Int SoftFOLMorphism) Source # qualify :: SoftFOL -> SIMPLE_ID -> LibName -> SoftFOLMorphism -> Sign -> Result (SoftFOLMorphism, [Named Sentence]) Source # symbol_to_raw :: SoftFOL -> SFSymbol -> () Source # id_to_raw :: SoftFOL -> Id -> () Source # matches :: SoftFOL -> SFSymbol -> () -> Bool Source # empty_signature :: SoftFOL -> Sign Source # add_symb_to_sign :: SoftFOL -> Sign -> SFSymbol -> Result Sign Source # signature_union :: SoftFOL -> Sign -> Sign -> Result Sign Source # signatureDiff :: SoftFOL -> Sign -> Sign -> Result Sign Source # intersection :: SoftFOL -> Sign -> Sign -> Result Sign Source # final_union :: SoftFOL -> Sign -> Sign -> Result Sign Source # morphism_union :: SoftFOL -> SoftFOLMorphism -> SoftFOLMorphism -> Result SoftFOLMorphism Source # is_subsig :: SoftFOL -> Sign -> Sign -> Bool Source # subsig_inclusion :: SoftFOL -> Sign -> Sign -> Result SoftFOLMorphism Source # generated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source # cogenerated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source # induced_from_morphism :: SoftFOL -> EndoMap () -> Sign -> Result SoftFOLMorphism Source # induced_from_to_morphism :: SoftFOL -> EndoMap () -> ExtSign Sign SFSymbol -> ExtSign Sign SFSymbol -> Result SoftFOLMorphism Source # is_transportable :: SoftFOL -> SoftFOLMorphism -> Bool Source # is_injective :: SoftFOL -> SoftFOLMorphism -> Bool Source # theory_to_taxonomy :: SoftFOL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: SoftFOL -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap SFSymbol -> EndoMap SFSymbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source # equiv2cospan :: SoftFOL -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source # extract_module :: SoftFOL -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #
type Rep Sign
Instance details Defined in SoftFOL.ATC_SoftFOL type Rep Sign = D1 ('MetaData "Sign" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "Sign" 'PrefixI 'True) ((S1 ('MetaSel ('Just "sortRel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Rel SPIdentifier)) :: S1 ('MetaSel ('Just "sortMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SortMap)) :: (S1 ('MetaSel ('Just "funcMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FuncMap) :: (S1 ('MetaSel ('Just "predMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PredMap) :: S1 ('MetaSel ('Just "singleSorted") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

data Generated Source #

Sorts can be (freely) generated by a set of functions.

Constructors

Generated
Fields freely :: Bool byFunctions :: [SPIdentifier]

Instances

Instances details

Eq Generated Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: Generated -> Generated -> Bool (/=) :: Generated -> Generated -> Bool
Data Generated Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: Generated -> Generated -> Ordering (<) :: Generated -> Generated -> Bool (<=) :: Generated -> Generated -> Bool (>) :: Generated -> Generated -> Bool (>=) :: Generated -> Generated -> Bool max :: Generated -> Generated -> Generated min :: Generated -> Generated -> Generated
Show Generated Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> Generated -> ShowS show :: Generated -> String showList :: [Generated] -> ShowS
Generic Generated
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep Generated :: Type -> Type Methods from :: Generated -> Rep Generated x to :: Rep Generated x -> Generated
FromJSON Generated
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser Generated parseJSONList :: Value -> Parser [Generated]
ToJSON Generated
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: Generated -> Value toEncoding :: Generated -> Encoding toJSONList :: [Generated] -> Value toEncodingList :: [Generated] -> Encoding
ShATermConvertible Generated
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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])))

emptySign :: Sign Source #

Creates an empty Signature.

type Sentence = SPTerm Source #

A Sentence is a SoftFOL Term.

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

data SFSymbol Source #

Symbols of SoftFOL.

Constructors

SFSymbol
Fields sym_ident :: SPIdentifier sym_type :: SFSymbType

Instances

Instances details

Eq SFSymbol Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SFSymbol -> SFSymbol -> Bool (/=) :: SFSymbol -> SFSymbol -> Bool
Data SFSymbol Source #
Instance details Defined in SoftFOL.Sign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SFSymbol -> c SFSymbol gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SFSymbol toConstr :: SFSymbol -> Constr dataTypeOf :: SFSymbol -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SFSymbol) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SFSymbol) gmapT :: (forall b. Data b => b -> b) -> SFSymbol -> SFSymbol gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SFSymbol -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SFSymbol -> r gmapQ :: (forall d. Data d => d -> u) -> SFSymbol -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SFSymbol -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SFSymbol -> m SFSymbol gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SFSymbol -> m SFSymbol gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SFSymbol -> m SFSymbol
Ord SFSymbol Source #
Instance details Defined in SoftFOL.Sign Methods compare :: SFSymbol -> SFSymbol -> Ordering (<) :: SFSymbol -> SFSymbol -> Bool (<=) :: SFSymbol -> SFSymbol -> Bool (>) :: SFSymbol -> SFSymbol -> Bool (>=) :: SFSymbol -> SFSymbol -> Bool max :: SFSymbol -> SFSymbol -> SFSymbol min :: SFSymbol -> SFSymbol -> SFSymbol
Show SFSymbol Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SFSymbol -> ShowS show :: SFSymbol -> String showList :: [SFSymbol] -> ShowS
Generic SFSymbol
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SFSymbol :: Type -> Type Methods from :: SFSymbol -> Rep SFSymbol x to :: Rep SFSymbol x -> SFSymbol
GetRange SFSymbol Source #
Instance details Defined in SoftFOL.Sign Methods getRange :: SFSymbol -> Range Source # rangeSpan :: SFSymbol -> [Pos] Source #
FromJSON SFSymbol
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SFSymbol parseJSONList :: Value -> Parser [SFSymbol]
ToJSON SFSymbol
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SFSymbol -> Value toEncoding :: SFSymbol -> Encoding toJSONList :: [SFSymbol] -> Value toEncodingList :: [SFSymbol] -> Encoding
ShATermConvertible SFSymbol
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toShATermAux :: ATermTable -> SFSymbol -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SFSymbol] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SFSymbol) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SFSymbol])
Pretty SFSymbol Source #
Instance details Defined in SoftFOL.Print Methods pretty :: SFSymbol -> Doc Source # pretties :: [SFSymbol] -> Doc Source #
Sentences SoftFOL Sentence Sign SoftFOLMorphism SFSymbol Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods map_sen :: SoftFOL -> SoftFOLMorphism -> Sentence -> Result Sentence Source # simplify_sen :: SoftFOL -> Sign -> Sentence -> Sentence Source # negation :: SoftFOL -> Sentence -> Maybe Sentence Source # print_sign :: SoftFOL -> Sign -> Doc Source # print_named :: SoftFOL -> Named Sentence -> Doc Source # sym_of :: SoftFOL -> Sign -> [Set SFSymbol] Source # mostSymsOf :: SoftFOL -> Sign -> [SFSymbol] Source # symmap_of :: SoftFOL -> SoftFOLMorphism -> EndoMap SFSymbol Source # sym_name :: SoftFOL -> SFSymbol -> Id Source # sym_label :: SoftFOL -> SFSymbol -> Maybe String Source # fullSymName :: SoftFOL -> SFSymbol -> String Source # symKind :: SoftFOL -> SFSymbol -> String Source # symsOfSen :: SoftFOL -> Sign -> Sentence -> [SFSymbol] Source # pair_symbols :: SoftFOL -> SFSymbol -> SFSymbol -> Result SFSymbol Source #
Comorphism SoftFOL2CommonLogic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.SoftFOL2CommonLogic Methods sourceLogic :: SoftFOL2CommonLogic -> SoftFOL Source # sourceSublogic :: SoftFOL2CommonLogic -> () Source # sourceSublogicLossy :: SoftFOL2CommonLogic -> () Source # minSourceTheory :: SoftFOL2CommonLogic -> Maybe (LibName, String) Source # targetLogic :: SoftFOL2CommonLogic -> CommonLogic Source # mapSublogic :: SoftFOL2CommonLogic -> () -> Maybe CommonLogicSL Source # map_theory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source # mapMarkedTheory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source # map_morphism :: SoftFOL2CommonLogic -> SoftFOLMorphism -> Result Morphism Source # map_sentence :: SoftFOL2CommonLogic -> Sign -> Sentence -> Result TEXT_META Source # map_symbol :: SoftFOL2CommonLogic -> Sign -> SFSymbol -> Set Symbol Source # extractModel :: SoftFOL2CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: SoftFOL2CommonLogic -> Bool Source # has_model_expansion :: SoftFOL2CommonLogic -> Bool Source # is_weakly_amalgamable :: SoftFOL2CommonLogic -> Bool Source # constituents :: SoftFOL2CommonLogic -> [String] Source # isInclusionComorphism :: SoftFOL2CommonLogic -> Bool Source # rps :: SoftFOL2CommonLogic -> Bool Source # eps :: SoftFOL2CommonLogic -> Bool Source # isGTC :: SoftFOL2CommonLogic -> Bool Source #
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods parse_basic_sen :: SoftFOL -> Maybe ([TPTP] -> AParser st Sentence) Source # stability :: SoftFOL -> Stability Source # data_logic :: SoftFOL -> Maybe AnyLogic Source # top_sublogic :: SoftFOL -> () Source # all_sublogics :: SoftFOL -> [()] Source # bottomSublogic :: SoftFOL -> Maybe () Source # sublogicDimensions :: SoftFOL -> [[()]] Source # parseSublogic :: SoftFOL -> String -> Maybe () Source # proj_sublogic_epsilon :: SoftFOL -> () -> Sign -> SoftFOLMorphism Source # provers :: SoftFOL -> [Prover Sign Sentence SoftFOLMorphism () ProofTree] Source # default_prover :: SoftFOL -> String Source # cons_checkers :: SoftFOL -> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree] Source # conservativityCheck :: SoftFOL -> [ConservativityChecker Sign Sentence SoftFOLMorphism] Source # empty_proof_tree :: SoftFOL -> ProofTree Source # syntaxTable :: SoftFOL -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: SoftFOL -> Maybe OMCD Source # export_symToOmdoc :: SoftFOL -> NameMap SFSymbol -> SFSymbol -> String -> Result TCElement Source # export_senToOmdoc :: SoftFOL -> NameMap SFSymbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: SoftFOL -> SigMap SFSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result SFSymbol Source # omdocToSen :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source # addOmdocToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source # sublogicOfTheo :: SoftFOL -> (Sign, [Sentence]) -> () Source #
Syntax SoftFOL [TPTP] SFSymbol () () Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods parsersAndPrinters :: SoftFOL -> Map String (PrefixMap -> AParser st [TPTP], [TPTP] -> Doc) Source # parse_basic_spec :: SoftFOL -> Maybe (PrefixMap -> AParser st [TPTP]) Source # parseSingleSymbItem :: SoftFOL -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: SoftFOL -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: SoftFOL -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: SoftFOL -> [TPTP] -> Item Source # symb_items_name :: SoftFOL -> () -> [String] Source #
StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods basic_analysis :: SoftFOL -> Maybe (([TPTP], Sign, GlobalAnnos) -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])) Source # sen_analysis :: SoftFOL -> Maybe (([TPTP], Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: SoftFOL -> IRI -> LibName -> [TPTP] -> Sign -> GlobalAnnos -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]) Source # stat_symb_map_items :: SoftFOL -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: SoftFOL -> Sign -> [()] -> Result [()] Source # convertTheory :: SoftFOL -> Maybe ((Sign, [Named Sentence]) -> [TPTP]) Source # ensures_amalgamability :: SoftFOL -> ([CASLAmalgOpt], Gr Sign (Int, SoftFOLMorphism), [(Int, SoftFOLMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: SoftFOL -> SoftFOLMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: SoftFOL -> Gr Sign (Int, SoftFOLMorphism) -> Result (Sign, Map Int SoftFOLMorphism) Source # qualify :: SoftFOL -> SIMPLE_ID -> LibName -> SoftFOLMorphism -> Sign -> Result (SoftFOLMorphism, [Named Sentence]) Source # symbol_to_raw :: SoftFOL -> SFSymbol -> () Source # id_to_raw :: SoftFOL -> Id -> () Source # matches :: SoftFOL -> SFSymbol -> () -> Bool Source # empty_signature :: SoftFOL -> Sign Source # add_symb_to_sign :: SoftFOL -> Sign -> SFSymbol -> Result Sign Source # signature_union :: SoftFOL -> Sign -> Sign -> Result Sign Source # signatureDiff :: SoftFOL -> Sign -> Sign -> Result Sign Source # intersection :: SoftFOL -> Sign -> Sign -> Result Sign Source # final_union :: SoftFOL -> Sign -> Sign -> Result Sign Source # morphism_union :: SoftFOL -> SoftFOLMorphism -> SoftFOLMorphism -> Result SoftFOLMorphism Source # is_subsig :: SoftFOL -> Sign -> Sign -> Bool Source # subsig_inclusion :: SoftFOL -> Sign -> Sign -> Result SoftFOLMorphism Source # generated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source # cogenerated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source # induced_from_morphism :: SoftFOL -> EndoMap () -> Sign -> Result SoftFOLMorphism Source # induced_from_to_morphism :: SoftFOL -> EndoMap () -> ExtSign Sign SFSymbol -> ExtSign Sign SFSymbol -> Result SoftFOLMorphism Source # is_transportable :: SoftFOL -> SoftFOLMorphism -> Bool Source # is_injective :: SoftFOL -> SoftFOLMorphism -> Bool Source # theory_to_taxonomy :: SoftFOL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: SoftFOL -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap SFSymbol -> EndoMap SFSymbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source # equiv2cospan :: SoftFOL -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source # extract_module :: SoftFOL -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #
type Rep SFSymbol
Instance details Defined in SoftFOL.ATC_SoftFOL type Rep SFSymbol = D1 ('MetaData "SFSymbol" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SFSymbol" 'PrefixI 'True) (S1 ('MetaSel ('Just "sym_ident") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPIdentifier) :*: S1 ('MetaSel ('Just "sym_type") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SFSymbType)))

data SFSymbType Source #

Symbol types of SoftFOL. (not related to CASL)

Constructors

SFOpType [SPIdentifier] SPIdentifier
SFPredType [SPIdentifier]
SFSortType

Instances

Instances details

Eq SFSymbType Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SFSymbType -> SFSymbType -> Bool (/=) :: SFSymbType -> SFSymbType -> Bool
Data SFSymbType Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SFSymbType -> ShowS show :: SFSymbType -> String showList :: [SFSymbType] -> ShowS
Generic SFSymbType
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SFSymbType :: Type -> Type Methods from :: SFSymbType -> Rep SFSymbType x to :: Rep SFSymbType x -> SFSymbType
FromJSON SFSymbType
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SFSymbType parseJSONList :: Value -> Parser [SFSymbType]
ToJSON SFSymbType
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SFSymbType -> Value toEncoding :: SFSymbType -> Encoding toJSONList :: [SFSymbType] -> Value toEncodingList :: [SFSymbType] -> Encoding
ShATermConvertible SFSymbType
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SFSymbType -> Doc Source # pretties :: [SFSymbType] -> Doc Source #
type Rep SFSymbType
Instance details 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

data SPProblem Source #

A SPASS problem consists of a description and a logical part. The optional settings part hasn't been implemented yet.

Constructors

SPProblem
Fields identifier :: String description :: SPDescription logicalPart :: SPLogicalPart settings :: [SPSetting]

Instances

Instances details

Eq SPProblem Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPProblem -> SPProblem -> Bool (/=) :: SPProblem -> SPProblem -> Bool
Data SPProblem Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: SPProblem -> SPProblem -> Ordering (<) :: SPProblem -> SPProblem -> Bool (<=) :: SPProblem -> SPProblem -> Bool (>) :: SPProblem -> SPProblem -> Bool (>=) :: SPProblem -> SPProblem -> Bool max :: SPProblem -> SPProblem -> SPProblem min :: SPProblem -> SPProblem -> SPProblem
Show SPProblem Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPProblem -> ShowS show :: SPProblem -> String showList :: [SPProblem] -> ShowS
Generic SPProblem
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPProblem :: Type -> Type Methods from :: SPProblem -> Rep SPProblem x to :: Rep SPProblem x -> SPProblem
FromJSON SPProblem
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPProblem parseJSONList :: Value -> Parser [SPProblem]
ToJSON SPProblem
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPProblem -> Value toEncoding :: SPProblem -> Encoding toJSONList :: [SPProblem] -> Value toEncodingList :: [SPProblem] -> Encoding
ShATermConvertible SPProblem
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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.
Instance details Defined in SoftFOL.Print Methods pretty :: SPProblem -> Doc Source # pretties :: [SPProblem] -> Doc Source #
PrintTPTP SPProblem Source #	Creates a Doc from a SoftFOL Problem.
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: SPProblem -> Doc Source #
type Rep SPProblem
Instance details 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.

Constructors

SPLogicalPart
Fields symbolList :: Maybe SPSymbolList declarationList :: Maybe [SPDeclaration] formulaLists :: [SPFormulaList] clauseLists :: [SPClauseList] proofLists :: [SPProofList]

Instances

Instances details

Eq SPLogicalPart Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPLogicalPart -> SPLogicalPart -> Bool (/=) :: SPLogicalPart -> SPLogicalPart -> Bool
Data SPLogicalPart Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPLogicalPart -> ShowS show :: SPLogicalPart -> String showList :: [SPLogicalPart] -> ShowS
Generic SPLogicalPart
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPLogicalPart :: Type -> Type Methods from :: SPLogicalPart -> Rep SPLogicalPart x to :: Rep SPLogicalPart x -> SPLogicalPart
FromJSON SPLogicalPart
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPLogicalPart parseJSONList :: Value -> Parser [SPLogicalPart]
ToJSON SPLogicalPart
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPLogicalPart -> Value toEncoding :: SPLogicalPart -> Encoding toJSONList :: [SPLogicalPart] -> Value toEncodingList :: [SPLogicalPart] -> Encoding
ShATermConvertible SPLogicalPart
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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.
Instance details Defined in SoftFOL.Print Methods pretty :: SPLogicalPart -> Doc Source # pretties :: [SPLogicalPart] -> Doc Source #
PrintTPTP SPLogicalPart Source #	Creates a Doc from a SoftFOL Logical Part.
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: SPLogicalPart -> Doc Source #
type Rep SPLogicalPart
Instance details 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])))))

emptySPLogicalPart :: SPLogicalPart Source #

Symbol Lists

data SPSymbolList Source #

All non-predefined signature symbols must be declared as part of a SPASS symbol list.

Constructors

SPSymbolList
Fields functions :: [SPSignSym] predicates :: [SPSignSym] sorts :: [SPSignSym]

Instances

Instances details

Eq SPSymbolList Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPSymbolList -> SPSymbolList -> Bool (/=) :: SPSymbolList -> SPSymbolList -> Bool
Data SPSymbolList Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPSymbolList -> ShowS show :: SPSymbolList -> String showList :: [SPSymbolList] -> ShowS
Generic SPSymbolList
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPSymbolList :: Type -> Type Methods from :: SPSymbolList -> Rep SPSymbolList x to :: Rep SPSymbolList x -> SPSymbolList
FromJSON SPSymbolList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPSymbolList parseJSONList :: Value -> Parser [SPSymbolList]
ToJSON SPSymbolList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPSymbolList -> Value toEncoding :: SPSymbolList -> Encoding toJSONList :: [SPSymbolList] -> Value toEncodingList :: [SPSymbolList] -> Encoding
ShATermConvertible SPSymbolList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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.
Instance details Defined in SoftFOL.Print Methods pretty :: SPSymbolList -> Doc Source # pretties :: [SPSymbolList] -> Doc Source #
type Rep SPSymbolList
Instance details 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.

data SPSignSym Source #

A common data type used for all signature symbols.

Constructors

SPSignSym
Fields sym :: SPIdentifier arity :: Int
SPSimpleSignSym SPIdentifier

Instances

Instances details

Eq SPSignSym Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPSignSym -> SPSignSym -> Bool (/=) :: SPSignSym -> SPSignSym -> Bool
Data SPSignSym Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: SPSignSym -> SPSignSym -> Ordering (<) :: SPSignSym -> SPSignSym -> Bool (<=) :: SPSignSym -> SPSignSym -> Bool (>) :: SPSignSym -> SPSignSym -> Bool (>=) :: SPSignSym -> SPSignSym -> Bool max :: SPSignSym -> SPSignSym -> SPSignSym min :: SPSignSym -> SPSignSym -> SPSignSym
Show SPSignSym Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPSignSym -> ShowS show :: SPSignSym -> String showList :: [SPSignSym] -> ShowS
Generic SPSignSym
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPSignSym :: Type -> Type Methods from :: SPSignSym -> Rep SPSignSym x to :: Rep SPSignSym x -> SPSignSym
FromJSON SPSignSym
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPSignSym parseJSONList :: Value -> Parser [SPSignSym]
ToJSON SPSignSym
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPSignSym -> Value toEncoding :: SPSignSym -> Encoding toJSONList :: [SPSignSym] -> Value toEncodingList :: [SPSignSym] -> Encoding
ShATermConvertible SPSignSym
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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.
Instance details Defined in SoftFOL.Print Methods pretty :: SPSignSym -> Doc Source # pretties :: [SPSignSym] -> Doc Source #
type Rep SPSignSym
Instance details 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)))

data SPSortSym Source #

Constructors

SPSortSym SPIdentifier

Instances

Instances details

Eq SPSortSym Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPSortSym -> SPSortSym -> Bool (/=) :: SPSortSym -> SPSortSym -> Bool
Data SPSortSym Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: SPSortSym -> SPSortSym -> Ordering (<) :: SPSortSym -> SPSortSym -> Bool (<=) :: SPSortSym -> SPSortSym -> Bool (>) :: SPSortSym -> SPSortSym -> Bool (>=) :: SPSortSym -> SPSortSym -> Bool max :: SPSortSym -> SPSortSym -> SPSortSym min :: SPSortSym -> SPSortSym -> SPSortSym
Show SPSortSym Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPSortSym -> ShowS show :: SPSortSym -> String showList :: [SPSortSym] -> ShowS
Generic SPSortSym
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPSortSym :: Type -> Type Methods from :: SPSortSym -> Rep SPSortSym x to :: Rep SPSortSym x -> SPSortSym
FromJSON SPSortSym
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPSortSym parseJSONList :: Value -> Parser [SPSortSym]
ToJSON SPSortSym
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPSortSym -> Value toEncoding :: SPSortSym -> Encoding toJSONList :: [SPSortSym] -> Value toEncodingList :: [SPSortSym] -> Encoding
ShATermConvertible SPSortSym
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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.

Constructors

SPSubsortDecl
Fields sortSymA :: SPIdentifier sortSymB :: SPIdentifier
SPTermDecl
Fields termDeclTermList :: [SPTerm] termDeclTerm :: SPTerm
SPSimpleTermDecl SPTerm
SPPredDecl
Fields predSym :: SPIdentifier sortSyms :: [SPIdentifier]
SPGenDecl
Fields sortSym :: SPIdentifier freelyGenerated :: Bool funcList :: [SPIdentifier]

Instances

Instances details

Eq SPDeclaration Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPDeclaration -> SPDeclaration -> Bool (/=) :: SPDeclaration -> SPDeclaration -> Bool
Data SPDeclaration Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPDeclaration -> ShowS show :: SPDeclaration -> String showList :: [SPDeclaration] -> ShowS
Generic SPDeclaration
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPDeclaration :: Type -> Type Methods from :: SPDeclaration -> Rep SPDeclaration x to :: Rep SPDeclaration x -> SPDeclaration
FromJSON SPDeclaration
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPDeclaration parseJSONList :: Value -> Parser [SPDeclaration]
ToJSON SPDeclaration
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPDeclaration -> Value toEncoding :: SPDeclaration -> Encoding toJSONList :: [SPDeclaration] -> Value toEncodingList :: [SPDeclaration] -> Encoding
ShATermConvertible SPDeclaration
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details Defined in SoftFOL.Print Methods 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.
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: SPDeclaration -> Doc Source #
type Rep SPDeclaration
Instance details 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

Constructors

SPFormulaList
Fields originType :: SPOriginType formulae :: [SPFormula]

Instances

Instances details

Eq SPFormulaList Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPFormulaList -> SPFormulaList -> Bool (/=) :: SPFormulaList -> SPFormulaList -> Bool
Data SPFormulaList Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPFormulaList -> ShowS show :: SPFormulaList -> String showList :: [SPFormulaList] -> ShowS
Generic SPFormulaList
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPFormulaList :: Type -> Type Methods from :: SPFormulaList -> Rep SPFormulaList x to :: Rep SPFormulaList x -> SPFormulaList
FromJSON SPFormulaList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPFormulaList parseJSONList :: Value -> Parser [SPFormulaList]
ToJSON SPFormulaList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPFormulaList -> Value toEncoding :: SPFormulaList -> Encoding toJSONList :: [SPFormulaList] -> Value toEncodingList :: [SPFormulaList] -> Encoding
ShATermConvertible SPFormulaList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details Defined in SoftFOL.Print Methods pretty :: SPFormulaList -> Doc Source # pretties :: [SPFormulaList] -> Doc Source #
PrintTPTP SPFormulaList Source #	Creates a Doc from a SoftFOL Formula List.
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: SPFormulaList -> Doc Source #
type Rep SPFormulaList
Instance details 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

Constructors

SPClauseList
Fields coriginType :: SPOriginType clauseType :: SPClauseType clauses :: [SPClause]

Instances

Instances details

Eq SPClauseList Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPClauseList -> SPClauseList -> Bool (/=) :: SPClauseList -> SPClauseList -> Bool
Data SPClauseList Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPClauseList -> ShowS show :: SPClauseList -> String showList :: [SPClauseList] -> ShowS
Generic SPClauseList
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPClauseList :: Type -> Type Methods from :: SPClauseList -> Rep SPClauseList x to :: Rep SPClauseList x -> SPClauseList
FromJSON SPClauseList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPClauseList parseJSONList :: Value -> Parser [SPClauseList]
ToJSON SPClauseList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPClauseList -> Value toEncoding :: SPClauseList -> Encoding toJSONList :: [SPClauseList] -> Value toEncodingList :: [SPClauseList] -> Encoding
ShATermConvertible SPClauseList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPClauseList -> Doc Source # pretties :: [SPClauseList] -> Doc Source #
type Rep SPClauseList
Instance details 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.

Constructors

SPOriginAxioms
SPOriginConjectures

Instances

Instances details

Eq SPOriginType Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPOriginType -> SPOriginType -> Bool (/=) :: SPOriginType -> SPOriginType -> Bool
Data SPOriginType Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPOriginType -> ShowS show :: SPOriginType -> String showList :: [SPOriginType] -> ShowS
Generic SPOriginType
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPOriginType :: Type -> Type Methods from :: SPOriginType -> Rep SPOriginType x to :: Rep SPOriginType x -> SPOriginType
FromJSON SPOriginType
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPOriginType parseJSONList :: Value -> Parser [SPOriginType]
ToJSON SPOriginType
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPOriginType -> Value toEncoding :: SPOriginType -> Encoding toJSONList :: [SPOriginType] -> Value toEncodingList :: [SPOriginType] -> Encoding
ShATermConvertible SPOriginType
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details Defined in SoftFOL.Print Methods pretty :: SPOriginType -> Doc Source # pretties :: [SPOriginType] -> Doc Source #
PrintTPTP SPOriginType Source #	Creates a Doc from a SoftFOL Origin Type.
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: SPOriginType -> Doc Source #
type Rep SPOriginType
Instance details 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

Constructors

SPCNF
SPDNF

Instances

Instances details

Eq SPClauseType Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPClauseType -> SPClauseType -> Bool (/=) :: SPClauseType -> SPClauseType -> Bool
Data SPClauseType Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPClauseType -> ShowS show :: SPClauseType -> String showList :: [SPClauseType] -> ShowS
Generic SPClauseType
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPClauseType :: Type -> Type Methods from :: SPClauseType -> Rep SPClauseType x to :: Rep SPClauseType x -> SPClauseType
FromJSON SPClauseType
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPClauseType parseJSONList :: Value -> Parser [SPClauseType]
ToJSON SPClauseType
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPClauseType -> Value toEncoding :: SPClauseType -> Encoding toJSONList :: [SPClauseType] -> Value toEncodingList :: [SPClauseType] -> Encoding
ShATermConvertible SPClauseType
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPClauseType -> Doc Source # pretties :: [SPClauseType] -> Doc Source #
type Rep SPClauseType
Instance details 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))

type SPClause = Named NSPClause Source #

data NSPClause Source #

Constructors

QuanClause [SPTerm] NSPClauseBody
SimpleClause NSPClauseBody
BriefClause TermWsList TermWsList TermWsList

Instances

Instances details

Eq NSPClause Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: NSPClause -> NSPClause -> Bool (/=) :: NSPClause -> NSPClause -> Bool
Data NSPClause Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: NSPClause -> NSPClause -> Ordering (<) :: NSPClause -> NSPClause -> Bool (<=) :: NSPClause -> NSPClause -> Bool (>) :: NSPClause -> NSPClause -> Bool (>=) :: NSPClause -> NSPClause -> Bool max :: NSPClause -> NSPClause -> NSPClause min :: NSPClause -> NSPClause -> NSPClause
Show NSPClause Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> NSPClause -> ShowS show :: NSPClause -> String showList :: [NSPClause] -> ShowS
Generic NSPClause
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep NSPClause :: Type -> Type Methods from :: NSPClause -> Rep NSPClause x to :: Rep NSPClause x -> NSPClause
FromJSON NSPClause
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser NSPClause parseJSONList :: Value -> Parser [NSPClause]
ToJSON NSPClause
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: NSPClause -> Value toEncoding :: NSPClause -> Encoding toJSONList :: [NSPClause] -> Value toEncodingList :: [NSPClause] -> Encoding
ShATermConvertible NSPClause
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: NSPClause -> Doc Source # pretties :: [NSPClause] -> Doc Source #
type Rep NSPClause
Instance details 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

Constructors

NSPClauseBody SPClauseType [SPLiteral]

Instances

Instances details

Eq NSPClauseBody Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: NSPClauseBody -> NSPClauseBody -> Bool (/=) :: NSPClauseBody -> NSPClauseBody -> Bool
Data NSPClauseBody Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> NSPClauseBody -> ShowS show :: NSPClauseBody -> String showList :: [NSPClauseBody] -> ShowS
Generic NSPClauseBody
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep NSPClauseBody :: Type -> Type Methods from :: NSPClauseBody -> Rep NSPClauseBody x to :: Rep NSPClauseBody x -> NSPClauseBody
FromJSON NSPClauseBody
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser NSPClauseBody parseJSONList :: Value -> Parser [NSPClauseBody]
ToJSON NSPClauseBody
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: NSPClauseBody -> Value toEncoding :: NSPClauseBody -> Encoding toJSONList :: [NSPClauseBody] -> Value toEncodingList :: [NSPClauseBody] -> Encoding
ShATermConvertible NSPClauseBody
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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 #

Constructors

TWL [SPTerm] Bool

Instances

Instances details

Eq TermWsList Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: TermWsList -> TermWsList -> Bool (/=) :: TermWsList -> TermWsList -> Bool
Data TermWsList Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> TermWsList -> ShowS show :: TermWsList -> String showList :: [TermWsList] -> ShowS
Generic TermWsList
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep TermWsList :: Type -> Type Methods from :: TermWsList -> Rep TermWsList x to :: Rep TermWsList x -> TermWsList
FromJSON TermWsList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser TermWsList parseJSONList :: Value -> Parser [TermWsList]
ToJSON TermWsList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: TermWsList -> Value toEncoding :: TermWsList -> Encoding toJSONList :: [TermWsList] -> Value toEncodingList :: [TermWsList] -> Encoding
ShATermConvertible TermWsList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: TermWsList -> Doc Source # pretties :: [TermWsList] -> Doc Source #
type Rep TermWsList
Instance details 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)))

data SPTerm Source #

A SPASS Term.

Constructors

SPQuantTerm
Fields quantSym :: SPQuantSym variableList :: [SPTerm] qFormula :: SPTerm
SPComplexTerm
Fields symbol :: SPSymbol arguments :: [SPTerm]

Instances

Instances details

Eq SPTerm Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPTerm -> SPTerm -> Bool (/=) :: SPTerm -> SPTerm -> Bool
Data SPTerm Source #
Instance details Defined in SoftFOL.Sign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SPTerm -> c SPTerm gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SPTerm toConstr :: SPTerm -> Constr dataTypeOf :: SPTerm -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SPTerm) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SPTerm) gmapT :: (forall b. Data b => b -> b) -> SPTerm -> SPTerm gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SPTerm -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SPTerm -> r gmapQ :: (forall d. Data d => d -> u) -> SPTerm -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SPTerm -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SPTerm -> m SPTerm gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SPTerm -> m SPTerm gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SPTerm -> m SPTerm
Ord SPTerm Source #
Instance details Defined in SoftFOL.Sign Methods compare :: SPTerm -> SPTerm -> Ordering (<) :: SPTerm -> SPTerm -> Bool (<=) :: SPTerm -> SPTerm -> Bool (>) :: SPTerm -> SPTerm -> Bool (>=) :: SPTerm -> SPTerm -> Bool max :: SPTerm -> SPTerm -> SPTerm min :: SPTerm -> SPTerm -> SPTerm
Show SPTerm Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPTerm -> ShowS show :: SPTerm -> String showList :: [SPTerm] -> ShowS
Generic SPTerm
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPTerm :: Type -> Type Methods from :: SPTerm -> Rep SPTerm x to :: Rep SPTerm x -> SPTerm
GetRange SPTerm Source #
Instance details Defined in SoftFOL.Sign Methods getRange :: SPTerm -> Range Source # rangeSpan :: SPTerm -> [Pos] Source #
FromJSON SPTerm
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPTerm parseJSONList :: Value -> Parser [SPTerm]
ToJSON SPTerm
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPTerm -> Value toEncoding :: SPTerm -> Encoding toJSONList :: [SPTerm] -> Value toEncodingList :: [SPTerm] -> Encoding
ShATermConvertible SPTerm
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toShATermAux :: ATermTable -> SPTerm -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SPTerm] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SPTerm) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SPTerm])
Pretty SPTerm Source #	Creates a Doc from a SPASS Term.
Instance details Defined in SoftFOL.Print Methods pretty :: SPTerm -> Doc Source # pretties :: [SPTerm] -> Doc Source #
PrintTPTP SPTerm Source #	Creates a Doc from a SoftFOL Term.
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: SPTerm -> Doc Source #
Sentences SoftFOL Sentence Sign SoftFOLMorphism SFSymbol Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods map_sen :: SoftFOL -> SoftFOLMorphism -> Sentence -> Result Sentence Source # simplify_sen :: SoftFOL -> Sign -> Sentence -> Sentence Source # negation :: SoftFOL -> Sentence -> Maybe Sentence Source # print_sign :: SoftFOL -> Sign -> Doc Source # print_named :: SoftFOL -> Named Sentence -> Doc Source # sym_of :: SoftFOL -> Sign -> [Set SFSymbol] Source # mostSymsOf :: SoftFOL -> Sign -> [SFSymbol] Source # symmap_of :: SoftFOL -> SoftFOLMorphism -> EndoMap SFSymbol Source # sym_name :: SoftFOL -> SFSymbol -> Id Source # sym_label :: SoftFOL -> SFSymbol -> Maybe String Source # fullSymName :: SoftFOL -> SFSymbol -> String Source # symKind :: SoftFOL -> SFSymbol -> String Source # symsOfSen :: SoftFOL -> Sign -> Sentence -> [SFSymbol] Source # pair_symbols :: SoftFOL -> SFSymbol -> SFSymbol -> Result SFSymbol Source #
Comorphism SoftFOL2CommonLogic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.SoftFOL2CommonLogic Methods sourceLogic :: SoftFOL2CommonLogic -> SoftFOL Source # sourceSublogic :: SoftFOL2CommonLogic -> () Source # sourceSublogicLossy :: SoftFOL2CommonLogic -> () Source # minSourceTheory :: SoftFOL2CommonLogic -> Maybe (LibName, String) Source # targetLogic :: SoftFOL2CommonLogic -> CommonLogic Source # mapSublogic :: SoftFOL2CommonLogic -> () -> Maybe CommonLogicSL Source # map_theory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source # mapMarkedTheory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source # map_morphism :: SoftFOL2CommonLogic -> SoftFOLMorphism -> Result Morphism Source # map_sentence :: SoftFOL2CommonLogic -> Sign -> Sentence -> Result TEXT_META Source # map_symbol :: SoftFOL2CommonLogic -> Sign -> SFSymbol -> Set Symbol Source # extractModel :: SoftFOL2CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: SoftFOL2CommonLogic -> Bool Source # has_model_expansion :: SoftFOL2CommonLogic -> Bool Source # is_weakly_amalgamable :: SoftFOL2CommonLogic -> Bool Source # constituents :: SoftFOL2CommonLogic -> [String] Source # isInclusionComorphism :: SoftFOL2CommonLogic -> Bool Source # rps :: SoftFOL2CommonLogic -> Bool Source # eps :: SoftFOL2CommonLogic -> Bool Source # isGTC :: SoftFOL2CommonLogic -> Bool Source #
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods parse_basic_sen :: SoftFOL -> Maybe ([TPTP] -> AParser st Sentence) Source # stability :: SoftFOL -> Stability Source # data_logic :: SoftFOL -> Maybe AnyLogic Source # top_sublogic :: SoftFOL -> () Source # all_sublogics :: SoftFOL -> [()] Source # bottomSublogic :: SoftFOL -> Maybe () Source # sublogicDimensions :: SoftFOL -> [[()]] Source # parseSublogic :: SoftFOL -> String -> Maybe () Source # proj_sublogic_epsilon :: SoftFOL -> () -> Sign -> SoftFOLMorphism Source # provers :: SoftFOL -> [Prover Sign Sentence SoftFOLMorphism () ProofTree] Source # default_prover :: SoftFOL -> String Source # cons_checkers :: SoftFOL -> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree] Source # conservativityCheck :: SoftFOL -> [ConservativityChecker Sign Sentence SoftFOLMorphism] Source # empty_proof_tree :: SoftFOL -> ProofTree Source # syntaxTable :: SoftFOL -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: SoftFOL -> Maybe OMCD Source # export_symToOmdoc :: SoftFOL -> NameMap SFSymbol -> SFSymbol -> String -> Result TCElement Source # export_senToOmdoc :: SoftFOL -> NameMap SFSymbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: SoftFOL -> SigMap SFSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result SFSymbol Source # omdocToSen :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source # addOmdocToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source # sublogicOfTheo :: SoftFOL -> (Sign, [Sentence]) -> () Source #
StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods basic_analysis :: SoftFOL -> Maybe (([TPTP], Sign, GlobalAnnos) -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])) Source # sen_analysis :: SoftFOL -> Maybe (([TPTP], Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: SoftFOL -> IRI -> LibName -> [TPTP] -> Sign -> GlobalAnnos -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]) Source # stat_symb_map_items :: SoftFOL -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: SoftFOL -> Sign -> [()] -> Result [()] Source # convertTheory :: SoftFOL -> Maybe ((Sign, [Named Sentence]) -> [TPTP]) Source # ensures_amalgamability :: SoftFOL -> ([CASLAmalgOpt], Gr Sign (Int, SoftFOLMorphism), [(Int, SoftFOLMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: SoftFOL -> SoftFOLMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: SoftFOL -> Gr Sign (Int, SoftFOLMorphism) -> Result (Sign, Map Int SoftFOLMorphism) Source # qualify :: SoftFOL -> SIMPLE_ID -> LibName -> SoftFOLMorphism -> Sign -> Result (SoftFOLMorphism, [Named Sentence]) Source # symbol_to_raw :: SoftFOL -> SFSymbol -> () Source # id_to_raw :: SoftFOL -> Id -> () Source # matches :: SoftFOL -> SFSymbol -> () -> Bool Source # empty_signature :: SoftFOL -> Sign Source # add_symb_to_sign :: SoftFOL -> Sign -> SFSymbol -> Result Sign Source # signature_union :: SoftFOL -> Sign -> Sign -> Result Sign Source # signatureDiff :: SoftFOL -> Sign -> Sign -> Result Sign Source # intersection :: SoftFOL -> Sign -> Sign -> Result Sign Source # final_union :: SoftFOL -> Sign -> Sign -> Result Sign Source # morphism_union :: SoftFOL -> SoftFOLMorphism -> SoftFOLMorphism -> Result SoftFOLMorphism Source # is_subsig :: SoftFOL -> Sign -> Sign -> Bool Source # subsig_inclusion :: SoftFOL -> Sign -> Sign -> Result SoftFOLMorphism Source # generated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source # cogenerated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source # induced_from_morphism :: SoftFOL -> EndoMap () -> Sign -> Result SoftFOLMorphism Source # induced_from_to_morphism :: SoftFOL -> EndoMap () -> ExtSign Sign SFSymbol -> ExtSign Sign SFSymbol -> Result SoftFOLMorphism Source # is_transportable :: SoftFOL -> SoftFOLMorphism -> Bool Source # is_injective :: SoftFOL -> SoftFOLMorphism -> Bool Source # theory_to_taxonomy :: SoftFOL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: SoftFOL -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap SFSymbol -> EndoMap SFSymbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source # equiv2cospan :: SoftFOL -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source # extract_module :: SoftFOL -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #
type Rep SPTerm
Instance details Defined in SoftFOL.ATC_SoftFOL type Rep SPTerm = D1 ('MetaData "SPTerm" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "SPQuantTerm" 'PrefixI 'True) (S1 ('MetaSel ('Just "quantSym") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPQuantSym) :: (S1 ('MetaSel ('Just "variableList") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPTerm]) :: S1 ('MetaSel ('Just "qFormula") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPTerm))) :+: C1 ('MetaCons "SPComplexTerm" 'PrefixI 'True) (S1 ('MetaSel ('Just "symbol") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPSymbol) :*: S1 ('MetaSel ('Just "arguments") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SPTerm])))

data FileName Source #

Constructors

FileName String

Instances

Instances details

Data FileName Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> FileName -> ShowS show :: FileName -> String showList :: [FileName] -> ShowS
Generic FileName
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep FileName :: Type -> Type Methods from :: FileName -> Rep FileName x to :: Rep FileName x -> FileName
FromJSON FileName
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser FileName parseJSONList :: Value -> Parser [FileName]
ToJSON FileName
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: FileName -> Value toEncoding :: FileName -> Encoding toJSONList :: [FileName] -> Value toEncodingList :: [FileName] -> Encoding
ShATermConvertible FileName
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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)))

data FormKind Source #

Constructors

FofKind
CnfKind
FotKind

Instances

Instances details

Data FormKind Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> FormKind -> ShowS show :: FormKind -> String showList :: [FormKind] -> ShowS
Generic FormKind
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep FormKind :: Type -> Type Methods from :: FormKind -> Rep FormKind x to :: Rep FormKind x -> FormKind
FromJSON FormKind
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser FormKind parseJSONList :: Value -> Parser [FormKind]
ToJSON FormKind
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: FormKind -> Value toEncoding :: FormKind -> Encoding toJSONList :: [FormKind] -> Value toEncodingList :: [FormKind] -> Encoding
ShATermConvertible FormKind
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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)))

data Role Source #

Constructors

Axiom
Hypothesis
Definition
Assumption
Lemma
Theorem
Conjecture
Negated_conjecture
Plain
Fi_domain
Fi_functors
Fi_predicates
Type
Unknown

Instances

Instances details

Data Role Source #
Instance details Defined in SoftFOL.Sign Methods 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 toConstr :: Role -> Constr 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> Role -> ShowS show :: Role -> String showList :: [Role] -> ShowS
Generic Role
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep Role :: Type -> Type Methods from :: Role -> Rep Role x to :: Rep Role x -> Role
FromJSON Role
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser Role parseJSONList :: Value -> Parser [Role]
ToJSON Role
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: Role -> Value toEncoding :: Role -> Encoding toJSONList :: [Role] -> Value toEncodingList :: [Role] -> Encoding
ShATermConvertible Role
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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)))))

data Name Source #

Constructors

Name String

Instances

Instances details

Data Name Source #
Instance details Defined in SoftFOL.Sign Methods 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 toConstr :: Name -> Constr 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> Name -> ShowS show :: Name -> String showList :: [Name] -> ShowS
Generic Name
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep Name :: Type -> Type Methods from :: Name -> Rep Name x to :: Rep Name x -> Name
FromJSON Name
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser Name parseJSONList :: Value -> Parser [Name]
ToJSON Name
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: Name -> Value toEncoding :: Name -> Encoding toJSONList :: [Name] -> Value toEncodingList :: [Name] -> Encoding
ShATermConvertible Name
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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)))

data Annos Source #

Constructors

Annos Source (Maybe Info)

Instances

Instances details

Data Annos Source #
Instance details Defined in SoftFOL.Sign Methods 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 toConstr :: Annos -> Constr 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> Annos -> ShowS show :: Annos -> String showList :: [Annos] -> ShowS
Generic Annos
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep Annos :: Type -> Type Methods from :: Annos -> Rep Annos x to :: Rep Annos x -> Annos
FromJSON Annos
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser Annos parseJSONList :: Value -> Parser [Annos]
ToJSON Annos
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: Annos -> Value toEncoding :: Annos -> Encoding toJSONList :: [Annos] -> Value toEncodingList :: [Annos] -> Encoding
ShATermConvertible Annos
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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))))

data Source Source #

Constructors

Source GenTerm

Instances

Instances details

Data Source Source #
Instance details Defined in SoftFOL.Sign Methods 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 toConstr :: Source -> Constr 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> Source -> ShowS show :: Source -> String showList :: [Source] -> ShowS
Generic Source
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep Source :: Type -> Type Methods from :: Source -> Rep Source x to :: Rep Source x -> Source
FromJSON Source
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser Source parseJSONList :: Value -> Parser [Source]
ToJSON Source
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: Source -> Value toEncoding :: Source -> Encoding toJSONList :: [Source] -> Value toEncodingList :: [Source] -> Encoding
ShATermConvertible Source
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details Defined in SoftFOL.ATC_SoftFOL type Rep Source = D1 ('MetaData "Source" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "Source" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GenTerm)))

data AWord Source #

Constructors

AWord String

Instances

Instances details

Data AWord Source #
Instance details Defined in SoftFOL.Sign Methods 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 toConstr :: AWord -> Constr 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> AWord -> ShowS show :: AWord -> String showList :: [AWord] -> ShowS
Generic AWord
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep AWord :: Type -> Type Methods from :: AWord -> Rep AWord x to :: Rep AWord x -> AWord
FromJSON AWord
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser AWord parseJSONList :: Value -> Parser [AWord]
ToJSON AWord
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: AWord -> Value toEncoding :: AWord -> Encoding toJSONList :: [AWord] -> Value toEncodingList :: [AWord] -> Encoding
ShATermConvertible AWord
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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)))

data GenTerm Source #

Constructors

GenTerm GenData (Maybe GenTerm)
GenTermList [GenTerm]

Instances

Instances details

Data GenTerm Source #
Instance details Defined in SoftFOL.Sign Methods 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 toConstr :: GenTerm -> Constr 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> GenTerm -> ShowS show :: GenTerm -> String showList :: [GenTerm] -> ShowS
Generic GenTerm
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep GenTerm :: Type -> Type Methods from :: GenTerm -> Rep GenTerm x to :: Rep GenTerm x -> GenTerm
FromJSON GenTerm
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser GenTerm parseJSONList :: Value -> Parser [GenTerm]
ToJSON GenTerm
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: GenTerm -> Value toEncoding :: GenTerm -> Encoding toJSONList :: [GenTerm] -> Value toEncodingList :: [GenTerm] -> Encoding
ShATermConvertible GenTerm
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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])))

data GenData Source #

Constructors

GenData AWord [GenTerm]
OtherGenData String
GenFormData FormData

Instances

Instances details

Data GenData Source #
Instance details Defined in SoftFOL.Sign Methods 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 toConstr :: GenData -> Constr 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> GenData -> ShowS show :: GenData -> String showList :: [GenData] -> ShowS
Generic GenData
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep GenData :: Type -> Type Methods from :: GenData -> Rep GenData x to :: Rep GenData x -> GenData
FromJSON GenData
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser GenData parseJSONList :: Value -> Parser [GenData]
ToJSON GenData
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: GenData -> Value toEncoding :: GenData -> Encoding toJSONList :: [GenData] -> Value toEncodingList :: [GenData] -> Encoding
ShATermConvertible GenData
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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))))

data FormData Source #

Constructors

FormData FormKind SPTerm

Instances

Instances details

Data FormData Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> FormData -> ShowS show :: FormData -> String showList :: [FormData] -> ShowS
Generic FormData
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep FormData :: Type -> Type Methods from :: FormData -> Rep FormData x to :: Rep FormData x -> FormData
FromJSON FormData
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser FormData parseJSONList :: Value -> Parser [FormData]
ToJSON FormData
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: FormData -> Value toEncoding :: FormData -> Encoding toJSONList :: [FormData] -> Value toEncodingList :: [FormData] -> Encoding
ShATermConvertible FormData
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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)))

data Info Source #

Constructors

Info [GenTerm]

Instances

Instances details

Data Info Source #
Instance details Defined in SoftFOL.Sign Methods 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 toConstr :: Info -> Constr 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> Info -> ShowS show :: Info -> String showList :: [Info] -> ShowS
Generic Info
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep Info :: Type -> Type Methods from :: Info -> Rep Info x to :: Rep Info x -> Info
FromJSON Info
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser Info parseJSONList :: Value -> Parser [Info]
ToJSON Info
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: Info -> Value toEncoding :: Info -> Encoding toJSONList :: [Info] -> Value toEncodingList :: [Info] -> Encoding
ShATermConvertible Info
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details Defined in SoftFOL.ATC_SoftFOL type Rep Info = D1 ('MetaData "Info" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "Info" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GenTerm])))

data TPTP Source #

Constructors

FormAnno FormKind Name Role SPTerm (Maybe Annos)
Include FileName [Name]
CommentLine String
EmptyLine

Instances

Instances details

Data TPTP Source #
Instance details Defined in SoftFOL.Sign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TPTP -> c TPTP gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TPTP toConstr :: TPTP -> Constr dataTypeOf :: TPTP -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TPTP) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPTP) gmapT :: (forall b. Data b => b -> b) -> TPTP -> TPTP gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPTP -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPTP -> r gmapQ :: (forall d. Data d => d -> u) -> TPTP -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TPTP -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TPTP -> m TPTP gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP -> m TPTP gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TPTP -> m TPTP
Show TPTP Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> TPTP -> ShowS show :: TPTP -> String showList :: [TPTP] -> ShowS
Generic TPTP
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep TPTP :: Type -> Type Methods from :: TPTP -> Rep TPTP x to :: Rep TPTP x -> TPTP
GetRange TPTP Source #
Instance details Defined in SoftFOL.Sign Methods getRange :: TPTP -> Range Source # rangeSpan :: TPTP -> [Pos] Source #
FromJSON TPTP
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser TPTP parseJSONList :: Value -> Parser [TPTP]
ToJSON TPTP
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: TPTP -> Value toEncoding :: TPTP -> Encoding toJSONList :: [TPTP] -> Value toEncodingList :: [TPTP] -> Encoding
ShATermConvertible TPTP
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toShATermAux :: ATermTable -> TPTP -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TPTP] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TPTP) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TPTP])
Pretty TPTP Source #
Instance details Defined in SoftFOL.PrintTPTP Methods pretty :: TPTP -> Doc Source # pretties :: [TPTP] -> Doc Source #
Comorphism SoftFOL2CommonLogic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source #
Instance details Defined in Comorphisms.SoftFOL2CommonLogic Methods sourceLogic :: SoftFOL2CommonLogic -> SoftFOL Source # sourceSublogic :: SoftFOL2CommonLogic -> () Source # sourceSublogicLossy :: SoftFOL2CommonLogic -> () Source # minSourceTheory :: SoftFOL2CommonLogic -> Maybe (LibName, String) Source # targetLogic :: SoftFOL2CommonLogic -> CommonLogic Source # mapSublogic :: SoftFOL2CommonLogic -> () -> Maybe CommonLogicSL Source # map_theory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source # mapMarkedTheory :: SoftFOL2CommonLogic -> (Sign, [Named Sentence]) -> Result (Sign0, [Named TEXT_META]) Source # map_morphism :: SoftFOL2CommonLogic -> SoftFOLMorphism -> Result Morphism Source # map_sentence :: SoftFOL2CommonLogic -> Sign -> Sentence -> Result TEXT_META Source # map_symbol :: SoftFOL2CommonLogic -> Sign -> SFSymbol -> Set Symbol Source # extractModel :: SoftFOL2CommonLogic -> Sign -> ProofTree -> Result (Sign, [Named Sentence]) Source # is_model_transportable :: SoftFOL2CommonLogic -> Bool Source # has_model_expansion :: SoftFOL2CommonLogic -> Bool Source # is_weakly_amalgamable :: SoftFOL2CommonLogic -> Bool Source # constituents :: SoftFOL2CommonLogic -> [String] Source # isInclusionComorphism :: SoftFOL2CommonLogic -> Bool Source # rps :: SoftFOL2CommonLogic -> Bool Source # eps :: SoftFOL2CommonLogic -> Bool Source # isGTC :: SoftFOL2CommonLogic -> Bool Source #
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods parse_basic_sen :: SoftFOL -> Maybe ([TPTP] -> AParser st Sentence) Source # stability :: SoftFOL -> Stability Source # data_logic :: SoftFOL -> Maybe AnyLogic Source # top_sublogic :: SoftFOL -> () Source # all_sublogics :: SoftFOL -> [()] Source # bottomSublogic :: SoftFOL -> Maybe () Source # sublogicDimensions :: SoftFOL -> [[()]] Source # parseSublogic :: SoftFOL -> String -> Maybe () Source # proj_sublogic_epsilon :: SoftFOL -> () -> Sign -> SoftFOLMorphism Source # provers :: SoftFOL -> [Prover Sign Sentence SoftFOLMorphism () ProofTree] Source # default_prover :: SoftFOL -> String Source # cons_checkers :: SoftFOL -> [ConsChecker Sign Sentence () SoftFOLMorphism ProofTree] Source # conservativityCheck :: SoftFOL -> [ConservativityChecker Sign Sentence SoftFOLMorphism] Source # empty_proof_tree :: SoftFOL -> ProofTree Source # syntaxTable :: SoftFOL -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: SoftFOL -> Maybe OMCD Source # export_symToOmdoc :: SoftFOL -> NameMap SFSymbol -> SFSymbol -> String -> Result TCElement Source # export_senToOmdoc :: SoftFOL -> NameMap SFSymbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: SoftFOL -> SigMap SFSymbol -> Sign -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result SFSymbol Source # omdocToSen :: SoftFOL -> SigMapI SFSymbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source # addOmdocToTheory :: SoftFOL -> SigMapI SFSymbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source # sublogicOfTheo :: SoftFOL -> (Sign, [Sentence]) -> () Source #
Syntax SoftFOL [TPTP] SFSymbol () () Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods parsersAndPrinters :: SoftFOL -> Map String (PrefixMap -> AParser st [TPTP], [TPTP] -> Doc) Source # parse_basic_spec :: SoftFOL -> Maybe (PrefixMap -> AParser st [TPTP]) Source # parseSingleSymbItem :: SoftFOL -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: SoftFOL -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: SoftFOL -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: SoftFOL -> [TPTP] -> Item Source # symb_items_name :: SoftFOL -> () -> [String] Source #
StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source #
Instance details Defined in SoftFOL.Logic_SoftFOL Methods basic_analysis :: SoftFOL -> Maybe (([TPTP], Sign, GlobalAnnos) -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence])) Source # sen_analysis :: SoftFOL -> Maybe (([TPTP], Sign, Sentence) -> Result Sentence) Source # extBasicAnalysis :: SoftFOL -> IRI -> LibName -> [TPTP] -> Sign -> GlobalAnnos -> Result ([TPTP], ExtSign Sign SFSymbol, [Named Sentence]) Source # stat_symb_map_items :: SoftFOL -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source # stat_symb_items :: SoftFOL -> Sign -> [()] -> Result [()] Source # convertTheory :: SoftFOL -> Maybe ((Sign, [Named Sentence]) -> [TPTP]) Source # ensures_amalgamability :: SoftFOL -> ([CASLAmalgOpt], Gr Sign (Int, SoftFOLMorphism), [(Int, SoftFOLMorphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: SoftFOL -> SoftFOLMorphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source # signature_colimit :: SoftFOL -> Gr Sign (Int, SoftFOLMorphism) -> Result (Sign, Map Int SoftFOLMorphism) Source # qualify :: SoftFOL -> SIMPLE_ID -> LibName -> SoftFOLMorphism -> Sign -> Result (SoftFOLMorphism, [Named Sentence]) Source # symbol_to_raw :: SoftFOL -> SFSymbol -> () Source # id_to_raw :: SoftFOL -> Id -> () Source # matches :: SoftFOL -> SFSymbol -> () -> Bool Source # empty_signature :: SoftFOL -> Sign Source # add_symb_to_sign :: SoftFOL -> Sign -> SFSymbol -> Result Sign Source # signature_union :: SoftFOL -> Sign -> Sign -> Result Sign Source # signatureDiff :: SoftFOL -> Sign -> Sign -> Result Sign Source # intersection :: SoftFOL -> Sign -> Sign -> Result Sign Source # final_union :: SoftFOL -> Sign -> Sign -> Result Sign Source # morphism_union :: SoftFOL -> SoftFOLMorphism -> SoftFOLMorphism -> Result SoftFOLMorphism Source # is_subsig :: SoftFOL -> Sign -> Sign -> Bool Source # subsig_inclusion :: SoftFOL -> Sign -> Sign -> Result SoftFOLMorphism Source # generated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source # cogenerated_sign :: SoftFOL -> Set SFSymbol -> Sign -> Result SoftFOLMorphism Source # induced_from_morphism :: SoftFOL -> EndoMap () -> Sign -> Result SoftFOLMorphism Source # induced_from_to_morphism :: SoftFOL -> EndoMap () -> ExtSign Sign SFSymbol -> ExtSign Sign SFSymbol -> Result SoftFOLMorphism Source # is_transportable :: SoftFOL -> SoftFOLMorphism -> Bool Source # is_injective :: SoftFOL -> SoftFOLMorphism -> Bool Source # theory_to_taxonomy :: SoftFOL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: SoftFOL -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap SFSymbol -> EndoMap SFSymbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source # equiv2cospan :: SoftFOL -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap SFSymbol, EndoMap SFSymbol) Source # extract_module :: SoftFOL -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #
type Rep TPTP
Instance details Defined in SoftFOL.ATC_SoftFOL type Rep TPTP = D1 ('MetaData "TPTP" "SoftFOL.Sign" "main" 'False) ((C1 ('MetaCons "FormAnno" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FormKind) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Role) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPTerm) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Annos))))) :+: C1 ('MetaCons "Include" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))) :+: (C1 ('MetaCons "CommentLine" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "EmptyLine" 'PrefixI 'False) (U1 :: Type -> Type)))

data SPLiteral Source #

Literals for SPASS CNF and DNF (the boolean indicates a negated literal).

Constructors

SPLiteral Bool SPSymbol

Instances

Instances details

Eq SPLiteral Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPLiteral -> SPLiteral -> Bool (/=) :: SPLiteral -> SPLiteral -> Bool
Data SPLiteral Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: SPLiteral -> SPLiteral -> Ordering (<) :: SPLiteral -> SPLiteral -> Bool (<=) :: SPLiteral -> SPLiteral -> Bool (>) :: SPLiteral -> SPLiteral -> Bool (>=) :: SPLiteral -> SPLiteral -> Bool max :: SPLiteral -> SPLiteral -> SPLiteral min :: SPLiteral -> SPLiteral -> SPLiteral
Show SPLiteral Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPLiteral -> ShowS show :: SPLiteral -> String showList :: [SPLiteral] -> ShowS
Generic SPLiteral
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPLiteral :: Type -> Type Methods from :: SPLiteral -> Rep SPLiteral x to :: Rep SPLiteral x -> SPLiteral
FromJSON SPLiteral
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPLiteral parseJSONList :: Value -> Parser [SPLiteral]
ToJSON SPLiteral
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPLiteral -> Value toEncoding :: SPLiteral -> Encoding toJSONList :: [SPLiteral] -> Value toEncodingList :: [SPLiteral] -> Encoding
ShATermConvertible SPLiteral
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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)))

toLiteral :: MonadFail m => SPTerm -> m SPLiteral Source #

data SPQuantSym Source #

SPASS Quantifier Symbols.

Constructors

SPForall
SPExists
SPCustomQuantSym SPIdentifier

Instances

Instances details

Eq SPQuantSym Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPQuantSym -> SPQuantSym -> Bool (/=) :: SPQuantSym -> SPQuantSym -> Bool
Data SPQuantSym Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPQuantSym -> ShowS show :: SPQuantSym -> String showList :: [SPQuantSym] -> ShowS
Generic SPQuantSym
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPQuantSym :: Type -> Type Methods from :: SPQuantSym -> Rep SPQuantSym x to :: Rep SPQuantSym x -> SPQuantSym
FromJSON SPQuantSym
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPQuantSym parseJSONList :: Value -> Parser [SPQuantSym]
ToJSON SPQuantSym
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPQuantSym -> Value toEncoding :: SPQuantSym -> Encoding toJSONList :: [SPQuantSym] -> Value toEncodingList :: [SPQuantSym] -> Encoding
ShATermConvertible SPQuantSym
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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.
Instance details Defined in SoftFOL.Print Methods pretty :: SPQuantSym -> Doc Source # pretties :: [SPQuantSym] -> Doc Source #
PrintTPTP SPQuantSym Source #	Creates a Doc from a SoftFOL Quantifier Symbol.
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: SPQuantSym -> Doc Source #
type Rep SPQuantSym
Instance details 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))))

data SPSymbol Source #

SPASS Symbols.

Constructors

SPEqual
SPTrue
SPFalse
SPOr
SPAnd
SPNot
SPImplies
SPImplied
SPEquiv
SPID
SPDiv
SPComp
SPSum
SPConv
SPCustomSymbol SPIdentifier

Instances

Instances details

Eq SPSymbol Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPSymbol -> SPSymbol -> Bool (/=) :: SPSymbol -> SPSymbol -> Bool
Data SPSymbol Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: SPSymbol -> SPSymbol -> Ordering (<) :: SPSymbol -> SPSymbol -> Bool (<=) :: SPSymbol -> SPSymbol -> Bool (>) :: SPSymbol -> SPSymbol -> Bool (>=) :: SPSymbol -> SPSymbol -> Bool max :: SPSymbol -> SPSymbol -> SPSymbol min :: SPSymbol -> SPSymbol -> SPSymbol
Show SPSymbol Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPSymbol -> ShowS show :: SPSymbol -> String showList :: [SPSymbol] -> ShowS
Generic SPSymbol
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPSymbol :: Type -> Type Methods from :: SPSymbol -> Rep SPSymbol x to :: Rep SPSymbol x -> SPSymbol
FromJSON SPSymbol
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPSymbol parseJSONList :: Value -> Parser [SPSymbol]
ToJSON SPSymbol
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPSymbol -> Value toEncoding :: SPSymbol -> Encoding toJSONList :: [SPSymbol] -> Value toEncodingList :: [SPSymbol] -> Encoding
ShATermConvertible SPSymbol
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details Defined in SoftFOL.Print Methods pretty :: SPSymbol -> Doc Source # pretties :: [SPSymbol] -> Doc Source #
PrintTPTP SPSymbol Source #	Creates a Doc from a SoftFOL Symbol.
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: SPSymbol -> Doc Source #
type Rep SPSymbol
Instance details 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

Constructors

SPProofList
Fields proofType :: Maybe SPProofType plAssocList :: SPAssocList step :: [SPProofStep]

Instances

Instances details

Eq SPProofList Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPProofList -> SPProofList -> Bool (/=) :: SPProofList -> SPProofList -> Bool
Data SPProofList Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPProofList -> ShowS show :: SPProofList -> String showList :: [SPProofList] -> ShowS
Generic SPProofList
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPProofList :: Type -> Type Methods from :: SPProofList -> Rep SPProofList x to :: Rep SPProofList x -> SPProofList
FromJSON SPProofList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPProofList parseJSONList :: Value -> Parser [SPProofList]
ToJSON SPProofList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPProofList -> Value toEncoding :: SPProofList -> Encoding toJSONList :: [SPProofList] -> Value toEncodingList :: [SPProofList] -> Encoding
ShATermConvertible SPProofList
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPProofList -> Doc Source # pretties :: [SPProofList] -> Doc Source #
type Rep SPProofList
Instance details 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 #

Constructors

SPProofStep
Fields reference :: SPReference result :: SPResult ruleAppl :: SPRuleAppl parentList :: [SPParent] stepAssocList :: SPAssocList

Instances

Instances details

Eq SPProofStep Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPProofStep -> SPProofStep -> Bool (/=) :: SPProofStep -> SPProofStep -> Bool
Data SPProofStep Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPProofStep -> ShowS show :: SPProofStep -> String showList :: [SPProofStep] -> ShowS
Generic SPProofStep
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPProofStep :: Type -> Type Methods from :: SPProofStep -> Rep SPProofStep x to :: Rep SPProofStep x -> SPProofStep
FromJSON SPProofStep
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPProofStep parseJSONList :: Value -> Parser [SPProofStep]
ToJSON SPProofStep
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPProofStep -> Value toEncoding :: SPProofStep -> Encoding toJSONList :: [SPProofStep] -> Value toEncodingList :: [SPProofStep] -> Encoding
ShATermConvertible SPProofStep
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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
Instance details 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 #

Constructors

PRefTerm SPTerm

Instances

Instances details

Eq SPReference Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPReference -> SPReference -> Bool (/=) :: SPReference -> SPReference -> Bool
Data SPReference Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPReference -> ShowS show :: SPReference -> String showList :: [SPReference] -> ShowS
Generic SPReference
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPReference :: Type -> Type Methods from :: SPReference -> Rep SPReference x to :: Rep SPReference x -> SPReference
FromJSON SPReference
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPReference parseJSONList :: Value -> Parser [SPReference]
ToJSON SPReference
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPReference -> Value toEncoding :: SPReference -> Encoding toJSONList :: [SPReference] -> Value toEncodingList :: [SPReference] -> Encoding
ShATermConvertible SPReference
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPReference -> Doc Source # pretties :: [SPReference] -> Doc Source #
type Rep SPReference
Instance details 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)))

data SPResult Source #

Constructors

PResTerm SPTerm

Instances

Instances details

Eq SPResult Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPResult -> SPResult -> Bool (/=) :: SPResult -> SPResult -> Bool
Data SPResult Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: SPResult -> SPResult -> Ordering (<) :: SPResult -> SPResult -> Bool (<=) :: SPResult -> SPResult -> Bool (>) :: SPResult -> SPResult -> Bool (>=) :: SPResult -> SPResult -> Bool max :: SPResult -> SPResult -> SPResult min :: SPResult -> SPResult -> SPResult
Show SPResult Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPResult -> ShowS show :: SPResult -> String showList :: [SPResult] -> ShowS
Generic SPResult
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPResult :: Type -> Type Methods from :: SPResult -> Rep SPResult x to :: Rep SPResult x -> SPResult
FromJSON SPResult
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPResult parseJSONList :: Value -> Parser [SPResult]
ToJSON SPResult
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPResult -> Value toEncoding :: SPResult -> Encoding toJSONList :: [SPResult] -> Value toEncodingList :: [SPResult] -> Encoding
ShATermConvertible SPResult
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPResult -> Doc Source # pretties :: [SPResult] -> Doc Source #
type Rep SPResult
Instance details Defined in SoftFOL.ATC_SoftFOL type Rep SPResult = D1 ('MetaData "SPResult" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "PResTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPTerm)))

data SPRuleAppl Source #

Constructors

PRuleTerm SPTerm
PRuleUser SPUserRuleAppl

Instances

Instances details

Eq SPRuleAppl Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPRuleAppl -> SPRuleAppl -> Bool (/=) :: SPRuleAppl -> SPRuleAppl -> Bool
Data SPRuleAppl Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPRuleAppl -> ShowS show :: SPRuleAppl -> String showList :: [SPRuleAppl] -> ShowS
Generic SPRuleAppl
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPRuleAppl :: Type -> Type Methods from :: SPRuleAppl -> Rep SPRuleAppl x to :: Rep SPRuleAppl x -> SPRuleAppl
FromJSON SPRuleAppl
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPRuleAppl parseJSONList :: Value -> Parser [SPRuleAppl]
ToJSON SPRuleAppl
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPRuleAppl -> Value toEncoding :: SPRuleAppl -> Encoding toJSONList :: [SPRuleAppl] -> Value toEncodingList :: [SPRuleAppl] -> Encoding
ShATermConvertible SPRuleAppl
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPRuleAppl -> Doc Source # pretties :: [SPRuleAppl] -> Doc Source #
type Rep SPRuleAppl
Instance details 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 #

Constructors

GeR
SpL
SpR
EqF
Rew
Obv
EmS
SoR
EqR
Mpm
SPm
OPm
SHy
OHy
URR
Fac
Spt
Inp
Con
RRE
SSi
ClR
UnC
Ter

Instances

Instances details

Eq SPUserRuleAppl Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPUserRuleAppl -> SPUserRuleAppl -> Bool (/=) :: SPUserRuleAppl -> SPUserRuleAppl -> Bool
Data SPUserRuleAppl Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPUserRuleAppl -> ShowS show :: SPUserRuleAppl -> String showList :: [SPUserRuleAppl] -> ShowS
Generic SPUserRuleAppl
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPUserRuleAppl :: Type -> Type Methods from :: SPUserRuleAppl -> Rep SPUserRuleAppl x to :: Rep SPUserRuleAppl x -> SPUserRuleAppl
FromJSON SPUserRuleAppl
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPUserRuleAppl parseJSONList :: Value -> Parser [SPUserRuleAppl]
ToJSON SPUserRuleAppl
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPUserRuleAppl -> Value toEncoding :: SPUserRuleAppl -> Encoding toJSONList :: [SPUserRuleAppl] -> Value toEncodingList :: [SPUserRuleAppl] -> Encoding
ShATermConvertible SPUserRuleAppl
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPUserRuleAppl -> Doc Source # pretties :: [SPUserRuleAppl] -> Doc Source #
type Rep SPUserRuleAppl
Instance details 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))))))

data SPParent Source #

Constructors

PParTerm SPTerm

Instances

Instances details

Eq SPParent Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPParent -> SPParent -> Bool (/=) :: SPParent -> SPParent -> Bool
Data SPParent Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: SPParent -> SPParent -> Ordering (<) :: SPParent -> SPParent -> Bool (<=) :: SPParent -> SPParent -> Bool (>) :: SPParent -> SPParent -> Bool (>=) :: SPParent -> SPParent -> Bool max :: SPParent -> SPParent -> SPParent min :: SPParent -> SPParent -> SPParent
Show SPParent Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPParent -> ShowS show :: SPParent -> String showList :: [SPParent] -> ShowS
Generic SPParent
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPParent :: Type -> Type Methods from :: SPParent -> Rep SPParent x to :: Rep SPParent x -> SPParent
FromJSON SPParent
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPParent parseJSONList :: Value -> Parser [SPParent]
ToJSON SPParent
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPParent -> Value toEncoding :: SPParent -> Encoding toJSONList :: [SPParent] -> Value toEncodingList :: [SPParent] -> Encoding
ShATermConvertible SPParent
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPParent -> Doc Source # pretties :: [SPParent] -> Doc Source #
type Rep SPParent
Instance details Defined in SoftFOL.ATC_SoftFOL type Rep SPParent = D1 ('MetaData "SPParent" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "PParTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPTerm)))

type SPAssocList = Map SPKey SPValue Source #

data SPKey Source #

Constructors

PKeyTerm SPTerm

Instances

Instances details

Eq SPKey Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPKey -> SPKey -> Bool (/=) :: SPKey -> SPKey -> Bool
Data SPKey Source #
Instance details Defined in SoftFOL.Sign Methods 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 toConstr :: SPKey -> Constr 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: SPKey -> SPKey -> Ordering (<) :: SPKey -> SPKey -> Bool (<=) :: SPKey -> SPKey -> Bool (>) :: SPKey -> SPKey -> Bool (>=) :: SPKey -> SPKey -> Bool max :: SPKey -> SPKey -> SPKey min :: SPKey -> SPKey -> SPKey
Show SPKey Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPKey -> ShowS show :: SPKey -> String showList :: [SPKey] -> ShowS
Generic SPKey
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPKey :: Type -> Type Methods from :: SPKey -> Rep SPKey x to :: Rep SPKey x -> SPKey
FromJSON SPKey
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPKey parseJSONList :: Value -> Parser [SPKey]
ToJSON SPKey
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPKey -> Value toEncoding :: SPKey -> Encoding toJSONList :: [SPKey] -> Value toEncodingList :: [SPKey] -> Encoding
ShATermConvertible SPKey
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPKey -> Doc Source # pretties :: [SPKey] -> Doc Source #
type Rep SPKey
Instance details Defined in SoftFOL.ATC_SoftFOL type Rep SPKey = D1 ('MetaData "SPKey" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "PKeyTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPTerm)))

data SPValue Source #

Constructors

PValTerm SPTerm

Instances

Instances details

Eq SPValue Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPValue -> SPValue -> Bool (/=) :: SPValue -> SPValue -> Bool
Data SPValue Source #
Instance details Defined in SoftFOL.Sign Methods 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 toConstr :: SPValue -> Constr 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: SPValue -> SPValue -> Ordering (<) :: SPValue -> SPValue -> Bool (<=) :: SPValue -> SPValue -> Bool (>) :: SPValue -> SPValue -> Bool (>=) :: SPValue -> SPValue -> Bool max :: SPValue -> SPValue -> SPValue min :: SPValue -> SPValue -> SPValue
Show SPValue Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPValue -> ShowS show :: SPValue -> String showList :: [SPValue] -> ShowS
Generic SPValue
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPValue :: Type -> Type Methods from :: SPValue -> Rep SPValue x to :: Rep SPValue x -> SPValue
FromJSON SPValue
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPValue parseJSONList :: Value -> Parser [SPValue]
ToJSON SPValue
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPValue -> Value toEncoding :: SPValue -> Encoding toJSONList :: [SPValue] -> Value toEncodingList :: [SPValue] -> Encoding
ShATermConvertible SPValue
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPValue -> Doc Source # pretties :: [SPValue] -> Doc Source #
type Rep SPValue
Instance details Defined in SoftFOL.ATC_SoftFOL type Rep SPValue = D1 ('MetaData "SPValue" "SoftFOL.Sign" "main" 'False) (C1 ('MetaCons "PValTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SPTerm)))

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

typedVarTerm Source #

Arguments

:: SPIdentifier	Variable symbol: v
-> SPIdentifier	Sort symbol: s
-> SPTerm	Term: s(v)

spTerms :: [SPIdentifier] -> [SPTerm] Source #

spSym :: SPIdentifier -> SPSymbol Source #

compTerm :: SPSymbol -> [SPTerm] -> SPTerm Source #

simpTerm :: SPSymbol -> SPTerm Source #

mkConj :: SPTerm -> SPTerm -> SPTerm Source #

mkDisj :: SPTerm -> SPTerm -> SPTerm Source #

mkEq :: SPTerm -> SPTerm -> SPTerm 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.

Constructors

SPDescription
Fields name :: String author :: String version :: Maybe String logic :: Maybe String status :: SPLogState desc :: String date :: Maybe String

Instances

Instances details

Eq SPDescription Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPDescription -> SPDescription -> Bool (/=) :: SPDescription -> SPDescription -> Bool
Data SPDescription Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPDescription -> ShowS show :: SPDescription -> String showList :: [SPDescription] -> ShowS
Generic SPDescription
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPDescription :: Type -> Type Methods from :: SPDescription -> Rep SPDescription x to :: Rep SPDescription x -> SPDescription
FromJSON SPDescription
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPDescription parseJSONList :: Value -> Parser [SPDescription]
ToJSON SPDescription
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPDescription -> Value toEncoding :: SPDescription -> Encoding toJSONList :: [SPDescription] -> Value toEncodingList :: [SPDescription] -> Encoding
ShATermConvertible SPDescription
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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.
Instance details Defined in SoftFOL.Print Methods pretty :: SPDescription -> Doc Source # pretties :: [SPDescription] -> Doc Source #
PrintTPTP SPDescription Source #	Creates a Doc from a SoftFOL description.
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: SPDescription -> Doc Source #
type Rep SPDescription
Instance details 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.

Constructors

SPStateSatisfiable
SPStateUnsatisfiable
SPStateUnknown

Instances

Instances details

Eq SPLogState Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPLogState -> SPLogState -> Bool (/=) :: SPLogState -> SPLogState -> Bool
Data SPLogState Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPLogState -> ShowS show :: SPLogState -> String showList :: [SPLogState] -> ShowS
Generic SPLogState
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPLogState :: Type -> Type Methods from :: SPLogState -> Rep SPLogState x to :: Rep SPLogState x -> SPLogState
FromJSON SPLogState
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPLogState parseJSONList :: Value -> Parser [SPLogState]
ToJSON SPLogState
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPLogState -> Value toEncoding :: SPLogState -> Encoding toJSONList :: [SPLogState] -> Value toEncodingList :: [SPLogState] -> Encoding
ShATermConvertible SPLogState
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 `SPLogState`.
Instance details Defined in SoftFOL.Print Methods pretty :: SPLogState -> Doc Source # pretties :: [SPLogState] -> Doc Source #
PrintTPTP SPLogState Source #	Creates a Doc from an `SPLogState`.
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: SPLogState -> Doc Source #
type Rep SPLogState
Instance details 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

data SPSetting Source #

New impelmentation of Settings. See spass input syntax Version 1.5.

Constructors

SPGeneralSettings
Fields entries :: [SPHypothesis]
SPSettings
Fields settingName :: SPSettingLabel settingBody :: [SPSettingBody]

Instances

Instances details

Eq SPSetting Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPSetting -> SPSetting -> Bool (/=) :: SPSetting -> SPSetting -> Bool
Data SPSetting Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: SPSetting -> SPSetting -> Ordering (<) :: SPSetting -> SPSetting -> Bool (<=) :: SPSetting -> SPSetting -> Bool (>) :: SPSetting -> SPSetting -> Bool (>=) :: SPSetting -> SPSetting -> Bool max :: SPSetting -> SPSetting -> SPSetting min :: SPSetting -> SPSetting -> SPSetting
Show SPSetting Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPSetting -> ShowS show :: SPSetting -> String showList :: [SPSetting] -> ShowS
Generic SPSetting
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPSetting :: Type -> Type Methods from :: SPSetting -> Rep SPSetting x to :: Rep SPSetting x -> SPSetting
FromJSON SPSetting
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPSetting parseJSONList :: Value -> Parser [SPSetting]
ToJSON SPSetting
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPSetting -> Value toEncoding :: SPSetting -> Encoding toJSONList :: [SPSetting] -> Value toEncodingList :: [SPSetting] -> Encoding
ShATermConvertible SPSetting
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPSetting -> Doc Source # pretties :: [SPSetting] -> Doc Source #
PrintTPTP SPSetting Source #
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: SPSetting -> Doc Source #
type Rep SPSetting
Instance details 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 #

Constructors

SPClauseRelation [SPCRBIND]
SPFlag String [String]

Instances

Instances details

Eq SPSettingBody Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPSettingBody -> SPSettingBody -> Bool (/=) :: SPSettingBody -> SPSettingBody -> Bool
Data SPSettingBody Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPSettingBody -> ShowS show :: SPSettingBody -> String showList :: [SPSettingBody] -> ShowS
Generic SPSettingBody
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPSettingBody :: Type -> Type Methods from :: SPSettingBody -> Rep SPSettingBody x to :: Rep SPSettingBody x -> SPSettingBody
FromJSON SPSettingBody
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPSettingBody parseJSONList :: Value -> Parser [SPSettingBody]
ToJSON SPSettingBody
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPSettingBody -> Value toEncoding :: SPSettingBody -> Encoding toJSONList :: [SPSettingBody] -> Value toEncodingList :: [SPSettingBody] -> Encoding
ShATermConvertible SPSettingBody
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPSettingBody -> Doc Source # pretties :: [SPSettingBody] -> Doc Source #
PrintTPTP SPSettingBody Source #
Instance details Defined in SoftFOL.PrintTPTP Methods printTPTP :: SPSettingBody -> Doc Source #
type Rep SPSettingBody
Instance details 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 #

Constructors

SPHypothesis [SPIdentifier]

Instances

Instances details

Eq SPHypothesis Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPHypothesis -> SPHypothesis -> Bool (/=) :: SPHypothesis -> SPHypothesis -> Bool
Data SPHypothesis Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPHypothesis -> ShowS show :: SPHypothesis -> String showList :: [SPHypothesis] -> ShowS
Generic SPHypothesis
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPHypothesis :: Type -> Type Methods from :: SPHypothesis -> Rep SPHypothesis x to :: Rep SPHypothesis x -> SPHypothesis
FromJSON SPHypothesis
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPHypothesis parseJSONList :: Value -> Parser [SPHypothesis]
ToJSON SPHypothesis
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPHypothesis -> Value toEncoding :: SPHypothesis -> Encoding toJSONList :: [SPHypothesis] -> Value toEncodingList :: [SPHypothesis] -> Encoding
ShATermConvertible SPHypothesis
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPHypothesis -> Doc Source # pretties :: [SPHypothesis] -> Doc Source #
type Rep SPHypothesis
Instance details 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 #

Constructors

KIV
LEM
OTTER
PROTEIN
SATURATE
ThreeTAP
SETHEO
SPASS

Instances

Instances details

Eq SPSettingLabel Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPSettingLabel -> SPSettingLabel -> Bool (/=) :: SPSettingLabel -> SPSettingLabel -> Bool
Data SPSettingLabel Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPSettingLabel -> ShowS show :: SPSettingLabel -> String showList :: [SPSettingLabel] -> ShowS
Generic SPSettingLabel
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPSettingLabel :: Type -> Type Methods from :: SPSettingLabel -> Rep SPSettingLabel x to :: Rep SPSettingLabel x -> SPSettingLabel
FromJSON SPSettingLabel
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPSettingLabel parseJSONList :: Value -> Parser [SPSettingLabel]
ToJSON SPSettingLabel
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPSettingLabel -> Value toEncoding :: SPSettingLabel -> Encoding toJSONList :: [SPSettingLabel] -> Value toEncodingList :: [SPSettingLabel] -> Encoding
ShATermConvertible SPSettingLabel
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPSettingLabel -> Doc Source # pretties :: [SPSettingLabel] -> Doc Source #
type Rep SPSettingLabel
Instance details 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 #

data SPCRBIND Source #

A Tupel of the Clause Relation

Constructors

SPCRBIND
Fields clauseSPR :: String formulaSPR :: String

Instances

Instances details

Eq SPCRBIND Source #
Instance details Defined in SoftFOL.Sign Methods (==) :: SPCRBIND -> SPCRBIND -> Bool (/=) :: SPCRBIND -> SPCRBIND -> Bool
Data SPCRBIND Source #
Instance details Defined in SoftFOL.Sign Methods 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 #
Instance details Defined in SoftFOL.Sign Methods compare :: SPCRBIND -> SPCRBIND -> Ordering (<) :: SPCRBIND -> SPCRBIND -> Bool (<=) :: SPCRBIND -> SPCRBIND -> Bool (>) :: SPCRBIND -> SPCRBIND -> Bool (>=) :: SPCRBIND -> SPCRBIND -> Bool max :: SPCRBIND -> SPCRBIND -> SPCRBIND min :: SPCRBIND -> SPCRBIND -> SPCRBIND
Show SPCRBIND Source #
Instance details Defined in SoftFOL.Sign Methods showsPrec :: Int -> SPCRBIND -> ShowS show :: SPCRBIND -> String showList :: [SPCRBIND] -> ShowS
Generic SPCRBIND
Instance details Defined in SoftFOL.ATC_SoftFOL Associated Types type Rep SPCRBIND :: Type -> Type Methods from :: SPCRBIND -> Rep SPCRBIND x to :: Rep SPCRBIND x -> SPCRBIND
FromJSON SPCRBIND
Instance details Defined in SoftFOL.ATC_SoftFOL Methods parseJSON :: Value -> Parser SPCRBIND parseJSONList :: Value -> Parser [SPCRBIND]
ToJSON SPCRBIND
Instance details Defined in SoftFOL.ATC_SoftFOL Methods toJSON :: SPCRBIND -> Value toEncoding :: SPCRBIND -> Encoding toJSONList :: [SPCRBIND] -> Value toEncodingList :: [SPCRBIND] -> Encoding
ShATermConvertible SPCRBIND
Instance details Defined in SoftFOL.ATC_SoftFOL Methods 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 #
Instance details Defined in SoftFOL.Print Methods pretty :: SPCRBIND -> Doc Source # pretties :: [SPCRBIND] -> Doc Source #
type Rep SPCRBIND
Instance details 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

GeR
SpL
SpR
EqF
Rew
Obv
EmS
SoR
EqR
Mpm
SPm
OPm
SHy
OHy
URR
Fac
Spt
Inp
Con
RRE
SSi
ClR
UnC
Ter

GeR
SpL
SpR
EqF
Rew
Obv
EmS
SoR
EqR
Mpm
SPm
OPm
SHy
OHy
URR
Fac
Spt
Inp
Con
RRE
SSi
ClR
UnC
Ter

GeR
SpL
SpR
EqF
Rew
Obv
EmS
SoR
EqR
Mpm
SPm
OPm
SHy
OHy
URR
Fac
Spt
Inp
Con
RRE
SSi
ClR
UnC
Ter