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.

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.

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

replace a subterm at a given position.

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 a term is an instance of another.

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

Check whether a term is a variant of another.