Module Subst

ppSubst :: Subst -> Doc   

Pretty printing of a substitution

emptySubst :: Subst   

empty substitution

Further infos:

• solution complete, i.e., able to compute all solutions

singleSubst :: Int -> Expr -> Subst   

substitute a variable by an expression

Further infos:

• solution complete, i.e., able to compute all solutions

mkSubst :: [Int] -> [Expr] -> Subst   

create a substitution from a list of variables and a list of expressions

toSubst :: [(Int,Expr)] -> Subst   

create a substitution from a list of variable/expression pairs.

Further infos:

• solution complete, i.e., able to compute all solutions

dom :: Subst -> [Int]   

extract domain of a given substitution

rng :: Subst -> [Expr]   

extract range of a given substitution

restrict :: [Int] -> Subst -> Subst   

Restrict a substititution to a given domain.

without :: [Int] -> Subst -> Subst   

Remove a given part of the domain from a substititution.

compose :: Subst -> Subst -> Subst   

compose s1 s2 composes the substitutions s1 and s2. The result is s1 . s2, i.e., it has the same effect as s1(s2(t)) when applied to a term t.

combine :: Subst -> Subst -> Maybe Subst   

Try to combine two substitutions $\sigma$ and $\theta$. This operation returns Nothing if there exists a conflicting substitution, i.e., there exists a variable $x \in \dom(\sigma)$, $x \in \dom(\theta)$ such that $\sigma(x) \neq $\theta(x)$.

lookupSubst :: Int -> Subst -> Expr   

Lookup a substititution for a variable. If there is no substitution given, the variable is substituted by itself.

findSubstWithDefault :: Expr -> Int -> Subst -> Expr   

Find a substititution for a variable with a given default value.

fmapSubst :: (Expr -> Expr) -> Subst -> Subst   

fmap f sigma applies f on all expressions in the range of sigma. That is, if $\sigma = { v1 \mapsto e1 \dots vn \mapsto en }$, then fmap f sigma equals { v1 \mapsto f(e1) \dots vn \mapsto f(en) }$

substSingle :: Int -> Expr -> Expr -> Expr   

substSingle v s e substitutes v by s in e

varSubst :: [Int] -> [Int] -> Expr -> Expr   

Replace a list of variables by another list of variables in the given expression.

isVariableRenaming :: Subst -> Bool   

Is the substititution sigma a variable renaming, i.e., are the expressions in rng(sigma) all variables?

isDetSubst :: Expr -> Subst -> Bool   

Is the substititution sigma a deterministic substitution w.r.t e, i.e., are the expressions in rng(sigma) all either constructor terms or does the variable occur at most once in e?

subst :: Subst -> Expr -> Expr   

subst sigma e = sigma(e) substitutes all occurrences of variables by corresponding expressions. substitute all occurrences of $vi$ by $ei$ in $e$ if $s = { v1 \mapsto e1 \dots vn \mapsto en }$

Note: The substititution must not replace variables introduced in the expression itself, either as a free variable, a let binding or a pattern variable. This is guaranteed and checked as an assertion. If the assertion is violated, an error is thrown.