Term.Unification

AC unification based on maude and free unification.

Unification modulo AC

unifyLTerm :: (IsConst c, Show (Lit c LVar), Ord c) => (c -> LSort) -> [Equal (LTerm c)] -> WithMaude [SubstVFresh c LVar]

unifyLNTerm eqs returns a complete set of unifiers for eqs modulo AC.

unifyLNTerm :: [Equal LNTerm] -> WithMaude [SubstVFresh Name LVar]

unifyLNTerm eqs returns a complete set of unifiers for eqs modulo AC.

unifiableLNTerms :: LNTerm -> LNTerm -> WithMaude Bool

True iff the terms are unifiable.

unifyLTermFactored :: (IsConst c, Show (Lit c LVar), Ord c) => (c -> LSort) -> [Equal (LTerm c)] -> WithMaude (LSubst c, [SubstVFresh c LVar])

unifyLTerm sortOf eqs returns a complete set of unifiers for eqs modulo AC.

unifyLNTermFactored :: [Equal LNTerm] -> WithMaude (LNSubst, [SubstVFresh Name LVar])

unifyLTerm sortOf eqs returns a complete set of unifiers for eqs modulo AC.

matching modulo AC

Constructing matching problems

matchLVar :: LVar -> LVar -> Match (LTerm c)

Match an LVar term to an LVar pattern.

Solving matching problems

solveMatchLTerm :: (IsConst c, Show (Lit c LVar), Ord c) => (c -> LSort) -> Match (LTerm c) -> WithMaude [Subst c LVar]

solveMatchLNTerm sortOf eqs returns a complete set of matchers for eqs modulo AC.

solveMatchLNTerm :: Match LNTerm -> WithMaude [Subst Name LVar]

solveMatchLNTerm eqs returns a complete set of matchers for eqs modulo AC.

Handles to a Maude process

data MaudeHandle

A handle to a Maude process. It requires the Maude path for Signatures to be serializable. If we also add the string for the Maude config file, then it would even be serializable on its own.

type WithMaude = Reader MaudeHandle

Values that depend on a MaudeHandle.

startMaude :: FilePath -> MaudeSig -> IO MaudeHandle

startMaude starts a new instance of Maude and returns a Handle to it.

getMaudeStats :: MaudeHandle -> IO String

getMaudeStats returns the maude stats formatted as a string.

mhMaudeSig :: MaudeHandle -> MaudeSig

mhFilePath :: MaudeHandle -> FilePath

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

minimalMaudeSig :: MaudeSig

The minimal maude signature.

dhMaudeSig, msetMaudeSig, xorMaudeSig :: MaudeSig

Maude signatures for the AC symbols.

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

Maude signatures for the default subterm symbols.

rrulesForMaudeSig :: MaudeSig -> Set (RRule LNTerm)

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

allFunctionSymbols :: MaudeSig -> Set NonACSym

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

stRules :: MaudeSig -> Set StRule

irreducibleFunctionSymbols :: MaudeSig -> Set NonACSym

addFunctionSymbol :: NonACSym -> MaudeSig -> MaudeSig

Add function symbol to given maude signature.

addStRule :: StRule -> MaudeSig -> MaudeSig

Add subterm rule to given maude signature.

Convenience exports

module Term.Substitution

module Term.Rewriting.Definitions