[Haskell-cafe] Haskell Help

[PatrickM]

I'm writting a function that will remove tautologies from a fomula.The basic
idea is that if in a clause, a literal and its negation are found, it means
that the clause will be true, regardless of the value finally assigned to
that propositional variable.My appoach is to create a function that will
remove this but for a clause and map it to the fomula.Of course I have to
remove duplicates at the beginning.

    module Algorithm where

    import System.Random
    import Data.Maybe
    import Data.List

    type Atom = String
    type Literal = (Bool,Atom)
    type Clause = [Literal]
    type Formula = [Clause]
    type Model = [(Atom, Bool)]
    type Node = (Formula, ([Atom], Model))
    removeTautologies :: Formula -> Formula
    removeTautologies = map tC.map head.group.sort
      where rt ((vx, x) : (vy, y) : clauses) | x == y = rt rest
                                          | otherwise = (vx, x) : rt ((vy,
y) : clauses)
Now I have problems  when I try to give it a formula (for example (A v B v
-A) ^ (B v C v A)).Considering that example the first clause contains the
literals A and -A. This means that the clause will always be true, in which
case it can be simplify the whole set to simply (B v C v A) . But I get the
following

    Loading package old-locale-1.0.0.2 ... linking ... done.
    Loading package time-1.1.4 ... linking ... done.
    Loading package random-1.0.0.2 ... linking ... done.
    [[(True,"A"),(True,"B")*** Exception: Assignment.hs:(165,11)-(166,83):
Non-exhaustive patterns in function rt

What should I do?
-- 
View this message in context: http://haskell.1045720.n5.nabble.com/Haskell-Help-tp3381647p3381647.html
Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.