Hets - the Heterogeneous Tool Set

Copyright(c) Karl Luc DFKI Bremen 2010 Eugen Kuksa and Uni Bremen 2011
LicenseGPLv2 or higher, see LICENSE.txt
Maintainereugenk@informatik.uni-bremen.de
Stabilityprovisional
Portabilityportable
Safe HaskellSafe

CommonLogic.AS_CommonLogic

Description

Definition of abstract syntax for common logic

Documentation

newtype BASIC_SPEC Source #

Instances

Eq BASIC_SPEC Source # 

Methods

(==) :: BASIC_SPEC -> BASIC_SPEC -> Bool

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

Ord BASIC_SPEC Source # 
Show BASIC_SPEC Source # 

Methods

showsPrec :: Int -> BASIC_SPEC -> ShowS

show :: BASIC_SPEC -> String

showList :: [BASIC_SPEC] -> ShowS

GetRange BASIC_SPEC Source # 
Pretty BASIC_SPEC Source # 
Syntax CommonLogic BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis CommonLogic BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # 

Methods

basic_analysis :: CommonLogic -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])) Source #

sen_analysis :: CommonLogic -> Maybe ((BASIC_SPEC, Sign, TEXT_META) -> Result TEXT_META) Source #

extBasicAnalysis :: CommonLogic -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META]) Source #

stat_symb_map_items :: CommonLogic -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #

stat_symb_items :: CommonLogic -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

convertTheory :: CommonLogic -> Maybe ((Sign, [Named TEXT_META]) -> BASIC_SPEC) Source #

ensures_amalgamability :: CommonLogic -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CommonLogic -> Morphism -> [Named TEXT_META] -> Result (Sign, [Named TEXT_META]) Source #

signature_colimit :: CommonLogic -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: CommonLogic -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named TEXT_META]) Source #

symbol_to_raw :: CommonLogic -> Symbol -> Symbol Source #

id_to_raw :: CommonLogic -> Id -> Symbol Source #

matches :: CommonLogic -> Symbol -> Symbol -> Bool Source #

empty_signature :: CommonLogic -> Sign Source #

add_symb_to_sign :: CommonLogic -> Sign -> Symbol -> Result Sign Source #

signature_union :: CommonLogic -> Sign -> Sign -> Result Sign Source #

signatureDiff :: CommonLogic -> Sign -> Sign -> Result Sign Source #

intersection :: CommonLogic -> Sign -> Sign -> Result Sign Source #

final_union :: CommonLogic -> Sign -> Sign -> Result Sign Source #

morphism_union :: CommonLogic -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: CommonLogic -> Sign -> Sign -> Bool Source #

subsig_inclusion :: CommonLogic -> Sign -> Sign -> Result Morphism Source #

generated_sign :: CommonLogic -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: CommonLogic -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: CommonLogic -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: CommonLogic -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: CommonLogic -> Morphism -> Bool Source #

is_injective :: CommonLogic -> Morphism -> Bool Source #

theory_to_taxonomy :: CommonLogic -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named TEXT_META] -> Result MMiSSOntology Source #

corresp2th :: CommonLogic -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named TEXT_META], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CommonLogic -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CommonLogic -> [IRI] -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

Logic CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 

Methods

parse_basic_sen :: CommonLogic -> Maybe (BASIC_SPEC -> AParser st TEXT_META) Source #

stability :: CommonLogic -> Stability Source #

data_logic :: CommonLogic -> Maybe AnyLogic Source #

top_sublogic :: CommonLogic -> CommonLogicSL Source #

all_sublogics :: CommonLogic -> [CommonLogicSL] Source #

bottomSublogic :: CommonLogic -> Maybe CommonLogicSL Source #

sublogicDimensions :: CommonLogic -> [[CommonLogicSL]] Source #

parseSublogic :: CommonLogic -> String -> Maybe CommonLogicSL Source #

proj_sublogic_epsilon :: CommonLogic -> CommonLogicSL -> Sign -> Morphism Source #

provers :: CommonLogic -> [Prover Sign TEXT_META Morphism CommonLogicSL ProofTree] Source #

default_prover :: CommonLogic -> String Source #

cons_checkers :: CommonLogic -> [ConsChecker Sign TEXT_META CommonLogicSL Morphism ProofTree] Source #

conservativityCheck :: CommonLogic -> [ConservativityChecker Sign TEXT_META Morphism] Source #

empty_proof_tree :: CommonLogic -> ProofTree Source #

syntaxTable :: CommonLogic -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CommonLogic -> Maybe OMCD Source #

export_symToOmdoc :: CommonLogic -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CommonLogic -> NameMap Symbol -> TEXT_META -> Result TCorOMElement Source #

export_theoryToOmdoc :: CommonLogic -> SigMap Symbol -> Sign -> [Named TEXT_META] -> Result [TCElement] Source #

omdocToSym :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named TEXT_META)) Source #

addOMadtToTheory :: CommonLogic -> SigMapI Symbol -> (Sign, [Named TEXT_META]) -> [[OmdADT]] -> Result (Sign, [Named TEXT_META]) Source #

addOmdocToTheory :: CommonLogic -> SigMapI Symbol -> (Sign, [Named TEXT_META]) -> [TCElement] -> Result (Sign, [Named TEXT_META]) Source #

Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CommonLogicModuleElimination CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 

Methods

sourceLogic :: CommonLogicModuleElimination -> CommonLogic Source #

sourceSublogic :: CommonLogicModuleElimination -> CommonLogicSL Source #

sourceSublogicLossy :: CommonLogicModuleElimination -> CommonLogicSL Source #

minSourceTheory :: CommonLogicModuleElimination -> Maybe (LibName, String) Source #

targetLogic :: CommonLogicModuleElimination -> CommonLogic Source #

mapSublogic :: CommonLogicModuleElimination -> CommonLogicSL -> Maybe CommonLogicSL Source #

map_theory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

mapMarkedTheory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

map_morphism :: CommonLogicModuleElimination -> Morphism -> Result Morphism Source #

map_sentence :: CommonLogicModuleElimination -> Sign -> TEXT_META -> Result TEXT_META Source #

map_symbol :: CommonLogicModuleElimination -> Sign -> Symbol -> Set Symbol Source #

