Hets - the Heterogeneous Tool Set

Copyright(c) Christian Maeder and Uni Bremen 2003-2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellSafe

HasCASL.Le

Contents

Description

abstract syntax during static analysis

Synopsis

class info

data ClassInfo Source #

store the raw kind and all superclasses of a class identifier

Constructors

ClassInfo 

Fields

Instances

Eq ClassInfo Source # 

Methods

(==) :: ClassInfo -> ClassInfo -> Bool

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

Data ClassInfo Source # 

Methods

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

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

toConstr :: ClassInfo -> Constr

dataTypeOf :: ClassInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ClassInfo Source # 

Methods

compare :: ClassInfo -> ClassInfo -> Ordering

(<) :: ClassInfo -> ClassInfo -> Bool

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

(>) :: ClassInfo -> ClassInfo -> Bool

(>=) :: ClassInfo -> ClassInfo -> Bool

max :: ClassInfo -> ClassInfo -> ClassInfo

min :: ClassInfo -> ClassInfo -> ClassInfo

Show ClassInfo Source # 

Methods

showsPrec :: Int -> ClassInfo -> ShowS

show :: ClassInfo -> String

showList :: [ClassInfo] -> ShowS

type ClassMap = Map Id ClassInfo Source #

mapping class identifiers to their definition

type info

data GenKind Source #

data type generatedness indicator

Constructors

Free 
Generated 
Loose 

Instances

Eq GenKind Source # 

Methods

(==) :: GenKind -> GenKind -> Bool

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

Data GenKind Source # 

Methods

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

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

toConstr :: GenKind -> Constr

dataTypeOf :: GenKind -> DataType

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

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

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

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

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

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

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

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

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

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

Ord GenKind Source # 

Methods

compare :: GenKind -> GenKind -> Ordering

(<) :: GenKind -> GenKind -> Bool

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

(>) :: GenKind -> GenKind -> Bool

(>=) :: GenKind -> GenKind -> Bool

max :: GenKind -> GenKind -> GenKind

min :: GenKind -> GenKind -> GenKind

Show GenKind Source # 

Methods

showsPrec :: Int -> GenKind -> ShowS

show :: GenKind -> String

showList :: [GenKind] -> ShowS

data AltDefn Source #

an analysed alternative with a list of (product) types

Constructors

Construct (Maybe Id) [Type] Partiality [[Selector]] 

Instances

Eq AltDefn Source # 

Methods

(==) :: AltDefn -> AltDefn -> Bool

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

Data AltDefn Source # 

Methods

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

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

toConstr :: AltDefn -> Constr

dataTypeOf :: AltDefn -> DataType

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

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

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

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

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

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

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

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

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

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

Ord AltDefn Source # 

Methods

compare :: AltDefn -> AltDefn -> Ordering

(<) :: AltDefn -> AltDefn -> Bool

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

(>) :: AltDefn -> AltDefn -> Bool

(>=) :: AltDefn -> AltDefn -> Bool

max :: AltDefn -> AltDefn -> AltDefn

min :: AltDefn -> AltDefn -> AltDefn

Show AltDefn Source # 

Methods

showsPrec :: Int -> AltDefn -> ShowS

show :: AltDefn -> String

showList :: [AltDefn] -> ShowS

data Selector Source #

an analysed component

Constructors

Select (Maybe Id) Type Partiality 

Instances

Eq Selector Source # 

Methods

(==) :: Selector -> Selector -> Bool

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

Data Selector Source # 

Methods

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

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

toConstr :: Selector -> Constr

dataTypeOf :: Selector -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Selector Source # 

Methods

compare :: Selector -> Selector -> Ordering

(<) :: Selector -> Selector -> Bool

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

(>) :: Selector -> Selector -> Bool

(>=) :: Selector -> Selector -> Bool

max :: Selector -> Selector -> Selector

min :: Selector -> Selector -> Selector

Show Selector Source # 

Methods

showsPrec :: Int -> Selector -> ShowS

show :: Selector -> String

showList :: [Selector] -> ShowS

type IdMap = Map Id Id Source #

a mapping of type (and disjoint class) identifiers

data DataEntry Source #

