Ideas.Common.Rewriting.Substitution

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

Documentation

data Substitution

Abstract data type for substitutions

Instances

Eq Substitution

Methods

(==) :: Substitution -> Substitution -> Bool

(/=) :: Substitution -> Substitution -> Bool

Show Substitution

Methods

showsPrec :: Int -> Substitution -> ShowS

show :: Substitution -> String

showList :: [Substitution] -> ShowS

Monoid Substitution

Methods

mempty :: Substitution

mappend :: Substitution -> Substitution -> Substitution

mconcat :: [Substitution] -> Substitution

Arbitrary Substitution

Methods

arbitrary :: Gen Substitution

shrink :: Substitution -> [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 infixr 6

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

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

Apply the substitution

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

Turns a list into a substitution

composable :: Substitution -> Substitution -> Bool

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

tests :: TestSuite