module DataTypes
where

import Prelude hiding (and, or)

data RoseTree a
    = RT a [RoseTree a]
    deriving (Eq, Ord, Show, Read)

data BoolOp
    = F
    | T
    | V Name
    | NOT
    | AND
    | OR
    | IMPL
    | EQUIV
    | XOR
    | NAND
    | NOR
    deriving (Eq, Ord)

instance Show BoolOp
    where
    show = showOp

type BoolExpr = RoseTree BoolOp

type Name = String

type Env = [(Name, Bool)]

type Names = [Name]

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

-- useful rosetree visitors

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


mapRT	:: (a -> b) -> (RoseTree a -> RoseTree b)
mapRT f (RT e al)
    = RT (f e) (map (mapRT f) al)
 
-- ------------------------------

-- consistency

invBoolEx :: BoolExpr -> Bool
invBoolEx (RT op al)
    | op `elem` [F, T]
	= null al
invBoolEx (RT (V _) al)
    = null al
invBoolEx (RT NOT al)
    = length al == 1
invBoolEx (RT IMPL al)
    = length al == 2
invBoolEx (RT op al)
    | op `elem` [AND, OR, EQUIV, XOR, NAND, NOR]
	= length al >= 2

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

opr	:: BoolExpr -> BoolOp
opr (RT op _) = op

args	:: BoolExpr -> [BoolExpr]
args (RT _ al) = al

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

-- constants

true	:: BoolExpr
true
    = RT T []

false	:: BoolExpr
false
    = RT F []

var	:: Name -> BoolExpr
var n
    = RT (V n) []

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

-- smart constructor function

boolEx	:: BoolOp -> [BoolExpr] -> BoolExpr
boolEx op []
    | op `elem` [AND, EQUIV, NOR]
	= true
    | op `elem` [OR, XOR, NAND]
	= false

boolEx op [e1]
    | op `elem` [AND, OR, EQUIV]
	= e1
    | op `elem` [XOR, NAND, NOR]
	= boolEx NOT [e1]

boolEx op al
    | op `elem` [F,T]
      &&
      not (null al)
	= error ( "boolEx: Illegal constant expression "
	          ++ show (RT op al)
		)
boolEx (V n) al
    | not (null al)
	= error ( "boolEx: Illegal variable expression "
		  ++ show (RT (V n) al)
		)
boolEx NOT al
    | length al /= 1
	= error ( "boolEx: Illegal NOT expression "
		  ++ show (RT NOT al)
		)
boolEx IMPL al
    | length al /= 2
	= error ( "boolEx: Illegal IMPL expression "
		  ++ show (RT IMPL al)
		)

boolEx op al
    = RT op al


-- some useful unary and binary constructors

neg	:: BoolExpr -> BoolExpr
neg e
    = boolEx NOT [e]

impl	:: BoolExpr -> BoolExpr -> BoolExpr
a `impl` b
    = boolEx IMPL [a, b]

and	:: BoolExpr -> BoolExpr -> BoolExpr
a `and` b
    = boolEx AND [a, b]

or	:: BoolExpr -> BoolExpr -> BoolExpr
a `or` b
    = boolEx OR [a, b]

equiv	:: BoolExpr -> BoolExpr -> BoolExpr
a `equiv` b
    = boolEx EQUIV [a, b]

xor	:: BoolExpr -> BoolExpr -> BoolExpr
a `xor` b
    = boolEx XOR [a, b]

nand	:: BoolExpr -> BoolExpr -> BoolExpr
a `nand` b
    = boolEx NAND [a, b]

nor	:: BoolExpr -> BoolExpr -> BoolExpr
a `nor` b
    = boolEx NOR [a, b]

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

-- show functions

prio :: BoolOp -> Int
prio NOT   = 1
prio AND   = 3
prio NAND  = 3
prio OR    = 3
prio XOR   = 3
prio NOR   = 3
prio IMPL  = 4
prio EQUIV = 5
prio _     = 0

showOp F	= "false"
showOp T	= "true"
showOp (V n)	= n
showOp NOT	= "not"
showOp AND	= "and"
showOp OR	= "or"
showOp IMPL	= "=>"
showOp EQUIV	= "<=>"
showOp XOR	= "xor"
showOp NAND	= "nand"
showOp NOR	= "nor"

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

showEx :: BoolExpr -> String
showEx = showEx' 10

showEx' :: Int -> BoolExpr -> String
showEx' p (RT op al)
    | p <= pop
	= "(" ++ str ++ ")"
    | otherwise
	= str
    where
    pop = prio op

    str = show' op al

    show' op al
	| op `elem` [AND,OR,IMPL,EQUIV,XOR,NAND,NOR]
	    = foldl1 (\ x y -> x ++ " " ++ show op ++ " " ++ y)
	      .
	      map (showEx' pop) $ al
	| op == NOT
	    = show op ++ " " ++ showEx' pop (head al)
	| otherwise
	    = show op

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