data entries are produced from possibly mutual recursive data types. The top-level identifiers of these types are never renamed but there renaming is stored in the identifier map. This identifier map must never be empty (even without renamings) because (the domain of) this map is used to store the other (recursively dependent) top-level identifiers.

Instances

Eq DataEntry Source # 

Methods

(==) :: DataEntry -> DataEntry -> Bool

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

Data DataEntry Source # 

Methods

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

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

toConstr :: DataEntry -> Constr

dataTypeOf :: DataEntry -> DataType

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

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

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

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

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

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

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

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

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

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

Ord DataEntry Source # 

Methods

compare :: DataEntry -> DataEntry -> Ordering

(<) :: DataEntry -> DataEntry -> Bool

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

(>) :: DataEntry -> DataEntry -> Bool

(>=) :: DataEntry -> DataEntry -> Bool

max :: DataEntry -> DataEntry -> DataEntry

min :: DataEntry -> DataEntry -> DataEntry

Show DataEntry Source # 

Methods

showsPrec :: Int -> DataEntry -> ShowS

show :: DataEntry -> String

showList :: [DataEntry] -> ShowS

data TypeDefn Source #

possible definitions for type identifiers

Instances

Eq TypeDefn Source # 

Methods

(==) :: TypeDefn -> TypeDefn -> Bool

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

Data TypeDefn Source # 

Methods

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

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

toConstr :: TypeDefn -> Constr

dataTypeOf :: TypeDefn -> DataType

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

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

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

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

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

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

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

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

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

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

Ord TypeDefn Source # 

Methods

compare :: TypeDefn -> TypeDefn -> Ordering

(<) :: TypeDefn -> TypeDefn -> Bool

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

(>) :: TypeDefn -> TypeDefn -> Bool

(>=) :: TypeDefn -> TypeDefn -> Bool

max :: TypeDefn -> TypeDefn -> TypeDefn

min :: TypeDefn -> TypeDefn -> TypeDefn

Show TypeDefn Source # 

Methods

showsPrec :: Int -> TypeDefn -> ShowS

show :: TypeDefn -> String

showList :: [TypeDefn] -> ShowS

data TypeInfo Source #

for type identifiers also store the raw kind, instances and supertypes

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

type TypeMap = Map Id TypeInfo Source #

mapping type identifiers to their definition

starTypeInfo :: TypeInfo Source #

the minimal information for a sort

mapType :: IdMap -> Type -> Type Source #

rename the type according to identifier map (for comorphisms)

sentences

data Sentence Source #

data types are also special sentences because of their properties

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 # 
Sentences HasCASL Sentence Env Morphism Symbol Source # 
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source # 

Methods

basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source #

sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source #

stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source #

convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source #

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

quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source #

signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source #

qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source #

id_to_raw :: HasCASL -> Id -> RawSymbol Source #

matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: HasCASL -> Env Source #

add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source #

signature_union :: HasCASL -> Env -> Env -> Result Env Source #

signatureDiff :: HasCASL -> Env -> Env -> Result Env Source #

intersection :: HasCASL -> Env -> Env -> Result Env Source #

final_union :: HasCASL -> Env -> Env -> Result Env Source #

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

is_subsig :: HasCASL -> Env -> Env -> Bool Source #

subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source #

generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source #

induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source #

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

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

theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #

Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source #

stability :: HasCASL -> Stability Source #

data_logic :: HasCASL -> Maybe AnyLogic Source #

top_sublogic :: HasCASL -> Sublogic Source #

all_sublogics :: HasCASL -> [Sublogic] Source #

bottomSublogic :: HasCASL -> Maybe Sublogic Source #

sublogicDimensions :: HasCASL -> [[Sublogic]] Source #

parseSublogic :: HasCASL -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source #

provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source #

default_prover :: HasCASL -> String Source #

cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source #

conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source #

empty_proof_tree :: HasCASL -> () Source #

syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source #

omdoc_metatheory :: HasCASL -> Maybe OMCD Source #

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

export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source #

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

omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source #

addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source #

Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 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 # 

variables

data TypeVarDefn Source #

type variable are kept separately

Instances

Data TypeVarDefn Source # 

Methods

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

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

toConstr :: TypeVarDefn -> Constr

