-- | Proper documentation is TBD

module Data.Coolean
 ( Cool(..)
 -- * Overloaded parallel operators

 , Coolean(..)
 , true, false, nott
 , (&&&), (|||), (==>)
 -- * Overloaded sequential operators

 , (!&&), (!||), (!=>)
 -- * Consumers

 , Sched(..), sched0
 , run, lookahead, par, subsetsc
 ) where

import Control.Exception
import Data.IORef
import System.IO.Unsafe

-- import Data.Tree


-- | Concurrent booleans. Writing properties with the Cool data type often yields faster searches compared to Bool. 

data Cool = Atom Bool
          | Not Cool
          | And Cool Cool
          -- | Sequential conjunction, the second operator is not evaluated unless the first is true. 

          | Seq Cool Cool
          deriving Int -> Cool -> ShowS
[Cool] -> ShowS
Cool -> String
(Int -> Cool -> ShowS)
-> (Cool -> String) -> ([Cool] -> ShowS) -> Show Cool
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Cool] -> ShowS
$cshowList :: [Cool] -> ShowS
show :: Cool -> String
$cshow :: Cool -> String
showsPrec :: Int -> Cool -> ShowS
$cshowsPrec :: Int -> Cool -> ShowS
Show

-- Class based construction

true :: Cool
true :: Cool
true = Bool -> Cool
Atom Bool
True

false :: Cool
false :: Cool
false = Bool -> Cool
Atom Bool
False

-- | Commutative conjunction

(&&&) :: (Coolean a, Coolean b) => a -> b -> Cool
a
a &&& :: a -> b -> Cool
&&& b
b = a -> Cool
forall b. Coolean b => b -> Cool
toCool a
a Cool -> Cool -> Cool
<&> b -> Cool
forall b. Coolean b => b -> Cool
toCool b
b

infixr 3 &&&

-- | Commutative disjunction

(|||) :: (Coolean a, Coolean b) => a -> b -> Cool
a
a ||| :: a -> b -> Cool
||| b
b = a -> Cool
forall b. Coolean b => b -> Cool
toCool a
a Cool -> Cool -> Cool
<||> b -> Cool
forall b. Coolean b => b -> Cool
toCool b
b

infixr 2 |||

-- | Negation

nott :: Coolean a => a -> Cool
nott :: a -> Cool
nott a
a = Cool -> Cool
Not (a -> Cool
forall b. Coolean b => b -> Cool
toCool a
a)

-- | Parallel implication

(==>) :: (Coolean a, Coolean b) => a -> b -> Cool
a
a ==> :: a -> b -> Cool
==> b
b = Cool -> Cool
Not (a -> Cool
forall b. Coolean b => b -> Cool
toCool a
a Cool -> Cool -> Cool
<&> Cool -> Cool
Not (b -> Cool
forall b. Coolean b => b -> Cool
toCool b
b))

infixr 0 ==>

-- | Sequential conjunction. Does not evaluate second operand unless first is True. 

(!&&) :: (Coolean a, Coolean b) => a -> b -> Cool
a
a !&& :: a -> b -> Cool
!&& b
b = a -> Cool
forall b. Coolean b => b -> Cool
toCool a
a Cool -> Cool -> Cool
`Seq` b -> Cool
forall b. Coolean b => b -> Cool
toCool b
b

-- | Sequential disjunction. Does not evaluate second operand unless first is True. 

(!||) :: (Coolean a, Coolean b) => a -> b -> Cool
a
a !|| :: a -> b -> Cool
!|| b
b = Cool -> Cool
Not (Cool -> Cool
Not (a -> Cool
forall b. Coolean b => b -> Cool
toCool a
a) Cool -> Cool -> Cool
`Seq` Cool -> Cool
Not (b -> Cool
forall b. Coolean b => b -> Cool
toCool b
b))

-- | Sequential implication. Does not evaluate second operand unless first is True. 

(!=>) :: (Coolean a, Coolean b) => a -> b -> Cool
a
a !=> :: a -> b -> Cool
!=> b
b = Cool -> Cool
Not (a -> Cool
forall b. Coolean b => b -> Cool
toCool a
a Cool -> Cool -> Cool
`Seq` Cool -> Cool
Not (b -> Cool
forall b. Coolean b => b -> Cool
toCool b
b))


