Hets - the Heterogeneous Tool Set

Copyright(c) A. Tsogias DFKI Bremen 2011
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerAlexis.Tsogias@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellSafe

THF.Sign

Description

Data structures and functions for thf THF Signatures. Note: Most of the implenentations support only THF0.

Documentation

data SignTHF Source #

Constructors

Sign 

Instances

Eq SignTHF Source # 

Methods

(==) :: SignTHF -> SignTHF -> Bool

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

Data SignTHF Source # 

Methods

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

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

toConstr :: SignTHF -> Constr

dataTypeOf :: SignTHF -> DataType

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

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

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

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

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

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

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

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

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

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

Ord SignTHF Source # 

Methods

compare :: SignTHF -> SignTHF -> Ordering

(<) :: SignTHF -> SignTHF -> Bool

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

(>) :: SignTHF -> SignTHF -> Bool

(>=) :: SignTHF -> SignTHF -> Bool

max :: SignTHF -> SignTHF -> SignTHF

min :: SignTHF -> SignTHF -> SignTHF

Show SignTHF Source # 

Methods

showsPrec :: Int -> SignTHF -> ShowS

show :: SignTHF -> String

showList :: [SignTHF] -> ShowS

GetRange SignTHF Source # 
Sentences THF THFFormula SignTHF MorphismTHF SymbolTHF Source # 
StaticAnalysis THF BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () Source # 

Methods

basic_analysis :: THF -> Maybe ((BasicSpecTHF, SignTHF, GlobalAnnos) -> Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])) Source #

sen_analysis :: THF -> Maybe ((BasicSpecTHF, SignTHF, THFFormula) -> Result THFFormula) Source #

extBasicAnalysis :: THF -> IRI -> LibName -> BasicSpecTHF -> SignTHF -> GlobalAnnos -> Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula]) Source #

stat_symb_map_items :: THF -> SignTHF -> Maybe SignTHF -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: THF -> SignTHF -> [()] -> Result [()] Source #

convertTheory :: THF -> Maybe ((SignTHF, [Named THFFormula]) -> BasicSpecTHF) Source #

