Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|
Safe Haskell | None |
AC-unification of DH terms using Maude as a backend.
- data MaudeHandle = MaudeHandle {
- mhFilePath :: FilePath
- mhMaudeSig :: MaudeSig
- mhProc :: MVar MaudeProcess
- startMaude :: FilePath -> MaudeSig -> IO MaudeHandle
- getMaudeStats :: MaudeHandle -> IO String
- unifyViaMaude :: (IsConst c, Show (Lit c LVar), Ord c) => MaudeHandle -> (c -> LSort) -> [Equal (VTerm c LVar)] -> IO [SubstVFresh c LVar]
- matchViaMaude :: (IsConst c, Show (Lit c LVar), Ord c) => MaudeHandle -> (c -> LSort) -> Match (VTerm c LVar) -> IO [Subst c LVar]
- normViaMaude :: (IsConst c, Show (Lit c LVar), Ord c) => MaudeHandle -> (c -> LSort) -> VTerm c LVar -> IO (VTerm c LVar)
- type WithMaude = Reader MaudeHandle
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.
MaudeHandle | |
|
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
.