Data.Rewriting.Term.Ops

Operations on Terms

funs :: Term f v -> [f]

Return the list of all function symbols in the term, from left to right.

>>> funs (Fun 'f' [Var 3, Fun 'g' [Fun 'f' []]])
"fgf"

funsDL :: Term f v -> [f] -> [f]

Difference List version of funs. We have funsDL t vs = funs t ++ vs.

vars :: Term f v -> [v]

Return the list of all variables in the term, from left to right.

>>> vars (Fun 'g' [Var 3, Fun 'f' [Var 1, Var 2, Var 3]])
[3,1,2,3]

varsDL :: Term f v -> [v] -> [v]

Difference List version of vars. We have varsDL t vs = vars t ++ vs.

root :: Term f v -> Either v f

Return the root symbol of the given term.

>>> root (Fun 'f' [Var 1, Fun 'g' []])
Right 'f'

>>> root (Var 1)
Left 1

withArity :: Term f v -> Term (f, Int) v

Annotate each occurrence of a function symbol with its actual arity, i.e., its number of arguments.

>>> withArity (Fun 'f' [Var 1, Fun 'f' []])
Fun ('f',2) [Var 1,Fun ('f',0) []]

subtermAt :: Term f v -> Pos -> Maybe (Term f v)

Return the subterm at a given position.

properSubterms :: Term f v -> [Term f v]

Return the list of all proper subterms.

>>> properSubterms (Fun 'g' [Fun 'f' [Var 1], Fun 'f' [Var 1]])
[Fun 'f' [Var 1],Var 1,Fun 'f' [Var 1],Var 1]

subterms :: Term f v -> [Term f v]

Return the list of all subterms.

subterms t = t : properSubterms t

replaceAt :: Term f v -> Pos -> Term f v -> Maybe (Term f v)

replace a subterm at a given position.

rename :: (v -> v') -> Term f v -> Term f v'

Rename the variables in a term.

>>> rename (+ 1) (Fun 'f' [Var 1, Fun 'g' [Var 2]])
(Fun 'f' [Var 2, Fun 'g' [Var 3]])

Predicates on Terms

isVar :: Term f v -> Bool

Return True if the term is a variable, False otherwise.

isFun :: Term f v -> Bool

Return True if the term is a function application, False otherwise.

isGround :: Term f v -> Bool

Check whether the term is a ground term, i.e., contains no variables.

isLinear :: Ord v => Term f v -> Bool

Check whether the term is linear, i.e., contains each variable at most once.

isInstanceOf :: (Eq f, Ord v, Ord v') => Term f v -> Term f v' -> Bool

Check whether the first term is an instance of the second term.

isVariantOf :: (Eq f, Ord v, Ord v') => Term f v -> Term f v' -> Bool

Check whether two terms are variants of each other.