Skip to content

Commit 11ac801

Browse files
committed
monad-stm: MonadFix instance
1 parent a51ee3d commit 11ac801

File tree

3 files changed

+61
-14
lines changed

3 files changed

+61
-14
lines changed

io-sim/src/Control/Monad/IOSim/Internal.hs

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1008,6 +1008,19 @@ execAtomically !time !tid !tlbl !nextVid0 action0 k0 =
10081008
trace <- go ctl read written writtenSeq createdSeq nextVid k
10091009
return $ SimTrace time tid tlbl (EventLog x) trace
10101010

1011+
LiftSTStm st k ->
1012+
{-# SCC "schedule.LiftSTStm" #-} do
1013+
x <- strictToLazyST st
1014+
go ctl read written writtenSeq createdSeq nextVid (k x)
1015+
1016+
FixStm f k ->
1017+
{-# SCC "execAtomically.go.FixStm" #-} do
1018+
r <- newSTRef (throw NonTermination)
1019+
x <- unsafeInterleaveST $ readSTRef r
1020+
let k' = unSTM (f x) $ \x' ->
1021+
LiftSTStm (lazyToStrictST (writeSTRef r x')) (\() -> k x')
1022+
go ctl read written writtenSeq createdSeq nextVid k'
1023+
10111024
where
10121025
localInvariant =
10131026
Map.keysSet written

io-sim/src/Control/Monad/IOSim/Types.hs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -205,6 +205,9 @@ data StmA s a where
205205
-> (Maybe a -> a -> ST s TraceValue)
206206
-> StmA s b -> StmA s b
207207

208+
LiftSTStm :: StrictST.ST s a -> (a -> StmA s b) -> StmA s b
209+
FixStm :: (x -> STM s x) -> (x -> StmA s r) -> StmA s r
210+
208211
-- Exported type
209212
type STMSim = STM
210213

@@ -297,6 +300,9 @@ instance Alternative (STM s) where
297300

298301
instance MonadPlus (STM s) where
299302

303+
instance MonadFix (STM s) where
304+
mfix f = STM $ oneShot $ \k -> FixStm f k
305+
300306
instance MonadSay (IOSim s) where
301307
say msg = IOSim $ oneShot $ \k -> Say msg (k ())
302308

io-sim/test/Test/IOSim.hs

Lines changed: 42 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -139,12 +139,18 @@ tests =
139139
[ testProperty "Reference vs IO" prop_stm_referenceIO
140140
, testProperty "Reference vs Sim" prop_stm_referenceSim
141141
]
142-
, testGroup "MonadFix instance"
143-
[ testProperty "purity" prop_mfix_purity
144-
, testProperty "purity2" prop_mfix_purity_2
145-
, testProperty "tightening" prop_mfix_left_shrinking
146-
, testProperty "lazy" prop_mfix_lazy
147-
, testProperty "recdata" prop_mfix_recdata
142+
, testGroup "MonadFix instances"
143+
[ testGroup "IOSim"
144+
[ testProperty "purity" prop_mfix_purity_IOSim
145+
, testProperty "purity2" prop_mfix_purity_2
146+
, testProperty "tightening" prop_mfix_left_shrinking_IOSim
147+
, testProperty "lazy" prop_mfix_lazy
148+
, testProperty "recdata" prop_mfix_recdata
149+
]
150+
, testGroup "STM"
151+
[ testProperty "purity" prop_mfix_purity_STM
152+
, testProperty "tightening" prop_mfix_left_shrinking_STM
153+
]
148154
]
149155
-- NOTE: Most of the tests below only work because the io-sim
150156
-- scheduler works the way it does.
@@ -592,15 +598,18 @@ test_wakeup_order = do
592598

593599
-- | Purity demands that @mfix (return . f) = return (fix f)@.
594600
--
595-
prop_mfix_purity :: Positive Int -> Bool
596-
prop_mfix_purity (Positive n) =
597-
runSimOrThrow
598-
(mfix (return . factorial)) n
599-
== fix factorial n
601+
prop_mfix_purity_m :: forall m. MonadFix m => Positive Int -> m Bool
602+
prop_mfix_purity_m (Positive n) =
603+
(== fix factorial n) . ($ n) <$> mfix (return . factorial)
600604
where
601605
factorial :: (Int -> Int) -> Int -> Int
602606
factorial = \rec_ k -> if k <= 1 then 1 else k * rec_ (k - 1)
603607

608+
prop_mfix_purity_IOSim :: Positive Int -> Bool
609+
prop_mfix_purity_IOSim a = runSimOrThrow $ prop_mfix_purity_m a
610+
611+
prop_mfix_purity_STM:: Positive Int -> Bool
612+
prop_mfix_purity_STM a = runSimOrThrow $ atomically $ prop_mfix_purity_m a
604613

605614
prop_mfix_purity_2 :: [Positive Int] -> Bool
606615
prop_mfix_purity_2 as =
@@ -634,12 +643,12 @@ prop_mfix_purity_2 as =
634643
(realToFrac `map` as')
635644

636645

637-
prop_mfix_left_shrinking
646+
prop_mfix_left_shrinking_IOSim
638647
:: Int
639648
-> NonNegative Int
640649
-> Positive Int
641650
-> Bool
642-
prop_mfix_left_shrinking n (NonNegative d) (Positive i) =
651+
prop_mfix_left_shrinking_IOSim n (NonNegative d) (Positive i) =
643652
let mn :: IOSim s Int
644653
mn = do say ""
645654
threadDelay (realToFrac d)
@@ -657,6 +666,25 @@ prop_mfix_left_shrinking n (NonNegative d) (Positive i) =
657666
threadDelay (realToFrac d) $> a : rec_)))
658667

659668

669+
prop_mfix_left_shrinking_STM
670+
:: Int
671+
-> Positive Int
672+
-> Bool
673+
prop_mfix_left_shrinking_STM n (Positive i) =
674+
let mn :: STMSim s Int
675+
mn = do say ""
676+
return n
677+
in
678+
take i
679+
(runSimOrThrow $ atomically $
680+
mfix (\rec_ -> mn >>= \a -> return $ a : rec_))
681+
==
682+
take i
683+
(runSimOrThrow $ atomically $
684+
mn >>= \a ->
685+
(mfix (\rec_ -> return $ a : rec_)))
686+
687+
660688

661689
-- | 'Example 8.2.1' in 'Value Recursion in Monadic Computations'
662690
-- <https://leventerkok.github.io/papers/erkok-thesis.pdf>
@@ -756,7 +784,7 @@ probeOutput probe x = atomically (modifyTVar probe (x:))
756784

757785

758786
--
759-
-- Syncronous exceptions
787+
-- Synchronous exceptions
760788
--
761789

762790
unit_catch_0, unit_catch_1, unit_catch_2, unit_catch_3, unit_catch_4,

0 commit comments

Comments
 (0)