-- v1: name types: Tableau and Branch
-- v2: change names of functions etc.
--      - ensures that the names are appropriate, as well as
--      - fitting in with newly named types
-- v3: change to non-literate form
-- v4: some algorithmic changes: introducing HOFs etc. this is v4-1,
--     had to backtrack to accommodate mistake in introducing list
--     comprehesions.
-- v5: changes in the definintions of nub-like functiond
--	- remove 'test' functions that retrun non-Bool values
--	  and then test them for equality. This requires changes of
--	  type.

import List

-- Defining the Data type Prop and creating the show function for it

-- This is the structure of the data type of our proposition.  It determines the ways that 
-- a Prop can be consructed, beging TRUE/FALSE (these arn't actually implomented, but can be
-- implomented if required), or a variable (eg A,B,C etc..), or type of compound formula (ie
-- AND, OR, NOT, IMPLIES and IFF).  This data type also needs to have equality tested on it

type Variable = Char
data Prop = TRUE | FALSE |
            VAR Variable |
            NOT Prop |
            AND Prop Prop |
            OR Prop Prop |
            IMPLIES Prop Prop |
            IFF Prop Prop
            deriving (Eq)

-- This is the Show function that outputs the propositions as readable sentences.  Whenever a
-- Prop is outputed, it shows it in the style created in the Show.

instance Show Prop where
    show TRUE = "TRUE"
    show FALSE = "FALSE"
    show (VAR c) = [c]
    show (NOT p) = "(¬" ++ show p ++ ")"
    show (AND p q) = "(" ++ show p ++ "&" ++ show q ++ ")"
    show (OR p q) = "(" ++ show p ++ "|" ++ show q ++ ")"
    show (IMPLIES p q) = "(" ++ show p ++ "=>" ++ show q ++ ")"
    show (IFF p q) = "(" ++ show p ++ "<=>" ++ show q ++ ")"

-- Addition in v1:

type Branch  = [Prop]
type Tableau = [Branch]

-- The next 3 functions are the ones that control the output to the screen of the tableau.

-- This function is the main function you use when you want to find the result.  The syntax 
-- is "Main> tableauMain [prop]" (ie "tableauMain box" will give you the tableaux result for 
-- the box problem).

tableauMain :: Tableau -> IO ()
tableauMain x = putStr (displayAllBranches (buildTableau x))

-- This function displays one branch of the tableau results, it puts every variable on a
-- new line to make it easy to look at and understand.

displayBranch :: Branch -> String
displayBranch = concat . map (++"\n") . map show

-- This function displays all the branches of the tableau, by calling the above function.
-- It then seperates each branch with a space, to make the final output clear.

displayAllBranches :: Tableau -> String
displayAllBranches = concat . intersperse "\n" . map displayBranch

-- This function is the main function that brings all the seperate parts of calculating a
-- tableaux together.

buildTableau :: Tableau -> Tableau
buildTableau = removeDuplicateBranches . removeDuplicatesInBranches . removeConts . reduceRoot

-- This function finds any identical branches and removes the duplicates.  This is just here
-- to make the output simplier, because somtimes different branches give the same results as
-- others, and this just makes the output look more complex.

removeDuplicateBranches :: Tableau -> Tableau
removeDuplicateBranches = nubVar

-- New function introduced: generalises both removeDuplicateBranches
-- and removeDuplicateProps below. This is not the same as the built-in
-- nub: this function chooses the last occurrence of an element, nub
-- chooses the first, so
--
--	Main> nubVar [1,2,2,1]
--	[2,1]
--	Main> nub [1,2,2,1]
--	[1,2]

nubVar :: Eq a => [a] -> [a]
nubVar [] = []
nubVar (x:xs)
    | elem x xs  =     nubVar xs
    | otherwise  = x : nubVar xs

-- This function any identical variables and removes the duplicates.  This is just here to
-- make the output simplier, by removing any unnessary duplicates of variables.

removeDuplicatesInBranches :: Tableau -> Tableau
removeDuplicatesInBranches = map removeDuplicateProps

-- This function is part of the above function, this one works on single lists of Props, 
-- where as the above one works of lists of lists of Props.

removeDuplicateProps :: Branch -> Branch
removeDuplicateProps = nubVar

-- Refactored to here.


-- Functions to split the Props

-- combine takes a list of Props and a list of Prop lists and adds all the values in the
-- single list of Props to all the lists in the list of Prop lists