extractModel :: CommonLogicModuleElimination -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source #

is_model_transportable :: CommonLogicModuleElimination -> Bool Source #

has_model_expansion :: CommonLogicModuleElimination -> Bool Source #

is_weakly_amalgamable :: CommonLogicModuleElimination -> Bool Source #

constituents :: CommonLogicModuleElimination -> [String] Source #

isInclusionComorphism :: CommonLogicModuleElimination -> Bool Source #

rps :: CommonLogicModuleElimination -> Bool Source #

eps :: CommonLogicModuleElimination -> Bool Source #

Comorphism OWL22CommonLogic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Comorphism Prop2CommonLogic Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree 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 # 

type PrefixMapping = (String, IRI) Source #

data TEXT_META Source #

Constructors

Text_meta 

Fields

Instances

Eq TEXT_META Source # 

Methods

(==) :: TEXT_META -> TEXT_META -> Bool

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

Data TEXT_META Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TEXT_META -> c TEXT_META

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TEXT_META

toConstr :: TEXT_META -> Constr

dataTypeOf :: TEXT_META -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c TEXT_META)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TEXT_META)

gmapT :: (forall b. Data b => b -> b) -> TEXT_META -> TEXT_META

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TEXT_META -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TEXT_META -> r

gmapQ :: (forall d. Data d => d -> u) -> TEXT_META -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TEXT_META -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TEXT_META -> m TEXT_META

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TEXT_META -> m TEXT_META

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TEXT_META -> m TEXT_META

Ord TEXT_META Source # 

Methods

compare :: TEXT_META -> TEXT_META -> Ordering

(<) :: TEXT_META -> TEXT_META -> Bool

(<=) :: TEXT_META -> TEXT_META -> Bool

(>) :: TEXT_META -> TEXT_META -> Bool

(>=) :: TEXT_META -> TEXT_META -> Bool

max :: TEXT_META -> TEXT_META -> TEXT_META

min :: TEXT_META -> TEXT_META -> TEXT_META

Show TEXT_META Source # 

Methods

showsPrec :: Int -> TEXT_META -> ShowS

show :: TEXT_META -> String

showList :: [TEXT_META] -> ShowS

GetRange TEXT_META Source # 
Pretty TEXT_META Source # 
Sentences CommonLogic TEXT_META Sign Morphism Symbol Source # 
StaticAnalysis CommonLogic BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # 

Methods

basic_analysis :: CommonLogic -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])) Source #

sen_analysis :: CommonLogic -> Maybe ((BASIC_SPEC, Sign, TEXT_META) -> Result TEXT_META) Source #

extBasicAnalysis :: CommonLogic -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META]) Source #

stat_symb_map_items :: CommonLogic -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #

stat_symb_items :: CommonLogic -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

convertTheory :: CommonLogic -> Maybe ((Sign, [Named TEXT_META]) -> BASIC_SPEC) Source #

ensures_amalgamability :: CommonLogic -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CommonLogic -> Morphism -> [Named TEXT_META] -> Result (Sign, [Named TEXT_META]) Source #

signature_colimit :: CommonLogic -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: CommonLogic -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named TEXT_META]) Source #

symbol_to_raw :: CommonLogic -> Symbol -> Symbol Source #

id_to_raw :: CommonLogic -> Id -> Symbol Source #

matches :: CommonLogic -> Symbol -> Symbol -> Bool Source #

empty_signature :: CommonLogic -> Sign Source #

add_symb_to_sign :: CommonLogic -> Sign -> Symbol -> Result Sign Source #

signature_union :: CommonLogic -> Sign -> Sign -> Result Sign Source #

signatureDiff :: CommonLogic -> Sign -> Sign -> Result Sign Source #

intersection :: CommonLogic -> Sign -> Sign -> Result Sign Source #

final_union :: CommonLogic -> Sign -> Sign -> Result Sign Source #

morphism_union :: CommonLogic -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: CommonLogic -> Sign -> Sign -> Bool Source #

subsig_inclusion :: CommonLogic -> Sign -> Sign -> Result Morphism Source #

generated_sign :: CommonLogic -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: CommonLogic -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: CommonLogic -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: CommonLogic -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: CommonLogic -> Morphism -> Bool Source #

is_injective :: CommonLogic -> Morphism -> Bool Source #

theory_to_taxonomy :: CommonLogic -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named TEXT_META] -> Result MMiSSOntology Source #

corresp2th :: CommonLogic -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named TEXT_META], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CommonLogic -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CommonLogic -> [IRI] -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

Logic CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 

Methods

parse_basic_sen :: CommonLogic -> Maybe (BASIC_SPEC -> AParser st TEXT_META) Source #

stability :: CommonLogic -> Stability Source #

data_logic :: CommonLogic -> Maybe AnyLogic Source #

top_sublogic :: CommonLogic -> CommonLogicSL Source #

all_sublogics :: CommonLogic -> [CommonLogicSL] Source #

bottomSublogic :: CommonLogic -> Maybe CommonLogicSL Source #

sublogicDimensions :: CommonLogic -> [[CommonLogicSL]] Source #

parseSublogic :: CommonLogic -> String -> Maybe CommonLogicSL Source #

proj_sublogic_epsilon :: CommonLogic -> CommonLogicSL -> Sign -> Morphism Source #

provers :: CommonLogic -> [Prover Sign TEXT_META Morphism CommonLogicSL ProofTree] Source #

default_prover :: CommonLogic -> String Source #

cons_checkers :: CommonLogic -> [ConsChecker Sign TEXT_META CommonLogicSL Morphism ProofTree] Source #

conservativityCheck :: CommonLogic -> [ConservativityChecker Sign TEXT_META Morphism] Source #

empty_proof_tree :: CommonLogic -> ProofTree Source #

syntaxTable :: CommonLogic -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CommonLogic -> Maybe OMCD Source #

export_symToOmdoc :: CommonLogic -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CommonLogic -> NameMap Symbol -> TEXT_META -> Result TCorOMElement Source #

export_theoryToOmdoc :: CommonLogic -> SigMap Symbol -> Sign -> [Named TEXT_META] -> Result [TCElement] Source #

omdocToSym :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named TEXT_META)) Source #