dataTypeOf :: TypeVarDefn -> DataType

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

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

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

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

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

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

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

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

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

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

Show TypeVarDefn Source # 

Methods

showsPrec :: Int -> TypeVarDefn -> ShowS

show :: TypeVarDefn -> String

showList :: [TypeVarDefn] -> ShowS

type LocalTypeVars = Map Id TypeVarDefn Source #

mapping type variables to their definition

data VarDefn Source #

the type of a local variable

Constructors

VarDefn Type 

Instances

Data VarDefn Source # 

Methods

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

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

toConstr :: VarDefn -> Constr

dataTypeOf :: VarDefn -> DataType

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

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

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

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

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

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

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

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

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

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

Show VarDefn Source # 

Methods

showsPrec :: Int -> VarDefn -> ShowS

show :: VarDefn -> String

showList :: [VarDefn] -> ShowS

assumptions

data ConstrInfo Source #

name and scheme of a constructor

Constructors

ConstrInfo 

Instances

Eq ConstrInfo Source # 

Methods

(==) :: ConstrInfo -> ConstrInfo -> Bool

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

Data ConstrInfo Source # 

Methods

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

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

toConstr :: ConstrInfo -> Constr

dataTypeOf :: ConstrInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Ord ConstrInfo Source # 
Show ConstrInfo Source # 

Methods

showsPrec :: Int -> ConstrInfo -> ShowS

show :: ConstrInfo -> String

showList :: [ConstrInfo] -> ShowS

data OpDefn Source #

possible definitions of functions

Constructors

NoOpDefn OpBrand 
ConstructData Id

target type

SelectData (Set ConstrInfo) Id

constructors of source type

Definition OpBrand Term 

Instances

Eq OpDefn Source # 

Methods

(==) :: OpDefn -> OpDefn -> Bool

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

Data OpDefn Source # 

Methods

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

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

toConstr :: OpDefn -> Constr

dataTypeOf :: OpDefn -> DataType

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

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

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

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

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

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

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

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

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

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

Ord OpDefn Source # 

Methods

compare :: OpDefn -> OpDefn -> Ordering

(<) :: OpDefn -> OpDefn -> Bool

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

(>) :: OpDefn -> OpDefn -> Bool

(>=) :: OpDefn -> OpDefn -> Bool

max :: OpDefn -> OpDefn -> OpDefn

min :: OpDefn -> OpDefn -> OpDefn

Show OpDefn Source # 

Methods

showsPrec :: Int -> OpDefn -> ShowS

show :: OpDefn -> String

showList :: [OpDefn] -> ShowS

data OpInfo Source #

scheme, attributes and definition for function identifiers

Constructors

OpInfo 

Fields

Instances

Eq OpInfo Source # 

Methods

(==) :: OpInfo -> OpInfo -> Bool

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

Data OpInfo Source # 

Methods

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

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

toConstr :: OpInfo -> Constr

dataTypeOf :: OpInfo -> DataType

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

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

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

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

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

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

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

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

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

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

Ord OpInfo Source # 

Methods

compare :: OpInfo -> OpInfo -> Ordering

(<) :: OpInfo -> OpInfo -> Bool

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

(>) :: OpInfo -> OpInfo -> Bool

(>=) :: OpInfo -> OpInfo -> Bool

max :: OpInfo -> OpInfo -> OpInfo

min :: OpInfo -> OpInfo -> OpInfo

Show OpInfo Source # 

Methods

showsPrec :: Int -> OpInfo -> ShowS

show :: OpInfo -> String

showList :: [OpInfo] -> ShowS

isConstructor :: OpInfo -> Bool Source #

test for constructor

type Assumps = Map Id (Set OpInfo) Source #

mapping operation identifiers to their definition

the local environment and final signature

data Env Source #

the signature is established by the classes, types and assumptions

Instances

Eq Env Source # 

Methods

(==) :: Env -> Env -> Bool

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

Data Env Source # 

Methods

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

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

toConstr :: Env -> Constr

dataTypeOf :: Env -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Env Source # 

Methods

compare :: Env -> Env -> Ordering

(<) :: Env -> Env -> Bool

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

(>) :: Env -> Env -> Bool