-- | Provides better interoperability between Bool and Cool by overloading operators. 

class Coolean b where
  toCool :: b -> Cool
  toBool :: b -> Bool
  isCool :: (a -> b) -> Bool

instance Coolean Cool where 
  toCool :: Cool -> Cool
toCool = Cool -> Cool
forall a. a -> a
id
  toBool :: Cool -> Bool
toBool (And Cool
a Cool
b) = Cool -> Bool
forall b. Coolean b => b -> Bool
toBool Cool
a Bool -> Bool -> Bool
&& Cool -> Bool
forall b. Coolean b => b -> Bool
toBool Cool
b
  toBool (Seq Cool
a Cool
b) = Cool -> Bool
forall b. Coolean b => b -> Bool
toBool Cool
a Bool -> Bool -> Bool
&& Cool -> Bool
forall b. Coolean b => b -> Bool
toBool Cool
b
  toBool (Not Cool
a)   = Bool -> Bool
not (Cool -> Bool
forall b. Coolean b => b -> Bool
toBool Cool
a)
  toBool (Atom Bool
a)  = Bool
a
  isCool :: (a -> Cool) -> Bool
isCool a -> Cool
_ = Bool
True

instance Coolean Bool where 
  toCool :: Bool -> Cool
toCool = Bool -> Cool
Atom
  toBool :: Bool -> Bool
toBool = Bool -> Bool
forall a. a -> a
id
  isCool :: (a -> Bool) -> Bool
isCool a -> Bool
_ = Bool
False


-- Explicit construction

(<&>) :: Cool -> Cool -> Cool
<&> :: Cool -> Cool -> Cool
(<&>) = Cool -> Cool -> Cool
And

(<&) :: Bool -> Cool -> Cool
Bool
a <& :: Bool -> Cool -> Cool
<& Cool
b = Bool -> Cool
Atom Bool
a Cool -> Cool -> Cool
<&> Cool
b

(&>) :: Cool -> Bool -> Cool
Cool
a &> :: Cool -> Bool -> Cool
&> Bool
b = Cool
a Cool -> Cool -> Cool
<&> Bool -> Cool
Atom Bool
b

(&) :: Bool -> Bool -> Cool
Bool
a & :: Bool -> Bool -> Cool
& Bool
b = Bool -> Cool
Atom Bool
a Cool -> Cool -> Cool
<&> Bool -> Cool
Atom Bool
b


Cool
a <||> :: Cool -> Cool -> Cool
<||> Cool
b = Cool -> Cool
Not (Cool -> Cool
Not Cool
a Cool -> Cool -> Cool
<&> Cool -> Cool
Not Cool
b)


-- Consumers

data Sched = Flip Bool Sched Sched
--           | Fixed

           | Unsched
           deriving (Int -> Sched -> ShowS
[Sched] -> ShowS
Sched -> String
(Int -> Sched -> ShowS)
-> (Sched -> String) -> ([Sched] -> ShowS) -> Show Sched
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sched] -> ShowS
$cshowList :: [Sched] -> ShowS
show :: Sched -> String
$cshow :: Sched -> String
showsPrec :: Int -> Sched -> ShowS
$cshowsPrec :: Int -> Sched -> ShowS
Show, Sched -> Sched -> Bool
(Sched -> Sched -> Bool) -> (Sched -> Sched -> Bool) -> Eq Sched
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sched -> Sched -> Bool
$c/= :: Sched -> Sched -> Bool
== :: Sched -> Sched -> Bool
$c== :: Sched -> Sched -> Bool
Eq)

-- instance Show Sched where show = drawTree . toTree


split :: Sched -> Sched
split :: Sched -> Sched
split Sched
Unsched = Bool -> Sched -> Sched -> Sched
Flip Bool
False Sched
Unsched Sched
Unsched
split Sched
s   = Sched
s

sched0 :: Sched
sched0 = Sched
Unsched

-- toTree :: Sched -> Tree String

-- toTree Unsched = Node "*" []

-- toTree (Flip b s1 s2) = Node (show b) [toTree s1, toTree s2]



-- Run the given schedule