addOMadtToTheory :: CommonLogic -> SigMapI Symbol -> (Sign, [Named TEXT_META]) -> [[OmdADT]] -> Result (Sign, [Named TEXT_META]) Source #

addOmdocToTheory :: CommonLogic -> SigMapI Symbol -> (Sign, [Named TEXT_META]) -> [TCElement] -> Result (Sign, [Named TEXT_META]) Source #

Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CommonLogicModuleElimination CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 

Methods

sourceLogic :: CommonLogicModuleElimination -> CommonLogic Source #

sourceSublogic :: CommonLogicModuleElimination -> CommonLogicSL Source #

sourceSublogicLossy :: CommonLogicModuleElimination -> CommonLogicSL Source #

minSourceTheory :: CommonLogicModuleElimination -> Maybe (LibName, String) Source #

targetLogic :: CommonLogicModuleElimination -> CommonLogic Source #

mapSublogic :: CommonLogicModuleElimination -> CommonLogicSL -> Maybe CommonLogicSL Source #

map_theory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

mapMarkedTheory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

map_morphism :: CommonLogicModuleElimination -> Morphism -> Result Morphism Source #

map_sentence :: CommonLogicModuleElimination -> Sign -> TEXT_META -> Result TEXT_META Source #

map_symbol :: CommonLogicModuleElimination -> Sign -> Symbol -> Set Symbol Source #

extractModel :: CommonLogicModuleElimination -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source #

is_model_transportable :: CommonLogicModuleElimination -> Bool Source #

has_model_expansion :: CommonLogicModuleElimination -> Bool Source #

is_weakly_amalgamable :: CommonLogicModuleElimination -> Bool Source #

constituents :: CommonLogicModuleElimination -> [String] Source #

isInclusionComorphism :: CommonLogicModuleElimination -> Bool Source #

rps :: CommonLogicModuleElimination -> Bool Source #

eps :: CommonLogicModuleElimination -> Bool Source #

Comorphism OWL22CommonLogic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Comorphism Prop2CommonLogic Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree 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 # 

data TEXT Source #

Instances

Eq TEXT Source # 

Methods

(==) :: TEXT -> TEXT -> Bool

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

Data TEXT Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TEXT -> c TEXT

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TEXT

toConstr :: TEXT -> Constr

dataTypeOf :: TEXT -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c TEXT)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TEXT)

gmapT :: (forall b. Data b => b -> b) -> TEXT -> TEXT

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TEXT -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TEXT -> r

gmapQ :: (forall d. Data d => d -> u) -> TEXT -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TEXT -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TEXT -> m TEXT

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TEXT -> m TEXT

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TEXT -> m TEXT

Ord TEXT Source # 

Methods

compare :: TEXT -> TEXT -> Ordering

(<) :: TEXT -> TEXT -> Bool

(<=) :: TEXT -> TEXT -> Bool

(>) :: TEXT -> TEXT -> Bool

(>=) :: TEXT -> TEXT -> Bool

max :: TEXT -> TEXT -> TEXT

min :: TEXT -> TEXT -> TEXT

Show TEXT Source # 

Methods

showsPrec :: Int -> TEXT -> ShowS

show :: TEXT -> String

showList :: [TEXT] -> ShowS

GetRange TEXT Source # 
Pretty TEXT Source # 

Methods

pretty :: TEXT -> Doc Source #

pretties :: [TEXT] -> Doc Source #

data PHRASE Source #

Instances

Eq PHRASE Source # 

Methods

(==) :: PHRASE -> PHRASE -> Bool

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

Data PHRASE Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PHRASE -> c PHRASE

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PHRASE

toConstr :: PHRASE -> Constr

dataTypeOf :: PHRASE -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c PHRASE)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PHRASE)

gmapT :: (forall b. Data b => b -> b) -> PHRASE -> PHRASE

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PHRASE -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PHRASE -> r

gmapQ :: (forall d. Data d => d -> u) -> PHRASE -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PHRASE -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PHRASE -> m PHRASE

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PHRASE -> m PHRASE

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PHRASE -> m PHRASE

Ord PHRASE Source # 

Methods

compare :: PHRASE -> PHRASE -> Ordering

(<) :: PHRASE -> PHRASE -> Bool

(<=) :: PHRASE -> PHRASE -> Bool

(>) :: PHRASE -> PHRASE -> Bool

(>=) :: PHRASE -> PHRASE -> Bool

max :: PHRASE -> PHRASE -> PHRASE

min :: PHRASE -> PHRASE -> PHRASE

Show PHRASE Source # 

Methods

showsPrec :: Int -> PHRASE -> ShowS

show :: PHRASE -> String

showList :: [PHRASE] -> ShowS

GetRange PHRASE Source # 
Pretty PHRASE Source # 

data COMMENT Source #

Constructors

Comment String Range 

Instances

Eq COMMENT Source # 

Methods

(==) :: COMMENT -> COMMENT -> Bool

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

Data COMMENT Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> COMMENT -> c COMMENT

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c COMMENT

toConstr :: COMMENT -> Constr

dataTypeOf :: COMMENT -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c COMMENT)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c COMMENT)

gmapT :: (forall b. Data b => b -> b) -> COMMENT -> COMMENT

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> COMMENT -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> COMMENT -> r

gmapQ :: (forall d. Data d => d -> u) -> COMMENT -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> COMMENT -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> COMMENT -> m COMMENT

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> COMMENT -> m COMMENT

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> COMMENT -> m COMMENT

Ord COMMENT Source # 

Methods

compare :: COMMENT -> COMMENT -> Ordering

(<) :: COMMENT -> COMMENT -> Bool

(<=) :: COMMENT -> COMMENT -> Bool

(>) :: COMMENT -> COMMENT -> Bool

(>=) :: COMMENT -> COMMENT -> Bool

max :: COMMENT -> COMMENT -> COMMENT

min :: COMMENT -> COMMENT -> COMMENT

Show COMMENT Source # 

Methods

showsPrec :: Int -> COMMENT -> ShowS

show :: COMMENT -> String

showList :: [COMMENT] -> ShowS

GetRange COMMENT Source # 
Pretty COMMENT Source # 

data MODULE Source #

Instances

Eq MODULE Source # 

Methods

(==) :: MODULE -> MODULE -> Bool

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

