module Language.Atom.Expressions
  (
  -- * Types
    E     (..)
  , V     (..)
  , UE    (..)
  , UV    (..)
  , Expr  (..)
  , Expression (..)
  , Variable   (..)
  , Type  (..)
  , Const (..)
  , Width (..)
  , constType
  , ue
  , uv
  , ueType
  , uvType
  , ueUpstream
  , uvSet
  , NumE
  , FloatingE
  , EqE
  , OrdE
  -- * Custom Es
  , customDouble
  -- * Constants
  , true
  , false
  -- * Variable Reference and Assignment
  , value
  -- * Logical Operations
  , not_
  , (&&.)
  , (||.)
  , and_
  , or_
  , any_
  , all_
  -- * Equality and Comparison
  , (==.)
  , (/=.)
  , (<.)
  , (<=.)
  , (>.)
  , (>=.)
  , min_
  , minimum_
  , max_
  , maximum_
  , limit
  -- * Arithmetic Operations
  , div_
  , mod_
  -- * Conditional Operator
  , mux
  -- * Smart constructors for untyped expressions.
  , ubool
  , unot
  , uand
  , uor
  , ueq
  , umux
  ) where

import Data.Bits
import Data.Int
import Data.List
import Data.Ratio
import Data.Word

--infixl 7 /., %.
--infixl 6 +., -.
--infixr 5 ++.
infix  4 ==., /=., <., <=., >., >=.
infixl 3 &&. --, ^. -- , &&&, $&, $&&
infixl 2 ||. -- , |||, $$, $:, $|
--infixr 1 -- <==, <-- -- , |->, |=>, -->

-- | The type of a 'E'.
data Type
  = Bool
  | Int8
  | Int16
  | Int32
  | Int64
  | Word8
  | Word16
  | Word32
  | Word64
  | Float
  | Double
  deriving (Show, Read, Eq, Ord)

data Const
  = CBool   Bool
  | CInt8   Int8
  | CInt16  Int16
  | CInt32  Int32
  | CInt64  Int64
  | CWord8  Word8
  | CWord16 Word16
  | CWord32 Word32
  | CWord64 Word64
  | CFloat  Float
  | CDouble Double
  deriving (Eq, Ord)

instance Show Const where
  show c = case c of
    CBool   True  -> "1"
    CBool   False -> "0"
    CInt8   c -> show c
    CInt16  c -> show c
    CInt32  c -> show c
    CInt64  c -> show c
    CWord8  c -> show c
    CWord16 c -> show c
    CWord32 c -> show c
    CWord64 c -> show c
    CFloat  c -> show c
    CDouble c -> show c

constType :: Const -> Type
constType c = case c of
  CBool   _ -> Bool
  CInt8   _ -> Int8
  CInt16  _ -> Int16
  CInt32  _ -> Int32
  CInt64  _ -> Int64
  CWord8  _ -> Word8
  CWord16 _ -> Word16
  CWord32 _ -> Word32
  CWord64 _ -> Word64
  CFloat  _ -> Float
  CDouble _ -> Double

data Expression
  = EBool   (E Bool)
  | EInt8   (E Int8)
  | EInt16  (E Int16)
  | EInt32  (E Int32)
  | EInt64  (E Int64)
  | EWord8  (E Word8)
  | EWord16 (E Word16)
  | EWord32 (E Word32)
  | EWord64 (E Word64)
  | EFloat  (E Float)
  | EDouble (E Double)
  
data Variable
  = VBool   (V Bool)
  | VInt8   (V Int8)
  | VInt16  (V Int16)
  | VInt32  (V Int32)
  | VInt64  (V Int64)
  | VWord8  (V Word8)
  | VWord16 (V Word16)
  | VWord32 (V Word32)
  | VWord64 (V Word64)
  | VFloat  (V Float)
  | VDouble (V Double) deriving Eq
  

-- | Variables updated by state transition rules.
data V a = V UV deriving Eq

-- | Unsigned variables.
data UV = UV Int String Const deriving Show
instance Eq   UV where UV a _ _  == UV b _ _ = a == b
instance Ord  UV where compare (UV a _ _) (UV b _ _) = compare a b

