{-#LANGUAGE GADTs, DeriveDataTypeable, DeriveFunctor #-}
module Control.Search
(
search, sat, ctrex, searchRaw, usearch
, test, testTime
, Options (..)
, sat', search', ctrex', searchRaw', test', testTime'
, (&&&), (|||), (==>), nott, true, false
, Cool(..)
, Coolean
, module Control.Enumerable
) where
import Data.IORef
import Control.Sized
import Control.Enumerable
import System.IO.Unsafe
import Control.Enumerable.Count
import Data.Coolean
import System.Timeout
newCounter :: IO (IO Int)
newCounter :: IO (IO Int)
newCounter = do
IORef Int
ref <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0
IO Int -> IO (IO Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (IORef Int -> (Int -> (Int, Int)) -> IO Int
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef Int
ref (\Int
i -> (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Int
i)))
attach :: (IO Int) -> a -> IO (IO Int, a)
attach :: IO Int -> a -> IO (IO Int, a)
attach IO Int
c a
a = do
IORef Int
ref <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef (-Int
1)
(IO Int, a) -> IO (IO Int, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
ref, IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> IO a -> a
forall a b. (a -> b) -> a -> b
$ IO Int
c IO Int -> (Int -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IORef Int -> Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Int
ref IO () -> IO a -> IO a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a)
data Value a where
Pair :: (a,b) -> Value a -> Value b -> Value (a,b)
Map :: a -> (b -> a) -> Value b -> Value a
Unit :: a -> Value a
Alt :: a -> Value a -> Minimal a -> Value a
instance Show a => Show (Value a) where
show :: Value a -> String
show Value a
v = String
"("String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value a -> String
forall a. Value a -> String
repV Value a
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (Value a -> a
forall a. Value a -> a
plainV Value a
v) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
instance Functor Value where
fmap :: (a -> b) -> Value a -> Value b
fmap a -> b
f Value a
a = b -> (a -> b) -> Value a -> Value b
forall a b. a -> (b -> a) -> Value b -> Value a
Map (a -> b
f (Value a -> a
forall a. Value a -> a
plainV Value a
a)) a -> b
f Value a
a
repV :: Value a -> String
repV :: Value a -> String
repV (Unit a
_) = String
"1"
repV (Pair (a, b)
_ Value a
a Value b
b) = String
"("String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value a -> String
forall a. Value a -> String
repV Value a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value b -> String
forall a. Value a -> String
repV Value b
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
repV (Alt a
_ Value a
a Minimal a
_) = String
"?"String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value a -> String
forall a. Value a -> String
repV Value a
a
repV (Map a
a b -> a
f Value b
v) = String
"$"String -> ShowS
forall a. [a] -> [a] -> [a]
++ Value b -> String
forall a. Value a -> String
repV Value b
v
plainV :: Value a -> a
plainV :: Value a -> a
plainV (Pair (a, b)
a Value a
_ Value b
_) = a
(a, b)
a
plainV (Map a
a b -> a
_ Value b
_) = a
a
plainV (Unit a
a) = a
a
plainV (Alt a
a Value a
_ Minimal a
_) = a
a
mkPair :: Value a -> Value b -> Value (a,b)
mkPair :: Value a -> Value b -> Value (a, b)
mkPair (Unit a
a) (Unit b
b) = (a, b) -> Value (a, b)
forall a. a -> Value a
Unit (a
a,b
b)
mkPair (Unit a
a) Value b
v = (b -> (a, b)) -> Value b -> Value (a, b)
forall a b. (a -> b) -> Value a -> Value b
mkMap ((,) a
a) Value b
v
mkPair Value a
v (Unit b
b) = (a -> (a, b)) -> Value a -> Value (a, b)
forall a b. (a -> b) -> Value a -> Value b
mkMap (\a
a -> (a
a,b
b)) Value a
v
mkPair Value a
v1 Value b
v2 = (a, b) -> Value a -> Value b -> Value (a, b)
forall a b. (a, b) -> Value a -> Value b -> Value (a, b)
Pair (Value a -> a
forall a. Value a -> a
plainV Value a
v1,Value b -> b
forall a. Value a -> a
plainV Value b
v2) Value a
v1 Value b
v2
mkAlt :: Value a -> Minimal a -> Value a
mkAlt :: Value a -> Minimal a -> Value a
mkAlt Value a
v Minimal a
s = a -> Value a -> Minimal a -> Value a
forall a. a -> Value a -> Minimal a -> Value a
Alt (Value a -> a
forall a. Value a -> a
plainV Value a
v) Value a
v Minimal a
s
mkMap :: (a -> b) -> Value a -> Value b
mkMap :: (a -> b) -> Value a -> Value b
mkMap a -> b
f (Unit a
a) = b -> Value b
forall a. a -> Value a
Unit (a -> b
f a
a)
mkMap a -> b
f (Map a
a b -> a
g Value b
v) = b -> (b -> b) -> Value b -> Value b
forall a b. a -> (b -> a) -> Value b -> Value a
Map (a -> b
f a
a) (a -> b
f (a -> b) -> (b -> a) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
g) Value b
v
mkMap a -> b
f Value a
v = b -> (a -> b) -> Value a -> Value b
forall a b. a -> (b -> a) -> Value b -> Value a
Map (a -> b
f (Value a -> a
forall a. Value a -> a
plainV Value a
v)) a -> b
f Value a
v
data Minimal a where
Pay :: Minimal a -> Minimal a
Value :: Value a -> Minimal a
Empty :: Minimal a
deriving Typeable
instance Functor Minimal where
fmap :: (a -> b) -> Minimal a -> Minimal b
fmap a -> b
f (Pay Minimal a
s) = Minimal b -> Minimal b
forall a. Minimal a -> Minimal a
Pay ((a -> b) -> Minimal a -> Minimal b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Minimal a
s)
fmap a -> b
f (Value Value a
v) = Value b -> Minimal b
forall a. Value a -> Minimal a
Value ((a -> b) -> Value a -> Value b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Value a
v)
fmap a -> b
_ Minimal a
Empty = Minimal b
forall a. Minimal a
Empty
instance Applicative Minimal where
pure :: a -> Minimal a
pure a
a = Value a -> Minimal a
forall a. Value a -> Minimal a
Value (a -> Value a
forall a. a -> Value a
Unit a
a)
Minimal (a -> b)
sf <*> :: Minimal (a -> b) -> Minimal a -> Minimal b
<*> Minimal a
sa = ((a -> b, a) -> b) -> Minimal (a -> b, a) -> Minimal b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((a -> b) -> a -> b) -> (a -> b, a) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)) (Minimal (a -> b) -> Minimal a -> Minimal (a -> b, a)
forall (f :: * -> *) a b. Sized f => f a -> f b -> f (a, b)
pair Minimal (a -> b)
sf Minimal a
sa)
instance Alternative Minimal where
empty :: Minimal a
empty = Minimal a
forall a. Minimal a
Empty
Minimal a
Empty <|> :: Minimal a -> Minimal a -> Minimal a
<|> Minimal a
s = Minimal a
s
Minimal a
s <|> Minimal a
Empty = Minimal a
s
Pay Minimal a
a <|> Pay Minimal a
b = Minimal a -> Minimal a
forall a. Minimal a -> Minimal a
Pay (Minimal a
a Minimal a -> Minimal a -> Minimal a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Minimal a
b)
Value Value a
vf <|> Minimal a
s = Value a -> Minimal a
forall a. Value a -> Minimal a
Value (Value a -> Minimal a -> Value a
forall a. Value a -> Minimal a -> Value a
mkAlt Value a
vf Minimal a
s)
Minimal a
a <|> Value Value a
vf = Value a -> Minimal a
forall a. Value a -> Minimal a
Value (Value a -> Minimal a -> Value a
forall a. Value a -> Minimal a -> Value a
mkAlt Value a
vf Minimal a
a)
instance Sized Minimal where
pay :: Minimal a -> Minimal a
pay = Minimal a -> Minimal a
forall a. Minimal a -> Minimal a
Pay
pair :: Minimal a -> Minimal b -> Minimal (a, b)
pair Minimal a
Empty Minimal b
_ = Minimal (a, b)
forall a. Minimal a
Empty
pair Minimal a
_ Minimal b
Empty = Minimal (a, b)
forall a. Minimal a
Empty
pair (Pay Minimal a
a) Minimal b
b = Minimal (a, b) -> Minimal (a, b)
forall a. Minimal a -> Minimal a
Pay (Minimal a -> Minimal b -> Minimal (a, b)
forall (f :: * -> *) a b. Sized f => f a -> f b -> f (a, b)
pair Minimal a
a Minimal b
b)
pair Minimal a
a (Pay Minimal b
b) = Minimal (a, b) -> Minimal (a, b)
forall a. Minimal a -> Minimal a
Pay (Minimal a -> Minimal b -> Minimal (a, b)
forall (f :: * -> *) a b. Sized f => f a -> f b -> f (a, b)
pair Minimal a
a Minimal b
b)
pair (Value Value a
f) (Value Value b
g) = Value (a, b) -> Minimal (a, b)
forall a. Value a -> Minimal a
Value (Value a -> Value b -> Value (a, b)
forall a b. Value a -> Value b -> Value (a, b)
mkPair Value a
f Value b
g)
naturals :: Minimal Integer
naturals = Integer -> Minimal Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
0 Minimal Integer -> Minimal Integer -> Minimal Integer
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Minimal Integer -> Minimal Integer
forall (f :: * -> *) a. Sized f => f a -> f a
pay ((Integer -> Integer) -> Minimal Integer -> Minimal Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) Minimal Integer
forall (f :: * -> *). Sized f => f Integer
naturals)
aconcat :: [Minimal a] -> Minimal a
aconcat [] = Minimal a
forall (f :: * -> *) a. Alternative f => f a
empty
aconcat [Minimal a
s] = Minimal a
s
aconcat [Minimal a
s1,Minimal a
s2] = Minimal a
s1 Minimal a -> Minimal a -> Minimal a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Minimal a
s2
aconcat [Minimal a]
ss0 = case [Minimal a] -> ([Minimal a], Maybe (Value a))
forall a. [Minimal a] -> ([Minimal a], Maybe (Value a))
extr [Minimal a]
ss0 of
([],Maybe (Value a)
m) -> Minimal a -> (Value a -> Minimal a) -> Maybe (Value a) -> Minimal a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Minimal a
forall a. Minimal a
Empty Value a -> Minimal a
forall a. Value a -> Minimal a
Value Maybe (Value a)
m
([Minimal a]
ss',Maybe (Value a)
m) -> Minimal a -> (Value a -> Minimal a) -> Maybe (Value a) -> Minimal a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Minimal a -> Minimal a
forall (f :: * -> *) a. Sized f => f a -> f a
pay ([Minimal a] -> Minimal a
forall (f :: * -> *) a. Sized f => [f a] -> f a
aconcat [Minimal a]
ss')) (Value a -> Minimal a
forall a. Value a -> Minimal a
Value (Value a -> Minimal a)
-> (Value a -> Value a) -> Value a -> Minimal a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value a -> Minimal a -> Value a
forall a. Value a -> Minimal a -> Value a
`mkAlt` ([Minimal a] -> Minimal a
forall (f :: * -> *) a. Sized f => [f a] -> f a
aconcat [Minimal a]
ss'))) Maybe (Value a)
m
where
extr :: [Minimal a] -> ([Minimal a], Maybe (Value a))
extr :: [Minimal a] -> ([Minimal a], Maybe (Value a))
extr (Minimal a
s:[Minimal a]
ss) = case Minimal a
s of
Value Value a
v -> ([Minimal a]
ss,Value a -> Maybe (Value a)
forall a. a -> Maybe a
Just Value a
v)
Minimal a
Empty -> [Minimal a] -> ([Minimal a], Maybe (Value a))
forall a. [Minimal a] -> ([Minimal a], Maybe (Value a))
extr [Minimal a]
ss
Pay Minimal a
s' -> case [Minimal a] -> ([Minimal a], Maybe (Value a))
forall a. [Minimal a] -> ([Minimal a], Maybe (Value a))
extr [Minimal a]
ss of
([Minimal a]
ss',Maybe (Value a)
Nothing) -> (Minimal a
s'Minimal a -> [Minimal a] -> [Minimal a]
forall a. a -> [a] -> [a]
:[Minimal a]
ss',Maybe (Value a)
forall a. Maybe a
Nothing)
([Minimal a]
ss',Maybe (Value a)
j) -> (Minimal a
sMinimal a -> [Minimal a] -> [Minimal a]
forall a. a -> [a] -> [a]
:[Minimal a]
ss', Maybe (Value a)
j)
extr [Minimal a]
_ = ([], Maybe (Value a)
forall a. Maybe a
Nothing)
data Observed a = Observed { Observed a -> Int
sizeLeft :: Int, Observed a -> Value a
val :: Value a } deriving a -> Observed b -> Observed a
(a -> b) -> Observed a -> Observed b
(forall a b. (a -> b) -> Observed a -> Observed b)
-> (forall a b. a -> Observed b -> Observed a) -> Functor Observed
forall a b. a -> Observed b -> Observed a
forall a b. (a -> b) -> Observed a -> Observed b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Observed b -> Observed a
$c<$ :: forall a b. a -> Observed b -> Observed a
fmap :: (a -> b) -> Observed a -> Observed b
$cfmap :: forall a b. (a -> b) -> Observed a -> Observed b
Functor
instance Show a => Show (Observed a) where
show :: Observed a -> String
show = Value a -> String
forall a. Show a => a -> String
show (Value a -> String)
-> (Observed a -> Value a) -> Observed a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Observed a -> Value a
forall a. Observed a -> Value a
val
minimal :: Minimal a -> Int -> Maybe (Observed a)
minimal :: Minimal a -> Int -> Maybe (Observed a)
minimal Minimal a
_ Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = Maybe (Observed a)
forall a. Maybe a
Nothing
minimal Minimal a
Empty Int
_ = Maybe (Observed a)
forall a. Maybe a
Nothing
minimal (Pay Minimal a
s) Int
n = Minimal a -> Int -> Maybe (Observed a)
forall a. Minimal a -> Int -> Maybe (Observed a)
minimal Minimal a
s (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
minimal (Value Value a
vf) Int
n = Observed a -> Maybe (Observed a)
forall a. a -> Maybe a
Just (Int -> Value a -> Observed a
forall a. Int -> Value a -> Observed a
Observed Int
n Value a
vf)
data Relevant a = Relevant
{
Relevant a -> Int
evalOrder :: Int,
Relevant a -> Value a
fixed :: Value a,
Relevant a -> Observed a
swapped :: Observed a
}
(<<) :: Relevant a -> Relevant b -> Bool
Relevant a
r << :: Relevant a -> Relevant b -> Bool
<< Relevant b
q = Relevant a -> Int
forall a. Relevant a -> Int
evalOrder Relevant a
r Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Relevant b -> Int
forall a. Relevant a -> Int
evalOrder Relevant b
q
merge :: Value a -> Value b -> [Relevant a] -> [Relevant b] -> [Relevant (a,b)]
merge :: Value a
-> Value b -> [Relevant a] -> [Relevant b] -> [Relevant (a, b)]
merge Value a
va Value b
_ [] [Relevant b]
r = (Value b -> Value (a, b)) -> [Relevant b] -> [Relevant (a, b)]
forall a b. (Value a -> Value b) -> [Relevant a] -> [Relevant b]
rsmap (Value a -> Value b -> Value (a, b)
forall a b. Value a -> Value b -> Value (a, b)
mkPair Value a
va) [Relevant b]
r
merge Value a
_ Value b
vb [Relevant a]
r [] = (Value a -> Value (a, b)) -> [Relevant a] -> [Relevant (a, b)]
forall a b. (Value a -> Value b) -> [Relevant a] -> [Relevant b]
rsmap (Value a -> Value b -> Value (a, b)
forall a b. Value a -> Value b -> Value (a, b)
`mkPair` Value b
vb) [Relevant a]
r
merge Value a
va Value b
vb rs :: [Relevant a]
rs@(Relevant a
r:[Relevant a]
rs') qs :: [Relevant b]
qs@(Relevant b
q:[Relevant b]
qs')
| Relevant b
q Relevant b -> Relevant a -> Bool
forall a b. Relevant a -> Relevant b -> Bool
<< Relevant a
r = (Value b -> Value (a, b)) -> Relevant b -> Relevant (a, b)
forall a b. (Value a -> Value b) -> Relevant a -> Relevant b
rmap (Value a
va Value a -> Value b -> Value (a, b)
forall a b. Value a -> Value b -> Value (a, b)
`mkPair`) Relevant b
q Relevant (a, b) -> [Relevant (a, b)] -> [Relevant (a, b)]
forall a. a -> [a] -> [a]
: Value a
-> Value b -> [Relevant a] -> [Relevant b] -> [Relevant (a, b)]
forall a b.
Value a
-> Value b -> [Relevant a] -> [Relevant b] -> [Relevant (a, b)]
merge Value a
va (Relevant b -> Value b
forall a. Relevant a -> Value a
fixed Relevant b
q) [Relevant a]
rs [Relevant b]
qs'
| Bool
otherwise = (Value a -> Value (a, b)) -> Relevant a -> Relevant (a, b)
forall a b. (Value a -> Value b) -> Relevant a -> Relevant b
rmap (Value a -> Value b -> Value (a, b)
forall a b. Value a -> Value b -> Value (a, b)
`mkPair` Value b
vb) Relevant a
r Relevant (a, b) -> [Relevant (a, b)] -> [Relevant (a, b)]
forall a. a -> [a] -> [a]
: Value a
-> Value b -> [Relevant a] -> [Relevant b] -> [Relevant (a, b)]
forall a b.
Value a
-> Value b -> [Relevant a] -> [Relevant b] -> [Relevant (a, b)]
merge (Relevant a -> Value a
forall a. Relevant a -> Value a
fixed Relevant a
r) Value b
vb [Relevant a]
rs' [Relevant b]
qs
rmap :: (Value a -> Value b) -> Relevant a -> Relevant b
rmap :: (Value a -> Value b) -> Relevant a -> Relevant b
rmap Value a -> Value b
f Relevant a
r = Relevant a
r{fixed :: Value b
fixed = Value a -> Value b
f (Relevant a -> Value a
forall a. Relevant a -> Value a
fixed Relevant a
r), swapped :: Observed b
swapped = (Value a -> Value b) -> Observed a -> Observed b
forall a a. (Value a -> Value a) -> Observed a -> Observed a
omap Value a -> Value b
f (Relevant a -> Observed a
forall a. Relevant a -> Observed a
swapped Relevant a
r)} where
omap :: (Value a -> Value a) -> Observed a -> Observed a
omap Value a -> Value a
g Observed a
o' = Observed a
o'{val :: Value a
val = Value a -> Value a
g (Observed a -> Value a
forall a. Observed a -> Value a
val Observed a
o')}
rsmap :: (Value a -> Value b) -> [Relevant a] -> [Relevant b]
rsmap :: (Value a -> Value b) -> [Relevant a] -> [Relevant b]
rsmap Value a -> Value b
f = (Relevant a -> Relevant b) -> [Relevant a] -> [Relevant b]
forall a b. (a -> b) -> [a] -> [b]
map ((Value a -> Value b) -> Relevant a -> Relevant b
forall a b. (Value a -> Value b) -> Relevant a -> Relevant b
rmap Value a -> Value b
f)
observed :: Observed a -> IO (IO [Observed a], a)
observed :: Observed a -> IO (IO [Observed a], a)
observed Observed a
o = do
IO Int
c <- IO (IO Int)
newCounter
let go :: Value a -> IO (IO [Relevant a], a)
go :: Value a -> IO (IO [Relevant a], a)
go (Pair (a, b)
_ Value a
va Value b
vb) = do
(IO [Relevant a]
rs, a
xa) <- Value a -> IO (IO [Relevant a], a)
forall a. Value a -> IO (IO [Relevant a], a)
go Value a
va
(IO [Relevant b]
qs, b
xb) <- Value b -> IO (IO [Relevant b], b)
forall a. Value a -> IO (IO [Relevant a], a)
go Value b
vb
(IO [Relevant (a, b)], (a, b)) -> IO (IO [Relevant (a, b)], (a, b))
forall (m :: * -> *) a. Monad m => a -> m a
return (([Relevant a] -> [Relevant b] -> [Relevant (a, b)])
-> IO [Relevant a] -> IO [Relevant b] -> IO [Relevant (a, b)]
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (Value a
-> Value b -> [Relevant a] -> [Relevant b] -> [Relevant (a, b)]
forall a b.
Value a
-> Value b -> [Relevant a] -> [Relevant b] -> [Relevant (a, b)]
merge Value a
va Value b
vb) IO [Relevant a]
rs IO [Relevant b]
qs, (a
xa,b
xb))
go (Map a
_ b -> a
f Value b
v) = do
~(IO [Relevant b]
x,b
a) <- (Value b -> IO (IO [Relevant b], b)
forall a. Value a -> IO (IO [Relevant a], a)
go Value b
v)
(IO [Relevant a], a) -> IO (IO [Relevant a], a)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Relevant b] -> [Relevant a])
-> IO [Relevant b] -> IO [Relevant a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Value b -> Value a) -> [Relevant b] -> [Relevant a]
forall a b. (Value a -> Value b) -> [Relevant a] -> [Relevant b]
rsmap ((b -> a) -> Value b -> Value a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> a
f)) IO [Relevant b]
x,b -> a
f b
a)
go (Unit a
a) = (IO [Relevant a], a) -> IO (IO [Relevant a], a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Relevant a] -> IO [Relevant a]
forall (m :: * -> *) a. Monad m => a -> m a
return [], a
a)
go (Alt a
_ Value a
v Minimal a
x) = do
~(IO [Relevant a]
tr,a
a) <- Value a -> IO (IO [Relevant a], a)
forall a. Value a -> IO (IO [Relevant a], a)
go Value a
v
(IO Int
i, a
a') <- IO Int -> a -> IO (IO Int, a)
forall a. IO Int -> a -> IO (IO Int, a)
attach IO Int
c a
a
(IO [Relevant a], a) -> IO (IO [Relevant a], a)
forall (m :: * -> *) a. Monad m => a -> m a
return (IO [Relevant a] -> IO Int -> IO [Relevant a]
tralt IO [Relevant a]
tr IO Int
i, a
a')
where
tralt :: IO [Relevant a] -> IO Int -> IO [Relevant a]
tralt IO [Relevant a]
tr IO Int
i = IO Int
i IO Int -> (Int -> IO [Relevant a]) -> IO [Relevant a]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Int
n -> case Int
n of
-1 -> [Relevant a] -> IO [Relevant a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
Int
_ -> case Minimal a -> Int -> Maybe (Observed a)
forall a. Minimal a -> Int -> Maybe (Observed a)
minimal Minimal a
x (Observed a -> Int
forall a. Observed a -> Int
sizeLeft Observed a
o) of
Just Observed a
nv -> ([Relevant a] -> [Relevant a])
-> IO [Relevant a] -> IO [Relevant a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Value a -> Observed a -> Relevant a
forall a. Int -> Value a -> Observed a -> Relevant a
Relevant Int
n Value a
v Observed a
nv Relevant a -> [Relevant a] -> [Relevant a]
forall a. a -> [a] -> [a]
:) IO [Relevant a]
tr
Maybe (Observed a)
Nothing -> IO [Relevant a]
tr
((IO [Relevant a], a) -> (IO [Observed a], a))
-> IO (IO [Relevant a], a) -> IO (IO [Observed a], a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(IO [Relevant a]
a,a
b) -> (([Relevant a] -> [Observed a])
-> IO [Relevant a] -> IO [Observed a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Relevant a] -> [Observed a]
forall a. [Relevant a] -> [Observed a]
fx IO [Relevant a]
a, a
b)) (IO (IO [Relevant a], a) -> IO (IO [Observed a], a))
-> IO (IO [Relevant a], a) -> IO (IO [Observed a], a)
forall a b. (a -> b) -> a -> b
$ Value a -> IO (IO [Relevant a], a)
forall a. Value a -> IO (IO [Relevant a], a)
go (Observed a -> Value a
forall a. Observed a -> Value a
val Observed a
o) where
fx :: [Relevant a] -> [Observed a]
fx :: [Relevant a] -> [Observed a]
fx [Relevant a]
rs = [Observed a] -> [Observed a]
forall a. [a] -> [a]
reverse ((Relevant a -> Observed a) -> [Relevant a] -> [Observed a]
forall a b. (a -> b) -> [a] -> [b]
map Relevant a -> Observed a
forall a. Relevant a -> Observed a
swapped [Relevant a]
rs)
observedc :: Observed a -> IO (IO Int, IO [Observed a], a)
observedc :: Observed a -> IO (IO Int, IO [Observed a], a)
observedc Observed a
o = do
IORef Int
ref <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0
let c :: IO Int
c = IORef Int -> (Int -> (Int, Int)) -> IO Int
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef Int
ref (\Int
i -> (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Int
i))
let go :: Value a -> IO (IO [Relevant a], a)
go :: Value a -> IO (IO [Relevant a], a)
go (Pair (a, b)
_ Value a
va Value b
vb) = do
(IO [Relevant a]
rs, a
xa) <- Value a -> IO (IO [Relevant a], a)
forall a. Value a -> IO (IO [Relevant a], a)
go Value a
va
(IO [Relevant b]
qs, b
xb) <- Value b -> IO (IO [Relevant b], b)
forall a. Value a -> IO (IO [Relevant a], a)
go Value b
vb
(IO [Relevant (a, b)], (a, b)) -> IO (IO [Relevant (a, b)], (a, b))
forall (m :: * -> *) a. Monad m => a -> m a
return (([Relevant a] -> [Relevant b] -> [Relevant (a, b)])
-> IO [Relevant a] -> IO [Relevant b] -> IO [Relevant (a, b)]
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (Value a
-> Value b -> [Relevant a] -> [Relevant b] -> [Relevant (a, b)]
forall a b.
Value a
-> Value b -> [Relevant a] -> [Relevant b] -> [Relevant (a, b)]
merge Value a
va Value b
vb) IO [Relevant a]
rs IO [Relevant b]
qs, (a
xa,b
xb))
go (Map a
_ b -> a
f Value b
v) = do
~(IO [Relevant b]
x,b
a) <- (Value b -> IO (IO [Relevant b], b)
forall a. Value a -> IO (IO [Relevant a], a)
go Value b
v)
(IO [Relevant a], a) -> IO (IO [Relevant a], a)
forall (m :: * -> *) a. Monad m => a -> m a
return (([Relevant b] -> [Relevant a])
-> IO [Relevant b] -> IO [Relevant a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Value b -> Value a) -> [Relevant b] -> [Relevant a]
forall a b. (Value a -> Value b) -> [Relevant a] -> [Relevant b]
rsmap ((b -> a) -> Value b -> Value a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> a
f)) IO [Relevant b]
x,b -> a
f b
a)
go (Unit a
a) = (IO [Relevant a], a) -> IO (IO [Relevant a], a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Relevant a] -> IO [Relevant a]
forall (m :: * -> *) a. Monad m => a -> m a
return [], a
a)
go (Alt a
_ Value a
v Minimal a
x) = do
~(IO [Relevant a]
tr,a
a) <- Value a -> IO (IO [Relevant a], a)
forall a. Value a -> IO (IO [Relevant a], a)
go Value a
v
(IO Int
i, a
a') <- IO Int -> a -> IO (IO Int, a)
forall a. IO Int -> a -> IO (IO Int, a)
attach IO Int
c a
a
(IO [Relevant a], a) -> IO (IO [Relevant a], a)
forall (m :: * -> *) a. Monad m => a -> m a
return (IO [Relevant a] -> IO Int -> IO [Relevant a]
tralt IO [Relevant a]
tr IO Int
i, a
a')
where
tralt :: IO [Relevant a] -> IO Int -> IO [Relevant a]
tralt IO [Relevant a]
tr IO Int
i = IO Int
i IO Int -> (Int -> IO [Relevant a]) -> IO [Relevant a]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Int
n -> case Int
n of
-1 -> [Relevant a] -> IO [Relevant a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
Int
_ -> case Minimal a -> Int -> Maybe (Observed a)
forall a. Minimal a -> Int -> Maybe (Observed a)
minimal Minimal a
x (Observed a -> Int
forall a. Observed a -> Int
sizeLeft Observed a
o) of
Just Observed a
nv -> ([Relevant a] -> [Relevant a])
-> IO [Relevant a] -> IO [Relevant a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Value a -> Observed a -> Relevant a
forall a. Int -> Value a -> Observed a -> Relevant a
Relevant Int
n Value a
v Observed a
nv Relevant a -> [Relevant a] -> [Relevant a]
forall a. a -> [a] -> [a]
:) IO [Relevant a]
tr
Maybe (Observed a)
Nothing -> IO [Relevant a]
tr
((IO [Relevant a], a) -> (IO Int, IO [Observed a], a))
-> IO (IO [Relevant a], a) -> IO (IO Int, IO [Observed a], a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(IO [Relevant a]
a,a
b) -> (IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef IORef Int
ref, ([Relevant a] -> [Observed a])
-> IO [Relevant a] -> IO [Observed a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Relevant a] -> [Observed a]
forall a. [Relevant a] -> [Observed a]
fx IO [Relevant a]
a, a
b)) (IO (IO [Relevant a], a) -> IO (IO Int, IO [Observed a], a))
-> IO (IO [Relevant a], a) -> IO (IO Int, IO [Observed a], a)
forall a b. (a -> b) -> a -> b
$ Value a -> IO (IO [Relevant a], a)
forall a. Value a -> IO (IO [Relevant a], a)
go (Observed a -> Value a
forall a. Observed a -> Value a
val Observed a
o) where
fx :: [Relevant a] -> [Observed a]
fx :: [Relevant a] -> [Observed a]
fx [Relevant a]
rs = [Observed a] -> [Observed a]
forall a. [a] -> [a]
reverse ((Relevant a -> Observed a) -> [Relevant a] -> [Observed a]
forall a b. (a -> b) -> [a] -> [b]
map Relevant a -> Observed a
forall a. Relevant a -> Observed a
swapped [Relevant a]
rs)
type State a = [[Observed a]]
type StateP a = [(Sched, [Observed a])]
{-#INLINE stepD #-}
stepD :: (a -> Bool) -> State a -> IO ((Bool, a), State a)
stepD :: (a -> Bool) -> State a -> IO ((Bool, a), State a)
stepD a -> Bool
q ((Observed a
o:[Observed a]
os):State a
s) = do
let s' :: State a
s' = if [Observed a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Observed a]
os then State a
s else [Observed a]
os[Observed a] -> State a -> State a
forall a. a -> [a] -> [a]
:State a
s
(IO [Observed a]
ins, a
a) <- Observed a -> IO (IO [Observed a], a)
forall a. Observed a -> IO (IO [Observed a], a)
observed Observed a
o
let b :: Bool
b = a -> Bool
q a
a
() <- Bool
b Bool -> IO () -> IO ()
`seq` () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Observed a]
os' <- IO [Observed a]
ins
((Bool, a), State a) -> IO ((Bool, a), State a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
b, Value a -> a
forall a. Value a -> a
plainV (Observed a -> Value a
forall a. Observed a -> Value a
val Observed a
o)), if [Observed a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Observed a]
os' then State a
s' else [Observed a]
os'[Observed a] -> State a -> State a
forall a. a -> [a] -> [a]
:State a
s')
stepD a -> Bool
_ State a
_ = String -> IO ((Bool, a), State a)
forall a. HasCallStack => String -> a
error (String -> IO ((Bool, a), State a))
-> String -> IO ((Bool, a), State a)
forall a b. (a -> b) -> a -> b
$ String
"Invalid state"
searchRawD :: Enumerable a => Int -> (a -> Bool) -> IO [(Bool,a)]
searchRawD :: Int -> (a -> Bool) -> IO [(Bool, a)]
searchRawD Int
n a -> Bool
q = do
let mo :: Maybe (Observed a)
mo = Minimal a -> Int -> Maybe (Observed a)
forall a. Minimal a -> Int -> Maybe (Observed a)
minimal Minimal a
forall (f :: * -> *) a. (Typeable f, Sized f, Enumerable a) => f a
local Int
n
IO [(Bool, a)]
-> (Observed a -> IO [(Bool, a)])
-> Maybe (Observed a)
-> IO [(Bool, a)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([(Bool, a)] -> IO [(Bool, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (\Observed a
o -> (a -> Bool) -> State a -> IO [(Bool, a)]
forall a. (a -> Bool) -> State a -> IO [(Bool, a)]
lazy a -> Bool
q [[Observed a
o]]) Maybe (Observed a)
mo
where
lazy :: (a -> Bool) -> State a -> IO [(Bool,a)]
lazy :: (a -> Bool) -> State a -> IO [(Bool, a)]
lazy a -> Bool
_ [] = [(Bool, a)] -> IO [(Bool, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
lazy a -> Bool
q' State a
s = do
((Bool, a)
ba,State a
s') <- (a -> Bool) -> State a -> IO ((Bool, a), State a)
forall a. (a -> Bool) -> State a -> IO ((Bool, a), State a)
stepD a -> Bool
q' State a
s
([(Bool, a)] -> [(Bool, a)]) -> IO [(Bool, a)] -> IO [(Bool, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bool, a)
ba(Bool, a) -> [(Bool, a)] -> [(Bool, a)]
forall a. a -> [a] -> [a]
:) (IO [(Bool, a)] -> IO [(Bool, a)]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [(Bool, a)] -> IO [(Bool, a)])
-> IO [(Bool, a)] -> IO [(Bool, a)]
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> State a -> IO [(Bool, a)]
forall a. (a -> Bool) -> State a -> IO [(Bool, a)]
lazy a -> Bool
q' State a
s')
stepF :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepF :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepF a -> Cool
q ((Sched
sc,(Observed a
o:[Observed a]
os)):StateP a
s) = do
let s' :: StateP a
s' = if [Observed a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Observed a]
os then StateP a
s else (Sched
sc,[Observed a]
os)(Sched, [Observed a]) -> StateP a -> StateP a
forall a. a -> [a] -> [a]
:StateP a
s
(IO [Observed a]
ins, a
a) <- Observed a -> IO (IO [Observed a], a)
forall a. Observed a -> IO (IO [Observed a], a)
observed Observed a
o
let (Sched
sc',Bool
b) = Sched -> Cool -> (Sched, Bool)
par Sched
sc (a -> Cool
q a
a)
() <- Bool
b Bool -> IO () -> IO ()
`seq` () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Observed a]
os' <- IO [Observed a]
ins
((Bool, a), StateP a) -> IO ((Bool, a), StateP a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
b, Value a -> a
forall a. Value a -> a
plainV (Observed a -> Value a
forall a. Observed a -> Value a
val Observed a
o)), if [Observed a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Observed a]
os' then StateP a
s' else ((Sched
sc',[Observed a]
os')(Sched, [Observed a]) -> StateP a -> StateP a
forall a. a -> [a] -> [a]
:StateP a
s'))
stepF a -> Cool
_ StateP a
_ = String -> IO ((Bool, a), StateP a)
forall a. HasCallStack => String -> a
error (String -> IO ((Bool, a), StateP a))
-> String -> IO ((Bool, a), StateP a)
forall a b. (a -> b) -> a -> b
$ String
"Invalid state"
searchRawF :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
searchRawF :: Int -> (a -> Cool) -> IO [(Bool, a)]
searchRawF Int
n a -> Cool
q = do
let mo :: Maybe (Observed a)
mo = Minimal a -> Int -> Maybe (Observed a)
forall a. Minimal a -> Int -> Maybe (Observed a)
minimal Minimal a
forall (f :: * -> *) a. (Typeable f, Sized f, Enumerable a) => f a
local Int
n
IO [(Bool, a)]
-> (Observed a -> IO [(Bool, a)])
-> Maybe (Observed a)
-> IO [(Bool, a)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([(Bool, a)] -> IO [(Bool, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (\Observed a
o -> (a -> Cool) -> StateP a -> IO [(Bool, a)]
forall a. (a -> Cool) -> StateP a -> IO [(Bool, a)]
lazy a -> Cool
q [(Sched
sched0, [Observed a
o])]) Maybe (Observed a)
mo
where
lazy :: (a -> Cool) -> StateP a -> IO [(Bool,a)]
lazy :: (a -> Cool) -> StateP a -> IO [(Bool, a)]
lazy a -> Cool
_ [] = [(Bool, a)] -> IO [(Bool, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
lazy a -> Cool
q' StateP a
s = do
((Bool, a)
ba,StateP a
s') <- (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
forall a. (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepF a -> Cool
q' StateP a
s
([(Bool, a)] -> [(Bool, a)]) -> IO [(Bool, a)] -> IO [(Bool, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bool, a)
ba(Bool, a) -> [(Bool, a)] -> [(Bool, a)]
forall a. a -> [a] -> [a]
:) (IO [(Bool, a)] -> IO [(Bool, a)]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [(Bool, a)] -> IO [(Bool, a)])
-> IO [(Bool, a)] -> IO [(Bool, a)]
forall a b. (a -> b) -> a -> b
$ (a -> Cool) -> StateP a -> IO [(Bool, a)]
forall a. (a -> Cool) -> StateP a -> IO [(Bool, a)]
lazy a -> Cool
q' StateP a
s')
stepO :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepO :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepO a -> Cool
q ((Sched
sc,(Observed a
o:[Observed a]
os)):StateP a
s) = do
let s' :: StateP a
s' = if [Observed a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Observed a]
os then StateP a
s else (Sched
sc,[Observed a]
os)(Sched, [Observed a]) -> StateP a -> StateP a
forall a. a -> [a] -> [a]
:StateP a
s
let (Sched
sc', Bool
_) = Sched -> Cool -> (Sched, Bool)
lookahead Sched
sc (a -> Cool
q (Value a -> a
forall a. Value a -> a
plainV (Observed a -> Value a
forall a. Observed a -> Value a
val Observed a
o)))
(IO [Observed a]
ins, a
a) <- Observed a -> IO (IO [Observed a], a)
forall a. Observed a -> IO (IO [Observed a], a)
observed Observed a
o
let b :: Bool
b = Sched -> Cool -> Bool
run Sched
sc' (a -> Cool
q a
a)
() <- Bool
b Bool -> IO () -> IO ()
`seq` () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Observed a]
os' <- IO [Observed a]
ins
((Bool, a), StateP a) -> IO ((Bool, a), StateP a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
b, Value a -> a
forall a. Value a -> a
plainV (Observed a -> Value a
forall a. Observed a -> Value a
val Observed a
o)), if [Observed a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Observed a]
os' then StateP a
s' else ((Sched
sc',[Observed a]
os')(Sched, [Observed a]) -> StateP a -> StateP a
forall a. a -> [a] -> [a]
:StateP a
s'))
stepO a -> Cool
_ StateP a
_ = String -> IO ((Bool, a), StateP a)
forall a. HasCallStack => String -> a
error (String -> IO ((Bool, a), StateP a))
-> String -> IO ((Bool, a), StateP a)
forall a b. (a -> b) -> a -> b
$ String
"Invalid state"
searchRawO :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
searchRawO :: Int -> (a -> Cool) -> IO [(Bool, a)]
searchRawO Int
n a -> Cool
q = do
let mo :: Maybe (Observed a)
mo = Minimal a -> Int -> Maybe (Observed a)
forall a. Minimal a -> Int -> Maybe (Observed a)
minimal Minimal a
forall (f :: * -> *) a. (Typeable f, Sized f, Enumerable a) => f a
local Int
n
IO [(Bool, a)]
-> (Observed a -> IO [(Bool, a)])
-> Maybe (Observed a)
-> IO [(Bool, a)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([(Bool, a)] -> IO [(Bool, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (\Observed a
o -> StateP a -> IO [(Bool, a)]
lazy [(Sched
sched0, [Observed a
o])]) Maybe (Observed a)
mo
where
lazy :: StateP a -> IO [(Bool, a)]
lazy [] = [(Bool, a)] -> IO [(Bool, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
lazy StateP a
s = do
((Bool, a)
ba,StateP a
s') <- (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
forall a. (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepO a -> Cool
q StateP a
s
([(Bool, a)] -> [(Bool, a)]) -> IO [(Bool, a)] -> IO [(Bool, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bool, a)
ba(Bool, a) -> [(Bool, a)] -> [(Bool, a)]
forall a. a -> [a] -> [a]
:) (IO [(Bool, a)] -> IO [(Bool, a)]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [(Bool, a)] -> IO [(Bool, a)])
-> IO [(Bool, a)] -> IO [(Bool, a)]
forall a b. (a -> b) -> a -> b
$ StateP a -> IO [(Bool, a)]
lazy StateP a
s')
stepOF :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepOF :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepOF a -> Cool
q ((Sched
sc,(Observed a
o:[Observed a]
os)):StateP a
s) = do
let s' :: StateP a
s' = if [Observed a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Observed a]
os then StateP a
s else (Sched
sc,[Observed a]
os)(Sched, [Observed a]) -> StateP a -> StateP a
forall a. a -> [a] -> [a]
:StateP a
s
let (Sched
sc', Bool
_) = Sched -> Cool -> (Sched, Bool)
lookahead Sched
sc (a -> Cool
q (Value a -> a
forall a. Value a -> a
plainV (Observed a -> Value a
forall a. Observed a -> Value a
val Observed a
o)))
(IO [Observed a]
ins, a
a) <- Observed a -> IO (IO [Observed a], a)
forall a. Observed a -> IO (IO [Observed a], a)
observed Observed a
o
let (Sched
sc'',Bool
b) = Sched -> Cool -> (Sched, Bool)
par Sched
sc' (a -> Cool
q a
a)
() <- Bool
b Bool -> IO () -> IO ()
`seq` () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Observed a]
os' <- IO [Observed a]
ins
((Bool, a), StateP a) -> IO ((Bool, a), StateP a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
b, Value a -> a
forall a. Value a -> a
plainV (Observed a -> Value a
forall a. Observed a -> Value a
val Observed a
o)), if [Observed a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Observed a]
os' then StateP a
s' else ((Sched
sc'',[Observed a]
os')(Sched, [Observed a]) -> StateP a -> StateP a
forall a. a -> [a] -> [a]
:StateP a
s'))
stepOF a -> Cool
_ StateP a
_ = String -> IO ((Bool, a), StateP a)
forall a. HasCallStack => String -> a
error (String -> IO ((Bool, a), StateP a))
-> String -> IO ((Bool, a), StateP a)
forall a b. (a -> b) -> a -> b
$ String
"Invalid state"
searchRawOF :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
searchRawOF :: Int -> (a -> Cool) -> IO [(Bool, a)]
searchRawOF Int
n a -> Cool
q = do
let mo :: Maybe (Observed a)
mo = Minimal a -> Int -> Maybe (Observed a)
forall a. Minimal a -> Int -> Maybe (Observed a)
minimal Minimal a
forall (f :: * -> *) a. (Typeable f, Sized f, Enumerable a) => f a
local Int
n
IO [(Bool, a)]
-> (Observed a -> IO [(Bool, a)])
-> Maybe (Observed a)
-> IO [(Bool, a)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([(Bool, a)] -> IO [(Bool, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (\Observed a
o -> StateP a -> IO [(Bool, a)]
lazy [(Sched
sched0, [Observed a
o])]) Maybe (Observed a)
mo
where
lazy :: StateP a -> IO [(Bool, a)]
lazy [] = [(Bool, a)] -> IO [(Bool, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
lazy StateP a
s = do
((Bool, a)
ba,StateP a
s') <- (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
forall a. (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepOF a -> Cool
q StateP a
s
([(Bool, a)] -> [(Bool, a)]) -> IO [(Bool, a)] -> IO [(Bool, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bool, a)
ba(Bool, a) -> [(Bool, a)] -> [(Bool, a)]
forall a. a -> [a] -> [a]
:) (IO [(Bool, a)] -> IO [(Bool, a)]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [(Bool, a)] -> IO [(Bool, a)])
-> IO [(Bool, a)] -> IO [(Bool, a)]
forall a b. (a -> b) -> a -> b
$ StateP a -> IO [(Bool, a)]
lazy StateP a
s')
stepOS :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepOS :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepOS a -> Cool
q ((Sched
sc,(Observed a
o:[Observed a]
os)):StateP a
s) = do
let s' :: StateP a
s' = if [Observed a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Observed a]
os then StateP a
s else (Sched
sc,[Observed a]
os)(Sched, [Observed a]) -> StateP a -> StateP a
forall a. a -> [a] -> [a]
:StateP a
s
(IO Int
c,IO [Observed a]
_, a
a1) <- Observed a -> IO (IO Int, IO [Observed a], a)
forall a. Observed a -> IO (IO Int, IO [Observed a], a)
observedc Observed a
o
(Sched
sc', Bool
_) <- IO Int -> Sched -> Cool -> IO (Sched, Bool)
subsetsc IO Int
c Sched
sc (a -> Cool
q a
a1)
(IO [Observed a]
ins, a
a) <- Observed a -> IO (IO [Observed a], a)
forall a. Observed a -> IO (IO [Observed a], a)
observed Observed a
o
let b :: Bool
b = Sched -> Cool -> Bool
run Sched
sc' (a -> Cool
q a
a)
() <- Bool
b Bool -> IO () -> IO ()
`seq` () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Observed a]
os' <- IO [Observed a]
ins
((Bool, a), StateP a) -> IO ((Bool, a), StateP a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
b, Value a -> a
forall a. Value a -> a
plainV (Observed a -> Value a
forall a. Observed a -> Value a
val Observed a
o)), if [Observed a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Observed a]
os' then StateP a
s' else ((Sched
sc',[Observed a]
os')(Sched, [Observed a]) -> StateP a -> StateP a
forall a. a -> [a] -> [a]
:StateP a
s'))
stepOS a -> Cool
_ StateP a
_ = String -> IO ((Bool, a), StateP a)
forall a. HasCallStack => String -> a
error (String -> IO ((Bool, a), StateP a))
-> String -> IO ((Bool, a), StateP a)
forall a b. (a -> b) -> a -> b
$ String
"Invalid state"
searchRawOS :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
searchRawOS :: Int -> (a -> Cool) -> IO [(Bool, a)]
searchRawOS Int
n a -> Cool
q = do
let mo :: Maybe (Observed a)
mo = Minimal a -> Int -> Maybe (Observed a)
forall a. Minimal a -> Int -> Maybe (Observed a)
minimal Minimal a
forall (f :: * -> *) a. (Typeable f, Sized f, Enumerable a) => f a
local Int
n
IO [(Bool, a)]
-> (Observed a -> IO [(Bool, a)])
-> Maybe (Observed a)
-> IO [(Bool, a)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([(Bool, a)] -> IO [(Bool, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (\Observed a
o -> StateP a -> IO [(Bool, a)]
lazy [(Sched
sched0, [Observed a
o])]) Maybe (Observed a)
mo
where
lazy :: StateP a -> IO [(Bool, a)]
lazy [] = [(Bool, a)] -> IO [(Bool, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
lazy StateP a
s = do
((Bool, a)
ba,StateP a
s') <- (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
forall a. (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepOS a -> Cool
q StateP a
s
([(Bool, a)] -> [(Bool, a)]) -> IO [(Bool, a)] -> IO [(Bool, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bool, a)
ba(Bool, a) -> [(Bool, a)] -> [(Bool, a)]
forall a. a -> [a] -> [a]
:) (IO [(Bool, a)] -> IO [(Bool, a)]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [(Bool, a)] -> IO [(Bool, a)])
-> IO [(Bool, a)] -> IO [(Bool, a)]
forall a b. (a -> b) -> a -> b
$ StateP a -> IO [(Bool, a)]
lazy StateP a
s')
stepOSF :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepOSF :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepOSF a -> Cool
q ((Sched
sc,(Observed a
o:[Observed a]
os)):StateP a
s) = do
let s' :: StateP a
s' = if [Observed a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Observed a]
os then StateP a
s else (Sched
sc,[Observed a]
os)(Sched, [Observed a]) -> StateP a -> StateP a
forall a. a -> [a] -> [a]
:StateP a
s
(IO Int
c,IO [Observed a]
_, a
a1) <- Observed a -> IO (IO Int, IO [Observed a], a)
forall a. Observed a -> IO (IO Int, IO [Observed a], a)
observedc Observed a
o
(Sched
sc', Bool
_) <- IO Int -> Sched -> Cool -> IO (Sched, Bool)
subsetsc IO Int
c Sched
sc (a -> Cool
q a
a1)
(IO [Observed a]
ins, a
a) <- Observed a -> IO (IO [Observed a], a)
forall a. Observed a -> IO (IO [Observed a], a)
observed Observed a
o
let (Sched
sc'',Bool
b) = Sched -> Cool -> (Sched, Bool)
par Sched
sc' (a -> Cool
q a
a)
() <- Bool
b Bool -> IO () -> IO ()
`seq` () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[Observed a]
os' <- IO [Observed a]
ins
((Bool, a), StateP a) -> IO ((Bool, a), StateP a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Bool
b, Value a -> a
forall a. Value a -> a
plainV (Observed a -> Value a
forall a. Observed a -> Value a
val Observed a
o)), if [Observed a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Observed a]
os' then StateP a
s' else ((Sched
sc'',[Observed a]
os')(Sched, [Observed a]) -> StateP a -> StateP a
forall a. a -> [a] -> [a]
:StateP a
s'))
stepOSF a -> Cool
_ StateP a
_ = String -> IO ((Bool, a), StateP a)
forall a. HasCallStack => String -> a
error (String -> IO ((Bool, a), StateP a))
-> String -> IO ((Bool, a), StateP a)
forall a b. (a -> b) -> a -> b
$ String
"Invalid state"
searchRawOSF :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
searchRawOSF :: Int -> (a -> Cool) -> IO [(Bool, a)]
searchRawOSF Int
n a -> Cool
q = do
let mo :: Maybe (Observed a)
mo = Minimal a -> Int -> Maybe (Observed a)
forall a. Minimal a -> Int -> Maybe (Observed a)
minimal Minimal a
forall (f :: * -> *) a. (Typeable f, Sized f, Enumerable a) => f a
local Int
n
IO [(Bool, a)]
-> (Observed a -> IO [(Bool, a)])
-> Maybe (Observed a)
-> IO [(Bool, a)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([(Bool, a)] -> IO [(Bool, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (\Observed a
o -> StateP a -> IO [(Bool, a)]
lazy [(Sched
sched0, [Observed a
o])]) Maybe (Observed a)
mo
where
lazy :: StateP a -> IO [(Bool, a)]
lazy [] = [(Bool, a)] -> IO [(Bool, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
lazy StateP a
s = do
((Bool, a)
ba,StateP a
s') <- (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
forall a. (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepOSF a -> Cool
q StateP a
s
([(Bool, a)] -> [(Bool, a)]) -> IO [(Bool, a)] -> IO [(Bool, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Bool, a)
ba(Bool, a) -> [(Bool, a)] -> [(Bool, a)]
forall a. a -> [a] -> [a]
:) (IO [(Bool, a)] -> IO [(Bool, a)]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [(Bool, a)] -> IO [(Bool, a)])
-> IO [(Bool, a)] -> IO [(Bool, a)]
forall a b. (a -> b) -> a -> b
$ StateP a -> IO [(Bool, a)]
lazy StateP a
s')
data Options
=
D
| O
| F
| OF
| OS
| OSF
deriving (Int -> Options -> ShowS
[Options] -> ShowS
Options -> String
(Int -> Options -> ShowS)
-> (Options -> String) -> ([Options] -> ShowS) -> Show Options
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Options] -> ShowS
$cshowList :: [Options] -> ShowS
show :: Options -> String
$cshow :: Options -> String
showsPrec :: Int -> Options -> ShowS
$cshowsPrec :: Int -> Options -> ShowS
Show, ReadPrec [Options]
ReadPrec Options
Int -> ReadS Options
ReadS [Options]
(Int -> ReadS Options)
-> ReadS [Options]
-> ReadPrec Options
-> ReadPrec [Options]
-> Read Options
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Options]
$creadListPrec :: ReadPrec [Options]
readPrec :: ReadPrec Options
$creadPrec :: ReadPrec Options
readList :: ReadS [Options]
$creadList :: ReadS [Options]
readsPrec :: Int -> ReadS Options
$creadsPrec :: Int -> ReadS Options
Read, Options -> Options -> Bool
(Options -> Options -> Bool)
-> (Options -> Options -> Bool) -> Eq Options
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Options -> Options -> Bool
$c/= :: Options -> Options -> Bool
== :: Options -> Options -> Bool
$c== :: Options -> Options -> Bool
Eq, Int -> Options
Options -> Int
Options -> [Options]
Options -> Options
Options -> Options -> [Options]
Options -> Options -> Options -> [Options]
(Options -> Options)
-> (Options -> Options)
-> (Int -> Options)
-> (Options -> Int)
-> (Options -> [Options])
-> (Options -> Options -> [Options])
-> (Options -> Options -> [Options])
-> (Options -> Options -> Options -> [Options])
-> Enum Options
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Options -> Options -> Options -> [Options]
$cenumFromThenTo :: Options -> Options -> Options -> [Options]
enumFromTo :: Options -> Options -> [Options]
$cenumFromTo :: Options -> Options -> [Options]
enumFromThen :: Options -> Options -> [Options]
$cenumFromThen :: Options -> Options -> [Options]
enumFrom :: Options -> [Options]
$cenumFrom :: Options -> [Options]
fromEnum :: Options -> Int
$cfromEnum :: Options -> Int
toEnum :: Int -> Options
$ctoEnum :: Int -> Options
pred :: Options -> Options
$cpred :: Options -> Options
succ :: Options -> Options
$csucc :: Options -> Options
Enum)
defOptions :: Coolean cool => (a -> cool) -> Options
defOptions :: (a -> cool) -> Options
defOptions a -> cool
p | (a -> cool) -> Bool
forall b a. Coolean b => (a -> b) -> Bool
isCool a -> cool
p = Options
OF
defOptions a -> cool
_ = Options
D
searchRaw :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> IO [(Bool,a)]
searchRaw :: Int -> (a -> cool) -> IO [(Bool, a)]
searchRaw Int
n a -> cool
p = Options -> Int -> (a -> cool) -> IO [(Bool, a)]
forall a cool.
(Enumerable a, Coolean cool) =>
Options -> Int -> (a -> cool) -> IO [(Bool, a)]
searchRaw' ((a -> cool) -> Options
forall cool a. Coolean cool => (a -> cool) -> Options
defOptions a -> cool
p) Int
n a -> cool
p
searchRaw' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> IO [(Bool,a)]
searchRaw' :: Options -> Int -> (a -> cool) -> IO [(Bool, a)]
searchRaw' Options
D Int
n a -> cool
p = Int -> (a -> Bool) -> IO [(Bool, a)]
forall a. Enumerable a => Int -> (a -> Bool) -> IO [(Bool, a)]
searchRawD Int
n (cool -> Bool
forall b. Coolean b => b -> Bool
toBool (cool -> Bool) -> (a -> cool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> cool
p)
searchRaw' Options
O Int
n a -> cool
p = Int -> (a -> Cool) -> IO [(Bool, a)]
forall a. Enumerable a => Int -> (a -> Cool) -> IO [(Bool, a)]
searchRawO Int
n (cool -> Cool
forall b. Coolean b => b -> Cool
toCool (cool -> Cool) -> (a -> cool) -> a -> Cool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> cool
p)
searchRaw' Options
F Int
n a -> cool
p = Int -> (a -> Cool) -> IO [(Bool, a)]
forall a. Enumerable a => Int -> (a -> Cool) -> IO [(Bool, a)]
searchRawF Int
n (cool -> Cool
forall b. Coolean b => b -> Cool
toCool (cool -> Cool) -> (a -> cool) -> a -> Cool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> cool
p)
searchRaw' Options
OF Int
n a -> cool
p = Int -> (a -> Cool) -> IO [(Bool, a)]
forall a. Enumerable a => Int -> (a -> Cool) -> IO [(Bool, a)]
searchRawOF Int
n (cool -> Cool
forall b. Coolean b => b -> Cool
toCool (cool -> Cool) -> (a -> cool) -> a -> Cool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> cool
p)
searchRaw' Options
OS Int
n a -> cool
p = Int -> (a -> Cool) -> IO [(Bool, a)]
forall a. Enumerable a => Int -> (a -> Cool) -> IO [(Bool, a)]
searchRawOS Int
n (cool -> Cool
forall b. Coolean b => b -> Cool
toCool (cool -> Cool) -> (a -> cool) -> a -> Cool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> cool
p)
searchRaw' Options
OSF Int
n a -> cool
p = Int -> (a -> Cool) -> IO [(Bool, a)]
forall a. Enumerable a => Int -> (a -> Cool) -> IO [(Bool, a)]
searchRawOSF Int
n (cool -> Cool
forall b. Coolean b => b -> Cool
toCool (cool -> Cool) -> (a -> cool) -> a -> Cool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> cool
p)
search :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> IO [a]
search :: Int -> (a -> cool) -> IO [a]
search Int
n a -> cool
p = Options -> Int -> (a -> cool) -> IO [a]
forall a cool.
(Enumerable a, Coolean cool) =>
Options -> Int -> (a -> cool) -> IO [a]
search' ((a -> cool) -> Options
forall cool a. Coolean cool => (a -> cool) -> Options
defOptions a -> cool
p) Int
n a -> cool
p
search' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> IO [a]
search' :: Options -> Int -> (a -> cool) -> IO [a]
search' Options
o Int
n a -> cool
q = do
[(Bool, a)]
xs <- Options -> Int -> (a -> cool) -> IO [(Bool, a)]
forall a cool.
(Enumerable a, Coolean cool) =>
Options -> Int -> (a -> cool) -> IO [(Bool, a)]
searchRaw' Options
o Int
n a -> cool
q
[a] -> IO [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a
a | (Bool
b,a
a) <- [(Bool, a)]
xs, Bool
b]
sat :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> Bool
sat :: Int -> (a -> cool) -> Bool
sat Int
n a -> cool
p = Options -> Int -> (a -> cool) -> Bool
forall a cool.
(Enumerable a, Coolean cool) =>
Options -> Int -> (a -> cool) -> Bool
sat' ((a -> cool) -> Options
forall cool a. Coolean cool => (a -> cool) -> Options
defOptions a -> cool
p) Int
n a -> cool
p
sat' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> Bool
sat' :: Options -> Int -> (a -> cool) -> Bool
sat' Options
o Int
n a -> cool
q = IO Bool -> Bool
forall a. IO a -> a
unsafePerformIO (([a] -> Bool) -> IO [a] -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool -> Bool
not (Bool -> Bool) -> ([a] -> Bool) -> [a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (Options -> Int -> (a -> cool) -> IO [a]
forall a cool.
(Enumerable a, Coolean cool) =>
Options -> Int -> (a -> cool) -> IO [a]
search' Options
o Int
n a -> cool
q))
usearch :: Enumerable a => Int -> (a -> Bool) -> [a]
usearch :: Int -> (a -> Bool) -> [a]
usearch Int
n a -> Bool
p = Options -> Int -> (a -> Bool) -> [a]
forall a. Enumerable a => Options -> Int -> (a -> Bool) -> [a]
usearch' ((a -> Bool) -> Options
forall cool a. Coolean cool => (a -> cool) -> Options
defOptions a -> Bool
p) Int
n a -> Bool
p
usearch' :: Enumerable a => Options -> Int -> (a -> Bool) -> [a]
usearch' :: Options -> Int -> (a -> Bool) -> [a]
usearch' Options
o Int
n a -> Bool
q = IO [a] -> [a]
forall a. IO a -> a
unsafePerformIO (Options -> Int -> (a -> Bool) -> IO [a]
forall a cool.
(Enumerable a, Coolean cool) =>
Options -> Int -> (a -> cool) -> IO [a]
search' Options
o Int
n a -> Bool
q)
ctrex :: (Coolean cool, Enumerable a) => Int -> (a -> cool) -> IO (Either Integer a)
ctrex :: Int -> (a -> cool) -> IO (Either Integer a)
ctrex Int
n a -> cool
p = Options -> Int -> (a -> cool) -> IO (Either Integer a)
forall cool a.
(Coolean cool, Enumerable a) =>
Options -> Int -> (a -> cool) -> IO (Either Integer a)
ctrex' ((a -> cool) -> Options
forall cool a. Coolean cool => (a -> cool) -> Options
defOptions a -> cool
p) Int
n a -> cool
p
ctrex' :: (Coolean cool, Enumerable a) => Options -> Int -> (a -> cool) -> IO (Either Integer a)
ctrex' :: Options -> Int -> (a -> cool) -> IO (Either Integer a)
ctrex' Options
o Int
n0 a -> cool
q0 = do
let q :: a -> Cool
q = cool -> Cool
forall b. Coolean b => b -> Cool
nott (cool -> Cool) -> (a -> cool) -> a -> Cool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> cool
q0
[(Bool, a)]
xs <- Options -> Int -> (a -> Cool) -> IO [(Bool, a)]
forall a cool.
(Enumerable a, Coolean cool) =>
Options -> Int -> (a -> cool) -> IO [(Bool, a)]
searchRaw' Options
o Int
n0 a -> Cool
q
Either Integer a -> IO (Either Integer a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Bool, a)] -> Integer -> Either Integer a
forall a b. Num a => [(Bool, b)] -> a -> Either a b
go [(Bool, a)]
xs Integer
0)
where go :: [(Bool, b)] -> a -> Either a b
go [] a
n = a -> Either a b
forall a b. a -> Either a b
Left a
n
go ((Bool
b,b
a):[(Bool, b)]
_) a
_ | Bool
b = b -> Either a b
forall a b. b -> Either a b
Right b
a
go ((Bool, b)
_ :[(Bool, b)]
xs') a
n = [(Bool, b)] -> a -> Either a b
go [(Bool, b)]
xs' (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$! (a
na -> a -> a
forall a. Num a => a -> a -> a
+a
1)
countdom :: Enumerable a => (a -> b) -> Count a
countdom :: (a -> b) -> Count a
countdom a -> b
_ = Count a
forall (f :: * -> *) a. (Typeable f, Sized f, Enumerable a) => f a
global
test' :: (Coolean cool, Enumerable a, Show a) => Options -> (a -> cool) -> IO ()
test' :: Options -> (a -> cool) -> IO ()
test' Options
o a -> cool
q = Int -> Integer -> [Integer] -> IO ()
go Int
0 Integer
0 (Count a -> [Integer]
forall a. Count a -> [Integer]
count ((a -> cool) -> Count a
forall a b. Enumerable a => (a -> b) -> Count a
countdom a -> cool
q)) where
go :: Int -> Integer -> [Integer] -> IO ()
go Int
_ Integer
_ [] = String -> IO ()
putStrLn String
"No counterexample found"
go Int
n Integer
acc (Integer
c:[Integer]
cs) = do
let acc' :: Integer
acc' = Integer
acc Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
c
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Testing to size "String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", worst case "String -> ShowS
forall a. [a] -> [a] -> [a]
++Integer -> String
forall a. Show a => a -> String
show Integer
acc'String -> ShowS
forall a. [a] -> [a] -> [a]
++String
" tests"
Either Integer a
e <- Options -> Int -> (a -> cool) -> IO (Either Integer a)
forall cool a.
(Coolean cool, Enumerable a) =>
Options -> Int -> (a -> cool) -> IO (Either Integer a)
ctrex' Options
o Int
n a -> cool
q
case Either Integer a
e of
Left Integer
t -> String -> IO ()
putStrLn (String
"No counterexample found in "String -> ShowS
forall a. [a] -> [a] -> [a]
++Integer -> String
forall a. Show a => a -> String
show Integer
tString -> ShowS
forall a. [a] -> [a] -> [a]
++String
" tests") IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
putStrLn String
"" IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
Int -> Integer -> [Integer] -> IO ()
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Integer
acc' [Integer]
cs
Right a
x -> String -> IO ()
putStrLn String
"Counterexample found:" IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> IO ()
forall a. Show a => a -> IO ()
print a
x
test :: (Coolean cool, Enumerable a, Show a) => (a -> cool) -> IO ()
test :: (a -> cool) -> IO ()
test a -> cool
p = Options -> (a -> cool) -> IO ()
forall cool a.
(Coolean cool, Enumerable a, Show a) =>
Options -> (a -> cool) -> IO ()
test' ((a -> cool) -> Options
forall cool a. Coolean cool => (a -> cool) -> Options
defOptions a -> cool
p) a -> cool
p
testTime :: (Coolean cool, Enumerable a, Show a) => Int -> (a -> cool) -> IO ()
testTime :: Int -> (a -> cool) -> IO ()
testTime Int
t a -> cool
p = Options -> Int -> (a -> cool) -> IO ()
forall cool a.
(Coolean cool, Enumerable a, Show a) =>
Options -> Int -> (a -> cool) -> IO ()
testTime' ((a -> cool) -> Options
forall cool a. Coolean cool => (a -> cool) -> Options
defOptions a -> cool
p) Int
t a -> cool
p
testTime' :: (Coolean cool, Enumerable a, Show a) => Options -> Int -> (a -> cool) -> IO ()
testTime' :: Options -> Int -> (a -> cool) -> IO ()
testTime' Options
o Int
t a -> cool
p = do
Maybe ()
mu <- Int -> IO () -> IO (Maybe ())
forall a. Int -> IO a -> IO (Maybe a)
timeout (Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
1000000) (Options -> (a -> cool) -> IO ()
forall cool a.
(Coolean cool, Enumerable a, Show a) =>
Options -> (a -> cool) -> IO ()
test' Options
o a -> cool
p)
case Maybe ()
mu of Maybe ()
Nothing -> String -> IO ()
putStrLn String
"Timed out"
Just{} -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()