Data MODULE Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MODULE -> c MODULE

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MODULE

toConstr :: MODULE -> Constr

dataTypeOf :: MODULE -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c MODULE)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MODULE)

gmapT :: (forall b. Data b => b -> b) -> MODULE -> MODULE

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MODULE -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MODULE -> r

gmapQ :: (forall d. Data d => d -> u) -> MODULE -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> MODULE -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MODULE -> m MODULE

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MODULE -> m MODULE

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MODULE -> m MODULE

Ord MODULE Source # 

Methods

compare :: MODULE -> MODULE -> Ordering

(<) :: MODULE -> MODULE -> Bool

(<=) :: MODULE -> MODULE -> Bool

(>) :: MODULE -> MODULE -> Bool

(>=) :: MODULE -> MODULE -> Bool

max :: MODULE -> MODULE -> MODULE

min :: MODULE -> MODULE -> MODULE

Show MODULE Source # 

Methods

showsPrec :: Int -> MODULE -> ShowS

show :: MODULE -> String

showList :: [MODULE] -> ShowS

GetRange MODULE Source # 
Pretty MODULE Source # 

data IMPORTATION Source #

Constructors

Imp_name NAME 

Instances

Eq IMPORTATION Source # 

Methods

(==) :: IMPORTATION -> IMPORTATION -> Bool

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

Data IMPORTATION Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IMPORTATION -> c IMPORTATION

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c IMPORTATION

toConstr :: IMPORTATION -> Constr

dataTypeOf :: IMPORTATION -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c IMPORTATION)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c IMPORTATION)

gmapT :: (forall b. Data b => b -> b) -> IMPORTATION -> IMPORTATION

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IMPORTATION -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IMPORTATION -> r

gmapQ :: (forall d. Data d => d -> u) -> IMPORTATION -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> IMPORTATION -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> IMPORTATION -> m IMPORTATION

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IMPORTATION -> m IMPORTATION

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IMPORTATION -> m IMPORTATION

Ord IMPORTATION Source # 
Show IMPORTATION Source # 

Methods

showsPrec :: Int -> IMPORTATION -> ShowS

show :: IMPORTATION -> String

showList :: [IMPORTATION] -> ShowS

GetRange IMPORTATION Source # 
Pretty IMPORTATION Source # 

data SENTENCE Source #

Instances

Eq SENTENCE Source # 

Methods

(==) :: SENTENCE -> SENTENCE -> Bool

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

Data SENTENCE Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SENTENCE -> c SENTENCE

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SENTENCE

toConstr :: SENTENCE -> Constr

dataTypeOf :: SENTENCE -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SENTENCE)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SENTENCE)

gmapT :: (forall b. Data b => b -> b) -> SENTENCE -> SENTENCE

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SENTENCE -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SENTENCE -> r

gmapQ :: (forall d. Data d => d -> u) -> SENTENCE -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SENTENCE -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SENTENCE -> m SENTENCE

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SENTENCE -> m SENTENCE

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SENTENCE -> m SENTENCE

Ord SENTENCE Source # 

Methods

compare :: SENTENCE -> SENTENCE -> Ordering

(<) :: SENTENCE -> SENTENCE -> Bool

(<=) :: SENTENCE -> SENTENCE -> Bool

(>) :: SENTENCE -> SENTENCE -> Bool

(>=) :: SENTENCE -> SENTENCE -> Bool

max :: SENTENCE -> SENTENCE -> SENTENCE

min :: SENTENCE -> SENTENCE -> SENTENCE

Show SENTENCE Source # 

Methods

showsPrec :: Int -> SENTENCE -> ShowS

show :: SENTENCE -> String

showList :: [SENTENCE] -> ShowS

GetRange SENTENCE Source # 
Pretty SENTENCE Source # 

data QUANT Source #

Constructors

Universal 
Existential 

Instances

Eq QUANT Source # 

Methods

(==) :: QUANT -> QUANT -> Bool

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

Data QUANT Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> QUANT -> c QUANT

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c QUANT

toConstr :: QUANT -> Constr

dataTypeOf :: QUANT -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c QUANT)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QUANT)

gmapT :: (forall b. Data b => b -> b) -> QUANT -> QUANT

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QUANT -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QUANT -> r

gmapQ :: (forall d. Data d => d -> u) -> QUANT -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> QUANT -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> QUANT -> m QUANT

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> QUANT -> m QUANT

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> QUANT -> m QUANT

Ord QUANT Source # 

Methods

compare :: QUANT -> QUANT -> Ordering

(<) :: QUANT -> QUANT -> Bool

(<=) :: QUANT -> QUANT -> Bool

(>) :: QUANT -> QUANT -> Bool

(>=) :: QUANT -> QUANT -> Bool

max :: QUANT -> QUANT -> QUANT

min :: QUANT -> QUANT -> QUANT

Show QUANT Source # 

Methods

showsPrec :: Int -> QUANT -> ShowS

show :: QUANT -> String

showList :: [QUANT] -> ShowS

GetRange QUANT Source # 
Pretty QUANT Source # 

data BOOL_SENT Source #

Instances

Eq BOOL_SENT Source # 

Methods

(==) :: BOOL_SENT -> BOOL_SENT -> Bool

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

Data BOOL_SENT Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BOOL_SENT -> c BOOL_SENT

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BOOL_SENT

toConstr :: BOOL_SENT -> Constr

dataTypeOf :: BOOL_SENT -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c BOOL_SENT)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BOOL_SENT)

gmapT :: (forall b. Data b => b -> b) -> BOOL_SENT -> BOOL_SENT

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BOOL_SENT -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BOOL_SENT -> r

gmapQ :: (forall d. Data d => d -> u) -> BOOL_SENT -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BOOL_SENT -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BOOL_SENT -> m BOOL_SENT

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BOOL_SENT -> m BOOL_SENT

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BOOL_SENT -> m BOOL_SENT

Ord BOOL_SENT Source # 

Methods

compare :: BOOL_SENT -> BOOL_SENT -> Ordering

(<) :: BOOL_SENT -> BOOL_SENT -> Bool

(<=) :: BOOL_SENT -> BOOL_SENT -> Bool

(>) :: BOOL_SENT -> BOOL_SENT -> Bool

