| 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 |
Maude.Sign
Contents
Description
Definition of signatures for Maude.
- data Sign = Sign {}
- type SortSet = SymbolSet
- type KindRel = Map Symbol Symbol
- type SubsortRel = SymbolRel
- type OpDecl = (Set Symbol, [Attr])
- type OpDeclSet = Set OpDecl
- type OpMap = Map Qid OpDeclSet
- type Sentences = Set Sentence
- fromSpec :: Module -> Sign
- empty :: Sign
- union :: Sign -> Sign -> Sign
- intersection :: Sign -> Sign -> Sign
- symbols :: Sign -> SymbolSet
- isLegal :: Sign -> Bool
- isSubsign :: Sign -> Sign -> Bool
- simplifySentence :: Sign -> Sentence -> Sentence
- renameSort :: Symbol -> Symbol -> Sign -> Sign
- renameLabel :: Symbol -> Symbol -> Sign -> Sign
- renameOp :: Symbol -> Symbol -> [Attr] -> Sign -> Sign
- inlineSign :: Sign -> Doc
Types
The Signature type
data Sign
The Signature of a Maude Module.
Constructors
| Sign | |
Instances
| Eq Sign | |
| Ord Sign | |
| Show Sign | |
| ShATermConvertible Sign | |
| Pretty Sign | |
| HasSorts Sign | |
| HasOps Sign | |
| HasLabels Sign | |
| Typeable * Sign | |
| Category Sign Morphism | Instance of Category for Maude |
| Sentences Maude Sentence Sign Morphism Symbol | Instance of Sentences for Maude |
| StaticAnalysis Maude MaudeText Sentence () () Sign Morphism Symbol Symbol | Instance of StaticAnalysis for Maude |
| LogicalFramework Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () | |
| Logic Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () | 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 |
Auxiliary types
type SubsortRel = SymbolRel
Construction
Combination
intersection :: Sign -> Sign -> Sign
The intersection of two Signatures.
Conversion
Testing
Modification
simplifySentence :: Sign -> Sentence -> Sentence
Simplification of sentences (leave out qualifications)
Inline printing
inlineSign :: Sign -> Doc