-- | A typed expression.
data E a where
  VRef    :: V a -> E a
  Const   :: a -> E a
  Cust    :: String -> E a
  Cast    :: (NumE a, NumE b) => E a -> E b
  Add     :: NumE a => E a -> E a -> E a
  Sub     :: NumE a => E a -> E a -> E a
  Mul     :: NumE a => E a -> E a -> E a
  Div     :: NumE a => E a -> E a -> E a
  Mod     :: IntegralE a => E a -> E a -> E a
  Not     :: E Bool -> E Bool
  And     :: E Bool -> E Bool -> E Bool
  BWNot   :: IntegralE a => E a -> E a
  BWAnd   :: IntegralE a => E a -> E a -> E a
  BWOr    :: IntegralE a => E a -> E a -> E a
  Shift   :: IntegralE a => E a -> Int -> E a
  Eq      :: (EqE a, OrdE a) => E a -> E a -> E Bool
  Lt      :: OrdE a => E a -> E a -> E Bool
  Mux     :: E Bool -> E a -> E a -> E a
  F2B     :: E Float  -> E Word32
  D2B     :: E Double -> E Word64
  B2F     :: E Word32 -> E Float
  B2D     :: E Word64 -> E Double

instance Show (E a) where
  show _ = error "Show (E a) not implemented"

instance Expr a => Eq (E a) where
  a == b = ue a == ue b

-- | An untyped term.
data UE
  = UVRef UV
  | UConst Const
  | UCust  Type String
  | UCast  Type UE
  | UAdd   UE UE
  | USub   UE UE
  | UMul   UE UE
  | UDiv   UE UE
  | UMod   UE UE
  | UNot   UE
  | UAnd   [UE]
  | UBWNot UE
  | UBWAnd UE UE
  | UBWOr  UE UE
  | UShift UE Int
  | UEq    UE UE
  | ULt    UE UE
  | UMux   UE UE UE
  | UF2B   UE
  | UD2B   UE
  | UB2F   UE
  | UB2D   UE
  deriving (Show, Eq, Ord)

class Width a where
  width :: a -> Int

instance Width Type where
  width t = case t of
    Bool   -> 1
    Int8   -> 8
    Int16  -> 16
    Int32  -> 32
    Int64  -> 64
    Word8  -> 8
    Word16 -> 16
    Word32 -> 32
    Word64 -> 64
    Float  -> 32
    Double -> 64

instance Width Const           where width = width . constType
instance Expr a => Width (E a) where width = width . eType
instance Expr a => Width (V a) where width = width . eType . value
instance Width UE              where width = width . ueType

class Eq a => Expr a where
  eType      :: E a -> Type
  constant   :: a -> Const
  expression :: E a -> Expression
  variable   :: V a -> Variable
  rawBits    :: E a -> E Word64

instance Expr Bool   where
  eType _    = Bool
  constant   = CBool
  expression = EBool
  variable   = VBool
  rawBits a  = mux a 1 0

instance Expr Int8   where
  eType _    = Int8
  constant   = CInt8
  expression = EInt8
  variable   = VInt8
  rawBits    = Cast

instance Expr Int16  where
  eType _    = Int16
  constant   = CInt16
  expression = EInt16
  variable   = VInt16
  rawBits    = Cast

instance Expr Int32  where
  eType _    = Int32
  constant   = CInt32
  expression = EInt32
  variable   = VInt32
  rawBits     = Cast

instance Expr Int64  where
  eType _    = Int64
  constant   = CInt64
  expression = EInt64
  variable   = VInt64
  rawBits    = Cast

instance Expr Word8  where
  eType _    = Word8
  constant   = CWord8
  expression = EWord8
  variable   = VWord8
  rawBits    = Cast

instance Expr Word16 where
  eType _    = Word16
  constant   = CWord16
  expression = EWord16
  variable   = VWord16
  rawBits    = Cast

instance Expr Word32 where
  eType _    = Word32
  constant   = CWord32
  expression = EWord32
  variable   = VWord32
  rawBits    = Cast

