lazy-search (empty) → 0.1.0.0
raw patch · 5 files changed
+969/−0 lines, 5 filesdep +basedep +size-basedsetup-changed
Dependencies added: base, size-based
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- lazy-search.cabal +24/−0
- src/Control/Search.hs +573/−0
- src/Data/Coolean.hs +340/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2016, Jonas Duregard + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Jonas Duregard nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple +main = defaultMain
+ lazy-search.cabal view
@@ -0,0 +1,24 @@+-- Initial lazy-search.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: lazy-search +version: 0.1.0.0 +synopsis: Finds values satisfying a lazy predicate +-- description: +license: BSD3 +license-file: LICENSE +author: Jonas Duregard +maintainer: jonas.duregard@chalmers.se +-- copyright: +category: Testing +build-type: Simple +-- extra-source-files: +cabal-version: >=1.10 + +library + exposed-modules: Data.Coolean, Control.Search + -- other-modules: + -- other-extensions: + build-depends: base >=4.8 && <4.9, size-based >=0.1 && <0.2 + hs-source-dirs: src + default-language: Haskell2010
+ src/Control/Search.hs view
@@ -0,0 +1,573 @@+{-#LANGUAGE GADTs, DeriveDataTypeable, DeriveFunctor #-} + +-- | Efficient size-based search for values satisfying/falsifying a lazy boolean predicate. See "Control.Enumerable" for defining enumerations of data types. +module Control.Search + ( + -- * Searching + search, sat, searchRaw, usearch + -- * Testing properties + , test, testTime + -- * Options for parallel conjunction + , Options (..) + , sat', search', searchRaw', test' + -- * Deep embedded boolean type + , Cool(..) + , Coolean + , (&&&), (|||), (==>), nott, true, false + -- * Re-exported + , module Control.Enumerable + ) where + +import Data.IORef +import Control.Sized +import Control.Enumerable + +import Data.Bits +import System.IO.Unsafe + +import Control.Enumerable.Count +import Control.Enumerable.Values + +import Data.List ( partition ) + +import Data.Coolean + +import System.Timeout + +import Data.List ( nub, (\\) ) -- Just for testing +import Data.List ( minimumBy ) -- Just for testing +-- import Test.QuickCheck (quickCheck) + + +newCounter :: IO (IO Int) +newCounter = do + ref <- newIORef 0 + return (atomicModifyIORef ref (\i -> (i+1,i))) + +attach :: (IO Int) -> a -> IO (IO Int, a) +attach c a = do + ref <- newIORef (-1) + return (readIORef ref, unsafePerformIO $ c >>= writeIORef ref >> return 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 + +instance Show a => Show (Value a) where + show v = "("++ repV v ++ ", " ++ show (plainV v) ++ ")" + +instance Functor Value where + fmap = mkMap + + +repV :: Value a -> String +repV (Unit _) = "1" +repV (Pair _ a b) = "("++ repV a ++ ", " ++ repV b ++ ")" +repV (Alt _ a _) = "?"++ repV a +repV (Map _ _ v) = "$"++ repV v + +plainV :: Value a -> a +plainV (Pair a _ _) = a +plainV (Map a _ _) = a +plainV (Unit a) = a +plainV (Alt a _ _) = a + +mkPair :: Value a -> Value b -> Value (a,b) +mkPair (Unit a) (Unit b) = Unit (a,b) +mkPair (Unit a) v = mkMap ((,) a) v +mkPair v (Unit b) = mkMap (\a -> (a,b)) v +mkPair v1 v2 = Pair (plainV v1,plainV v2) v1 v2 + +mkAlt :: Value a -> Minimal a -> Value a +mkAlt v s = Alt (plainV v) v s + +mkMap :: (a -> b) -> Value a -> Value b +mkMap f (Unit a) = Unit (f a) +mkMap f (Map a g v) = Map (f a) (f . g) v +mkMap f v = Map (f (plainV v)) f 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 f (Pay s) = Pay (fmap f s) + fmap f (Value v) = Value (fmap f v) + fmap _ Empty = Empty + +instance Applicative Minimal where + pure a = Value (Unit a) + sf <*> sa = fmap (uncurry ($)) (pair sf sa) + +instance Alternative Minimal where + empty = Empty + Empty <|> s = s + s <|> Empty = s + Pay a <|> Pay b = Pay (a <|> b) + Value vf <|> s = Value (mkAlt vf s) + a <|> Value vf = Value (mkAlt vf a) + +instance Sized Minimal where + pay = Pay + pair Empty _ = Empty + pair _ Empty = Empty + pair (Pay a) b = Pay (pair a b) + pair a (Pay b) = Pay (pair a b) + pair (Value f) (Value g) = Value (mkPair f g) + + aconcat [] = empty + aconcat [s] = s + aconcat [s1,s2] = s1 <|> s2 + aconcat ss = case extr ss of + ([],m) -> maybe Empty Value m + (ss',m) -> maybe (pay (aconcat ss')) (Value . (`mkAlt` (aconcat ss'))) m + where + extr :: [Minimal a] -> ([Minimal a], Maybe (Value a)) + extr (s:ss) = case s of + Value v -> (ss,Just v) + Empty -> extr ss + Pay s' -> case extr ss of + (ss',Nothing) -> (s':ss',Nothing) + (ss',j) -> (s:ss', j) + + +data Observed a = Observed { sizeLeft :: Int, val :: Value a } deriving Functor +instance Show a => Show (Observed a) where + show = show . val + + +minimal :: Minimal a -> Int -> Maybe (Observed a) +minimal _ n | n < 0 = Nothing +minimal Empty _ = Nothing +minimal (Pay s) n = minimal s (n-1) +minimal (Value vf) n = Just (Observed n vf) + + + + +data Relevant a = Relevant + { -- | The order in which this choice was made + evalOrder :: Int, + -- | The result of fixing this and all earlier choices + fixed :: Value a, + -- | The result of swapping this and fixing earlier choices + swapped :: Observed a + } + +r << q = evalOrder r < evalOrder q + +merge :: Value a -> Value b -> [Relevant a] -> [Relevant b] -> [Relevant (a,b)] +merge va vb [] r = rsmap (mkPair va) r +merge va vb r [] = rsmap (`mkPair` vb) r +merge va vb rs@(r:rs') qs@(q:qs') + | q << r = rmap (va `mkPair`) q : merge va (fixed q) rs qs' + | otherwise = rmap (`mkPair` vb) r : merge (fixed r) vb rs' qs + +-- Alter a Relevant choice by altering both the swapped and fixed value +rmap :: (Value a -> Value b) -> Relevant a -> Relevant b +rmap f r = r{fixed = f (fixed r), swapped = omap f (swapped r)} where + omap f o' = o'{val = f (val o')} + +rsmap f = map (rmap f) + + +observed :: Observed a -> IO (IO [Observed a], a) +observed o = do + c <- newCounter + let go :: Value a -> IO (IO [Relevant a], a) + go (Pair _ va vb) = do + (rs, xa) <- go va + (qs, xb) <- go vb + return (liftA2 (merge va vb) rs qs, (xa,xb)) + go (Map _ f v) = do + ~(x,a) <- (go v) + return (fmap (rsmap (fmap f)) x,f a) + go (Unit a) = return (return [], a) + go (Alt _ v x) = do + ~(tr,a) <- go v + (i, a') <- attach c a + return (tralt tr i, a') + where + tralt tr i = i >>= \n -> case n of + -1 -> return [] + _ -> case minimal x (sizeLeft o) of + Just nv -> fmap (Relevant n v nv :) tr + Nothing -> tr + fmap (\(a,b) -> (fmap fx a, b)) $ go (val o) where + fx :: [Relevant a] -> [Observed a] + fx rs = reverse (map swapped rs) + +observedc :: Observed a -> IO (IO Int, IO [Observed a], a) +observedc o = do + ref <- newIORef 0 + let c = atomicModifyIORef ref (\i -> (i+1,i)) + let go :: Value a -> IO (IO [Relevant a], a) + go (Pair _ va vb) = do + (rs, xa) <- go va + (qs, xb) <- go vb + return (liftA2 (merge va vb) rs qs, (xa,xb)) + go (Map _ f v) = do + ~(x,a) <- (go v) + return (fmap (rsmap (fmap f)) x,f a) + go (Unit a) = return (return [], a) + go (Alt _ v x) = do + ~(tr,a) <- go v + (i, a') <- attach c a + return (tralt tr i, a') + where + tralt tr i = i >>= \n -> case n of + -1 -> return [] + _ -> case minimal x (sizeLeft o) of + Just nv -> fmap (Relevant n v nv :) tr + Nothing -> tr + fmap (\(a,b) -> (readIORef ref, fmap fx a, b)) $ go (val o) where + fx :: [Relevant a] -> [Observed a] + fx rs = reverse (map swapped rs) + + + + + + + + +type State a = [[Observed a]] +type StateP a = [(Sched, [Observed a])] + + +-- Sequential search +{-#INLINE stepQ #-} +stepQ :: (a -> Bool) -> State a -> IO ((Bool, a), State a) +stepQ q ((o:os):s) = do + let s' = if null os then s else os:s -- Pick a value from the stack + (ins, a) <- observed o -- Get an observable copy + let b = q a + () <- b `seq` return () + os' <- ins -- Swap all choices + return ((b, plainV (val o)), if null os' then s' else os':s') +stepQ q s = error $ "Invalid state" + + +searchRawQ :: Enumerable a => Int -> (a -> Bool) -> IO [(Bool,a)] +searchRawQ n q = do + let mo = minimal local n + maybe (return []) (\o -> lazy q [[o]]) mo + where + lazy :: (a -> Bool) -> State a -> IO [(Bool,a)] + lazy q [] = return [] + lazy q s = do + (ba,s') <- stepQ q s + fmap (ba:) (unsafeInterleaveIO $ lazy q s') + +-- Fair Parallel conjunction +stepP :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a) +stepP 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 (sc',b) = par sc (q a) + () <- b `seq` return () + os' <- ins -- Swap all choices + return ((b, plainV (val o)), if null os' then s' else ((sc',os'):s')) +stepP q s = error $ "Invalid state" + + +searchRawP :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)] +searchRawP n q = do + let mo = minimal local n + maybe (return []) (\o -> lazyP q [(sched0, [o])]) mo + where + lazyP :: (a -> Cool) -> StateP a -> IO [(Bool,a)] + lazyP q [] = return [] + lazyP q s = do + (ba,s') <- stepP q s + fmap (ba:) (unsafeInterleaveIO $ lazyP q s') + + + +-- Short-circuiting sequential search +stepS :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a) +stepS q ((sc,(o:os)):s) = do + let s' = if null os then s else (sc,os):s -- Pick a value from the stack + + let (sc', _) = lookahead sc (q (plainV (val o))) + + (ins, a) <- observed o -- Get an observable copy + let b = run sc' (q a) + + () <- b `seq` return () + os' <- ins -- Swap all choices + return ((b, plainV (val o)), if null os' then s' else ((sc',os'):s')) +stepS q s = error $ "Invalid state" + +searchRawS :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)] +searchRawS n q = do + let mo = minimal local n + maybe (return []) (\o -> lazy [(sched0, [o])]) mo + where + -- lazy :: StateP a -> IO [(Bool,a)] + lazy [] = return [] + lazy s = do + (ba,s') <- stepS q s + fmap (ba:) (unsafeInterleaveIO $ lazy s') + + + + + +-- Short-circuiting parallel search +stepSP :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a) +stepSP q ((sc,(o:os)):s) = do + let s' = if null os then s else (sc,os):s -- Pick a value from the stack + + let (sc', _) = lookahead sc (q (plainV (val o))) + (ins, a) <- observed o -- Get an observable copy + let (sc'',b) = par sc' (q a) + () <- b `seq` return () + os' <- ins -- Swap all choices + return ((b, plainV (val o)), if null os' then s' else ((sc'',os'):s')) +stepSP q s = error $ "Invalid state" + +searchRawSP :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)] +searchRawSP n q = do + let mo = minimal local n + maybe (return []) (\o -> lazy [(sched0, [o])]) mo + where + -- lazy :: StateP a -> IO [(Bool,a)] + lazy [] = return [] + lazy s = do + (ba,s') <- stepSP q s + fmap (ba:) (unsafeInterleaveIO $ lazy s') + +-- Subset-minimize +stepT :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a) +stepT q ((sc,(o:os)):s) = do + let s' = if null os then s else (sc,os):s -- Pick a value from the stack + + (c,ins, a1) <- observedc o -- Get an observable copy + (sc', _) <- subsetsc c sc (q a1) + + (ins, a) <- observed o -- Get an observable copy + let b = run sc' (q a) + + () <- b `seq` return () + os' <- ins -- Swap all choices + return ((b, plainV (val o)), if null os' then s' else ((sc',os'):s')) + + +stepT q s = error $ "Invalid state" + +searchRawT :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)] +searchRawT n q = do + let mo = minimal local n + maybe (return []) (\o -> lazy [(sched0, [o])]) mo + where + lazy [] = return [] + lazy s = do + (ba,s') <- stepT q s + fmap (ba:) (unsafeInterleaveIO $ lazy s') + + +-- T + parallel +stepTP :: (a -> Cool) -> StateP a -> IO ((Bool, a), StateP a) +stepTP q ((sc,(o:os)):s) = do + let s' = if null os then s else (sc,os):s -- Pick a value from the stack + + + (c,ins, a1) <- observedc o -- Get an observable copy + (sc', _) <- subsetsc c sc (q a1) + + (ins, a) <- observed o -- Get an observable copy + let (sc'',b) = par sc' (q a) + + () <- b `seq` return () + os' <- ins -- Swap all choices + return ((b, plainV (val o)), if null os' then s' else ((sc'',os'):s')) +stepTP q s = error $ "Invalid state" + +searchRawTP :: Enumerable a => Int -> (a -> Cool) -> IO [(Bool,a)] +searchRawTP n q = do + let mo = minimal local n + maybe (return []) (\o -> lazy [(sched0, [o])]) mo + where + lazy [] = return [] + lazy s = do + (ba,s') <- stepTP q s + fmap (ba:) (unsafeInterleaveIO $ lazy 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 +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 (Show, Read, Eq, Enum) + +defOptions p | isCool p = OF +defOptions p = D + +-- | Lazily finds all values isomorphic to p (w.r.t. laziness) and returns them along with the result of p. +searchRaw :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> IO [(Bool,a)] +searchRaw n p = searchRaw' (defOptions p) n p + +searchRaw' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> IO [(Bool,a)] +searchRaw' D n p = searchRawQ n (toBool . p) +searchRaw' O n p = searchRawS n (toCool . p) +searchRaw' F n p = searchRawP n (toCool . p) +searchRaw' OF n p = searchRawSP n (toCool . p) +searchRaw' OS n p = searchRawT n (toCool . p) +searchRaw' OSF n p = searchRawTP n (toCool . p) + +-- | Lazily finds all values of or below a given size that satisfies this predicate. +search :: (Enumerable a, Coolean cool) => Int -> (a -> cool) -> IO [a] +search n p = search' (defOptions p) n p + +search' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> IO [a] +search' o n q = do + xs <- searchRaw' o n q + return [a | (b,a) <- xs, 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 n p = sat' (defOptions p) n p + +sat' :: (Enumerable a, Coolean cool) => Options -> Int -> (a -> cool) -> Bool +sat' o n q = unsafePerformIO (fmap (not . null) (search' o n q)) + +-- | Unsafe search, the order in which values are found is non-deterministic for some predicates. +usearch :: Enumerable a => Int -> (a -> Bool) -> [a] +usearch n p = usearch' (defOptions p) n p + +usearch' :: Enumerable a => Options -> Int -> (a -> Bool) -> [a] +usearch' o n q = unsafePerformIO (search' o n q) + +-- sat' :: Enumerable a => Int -> (a -> Bool) -> Bool +-- sat' n q = unsafePerformIO (fmap (not . null) (search' n q)) + + + +ctrex' :: (Coolean cool, Enumerable a) => Options -> Int -> (a -> cool) -> IO (Either Integer a) +ctrex' o n q0 = do + let q = nott . q0 + xs <- searchRaw' o n q + return (go xs 0) + where go [] n = Left n + go ((b,a):_) n | b = Right a + go (_ :xs') n = go xs' (n+1) + +-- Count the domain of a function +countdom :: Enumerable a => (a -> b) -> Count a +countdom f = global + +test' :: (Coolean cool, Enumerable a, Show a) => Options -> (a -> cool) -> IO () +test' 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 $ "Testing to size "++ show n ++ ", worst case "++show acc'++" tests" + e <- ctrex' o n q + case e of + Left t -> putStrLn ("No counterexample found in "++show t++" tests") >> putStrLn "" >> + go (n+1) acc' cs + Right x -> putStrLn "Counterexample found:" >> print x + +-- | SmallCheck-like test driver. Tests a property with gradually increasing sizes until a conunterexample is found. +test :: (Coolean cool, Enumerable a, Show a) => (a -> cool) -> IO () +test p = test' (defOptions p) p + + +-- | Stop testing after a given number of seconds +testTime :: (Coolean cool, Enumerable a, Show a) => Int -> (a -> cool) -> IO () +testTime t p = do + mu <- timeout (t*1000000) (test p) + case mu of Nothing -> putStrLn "Timed out" + Just x -> 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' SP n p + case xs of + [] -> return Nothing + (x:_) -> return (Just (show x)) + +-}
+ src/Data/Coolean.hs view
@@ -0,0 +1,340 @@+ +-- | Proper documentation is TBD +module Data.Coolean where + +import Control.Exception +import Data.IORef +import System.IO.Unsafe + +-- import Data.Tree + +-- | Concurrent booleans. Writing properties with the Cool data type often yields faster searches compared to Bool. +data Cool = Atom Bool + | Not Cool + | And Cool Cool + -- | Sequential conjunction, the second operator is not evaluated unless the first is true. + | Seq Cool Cool + deriving Show + +-- Class based construction +true, false :: Cool +true = Atom True +false = Atom False + + +(&&&) :: (Coolean a, Coolean b) => a -> b -> Cool +a &&& b = toCool a <&> toCool b + +infixr 2 &&& + +(|||) :: (Coolean a, Coolean b) => a -> b -> Cool +a ||| b = toCool a <||> toCool b + +nott :: Coolean a => a -> Cool +nott a = Not (toCool a) + +(==>) :: (Coolean a, Coolean b) => a -> b -> Cool +a ==> b = Not (toCool a <&> Not (toCool b)) + +-- Sequential operators +(!=>) :: (Coolean a, Coolean b) => a -> b -> Cool +a !=> b = Not (toCool a `Seq` Not (toCool b)) + +(!&&) :: (Coolean a, Coolean b) => a -> b -> Cool +a !&& b = toCool a `Seq` toCool b + +(!||) :: (Coolean a, Coolean b) => a -> b -> Cool +a !|| b = Not (Not (toCool a) `Seq` Not (toCool b)) + + +-- | Provides better interoperability between Bool and Cool by overloading operators. +class Coolean b where + toCool :: b -> Cool + toBool :: b -> Bool + isCool :: (a -> b) -> Bool + +instance Coolean Cool where + toCool = id + toBool (And a b) = toBool a && toBool b + toBool (Seq a b) = toBool a && toBool b + toBool (Not a) = not (toBool a) + toBool (Atom a) = a + isCool _ = True + +instance Coolean Bool where + toCool = Atom + toBool = id + isCool _ = False + + +-- Explicit construction +(<&>) :: Cool -> Cool -> Cool +(<&>) = And + +(<&) :: Bool -> Cool -> Cool +a <& b = Atom a <&> b + +(&>) :: Cool -> Bool -> Cool +a &> b = a <&> Atom b + +(&) :: Bool -> Bool -> Cool +a & b = Atom a <&> Atom b + + +a <||> b = Not (Not a <&> Not b) + + +-- Consumers +data Sched = Flip Bool Sched Sched +-- | Fixed + | Unsched + deriving (Show, Eq) + +-- instance Show Sched where show = drawTree . toTree + +split :: Sched -> Sched +split Unsched = Flip False Unsched Unsched +split s = s + +sched0 = Unsched + +-- toTree :: Sched -> Tree String +-- toTree Unsched = Node "*" [] +-- toTree (Flip b s1 s2) = Node (show b) [toTree s1, toTree s2] + + +-- Run the given schedule +run :: Sched -> Cool -> Bool +run (Unsched) c = toBool c +run s@(Flip b s1 s2) c = case c of + Atom b -> b + Not c -> not (run s c) + Seq c1 c2 -> run s1 c1 && run s2 c2 + And c1 c2 + | b -> run s2 c2 && run s1 c1 + | otherwise -> run s1 c1 && run s2 c2 + + +-- Returns a schedule with optimal short-circuiting behaviour +lookahead :: Sched -> Cool -> (Sched, Bool) +lookahead s c = case c of + Atom b -> (s,b) + Not c -> fmap not (lookahead s c) + Seq c1 c2 -> go (lookahead s1 c1) (lookahead s2 c2) + where + (Flip b s1 s2) = split s + go (s1',r1) ~(s2',r2) = case r1 of + True -> case r2 of + True -> (Flip False s1' s2', True) -- Set to unflipped if True + False -> (Flip True s1 s2', False) + False -> (Flip b s1' s2, False) + + -- (Flip b s1' s2', r1 && r2) + -- where (s1', r1) = lookahead s1 c1 + -- (s2', r2) = lookahead s2 c2 + -- (Flip b s1 s2) = split s + And c1 c2 + | b -> go (\b' -> flip (Flip b')) (lookahead s2 c2) (lookahead s1 c1) + | otherwise -> go (\b' -> Flip b') (lookahead s1 c1) (lookahead s2 c2) + where + (Flip b s1 s2) = split s + go flp (s1',r1) ~(s2',r2) = case r1 of + True -> case r2 of + True -> (flp False s1' s2', True) -- Set to unflipped if True + False -> (flp (not b) s1 s2', False) + False -> (flp b s1' s2, False) + + + + +-- Flip all evaluated parallel conjunctions +par :: Sched -> Cool -> (Sched, Bool) +par s c = case c of + Atom b -> (s,b) + Not c -> fmap not (par s c) + Seq c1 c2 -- -> (Flip b s1' s2', r1 && r2) + | b -> go (\b' -> flip (Flip b')) (par s2 c2) (par s1 c1) + | otherwise -> go (\b' -> Flip b') (par s1 c1) (par s2 c2) + where + (Flip b s1 s2) = split s + go flp (s1',r1) ~(s2',r2) = case r1 of + True -> case r2 of + True -> (flp b s1' s2', True) -- Flip here? + False -> (flp b s1 s2', False) + False -> (flp b s1' s2, False) + And c1 c2 + | b -> go (\b' -> flip (Flip b')) (par s2 c2) (par s1 c1) + | otherwise -> go (\b' -> Flip b') (par s1 c1) (par s2 c2) + where + (Flip b s1 s2) = split s + go flp (s1',r1) ~(s2',r2) = case r1 of + True -> case r2 of + True -> (flp (False) s1' s2', True) -- Flip here? + False -> (flp (not b) s1 s2', False) + False -> (flp (not b) s1' s2, False) + + + + +-- Returns a schedule with optimal short-circuiting behaviour and +-- giving preference to choice-subset operands +subsetsc :: IO Int -> Sched -> Cool -> IO (Sched, Bool) +subsetsc io s0 c0 = go s0 c0 where + go s c = case c of + Atom b -> return (s,b) + Not c' -> fmap (fmap not) (go s c') + Seq c1 c2 -> do + (s1', r1) <- go s1 c1 + (s2', r2) <- go s2 c2 + return (Flip b s1' s2', r1 && r2) + where (Flip b s1 s2) = split s + And c1 c2 + | b -> go' (\b' -> flip (Flip b')) (go s2 c2) (go s1 c1) + | otherwise -> go' (\b' -> Flip b') (go s1 c1) (go s2 c2) + where +-- unchanged s1' s2' | b = Flip + (Flip b s1 s2) = split s + go' flp m1 m2 = do + (s1',r1) <- m1 + case r1 of + True -> do + (s2',r2) <- m2 + case r2 of + True -> return (flp False s1' s2', True) -- Set to unflipped if True + False -> return (flp (not b) s1 s2', False) + False -> do + n <- io + (s2',r2) <- m2 + + case r2 of + True -> return (flp b s1' s2, False) + False -> do + n' <- io + if (n' > n) -- The other operand made at least one distinct choice + then return (flp b s1' s2, False) + else return (flp (not b) s1 s2', False) + +-- measure :: IO Int -> Sched -> Cool + +{- + +runInterl :: Cool -> Bool +runInterl = unRes . interl + +data Res = Now Bool | Later Res +unRes :: Res -> Bool +unRes (Now b) = b +unRes (Later x) = unRes x + + +interl :: Cool -> Res +interl (Not c) = Later (interl c) -- Negating consumes an action +interl (And c1 c2) = mer (interl c1) (interl c2) where +{- mer :: Res -> Res -> Res + mer r1 r2 = case r1 of + Now False -> Now False + Now True -> r2 + Later r1' -> Later (mer r2 r1') -} + mer :: Res -> Res -> Res + mer (Now False) _ = Now False + mer _ (Now False) = Now False + mer (Now True) (Now True) = Now True + mer (Later r1') (Later r2') = Later (mer r1' r2') +interl (Atom b) = Now b +interl (Seq c1 c2) = seqi (interl c1) (interl c2) where + seqi (Now False) r2 = Now False + seqi (Now True) r2 = r2 + seqi (Later r1') r2 = Later (seqi r1' r2) + + +prune :: Cool -> Cool -> (Bool,Cool) +prune (Atom a) c2 = (a, c2) +prune (Not c1) ~(Not d1) = case prune c1 d1 of (b,c) -> (not b, Not c) +prune (And c1 c2) ~(And d1 d2) = case prune c1 d1 of + (False, p) -> (False, p) + (True, p) -> case prune c2 d2 of + (False, q) -> (False, q) + (True, q) -> (True, Seq p q) +prune (Seq c1 c2) ~(Seq d1 d2) = case prune c1 d1 of + (False, p) -> case prune c2 d2 of + (False, q) -> (False, And p q) + (True, q) -> (False, p) + (True, p) -> case prune c2 d2 of + (False, q) -> (False, q) + (True, q) -> (True, Seq p q) + + + +-- Check that the schedule is optimal +rerun :: Sched -> Cool -> Maybe Bool +rerun Unsched c = Just (toBool c) -- Should only be Not and Atom +rerun s@(Flip b s1 s2) c = case c of + Atom b -> Just b + Not c -> fmap not (rerun s c) + Seq c1 c2 -> rerun s1 c1 && run s2 c2 + And c1 c2 + | b -> rerun s2 c2 &&&& rerun s1 c1 + | otherwise -> rerun s1 c1 &&&& rerun s2 c2 + where + Just False &&&& _ = Just False + Just True &&&& Just True = Just True + _ &&&& _ = Nothing +-} + + +{- +lazify :: Cool -> Cool -> (Bool, Bool) +lazify (Atom a) ~(Atom x) = (a,x) +lazify (Not a) ~(Not x) = case lazify a x of (b1,b2) -> (not b1, not b2) +lazify (And a b) ~(And x y) + = case lazify a x of + (False, p) -> (False, p) + (True, p) -> case lazify b y of + (False, q) -> (False, q) + (True, q) -> (True, p && q) + +coolio :: Cool -> Cool -> Cool -> (Bool, Bool, Bool) +coolio (Atom a) ~(Atom x) ~(Atom p) = (a,x,p) +coolio (And a b) ~(And x y) ~(And p q) + = case coolio a x p of + (False, rx, rp) -> (False, rx, rp) + (True, rx, rp) -> case coolio b y q of + (False, ry, rq) -> (False, ry, rq) + (True, ry, rq) -> (True, rx && ry, rp && rq) + + + +data UnCool = UnCool deriving (Show,Read) +instance Exception UnCool + +unCool :: a -> IO (IO Bool, a) +unCool a = do + r <- newIORef False + let toggle = atomicModifyIORef r (\b -> (not b, b)) + a' = unsafeDupablePerformIO $ do + b <- readIORef r + print b + if b then return a else throw UnCool + + return (toggle, a') + + +-- unCool :: a + +isCool :: Bool -> Bool +isCool b = unsafeDupablePerformIO $ do + catch (b `seq` return True) (\UnCool -> return False) + + +test = do + (tog,a) <- unCool 1 + let x = Just a + catch (x == Just 1 `seq` print True) (\UnCool -> print "Cool") + tog -- >>= print + catch (x == Just 1 `seq` print True) (\UnCool -> print "Not Cool") + + +-} + + +-- uncool