Ideas.Common.Rewriting.Substitution

Substitutions on terms. Substitutions are idempotent, and non-cyclic.

Documentation

data Substitution

Abstract data type for substitutions

Instances

Eq Substitution

Show Substitution

Arbitrary Substitution

Monoid Substitution

emptySubst :: Substitution

Returns the empty substitution

singletonSubst :: Int -> Term -> Substitution

Returns a singleton substitution

dom :: Substitution -> IntSet

Returns the domain of a substitution (as a set)

lookupVar :: Int -> Substitution -> Maybe Term

Lookups a variable in a substitution. Nothing indicates that the variable is not in the domain of the substitution

(@@) :: Substitution -> Substitution -> Substitution

Combines two substitutions. The left-hand side substitution is first applied to the co-domain of the right-hand side substitution

(|->) :: Substitution -> Term -> Term

Apply the substitution

listToSubst :: [(Int, Term)] -> Substitution

Turns a list into a substitution

composable :: Substitution -> Substitution -> Bool

(@+@) :: Substitution -> Substitution -> Maybe Substitution

tests :: TestSuite