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

MaintainerBenedikt Schmidt <beschmi@gmail.com>
Safe HaskellNone

Term.Maude.Process

Contents

Description

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

Synopsis

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.

Constructors

MaudeHandle 

Fields

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.