Term.Maude.Signature

Euqatiuonal signatures for Maude.

Maude signatures

data MaudeSig

The required information to define a Maude functional module.

Instances

Eq MaudeSig

Ord MaudeSig

Show MaudeSig

Monoid MaudeSig

A monoid instance to combine maude signatures.

Binary MaudeSig

NFData MaudeSig

enableDH :: MaudeSig -> Bool

enableXor :: MaudeSig -> Bool

enableMSet :: MaudeSig -> Bool

functionSymbols :: MaudeSig -> Set NonACSym

function signature not including the function symbols for DH, Xor, and MSet

stRules :: MaudeSig -> Set StRule

allFunctionSymbols :: MaudeSig -> Set NonACSym

function signature including the nonAC function symbols for DH, Xor, and MSet can be computed from enableX and functionSymbols

irreducibleFunctionSymbols :: MaudeSig -> Set NonACSym

rrulesForMaudeSig :: MaudeSig -> Set (RRule LNTerm)

rrulesForMaudeSig msig returns all rewriting rules including the rules for xor, dh, and multiset.

predefined maude signatures

dhMaudeSig, msetMaudeSig, xorMaudeSig :: MaudeSig

Maude signatures for the AC symbols.

pairMaudeSig, hashMaudeSig, signatureMaudeSig, asymEncMaudeSig, symEncMaudeSig :: MaudeSig

Maude signatures for the default subterm symbols.

minimalMaudeSig :: MaudeSig

The minimal maude signature.

extend maude signatures

addFunctionSymbol :: NonACSym -> MaudeSig -> MaudeSig

Add function symbol to given maude signature.

addStRule :: StRule -> MaudeSig -> MaudeSig

Add subterm rule to given maude signature.

pretty printing

prettyMaudeSig :: HighlightDocument d => MaudeSig -> d