(>=) :: BOOL_SENT -> BOOL_SENT -> Bool

max :: BOOL_SENT -> BOOL_SENT -> BOOL_SENT

min :: BOOL_SENT -> BOOL_SENT -> BOOL_SENT

Show BOOL_SENT Source # 

Methods

showsPrec :: Int -> BOOL_SENT -> ShowS

show :: BOOL_SENT -> String

showList :: [BOOL_SENT] -> ShowS

GetRange BOOL_SENT Source # 
Pretty BOOL_SENT Source # 

data AndOr Source #

Constructors

Conjunction 
Disjunction 

Instances

Eq AndOr Source # 

Methods

(==) :: AndOr -> AndOr -> Bool

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

Data AndOr Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AndOr -> c AndOr

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AndOr

toConstr :: AndOr -> Constr

dataTypeOf :: AndOr -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c AndOr)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AndOr)

gmapT :: (forall b. Data b => b -> b) -> AndOr -> AndOr

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AndOr -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AndOr -> r

gmapQ :: (forall d. Data d => d -> u) -> AndOr -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> AndOr -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> AndOr -> m AndOr

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AndOr -> m AndOr

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AndOr -> m AndOr

Ord AndOr Source # 

Methods

compare :: AndOr -> AndOr -> Ordering

(<) :: AndOr -> AndOr -> Bool

(<=) :: AndOr -> AndOr -> Bool

(>) :: AndOr -> AndOr -> Bool

(>=) :: AndOr -> AndOr -> Bool

max :: AndOr -> AndOr -> AndOr

min :: AndOr -> AndOr -> AndOr

Show AndOr Source # 

Methods

showsPrec :: Int -> AndOr -> ShowS

show :: AndOr -> String

showList :: [AndOr] -> ShowS

GetRange AndOr Source # 
Pretty AndOr Source # 

data ImplEq Source #

Constructors

Implication 
Biconditional 

Instances

Eq ImplEq Source # 

Methods

(==) :: ImplEq -> ImplEq -> Bool

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

Data ImplEq Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ImplEq -> c ImplEq

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ImplEq

toConstr :: ImplEq -> Constr

dataTypeOf :: ImplEq -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ImplEq)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ImplEq)

gmapT :: (forall b. Data b => b -> b) -> ImplEq -> ImplEq

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ImplEq -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ImplEq -> r

gmapQ :: (forall d. Data d => d -> u) -> ImplEq -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ImplEq -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ImplEq -> m ImplEq

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ImplEq -> m ImplEq

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ImplEq -> m ImplEq

Ord ImplEq Source # 

Methods

compare :: ImplEq -> ImplEq -> Ordering

(<) :: ImplEq -> ImplEq -> Bool

(<=) :: ImplEq -> ImplEq -> Bool

(>) :: ImplEq -> ImplEq -> Bool

(>=) :: ImplEq -> ImplEq -> Bool

max :: ImplEq -> ImplEq -> ImplEq

min :: ImplEq -> ImplEq -> ImplEq

Show ImplEq Source # 

Methods

showsPrec :: Int -> ImplEq -> ShowS

show :: ImplEq -> String

showList :: [ImplEq] -> ShowS

GetRange ImplEq Source # 
Pretty ImplEq Source # 

data ATOM Source #

Constructors

Equation TERM TERM 
Atom TERM [TERM_SEQ] 

Instances

Eq ATOM Source # 

Methods

(==) :: ATOM -> ATOM -> Bool

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

Data ATOM Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ATOM -> c ATOM

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ATOM

toConstr :: ATOM -> Constr

dataTypeOf :: ATOM -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ATOM)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ATOM)

gmapT :: (forall b. Data b => b -> b) -> ATOM -> ATOM

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ATOM -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ATOM -> r

gmapQ :: (forall d. Data d => d -> u) -> ATOM -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ATOM -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ATOM -> m ATOM

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ATOM -> m ATOM

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ATOM -> m ATOM

Ord ATOM Source # 

Methods

compare :: ATOM -> ATOM -> Ordering

(<) :: ATOM -> ATOM -> Bool

(<=) :: ATOM -> ATOM -> Bool

(>) :: ATOM -> ATOM -> Bool

(>=) :: ATOM -> ATOM -> Bool

max :: ATOM -> ATOM -> ATOM

min :: ATOM -> ATOM -> ATOM

Show ATOM Source # 

Methods

showsPrec :: Int -> ATOM -> ShowS

show :: ATOM -> String

showList :: [ATOM] -> ShowS

GetRange ATOM Source # 
Pretty ATOM Source # 

Methods

pretty :: ATOM -> Doc Source #

pretties :: [ATOM] -> Doc Source #

data TERM Source #

Instances

Eq TERM Source # 

Methods

(==) :: TERM -> TERM -> Bool

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

Data TERM Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TERM -> c TERM

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TERM

toConstr :: TERM -> Constr

dataTypeOf :: TERM -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c TERM)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TERM)

gmapT :: (forall b. Data b => b -> b) -> TERM -> TERM

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TERM -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TERM -> r

gmapQ :: (forall d. Data d => d -> u) -> TERM -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TERM -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TERM -> m TERM

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TERM -> m TERM

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TERM -> m TERM

Ord TERM Source # 

Methods

compare :: TERM -> TERM -> Ordering

(<) :: TERM -> TERM -> Bool

(<=) :: TERM -> TERM -> Bool

(>) :: TERM -> TERM -> Bool

(>=) :: TERM -> TERM -> Bool

max :: TERM -> TERM -> TERM

min :: TERM -> TERM -> TERM

Show TERM Source # 

Methods

showsPrec :: Int -> TERM -> ShowS

show :: TERM -> String

showList :: [TERM] -> ShowS

GetRange TERM Source # 
Pretty TERM Source # 

Methods

pretty :: TERM -> Doc Source #

pretties :: [TERM] -> Doc Source #

data TERM_SEQ Source #

Instances

Eq TERM_SEQ Source # 

Methods

(==) :: TERM_SEQ -> TERM_SEQ -> Bool

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

Data TERM_SEQ Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TERM_SEQ -> c TERM_SEQ

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TERM_SEQ

toConstr :: TERM_SEQ -> Constr