instance Expr Word64 where
  eType _    = Word64
  constant   = CWord64
  expression = EWord64
  variable   = VWord64
  rawBits    = id

instance Expr Float  where
  eType _    = Float
  constant   = CFloat
  expression = EFloat
  variable   = VFloat
  rawBits    = Cast . F2B

instance Expr Double where
  eType _    = Double
  constant   = CDouble
  expression = EDouble
  variable   = VDouble
  rawBits    = D2B


class (Num a, Expr a, EqE a, OrdE a) => NumE a
instance NumE Int8
instance NumE Int16
instance NumE Int32
instance NumE Int64
instance NumE Word8
instance NumE Word16
instance NumE Word32
instance NumE Word64
instance NumE Float
instance NumE Double

class (NumE a, Integral a) => IntegralE a where signed :: E a -> Bool
instance IntegralE Int8   where signed _ = True
instance IntegralE Int16  where signed _ = True
instance IntegralE Int32  where signed _ = True
instance IntegralE Int64  where signed _ = True
instance IntegralE Word8  where signed _ = False
instance IntegralE Word16 where signed _ = False
instance IntegralE Word32 where signed _ = False
instance IntegralE Word64 where signed _ = False

class (Eq a, Expr a) => EqE a
instance EqE Bool
instance EqE Int8
instance EqE Int16
instance EqE Int32
instance EqE Int64
instance EqE Word8
instance EqE Word16
instance EqE Word32
instance EqE Word64
instance EqE Float
instance EqE Double

class (Eq a, Ord a, EqE a) => OrdE a
instance OrdE Int8
instance OrdE Int16
instance OrdE Int32
instance OrdE Int64
instance OrdE Word8
instance OrdE Word16
instance OrdE Word32
instance OrdE Word64
instance OrdE Float
instance OrdE Double

class (RealFloat a, NumE a, OrdE a) => FloatingE a
instance FloatingE Float
instance FloatingE Double

instance (Num a, NumE a, OrdE a) => Num (E a) where
  (Const a) + (Const b) = Const $ a + b
  a + b = Add a b
  (Const a) - (Const b) = Const $ a - b
  a - b = Sub a b
  (Const a) * (Const b) = Const $ a * b
  a * b = Mul a b
  negate a = 0 - a
  abs a = mux (a <. 0) (negate a) a
  signum a = mux (a ==. 0) 0 $ mux (a <. 0) (-1) 1
  fromInteger i = Const $ fromInteger i

instance (OrdE a, NumE a, Num a, Fractional a) => Fractional (E a) where
  (Const a) / (Const b) = Const $ a / b
  a / b = Div a b
  recip a = 1 / a
  fromRational r = Const $ (fromInteger (numerator r)) / (fromInteger (denominator r))

{-
instance (Num a, Fractional a, Floating a, FloatingE a) => Floating (E a) where
  pi       = Const pi
  exp      (Const a) = Const $ exp a
  exp      a         = Exp a
  log      (Const a) = Const $ log a
  log      a         = Log a
  sqrt     (Const a) = Const $ sqrt a
  sqrt     a         = Sqrt a
  (**)     (Const a) (Const b) = Const $ a ** b
  (**)     a b       = Pow a b
  sin      (Const a) = Const $ sin a
  sin      a         = Sin a
  cos      a         = sqrt (1 - sin a ** 2)
  sinh     a         = (exp a - exp (-a)) / 2
  cosh     a         = (exp a + exp (-a)) / 2
  asin     (Const a) = Const $ asin a
  asin     a         = Asin a
  acos     a         = pi / 2 - asin a
  atan     a         = asin (a / (sqrt (a ** 2 + 1)))
  asinh    a         = log (a + sqrt (a ** 2 + 1))
  acosh    a         = log (a + sqrt (a ** 2 - 1))
  atanh    a         = 0.5 * log ((1 + a) / (1 - a))
-}

