{- |
Module      :  $EmptyHeader$
Description :  <optional short description entry>
Copyright   :  (c) <Authors or Affiliations>
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  <email>
Stability   :  unstable | experimental | provisional | stable | frozen
Portability :  portable | non-portable (<reason>)

<optional description>
-}


-- generic code (no need for duplication)
------------------------------------------

(-->) :: (Logic f) => f -> f -> f
x --> y = (neg x) \/ y

(<-->) :: (Logic f) => f -> f -> f
x <--> y = (x --> y) /\ (y --> x)

-- disjunction of negation of elements
ndisj :: (Logic f) => [f] -> f
ndisj xs = disj (map neg xs)

-- create singleton lists containing disjunctions
disjlst :: (Logic f) => [f] -> [f]
disjlst ls = [disj ls]

-- negate a list
neglst :: (Logic f) => [f] -> [f]
neglst xs = map neg xs

-- generic: purely generic

-- avoids []->[[]], otherwise F matches F
listify :: [a] -> [[a]]
listify [] = []; listify x = [x]

-- length ordering on lists
cmpsize :: [a] -> [a] -> Ordering
cmpsize s t = if(length(s) < length(t)) then LT else GT

-- zip two lists together using a binary operator
zipbin :: (a -> a -> a) -> [a] -> [a] -> [a]
zipbin _ [] _ = [];	zipbin _ _ [] = [];
zipbin f (x:xs) (y:ys) = (f x y):(zipbin f xs ys)

-- given indices and a list find image
img :: [Int] -> [a] -> [a]
img inds ls = map (ls!!) inds 

-- map a list to indices from 0 -> length -1
toinds :: [a] -> [Int]
toinds [] = []; toinds xs = [0..(length xs)-1]


-- construct all integer n-tuples with elements from 1,..,r
tuprange :: Int -> Int -> [[Int]]
tuprange _ 0 = [[]]
tuprange r n = 
	let rec xs ys = map (\z -> z:ys) xs
	in	concatMap (rec [1..r]) (tuprange r (n-1))

	
-- generic: set operations

pwdisj :: (Eq a) => [[a]] -> Bool
pwdisj [] = True
pwdisj (x:xs) = if (all (\y -> null(x `intersect` y)) xs) then (pwdisj xs) else False
	
pwrset :: [a] -> [[a]]
pwrset [] = [[]]; pwrset (x:xs) = (map ([x]++) (pwrset xs)) ++ (pwrset xs) 

-- remove subsets
rmsub :: (Eq a) => [[a]] -> [[a]]
rmsub [] = []
rmsub (x:xs) | (any (\y -> (x `intersect` y == x)) xs) = rmsub(xs) | otherwise = x:rmsub(xs) 


-- generic: strippers and box collecting

-- strip a list
striplst :: (Strip f g) => [f] -> [g]
striplst ls = concatMap strip ls

onlyboxes :: (Logic f) => [f] -> [f]
onlyboxes ls = concatMap onlybox ls

cml :: (a -> [a]) -> [a] -> [a]
cml f ls = concatMap f ls

-- generic unary and binary provable

provable1 :: UnaryMatch f g => f -> Bool
provable1 phi = all (\c -> any (all provable) (matchu c)) (cnf phi) 

provable2 :: BinaryMatch f g h => f -> Bool
provable2 phi =
	let	bothprvble (as,bs) = (all provable as) && (all provable bs)
	in	all (\c -> any (\pair -> bothprvble pair) (matchb c)) (cnf phi) 

-- generic: main prover

-- all possible clauses
clauses :: (Logic f) => [f] -> [Clause f]
clauses [] = [Clause ([],[])]
clauses (a:as) = 
	let	padd c (Clause (p, n)) = Clause (c:p, n)
		nadd c (Clause (p, n)) = Clause (p, c:n)
	in	(map (padd a) (clauses as)) ++ (map (nadd a) (clauses as))
	
-- dnf
allsat :: (Logic f) => f -> [Clause f]
allsat phi = filter (\x -> (eval phi x)) (clauses (ma phi))

-- cnf
cnf :: (Logic f) => f -> [Clause f]
cnf phi = map (\(Clause (x, y)) -> (Clause (y, x))) (allsat (neg phi))

-- sat
sat :: (Logic f) => f -> Bool
sat phi = not $ provable $ neg phi
