Term.Maude.Types

Types for communicating with Maude.

Maude terms

data MaudeLit

Constructors

MaudeVar Integer LSort

FreshVar Integer LSort

MaudeConst Integer LSort

Instances

Eq MaudeLit

Ord MaudeLit

Show MaudeLit

type MSubst = [((LSort, Integer), MTerm)]

type MTerm = Term MaudeLit

conversion from/to maude terms

lTermToMTerm

Arguments

:: (MonadBind (Lit c LVar) MaudeLit m, MonadFresh m, Show c, 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.

lTermToMTerm'

Arguments

:: (MonadBind (Lit Name LVar) MaudeLit m, MonadFresh m)

=> LNTerm

The term to translate.

-> m MTerm

Convert an LNTerm to an MTerm.

mTermToLNTerm

Arguments

:: (MonadBind MaudeLit (Lit c LVar) m, MonadFresh m, Show (Lit c LVar), Ord c, Show c)

=> String

Name hint for freshly generated variables.

-> MTerm

The maude term to convert.

-> m (VTerm c LVar)

Convert an MTerm to an LNTerm under the assumption that the bindings for the constants are already available.

runConversion

Arguments

:: 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.

msubstToLSubstVFresh

Arguments

:: (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 LVar

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.