(>=) :: Env -> Env -> Bool

max :: Env -> Env -> Env

min :: Env -> Env -> Env

Show Env Source # 

Methods

showsPrec :: Int -> Env -> ShowS

show :: Env -> String

showList :: [Env] -> ShowS

Sentences HasCASL Sentence Env Morphism Symbol Source # 
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source # 

Methods

basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source #

sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source #

stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source #

convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source #

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

quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source #

signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source #

qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source #

id_to_raw :: HasCASL -> Id -> RawSymbol Source #

matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: HasCASL -> Env Source #

add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source #

signature_union :: HasCASL -> Env -> Env -> Result Env Source #

signatureDiff :: HasCASL -> Env -> Env -> Result Env Source #

intersection :: HasCASL -> Env -> Env -> Result Env Source #

final_union :: HasCASL -> Env -> Env -> Result Env Source #

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

is_subsig :: HasCASL -> Env -> Env -> Bool Source #

subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source #

generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source #

induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source #

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

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

theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #

Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source #

stability :: HasCASL -> Stability Source #

data_logic :: HasCASL -> Maybe AnyLogic Source #

top_sublogic :: HasCASL -> Sublogic Source #

all_sublogics :: HasCASL -> [Sublogic] Source #

bottomSublogic :: HasCASL -> Maybe Sublogic Source #

sublogicDimensions :: HasCASL -> [[Sublogic]] Source #

parseSublogic :: HasCASL -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source #

provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source #

default_prover :: HasCASL -> String Source #

cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source #

conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source #

empty_proof_tree :: HasCASL -> () Source #

syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source #

omdoc_metatheory :: HasCASL -> Maybe OMCD Source #

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

export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source #

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

omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source #

addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source #

Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 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 # 

initialEnv :: Env Source #

the empty environment (fresh variables start with 1)

data Constrain Source #

Instances

Eq Constrain Source # 

Methods

(==) :: Constrain -> Constrain -> Bool

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

Data Constrain Source # 

Methods

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

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

toConstr :: Constrain -> Constr

dataTypeOf :: Constrain -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Constrain Source # 

Methods

compare :: Constrain -> Constrain -> Ordering

(<) :: Constrain -> Constrain -> Bool

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

(>) :: Constrain -> Constrain -> Bool

(>=) :: Constrain -> Constrain -> Bool

max :: Constrain -> Constrain -> Constrain

min :: Constrain -> Constrain -> Constrain

Show Constrain Source # 

Methods

showsPrec :: Int -> Constrain -> ShowS

show :: Constrain -> String

showList :: [Constrain] -> ShowS

accessing the environment

addDiags :: [Diagnosis] -> State Env () Source #

add diagnostic messages

appendSentences :: [Named Sentence] -> State Env () Source #

add sentences

putClassMap :: ClassMap -> State Env () Source #

store a class map

putLocalVars :: Map Id VarDefn -> State Env () Source #

store local assumptions

fromResult :: (Env -> Result a) -> State Env (Maybe a) Source #

converting a result to a state computation

addSymbol :: Symbol -> State Env () Source #

add the symbol to the state

putLocalTypeVars :: LocalTypeVars -> State Env () Source #

store local type variables

putTypeMap :: TypeMap -> State Env () Source #

store a complete type map

putAssumps :: Assumps -> State Env () Source #

store assumptions

putBinders :: Map Id Id -> State Env () Source #

store assumptions

getVar :: VarDecl -> Id Source #

get the variable

checkUniqueVars :: [VarDecl] -> State Env () Source #

check uniqueness of variables

morphisms

data Morphism Source #

keep types and class disjoint and use a single identifier map for both

Constructors

Morphism 

Instances

Eq Morphism Source # 

Methods

(==) :: Morphism -> Morphism -> Bool

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

Data Morphism Source # 

Methods

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

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

toConstr :: Morphism -> Constr

dataTypeOf :: Morphism -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Morphism Source # 

Methods

compare :: Morphism -> Morphism -> Ordering

(<) :: Morphism -> Morphism -> Bool

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

(>) :: Morphism -> Morphism -> Bool

(>=) :: Morphism -> Morphism -> Bool

max :: Morphism -> Morphism -> Morphism

