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

MaintainerBenedikt Schmidt <beschmi@gmail.com>
Safe HaskellNone




AC-unification of DH terms using Maude as a backend.


Handle to a maude process

data MaudeHandle Source

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.




mhFilePath :: FilePath
mhMaudeSig :: MaudeSig
mhProc :: MVar MaudeProcess

startMaude :: FilePath -> MaudeSig -> IO MaudeHandleSource

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

getMaudeStats :: MaudeHandle -> IO StringSource

getMaudeStats returns the maude stats formatted as a string.

Unification using Maude

unifyViaMaude :: (IsConst c, Show (Lit c LVar), Ord c) => MaudeHandle -> (c -> LSort) -> [Equal (VTerm c LVar)] -> IO [SubstVFresh c LVar]Source

unifyViaMaude hnd eqs computes all AC unifiers of eqs using the Maude process hnd.

Matching using Maude

matchViaMaude :: (IsConst c, Show (Lit c LVar), Ord c) => MaudeHandle -> (c -> LSort) -> [Match (VTerm c LVar)] -> IO [Subst c LVar]Source

matchViaMaude (t, p) computes a complete set of AC matchers of the term t to the pattern p via Maude.

Normalization using Maude

normViaMaude :: (IsConst c, Show (Lit c LVar), Ord c) => MaudeHandle -> (c -> LSort) -> VTerm c LVar -> IO (VTerm c LVar)Source

normViaMaude t normalizes the term t via Maude.

Managing the persistent Maude process

type WithMaude = Reader MaudeHandleSource

Values that depend on a MaudeHandle.