Documentation

Returns whether the given Defn is redundant with regards to repetitions on RHSs.

Here is an example of a redundant Defn:

0 ? 0  =  1
0 ? x  =  1
x ? 0  =  x
x ? y  =  x

It is redundant because it is equivalent to:

0 ? _  =  1
x ? _  =  x

This function safely handles holes on the RHSs by being conservative in cases these are found: nothing can be said before their fillings.

Returns whether the given Defn is redundant with regards to subsumption by latter patterns

Here is an example of a redundant Defn by this criterium:

foo 0  =  0
foo x  =  x

Returns whether the given Defn is redundant with regards to repetitions on RHSs.

Here is an example of a redundant Defn:

0 ? 0  =  1
0 ? x  =  1
x ? 0  =  x
x ? y  =  x

It is redundant because it is equivalent to:

0 ? _  =  1
x ? _  =  x

1 and x are repeated in the results for when the first arguments are 0 and x.

Returns whether the given Defn is redundant with regards to case elimination

The following is redundant according to this criterium:

foo []  =  []
foo (x:xs)  =  x:xs

It is equivalent to:

foo xs = xs

The following is also redundant:

[] ?? xs  =  []
(x:xs) ?? ys  =  x:xs

as it is equivalent to:

xs ?? ys == xs

This function is not used as one of the criteria in isRedundantDefn because it does not pay-off in terms of runtime vs number of pruned candidates.

Returns whether the given Defn is redundant modulo subsumption and rewriting.

(cf. subsumedWith)

Returns whether the given Defn is redundant with regards to recursions

The following is redundant:

xs ?? []  =  []
xs ?? (x:ys)  =  xs ?? []

The LHS of a base-case pattern, matches the RHS of a recursive pattern. The second RHS may be replaced by simply [] which makes it redundant.

Returns whether a binding is subsumed by another modulo rewriting

> let normalize = (// [(zero -+- zero, zero)])
> subsumedWith normalize (ff zero, zero) (ff xx, xx -+- xx)
True

> subsumedWith normalize (ff zero, zero) (ff xx, xx -+- one)
False

> subsumedWith normalize (zero -?- xx, zero) (xx -?- yy, xx -+- xx)
True

(cf. isRedundantModuloRewriting)

Simplifies a definition by removing redundant patterns

This may be useful in the following case:

0 ^^^ 0  =  0
0 ^^^ x  =  x
x ^^^ 0  =  x
_ ^^^ _  =  0

The first pattern is subsumed by the last pattern.

Introduces a hole at a given position in the binding:

> introduceVariableAt 1 (xxs -?- (yy -:- yys), (yy -:- yys) -++- (yy -:- yys))
(xs ? (y:ys) :: [Int],(y:ys) ++ (y:ys) :: [Int])

> introduceVariableAt 2 (xxs -?- (yy -:- yys), (yy -:- yys) -++- (yy -:- yys))
(xs ? x :: [Int],x ++ x :: [Int])

Relevant occurrences are replaced.