hets -- a heterogenous Specification (CASL) tool setContentsIndex
CASL.Morphism
Portability portable
Stability provisional
Maintainer hets@tzi.de
Description
Symbols and signature morphisms for the CASL logic
Synopsis
data SymbType
= OpAsItemType OpType
| PredAsItemType PredType
| SortAsItemType
data Symbol = Symbol {
symName :: Id
symbType :: SymbType
}
type SymbolSet = Set Symbol
type SymbolMap = EndoMap Symbol
data RawSymbol
= ASymbol Symbol
| AnID Id
| AKindedId Kind Id
type RawSymbolSet = Set RawSymbol
type RawSymbolMap = EndoMap RawSymbol
data Kind
= SortKind
| FunKind
| PredKind
type Sort_map = Map SORT SORT
type Fun_map = Map (Id, OpType) (Id, FunKind)
type Pred_map = Map (Id, PredType) Id
data Morphism = Morphism {
msource :: Sign
mtarget :: Sign
sort_map :: Sort_map
fun_map :: Fun_map
pred_map :: Pred_map
}
mapSort :: Sort_map -> SORT -> SORT
mapOpType :: Sort_map -> OpType -> OpType
mapOpTypeK :: Sort_map -> FunKind -> OpType -> OpType
makeTotal :: FunKind -> OpType -> OpType
mapOpSym :: Sort_map -> Fun_map -> (Id, OpType) -> Maybe (Id, OpType)
compatibleOpTypes :: OpType -> OpType -> Bool
mapPredType :: Sort_map -> PredType -> PredType
mapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> Maybe (Id, PredType)
embedMorphism :: Sign -> Sign -> Morphism
sentenceTc :: TyCon
signTc :: TyCon
morphismTc :: TyCon
symbolTc :: TyCon
rawSymbolTc :: TyCon
idToSortSymbol :: Id -> Symbol
idToOpSymbol :: Id -> OpType -> Symbol
idToPredSymbol :: Id -> PredType -> Symbol
symbTypeToKind :: SymbType -> Kind
symbolToRaw :: Symbol -> RawSymbol
idToRaw :: Id -> RawSymbol
rawSymName :: RawSymbol -> SORT
symOf :: Sign -> SymbolSet
statSymbMapItems :: [SYMB_MAP_ITEMS] -> Result RawSymbolMap
pairM :: Monad m => (m a, m b) -> m (a, b)
symbOrMapToRaw :: SYMB_KIND -> SYMB_OR_MAP -> Result (RawSymbol, RawSymbol)
statSymbItems :: [SYMB_ITEMS] -> Result [RawSymbol]
symbToRaw :: SYMB_KIND -> SYMB -> Result RawSymbol
symbKindToRaw :: SYMB_KIND -> Id -> Result RawSymbol
typedSymbKindToRaw :: SYMB_KIND -> Id -> TYPE -> Result RawSymbol
symbMapToMorphism :: Sign -> Sign -> SymbolMap -> Result Morphism
morphismToSymbMap :: Morphism -> SymbolMap
matches :: Symbol -> RawSymbol -> Bool
idMor :: Sign -> Morphism
compose :: Morphism -> Morphism -> Maybe Morphism
sigInclusion :: Sign -> Sign -> Result Morphism
Documentation
data SymbType
Constructors
OpAsItemType OpType
PredAsItemType PredType
SortAsItemType
Instances
ATermConvertible SymbType
Ord SymbType
Eq SymbType
PrettyPrint SymbType
Show SymbType
data Symbol
Constructors
Symbol
symName :: Id
symbType :: SymbType
Instances
ATermConvertible Symbol
Sentences CASL FORMULA () Sign Morphism Symbol
StaticAnalysis CASL BASIC_SPEC FORMULA () SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol
Logic CASL CASL_Sublogics BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol ()
Typeable Symbol
PrettyPrint Symbol
Show Symbol
Eq Symbol
Ord Symbol
Comorphism CASL2HasCASL CASL CASL_Sublogics BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol () HasCASL HasCASL_Sublogics BasicSpec Term SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
type SymbolSet = Set Symbol
type SymbolMap = EndoMap Symbol
data RawSymbol
Constructors
ASymbol Symbol
AnID Id
AKindedId Kind Id
Instances
ATermConvertible RawSymbol
StaticAnalysis CASL BASIC_SPEC FORMULA () SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol
Logic CASL CASL_Sublogics BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol ()
Typeable RawSymbol
PrettyPrint RawSymbol
Show RawSymbol
Eq RawSymbol
Ord RawSymbol
Comorphism CASL2HasCASL CASL CASL_Sublogics BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol () HasCASL HasCASL_Sublogics BasicSpec Term SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
type RawSymbolSet = Set RawSymbol
type RawSymbolMap = EndoMap RawSymbol
data Kind
Constructors
SortKind
FunKind
PredKind
Instances
ATermConvertible Kind
PrettyPrint Kind
Show Kind
Eq Kind
Ord Kind
type Sort_map = Map SORT SORT
type Fun_map = Map (Id, OpType) (Id, FunKind)
type Pred_map = Map (Id, PredType) Id
data Morphism
Constructors
Morphism
msource :: Sign
mtarget :: Sign
sort_map :: Sort_map
fun_map :: Fun_map
pred_map :: Pred_map
Instances
ATermConvertible Morphism
Category CASL Sign Morphism
Sentences CASL FORMULA () Sign Morphism Symbol
StaticAnalysis CASL BASIC_SPEC FORMULA () SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol
Logic CASL CASL_Sublogics BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol ()
Typeable Morphism
PrettyPrint Morphism
Eq Morphism
Show Morphism
Comorphism CASL2HasCASL CASL CASL_Sublogics BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol () HasCASL HasCASL_Sublogics BasicSpec Term SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
mapSort :: Sort_map -> SORT -> SORT
mapOpType :: Sort_map -> OpType -> OpType
mapOpTypeK :: Sort_map -> FunKind -> OpType -> OpType
makeTotal :: FunKind -> OpType -> OpType
mapOpSym :: Sort_map -> Fun_map -> (Id, OpType) -> Maybe (Id, OpType)
compatibleOpTypes :: OpType -> OpType -> Bool
Check if two OpTypes are equal except from totality or partiality
mapPredType :: Sort_map -> PredType -> PredType
mapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> Maybe (Id, PredType)
embedMorphism :: Sign -> Sign -> Morphism
sentenceTc :: TyCon
signTc :: TyCon
morphismTc :: TyCon
symbolTc :: TyCon
rawSymbolTc :: TyCon
idToSortSymbol :: Id -> Symbol
idToOpSymbol :: Id -> OpType -> Symbol
idToPredSymbol :: Id -> PredType -> Symbol
symbTypeToKind :: SymbType -> Kind
symbolToRaw :: Symbol -> RawSymbol
idToRaw :: Id -> RawSymbol
rawSymName :: RawSymbol -> SORT
symOf :: Sign -> SymbolSet
statSymbMapItems :: [SYMB_MAP_ITEMS] -> Result RawSymbolMap
pairM :: Monad m => (m a, m b) -> m (a, b)
symbOrMapToRaw :: SYMB_KIND -> SYMB_OR_MAP -> Result (RawSymbol, RawSymbol)
statSymbItems :: [SYMB_ITEMS] -> Result [RawSymbol]
symbToRaw :: SYMB_KIND -> SYMB -> Result RawSymbol
symbKindToRaw :: SYMB_KIND -> Id -> Result RawSymbol
typedSymbKindToRaw :: SYMB_KIND -> Id -> TYPE -> Result RawSymbol
symbMapToMorphism :: Sign -> Sign -> SymbolMap -> Result Morphism
morphismToSymbMap :: Morphism -> SymbolMap
matches :: Symbol -> RawSymbol -> Bool
idMor :: Sign -> Morphism
compose :: Morphism -> Morphism -> Maybe Morphism
sigInclusion :: Sign -> Sign -> Result Morphism
Produced by Haddock version 0.6