instance (Expr a, OrdE a, EqE a, IntegralE a, Bits a) => Bits (E a) where
  (Const a) .&. (Const b) = Const $ a .&. b
  a .&. b = BWAnd a b
  complement (Const a) = Const $ complement a
  complement a = BWNot a
  (Const a) .|. (Const b) = Const $ a .|. b
  a .|. b = BWOr a b
  xor a b = (a .&. complement b) .|. (complement a .&. b)
  shift (Const a) n = Const $ shift a n
  shift a n = Shift a n
  rotate = error "E rotate not supported."
  bitSize  a = width a
  isSigned a = signed a

-- | Creates a custom E Double.
customDouble :: String -> E Double
customDouble c = Cust c

-- | True term.
true :: E Bool
true = Const True

-- | False term.
false :: E Bool
false = Const False

-- | Logical negation.
not_ :: E Bool -> E Bool
not_ = Not

-- | Logical AND.
(&&.) :: E Bool -> E Bool -> E Bool
(&&.) = And

-- | Logical OR.
(||.) :: E Bool -> E Bool -> E Bool
(||.) a b = not_ $ not_ a &&. not_ b

-- | The conjunction of a E Bool list.
and_ :: [E Bool] -> E Bool
and_ = foldl (&&.) true

-- | The disjunction of a E Bool list.
or_ :: [E Bool] -> E Bool
or_ = foldl (||.) false

-- | True iff the predicate is true for all elements.
all_ :: (a -> E Bool) -> [a] -> E Bool
all_ f a = and_ $ map f a

-- | True iff the predicate is true for any element.
any_ :: (a -> E Bool) -> [a] -> E Bool
any_ f a = or_ $ map f a

-- | Equal.
(==.) :: (EqE a, OrdE a) => E a -> E a -> E Bool
(==.) = Eq

-- | Not equal.
(/=.) :: (EqE a, OrdE a) => E a -> E a -> E Bool
a /=. b = not_ (a ==. b)

-- | Less than.
(<.) :: OrdE a => E a -> E a -> E Bool
(<.) = Lt

-- | Greater than.
(>.) :: OrdE a => E a -> E a -> E Bool
a >. b = b <. a

-- | Less than or equal.
(<=.) :: OrdE a => E a -> E a -> E Bool
a <=. b =  not_ (a >. b)

-- | Greater than or equal.
(>=.) :: OrdE a => E a -> E a -> E Bool
a >=. b = not_ (a <. b)

-- | Returns the minimum of two numbers.
min_ :: OrdE a => E a -> E a -> E a
min_ a b = mux (a <=. b) a b

-- | Returns the minimum of a list of numbers.
minimum_ :: OrdE a => [E a] -> E a
minimum_ = foldl1 min_

-- | Returns the maximum of two numbers.
max_ :: OrdE a => E a -> E a -> E a
max_ a b = mux (a >=. b) a b

-- | Returns the maximum of a list of numbers.
maximum_ :: OrdE a => [E a] -> E a
maximum_ = foldl1 max_

-- | Limits between min and max.
limit :: OrdE a => E a -> E a -> E a -> E a
limit a b i = max_ min $ min_ max i
  where
  min = min_ a b
  max = max_ a b

-- | Division.
div_ :: IntegralE a => E a -> E a -> E a
div_ (Const a) (Const b) = Const $ a `div` b
div_ a b = Div a b

-- | Modulo.
mod_ :: IntegralE a => E a -> E a -> E a
mod_ (Const a) (Const b) = Const $ a `mod` b
mod_ a b = Mod a b

-- | Returns the value of a 'V'.
value :: V a -> E a
value a = VRef a

-- | Conditional expression.
--
-- > mux test onTrue ofFalse
mux :: Expr a => E Bool -> E a -> E a -> E a
mux = Mux

-- | A set of all variables referenced in a term.
uvSet :: UE -> [UV]
uvSet = nub . uvList

