mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-20 03:51:39 +03:00
Factor out the utility list functions to a separate module
This commit is contained in:
parent
d7e30e87ba
commit
69fdd561d9
@ -8,6 +8,7 @@ module Control.Monad.Conc.Fixed.Internal where
|
|||||||
import Control.DeepSeq (NFData(..))
|
import Control.DeepSeq (NFData(..))
|
||||||
import Control.Monad (liftM, mapAndUnzipM)
|
import Control.Monad (liftM, mapAndUnzipM)
|
||||||
import Control.Monad.Cont (Cont, runCont)
|
import Control.Monad.Cont (Cont, runCont)
|
||||||
|
import Data.List.Extra
|
||||||
import Data.Map (Map)
|
import Data.Map (Map)
|
||||||
import Data.Maybe (catMaybes, fromJust, isNothing)
|
import Data.Maybe (catMaybes, fromJust, isNothing)
|
||||||
|
|
||||||
@ -37,21 +38,6 @@ data Fixed c n r t = F
|
|||||||
-- type.
|
-- type.
|
||||||
}
|
}
|
||||||
|
|
||||||
-- * Non-Empty Lists
|
|
||||||
|
|
||||||
-- | The type of non-empty lists.
|
|
||||||
data NonEmpty a = a :| [a] deriving (Eq, Ord, Read, Show)
|
|
||||||
|
|
||||||
instance Functor NonEmpty where
|
|
||||||
fmap f (a :| as) = f a :| map f as
|
|
||||||
|
|
||||||
instance NFData a => NFData (NonEmpty a) where
|
|
||||||
rnf (x:|xs) = rnf (x, xs)
|
|
||||||
|
|
||||||
-- | Convert a 'NonEmpty' to a regular non-empty list.
|
|
||||||
toList :: NonEmpty a -> [a]
|
|
||||||
toList (a :| as) = a : as
|
|
||||||
|
|
||||||
-- * Running @Conc@ Computations
|
-- * Running @Conc@ Computations
|
||||||
|
|
||||||
-- | Scheduling is done in terms of a trace of 'Action's. Blocking can
|
-- | Scheduling is done in terms of a trace of 'Action's. Blocking can
|
||||||
|
@ -16,6 +16,7 @@ module Control.Monad.Conc.Fixed.Schedulers
|
|||||||
) where
|
) where
|
||||||
|
|
||||||
import Control.Monad.Conc.Fixed.Internal
|
import Control.Monad.Conc.Fixed.Internal
|
||||||
|
import Data.List.Extra
|
||||||
import System.Random (RandomGen, randomR)
|
import System.Random (RandomGen, randomR)
|
||||||
|
|
||||||
-- | A simple random scheduler which, at every step, picks a random
|
-- | A simple random scheduler which, at every step, picks a random
|
||||||
|
@ -7,6 +7,7 @@ module Control.Monad.Conc.SCT.Bounding where
|
|||||||
import Control.DeepSeq (NFData(..), force)
|
import Control.DeepSeq (NFData(..), force)
|
||||||
import Control.Monad.Conc.Fixed
|
import Control.Monad.Conc.Fixed
|
||||||
import Control.Monad.Conc.SCT.Internal
|
import Control.Monad.Conc.SCT.Internal
|
||||||
|
import Data.List.Extra
|
||||||
|
|
||||||
import qualified Control.Monad.Conc.Fixed.IO as CIO
|
import qualified Control.Monad.Conc.Fixed.IO as CIO
|
||||||
|
|
||||||
@ -83,16 +84,6 @@ sctBoundedIO siblings offspring b = runSCTIO' prefixSched (initialS, initialG) b
|
|||||||
|
|
||||||
-- * State
|
-- * State
|
||||||
|
|
||||||
-- | Data type representing a lazy, chunky, tagged, stream of data.
|
|
||||||
data Lazy t a = Lazy (t, NonEmpty a) (Lazy t a) | Empty t
|
|
||||||
|
|
||||||
-- | Prepend a value onto a lazy stream.
|
|
||||||
(+|) :: (t, [a]) -> Lazy t a -> Lazy t a
|
|
||||||
(_, []) +| l = l
|
|
||||||
(t, x:xs) +| l = Lazy (t, x:|xs) l
|
|
||||||
|
|
||||||
infixr +|
|
|
||||||
|
|
||||||
-- | State for the prefix scheduler.
|
-- | State for the prefix scheduler.
|
||||||
data Sched = S
|
data Sched = S
|
||||||
{ _decisions :: [Decision]
|
{ _decisions :: [Decision]
|
||||||
@ -106,7 +97,7 @@ instance NFData Sched where
|
|||||||
|
|
||||||
-- | State for the bounded runner.
|
-- | State for the bounded runner.
|
||||||
data State = P
|
data State = P
|
||||||
{ _next :: Lazy Int [Decision]
|
{ _next :: Stream Int [Decision]
|
||||||
-- ^ Schedules to try.
|
-- ^ Schedules to try.
|
||||||
, _halt :: Bool
|
, _halt :: Bool
|
||||||
-- ^ Indicates more schedules couldn't be found, and to halt
|
-- ^ Indicates more schedules couldn't be found, and to halt
|
||||||
@ -159,7 +150,7 @@ bStep :: (SCTTrace -> [[Decision]])
|
|||||||
-> (Sched, State) -> SCTTrace -> (Sched, State)
|
-> (Sched, State) -> SCTTrace -> (Sched, State)
|
||||||
bStep siblings offspring blim (s, g) t = case _next g of
|
bStep siblings offspring blim (s, g) t = case _next g of
|
||||||
-- We have schedules remaining, so run the next
|
-- We have schedules remaining, so run the next
|
||||||
Lazy (b, x:|xs) rest
|
Stream (b, x:|xs) rest
|
||||||
| b /= blim -> (s' x, g { _next = (b+1, next) +| (b, this) +| (b, xs) +| rest })
|
| b /= blim -> (s' x, g { _next = (b+1, next) +| (b, this) +| (b, xs) +| rest })
|
||||||
| otherwise -> (s' x, g { _next = (b, this) +| (b, xs) +| rest })
|
| otherwise -> (s' x, g { _next = (b, this) +| (b, xs) +| rest })
|
||||||
|
|
||||||
@ -184,7 +175,7 @@ bStep siblings offspring blim (s, g) t = case _next g of
|
|||||||
_ -> halt
|
_ -> halt
|
||||||
|
|
||||||
where
|
where
|
||||||
(pref, suff) = let ((Start 0,_,_):px, sx) = splitAt (_prefixlen s + 1) t in ((map (\(d,_,_) -> d) px ++), sx)
|
(pref, suff) = splitAtF (\((Start 0,_,_):px) -> (map (\(d,_,_) -> d) px ++)) id (_prefixlen s + 1) t
|
||||||
|
|
||||||
-- | New scheduler state, with a given list of initial decisions.
|
-- | New scheduler state, with a given list of initial decisions.
|
||||||
s' ds = initialS { _decisions = ds, _prefixlen = length ds }
|
s' ds = initialS { _decisions = ds, _prefixlen = length ds }
|
||||||
|
@ -34,6 +34,7 @@ import Control.Monad (when, void)
|
|||||||
import Control.Monad.Conc.Fixed
|
import Control.Monad.Conc.Fixed
|
||||||
import Control.Monad.Conc.SCT.Internal
|
import Control.Monad.Conc.SCT.Internal
|
||||||
import Control.Monad.Conc.SCT.Bounding
|
import Control.Monad.Conc.SCT.Bounding
|
||||||
|
import Data.List.Extra
|
||||||
import Data.Maybe (isJust, isNothing)
|
import Data.Maybe (isJust, isNothing)
|
||||||
|
|
||||||
import qualified Control.Monad.Conc.Fixed.IO as CIO
|
import qualified Control.Monad.Conc.Fixed.IO as CIO
|
||||||
@ -84,19 +85,6 @@ simplify ts = map (\t -> (pref, drop plen $ take (length t - slen) t, suff)) ts
|
|||||||
suff = commonSuffix ts
|
suff = commonSuffix ts
|
||||||
slen = length suff
|
slen = length suff
|
||||||
|
|
||||||
-- | Common prefix of a bunch of lists
|
|
||||||
commonPrefix = foldl1 commonPrefix2
|
|
||||||
|
|
||||||
-- | Common suffix of a bunch of lists
|
|
||||||
commonSuffix = reverse . commonPrefix . map reverse
|
|
||||||
|
|
||||||
-- | Common prefix of two lists
|
|
||||||
commonPrefix2 [] _ = []
|
|
||||||
commonPrefix2 _ [] = []
|
|
||||||
commonPrefix2 (x:xs) (y:ys)
|
|
||||||
| x == y = x : commonPrefix2 xs ys
|
|
||||||
| otherwise = []
|
|
||||||
|
|
||||||
-- | Pretty-print a simplified trace
|
-- | Pretty-print a simplified trace
|
||||||
showtrc :: (SCTTrace, SCTTrace, SCTTrace) -> String
|
showtrc :: (SCTTrace, SCTTrace, SCTTrace) -> String
|
||||||
showtrc (p, t, s) = case (p, s) of
|
showtrc (p, t, s) = case (p, s) of
|
||||||
|
54
Data/List/Extra.hs
Executable file
54
Data/List/Extra.hs
Executable file
@ -0,0 +1,54 @@
|
|||||||
|
-- | Extra list functions and list-like types.
|
||||||
|
module Data.List.Extra where
|
||||||
|
|
||||||
|
import Control.DeepSeq (NFData(..))
|
||||||
|
|
||||||
|
-- * Regular lists
|
||||||
|
|
||||||
|
-- | Split a list at an index and transform the two halves.
|
||||||
|
splitAtF :: ([a] -> b) -> ([a] -> c) -> Int -> [a] -> (b, c)
|
||||||
|
splitAtF f g i xs = let (l, r) = splitAt i xs in (f l, g r)
|
||||||
|
|
||||||
|
-- | Get the longest common prefix of a bunch of lists.
|
||||||
|
commonPrefix :: Eq a => [[a]] -> [a]
|
||||||
|
commonPrefix [] = []
|
||||||
|
commonPrefix ls = foldl1 commonPrefix2 ls where
|
||||||
|
commonPrefix2 [] _ = []
|
||||||
|
commonPrefix2 _ [] = []
|
||||||
|
commonPrefix2 (x:xs) (y:ys)
|
||||||
|
| x == y = x : commonPrefix2 xs ys
|
||||||
|
| otherwise = []
|
||||||
|
|
||||||
|
-- | Get the longest common suffix of a bunch of lists.
|
||||||
|
commonSuffix :: Eq a => [[a]] -> [a]
|
||||||
|
commonSuffix = reverse . commonPrefix . map reverse
|
||||||
|
|
||||||
|
-- * Non-empty lists
|
||||||
|
-- | This gets exposed to users of the library, so it has a bunch of
|
||||||
|
-- classes which aren't actually used in the rest of the code to make
|
||||||
|
-- it more friendly to further use.
|
||||||
|
|
||||||
|
-- | The type of non-empty lists.
|
||||||
|
data NonEmpty a = a :| [a] deriving (Eq, Ord, Read, Show)
|
||||||
|
|
||||||
|
instance Functor NonEmpty where
|
||||||
|
fmap f (a :| as) = f a :| map f as
|
||||||
|
|
||||||
|
instance NFData a => NFData (NonEmpty a) where
|
||||||
|
rnf (x:|xs) = rnf (x, xs)
|
||||||
|
|
||||||
|
-- | Convert a 'NonEmpty' to a regular non-empty list.
|
||||||
|
toList :: NonEmpty a -> [a]
|
||||||
|
toList (a :| as) = a : as
|
||||||
|
|
||||||
|
-- * Tagged streams
|
||||||
|
|
||||||
|
-- | Data type representing a chunky, tagged, stream of data.
|
||||||
|
data Stream t a = Stream (t, NonEmpty a) (Stream t a) | Empty t
|
||||||
|
|
||||||
|
-- | Prepend a value onto a lazy stream.
|
||||||
|
(+|) :: (t, [a]) -> Stream t a -> Stream t a
|
||||||
|
(_, []) +| l = l
|
||||||
|
(t, x:xs) +| l = Stream (t, x:|xs) l
|
||||||
|
|
||||||
|
infixr +|
|
@ -54,6 +54,7 @@ library
|
|||||||
other-modules: Control.Monad.Conc.Fixed.Internal
|
other-modules: Control.Monad.Conc.Fixed.Internal
|
||||||
, Control.Monad.Conc.SCT.Bounding
|
, Control.Monad.Conc.SCT.Bounding
|
||||||
, Control.Monad.Conc.SCT.Internal
|
, Control.Monad.Conc.SCT.Internal
|
||||||
|
, Data.List.Extra
|
||||||
-- other-extensions:
|
-- other-extensions:
|
||||||
build-depends: base >=4.6 && <5
|
build-depends: base >=4.6 && <5
|
||||||
, containers
|
, containers
|
||||||
|
Loading…
Reference in New Issue
Block a user