run :: Sched -> Cool -> Bool
run :: Sched -> Cool -> Bool
run (Sched
Unsched) Cool
c     = Cool -> Bool
forall b. Coolean b => b -> Bool
toBool Cool
c
run s :: Sched
s@(Flip Bool
b Sched
s1 Sched
s2) Cool
c = case Cool
c of
  Atom Bool
b     -> Bool
b
  Not Cool
c      -> Bool -> Bool
not (Sched -> Cool -> Bool
run Sched
s Cool
c)
  Seq Cool
c1 Cool
c2  -> Sched -> Cool -> Bool
run Sched
s1 Cool
c1 Bool -> Bool -> Bool
&& Sched -> Cool -> Bool
run Sched
s2 Cool
c2
  And Cool
c1 Cool
c2
    | Bool
b         -> Sched -> Cool -> Bool
run Sched
s2 Cool
c2 Bool -> Bool -> Bool
&& Sched -> Cool -> Bool
run Sched
s1 Cool
c1
    | Bool
otherwise -> Sched -> Cool -> Bool
run Sched
s1 Cool
c1 Bool -> Bool -> Bool
&& Sched -> Cool -> Bool
run Sched
s2 Cool
c2


-- Returns a schedule with optimal short-circuiting behaviour

lookahead :: Sched -> Cool  -> (Sched, Bool)
lookahead :: Sched -> Cool -> (Sched, Bool)
lookahead Sched
s Cool
c = case Cool
c of
  Atom Bool
b     -> (Sched
s,Bool
b)
  Not Cool