uvList :: UE -> [UV]
uvList t = case t of
  UVRef v      -> [v]
  UCust _ _    -> []
  UCast _ a    -> uvList a
  UConst _     -> []
  UAdd a b     -> uvList a ++ uvList b
  USub a b     -> uvList a ++ uvList b
  UMul a b     -> uvList a ++ uvList b
  UDiv a b     -> uvList a ++ uvList b
  UMod a b     -> uvList a ++ uvList b
  UNot a       -> uvList a
  UAnd a       -> concatMap uvList a
  UBWNot a     -> uvList a
  UBWAnd a b   -> uvList a ++ uvList b
  UBWOr  a b   -> uvList a ++ uvList b
  UShift a _   -> uvList a
  UEq  a b     -> uvList a ++ uvList b
  ULt  a b     -> uvList a ++ uvList b
  UMux a b c   -> uvList a ++ uvList b ++ uvList c
  UF2B a       -> uvList a
  UD2B a       -> uvList a
  UB2F a       -> uvList a
  UB2D a       -> uvList a

uvType :: UV -> Type
uvType (UV _ _ c) = constType c

-- | The type of an UE.
ueType :: UE -> Type
ueType t = case t of
  UVRef uvar -> uvType uvar
  UCust t _  -> t
  UCast t _  -> t
  UConst c   -> constType c
  UAdd a _   -> ueType a
  USub a _   -> ueType a
  UMul a _   -> ueType a
  UDiv a _   -> ueType a
  UMod a _   -> ueType a
  UNot _     -> Bool
  UAnd _     -> Bool
  UBWNot a   -> ueType a
  UBWAnd a _ -> ueType a
  UBWOr  a _ -> ueType a
  UShift a _ -> ueType a
  UEq  _ _   -> Bool
  ULt  _ _   -> Bool
  UMux _ a _ -> ueType a
  UF2B _     -> Word32
  UD2B _     -> Word64
  UB2F _     -> Float
  UB2D _     -> Double

-- | The list of UEs adjacent upstream of a UE.
ueUpstream :: UE -> [UE]
ueUpstream t = case t of
  UVRef _   -> []
  UCust _ _   -> []
  UCast _ a   -> [a]
  UConst _    -> []
  UAdd a b    -> [a, b]
  USub a b    -> [a, b]
  UMul a b    -> [a, b]
  UDiv a b    -> [a, b]
  UMod a b    -> [a, b]
  UNot a      -> [a]
  UAnd a      -> a
  UBWNot a    -> [a]
  UBWAnd a b  -> [a, b]
  UBWOr  a b  -> [a, b]
  UShift a _  -> [a]
  UEq  a b    -> [a, b]
  ULt  a b    -> [a, b]
  UMux a b c  -> [a, b, c]
  UF2B a      -> [a]
  UD2B a      -> [a]
  UB2F a      -> [a]
  UB2D a      -> [a]

ue :: Expr a => E a -> UE
ue t = case t of
  VRef (V v) -> UVRef v
  Const  a     -> UConst $ constant a
  Cust   a     -> UCust    tt a
  Cast   a     -> UCast    tt (ue a)
  Add    a b   -> UAdd     (ue a) (ue b)
  Sub    a b   -> USub     (ue a) (ue b)
  Mul    a b   -> UMul     (ue a) (ue b)
  Div    a b   -> UDiv     (ue a) (ue b)
  Mod    a b   -> UMod     (ue a) (ue b)
  Not    a     -> unot     (ue a)
  And    a b   -> uand     (ue a) (ue b)
  BWNot  a     -> UBWNot   (ue a)
  BWAnd  a b   -> UBWAnd   (ue a) (ue b)
  BWOr   a b   -> UBWOr    (ue a) (ue b)
  Shift  a b   -> UShift   (ue a) b
  Eq     a b   -> ueq      (ue a) (ue b)
  Lt     a b   -> ult      (ue a) (ue b)
  Mux    a b c -> umux     (ue a) (ue b) (ue c)
  F2B    a     -> UF2B     (ue a)
  D2B    a     -> UD2B     (ue a)
  B2F    a     -> UB2F     (ue a)
  B2D    a     -> UB2D     (ue a)
  where
  tt = eType t

uv :: V a -> UV
uv (V v) = v

-- XXX A future smart constructor for numeric type casting.
-- ucast :: Type -> UE -> UE

ubool :: Bool -> UE
ubool = UConst . CBool

unot :: UE -> UE
unot (UConst (CBool a)) = ubool $ not a
unot (UNot a) = a
unot a = UNot a

