Copyright | (c) Martin Kuehl Uni Bremen 2008-2009 |
---|---|

License | GPLv2 or higher, see LICENSE.txt |

Maintainer | mkhl@informatik.uni-bremen.de |

Stability | experimental |

Portability | portable |

Safe Haskell | None |

Definition of morphisms for Maude.

- data Morphism = Morphism {}
- type SortMap = SymbolMap
- type KindMap = SymbolMap
- type OpMap = SymbolMap
- fromSignRenamings :: Sign -> [Renaming] -> Morphism
- fromSignsRenamings :: Sign -> Sign -> [Renaming] -> Morphism
- empty :: Morphism
- identity :: Sign -> Morphism
- inclusion :: Sign -> Sign -> Morphism
- inverse :: Morphism -> Result Morphism
- union :: Morphism -> Morphism -> Morphism
- compose :: Morphism -> Morphism -> Result Morphism
- isInclusion :: Morphism -> Bool
- isLegal :: Morphism -> Result ()
- symbolMap :: Morphism -> SymbolMap
- setTarget :: Sign -> Morphism -> Morphism
- qualifySorts :: Morphism -> Qid -> Symbols -> Morphism
- applyRenamings :: Morphism -> [Renaming] -> Morphism
- extendWithSortRenaming :: Symbol -> Symbol -> Morphism -> Morphism
- translateSentence :: Morphism -> Sentence -> Result Sentence
- translateSorts :: HasSorts a => Morphism -> a -> a

# Types

## The Morphism type

Eq Morphism Source # | |

Ord Morphism Source # | |

Show Morphism Source # | |

Pretty Morphism Source # | |

Sentences Maude Sentence Sign Morphism Symbol Source # | Instance of Sentences for Maude |

StaticAnalysis Maude MaudeText Sentence () () Sign Morphism Symbol Symbol Source # | Instance of StaticAnalysis for Maude |

LogicalFramework Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () Source # | |

Logic Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () Source # | Instance of Logic for Maude |

Comorphism Maude2CASL Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source # | |

## Auxiliary type

# Construction

# Combination

# Testing

isInclusion :: Morphism -> Bool Source #

True iff the `Morphism`

is an inclusion