tamarin-prover-term-0.8.5.1: Term manipulation library for the tamarin prover.

Maintainer	Benedikt Schmidt <beschmi@gmail.com>
Safe Haskell	None

Term.Maude.Signature

Contents

Maude signatures
predefined maude signatures
extend maude signatures
pretty printing

Description

Equational signatures for Maude.

Synopsis

Maude signatures

data MaudeSig Source

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 Source

enableBP :: MaudeSig -> Bool Source

enableMSet :: MaudeSig -> Bool Source

stFunSyms :: MaudeSig -> Set NoEqSym Source

function signature for subterm theory

stRules :: MaudeSig -> Set StRule Source

rewriting rules for subterm theory

funSyms :: MaudeSig -> FunSig Source

function signature including the function symbols for DH, BP, and Multiset can be computed from enableX and stFunSyms

irreducibleFunSyms :: MaudeSig -> FunSig Source

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 -> NoEqFunSig Source

Non-AC function symbols.

predefined maude signatures

dhMaudeSig :: MaudeSig Source

Maude signatures for the AC symbols.

pairMaudeSig :: MaudeSig Source

Maude signatures for the default subterm symbols.

asymEncMaudeSig :: MaudeSig Source

Maude signatures for the default subterm symbols.

symEncMaudeSig :: MaudeSig Source

Maude signatures for the default subterm symbols.

signatureMaudeSig :: MaudeSig Source

Maude signatures for the default subterm symbols.

hashMaudeSig :: MaudeSig Source

Maude signatures for the default subterm symbols.

msetMaudeSig :: MaudeSig Source

Maude signatures for the AC symbols.

bpMaudeSig :: MaudeSig Source

Maude signatures for the AC symbols.

minimalMaudeSig :: MaudeSig Source

The minimal maude signature.

extend maude signatures

addFunSym :: NoEqSym -> MaudeSig -> MaudeSig Source

Add function symbol to given maude signature.

addStRule :: StRule -> MaudeSig -> MaudeSig Source

Add subterm rule to given maude signature.

pretty printing

prettyMaudeSig :: HighlightDocument d => MaudeSig -> dSource