ensures_amalgamability :: THF -> ([CASLAmalgOpt], Gr SignTHF (Int, MorphismTHF), [(Int, MorphismTHF)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: THF -> MorphismTHF -> [Named THFFormula] -> Result (SignTHF, [Named THFFormula]) Source #

signature_colimit :: THF -> Gr SignTHF (Int, MorphismTHF) -> Result (SignTHF, Map Int MorphismTHF) Source #

qualify :: THF -> SIMPLE_ID -> LibName -> MorphismTHF -> SignTHF -> Result (MorphismTHF, [Named THFFormula]) Source #

symbol_to_raw :: THF -> SymbolTHF -> () Source #

id_to_raw :: THF -> Id -> () Source #

matches :: THF -> SymbolTHF -> () -> Bool Source #

empty_signature :: THF -> SignTHF Source #

add_symb_to_sign :: THF -> SignTHF -> SymbolTHF -> Result SignTHF Source #

signature_union :: THF -> SignTHF -> SignTHF -> Result SignTHF Source #

signatureDiff :: THF -> SignTHF -> SignTHF -> Result SignTHF Source #

intersection :: THF -> SignTHF -> SignTHF -> Result SignTHF Source #

final_union :: THF -> SignTHF -> SignTHF -> Result SignTHF Source #

morphism_union :: THF -> MorphismTHF -> MorphismTHF -> Result MorphismTHF Source #

is_subsig :: THF -> SignTHF -> SignTHF -> Bool Source #

subsig_inclusion :: THF -> SignTHF -> SignTHF -> Result MorphismTHF Source #

generated_sign :: THF -> Set SymbolTHF -> SignTHF -> Result MorphismTHF Source #

cogenerated_sign :: THF -> Set SymbolTHF -> SignTHF -> Result MorphismTHF Source #

induced_from_morphism :: THF -> EndoMap () -> SignTHF -> Result MorphismTHF Source #

induced_from_to_morphism :: THF -> EndoMap () -> ExtSign SignTHF SymbolTHF -> ExtSign SignTHF SymbolTHF -> Result MorphismTHF Source #

is_transportable :: THF -> MorphismTHF -> Bool Source #

is_injective :: THF -> MorphismTHF -> Bool Source #

theory_to_taxonomy :: THF -> TaxoGraphKind -> MMiSSOntology -> SignTHF -> [Named THFFormula] -> Result MMiSSOntology Source #

corresp2th :: THF -> String -> Bool -> SignTHF -> SignTHF -> [()] -> [()] -> EndoMap SymbolTHF -> EndoMap SymbolTHF -> REL_REF -> Result (SignTHF, [Named THFFormula], SignTHF, SignTHF, EndoMap SymbolTHF, EndoMap SymbolTHF) Source #

equiv2cospan :: THF -> SignTHF -> SignTHF -> [()] -> [()] -> Result (SignTHF, SignTHF, SignTHF, EndoMap SymbolTHF, EndoMap SymbolTHF) Source #

extract_module :: THF -> [IRI] -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

Logic THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 

Methods

parse_basic_sen :: THF -> Maybe (BasicSpecTHF -> AParser st THFFormula) Source #

stability :: THF -> Stability Source #

data_logic :: THF -> Maybe AnyLogic Source #

top_sublogic :: THF -> THFSl Source #

all_sublogics :: THF -> [THFSl] Source #

bottomSublogic :: THF -> Maybe THFSl Source #

sublogicDimensions :: THF -> [[THFSl]] Source #

parseSublogic :: THF -> String -> Maybe THFSl Source #

proj_sublogic_epsilon :: THF -> THFSl -> SignTHF -> MorphismTHF Source #

provers :: THF -> [Prover SignTHF THFFormula MorphismTHF THFSl ProofTree] Source #

default_prover :: THF -> String Source #

cons_checkers :: THF -> [ConsChecker SignTHF THFFormula THFSl MorphismTHF ProofTree] Source #

conservativityCheck :: THF -> [ConservativityChecker SignTHF THFFormula MorphismTHF] Source #

empty_proof_tree :: THF -> ProofTree Source #

syntaxTable :: THF -> SignTHF -> Maybe SyntaxTable Source #

omdoc_metatheory :: THF -> Maybe OMCD Source #

export_symToOmdoc :: THF -> NameMap SymbolTHF -> SymbolTHF -> String -> Result TCElement Source #

export_senToOmdoc :: THF -> NameMap SymbolTHF -> THFFormula -> Result TCorOMElement Source #

export_theoryToOmdoc :: THF -> SigMap SymbolTHF -> SignTHF -> [Named THFFormula] -> Result [TCElement] Source #

omdocToSym :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result SymbolTHF Source #

omdocToSen :: THF -> SigMapI SymbolTHF -> TCElement -> String -> Result (Maybe (Named THFFormula)) Source #

addOMadtToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [[OmdADT]] -> Result (SignTHF, [Named THFFormula]) Source #

addOmdocToTheory :: THF -> SigMapI SymbolTHF -> (SignTHF, [Named THFFormula]) -> [TCElement] -> Result (SignTHF, [Named THFFormula]) Source #

Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP2THF0 THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism THFP_P2THFP THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 

data TypeInfo Source #

Constructors

TypeInfo 

Instances

Eq TypeInfo Source # 

Methods

(==) :: TypeInfo -> TypeInfo -> Bool

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

Data TypeInfo Source # 

Methods

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

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

toConstr :: TypeInfo -> Constr

dataTypeOf :: TypeInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Ord TypeInfo Source # 

Methods

compare :: TypeInfo -> TypeInfo -> Ordering

(<) :: TypeInfo -> TypeInfo -> Bool

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

(>) :: TypeInfo -> TypeInfo -> Bool

(>=) :: TypeInfo -> TypeInfo -> Bool

max :: TypeInfo -> TypeInfo -> TypeInfo

min :: TypeInfo -> TypeInfo -> TypeInfo

Show TypeInfo Source # 

Methods

showsPrec :: Int -> TypeInfo -> ShowS

show :: TypeInfo -> String

showList :: [TypeInfo] -> ShowS

data ConstInfo Source #

Instances

Eq ConstInfo Source # 

Methods

(==) :: ConstInfo -> ConstInfo -> Bool

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

Data ConstInfo Source # 

Methods

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

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

toConstr :: ConstInfo -> Constr

dataTypeOf :: ConstInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ConstInfo Source # 

Methods

compare :: ConstInfo -> ConstInfo -> Ordering

(<) :: ConstInfo -> ConstInfo -> Bool

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

(>) :: ConstInfo -> ConstInfo -> Bool

(>=) :: ConstInfo -> ConstInfo -> Bool

max :: ConstInfo -> ConstInfo -> ConstInfo

min :: ConstInfo -> ConstInfo -> ConstInfo

Show ConstInfo Source # 

Methods

showsPrec :: Int -> ConstInfo -> ShowS

show :: ConstInfo -> String

showList :: [ConstInfo] -> ShowS

type EitherMap c x = Map c (Either x Diagnosis) Source #

toEitherLeftMap :: Map c x -> EitherMap c x Source #

eitherMapGetMap :: EitherMap c x -> Map c x Source #

genRes :: EitherMap c x -> Either (Map c x) [Diagnosis] Source #

unite :: (Ord c, Eq x, Show x) => String -> EitherMap c x -> EitherMap c x -> EitherMap c x Source #

diff :: (Ord c, Eq x) => Map c x -> Map c x -> Map c x Source #

intersect :: (Ord c, Eq x, Show x) => String -> EitherMap c x -> EitherMap c x -> EitherMap c x Source #