min :: Morphism -> Morphism -> Morphism

Show Morphism Source # 

Methods

showsPrec :: Int -> Morphism -> ShowS

show :: Morphism -> String

showList :: [Morphism] -> ShowS

Sentences HasCASL Sentence Env Morphism Symbol Source # 
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source # 

Methods

basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source #

sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source #

stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source #

convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source #

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

quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source #

signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source #

qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source #

id_to_raw :: HasCASL -> Id -> RawSymbol Source #

matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: HasCASL -> Env Source #

add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source #

signature_union :: HasCASL -> Env -> Env -> Result Env Source #

signatureDiff :: HasCASL -> Env -> Env -> Result Env Source #

intersection :: HasCASL -> Env -> Env -> Result Env Source #

final_union :: HasCASL -> Env -> Env -> Result Env Source #

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

is_subsig :: HasCASL -> Env -> Env -> Bool Source #

subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source #

generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source #

induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source #

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

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

theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #

Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source #

stability :: HasCASL -> Stability Source #

data_logic :: HasCASL -> Maybe AnyLogic Source #

top_sublogic :: HasCASL -> Sublogic Source #

all_sublogics :: HasCASL -> [Sublogic] Source #

bottomSublogic :: HasCASL -> Maybe Sublogic Source #

sublogicDimensions :: HasCASL -> [[Sublogic]] Source #

parseSublogic :: HasCASL -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source #

provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source #

default_prover :: HasCASL -> String Source #

cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source #

conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source #

empty_proof_tree :: HasCASL -> () Source #

syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source #

omdoc_metatheory :: HasCASL -> Maybe OMCD Source #

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

export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source #

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

omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source #

addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source #

Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 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 # 

mkMorphism :: Env -> Env -> Morphism Source #

construct morphism for subsignatures

symbol stuff

data SymbolType Source #

the type or kind of an identifier

Instances

Eq SymbolType Source # 

Methods

(==) :: SymbolType -> SymbolType -> Bool

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

Data SymbolType Source # 

Methods

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

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

toConstr :: SymbolType -> Constr

dataTypeOf :: SymbolType -> DataType

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

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

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

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

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

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

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

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

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

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

Ord SymbolType Source # 
Show SymbolType Source # 

Methods

showsPrec :: Int -> SymbolType -> ShowS

show :: SymbolType -> String

showList :: [SymbolType] -> ShowS

data Symbol Source #

symbols with their type

Constructors

Symbol 

Fields

Instances

Eq Symbol Source # 

Methods

(==) :: Symbol -> Symbol -> Bool

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

Data Symbol Source # 

Methods

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

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

toConstr :: Symbol -> Constr

dataTypeOf :: Symbol -> DataType

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

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

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

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

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

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

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

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

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

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

Ord Symbol Source # 

Methods

compare :: Symbol -> Symbol -> Ordering

(<) :: Symbol -> Symbol -> Bool

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

(>) :: Symbol -> Symbol -> Bool

(>=) :: Symbol -> Symbol -> Bool

max :: Symbol -> Symbol -> Symbol

min :: Symbol -> Symbol -> Symbol

Show Symbol Source # 

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

Sentences HasCASL Sentence Env Morphism Symbol Source # 
Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems Source # 
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source # 

Methods

basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source #

sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source #

stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source #

convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source #

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

quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source #

signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source #

qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source #

id_to_raw :: HasCASL -> Id -> RawSymbol Source #

matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: HasCASL -> Env Source #

add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source #

signature_union :: HasCASL -> Env -> Env -> Result Env Source #

signatureDiff :: HasCASL -> Env -> Env -> Result Env Source #

intersection :: HasCASL -> Env -> Env -> Result Env Source #

final_union :: HasCASL -> Env -> Env -> Result Env Source #

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

is_subsig :: HasCASL -> Env -> Env -> Bool Source #

subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source #

generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source #

induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source #

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

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

theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #

Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source #

stability :: HasCASL -> Stability Source #

data_logic :: HasCASL -> Maybe AnyLogic Source #

top_sublogic :: HasCASL -> Sublogic Source #

all_sublogics :: HasCASL -> [Sublogic] Source #

