{-#LANGUAGE GADTs, DeriveDataTypeable, DeriveFunctor #-}

-- | Efficient size-based search for values satisfying/falsifying a lazy boolean predicate. 

-- Predicates are typically of type @a -> Bool@, although an alternative boolean type called 'Cool' is provided and using it may give faster searches. 

--

-- See "Control.Enumerable" for defining default enumerations of data types (required for searching). 

module Control.Search 
  ( 
  -- * Searching 

  search, sat, ctrex, searchRaw, usearch
  -- * Testing properties

  , test, testTime
  -- * Options for parallel conjunction

  , Options (..)
  , sat', search', ctrex', searchRaw', test', testTime'
  -- * Deep embedded boolean type

  , (&&&), (|||), (==>), nott, true, false 
  , Cool(..)
  , Coolean
  -- * Re-exported

  , 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
  -- A value that can potentially be replaced by a larger value

  Alt  :: a -> Value a -> Minimal a -> Value a
  
  -- StrictAlt :: a -> Value a -> (Int -> [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 -- ADT

  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 
  {  -- | The order in which this choice was made

     Relevant a -> Int
evalOrder  :: Int,  
     -- | The result of fixing this and all earlier choices

     Relevant a -> Value a
fixed      :: Value a,
     -- | The result of swapping this and fixing earlier choices

     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

-- Alter a Relevant choice by altering both the swapped and fixed value

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])]


-- Sequential search

{-#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  -- Pick a value from the stack

  (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                -- Get an observable copy

  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                            -- Swap all choices

  ((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')

-- Fair Parallel conjunction

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  -- Pick a value from the stack

  (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                     -- Get an observable copy

  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                                 -- Swap all choices

  ((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')



-- Short-circuiting sequential search

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  -- Pick a value from the stack

  
  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                     -- Get an observable copy

  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                                 -- Swap all choices

  ((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 :: 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')





-- Short-circuiting parallel search

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  -- Pick a value from the stack

  
  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                     -- Get an observable copy

  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                                 -- Swap all choices

  ((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 :: 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')

-- Subset-minimize

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  -- Pick a value from the stack

  
  (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                 -- Get an observable copy

  (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                     -- Get an observable copy

  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                                 -- Swap all choices

  ((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')


-- OS + parallel

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  -- Pick a value from the stack

  
  
  (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                 -- Get an observable copy

  (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                     -- Get an observable copy

  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                                 -- Swap all choices

  ((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')


{-
stepI :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a)
stepI q ((sc,(o:os)):s) = do
  let s' = if null os then s else (sc,os):s  -- Pick a value from the stack

  (ins, a) <- observed o                     -- Get an observable copy
  
  let c = prune (q (plainV (val o))) (q a)
  
  let b = runInterl (snd c)
  
  () <- b `seq` return ()
  os' <- ins                                 -- Swap all choices
  return ((b, plainV (val o)), if null os' then s' else ((sc,os'):s'))
stepI q s               = error $ "Invalid state"

searchRawI :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)]
searchRawI n q = do
  let mo = minimal local n
  maybe (return []) (\o -> lazy [(sched0, [o])]) mo
  where
    lazy [] = return []
    lazy s = do
      (ba,s') <- stepI q s
      fmap (ba:) (unsafeInterleaveIO $ lazy s')
-}

-- | Options for parallel conjunction strategies. Only matters for 

-- predicates using the @Cool@ data type instead of Bool.

data Options 
  = 
    -- | Sequential

    D    
    -- | Optimal Short-circuiting

  | O
    -- | Parallel (fair)

  | F
    -- | Optimal Short-circuiting and fairness

  | OF
    -- | Optimal Short-circuiting and choice-subset detection

  | OS    
    -- | Subset choice short-circuiting

  | 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

-- | Lazily finds all non-isomorphic (w.r.t. laziness) inputs to a 

-- predicate and returns them along with the result of the predicate. 

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)

-- | Lazily finds all (non-isomorphic) values of or below a given size that satisfy a predicate. 

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]

-- | Is there a value of or below a given size that satisfies this predicate?

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))

-- | Unsafe version of search. Non-deterministic for some predicates. 

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)


-- | Find a counterexample to the given predicate, of or below a given size. 

-- If no counterexample is found, the number of performed executions of the predicate is returned. 

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)
 
-- Count the domain of a function

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

-- | SmallCheck-like test driver. Tests a property with gradually increasing sizes until a conunterexample is found. For each size, it shows the worst case number of tests required 

-- (if the predicate is fully eager).

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


-- | Stop testing after a given number of seconds

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 ()

{-
testall :: (Coolean cool, Enumerable a, Show a) => Options -> (a -> cool) -> IO ()
testall o q = go 0 0 (count (countdom q)) where
  go n _   []     = putStrLn "No counterexample found"
  go n acc (c:cs) = do
    let acc' = acc + c 
    putStrLn $ show n ++ " ("++show acc'++")" 
    t <- fmap length (searchRaw' o n q)
    print t
    go (n+1) acc' cs



-- Testing framework
data Pred where 
  Pred :: (Enumerable a, Show a) => (a -> Cool) -> Pred

class Predicate p where
  predicate :: p -> Pred
  puncurry  :: (Enumerable a, Show a) => (a -> p) -> Pred

instance (Predicate b, Enumerable a, Show a) => Predicate (a -> b) where
  predicate = puncurry
  puncurry f = predicate (uncurry f)

instance Predicate Cool where
  predicate x = Pred (\() -> x)
  puncurry    = Pred


testN :: Predicate p => Int -> p -> IO (Maybe String)
testN n p = case predicate p of Pred x -> testN' n x

testN' :: (Show a, Enumerable a) => Int -> (a -> Cool) -> IO (Maybe String)
testN' n p = do
  xs <- search' OF n p
  case xs of
    []    -> return Nothing
    (x:_) -> return (Just (show x))

-}