lazy-search-0.1.2.0: src/Data/Coolean.hs
-- | 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 Show
-- Class based construction
true :: Cool
true = Atom True
false :: Cool
false = Atom False
-- | Commutative conjunction
(&&&) :: (Coolean a, Coolean b) => a -> b -> Cool
a &&& b = toCool a <&> toCool b
infixr 3 &&&
-- | Commutative disjunction
(|||) :: (Coolean a, Coolean b) => a -> b -> Cool
a ||| b = toCool a <||> toCool b
infixr 2 |||
-- | Negation
nott :: Coolean a => a -> Cool
nott a = Not (toCool a)
-- | Parallel implication
(==>) :: (Coolean a, Coolean b) => a -> b -> Cool
a ==> b = Not (toCool a <&> Not (toCool b))
infixr 0 ==>
-- | Sequential conjunction. Does not evaluate second operand unless first is True.
(!&&) :: (Coolean a, Coolean b) => a -> b -> Cool
a !&& b = toCool a `Seq` toCool b
-- | Sequential disjunction. Does not evaluate second operand unless first is True.
(!||) :: (Coolean a, Coolean b) => a -> b -> Cool
a !|| b = Not (Not (toCool a) `Seq` Not (toCool b))
-- | Sequential implication. Does not evaluate second operand unless first is True.
(!=>) :: (Coolean a, Coolean b) => a -> b -> Cool
a !=> b = Not (toCool a `Seq` Not (toCool 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 = id
toBool (And a b) = toBool a && toBool b
toBool (Seq a b) = toBool a && toBool b
toBool (Not a) = not (toBool a)
toBool (Atom a) = a
isCool _ = True
instance Coolean Bool where
toCool = Atom
toBool = id
isCool _ = False
-- Explicit construction
(<&>) :: Cool -> Cool -> Cool
(<&>) = And
(<&) :: Bool -> Cool -> Cool
a <& b = Atom a <&> b
(&>) :: Cool -> Bool -> Cool
a &> b = a <&> Atom b
(&) :: Bool -> Bool -> Cool
a & b = Atom a <&> Atom b
a <||> b = Not (Not a <&> Not b)
-- Consumers
data Sched = Flip Bool Sched Sched
-- | Fixed
| Unsched
deriving (Show, Eq)
-- instance Show Sched where show = drawTree . toTree
split :: Sched -> Sched
split Unsched = Flip False Unsched Unsched
split s = s
sched0 = 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 (Unsched) c = toBool c
run s@(Flip b s1 s2) c = case c of
Atom b -> b
Not c -> not (run s c)
Seq c1 c2 -> run s1 c1 && run s2 c2
And c1 c2
| b -> run s2 c2 && run s1 c1
| otherwise -> run s1 c1 && run s2 c2
-- Returns a schedule with optimal short-circuiting behaviour
lookahead :: Sched -> Cool -> (Sched, Bool)
lookahead s c = case c of
Atom b -> (s,b)
Not c -> fmap not (lookahead s c)
Seq c1 c2 -> go (lookahead s1 c1) (lookahead s2 c2)
where
(Flip b s1 s2) = split s
go (s1',r1) ~(s2',r2) = case r1 of
True -> case r2 of
True -> (Flip False s1' s2', True) -- Set to unflipped if True
False -> (Flip True s1 s2', False)
False -> (Flip b s1' s2, 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 c1 c2
| b -> go (\b' -> flip (Flip b')) (lookahead s2 c2) (lookahead s1 c1)
| otherwise -> go (\b' -> Flip b') (lookahead s1 c1) (lookahead s2 c2)
where
(Flip b s1 s2) = split s
go flp (s1',r1) ~(s2',r2) = case r1 of
True -> case r2 of
True -> (flp False s1' s2', True) -- Set to unflipped if True
False -> (flp (not b) s1 s2', False)
False -> (flp b s1' s2, False)
-- Flip all evaluated parallel conjunctions
par :: Sched -> Cool -> (Sched, Bool)
par s c = case c of
Atom b -> (s,b)
Not c -> fmap not (par s c)
Seq c1 c2 -- -> (Flip b s1' s2', r1 && r2)
| b -> go (\b' -> flip (Flip b')) (par s2 c2) (par s1 c1)
| otherwise -> go (\b' -> Flip b') (par s1 c1) (par s2 c2)
where
(Flip b s1 s2) = split s
go flp (s1',r1) ~(s2',r2) = case r1 of
True -> case r2 of
True -> (flp b s1' s2', True) -- Flip here?
False -> (flp b s1 s2', False)
False -> (flp b s1' s2, False)
And c1 c2
| b -> go (\b' -> flip (Flip b')) (par s2 c2) (par s1 c1)
| otherwise -> go (\b' -> Flip b') (par s1 c1) (par s2 c2)
where
(Flip b s1 s2) = split s
go flp (s1',r1) ~(s2',r2) = case r1 of
True -> case r2 of
True -> (flp (False) s1' s2', True) -- Flip here?
False -> (flp (not b) s1 s2', False)
False -> (flp (not b) s1' s2, 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 s0 c0 = go s0 c0 where
go s c = case c of
Atom b -> return (s,b)
Not c' -> fmap (fmap not) (go s c')
Seq c1 c2 -> do
(s1', r1) <- go s1 c1
(s2', r2) <- go s2 c2
return (Flip b s1' s2', r1 && r2)
where (Flip b s1 s2) = split s
And c1 c2
| b -> go' (\b' -> flip (Flip b')) (go s2 c2) (go s1 c1)
| otherwise -> go' (\b' -> Flip b') (go s1 c1) (go s2 c2)
where
-- unchanged s1' s2' | b = Flip
(Flip b s1 s2) = split s
go' flp m1 m2 = do
(s1',r1) <- m1
case r1 of
True -> do
(s2',r2) <- m2
case r2 of
True -> return (flp False s1' s2', True) -- Set to unflipped if True
False -> return (flp (not b) s1 s2', False)
False -> do
n <- io
(s2',r2) <- m2
case r2 of
True -> return (flp b s1' s2, False)
False -> do
n' <- io
if (n' > n) -- The other operand made at least one distinct choice
then return (flp b s1' s2, False)
else return (flp (not b) s1 s2', 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