uand :: UE -> UE -> UE
uand a b | a == b                   = a
uand a@(UConst (CBool False)) _     = a
uand _ a@(UConst (CBool False))     = a
uand (UConst (CBool True)) a        = a
uand a (UConst (CBool True))        = a
uand (UAnd a) (UAnd b)              = reduceAnd $ a ++ b
uand (UAnd a) b                     = reduceAnd $ b : a
uand a (UAnd b)                     = reduceAnd $ a : b
uand a b                            = reduceAnd [a, b]

reduceAnd :: [UE] -> UE

-- a && not a
reduceAnd terms | not $ null [ e | e <- terms, e' <- map unot terms, e == e' ] = ubool False

-- a == x && a == y && x /= y
reduceAnd terms | or [ f a b | a <- terms, b <- terms ]                        = ubool False
  where
  f :: UE -> UE -> Bool
  f (UEq a b) (UEq x y) | a == x = yep $ ueq b y
                        | a == y = yep $ ueq b x
                        | b == x = yep $ ueq a y
                        | b == y = yep $ ueq a x
  f _ _ = False
  yep :: UE -> Bool
  yep (UConst (CBool False)) = True
  yep _ = False

-- a && b && not (a && b)
reduceAnd terms | not $ null [ e | e <- terms, not $ null $ f e, all (flip elem terms) $ f e ] = ubool False
  where
  f :: UE -> [UE]
  f (UNot (UAnd a)) = a
  f _               = []

-- collect, sort, and return
reduceAnd terms = UAnd $ sort $ nub $ terms

uor :: UE -> UE -> UE
uor a b = unot (uand (unot a) (unot b))

ueq :: UE -> UE -> UE
ueq a b | a == b = ubool True
ueq (UConst (CBool   a)) (UConst (CBool   b)) = ubool $ a == b
ueq (UConst (CInt8   a)) (UConst (CInt8   b)) = ubool $ a == b
ueq (UConst (CInt16  a)) (UConst (CInt16  b)) = ubool $ a == b
ueq (UConst (CInt32  a)) (UConst (CInt32  b)) = ubool $ a == b
ueq (UConst (CInt64  a)) (UConst (CInt64  b)) = ubool $ a == b
ueq (UConst (CWord8  a)) (UConst (CWord8  b)) = ubool $ a == b
ueq (UConst (CWord16 a)) (UConst (CWord16 b)) = ubool $ a == b
ueq (UConst (CWord32 a)) (UConst (CWord32 b)) = ubool $ a == b
ueq (UConst (CWord64 a)) (UConst (CWord64 b)) = ubool $ a == b
ueq (UConst (CFloat  a)) (UConst (CFloat  b)) = ubool $ a == b
ueq (UConst (CDouble a)) (UConst (CDouble b)) = ubool $ a == b
ueq a b = UEq a b

ult :: UE -> UE -> UE
ult a b | a == b = ubool False
ult (UConst (CBool   a)) (UConst (CBool   b)) = ubool $ a < b
ult (UConst (CInt8   a)) (UConst (CInt8   b)) = ubool $ a < b
ult (UConst (CInt16  a)) (UConst (CInt16  b)) = ubool $ a < b
ult (UConst (CInt32  a)) (UConst (CInt32  b)) = ubool $ a < b
ult (UConst (CInt64  a)) (UConst (CInt64  b)) = ubool $ a < b
ult (UConst (CWord8  a)) (UConst (CWord8  b)) = ubool $ a < b
ult (UConst (CWord16 a)) (UConst (CWord16 b)) = ubool $ a < b
ult (UConst (CWord32 a)) (UConst (CWord32 b)) = ubool $ a < b
ult (UConst (CWord64 a)) (UConst (CWord64 b)) = ubool $ a < b
ult (UConst (CFloat  a)) (UConst (CFloat  b)) = ubool $ a < b
ult (UConst (CDouble a)) (UConst (CDouble b)) = ubool $ a < b
ult a b = ULt a b

