module Data.Coolean
( Cool(..)
, Coolean(..)
, true, false, nott
, (&&&), (|||), (==>)
, (!&&), (!||), (!=>)
, Sched(..), sched0
, run, lookahead, par, subsetsc
) where
import Control.Exception
import Data.IORef
import System.IO.Unsafe
data Cool = Atom Bool
| Not Cool
| And Cool Cool
| 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
true :: Cool
true :: Cool
true = Bool -> Cool
Atom Bool
True
false :: Cool
false :: Cool
false = Bool -> Cool
Atom Bool
False
(&&&) :: (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 &&&
(|||) :: (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 |||
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)
(==>) :: (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 ==>
(!&&) :: (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
(!||) :: (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))
(!=>) :: (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))
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
(<&>) :: 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)
data Sched = Flip Bool Sched Sched
| 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)
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
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
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)
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)
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)
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)
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
| 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)
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)
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)
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
(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)
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)
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)