dataTypeOf :: TERM_SEQ -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c TERM_SEQ)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TERM_SEQ)

gmapT :: (forall b. Data b => b -> b) -> TERM_SEQ -> TERM_SEQ

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TERM_SEQ -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TERM_SEQ -> r

gmapQ :: (forall d. Data d => d -> u) -> TERM_SEQ -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> TERM_SEQ -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TERM_SEQ -> m TERM_SEQ

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TERM_SEQ -> m TERM_SEQ

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TERM_SEQ -> m TERM_SEQ

Ord TERM_SEQ Source # 

Methods

compare :: TERM_SEQ -> TERM_SEQ -> Ordering

(<) :: TERM_SEQ -> TERM_SEQ -> Bool

(<=) :: TERM_SEQ -> TERM_SEQ -> Bool

(>) :: TERM_SEQ -> TERM_SEQ -> Bool

(>=) :: TERM_SEQ -> TERM_SEQ -> Bool

max :: TERM_SEQ -> TERM_SEQ -> TERM_SEQ

min :: TERM_SEQ -> TERM_SEQ -> TERM_SEQ

Show TERM_SEQ Source # 

Methods

showsPrec :: Int -> TERM_SEQ -> ShowS

show :: TERM_SEQ -> String

showList :: [TERM_SEQ] -> ShowS

GetRange TERM_SEQ Source # 
Pretty TERM_SEQ Source # 

data NAME_OR_SEQMARK Source #

Constructors

Name NAME 
SeqMark SEQ_MARK 

Instances

Eq NAME_OR_SEQMARK Source # 
Data NAME_OR_SEQMARK Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NAME_OR_SEQMARK -> c NAME_OR_SEQMARK

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NAME_OR_SEQMARK

toConstr :: NAME_OR_SEQMARK -> Constr

dataTypeOf :: NAME_OR_SEQMARK -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c NAME_OR_SEQMARK)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NAME_OR_SEQMARK)

gmapT :: (forall b. Data b => b -> b) -> NAME_OR_SEQMARK -> NAME_OR_SEQMARK

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NAME_OR_SEQMARK -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NAME_OR_SEQMARK -> r

gmapQ :: (forall d. Data d => d -> u) -> NAME_OR_SEQMARK -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NAME_OR_SEQMARK -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NAME_OR_SEQMARK -> m NAME_OR_SEQMARK

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NAME_OR_SEQMARK -> m NAME_OR_SEQMARK

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NAME_OR_SEQMARK -> m NAME_OR_SEQMARK

Ord NAME_OR_SEQMARK Source # 
Show NAME_OR_SEQMARK Source # 

Methods

showsPrec :: Int -> NAME_OR_SEQMARK -> ShowS

show :: NAME_OR_SEQMARK -> String

showList :: [NAME_OR_SEQMARK] -> ShowS

GetRange NAME_OR_SEQMARK Source # 
Pretty NAME_OR_SEQMARK Source # 

data SYMB_MAP_ITEMS Source #

Instances

Eq SYMB_MAP_ITEMS Source # 
Data SYMB_MAP_ITEMS Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_MAP_ITEMS -> c SYMB_MAP_ITEMS

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_MAP_ITEMS

toConstr :: SYMB_MAP_ITEMS -> Constr

dataTypeOf :: SYMB_MAP_ITEMS -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SYMB_MAP_ITEMS)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_MAP_ITEMS)

gmapT :: (forall b. Data b => b -> b) -> SYMB_MAP_ITEMS -> SYMB_MAP_ITEMS

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_MAP_ITEMS -> r

gmapQ :: (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_MAP_ITEMS -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_MAP_ITEMS -> m SYMB_MAP_ITEMS

Ord SYMB_MAP_ITEMS Source # 
Show SYMB_MAP_ITEMS Source # 

Methods

showsPrec :: Int -> SYMB_MAP_ITEMS -> ShowS

show :: SYMB_MAP_ITEMS -> String

showList :: [SYMB_MAP_ITEMS] -> ShowS

GetRange SYMB_MAP_ITEMS Source # 
Pretty SYMB_MAP_ITEMS Source # 
Syntax CommonLogic BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis CommonLogic BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # 

Methods

basic_analysis :: CommonLogic -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])) Source #

sen_analysis :: CommonLogic -> Maybe ((BASIC_SPEC, Sign, TEXT_META) -> Result TEXT_META) Source #

extBasicAnalysis :: CommonLogic -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META]) Source #

stat_symb_map_items :: CommonLogic -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #

stat_symb_items :: CommonLogic -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

convertTheory :: CommonLogic -> Maybe ((Sign, [Named TEXT_META]) -> BASIC_SPEC) Source #

ensures_amalgamability :: CommonLogic -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CommonLogic -> Morphism -> [Named TEXT_META] -> Result (Sign, [Named TEXT_META]) Source #

signature_colimit :: CommonLogic -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: CommonLogic -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named TEXT_META]) Source #

symbol_to_raw :: CommonLogic -> Symbol -> Symbol Source #

id_to_raw :: CommonLogic -> Id -> Symbol Source #

matches :: CommonLogic -> Symbol -> Symbol -> Bool Source #

empty_signature :: CommonLogic -> Sign Source #

add_symb_to_sign :: CommonLogic -> Sign -> Symbol -> Result Sign Source #

signature_union :: CommonLogic -> Sign -> Sign -> Result Sign Source #

signatureDiff :: CommonLogic -> Sign -> Sign -> Result Sign Source #

intersection :: CommonLogic -> Sign -> Sign -> Result Sign Source #

final_union :: CommonLogic -> Sign -> Sign -> Result Sign Source #

morphism_union :: CommonLogic -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: CommonLogic -> Sign -> Sign -> Bool Source #

subsig_inclusion :: CommonLogic -> Sign -> Sign -> Result Morphism Source #

generated_sign :: CommonLogic -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: CommonLogic -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: CommonLogic -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: CommonLogic -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: CommonLogic -> Morphism -> Bool Source #

is_injective :: CommonLogic -> Morphism -> Bool Source #

theory_to_taxonomy :: CommonLogic -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named TEXT_META] -> Result MMiSSOntology Source #

corresp2th :: CommonLogic -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named TEXT_META], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CommonLogic -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CommonLogic -> [IRI] -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