c      -> (Bool -> Bool) -> (Sched, Bool) -> (Sched, Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not (Sched -> Cool -> (Sched, Bool)
lookahead Sched
s Cool
c)
  Seq Cool
c1 Cool
c2  -> (Sched, Bool) -> (Sched, Bool) -> (Sched, Bool)
go (Sched -> Cool -> (Sched, Bool)
lookahead Sched
s1 Cool
c1) (Sched -> Cool -> (Sched, Bool)
lookahead Sched
s2 Cool
c2)
    where
    (Flip Bool
b Sched
s1 Sched
s2) = Sched -> Sched
split Sched
s
    go :: (Sched, Bool) -> (Sched, Bool) -> (Sched, Bool)
go (Sched
s1',Bool
r1) ~(Sched
s2',Bool
r2) = case Bool
r1 of
      Bool
True   -> case Bool
r2 of 
        Bool
True   -> (Bool -> Sched -> Sched -> Sched
Flip Bool
False Sched
s1' Sched
s2', Bool
True)    -- Set to unflipped if True

        Bool
False  -> (Bool -> Sched -> Sched -> Sched
Flip Bool
True  Sched
s1 Sched
s2', Bool
False)
      Bool
False  -> (Bool -> Sched -> Sched -> Sched
Flip Bool
b Sched
s1' Sched
s2, Bool
False)

    -- (Flip b s1' s2', r1 && r2)

    -- where (s1', r1) = lookahead s1 c1

    --      (s2', r2) = lookahead s2 c2

    --      (Flip b s1 s2) = split s

  And Cool
c1 Cool
c2
    | Bool
b         -> (Bool -> Sched -> Sched -> Sched)
-> (Sched, Bool) -> (Sched, Bool) -> (Sched, Bool)
forall a.
(Bool -> Sched -> Sched -> a)
-> (Sched, Bool) -> (Sched, Bool) -> (a, Bool)
go (\Bool
b' -> (Sched -> Sched -> Sched) -> Sched -> Sched -> Sched
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> Sched -> Sched -> Sched
Flip Bool
b')) (Sched -> Cool -> (Sched, Bool)
lookahead Sched
s2 Cool
c2) (Sched -> Cool -> (Sched, Bool)
lookahead Sched
s1 Cool
c1)
    | Bool
otherwise -> (Bool -> Sched -> Sched -> Sched)
-> (Sched, Bool) -> (Sched, Bool) -> (Sched, Bool)
forall a.
(Bool -> Sched -> Sched -> a)
-> (Sched, Bool) -> (Sched, Bool) -> (a, Bool)
go (\Bool
b' -> Bool -> Sched -> Sched -> Sched
Flip Bool
b')        (Sched -> Cool -> (Sched, Bool)
lookahead Sched
s1 Cool
c1) (Sched -> Cool -> (Sched, Bool)
lookahead Sched
s2 Cool
c2)
    where
    (Flip Bool
b Sched
s1 Sched
s2) = Sched -> Sched
split Sched
s
    go :: (Bool -> Sched -> Sched -> a)
-> (Sched, Bool) -> (Sched, Bool) -> (a, Bool)
go Bool -> Sched -> Sched -> a
flp (Sched
s1',Bool
r1) ~(Sched
s2',Bool
r2) = case Bool
r1 of
      Bool
True   -> case Bool
r2 of 
        Bool
True   -> (Bool -> Sched -> Sched -> a
flp Bool
False Sched
s1' Sched
s2', Bool
True)    -- Set to unflipped if True

        Bool
False  -> (Bool -> Sched -> Sched -> a
flp (Bool -> Bool
not Bool
b) Sched
s1 Sched
s2', Bool
False)
      Bool
False  -> (Bool -> Sched -> Sched -> a
flp Bool
b Sched
s1' Sched
s2, Bool
False)




-- Flip all evaluated parallel conjunctions

par :: Sched -> Cool -> (Sched, Bool)
par :: Sched -> Cool -> (Sched, Bool)
par Sched
s Cool
c = case Cool
c of
  Atom Bool
b     -> (Sched
s,Bool
b)
  Not Cool
c      -> (Bool -> Bool) -> (Sched, Bool) -> (Sched, Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not (Sched -> Cool -> (Sched, Bool)
par Sched
s Cool
c)
  Seq Cool
c1 Cool
c2  -- -> (Flip b s1' s2', r1 && r2)

    | Bool
b         -> (Bool -> Sched -> Sched -> Sched)
-> (Sched, Bool) -> (Sched, Bool) -> (Sched, Bool)
forall a.
(Bool -> Sched -> Sched -> a)
-> (Sched, Bool) -> (Sched, Bool) -> (a, Bool)
go (\Bool
b' -> (Sched -> Sched -> Sched) -> Sched -> Sched -> Sched
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> Sched -> Sched -> Sched
Flip Bool
b')) (Sched -> Cool -> (Sched, Bool)
par Sched
s2 Cool
c2) (Sched -> Cool -> (Sched, Bool)
par Sched
s1 Cool
c1)
    | Bool
otherwise -> (Bool -> Sched -> Sched -> Sched)
-> (Sched, Bool) -> (Sched, Bool) -> (Sched, Bool)
forall a.
(Bool -> Sched -> Sched -> a)
-> (Sched, Bool) -> (Sched, Bool) -> (a, Bool)
go (\Bool
b' -> Bool -> Sched -> Sched -> Sched
Flip Bool
b')        (Sched -> Cool -> (Sched, Bool)
par Sched
s1 Cool
c1) (Sched -> Cool -> (Sched, Bool)
par Sched
s2 Cool
c2)
    where
    (Flip Bool
b Sched
s1 Sched
s2) = Sched -> Sched
split Sched
s
    go :: (Bool -> Sched -> Sched -> a)
-> (Sched, Bool) -> (Sched, Bool) -> (a, Bool)
go Bool -> Sched -> Sched -> a
flp (Sched
s1',Bool
r1) ~(Sched
s2',Bool
r2) = case Bool
r1 of
      Bool
True   -> case Bool
r2 of 
        Bool
True   -> (Bool -> Sched -> Sched -> a
flp Bool
b Sched
s1' Sched
s2', Bool
True)       -- Flip here?

        Bool
False  -> (Bool -> Sched -> Sched -> a
flp Bool
b Sched
s1 Sched
s2', Bool
False)
      Bool
False  -> (Bool -> Sched -> Sched -> a
flp Bool
b Sched
s1' Sched
s2, Bool
False)
  And Cool
c1 Cool
c2
    | Bool
b         -> (Bool -> Sched -> Sched -> Sched)
-> (Sched, Bool) -> (Sched, Bool) -> (Sched, Bool)
forall a.
(Bool -> Sched -> Sched -> a)
-> (Sched, Bool) -> (Sched, Bool) -> (a, Bool)
go (\Bool
b' -> (Sched -> Sched -> Sched) -> Sched -> Sched -> Sched
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> Sched -> Sched -> Sched
Flip Bool
b')) (Sched -> Cool -> (Sched, Bool)
par Sched
s2 Cool
c2) (Sched -> Cool -> (Sched, Bool)
par Sched
s1 Cool
c1)
    | Bool
otherwise -> (Bool -> Sched -> Sched -> Sched)
-> (Sched, Bool) -> (Sched, Bool) -> (Sched, Bool)
forall a.
(Bool -> Sched -> Sched -> a)
-> (Sched, Bool) -> (Sched, Bool) -> (a, Bool)
go (\Bool
b' -> Bool -> Sched -> Sched -> Sched
Flip Bool
b')        (Sched -> Cool -> (Sched, Bool)
par Sched
s1 Cool
c1) (Sched -> Cool -> (Sched, Bool)
par Sched
s2 Cool
c2)
    where
    (Flip Bool
b Sched
s1 Sched
s2) = Sched -> Sched
split Sched
s
    go :: (Bool -> Sched -> Sched -> a)
-> (Sched, Bool) -> (Sched, Bool) -> (a, Bool)
go Bool -> Sched -> Sched -> a
flp (Sched
s1',Bool
r1) ~(Sched
s2',Bool
r2) = case Bool
r1 of
      Bool
True   -> case Bool
r2 of 
        Bool
True   -> (Bool -> Sched -> Sched -> a
flp (Bool
False) Sched
s1' Sched
s2', Bool
True)       -- Flip here?

        Bool
False  -> (Bool -> Sched -> Sched -> a
flp (Bool -> Bool
not Bool
b) Sched
s1 Sched
s2', Bool
False)
      Bool
False  -> (Bool -> Sched -> Sched -> a
flp (Bool -> Bool
not Bool
b) Sched
s1' Sched
s2, Bool
False)




-- Returns a schedule with optimal short-circuiting behaviour and 

-- giving preference to choice-subset operands

subsetsc :: IO Int -> Sched -> Cool -> IO (Sched, Bool)
subsetsc :: IO Int -> Sched -> Cool -> IO (Sched, Bool)
subsetsc IO Int
io Sched
s0 Cool
c0 = Sched -> Cool -> IO (Sched, Bool)
go Sched
s0 Cool
c0 where
  go :: Sched -> Cool -> IO (Sched, Bool)
go Sched
s Cool
c = case Cool
c of
    Atom Bool
b      -> (Sched, Bool) -> IO (Sched, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sched
s,Bool
b)
    Not Cool
c'      -> ((Sched, Bool) -> (Sched, Bool))
-> IO (Sched, Bool) -> IO (Sched, Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bool -> Bool) -> (Sched, Bool) -> (Sched, Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Bool -> Bool
not) (Sched -> Cool -> IO (Sched, Bool)
go Sched
s Cool
c')
    Seq Cool
c1 Cool
c2  -> do 
      (Sched
s1', Bool
r1) <- Sched -> Cool -> IO (Sched, Bool)
go Sched
s1 Cool
c1
      (Sched
s2', Bool
r2) <- Sched -> Cool -> IO (Sched, Bool)
go Sched
s2 Cool
c2
      (Sched, Bool) -> IO (Sched, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Sched -> Sched -> Sched
Flip Bool
b Sched
s1' Sched
s2', Bool
r1 Bool -> Bool -> Bool
&& Bool
r2)
      where (Flip Bool
b Sched
s1 Sched
s2) = Sched -> Sched
split Sched
s
    And Cool
c1 Cool
c2
      | Bool
b         -> (Bool -> Sched -> Sched -> Sched)
-> IO (Sched, Bool) -> IO (Sched, Bool) -> IO (Sched, Bool)
forall a.
(Bool -> Sched -> Sched -> a)
-> IO (Sched, Bool) -> IO (Sched, Bool) -> IO (a, Bool)
go' (\Bool
b' -> (Sched -> Sched -> Sched) -> Sched -> Sched -> Sched
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> Sched -> Sched -> Sched
Flip Bool
b')) (Sched -> Cool -> IO (Sched, Bool)
go Sched
s2 Cool
c2) (Sched -> Cool -> IO (Sched, Bool)
go Sched
s1 Cool
c1)
      | Bool
otherwise -> (Bool -> Sched -> Sched -> Sched)
-> IO (Sched, Bool) -> IO (Sched, Bool) -> IO (Sched, Bool)
forall a.
(Bool -> Sched -> Sched -> a)
-> IO (Sched, Bool) -> IO (Sched, Bool) -> IO (a, Bool)
go' (\Bool
b' -> Bool -> Sched -> Sched -> Sched
Flip Bool
b')        (Sched -> Cool -> IO (Sched, Bool)
go Sched
s1 Cool
c1) (Sched -> Cool -> IO (Sched, Bool)
go Sched
s2 Cool
c2)
      where
--      unchanged s1' s2' | b = Flip 

      (Flip Bool
b Sched
s1 Sched
s2) = Sched -> Sched
split Sched
s
      go' :: (Bool -> Sched -> Sched -> a)
-> IO (Sched, Bool) -> IO (Sched, Bool) -> IO (a, Bool)
go' Bool -> Sched -> Sched -> a
flp IO (Sched, Bool)
m1 IO (Sched, Bool)
m2 = do
        (Sched
s1',Bool
r1) <- IO (Sched, Bool)
m1 
        case Bool
r1 of
          Bool
True   -> do
            (Sched
s2',Bool
r2) <- IO (Sched, Bool)
m2
            case Bool
r2 of 
              Bool
True   -> (a, Bool) -> IO (a, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Sched -> Sched -> a
flp Bool
False Sched
s1' Sched
s2', Bool
True)    -- Set to unflipped if True

              Bool
False  -> (a, Bool) -> IO (a, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Sched -> Sched -> a
flp (Bool -> Bool
not Bool
b) Sched
s1 Sched
s2', Bool
False)
          Bool
False  -> do
            Int
n <- IO Int
io
            (Sched
s2',Bool
r2) <- IO (Sched, Bool)
m2

            case Bool
r2 of 
              Bool
True  -> (a, Bool) -> IO (a, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Sched -> Sched -> a
flp Bool
b Sched
s1' Sched
s2, Bool
False)
              Bool
False -> do
                Int
n' <- IO Int
io
                if (Int
n' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n) -- The other operand made at least one distinct choice

                  then (a, Bool) -> IO (a, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Sched -> Sched -> a
flp Bool
b Sched
s1' Sched
s2, Bool
False) 
                  else (a, Bool) -> IO (a, Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Sched -> Sched -> a
flp (Bool -> Bool
not Bool
b) Sched
s1 Sched
s2', Bool
False)

-- measure :: IO Int -> Sched -> Cool




{-
suspending :: IORef (Map ThreadId (ThreadId, ThreadId)) -> IORef (Map ThreadId Integer) -> Cool -> IO Bool
suspending threads ref c0 = do 
  mv <- newEmptyMVar
  forkIO (go (putMVar mv) c0)
  takeMVar mv
  
  where
  go :: (Bool -> IO ()) -> Cool -> IO ()
  go res c = case c of
    Not c'     -> go (res . not) c'
    And c1 c2  -> do
      mv <- newEmptyMVar 
      let res' = putMVar mv
      t <- myThreadId
      t1 <- forkIO (go res' c1)
      t2 <- forkIO (go res' c2)
      atomicModifyIORef threads (\m -> (M.insert t (t1,t2) m,()))
      b1 <- takeMVar mv
      let cleanup = do 
            ts <- fmap (`clean` (t1,t2)) (readIORef threads)
            mapM killThread ts
          ret b = cleanup >> res b
      case b1 of 
        False  -> ret False
        True   -> do
          b2 <- takeMVar mv
          case b2 of 
            False  -> ret False
            True   -> ret True
    Atom b     -> evaluate b >>= res


clean :: Map ThreadId (ThreadId, ThreadId) -> (ThreadId, ThreadId) -> [ThreadId]
clean m (t1,t2) = t1:t2:(r t1 ++ r t2)
  where r t = maybe [] id (fmap (clean m) (M.lookup t m))

-}
{-

runInterl :: Cool -> Bool
runInterl = unRes . interl

data Res = Now Bool | Later Res
unRes :: Res -> Bool
unRes (Now b)    = b
unRes (Later x)  = unRes x


interl :: Cool -> Res
interl (Not c)     = Later (interl c) -- Negating consumes an action
interl (And c1 c2) = mer (interl c1) (interl c2) where
{-  mer :: Res -> Res -> Res
  mer r1 r2 = case r1 of
    Now False -> Now False
    Now True  -> r2
    Later r1' -> Later (mer r2 r1') -}
  mer :: Res -> Res -> Res
  mer (Now False) _           = Now False
  mer _           (Now False) = Now False
  mer (Now True)  (Now True)  = Now True
  mer (Later r1') (Later r2') = Later (mer r1' r2')
interl (Atom b)    = Now b
interl (Seq c1 c2) = seqi (interl c1) (interl c2) where 
  seqi (Now False) r2 = Now False
  seqi (Now True)  r2 = r2
  seqi (Later r1') r2 = Later (seqi r1' r2)


prune :: Cool -> Cool -> (Bool,Cool)
prune (Atom a)     c2            = (a, c2)
prune (Not c1)     ~(Not d1)     = case prune c1 d1 of (b,c) -> (not b, Not c)
prune (And c1 c2)  ~(And d1 d2)  = case prune c1 d1 of
      (False, p)  -> (False, p)
      (True,  p)  -> case prune c2 d2 of
        (False, q) -> (False, q)
        (True,  q) -> (True, Seq p q)
prune (Seq c1 c2)  ~(Seq d1 d2)  = case prune c1 d1 of
      (False, p)  -> case prune c2 d2 of
        (False, q) -> (False, And p q)
        (True, q)  -> (False, p)
      (True,  p)  -> case prune c2 d2 of
        (False, q) -> (False, q)
        (True,  q) -> (True, Seq p q)



-- Check that the schedule is optimal
rerun :: Sched -> Cool -> Maybe Bool
rerun Unsched c       = Just (toBool c) -- Should only be Not and Atom
rerun s@(Flip b s1 s2) c = case c of
  Atom b     -> Just b
  Not c      -> fmap not (rerun s c)
  Seq c1 c2  -> rerun s1 c1 && run s2 c2
  And c1 c2
    | b         -> rerun s2 c2 &&&& rerun s1 c1
    | otherwise -> rerun s1 c1 &&&& rerun s2 c2
  where
    Just False &&&& _          = Just False
    Just True  &&&& Just True  = Just True
    _          &&&& _          = Nothing
-}
  

{-
lazify :: Cool -> Cool -> (Bool, Bool)
lazify (Atom a)   ~(Atom x)   = (a,x)
lazify (Not a)    ~(Not x)    = case lazify a x of (b1,b2) -> (not b1, not b2)
lazify (And a b)  ~(And x y)  
  = case lazify a x of
      (False, p)  -> (False, p)
      (True,  p)  -> case lazify b y of
        (False, q) -> (False, q)
        (True,  q) -> (True, p && q)

coolio :: Cool -> Cool -> Cool -> (Bool, Bool, Bool)
coolio (Atom a) ~(Atom x) ~(Atom p) = (a,x,p)
coolio (And a b) ~(And x y) ~(And p q)  
  = case coolio a x p of
      (False, rx, rp)  -> (False, rx, rp)
      (True, rx, rp)   -> case coolio b y q of
        (False, ry, rq) -> (False, ry, rq)
        (True, ry, rq)  -> (True, rx && ry, rp && rq)



data UnCool = UnCool deriving (Show,Read)
instance Exception UnCool

unCool :: a -> IO (IO Bool, a)
unCool a = do
  r <- newIORef False
  let toggle = atomicModifyIORef r (\b -> (not b, b))
      a'     = unsafeDupablePerformIO $ do
        b <- readIORef r
        print b
        if b then return a else throw UnCool
  
  return (toggle, a')


-- unCool :: a

isCool :: Bool -> Bool
isCool b = unsafeDupablePerformIO $ do
  catch (b `seq` return True) (\UnCool -> return False)


test = do
  (tog,a) <- unCool 1
  let x = Just a
  catch (x == Just 1 `seq` print True) (\UnCool -> print "Cool")
  tog -- >>= print
  catch (x == Just 1 `seq` print True) (\UnCool -> print "Not Cool")
  
  
-}
  
  
-- uncool