I am using pattern matching on argument passed to a function. The method works fine for "first level" matching so to say but any attempt to go deeper gives the error "stdIn:282.5-291.77 Error: match redundant"
example
fun nnf T = T
| nnf F = F
| nnf (LETTER(x)) = (LETTER(x))
| nnf (NEG(x)) = (NEG(nnf x))
| nnf (AND(x,y)) = (AND(nnf x, nnf y))
| nnf (OR(x,y)) = (OR(nnf x, nnf y))
| nnf (IMP(x,y)) = (OR(NEG(nnf x),(nnf y)))
| nnf (NEG(NEG(LETTER(x)))) = (LETTER(x))
| nnf (NEG(AND(LETTER(x),LETTER(y)))) = (OR(NEG(LETTER(x)),NEG(LETTER(y))))
| nnf (NEG(OR(LETTER(x),LETTER(y)))) = (AND(NEG(LETTER(x)),NEG(LETTER(y))));
val nnf = fn : prop -> prop
the error i get is
stdIn:282.5-291.77 Error: match redundant
T => ...
F => ...
LETTER x => ...
NEG x => ...
AND (x,y) => ...
OR (x,y) => ...
IMP (x,y) => ...
--> NEG (NEG (LETTER x)) => ...
--> NEG (AND (LETTER x,LETTER y)) => ...
--> NEG (OR (LETTER x,LETTER y)) => ...
so SML is saying that the last 3 clauses in the function definition are the same since they all begin with "(NEG(..." even though what follows is different.
how do i overcome this ?
The case NEG(x)
already covers any possible case involving outermost NEG
, so the others are never reached. Depending on what you actually want to achieve, either remove that case, or move it after the more specific ones (cases are tried in order).