bottomSublogic :: HasCASL -> Maybe Sublogic Source #

sublogicDimensions :: HasCASL -> [[Sublogic]] Source #

parseSublogic :: HasCASL -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source #

provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source #

default_prover :: HasCASL -> String Source #

cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source #

conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source #

empty_proof_tree :: HasCASL -> () Source #

syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source #

omdoc_metatheory :: HasCASL -> Maybe OMCD Source #

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

export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source #

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

omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source #

addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source #

Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 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 # 

type SymbolMap = Map Symbol Symbol Source #

mapping symbols to symbols

type SymbolSet = Set Symbol Source #

a set of symbols

idToTypeSymbol :: Id -> RawKind -> Symbol Source #

create a type symbol

idToClassSymbol :: Id -> RawKind -> Symbol Source #

create a class symbol

idToOpSymbol :: Id -> TypeScheme -> Symbol Source #

create an operation symbol

data RawSymbol Source #

raw symbols where the type of a qualified raw symbol can be a type scheme and also be a kind if the symbol kind is unknown.

Instances

Eq RawSymbol Source # 

Methods

(==) :: RawSymbol -> RawSymbol -> Bool

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

Data RawSymbol Source # 

Methods

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

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

toConstr :: RawSymbol -> Constr

dataTypeOf :: RawSymbol -> DataType

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

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

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

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

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

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

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

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

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

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

Ord RawSymbol Source # 

Methods

compare :: RawSymbol -> RawSymbol -> Ordering

(<) :: RawSymbol -> RawSymbol -> Bool

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

(>) :: RawSymbol -> RawSymbol -> Bool

(>=) :: RawSymbol -> RawSymbol -> Bool

max :: RawSymbol -> RawSymbol -> RawSymbol

min :: RawSymbol -> RawSymbol -> RawSymbol

Show RawSymbol Source # 

Methods

showsPrec :: Int -> RawSymbol -> ShowS

show :: RawSymbol -> String

showList :: [RawSymbol] -> ShowS

StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source # 

Methods

basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source #

sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source #

stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source #

stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source #

convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source #

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

quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source #

signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source #

qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source #

id_to_raw :: HasCASL -> Id -> RawSymbol Source #

matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source #

empty_signature :: HasCASL -> Env Source #

add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source #

signature_union :: HasCASL -> Env -> Env -> Result Env Source #

signatureDiff :: HasCASL -> Env -> Env -> Result Env Source #

intersection :: HasCASL -> Env -> Env -> Result Env Source #

final_union :: HasCASL -> Env -> Env -> Result Env Source #

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

is_subsig :: HasCASL -> Env -> Env -> Bool Source #

subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source #

generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source #

induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source #

induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source #

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

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

theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #

Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 

Methods

parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source #

stability :: HasCASL -> Stability Source #

data_logic :: HasCASL -> Maybe AnyLogic Source #

top_sublogic :: HasCASL -> Sublogic Source #

all_sublogics :: HasCASL -> [Sublogic] Source #

bottomSublogic :: HasCASL -> Maybe Sublogic Source #

sublogicDimensions :: HasCASL -> [[Sublogic]] Source #

parseSublogic :: HasCASL -> String -> Maybe Sublogic Source #

proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source #

provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source #

default_prover :: HasCASL -> String Source #

cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source #

conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source #

empty_proof_tree :: HasCASL -> () Source #

syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source #

omdoc_metatheory :: HasCASL -> Maybe OMCD Source #

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

export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source #

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

omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source #

addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source #

Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source # 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 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 # 

type RawSymbolMap = Map RawSymbol RawSymbol Source #

mapping raw symbols to raw symbols

idToRaw :: Id -> RawSymbol Source #

create a raw symbol from an identifier

rawSymName :: RawSymbol -> Id Source #

extract the top identifer from a raw symbol

symbTypeToKind :: SymbolType -> SymbKind Source #

convert a symbol type to a symbol kind

symbolToRaw :: Symbol -> RawSymbol Source #

wrap a symbol as raw symbol (is ASymbol)

symbKindToRaw :: SymbKind -> Id -> RawSymbol Source #

create a raw symbol from a symbol kind and an identifier