Logic CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 

Methods

parse_basic_sen :: CommonLogic -> Maybe (BASIC_SPEC -> AParser st TEXT_META) Source #

stability :: CommonLogic -> Stability Source #

data_logic :: CommonLogic -> Maybe AnyLogic Source #

top_sublogic :: CommonLogic -> CommonLogicSL Source #

all_sublogics :: CommonLogic -> [CommonLogicSL] Source #

bottomSublogic :: CommonLogic -> Maybe CommonLogicSL Source #

sublogicDimensions :: CommonLogic -> [[CommonLogicSL]] Source #

parseSublogic :: CommonLogic -> String -> Maybe CommonLogicSL Source #

proj_sublogic_epsilon :: CommonLogic -> CommonLogicSL -> Sign -> Morphism Source #

provers :: CommonLogic -> [Prover Sign TEXT_META Morphism CommonLogicSL ProofTree] Source #

default_prover :: CommonLogic -> String Source #

cons_checkers :: CommonLogic -> [ConsChecker Sign TEXT_META CommonLogicSL Morphism ProofTree] Source #

conservativityCheck :: CommonLogic -> [ConservativityChecker Sign TEXT_META Morphism] Source #

empty_proof_tree :: CommonLogic -> ProofTree Source #

syntaxTable :: CommonLogic -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CommonLogic -> Maybe OMCD Source #

export_symToOmdoc :: CommonLogic -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CommonLogic -> NameMap Symbol -> TEXT_META -> Result TCorOMElement Source #

export_theoryToOmdoc :: CommonLogic -> SigMap Symbol -> Sign -> [Named TEXT_META] -> Result [TCElement] Source #

omdocToSym :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named TEXT_META)) Source #

addOMadtToTheory :: CommonLogic -> SigMapI Symbol -> (Sign, [Named TEXT_META]) -> [[OmdADT]] -> Result (Sign, [Named TEXT_META]) Source #

addOmdocToTheory :: CommonLogic -> SigMapI Symbol -> (Sign, [Named TEXT_META]) -> [TCElement] -> Result (Sign, [Named TEXT_META]) Source #

Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CommonLogicModuleElimination CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 

Methods

sourceLogic :: CommonLogicModuleElimination -> CommonLogic Source #

sourceSublogic :: CommonLogicModuleElimination -> CommonLogicSL Source #

sourceSublogicLossy :: CommonLogicModuleElimination -> CommonLogicSL Source #

minSourceTheory :: CommonLogicModuleElimination -> Maybe (LibName, String) Source #

targetLogic :: CommonLogicModuleElimination -> CommonLogic Source #

mapSublogic :: CommonLogicModuleElimination -> CommonLogicSL -> Maybe CommonLogicSL Source #

map_theory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

mapMarkedTheory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

map_morphism :: CommonLogicModuleElimination -> Morphism -> Result Morphism Source #

map_sentence :: CommonLogicModuleElimination -> Sign -> TEXT_META -> Result TEXT_META Source #

map_symbol :: CommonLogicModuleElimination -> Sign -> Symbol -> Set Symbol Source #

extractModel :: CommonLogicModuleElimination -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source #

is_model_transportable :: CommonLogicModuleElimination -> Bool Source #

has_model_expansion :: CommonLogicModuleElimination -> Bool Source #

is_weakly_amalgamable :: CommonLogicModuleElimination -> Bool Source #

constituents :: CommonLogicModuleElimination -> [String] Source #

isInclusionComorphism :: CommonLogicModuleElimination -> Bool Source #

rps :: CommonLogicModuleElimination -> Bool Source #

eps :: CommonLogicModuleElimination -> Bool Source #

Comorphism OWL22CommonLogic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Comorphism Prop2CommonLogic Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree 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 # 

data SYMB_OR_MAP Source #

Instances

Eq SYMB_OR_MAP Source # 

Methods

(==) :: SYMB_OR_MAP -> SYMB_OR_MAP -> Bool

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

Data SYMB_OR_MAP Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_OR_MAP -> c SYMB_OR_MAP

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_OR_MAP

toConstr :: SYMB_OR_MAP -> Constr

dataTypeOf :: SYMB_OR_MAP -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SYMB_OR_MAP)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_OR_MAP)

gmapT :: (forall b. Data b => b -> b) -> SYMB_OR_MAP -> SYMB_OR_MAP

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_OR_MAP -> r

gmapQ :: (forall d. Data d => d -> u) -> SYMB_OR_MAP -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_OR_MAP -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_OR_MAP -> m SYMB_OR_MAP

Ord SYMB_OR_MAP Source # 
Show SYMB_OR_MAP Source # 

Methods

showsPrec :: Int -> SYMB_OR_MAP -> ShowS

show :: SYMB_OR_MAP -> String

showList :: [SYMB_OR_MAP] -> ShowS

GetRange SYMB_OR_MAP Source # 
Pretty SYMB_OR_MAP Source # 

data SYMB_ITEMS Source #

Instances

Eq SYMB_ITEMS Source # 

Methods

(==) :: SYMB_ITEMS -> SYMB_ITEMS -> Bool

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

Data SYMB_ITEMS Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SYMB_ITEMS -> c SYMB_ITEMS

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SYMB_ITEMS

toConstr :: SYMB_ITEMS -> Constr

dataTypeOf :: SYMB_ITEMS -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SYMB_ITEMS)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SYMB_ITEMS)

gmapT :: (forall b. Data b => b -> b) -> SYMB_ITEMS -> SYMB_ITEMS

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SYMB_ITEMS -> r

gmapQ :: (forall d. Data d => d -> u) -> SYMB_ITEMS -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SYMB_ITEMS -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SYMB_ITEMS -> m SYMB_ITEMS

Ord SYMB_ITEMS Source # 
Show SYMB_ITEMS Source # 

Methods

showsPrec :: Int -> SYMB_ITEMS -> ShowS

show :: SYMB_ITEMS -> String

showList :: [SYMB_ITEMS] -> ShowS

GetRange SYMB_ITEMS Source # 
Pretty SYMB_ITEMS Source # 
Syntax CommonLogic BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source # 
StaticAnalysis CommonLogic BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source # 

Methods

basic_analysis :: CommonLogic -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])) Source #

