Hets - the Heterogeneous Tool Set

Copyright(c) Rene Wagner Heng Jiang Uni Bremen 2007
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerluecke@informatik.uni-bremen.de
Stabilityprovisional
Portabilityportable
Safe HaskellSafe

SoftFOL.Sign

Contents

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

Externally used data structures

type SoftFOLMorphism = DefaultMorphism Sign Source #

We use the DefaultMorphism for SPASS.

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 

Instances

Eq Sign Source # 

Methods

(==) :: Sign -> Sign -> Bool

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

Data Sign Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> Sign -> ShowS

show :: Sign -> String

showList :: [Sign] -> ShowS

PrintTPTP Sign Source # 

Methods

printTPTP :: Sign -> Doc Source #

Sentences SoftFOL Sentence Sign SoftFOLMorphism 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 # 
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source # 

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 #

StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source # 

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 #

data Generated Source #

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

Constructors

Generated 

Fields

Instances

Eq Generated Source # 

Methods

(==) :: Generated -> Generated -> Bool

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

Data Generated Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> Generated -> ShowS

show :: Generated -> String

showList :: [Generated] -> ShowS

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 

Instances

Eq SFSymbol Source # 

Methods

(==) :: SFSymbol -> SFSymbol -> Bool

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

Data SFSymbol Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SFSymbol -> ShowS

show :: SFSymbol -> String

showList :: [SFSymbol] -> ShowS

GetRange SFSymbol Source # 
Sentences SoftFOL Sentence Sign SoftFOLMorphism 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 # 
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source # 

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 #

Syntax SoftFOL [TPTP] SFSymbol () () Source # 
StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source # 

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 #

data SFSymbType Source #

Symbol types of SoftFOL. (not related to CASL)

Instances

Eq SFSymbType Source # 

Methods

(==) :: SFSymbType -> SFSymbType -> Bool

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

