import Monad

-- design obvodu

halfAdd :: Circuit m => (Bit, Bit) -> m (Bit, Bit)
halfAdd (a,b) =
  do
    carry <- and2 (a, b)
    sum <- xor2 (a, b)
    return (carry, sum)

class Monad m => Circuit m where
  and2, or2, xor2 :: (Bit, Bit) -> m Bit

-- interpretace na vyssi urovni
class Circuit m => Arithmetic m where
  plus, times :: (NumSig, NumSig) -> m NumSig

class Circuit m => Sequential m where
  delay :: Bit->Bit->m Bit
  loop :: (Bit-> m Bit)->m Bit

square :: Arithmetic m => NumSig -> m NumSig
square x = times (x,x)

-- zakladni typy
type Var = String
data Bit = Bit Bool | BitVar Var deriving (Show)

low = Bit False
high = Bit True

data NumSig = I Int
int n = I n

-- kombinatory

(>->) :: Circuit m => (a->m b) -> (b -> m c) -> (a -> m c)
(c1 >-> c2) x =
  do 
    y <- c1 x
    c2 y

compose :: Circuit m => [a -> m a] -> (a -> m a)
compose = foldr (>->) return

-- aplikace obvodu na polovinu dratu
one :: Circuit m => ([a] -> m [a]) -> ([a] -> m [a])
one h inp =
  do
    a <- h (take l inp)
    return (a ++ drop l inp)
  where
    l = (length inp) `div` 2

two :: Circuit m => ([a] -> m [a]) -> ([a] -> m [a])
two h inp =
  do
    a <- h (take l inp)
    b <- h (drop l inp)
    return (a ++ b)
  where
    l = (length inp) `div` 2

-- raised 3 two f aplikuje f na osminy dratu
raised :: Int->(a->a)->(a->a)
raised n f = (!! n) . iterate f

-- decmap aplikuje indexovane verze obvodu na jednotlive draty
decmap :: Circuit m => Int -> (Int -> a -> m b) -> ([a] -> m [b])
decmap n f inp = zipWithM f [n - 1, n - 2 .. 0] inp

-- interpretace

-- standardni interpretace (vyhodnoceni)
data Std a = Std {simulate :: a}

instance Monad Std where
  (Std a) >>= f = f a
  return x = Std x

instance Circuit Std where
  and2 (Bit x, Bit y) = return $ Bit (x && y)
  or2 (Bit x, Bit y) = return $ Bit (x || y)
  xor2 (Bit x, Bit y) = return $ Bit (x /= y)

-- symbolicka interpretace

class Circuit m => Symbolic m where
  newBitVar :: m Bit

data Sym a = Sym ([Var] -> (a, [Var], [Assertion]))
data Assertion = Var := Expression
data Expression = And [Bit]
                  | Or [Bit]
                  | Xor [Bit] deriving (Show)

instance Monad Sym where
  ...

instance Circuit Sym where
  and2 (a,b) = 
    do
      v <- newBitVar
      addAssertion (v := And [a,b])
      return (BitVar v)
  ...

-- dalsi moznosti: overovani vlastnosti, ...