sen_analysis :: CommonLogic -> Maybe ((BASIC_SPEC, Sign, TEXT_META) -> Result TEXT_META) Source #

extBasicAnalysis :: CommonLogic -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META]) Source #

stat_symb_map_items :: CommonLogic -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source #

stat_symb_items :: CommonLogic -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source #

convertTheory :: CommonLogic -> Maybe ((Sign, [Named TEXT_META]) -> BASIC_SPEC) Source #

ensures_amalgamability :: CommonLogic -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: CommonLogic -> Morphism -> [Named TEXT_META] -> Result (Sign, [Named TEXT_META]) Source #

signature_colimit :: CommonLogic -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: CommonLogic -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named TEXT_META]) Source #

symbol_to_raw :: CommonLogic -> Symbol -> Symbol Source #

id_to_raw :: CommonLogic -> Id -> Symbol Source #

matches :: CommonLogic -> Symbol -> Symbol -> Bool Source #

empty_signature :: CommonLogic -> Sign Source #

add_symb_to_sign :: CommonLogic -> Sign -> Symbol -> Result Sign Source #

signature_union :: CommonLogic -> Sign -> Sign -> Result Sign Source #

signatureDiff :: CommonLogic -> Sign -> Sign -> Result Sign Source #

intersection :: CommonLogic -> Sign -> Sign -> Result Sign Source #

final_union :: CommonLogic -> Sign -> Sign -> Result Sign Source #

morphism_union :: CommonLogic -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: CommonLogic -> Sign -> Sign -> Bool Source #

subsig_inclusion :: CommonLogic -> Sign -> Sign -> Result Morphism Source #

generated_sign :: CommonLogic -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: CommonLogic -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: CommonLogic -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: CommonLogic -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: CommonLogic -> Morphism -> Bool Source #

is_injective :: CommonLogic -> Morphism -> Bool Source #

theory_to_taxonomy :: CommonLogic -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named TEXT_META] -> Result MMiSSOntology Source #

corresp2th :: CommonLogic -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named TEXT_META], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: CommonLogic -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: CommonLogic -> [IRI] -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

Logic CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 

Methods

parse_basic_sen :: CommonLogic -> Maybe (BASIC_SPEC -> AParser st TEXT_META) Source #

stability :: CommonLogic -> Stability Source #

data_logic :: CommonLogic -> Maybe AnyLogic Source #

top_sublogic :: CommonLogic -> CommonLogicSL Source #

all_sublogics :: CommonLogic -> [CommonLogicSL] Source #

bottomSublogic :: CommonLogic -> Maybe CommonLogicSL Source #

sublogicDimensions :: CommonLogic -> [[CommonLogicSL]] Source #

parseSublogic :: CommonLogic -> String -> Maybe CommonLogicSL Source #

proj_sublogic_epsilon :: CommonLogic -> CommonLogicSL -> Sign -> Morphism Source #

provers :: CommonLogic -> [Prover Sign TEXT_META Morphism CommonLogicSL ProofTree] Source #

default_prover :: CommonLogic -> String Source #

cons_checkers :: CommonLogic -> [ConsChecker Sign TEXT_META CommonLogicSL Morphism ProofTree] Source #

conservativityCheck :: CommonLogic -> [ConservativityChecker Sign TEXT_META Morphism] Source #

empty_proof_tree :: CommonLogic -> ProofTree Source #

syntaxTable :: CommonLogic -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: CommonLogic -> Maybe OMCD Source #

export_symToOmdoc :: CommonLogic -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: CommonLogic -> NameMap Symbol -> TEXT_META -> Result TCorOMElement Source #

export_theoryToOmdoc :: CommonLogic -> SigMap Symbol -> Sign -> [Named TEXT_META] -> Result [TCElement] Source #

omdocToSym :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: CommonLogic -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named TEXT_META)) Source #

addOMadtToTheory :: CommonLogic -> SigMapI Symbol -> (Sign, [Named TEXT_META]) -> [[OmdADT]] -> Result (Sign, [Named TEXT_META]) Source #

addOmdocToTheory :: CommonLogic -> SigMapI Symbol -> (Sign, [Named TEXT_META]) -> [TCElement] -> Result (Sign, [Named TEXT_META]) Source #

Comorphism CL2CFOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # 
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CommonLogicModuleElimination CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 

Methods

sourceLogic :: CommonLogicModuleElimination -> CommonLogic Source #

sourceSublogic :: CommonLogicModuleElimination -> CommonLogicSL Source #

sourceSublogicLossy :: CommonLogicModuleElimination -> CommonLogicSL Source #

minSourceTheory :: CommonLogicModuleElimination -> Maybe (LibName, String) Source #

targetLogic :: CommonLogicModuleElimination -> CommonLogic Source #

mapSublogic :: CommonLogicModuleElimination -> CommonLogicSL -> Maybe CommonLogicSL Source #

map_theory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

mapMarkedTheory :: CommonLogicModuleElimination -> (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META]) Source #

map_morphism :: CommonLogicModuleElimination -> Morphism -> Result Morphism Source #

map_sentence :: CommonLogicModuleElimination -> Sign -> TEXT_META -> Result TEXT_META Source #

map_symbol :: CommonLogicModuleElimination -> Sign -> Symbol -> Set Symbol Source #

extractModel :: CommonLogicModuleElimination -> Sign -> ProofTree -> Result (Sign, [Named TEXT_META]) Source #

is_model_transportable :: CommonLogicModuleElimination -> Bool Source #

has_model_expansion :: CommonLogicModuleElimination -> Bool Source #

is_weakly_amalgamable :: CommonLogicModuleElimination -> Bool Source #

constituents :: CommonLogicModuleElimination -> [String] Source #

isInclusionComorphism :: CommonLogicModuleElimination -> Bool Source #

rps :: CommonLogicModuleElimination -> Bool Source #

eps :: CommonLogicModuleElimination -> Bool Source #

Comorphism OWL22CommonLogic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Source # 
Comorphism Prop2CommonLogic Propositional PropSL BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree 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 # 

orS :: String Source #

iffS :: String Source #

clCommentS :: String Source #

clTextS :: String Source #

clImportS :: String Source #

clModuleS :: String Source #

clExcludeS :: String Source #