module BoolExprStep1
where

import Prelude hiding (and, or)
import qualified Prelude as P (and, or)

import Data.Maybe
    ( fromMaybe )

import Data.List
    ( nub
    , sort
    )

import DataTypes

-- ------------------------------

foldRT	:: (a -> [b] -> b) -> RoseTree a -> b
foldRT f (RT op al)
    = f op (map (foldRT f) al)

-- ------------------------------

eval	:: Env -> BoolExpr -> Bool
eval env
    = foldRT apply
    where
    apply F     []	= False
    apply T     []	= True
    apply (V n) []	= fromMaybe (error $ "Variable not defined: " ++ show n)
			  . lookup n
				$ env
    apply AND   al	= P.and al
    apply OR    al	= P.or  al
    apply NOT  [a1]	= not a1
    apply IMPL [a1, a2] = a1 <= a2
    apply EQUIV al	= -- even (length al - length (filter id al))
                          foldl (==) True al    
    apply XOR   al	= -- odd  (length al - length (filter id al))
                          foldl (/=) False al
    apply NAND	al	= not . P.and $ al
    apply NOR	al	= not . P.or $ al
    apply op    al	= error $ "eval: expression not wellformed: " ++ show op ++ " " ++ show al

-- ------------------------------

collectVars	:: BoolExpr -> Names
collectVars
    = sort . nub . foldRT ids
    where
    ids (V n) al = n : concat al
    ids _     al =     concat al

truthTable	:: Names -> [Env]
truthTable
    = foldr addVar [[]]
    where
    addVar x envs
	= map ((x, False):) envs ++ map ((x, True):) envs


proofByEnumeration	:: BoolExpr -> Bool
proofByEnumeration e
    = P.and . map (flip eval e) . truthTable . collectVars $ e

-- ------------------------------

processTopDown	:: (BoolExpr -> BoolExpr) -> BoolExpr -> BoolExpr
processTopDown f e
    = RT op (map (processTopDown f) al)
    where
    (RT op al) = f e

processBottomUp	:: (BoolExpr -> BoolExpr) -> BoolExpr -> BoolExpr
processBottomUp f (RT op al)
    = f (RT op (map (processBottomUp f) al))

-- ------------------------------

partialEval	:: BoolExpr -> BoolExpr
partialEval (RT NOT [a1])
    | a1 == true				-- not true
	= false
    | a1 == false				-- not false
	= true
partialEval (RT NOT [(RT NOT [e])])		-- double negation
    = e

partialEval (RT AND al)
    | containsFalse al				-- a and false <=> false
	= false
    | containsTrue al				-- a and true <=> a
	= boolEx AND (filter (/= true) al)

partialEval (RT OR al)
    | containsTrue al				-- a or true <=> true
	= true
    | containsFalse al				-- a or false <=> a
	= boolEx OR (filter (/= false) al)

partialEval (RT IMPL [a1,a2])
    | a1 == false
	= true
    | a1 == true
	= a2
    | a2 == false
	= true
    | a2 == true
	= a1

partialEval (RT EQUIV al)
    | containsTrue al				-- (a <=> true) <=> a
	= boolEx EQUIV (filter (/= true) al)
    | containsFalse al				-- (a <=> b <=> false) <=> a xor b
	= partialEval (boolEx (if neg
			       then XOR
			       else EQUIV
			      ) al')
    where
    al' = filter (/= false) al
    neg = (length al - length al') `mod` 2 == 1

partialEval (RT XOR al)
    | containsFalse al				-- (a xor false) <=> a
	= boolEx EQUIV (filter (/= false) al)
    | containsTrue al				-- (a xor b xor true) <=> a <=> b
	= partialEval (boolEx (if neg
			       then EQUIV
			       else XOR
			      ) al')
    where
    al' = filter (/= true) al
    neg = (length al - length al') `mod` 2 == 1

partialEval e
    = e

containsFalse = not . null . filter (== false)
containsTrue  = not . null . filter (== true)

-- ------------------------------