combine :: Branch -> Tableau -> Tableau
combine ps pls = [ps ++ pl | pl<-pls ]

-- For each of the semantic tableau rules there have been three functions created,
-- a split, a remove and a solve function

-- The split functions take a list of Props and splits the first occurence of the
-- relative rule into its simpler form by combing the result of the remove function
-- and the result of the solve function

-- The remove function scans the list of Props and removes the first occurence of
-- the relative rule from the list and returns the list

-- The solve function finds the first occurence of the relative rule in the list, solves it
-- according to the relative rule and returns only the simpler form

-- As there are different rules for Not Not, And, Or, Implies, Iff, Not And, Not Or, Not Implies
-- and Not Iff there are three functions for each

splitNotNot :: Branch -> Tableau
splitNotNot ps = combine (removeNotNot ps) (solveNotNot ps)

removeNotNot :: Branch -> Branch
removeNotNot [] = []
removeNotNot ((NOT (NOT _)):ps) = ps
removeNotNot (p:ps) = p : removeNotNot ps

solveNotNot :: Branch -> Tableau
solveNotNot [] = [[]]
solveNotNot ((NOT (NOT p)):_) = [[p]]
solveNotNot (_:ps) = solveNotNot ps

splitAnd :: Branch -> Tableau
splitAnd ps = combine (removeAnd ps) (solveAnd ps)

removeAnd :: Branch -> Branch
removeAnd [] = []
removeAnd ((AND p q):ps) = ps
removeAnd (p:ps) = p : removeAnd ps

solveAnd :: Branch -> Tableau
solveAnd [] = [[]]
solveAnd ((AND p q):_) = [[p,q]]
solveAnd (_:ps) = solveAnd ps

splitOr :: Branch -> Tableau
splitOr ps = combine (removeOr ps) (solveOr ps)

removeOr :: Branch -> Branch
removeOr [] = []
removeOr ((OR p q):ps) = ps
removeOr (p:ps) = p : removeOr ps

solveOr :: Branch -> Tableau
solveOr [] = [[]]
solveOr ((OR p q):_) = [[p],[q]]
solveOr (_:ps) = solveOr ps

splitImplies :: Branch -> Tableau
splitImplies ps = combine (removeImplies ps) (solveImplies ps)

removeImplies :: Branch -> Branch
removeImplies [] = []
removeImplies ((IMPLIES p q):ps) = ps
removeImplies (p:ps) = p : removeImplies ps

solveImplies :: Branch -> Tableau
solveImplies [] = [[]]
solveImplies ((IMPLIES p q):_) = [[NOT p],[q]]
solveImplies (_:ps) = solveImplies ps

splitIff :: Branch -> Tableau
splitIff ps = combine (removeIff ps) (solveIff ps)

removeIff :: Branch -> Branch
removeIff [] = []
removeIff ((IFF p q):ps) = ps
removeIff (p:ps) = p : removeIff ps

solveIff :: Branch -> Tableau
solveIff [] = [[]]
solveIff ((IFF p q):_) = [[p,q],[NOT p,NOT q]]
solveIff (_:ps) = solveIff ps

splitNotAnd :: Branch -> Tableau
splitNotAnd ps = combine (removeNotAnd ps) (solveNotAnd ps)

removeNotAnd :: Branch -> Branch
removeNotAnd [] = []
removeNotAnd ((NOT (AND p q)):ps) = ps
removeNotAnd (p:ps) = p : removeNotAnd ps

solveNotAnd :: Branch -> Tableau
solveNotAnd [] = [[]]
solveNotAnd ((NOT (AND p q)):_) = [[NOT p],[NOT q]]
solveNotAnd (_:ps) = solveNotAnd ps

splitNotOr :: Branch -> Tableau
splitNotOr ps = combine (removeNotOr ps) (solveNotOr ps)

removeNotOr :: Branch -> Branch
removeNotOr [] = []
removeNotOr ((NOT (OR p q)):ps) = ps
removeNotOr (p:ps) = p : removeNotOr ps

solveNotOr :: Branch -> Tableau
solveNotOr [] = [[]]
solveNotOr ((NOT (OR p q)):_) = [[NOT p,NOT q]]
solveNotOr (_:ps) = solveNotOr ps

splitNotImplies :: Branch -> Tableau
splitNotImplies ps = combine (removeNotImplies ps) (solveNotImplies ps)