Data SFSymbType Source # 

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 :: (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 # 
Show SFSymbType Source # 

Methods

showsPrec :: Int -> SFSymbType -> ShowS

show :: SFSymbType -> String

showList :: [SFSymbType] -> ShowS

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.

Instances

Eq SPProblem Source # 

Methods

(==) :: SPProblem -> SPProblem -> Bool

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

Data SPProblem Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SPProblem -> ShowS

show :: SPProblem -> String

showList :: [SPProblem] -> ShowS

PrintTPTP SPProblem Source #

Creates a Doc from a SoftFOL Problem.

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.

Instances

Eq SPLogicalPart Source # 
Data SPLogicalPart Source # 

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 :: (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 # 
Show SPLogicalPart Source # 

Methods

showsPrec :: Int -> SPLogicalPart -> ShowS

show :: SPLogicalPart -> String

showList :: [SPLogicalPart] -> ShowS

PrintTPTP SPLogicalPart Source #

Creates a Doc from a SoftFOL Logical Part.

Symbol Lists

data SPSymbolList Source #

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

Constructors

SPSymbolList 

Instances

Eq SPSymbolList Source # 

Methods

(==) :: SPSymbolList -> SPSymbolList -> Bool

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

Data SPSymbolList Source # 

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 :: (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 # 
Show SPSymbolList Source # 

Methods

showsPrec :: Int -> SPSymbolList -> ShowS

show :: SPSymbolList -> String

showList :: [SPSymbolList] -> ShowS

emptySymbolList :: SPSymbolList Source #

Creates an empty SPASS Symbol List.

data SPSignSym Source #

A common data type used for all signature symbols.

Constructors

SPSignSym 

Fields

SPSimpleSignSym SPIdentifier 

Instances

Eq SPSignSym Source # 

Methods

(==) :: SPSignSym -> SPSignSym -> Bool

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

Data SPSignSym Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SPSignSym -> ShowS

show :: SPSignSym -> String

showList :: [SPSignSym] -> ShowS

data SPSortSym Source #

Constructors

SPSortSym SPIdentifier 

Instances

Eq SPSortSym Source # 

Methods

(==) :: SPSortSym -> SPSortSym -> Bool

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

Data SPSortSym Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SPSortSym -> ShowS

show :: SPSortSym -> String

showList :: [SPSortSym] -> ShowS

Declarations

data SPDeclaration Source #

SPASS Declarations allow the introduction of sorts.

Instances

Eq SPDeclaration Source # 
Data SPDeclaration Source # 

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 :: (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 # 
Show SPDeclaration Source # 

Methods

showsPrec :: Int -> SPDeclaration -> ShowS

show :: SPDeclaration -> String

showList :: [SPDeclaration] -> ShowS

PrintTPTP SPDeclaration Source #

Creates a Doc from a SoftFOL Declaration. A subsort declaration will be rewritten as a special SPQuantTerm.

Formula List

data SPFormulaList Source #

SPASS Formula List

Instances

Eq SPFormulaList Source # 
Data SPFormulaList Source # 

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 :: (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 # 
Show SPFormulaList Source # 

Methods

showsPrec :: Int -> SPFormulaList -> ShowS

show :: SPFormulaList -> String

showList :: [SPFormulaList] -> ShowS

PrintTPTP SPFormulaList Source #

Creates a Doc from a SoftFOL Formula List.

isAxiomFormula :: SPFormulaList -> Bool Source #

test the origin type of the formula list

Clause List

data SPClauseList Source #

SPASS Clause List

Instances

Eq SPClauseList Source # 

Methods

(==) :: SPClauseList -> SPClauseList -> Bool

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

Data SPClauseList Source # 

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 :: (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 # 
Show SPClauseList Source # 

Methods

showsPrec :: Int -> SPClauseList -> ShowS

show :: SPClauseList -> String

showList :: [SPClauseList] -> ShowS

data SPOriginType Source #

There are axiom formulae and conjecture formulae.

Instances

Eq SPOriginType Source # 

Methods

(==) :: SPOriginType -> SPOriginType -> Bool

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

Data SPOriginType Source # 

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 :: (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 # 
Show SPOriginType Source # 

Methods

showsPrec :: Int -> SPOriginType -> ShowS

show :: SPOriginType -> String

showList :: [SPOriginType] -> ShowS

PrintTPTP SPOriginType Source #

Creates a Doc from a SoftFOL Origin Type.

data SPClauseType Source #

Formulae can be in cnf or dnf

Constructors

SPCNF 
SPDNF 

Instances

Eq SPClauseType Source # 

Methods

(==) :: SPClauseType -> SPClauseType -> Bool

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

Data SPClauseType Source # 

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 :: (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 # 
Show SPClauseType Source # 

Methods

showsPrec :: Int -> SPClauseType -> ShowS

show :: SPClauseType -> String

showList :: [SPClauseType] -> ShowS

data NSPClause Source #

Instances

Eq NSPClause Source # 

Methods

(==) :: NSPClause -> NSPClause -> Bool

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

Data NSPClause Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> NSPClause -> ShowS

show :: NSPClause -> String

showList :: [NSPClause] -> ShowS

data NSPClauseBody Source #

a true boolean indicates the cnf

Instances

Eq NSPClauseBody Source # 
Data NSPClauseBody Source # 

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 :: (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 # 
Show NSPClauseBody Source # 

Methods

showsPrec :: Int -> NSPClauseBody -> ShowS

show :: NSPClauseBody -> String

showList :: [NSPClauseBody] -> ShowS

data TermWsList Source #

Constructors

TWL [SPTerm] Bool 

Instances

Eq TermWsList Source # 

Methods

(==) :: TermWsList -> TermWsList -> Bool

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

Data TermWsList Source # 

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 :: (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 # 
Show TermWsList Source # 

Methods

showsPrec :: Int -> TermWsList -> ShowS

show :: TermWsList -> String

showList :: [TermWsList] -> ShowS

data SPTerm Source #

A SPASS Term.

Instances

Eq SPTerm Source # 

Methods

(==) :: SPTerm -> SPTerm -> Bool

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

Data SPTerm Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SPTerm -> ShowS

show :: SPTerm -> String

showList :: [SPTerm] -> ShowS

GetRange SPTerm Source # 
PrintTPTP SPTerm Source #

Creates a Doc from a SoftFOL Term.

Methods

printTPTP :: SPTerm -> Doc Source #

Sentences SoftFOL Sentence Sign SoftFOLMorphism 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 # 
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source # 

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 #

StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source # 

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 #

data FileName Source #

Constructors

FileName String 

Instances

Data FileName Source # 

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 :: (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 # 

Methods

showsPrec :: Int -> FileName -> ShowS

show :: FileName -> String

showList :: [FileName] -> ShowS

data FormKind Source #

Constructors

FofKind 
CnfKind 
FotKind 

Instances

Data FormKind Source # 

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 :: (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 # 

Methods

showsPrec :: Int -> FormKind -> ShowS

show :: FormKind -> String

showList :: [FormKind] -> ShowS

data Role Source #

Instances

Data Role Source # 

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 :: (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 # 

Methods

showsPrec :: Int -> Role -> ShowS

show :: Role -> String

showList :: [Role] -> ShowS

data Name Source #

Constructors

Name String 

Instances

Data Name Source # 

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 :: (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 # 

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

data Annos Source #

Constructors

Annos Source (Maybe Info) 

Instances

Data Annos Source # 

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 :: (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 # 

Methods

showsPrec :: Int -> Annos -> ShowS

show :: Annos -> String

showList :: [Annos] -> ShowS

data Source Source #

Constructors

Source GenTerm 

Instances

Data Source Source # 

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 :: (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 # 

Methods

showsPrec :: Int -> Source -> ShowS

show :: Source -> String

showList :: [Source] -> ShowS

data AWord Source #

Constructors

AWord String 

Instances

Data AWord Source # 

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 :: (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 # 

Methods

showsPrec :: Int -> AWord -> ShowS

show :: AWord -> String

showList :: [AWord] -> ShowS

data GenTerm Source #

Constructors

GenTerm GenData (Maybe GenTerm) 
GenTermList [GenTerm] 

Instances

Data GenTerm Source # 

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 :: (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 # 

Methods

showsPrec :: Int -> GenTerm -> ShowS

show :: GenTerm -> String

showList :: [GenTerm] -> ShowS

data GenData Source #

Instances

Data GenData Source # 

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 :: (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 # 

Methods

showsPrec :: Int -> GenData -> ShowS

show :: GenData -> String

showList :: [GenData] -> ShowS

data FormData Source #

Constructors

FormData FormKind SPTerm 

Instances

Data FormData Source # 

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 :: (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 # 

Methods

showsPrec :: Int -> FormData -> ShowS

show :: FormData -> String

showList :: [FormData] -> ShowS

data Info Source #

Constructors

Info [GenTerm] 

Instances

Data Info Source # 

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 :: (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 # 

Methods

showsPrec :: Int -> Info -> ShowS

show :: Info -> String

showList :: [Info] -> ShowS

data TPTP Source #

Instances

Data TPTP Source # 

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 :: (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 # 

Methods

showsPrec :: Int -> TPTP -> ShowS

show :: TPTP -> String

showList :: [TPTP] -> ShowS

GetRange TPTP 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 # 
Logic SoftFOL () [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () ProofTree Source # 

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 #

Syntax SoftFOL [TPTP] SFSymbol () () Source # 
StaticAnalysis SoftFOL [TPTP] Sentence () () Sign SoftFOLMorphism SFSymbol () Source # 

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 #

data SPLiteral Source #

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

Constructors

SPLiteral Bool SPSymbol 

Instances

Eq SPLiteral Source # 

Methods

(==) :: SPLiteral -> SPLiteral -> Bool

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

Data SPLiteral Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SPLiteral -> ShowS

show :: SPLiteral -> String

showList :: [SPLiteral] -> ShowS

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

data SPQuantSym Source #

SPASS Quantifier Symbols.

Instances

Eq SPQuantSym Source # 

Methods

(==) :: SPQuantSym -> SPQuantSym -> Bool

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

Data SPQuantSym Source # 

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 :: (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 # 
Show SPQuantSym Source # 

Methods

showsPrec :: Int -> SPQuantSym -> ShowS

show :: SPQuantSym -> String

showList :: [SPQuantSym] -> ShowS

PrintTPTP SPQuantSym Source #

Creates a Doc from a SoftFOL Quantifier Symbol.

data SPSymbol Source #

SPASS Symbols.

Instances

Eq SPSymbol Source # 

Methods

(==) :: SPSymbol -> SPSymbol -> Bool

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

Data SPSymbol Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SPSymbol -> ShowS

show :: SPSymbol -> String

showList :: [SPSymbol] -> ShowS

PrintTPTP SPSymbol Source #

Creates a Doc from a SoftFOL Symbol.

Proof List

data SPProofList Source #

SPASS Proof List

Constructors

SPProofList 

Instances

Eq SPProofList Source # 

Methods

(==) :: SPProofList -> SPProofList -> Bool

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

Data SPProofList Source # 

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 :: (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 # 
Show SPProofList Source # 

Methods

showsPrec :: Int -> SPProofList -> ShowS

show :: SPProofList -> String

showList :: [SPProofList] -> ShowS

data SPProofStep Source #

Instances

Eq SPProofStep Source # 

Methods

(==) :: SPProofStep -> SPProofStep -> Bool

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

Data SPProofStep Source # 

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 :: (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 # 
Show SPProofStep Source # 

Methods

showsPrec :: Int -> SPProofStep -> ShowS

show :: SPProofStep -> String

showList :: [SPProofStep] -> ShowS

data SPReference Source #

Constructors

PRefTerm SPTerm 

Instances

Eq SPReference Source # 

Methods

(==) :: SPReference -> SPReference -> Bool

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

Data SPReference Source # 

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 :: (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 # 
Show SPReference Source # 

Methods

showsPrec :: Int -> SPReference -> ShowS

show :: SPReference -> String

showList :: [SPReference] -> ShowS

data SPResult Source #

Constructors

PResTerm SPTerm 

Instances

Eq SPResult Source # 

Methods

(==) :: SPResult -> SPResult -> Bool

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

Data SPResult Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SPResult -> ShowS

show :: SPResult -> String

showList :: [SPResult] -> ShowS

data SPRuleAppl Source #

Instances

Eq SPRuleAppl Source # 

Methods

(==) :: SPRuleAppl -> SPRuleAppl -> Bool

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

Data SPRuleAppl Source # 

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 :: (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 # 
Show SPRuleAppl Source # 

Methods

showsPrec :: Int -> SPRuleAppl -> ShowS

show :: SPRuleAppl -> String

showList :: [SPRuleAppl] -> ShowS

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

Eq SPUserRuleAppl Source # 
Data SPUserRuleAppl Source # 

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 :: (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 # 
Show SPUserRuleAppl Source # 

Methods

showsPrec :: Int -> SPUserRuleAppl -> ShowS

show :: SPUserRuleAppl -> String

showList :: [SPUserRuleAppl] -> ShowS

data SPParent Source #

Constructors

PParTerm SPTerm 

Instances

Eq SPParent Source # 

Methods

(==) :: SPParent -> SPParent -> Bool

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

Data SPParent Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SPParent -> ShowS

show :: SPParent -> String

showList :: [SPParent] -> ShowS

data SPKey Source #

Constructors

PKeyTerm SPTerm 

Instances

Eq SPKey Source # 

Methods

(==) :: SPKey -> SPKey -> Bool

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

Data SPKey Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SPKey -> ShowS

show :: SPKey -> String

showList :: [SPKey] -> ShowS

data SPValue Source #

Constructors

PValTerm SPTerm 

Instances

Eq SPValue Source # 

Methods

(==) :: SPValue -> SPValue -> Bool

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

Data SPValue Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SPValue -> ShowS

show :: SPValue -> String

showList :: [SPValue] -> ShowS

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)

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

Instances

Eq SPDescription Source # 
Data SPDescription Source # 

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 :: (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 # 
Show SPDescription Source # 

Methods

showsPrec :: Int -> SPDescription -> ShowS

show :: SPDescription -> String

showList :: [SPDescription] -> ShowS

PrintTPTP SPDescription Source #

Creates a Doc from a SoftFOL description.

data SPLogState Source #

The state of a SPASS problem can be satisfiable, unsatisfiable, or unknown.

Instances

Eq SPLogState Source # 

Methods

(==) :: SPLogState -> SPLogState -> Bool

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

Data SPLogState Source # 

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 :: (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 # 
Show SPLogState Source # 

Methods

showsPrec :: Int -> SPLogState -> ShowS

show :: SPLogState -> String

showList :: [SPLogState] -> ShowS

PrintTPTP SPLogState Source #

Creates a Doc from an SPLogState.

SPASS Settings

data SPSetting Source #

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

Instances

Eq SPSetting Source # 

Methods

(==) :: SPSetting -> SPSetting -> Bool

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

Data SPSetting Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SPSetting -> ShowS

show :: SPSetting -> String

showList :: [SPSetting] -> ShowS

PrintTPTP SPSetting Source # 

data SPSettingBody Source #

Constructors

SPClauseRelation [SPCRBIND] 
SPFlag String [String] 

Instances

Eq SPSettingBody Source # 
Data SPSettingBody Source # 

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 :: (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 # 
Show SPSettingBody Source # 

Methods

showsPrec :: Int -> SPSettingBody -> ShowS

show :: SPSettingBody -> String

showList :: [SPSettingBody] -> ShowS

PrintTPTP SPSettingBody Source # 

data SPHypothesis Source #

Constructors

SPHypothesis [SPIdentifier] 

Instances

Eq SPHypothesis Source # 

Methods

(==) :: SPHypothesis -> SPHypothesis -> Bool

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

Data SPHypothesis Source # 

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 :: (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 # 
Show SPHypothesis Source # 

Methods

showsPrec :: Int -> SPHypothesis -> ShowS

show :: SPHypothesis -> String

showList :: [SPHypothesis] -> ShowS

data SPSettingLabel Source #

Instances

Eq SPSettingLabel Source # 
Data SPSettingLabel Source # 

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 :: (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 # 
Show SPSettingLabel Source # 

Methods

showsPrec :: Int -> SPSettingLabel -> ShowS

show :: SPSettingLabel -> String

showList :: [SPSettingLabel] -> ShowS

data SPCRBIND Source #

A Tupel of the Clause Relation

Constructors

SPCRBIND 

Fields

Instances

Eq SPCRBIND Source # 

Methods

(==) :: SPCRBIND -> SPCRBIND -> Bool

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

Data SPCRBIND Source # 

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 :: (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 # 

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 # 

Methods

showsPrec :: Int -> SPCRBIND -> ShowS

show :: SPCRBIND -> String

showList :: [SPCRBIND] -> ShowS

negateSentence :: SPTerm -> Maybe SPTerm Source #

negate a sentence