Conjure.Defn.Redundancy

This module is part of Conjure.

This module exports functions that check redundancy in Defns.

You are probably better off importing Conjure.

Documentation

isRedundantDefn :: Defn -> Bool

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.

isRedundantBySubsumption :: Defn -> Bool

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

isRedundantByRepetition :: Defn -> Bool

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.

isRedundantByIntroduction :: Defn -> Bool

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.

isRedundantModuloRewriting :: (Expr -> Expr) -> Defn -> Bool

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

(cf. subsumedWith)

hasRedundantRecursion :: Defn -> Bool

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.

subsumedWith :: (Expr -> Expr) -> Bndn -> Bndn -> Bool

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)

simplifyDefn :: Defn -> Defn

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.

introduceVariableAt :: Int -> Bndn -> Bndn

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.