removeNotImplies :: Branch -> Branch
removeNotImplies [] = []
removeNotImplies ((NOT (IMPLIES p q)):ps) = ps
removeNotImplies (p:ps) = p : removeNotImplies ps

solveNotImplies :: Branch -> Tableau
solveNotImplies [] = [[]]
solveNotImplies ((NOT (IMPLIES p q)):_) = [[p,NOT q]]
solveNotImplies (_:ps) = solveNotImplies ps

splitNotIff :: Branch -> Tableau
splitNotIff ps = combine (removeNotIff ps) (solveNotIff ps)

removeNotIff :: Branch -> Branch
removeNotIff [] = []
removeNotIff ((NOT (IFF p q)):ps) = ps
removeNotIff (p:ps) = p : removeNotIff ps

solveNotIff :: Branch -> Tableau
solveNotIff [] = [[]]
solveNotIff ((NOT (IFF p q)):_) = [[p,NOT q],[NOT p,q]]
solveNotIff (_:ps) = solveNotIff ps

-- The overall split function selects which split function to call dependent on the
-- integer passed to it

split :: Int -> Branch -> Tableau
split 1 pl = splitNotNot pl
split 2 pl = splitAnd pl
split 3 pl = splitNotOr pl
split 4 pl = splitNotImplies pl
split 5 pl = splitOr pl
split 6 pl = splitImplies pl
split 7 pl = splitNotAnd pl
split 8 pl = splitIff pl
split 9 pl = splitNotIff pl
split x pl = [pl]

-- reduced takes a list of Props and checks it for all the rules to see if it is
-- reduced to it's simplest form. If it is the function returns True, if not then
-- the function returns False

reduced :: Branch -> Bool
reduced [] = True
reduced ((NOT (NOT p)):_) = False
reduced ((AND p q):_) = False
reduced ((OR p q):_) = False
reduced ((IMPLIES p q):_) = False
reduced ((IFF p q):_) = False
reduced ((NOT (AND p q)):_) = False
reduced ((NOT (OR p q)):_) = False
reduced ((NOT (IMPLIES p q)):_) = False
reduced ((NOT (IFF p q)):_) = False
reduced (_:pl) = reduced pl

-- reduceable scans a list of Props for the existance of a specific rule indicated by the
-- integer value passed to it. If the rule exists the function returns an integer representing
-- the rule, if the rule doesn't exist then the value 10 is returned

reduceable :: Int -> Branch -> Int
reduceable x [] = 10
reduceable 1 ((NOT (NOT p)):_) = 1
reduceable 2 ((AND p q):_) = 2
reduceable 3 ((NOT (OR p q)):_) = 3
reduceable 4 ((NOT (IMPLIES p q)):_) = 4
reduceable 5 ((OR p q):_) = 5
reduceable 6 ((IMPLIES p q):_) = 6
reduceable 7 ((NOT (AND p q)):_) = 7
reduceable 8 ((IFF p q):_) = 8
reduceable 9 ((NOT (IFF p q)):_) = 9
reduceable x (p:pl) = reduceable x pl

-- reduceAll calls reduceable once for every rule, and returns the lowest integer returned
-- which represents the prefered rule to reduce next

reduceAll :: Int -> Branch -> Int
reduceAll 10 _ = 10
reduceAll x pl = min (reduceable x pl) (reduceAll (x+1) pl)

-- reduceRoot takes each Prop list in a list of Prop lists and checks to see if it is reduced,
-- if the Prop list is reduced the the list is returned with the result of reduceRoot on the rest
-- of the list. If the Prop list is not reduced though the list is reduced and checked for
-- contradictions, which are removed, and then passed into reduceRoot again. This has the affect
-- of recursively looping until the first Prop and any branches that may be produced from spliting
-- are delt with. Then the function returns the simplest form and processes the rest of the list
-- with reduceRoot

reduceRoot :: Tableau -> Tableau
reduceRoot [] = [[]]
reduceRoot [[]] = [[]]
reduceRoot (pl:pls) = (if (reduced pl) then [pl] else (reduceRoot (removeConts (reduce pl)))) ++ (reduceRoot pls)

-- reduce checks to see which rule needs to be split next and then calls the split function with
-- this information

reduce :: Branch -> Tableau
reduce pl = split (reduceAll 1 pl) pl

-- Remove contradictions

-- Function to remove a list if it contains a contradiction.

