Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|
Safe Haskell | None |
Types for communicating with Maude.
- data MaudeLit
- type MSubst = [((LSort, Integer), MTerm)]
- type MTerm = Term MaudeLit
- lTermToMTerm :: (MonadBind (Lit c LVar) MaudeLit m, MonadFresh m, Show (Lit c LVar), Ord c) => (c -> LSort) -> VTerm c LVar -> m MTerm
- lTermToMTerm' :: (MonadBind (Lit Name LVar) MaudeLit m, MonadFresh m) => LNTerm -> m MTerm
- mTermToLNTerm :: (MonadBind MaudeLit (Lit c LVar) m, MonadFresh m, Show (Lit c LVar), Ord c, Show c) => String -> MTerm -> m (VTerm c LVar)
- runConversion :: Ord c => BindT (Lit c LVar) MaudeLit Fresh a -> (a, Map MaudeLit (Lit c LVar))
- msubstToLSubstVFresh :: (Ord c, Show (Lit c LVar), Show c) => Map MaudeLit (Lit c LVar) -> MSubst -> SubstVFresh c LVar
- msubstToLSubstVFree :: (Ord c, Show (Lit c LVar), Show c) => Map MaudeLit (Lit c LVar) -> MSubst -> Subst c LVar
Maude terms
conversion from/to maude terms
:: (MonadBind (Lit c LVar) MaudeLit m, MonadFresh m, Show (Lit c LVar), Ord c) | |
=> (c -> LSort) | A function that returns the sort of a constant. |
-> VTerm c LVar | The term to translate. |
-> m MTerm |
Convert an LNTerm
with arbitrary names to an MTerm
.
Convert an LNTerm
to an MTerm
.
:: Ord c | |
=> BindT (Lit c LVar) MaudeLit Fresh a | Computation to execute. |
-> (a, Map MaudeLit (Lit c LVar)) |
Run a BindT (Lit c LVar) MaudeLit Fresh
computation
with an empty fresh supply and an empty binding map and return
the result and the resulting inverted binding map.
:: (Ord c, Show (Lit c LVar), Show c) | |
=> Map MaudeLit (Lit c LVar) | The binding map to use for constants. |
-> MSubst | The maude substitution. |
-> SubstVFresh c LVar |
msubstToLSubstVFresh bindings substMaude
converts a substitution
returned by Maude to a VFresh
substitution. It expects that the
range of the maude substitution contains only fresh variables in its
range and raises an error otherwise.
msubstToLSubstVFree :: (Ord c, Show (Lit c LVar), Show c) => Map MaudeLit (Lit c LVar) -> MSubst -> Subst c LVarSource
msubstToLSubstVFree bindings substMaude
converts a substitution
returned by Maude to a VFree
substitution. It expects that the
maude substitution contains no fresh variables in its range and raises an
error otherwise.