Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|
Safe Haskell | None |
AC unification based on maude and free unification.
- unifyLTerm :: (IsConst c, Show (Lit c LVar), Ord c) => (c -> LSort) -> [Equal (LTerm c)] -> WithMaude [SubstVFresh c LVar]
- unifyLNTerm :: [Equal LNTerm] -> WithMaude [SubstVFresh Name LVar]
- unifiableLNTerms :: LNTerm -> LNTerm -> WithMaude Bool
- unifyLTermFactored :: (IsConst c, Show (Lit c LVar), Ord c) => (c -> LSort) -> [Equal (LTerm c)] -> WithMaude (LSubst c, [SubstVFresh c LVar])
- unifyLNTermFactored :: [Equal LNTerm] -> WithMaude (LNSubst, [SubstVFresh Name LVar])
- matchLVar :: LVar -> LVar -> Match (LTerm c)
- solveMatchLTerm :: (IsConst c, Show (Lit c LVar), Ord c) => (c -> LSort) -> Match (LTerm c) -> WithMaude [Subst c LVar]
- solveMatchLNTerm :: Match LNTerm -> WithMaude [Subst Name LVar]
- data MaudeHandle
- type WithMaude = Reader MaudeHandle
- startMaude :: FilePath -> MaudeSig -> IO MaudeHandle
- getMaudeStats :: MaudeHandle -> IO String
- mhMaudeSig :: MaudeHandle -> MaudeSig
- mhFilePath :: MaudeHandle -> FilePath
- data MaudeSig
- enableDH :: MaudeSig -> Bool
- enableBP :: MaudeSig -> Bool
- enableMSet :: MaudeSig -> Bool
- minimalMaudeSig :: MaudeSig
- dhMaudeSig :: MaudeSig
- bpMaudeSig :: MaudeSig
- msetMaudeSig :: MaudeSig
- pairMaudeSig :: MaudeSig
- symEncMaudeSig :: MaudeSig
- asymEncMaudeSig :: MaudeSig
- signatureMaudeSig :: MaudeSig
- hashMaudeSig :: MaudeSig
- rrulesForMaudeSig :: MaudeSig -> Set (RRule LNTerm)
- stFunSyms :: MaudeSig -> Set NoEqSym
- funSyms :: MaudeSig -> FunSig
- stRules :: MaudeSig -> Set StRule
- irreducibleFunSyms :: MaudeSig -> FunSig
- noEqFunSyms :: MaudeSig -> NoEqFunSig
- addFunSym :: NoEqSym -> MaudeSig -> MaudeSig
- addStRule :: StRule -> MaudeSig -> MaudeSig
- module Term.Substitution
- module Term.Rewriting.Definitions
Unification modulo AC
unifyLTerm :: (IsConst c, Show (Lit c LVar), Ord c) => (c -> LSort) -> [Equal (LTerm c)] -> WithMaude [SubstVFresh c LVar]Source
unifyLNTerm eqs
returns a complete set of unifiers for eqs
modulo AC.
unifyLNTerm :: [Equal LNTerm] -> WithMaude [SubstVFresh Name LVar]Source
unifyLNTerm eqs
returns a complete set of unifiers for eqs
modulo AC.
unifyLTermFactored :: (IsConst c, Show (Lit c LVar), Ord c) => (c -> LSort) -> [Equal (LTerm c)] -> WithMaude (LSubst c, [SubstVFresh c LVar])Source
unifyLTerm sortOf eqs
returns a complete set of unifiers for eqs
modulo AC.
unifyLNTermFactored :: [Equal LNTerm] -> WithMaude (LNSubst, [SubstVFresh Name LVar])Source
unifyLTerm sortOf eqs
returns a complete set of unifiers for eqs
modulo AC.
matching modulo AC
Constructing matching problems
Solving matching problems
solveMatchLTerm :: (IsConst c, Show (Lit c LVar), Ord c) => (c -> LSort) -> Match (LTerm c) -> WithMaude [Subst c LVar]Source
solveMatchLNTerm sortOf eqs
returns a complete set of matchers for
eqs
modulo AC.
solveMatchLNTerm :: Match LNTerm -> WithMaude [Subst Name LVar]Source
solveMatchLNTerm eqs
returns a complete set of matchers for eqs
modulo AC.
Handles 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.
type WithMaude = Reader MaudeHandleSource
Values that depend on a 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.
Maude signatures
The required information to define a Maude functional module
.
enableMSet :: MaudeSig -> BoolSource
minimalMaudeSig :: MaudeSigSource
The minimal maude signature.
Maude signatures for the AC symbols.
Maude signatures for the AC symbols.
msetMaudeSig :: MaudeSigSource
Maude signatures for the AC symbols.
pairMaudeSig :: MaudeSigSource
Maude signatures for the default subterm symbols.
symEncMaudeSig :: MaudeSigSource
Maude signatures for the default subterm symbols.
asymEncMaudeSig :: MaudeSigSource
Maude signatures for the default subterm symbols.
signatureMaudeSig :: MaudeSigSource
Maude signatures for the default subterm symbols.
hashMaudeSig :: MaudeSigSource
Maude signatures for the default subterm symbols.
rrulesForMaudeSig :: MaudeSig -> Set (RRule LNTerm)Source
Returns all rewriting rules including the rules for DH, BP, and multiset.
funSyms :: MaudeSig -> FunSigSource
function signature including the function symbols for DH, BP, and Multiset can be computed from enableX and stFunSyms
irreducibleFunSyms :: MaudeSig -> FunSigSource
irreducible function symbols (can be computed)
noEqFunSyms :: MaudeSig -> NoEqFunSigSource
Non-AC function symbols.
Convenience exports
module Term.Substitution
module Term.Rewriting.Definitions