umux :: UE -> UE -> UE -> UE
umux _ t f | t == f = f
umux b t f | ueType t == Bool = uor (uand b t) (uand (unot b) f)
umux (UConst (CBool b)) t f = if b then t else f
umux (UNot b) t f = umux b f t
umux b1 (UMux b2 t _) f | b1 == b2 = umux b1 t f
umux b1 t (UMux b2 _ f) | b1 == b2 = umux b1 t f
umux b t f = UMux b t f

{-
-- | Balances mux trees in expression.  Reduces critical path at cost of additional logic.
balance :: UE -> UE
balance ue = case ue of
  UVRef _      -> ue
  UCust _ _    -> ue
  UCast t a    -> UCast t (balance a)
  UConst _     -> ue
  UAdd a b     -> UAdd   (balance a) (balance b)
  USub a b     -> USub   (balance a) (balance b)
  UMul a b     -> UMul   (balance a) (balance b)
  UDiv a b     -> UDiv   (balance a) (balance b)
  UMod a b     -> UMod   (balance a) (balance b)
  UNot a       -> UNot   (balance a)
  UAnd a       -> UAnd   (map balance a)
  UBWNot a     -> UBWNot (balance a)
  UBWAnd a b   -> UBWAnd (balance a) (balance b)
  UBWOr  a b   -> UBWOr  (balance a) (balance b)
  UShift a n   -> UShift (balance a) n
  UEq  a b     -> UEq    (balance a) (balance b)
  ULt  a b     -> ULt    (balance a) (balance b)
  UMux a t f   -> rotate $ umux a t' f'
    where
    t' = balance t
    f' = balance f
    depth :: UE -> Int
    depth (UMux _ t f) = 1 + max (depth t) (depth f)
    depth _            = 0
    rotate :: UE -> UE
    rotate ue = case ue of
      UMux a1 t1@(UMux a2 t2 f2) f1 | depth t1 >= depth f1 + 2 -> umux (uand a1 a2) t2 (umux a1 f2 f1)
      UMux a1 t1 f1@(UMux a2 t2 f2) | depth f1 >= depth t1 + 2 -> umux (uor  a1 a2) (umux a1 t1 t2) f2
      _ -> ue
-}

-- Idea analyzing a pair of comparisons with one common operand: take to other two operands and construct the appropriate
-- expression and check never.
-- never (a == x) && (a == y)  =>  never (x == y)
-- never (a == x) && (a <  y)  =>  never (x >= y)
-- never (a == x) && (a /= y)  =>  never (x == y)
-- never (a == x) || (a == y)  =>  never (x == y)
{-
isExclusiveCompare :: (ConstantCompare, ConstantCompare) -> Bool
isExclusiveCompare a = case a of
  (Equal a, Equal     b) -> a /= b
  (Equal a, NotEqual  b) -> a == b
  (Equal a, Less      b) -> a >= b
  (Equal a, LessEqual b) -> a >  b
  (Equal a, More      b) -> a <= b
  (Equal a, MoreEqual b) -> a <  b

  (NotEqual a, Equal     b) -> a == b
  (NotEqual _, _)           -> False

  (Less  a, Equal     b) -> a <= b
  (Less  a, More      b) -> a <= b
  (Less  a, MoreEqual b) -> a <= b
  (Less  _, _)           -> False

  (LessEqual  a, Equal     b) -> a <  b
  (LessEqual  a, More      b) -> a <= b
  (LessEqual  a, MoreEqual b) -> a <  b
  (LessEqual  _, _)           -> False

  (More  a, Equal     b) -> a >= b
  (More  a, Less      b) -> a >= b
  (More  a, LessEqual b) -> a >= b
  (More  _, _)           -> False

  (MoreEqual  a, Equal     b) -> a >  b
  (MoreEqual  a, Less      b) -> a >= b
  (MoreEqual  a, LessEqual b) -> a >  b
  (MoreEqual  _, _)           -> False

data ConstantCompare
  = Equal     TermConst
  | NotEqual  TermConst
  | Less      TermConst
  | LessEqual TermConst
  | More      TermConst
  | MoreEqual TermConst
  deriving (Eq, Ord)
-}

--data NetList = NetList Int (IntMap UE)