Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|
Safe Haskell | None |
Equational signatures for Maude.
- data MaudeSig
- enableDH :: MaudeSig -> Bool
- enableBP :: MaudeSig -> Bool
- enableMSet :: MaudeSig -> Bool
- stFunSyms :: MaudeSig -> Set NoEqSym
- stRules :: MaudeSig -> Set StRule
- funSyms :: MaudeSig -> FunSig
- irreducibleFunSyms :: MaudeSig -> FunSig
- rrulesForMaudeSig :: MaudeSig -> Set (RRule LNTerm)
- noEqFunSyms :: MaudeSig -> NoEqFunSig
- dhMaudeSig :: MaudeSig
- pairMaudeSig :: MaudeSig
- asymEncMaudeSig :: MaudeSig
- symEncMaudeSig :: MaudeSig
- signatureMaudeSig :: MaudeSig
- hashMaudeSig :: MaudeSig
- msetMaudeSig :: MaudeSig
- bpMaudeSig :: MaudeSig
- minimalMaudeSig :: MaudeSig
- addFunSym :: NoEqSym -> 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
funSyms :: MaudeSig -> FunSigSource
function signature including the function symbols for DH, BP, and Multiset can be computed from enableX and stFunSyms
irreducibleFunSyms :: MaudeSig -> FunSigSource
irreducible function symbols (can be computed)
rrulesForMaudeSig :: MaudeSig -> Set (RRule LNTerm)Source
Returns all rewriting rules including the rules for DH, BP, and multiset.
noEqFunSyms :: MaudeSig -> NoEqFunSigSource
Non-AC function symbols.
predefined maude signatures
Maude signatures for the AC symbols.
pairMaudeSig :: MaudeSigSource
Maude signatures for the default subterm symbols.
asymEncMaudeSig :: MaudeSigSource
Maude signatures for the default subterm symbols.
symEncMaudeSig :: MaudeSigSource
Maude signatures for the default subterm symbols.
signatureMaudeSig :: MaudeSigSource
Maude signatures for the default subterm symbols.
hashMaudeSig :: MaudeSigSource
Maude signatures for the default subterm symbols.
msetMaudeSig :: MaudeSigSource
Maude signatures for the AC symbols.
Maude signatures for the AC symbols.
minimalMaudeSig :: MaudeSigSource
The minimal maude signature.
extend maude signatures
pretty printing
prettyMaudeSig :: HighlightDocument d => MaudeSig -> dSource