Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|
Safe Haskell | None |
Euqatiuonal signatures for Maude.
- data MaudeSig
- enableDH :: MaudeSig -> Bool
- enableXor :: MaudeSig -> Bool
- enableMSet :: MaudeSig -> Bool
- functionSymbols :: MaudeSig -> Set NonACSym
- stRules :: MaudeSig -> Set StRule
- allFunctionSymbols :: MaudeSig -> Set NonACSym
- irreducibleFunctionSymbols :: MaudeSig -> Set NonACSym
- rrulesForMaudeSig :: MaudeSig -> Set (RRule LNTerm)
- dhMaudeSig, msetMaudeSig, xorMaudeSig :: MaudeSig
- pairMaudeSig, hashMaudeSig, signatureMaudeSig, asymEncMaudeSig, symEncMaudeSig :: MaudeSig
- minimalMaudeSig :: MaudeSig
- addFunctionSymbol :: NonACSym -> MaudeSig -> MaudeSig
- addStRule :: StRule -> MaudeSig -> MaudeSig
- prettyMaudeSig :: HighlightDocument d => MaudeSig -> d
Maude signatures
The required information to define a Maude functional module
.
enableMSet :: MaudeSig -> BoolSource
functionSymbols :: MaudeSig -> Set NonACSymSource
function signature not including the function symbols for DH, Xor, and MSet
allFunctionSymbols :: MaudeSig -> Set NonACSymSource
function signature including the nonAC function symbols for DH, Xor, and MSet can be computed from enableX and functionSymbols
rrulesForMaudeSig :: MaudeSig -> Set (RRule LNTerm)Source
rrulesForMaudeSig msig
returns all rewriting rules including the rules
for xor, dh, and multiset.
predefined maude signatures
dhMaudeSig, msetMaudeSig, xorMaudeSig :: MaudeSigSource
Maude signatures for the AC symbols.
pairMaudeSig, hashMaudeSig, signatureMaudeSig, asymEncMaudeSig, symEncMaudeSig :: MaudeSigSource
Maude signatures for the default subterm symbols.
minimalMaudeSig :: MaudeSigSource
The minimal maude signature.
extend maude signatures
addFunctionSymbol :: NonACSym -> MaudeSig -> MaudeSigSource
Add function symbol to given maude signature.
pretty printing
prettyMaudeSig :: HighlightDocument d => MaudeSig -> dSource