removeConts :: Tableau -> Tableau
removeConts x = looseEmptyLists (removeConts1 x)

-- Recurse through the list of lists, picking out 1 prop list at
-- a time and pass it to 'foo'

removeConts1 :: Tableau -> Tableau
removeConts1 [] = []
removeConts1 (x:xs) = (foo x):(removeConts1 xs)

-- Check the list of Props with 'bar'. If the list contains
-- a contradiction, the value returned by 'bar' will be False
-- so loose that list (return []).

foo :: Branch -> Branch
foo x
    | bar x = x
    | otherwise = []

-- 'bar' and comp recurse through the list comparing each prop
-- with every other one using 'contra'

bar :: Branch -> Bool
bar [] = True
bar (p:pl) = (comp p pl) && (bar pl)

comp :: Prop -> Branch -> Bool
comp p pl  = and [contra p pl2 | pl2 <- pl]

-- Return False if the 2 arguments are contradictions of eachother.

contra :: Prop -> Prop -> Bool
contra a b = not (((NOT a) == b) || (a == (NOT b)))

-- Tidy the resulting list of lists by removing all the empty lists.

looseEmptyLists :: Tableau -> Tableau
looseEmptyLists [] = []
looseEmptyLists [[]] = []
looseEmptyLists ([]:xs) = looseEmptyLists xs
looseEmptyLists (x:[]) = [x]
looseEmptyLists (x:xs) = [x] ++ (looseEmptyLists xs)

-- Some example Props

plist1, plist2, plist3, plist4 :: Tableau
plist1 = [[VAR 'a', (NOT (NOT (VAR 'c'))), VAR 'b']]
plist2 = [[VAR 'a', (AND (VAR 'b') (VAR 'c')), (OR (VAR 'b') (VAR 'c'))]]
plist3 = [[(IMPLIES (VAR 'a') (VAR 'b')), (IFF (VAR 'c') (VAR 'a')), (NOT (AND (VAR 'a') (VAR 'b')))]]
plist4 = [[(NOT (OR (VAR 'a') (VAR 'b'))), (NOT (IMPLIES (VAR 'c') (VAR 'd'))), (NOT (IFF (VAR 'a') (VAR 'b')))]]

-- The questions converted into Prop form

q1, q2, q3, q4 :: Tableau
q1 = [[(IFF (NOT (OR (VAR 'a') (VAR 'b'))) (NOT (AND (NOT (VAR 'a')) (NOT (VAR 'b')))))]]
q2 = [[(NOT (IFF (OR (VAR 'a') (VAR 'b')) (NOT (AND (NOT (VAR 'a')) (NOT (VAR 'b'))))))]]
q3 = [[(NOT (IMPLIES (IMPLIES (IMPLIES (VAR 'c') (VAR 'b')) (VAR 'c')) (VAR 'c')))]]
q4 = [[(IMPLIES (IMPLIES (VAR 'a') (VAR 'b')) (IMPLIES (VAR 'b') (VAR 'a')))]]

b1, b2, b3, b4, b5, b6, b7, b8, b9 :: Prop
b1 = (IFF (VAR 'f') (NOT (VAR 'c')))
b2 = (IFF (VAR 'g') (NOT (VAR 'c')))
b3 = (IFF (VAR 'h') (VAR 'd'))
b4 = (OR (OR (VAR 'b') (VAR 'c')) (VAR 'd'))
b5 = (NOT (AND (VAR 'b') (VAR 'c')))
b6 = (NOT (AND (VAR 'c') (VAR 'd')))
b7 = (NOT (AND (VAR 'd') (VAR 'b')))
b8 = (OR (OR (VAR 'f') (VAR 'g')) (VAR 'h'))
b9 = (OR (OR (NOT (VAR 'f')) (NOT (VAR 'g'))) (NOT (VAR 'h')))

-- box and box1 are virtualy identical, except that they AND the values in a slightly 
-- different way.  (box1 was only created to work out if another function was working
-- correctly or not).

box, box1 :: Tableau
box = [[(AND (AND (AND (b1) (b2)) (AND (b3) (b4))) (AND (AND (b5) (b6)) (AND (b7) (AND (b8) (b9)))))]]
box1 = [[(AND (AND (AND (AND (b1) (b2)) (AND (b3) (b4))) (AND (AND (b5) (b6)) (AND (b7) (b8)))) (b9))]]

-- The box example as a test.

test = tableauMain box