 | hets -- a heterogenous Specification (CASL) tool set | Contents | Index |
|
CASL.Morphism | Portability | portable | Stability | provisional | Maintainer | hets@tzi.de |
|
|
|
|
|
Description |
Symbols and signature morphisms for the CASL logic
|
|
Synopsis |
|
| | data Symbol = Symbol {} | | type SymbolSet = Set Symbol | | type SymbolMap = EndoMap Symbol | | | | type RawSymbolSet = Set RawSymbol | | type RawSymbolMap = EndoMap RawSymbol | | | | type Sort_map = Map SORT SORT | | type Fun_map = Map (Id, OpType) (Id, FunKind) | | type Pred_map = Map (Id, PredType) Id | | data Morphism = Morphism {} | | 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 |
|
|
data Symbol |
|
|
type SymbolSet = Set Symbol |
|
type SymbolMap = EndoMap Symbol |
|
data RawSymbol |
|
|
type RawSymbolSet = Set RawSymbol |
|
type RawSymbolMap = EndoMap RawSymbol |
|
data Kind |
|
|
type Sort_map = Map SORT SORT |
|
type Fun_map = Map (Id, OpType) (Id, FunKind) |
|
type Pred_map = Map (Id, PredType) Id |
|
data Morphism |
|
|
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 |