rec-def 0.1 → 0.2
raw patch · 26 files changed
+1391/−916 lines, 26 filesdep ~doctestdep ~tasty-dejafu
Dependency ranges changed: doctest, tasty-dejafu
Files
- CHANGELOG.md +9/−0
- Data/POrder.hs +27/−12
- Data/Propagator/Class.hs +22/−0
- Data/Propagator/Naive.hs +157/−0
- Data/Propagator/P2.hs +116/−0
- Data/Propagator/Purify.hs +110/−0
- Data/Recursive/Bool.hs +66/−59
- Data/Recursive/DualBool.hs +70/−46
- Data/Recursive/Examples.hs +71/−63
- Data/Recursive/Internal.hs +32/−0
- Data/Recursive/Map.hs +190/−0
- Data/Recursive/Propagator/Class.hs +0/−55
- Data/Recursive/Propagator/Naive.hs +0/−110
- Data/Recursive/Propagator/P2.hs +0/−101
- Data/Recursive/R.hs +0/−8
- Data/Recursive/R/Internal.hs +0/−113
- Data/Recursive/Set.hs +86/−48
- README.md +5/−4
- System/IO/RecThunk.hs +12/−12
- dejafu.hs +0/−203
- doctests.hs +0/−2
- examples.hs +71/−63
- rec-def.cabal +31/−17
- tests/dejafu.hs +203/−0
- tests/doctests.hs +8/−0
- tests/spaceleak.hs +105/−0
CHANGELOG.md view
@@ -1,5 +1,14 @@ # Revision history for rec-def +## 0.2 -- 2022-09-22++* The naive propagator does not use `(==)` to detect changes, but a custom+ operator, to allow faster and less restricted operators.+* Module structure refactoring+* No more `R` type constructor, instead individual `RBool` etc. types+* Addition of `Data.Recursive.Map`+* A space leak is fixed+ ## 0.1 -- 2022-09-03 * First version. Released on an unsuspecting world.
Data/POrder.hs view
@@ -7,24 +7,35 @@ import Data.Coerce import qualified Data.Set as S import Numeric.Natural+import Data.Function --- | This (empty) class indicates that the type @a@ is partially ordered.--- The class is empty because we do not need any of the operations on runtime.+-- | This class indicates that the type @a@ is partially ordered by some relation ⊑.+--+-- The class does not actually have a method for ⊑, because we do not need it at runtime. -- Nevertheless the order better exists for the safety of this API. -- -- This order may be unrelated to the total order given by 'Ord'.-class Eq a => POrder a+class POrder a where+ -- | The `eqOfLe` method checks _related_ elements for equality.+ --+ -- Formally: For all @x ⊑ y@, @eqOfLe x y == True@ iff @x == y@.+ --+ -- This can be more efficient than testing for equality. For example for+ -- sets, '(==)' needs to compare the elements, but @eqOfLe@ only needs to+ -- compare sizes. It is always ok to use '(==)' here.+ eqOfLe :: a -> a -> Bool --- | A class indicating that the type @a@ is partially ordered and has a bottom+-- | A class indicating that the type @a@ is has a bottom -- element.-class POrder a => Bottom a where bottom :: a+class Bottom a where bottom :: a --- | A class indicating that the type @a@ is partially ordered and has a top+-- | A class indicating that the type @a@ is has a top -- element. class POrder a => Top a where top :: a -- | The dual order-instance POrder a => POrder (Dual a)+instance POrder a => POrder (Dual a) where+ eqOfLe (Dual x) (Dual y) = eqOfLe y x -- | Bottom is the 'top' of @a@ instance Top a => Bottom (Dual a) where bottom = Dual top@@ -32,7 +43,7 @@ -- Annoyingly, we have to give all instances here, to avoid orphans -- | Arbitrary using the @False < True@ order-instance POrder Bool+instance POrder Bool where eqOfLe = (==) -- | Bottom is 'False' instance Bottom Bool where bottom = False@@ -41,19 +52,23 @@ instance Top Bool where top = True -- | Ordered by 'S.subsetOf'-instance Eq a => POrder (S.Set a)+instance POrder (S.Set a) where eqOfLe = (==) `on` S.size -- | Bottom is 'S.empty'-instance Eq a => Bottom (S.Set a) where bottom = S.empty+instance Bottom (S.Set a) where bottom = S.empty -- | Ordered by '(<=)f'-instance POrder Natural+instance POrder Natural where eqOfLe = (==) -- | Bottom is 0 instance Bottom Natural where bottom = 0 -- | Adds 'Nothing' as a least element to an existing partial order-instance POrder a => POrder (Maybe a)+instance POrder a => POrder (Maybe a) where+ eqOfLe Nothing Nothing = True+ eqOfLe Nothing (Just _) = False+ eqOfLe (Just x) (Just y) = eqOfLe x y+ eqOfLe (Just _) Nothing = error "eqOfLe/Maybe used with unrelated arguments" -- | Bottom is 'Nothing' instance POrder a => Bottom (Maybe a) where bottom = Nothing
+ Data/Propagator/Class.hs view
@@ -0,0 +1,22 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FunctionalDependencies #-}++-- | This module provides the 'Propagator' class+module Data.Propagator.Class where++import Control.Exception++-- | The Propagator class defines some functions shared by different propagator+-- implementations. This backs the generic "Data.Propagator.Purify" wrapper.+class Propagator p x | p -> x where+ newProp :: IO p+ newConstProp :: x -> IO p+ freezeProp :: p -> IO ()+ readProp :: p -> IO x++data WriteToFrozenPropagatorException = WriteToFrozenPropagatorException+ deriving Show+instance Exception WriteToFrozenPropagatorException
+ Data/Propagator/Naive.hs view
@@ -0,0 +1,157 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}++-- | A very naive propagator library.+--+-- This propagator implementation keeps updating the values accoring to their+-- definitions as other values change, until a fixed-point is reached.+--+-- It is a naive implementation and not very clever. Much more efficient+-- propagator implementations are possible, and may be used by this library in+-- the future.+module Data.Propagator.Naive+ ( Prop+ , newProp+ , newConstProp+ , freezeProp+ , readProp+ , watchProp+ , setProp+ , lift1+ , lift2+ , liftList+ )+ where++import Control.Monad+import Data.POrder+import Data.Maybe++import qualified Data.Propagator.Class as Class++-- I want to test this code with dejafu, without carrying it as a dependency+-- of the main library. So here is a bit of CPP to care for that.++#ifdef DEJAFU++#define Ctxt MonadConc m =>+#define Prop_ Prop m+#define IORef_ IORef m+#define MVar_ MVar m+#define M m++import Control.Concurrent.Classy++#else++#define Ctxt+#define Prop_ Prop+#define IORef_ IORef+#define MVar_ MVar+#define M IO++import Control.Exception+import Control.Concurrent.MVar+import Data.IORef++#endif++-- | A cell in a propagator network+data Prop_ a = Prop+ { val :: IORef_ a+ , lock :: MVar_ ()+ , onChange :: IORef_ (Maybe (M ()))+ }++-- | Creates a cell, initialized to bottom+newProp :: Ctxt a -> M (Prop_ a)+newProp x = do+ m <- newIORef x+ l <- newMVar ()+ notify <- newIORef (Just (pure ()))+ pure $ Prop m l notify++-- | Creates a constant cell, given an initial value+newConstProp :: Ctxt a -> M (Prop_ a)+newConstProp x = do+ m <- newIORef x+ l <- newMVar ()+ notify <- newIORef Nothing+ pure $ Prop m l notify++-- | Reads the current value of the cell+readProp :: Ctxt Prop_ a -> M a+readProp (Prop m _ _ ) = readIORef m++-- | Is the current propagator already frozen?+isFrozen :: Ctxt Prop_ a -> M Bool+isFrozen (Prop _ _ notify) = do+ isNothing <$> readIORef notify++-- | Marks the propagator as frozen.+--+-- Will prevent further calls to setProp and clears the list of watchers (to+-- allow GC).+freezeProp :: Ctxt Prop_ a -> M ()+freezeProp (Prop _ _ notify) = do+ writeIORef notify Nothing++-- | Sets a new value calculated from the given action. The action is executed atomically.+--+-- Throws if the propagator is already frozen+--+-- If the value has changed, all watchers are notified afterwards (not atomically).+setProp :: Ctxt POrder a => Prop_ a -> M a -> M ()+setProp p@(Prop m l notify) getX = do+ frozen <- isFrozen p+ when frozen $ throw Class.WriteToFrozenPropagatorException+ () <- takeMVar l+ old <- readIORef m+ new <- getX+ writeIORef m new+ putMVar l ()+ unless (old `eqOfLe` new) $+ readIORef notify >>= \case+ Nothing -> pure ()+ Just act -> act++-- | Watch a cell: If the value changes, the given action is executed+watchProp :: Ctxt Prop_ a -> M () -> M ()+watchProp (Prop _ _ notify) f =+ atomicModifyIORef notify $ \case+ Nothing -> (Nothing, ())+ Just a -> (Just (f >> a), ())++-- | Whenever the first cell changes, update the second, using the given function+lift1 :: Ctxt POrder b => (a -> b) -> Prop_ a -> Prop_ b -> M ()+lift1 f p1 p = do+ let update = setProp p $ f <$> readProp p1+ watchProp p1 update+ update++-- | Whenever any of the first two cells change, update the third, using the given function+lift2 :: Ctxt POrder c => (a -> b -> c) -> Prop_ a -> Prop_ b -> Prop_ c -> M ()+lift2 f p1 p2 p = do+ let update = setProp p $ f <$> readProp p1 <*> readProp p2+ watchProp p1 update+ watchProp p2 update+ update++-- | Whenever any of the cells in the list change, update the other, using the given function+liftList :: Ctxt POrder b => ([a] -> b) -> [Prop_ a] -> Prop_ b -> M ()+liftList f ps p = do+ let update = setProp p $ f <$> mapM readProp ps+ mapM_ (\p' -> watchProp p' update) ps+ update++#ifndef DEJAFU+instance Bottom a => Class.Propagator (Prop_ a) a where+ newProp = newProp bottom+ newConstProp = newConstProp+ freezeProp = freezeProp+ readProp = readProp+#endif
+ Data/Propagator/P2.hs view
@@ -0,0 +1,116 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE CPP #-}++-- | A propagator for the two-point lattice+--+module Data.Propagator.P2+ ( P2+ , newP2+ , newTopP2+ , setTop+ , whenTop+ , implies+ , isTop+ )+ where++import Data.Propagator.Class++-- I want to test this code with dejafu, without carrying it as a dependency+-- of the main library. So here is a bit of CPP to care for that.++#ifdef DEJAFU++#define Ctxt MonadConc m =>+#define MaybeTop_ (MaybeTop m)+#define P2_ (P2 m)+#define PBool_ PBool m+#define PDualBool_ PDualBool m+#define IORef_ IORef m+#define MVar_ MVar m+#define M m++import Control.Concurrent.Classy++#else++#define Ctxt+#define MaybeTop_ MaybeTop+#define P2_ P2+#define PBool_ PBool+#define PDualBool_ PDualBool+#define IORef_ IORef+#define MVar_ MVar+#define M IO++import Control.Exception+import Control.Concurrent.MVar+import Data.IORef++#endif++data MaybeTop_+ = StillBottom (M ()) -- ^ Just act: Still bottom, run act (once!) when triggered+ | SurelyBottom -- ^ Definitely bottom + | SurelyTop -- ^ Definitely top++-- | A type for propagators for the two-point lattice, consisting of bottom and top+newtype P2_ = P2 (MVar_ MaybeTop_)++-- | A new propagator, initialized at bottom+newP2 :: Ctxt M P2_+newP2 = P2 <$> newMVar (StillBottom (pure()))++-- | A new propagator, already set to top+newTopP2 :: Ctxt M P2_+newTopP2 = P2 <$> newMVar SurelyTop++-- | @whenTop p act@ runs @act@ if @p@ is already top, or after @setTop p@ is run+whenTop :: Ctxt P2_ -> M () -> M ()+whenTop (P2 p1) act = takeMVar p1 >>= \case+ SurelyTop -> putMVar p1 SurelyTop >> act+ SurelyBottom -> putMVar p1 SurelyBottom+ StillBottom act' -> putMVar p1 (StillBottom (act >> act'))+++-- | Set a propagator to top.+--+-- If it was bottom before, runs the actions queued with 'whenTop'. It does so+-- /after/ setting the propagator to top, so that cycles are broken.+setTop :: Ctxt P2_ -> M ()+setTop (P2 p) = takeMVar p >>= \case+ SurelyTop -> putMVar p SurelyTop+ SurelyBottom -> throw WriteToFrozenPropagatorException+ StillBottom act -> do+ -- Do this first, this breaks cycles+ putMVar p SurelyTop+ -- Now notify the dependencies+ act++-- | @p1 `implies` p2@ chains propagators: If @p1@ becomes top, then so does @p2@.+implies :: Ctxt P2_ -> P2_ -> M ()+implies p1 p2 = whenTop p1 (setTop p2)++-- | Queries the current state of the propagator. All related calls to @setTop@+-- that have executed so far are taken into account.+isTop :: Ctxt P2_ -> M Bool+isTop (P2 p) = readMVar p >>= \case+ SurelyTop -> pure True+ SurelyBottom -> pure False+ StillBottom _ -> pure False++-- | Freezes the value. Drops references to watchers.+freeze :: Ctxt P2_ -> M ()+freeze (P2 p) = takeMVar p >>= \case+ SurelyTop -> putMVar p SurelyTop+ _ -> putMVar p SurelyBottom++#ifndef DEJAFU+instance Propagator P2_ Bool where+ newProp = newP2+ newConstProp False = newP2+ newConstProp True = newTopP2+ freezeProp = freeze+ readProp = isTop+#endif
+ Data/Propagator/Purify.hs view
@@ -0,0 +1,110 @@+{-# OPTIONS_HADDOCK not-home #-}++{-# LANGUAGE GADTs #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE AllowAmbiguousTypes #-}++-- |+--+-- This module provides the 'Purify' data type, which wraps a imperative propagator+-- (for example "Data.Propagator.Naive") in a pure data structure.+--+-- It provides functions to declare the inputs to these propagators, which are unsafe on their own, but can be instantiated and wrapped to form safe APIs, e.g. "Data.Recursive.Bool".+--+-- This module is labeled as Internal because its safety depends on the behaviour of the+-- underlying propagator implementation. The assumptions is that+--+-- * The defining function passed to `def1` etc. declare a functional relation+-- between the input propagators and the output propagator.+-- * Defining functions do not (observably) affect their input propagators.+-- * Once all the functions passed to `def1` of a propagator and its+-- dependencies have run, `readProp` will return a correct value, i.e. one+-- that satisfies the functional relations.+-- * The order in which the defining functions are executed does not affect the+-- result.+-- * Termination depends on the termination of the underlying propagator+--+module Data.Propagator.Purify+ ( Purify+ , get+ , mk, def1, def2, defList+ )+where++import System.IO.Unsafe+import Control.Monad.ST+import Data.Monoid+import Data.Coerce++import Data.Propagator.Class+import System.IO.RecThunk++-- | A value of type @Purify p@ is a propagator @p@, gether with a (lazy)+-- action to define it.+--+-- You can use 'get' to extract the value from the propagator.+--+-- Do not use the extracted value in the definition of that value, this will+-- loop just like a recursive definition with plain values would!+data Purify p = Purify+ { prop :: p+ , pre :: Thunk+ , post :: Thunk+ }++-- | Any value of type @a@ is also a value of type @Purify p@ if @p@ is a propagator for @a@.+mk :: Propagator p a => a -> Purify p+mk x = unsafePerformIO $ do+ p <- newConstProp x+ t1 <- doneThunk+ t2 <- doneThunk+ pure (Purify p t1 t2)++new :: Propagator p a => [Thunk] -> [Thunk] -> (p -> IO ()) -> Purify p+new ts1 ts2 act = unsafePerformIO $ do+ p <- newProp+ t1 <- thunk $ act p >> pure ts1+ t2 <- thunk $ freezeProp p >> pure ts2+ pure (Purify p t1 t2)++-- | Defines a value of type @Purify b@ to be a function of the values of @Purify a@.+--+-- The action passed should declare that relation to the underlying propagator.+--+-- The @Prop a@ propagator must only be used for reading values /from/.+def1 :: (Propagator pa a, Propagator pb b) =>+ (pa -> pb -> IO ()) ->+ Purify pa -> Purify pb+def1 def r1 = new [pre r1] [post r1] $ \p -> do+ def (prop r1) p++-- | Defines a value of type @Purify c@ to be a function of the values of @Purify a@ and @Purify b@.+--+-- The action passed should declare that relation to the underlying propagator.+--+-- The @Prop a@ and @Prop b@ propagators must only be used for reading values /from/.+def2 :: (Propagator pa a, Propagator pb b, Propagator pc c) =>+ (pa -> pb -> pc -> IO ()) ->+ Purify pa -> Purify pb -> Purify pc+def2 def r1 r2 = new [pre r1, pre r2] [post r1, post r2] $ \p -> do+ def (prop r1) (prop r2) p++-- | Defines a value of type @Purify b@ to be a function of the values of a list of @Purify a@ values.+--+-- The action passed should declare that relation to the underlying propagator.+--+-- The @Prop a@ propagators must only be used for reading values /from/.+defList :: (Propagator pa a, Propagator pb b) =>+ ([pa] -> pb -> IO ()) ->+ [Purify pa] -> Purify pb+defList def rs = new (map pre rs) (map post rs) $ \p -> do+ def (map prop rs) p++-- | Extract the value from a @Purify a@. This must not be used when /defining/ that value.+get :: Propagator pa a => Purify pa -> a+get r = unsafePerformIO $ do+ force (pre r)+ force (post r)+ readProp (prop r)
Data/Recursive/Bool.hs view
@@ -1,12 +1,12 @@ {-# LANGUAGE TypeApplications #-} -{- | The type @R Bool@ is ike 'Bool', but allows recursive definitions:+{- | The type @RBool@ is like 'Bool', but allows recursive definitions: >>> :{- let x = rTrue- y = x &&& z- z = y ||| rFalse- in getR x+ let x = RB.true+ y = x RB.&& z+ z = y RB.|| RB.false+ in RB.get x :} True @@ -14,88 +14,95 @@ This finds the least solution, i.e. prefers 'False' over 'True': >>> :{- let x = x &&& y- y = y &&& x- in (getR x, getR y)+ let x = x RB.&& y+ y = y RB.&& x+ in (RB.get x, RB.get y) :} (False,False) -Use @R (Dual Bool)@ from "Data.Recursive.DualBool" if you want the greatest solution.+Use 'Data.Recursive.DualBool.RDualBool' from "Data.Recursive.DualBool" if you want the greatest solution. -}-module Data.Recursive.Bool- ( R- , getR- , module Data.Recursive.Bool- ) where+module Data.Recursive.Bool (RBool, module Data.Recursive.Bool) where import Data.Coerce import Data.Monoid -import Data.Recursive.R.Internal-import Data.Recursive.R-import Data.Recursive.Propagator.P2+import Data.Recursive.Internal+import qualified Data.Propagator.Purify as Purify+import Data.Propagator.P2 -- $setup+-- >>> :load Data.Recursive.Bool Data.Recursive.DualBool+-- >>> :module - Data.Recursive.Bool Data.Recursive.DualBool+-- -- >>> :set -XFlexibleInstances -- >>> import Test.QuickCheck--- >>> instance Arbitrary (R Bool) where arbitrary = mkR <$> arbitrary--- >>> instance Show (R Bool) where show = show . getR--- >>> instance Arbitrary (R (Dual Bool)) where arbitrary = mkR <$> arbitrary--- >>> instance Show (R (Dual Bool)) where show = show . getR---- | prop> getR rTrue == True-rTrue :: R Bool-rTrue = mkR True---- | prop> getR rFalse == False-rFalse :: R Bool-rFalse = mkR False--{- Using the naive propagator:--(&&&) :: R Bool -> R Bool -> R Bool-(&&&) = defR2 $ lift2 (&&)--(|||) :: R Bool -> R Bool -> R Bool-(|||) = defR2 $ lift2 (||)+-- >>> import qualified Data.Recursive.Bool as RB+-- >>> instance Arbitrary RB.RBool where arbitrary = RB.mk <$> arbitrary+-- >>> instance Show RB.RBool where show = show . RB.get+--+-- >>> import qualified Data.Recursive.DualBool as RDB+-- >>> instance Arbitrary RDB.RDualBool where arbitrary = RDB.mk <$> arbitrary+-- >>> instance Show RDB.RDualBool where show = show . RDB.get -rand :: [R Bool] -> R Bool-rand = defRList $ liftList and+-- | Extracts the value of a 'RBool'+get :: RBool -> Bool+get (RBool p) = Purify.get p -ror :: [R Bool] -> R Bool-ror = defRList $ liftList or+-- | prop> RB.get (RB.mk b) === b+mk :: Bool -> RBool+mk b = RBool $ Purify.mk b -rnot :: R (Dual Bool) -> R Bool-rnot = defR1 $ lift1 $ coerce not+-- | prop> RB.get RB.true == True+true :: RBool+true = RBool $ Purify.mk True --}+-- | prop> RB.get RB.false == False+false :: RBool+false = RBool $ Purify.mk False --- | prop> getR (r1 &&& r2) === (getR r1 && getR r2)-(&&&) :: R Bool -> R Bool -> R Bool-(&&&) = defR2 $ coerce $ \p1 p2 p ->+-- | prop> RB.get (r1 RB.&& r2) === (RB.get r1 && RB.get r2)+(&&) :: RBool -> RBool -> RBool+(&&) = coerce $ Purify.def2 $ \p1 p2 p -> whenTop p1 (whenTop p2 (setTop p)) --- | prop> getR (r1 ||| r2) === (getR r1 || getR r2)-(|||) :: R Bool -> R Bool -> R Bool-(|||) = defR2 $ coerce $ \p1 p2 p -> do+-- | prop> RB.get (r1 RB.|| r2) === (RB.get r1 || RB.get r2)+(||) :: RBool -> RBool -> RBool+(||) = coerce $ Purify.def2 $ \p1 p2 p -> do whenTop p1 (setTop p) whenTop p2 (setTop p) --- | prop> getR (rand rs) === and (map getR rs)-rand :: [R Bool] -> R Bool-rand = defRList $ coerce go+-- | prop> RB.get (RB.and rs) === and (map RB.get rs)+and :: [RBool] -> RBool+and = coerce $ Purify.defList $ go where go [] p = setTop p go (p':ps) p = whenTop p' (go ps p) --- | prop> getR (ror rs) === or (map getR rs)-ror :: [R Bool] -> R Bool-ror = defRList $ coerce $ \ps p ->+-- | prop> RB.get (RB.or rs) === or (map RB.get rs)+or :: [RBool] -> RBool+or = coerce $ Purify.defList $ \ps p -> mapM_ @[] (`implies` p) ps --- | prop> getR (rnot r1) === not (getRDual r1)-rnot :: R (Dual Bool) -> R Bool-rnot = defR1 $ coerce $ \p1 p -> do+-- | prop> RB.get (RB.not r1) === not (RDB.get r1)+not :: RDualBool -> RBool+not = coerce $ Purify.def1 $ \p1 p -> do+ implies p1 p++-- | The identity function. This is useful when tying the knot, to avoid a loop that bottoms out:+--+-- > let x = x in RB.get x+--+-- will not work, but+--+-- >>> let x = RB.id x in RB.get x+-- False+--+-- does.+--+-- prop> RB.get (RB.id r) === RB.get r+id :: RBool -> RBool+id = coerce $ Purify.def1 $ \p1 p -> implies p1 p
Data/Recursive/DualBool.hs view
@@ -1,14 +1,12 @@-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeApplications #-} -{- | The type @R (Dual Bool)@ is ike 'Bool', but allows recursive definitions:+{- | The type @RDualBool@ is like 'Bool', but allows recursive definitions: >>> :{- let x = rTrue- y = x &&& z- z = y ||| rFalse- in getRDual x+ let x = RDB.true+ y = x RDB.&& z+ z = y RDB.|| RDB.false+ in RDB.get x :} True @@ -16,68 +14,94 @@ This finds the greatest solution, i.e. prefers 'True' over 'False': >>> :{- let x = x &&& y- y = y &&& x- in (getRDual x, getRDual y)+ let x = x RDB.&& y+ y = y RDB.&& x+ in (RDB.get x, RDB.get y) :} (True,True) -Use @R Bool@ from "Data.Recursive.Bool" if you want the least solution.+Use @RBool@ from "Data.Recursive.Bool" if you want the least solution. -}-module Data.Recursive.DualBool- ( R- , getRDual- , module Data.Recursive.DualBool- ) where+module Data.Recursive.DualBool (RDualBool, module Data.Recursive.DualBool) where import Data.Coerce import Data.Monoid -import Data.Recursive.R.Internal-import Data.Recursive.R-import Data.Recursive.Propagator.P2+import Data.Recursive.Internal+import qualified Data.Propagator.Purify as Purify+import Data.Propagator.P2 -- $setup+-- >>> :load Data.Recursive.Bool Data.Recursive.DualBool+-- >>> :module - Data.Recursive.Bool Data.Recursive.DualBool+-- -- >>> :set -XFlexibleInstances -- >>> import Test.QuickCheck--- >>> instance Arbitrary (R Bool) where arbitrary = mkR <$> arbitrary--- >>> instance Show (R Bool) where show = show . getR--- >>> instance Arbitrary (R (Dual Bool)) where arbitrary = mkR <$> arbitrary--- >>> instance Show (R (Dual Bool)) where show = show . getR+-- >>> import qualified Data.Recursive.Bool as RB+-- >>> instance Arbitrary RB.RBool where arbitrary = RB.mk <$> arbitrary+-- >>> instance Show RB.RBool where show = show . RB.get+--+-- >>> import qualified Data.Recursive.DualBool as RDB+-- >>> instance Arbitrary RDB.RDualBool where arbitrary = RDB.mk <$> arbitrary+-- >>> instance Show RDB.RDualBool where show = show . RDB.get --- | prop> getRDual rTrue == True-rTrue :: R (Dual Bool)-rTrue = mkR (Dual True)+-- | Extracts the value of a 'RDualBool'+get :: RDualBool -> Bool+get (RDualBool p) = Prelude.not (Purify.get p) --- | prop> getRDual rFalse == False-rFalse :: R (Dual Bool)-rFalse = mkR (Dual False)+-- | prop> RDB.get (RDB.mk b) === b+mk :: Bool -> RDualBool+mk b = RDualBool $ Purify.mk (Prelude.not b) --- | prop> getRDual (r1 ||| r2) === (getRDual r1 || getRDual r2)-(|||) :: R (Dual Bool) -> R (Dual Bool) -> R (Dual Bool)-(|||) = defR2 $ coerce $ \p1 p2 p ->- whenTop p1 (whenTop p2 (setTop p))+-- | prop> RDB.get RDB.true == True+true :: RDualBool+true = RDualBool $ Purify.mk False --- | prop> getRDual (r1 &&& r2) === (getRDual r1 && getRDual r2)-(&&&) :: R (Dual Bool) -> R (Dual Bool) -> R (Dual Bool)-(&&&) = defR2 $ coerce $ \p1 p2 p -> do+-- | prop> RDB.get RDB.false == False+false :: RDualBool+false = RDualBool $ Purify.mk True++-- | prop> RDB.get (r1 RDB.&& r2) === (RDB.get r1 && RDB.get r2)+(&&) :: RDualBool -> RDualBool -> RDualBool+(&&) = coerce $ Purify.def2 $ \p1 p2 p -> do whenTop p1 (setTop p) whenTop p2 (setTop p) --- | prop> getRDual (ror rs) === or (map getRDual rs)-ror :: [R (Dual Bool)] -> R (Dual Bool)-ror = defRList $ coerce go+-- | prop> RDB.get (r1 RDB.|| r2) === (RDB.get r1 || RDB.get r2)+(||) :: RDualBool -> RDualBool -> RDualBool+(||) = coerce $ Purify.def2 $ \p1 p2 p ->+ whenTop p1 (whenTop p2 (setTop p))++-- | prop> RDB.get (RDB.and rs) === and (map RDB.get rs)+and :: [RDualBool] -> RDualBool+and = coerce $ Purify.defList $ \ps p ->+ mapM_ @[] (`implies` p) ps++-- | prop> RDB.get (RDB.or rs) === or (map RDB.get rs)+or :: [RDualBool] -> RDualBool+or = coerce $ Purify.defList go where go [] p = setTop p go (p':ps) p = whenTop p' (go ps p) --- | prop> getRDual (rand rs) === and (map getRDual rs)-rand :: [R (Dual Bool)] -> R (Dual Bool)-rand = defRList $ coerce $ \ps p ->- mapM_ @[] (`implies` p) ps+-- | prop> RDB.get (RDB.not r1) === not (RB.get r1)+not :: RBool -> RDualBool+not = coerce $ Purify.def1 $ \p1 p -> do+ implies p1 p --- | prop> getRDual (rnot r1) === not (getR r1)-rnot :: R Bool -> R (Dual Bool)-rnot = defR1 $ coerce $ \p1 p -> do+-- | The identity function. This is useful when tying the knot, to avoid a loop that bottoms out:+--+-- > let x = x in RDB.get x+--+-- will not work, but+--+-- >>> let x = RDB.id x in RDB.get x+-- True+--+-- does.+--+-- | prop> RDB.get (RDB.id r) === RDB.get r+id :: RDualBool -> RDualBool+id = coerce $ Purify.def1 $ \p1 p -> implies p1 p
Data/Recursive/Examples.hs view
@@ -18,37 +18,40 @@ This library provides data types where this works. You can write the equations in that way just fine, and still get a result. -For example, the @R Bool@ type comes with functions that look quite like their+For example, the 'Data.Recursive.Bool.RBool' type comes with functions that look quite like their ordinary counterparts acting on 'Bool'. ->>> :t rTrue-rTrue :: R Bool->>> :t rFalse-rFalse :: R Bool->>> :t (|||)-(|||) :: R Bool -> R Bool -> R Bool->>> :t (&&&)-(&&&) :: R Bool -> R Bool -> R Bool->>> getR rTrue+>>> import Data.Recursive.Bool (RBool)+>>> import qualified Data.Recursive.Bool as RB++>>> :t RB.true+RB.true :: RBool+>>> :t RB.false+RB.false :: RBool+>>> :t (RB.||)+(RB.||) :: RBool -> RBool -> RBool+>>> :t (RB.&&)+(RB.&&) :: RBool -> RBool -> RBool+>>> RB.get RB.true True->>> getR rFalse+>>> RB.get RB.false False->>> getR (rFalse &&& rTrue)+>>> RB.get (RB.false RB.&& RB.true) False->>> getR (rTrue &&& rTrue)+>>> RB.get (RB.true RB.&& RB.true) True->>> getR (ror [rTrue, rFalse, rTrue])+>>> RB.get (RB.or [RB.true, RB.false, RB.true]) True So far so good, lets see what happens when we try something recursive: ->>> let x = ror [y]; y = rand [x, rFalse] in getR x+>>> let x = RB.or [y]; y = RB.and [x, RB.false] in RB.get x False->>> let x = ror [y]; y = ror [x, rFalse] in getR x+>>> let x = RB.or [y]; y = RB.or [x, RB.false] in RB.get x False->>> let x = ror [y]; y = ror [x, rTrue] in getR x+>>> let x = RB.or [y]; y = RB.or [x, RB.true] in RB.get x True->>> let x = ror [y]; y = ror [x] in getR x+>>> let x = RB.or [y]; y = RB.or [x] in RB.get x False == Least or greatest solution@@ -60,42 +63,45 @@ We (arbitrary) choose to find the least solution, i.e. prefer @False@ and only find @True@ if we have to. This is useful, for example, if you check something recursive for errors. -Sometimes you want the other one. Then you can use @R (Dual Bool)@. The module-"Data.Recursive.DualBool" exports all the functions for that type too. Because-of the name class we have imported it qualified here. We can run run the same-quations, and get different answers:+Sometimes you want the other one. Then you can use @RDualBool@. The module+"Data.Recursive.DualBool" exports all the functions for that type too. We can+run the same equations, and get different answers: ->>> let x = DB.ror [y]; y = DB.rand [x, DB.rFalse] in getRDual x+>>> import Data.Recursive.DualBool (RDualBool)+>>> import qualified Data.Recursive.DualBool as RDB+++>>> let x = RDB.or [y]; y = RDB.and [x, RDB.false] in RDB.get x False->>> let x = DB.ror [y]; y = DB.ror [x, DB.rFalse] in getRDual x+>>> let x = RDB.or [y]; y = RDB.or [x, RDB.false] in RDB.get x True->>> let x = DB.ror [y]; y = DB.ror [x, DB.rTrue] in getRDual x+>>> let x = RDB.or [y]; y = RDB.or [x, RDB.true] in RDB.get x True->>> let x = DB.ror [y]; y = DB.ror [x] in getRDual x+>>> let x = RDB.or [y]; y = RDB.or [x] in RDB.get x True The negation function is also available, and goes from can-be-true to must-be-true and back: ->>> :t rnot-rnot :: R (Dual Bool) -> R Bool->>> :t DB.rnot-DB.rnot :: R Bool -> R (Dual Bool)+>>> :t RB.not+RB.not :: RDualBool -> RBool+>>> :t RDB.not+RDB.not :: RBool -> RDualBool This allows us to mix the different types in the same computation: >>> :{- let x = rnot y ||| rnot z- y = DB.rnot x DB.&&& z- z = DB.rTrue- in (getR x, getRDual y, getRDual z)+ let x = RB.not y RB.|| RB.not z+ y = RDB.not x RDB.&& z+ z = RDB.true+ in (RB.get x, RDB.get y, RDB.get z) :} (False,True,True) >>> :{- let x = rnot y ||| rnot z- y = DB.rnot x DB.&&& z- z = DB.rFalse- in (getR x, getRDual y, getRDual z)+ let x = RB.not y RB.|| RB.not z+ y = RDB.not x RDB.&& z+ z = RDB.false+ in (RB.get x, RDB.get y, RDB.get z) :} (True,False,False) @@ -104,27 +110,29 @@ We do not have to stop with booleans, and can define similar APIs for other data stuctures, e.g. sets: -Again we can describe sets recursively, using the monotone functions 'rEmpty',-'rInsert' and 'rUnion'+>>> import qualified Data.Recursive.Set as RS +Again we can describe sets recursively, using the monotone functions 'RS.empty',+'RS.insert' and 'RS.union'+ >>> :{- let s1 = rInsert 23 s2- s2 = rInsert 42 s1- in getR s1+ let s1 = RS.insert 23 s2+ s2 = RS.insert 42 s1+ in RS.get s1 :} fromList [23,42] -Here is a slightly larger example, where we can can use this API to elegantly+Here is a slightly larger example, where we can use this API to elegantly calculate the reachable nodes in a graph (represented as a map from vertices to their successors), using a typical knot-tying approach. But unless with plain 'S.Set', it now works even if the graph has cycles: >>> :{ reachable :: M.Map Int [Int] -> M.Map Int (S.Set Int)- reachable g = fmap getR sets+ reachable g = fmap RS.get sets where- sets :: M.Map Int (R (S.Set Int))- sets = M.mapWithKey (\v vs -> rInsert v (rUnions [ sets ! v' | v' <- vs ])) g+ sets :: M.Map Int (RS.RSet Int)+ sets = M.mapWithKey (\v vs -> RS.insert v (RS.unions [ sets ! v' | v' <- vs ])) g :} >>> let graph = M.fromList [(1,[2,3]),(2,[1]),(3,[])]@@ -137,37 +145,37 @@ Of course, the magic stops somewhere: Just like with the usual knot-tying tricks, you still have to make sure to be lazy enough. In particular, you should-not peek at the value (e.g. using 'getR') while you are building the graph:+not peek at the value (e.g. using 'RB.get') while you are building the graph: >>> :{ withTimeout $- let x = rand [x, if getR y then z else rTrue]- y = rand [x, rTrue]- z = rFalse- in getR y+ let x = RB.and [x, if RB.get y then z else RB.true]+ y = RB.and [x, RB.true]+ z = RB.false+ in RB.get y :} *** Exception: timed out Similarly, you have to make sure you recurse through one of these functions; @let x = x@ still does not work: ->>> withTimeout $ let x = x :: R Bool in getR x+>>> withTimeout $ let x = x :: RBool in RB.get x *** Exception: timed out->>> withTimeout $ let x = x &&& x in getR x+>>> withTimeout $ let x = x RB.&& x in RB.get x False We belive that the APIs provided here are still “pure”: evaluation order does not affect the results, and you can replace equals with equals, in the sense that -> let s = rInsert 42 s in s+> let s = RS.insert 42 s in s is the same as -> let s = rInsert 42 s in rInsert 42 s+> let s = RS.insert 42 s in RS.insert 42 s However, the the following two expressions are not equivalent: ->>> withTimeout $ S.toList $ let s = rInsert 42 s in getR s+>>> withTimeout $ S.toList $ let s = RS.insert 42 s in RS.get s [42]->>> withTimeout $ S.toList $ let s () = rInsert 42 (s ()) in getR (s ())+>>> withTimeout $ S.toList $ let s () = RS.insert 42 (s ()) in RS.get (s ()) *** Exception: timed out It is debatable if that is a problem.@@ -175,11 +183,11 @@ -} module Data.Recursive.Examples () where -import Data.Recursive.R-import Data.Recursive.Bool-import qualified Data.Recursive.DualBool as DB-import Data.Recursive.Set-import Data.Monoid+-- Imports for haddock++import qualified Data.Recursive.Bool as RB+import qualified Data.Recursive.DualBool as RDB+import qualified Data.Recursive.Set as RS -- $setup --
+ Data/Recursive/Internal.hs view
@@ -0,0 +1,32 @@+{-# OPTIONS_HADDOCK not-home #-}+{-# LANGUAGE TypeApplications #-}++{- |+ This modules contains the newtype definitions backing++ * "Data.Recursive.Bool"+ * "Data.Recursive.DualBool"+ * "Data.Recursive.Set"++ Access to the newtype contructor can break the guarantees of these modules.+ Only import this if you want to extend the APIs for these types.+-}+module Data.Recursive.Internal where++import qualified Data.Set as S+import qualified Data.Map as M+import qualified Data.Propagator.Purify as Purify+import Data.Propagator.P2+import Data.Propagator.Naive++-- | Like 'Bool', but admits recursive definitions, preferring the least solution.+newtype RBool = RBool (Purify.Purify P2)++-- | Like 'Bool', but admits recursive definitions, preferring the greatest solution.+newtype RDualBool = RDualBool (Purify.Purify P2)++-- | Like 'S.Set', but admits recursive definitions.+newtype RSet a = RSet (Purify.Purify (Prop (S.Set a)))++-- | Like 'M.Map', but admits recursive definitions.+data RMap a b = RMap (RSet a) (M.Map a b)
+ Data/Recursive/Map.hs view
@@ -0,0 +1,190 @@+{-# LANGUAGE TypeFamilies #-}+{- | The type 'RMap' @a@ @b@ is like 'M.Map' @a@ @b@, but allows recursive definitions:++>>> :{+ let m1 = RM.insert 23 "Hello" m2+ m2 = RM.insert 42 "World" m1+ in RM.get m1+ :}+fromList [(23,"Hello"),(42,"World")]++All functions in this API are monotone with regard to the ordering of maps that+uses the /discrete/ order on its elements. Furthermore, we only include+functions where the key set does not depend on the actual values of the maps.++This means that maps defined recursively using functions like 'RM.insertWith'+can be used to construct cyclic data structures:++>>> :{+ let m = RM.insertWith (++) 23 "Hi" m+ in take 20 $ RM.get m M.! 23+ :}+"HiHiHiHiHiHiHiHiHiHi"++And because the APIs provided by this package work similar to cyclic data+structures, we can use them inside these maps:++>>> :{+ let m = RM.insertWith RS.union 23 (RS.singleton "Hi") m+ in RM.get m+ :}+fromList [(23,fromList ["Hi"])]++I am looking for a concice but useful example for this feature to be put here! ++An alternative would be to order these maps using a pointwise order on the maps+of elements (and do a simple fixed-point iteration underneath). But then we+could provide a general 'RM.unionWith' function, because not every function+passed to it would be monotone.++-}+module Data.Recursive.Map+ ( RMap+ , get+ , mk+ , empty+ , singleton+ , insert+ , insertWith+ , insertWithKey+ , delete+ , adjust+ , adjustWithKey+ , union+ , unionWith+ , unionWithKey+ , intersection+ , intersectionWith+ , intersectionWithKey+ , member+ , notMember+ , disjoint+ , Data.Recursive.Map.null+ , fromSet+ , keysSet+ , restrictKeys+ ) where++import qualified Data.Map as M+import qualified Data.Set as S+import Data.Coerce+import Data.Monoid+import Control.Monad++import Data.Recursive.Internal+import qualified Data.Recursive.Set as RS++-- $setup+-- >>> :load Data.Recursive.Set Data.Recursive.Map Data.Recursive.Bool Data.Recursive.DualBool+-- >>> :module - Data.Recursive.Set Data.Recursive.Map Data.Recursive.Bool Data.Recursive.DualBool+-- >>> import qualified Data.Recursive.Set as RS+-- >>> import qualified Data.Recursive.Map as RM+-- >>> import qualified Data.Recursive.Bool as RB+-- >>> import qualified Data.Recursive.DualBool as RDB+-- >>> import qualified Data.Set as S+-- >>> import qualified Data.Map as M+-- >>> :set -XFlexibleInstances+-- >>> :set -XScopedTypeVariables+-- >>> import Test.QuickCheck+-- >>> instance (Ord a, Arbitrary a) => Arbitrary (RS.RSet a) where arbitrary = RS.mk <$> arbitrary+-- >>> instance (Ord a, Show a) => Show (RS.RSet a) where show = show . RS.get+-- >>> instance (Ord a, Arbitrary a, Arbitrary b) => Arbitrary (RM.RMap a b) where arbitrary = RM.mk <$> arbitrary+-- >>> instance (Ord a, Show a, Show b) => Show (RM.RMap a b) where show = show . RM.get++-- | Extracts the value of a 'MSet'+get :: RMap a b -> M.Map a b+get (RMap _s m) = m++-- | prop> RM.get (RM.mk m) === m+mk :: M.Map a b -> RMap a b+mk m = RMap (RS.mk (M.keysSet m)) m++-- | prop> RM.get RM.empty === M.empty+empty :: RMap a b+empty = RMap RS.empty M.empty++-- | prop> RM.get (RM.singleton k v) === M.singleton k v+singleton :: a -> b -> RMap a b+singleton k v = RMap (RS.singleton k) (M.singleton k v)++build :: Ord a => RS.RSet a -> M.Map a b -> RMap a b+build s m = RMap s (M.fromSet (m M.!) (RS.get s))++-- | prop> RM.get (RM.insert k v m) === M.insert k v (RM.get m)+insert :: Ord a => a -> b -> RMap a b -> RMap a b+insert k v ~(RMap rs m) = build (RS.insert k rs) (M.insert k v m)++-- | prop> RM.get (RM.insertWith (applyFun2 f) k v m) === M.insertWith (applyFun2 f) k v (RM.get m)+insertWith :: Ord a => (b -> b -> b) -> a -> b -> RMap a b -> RMap a b+insertWith f k v ~(RMap rs m) = build (RS.insert k rs) (M.insertWith f k v m)++-- | prop> RM.get (RM.insertWithKey (applyFun3 f) k v m) === M.insertWithKey (applyFun3 f) k v (RM.get m)+insertWithKey :: Ord a => (a -> b -> b -> b) -> a -> b -> RMap a b -> RMap a b+insertWithKey f k v ~(RMap rs m) = build (RS.insert k rs) (M.insertWithKey f k v m)++-- | prop> RM.get (RM.delete k m) === M.delete k (RM.get m)+delete :: Ord a => a -> RMap a b -> RMap a b+delete k ~(RMap rs m) = build (RS.delete k rs) (M.delete k m)++-- | prop> RM.get (RM.adjust (applyFun f) k m) === M.adjust (applyFun f) k (RM.get m)+adjust :: Ord a => (b -> b) -> a -> RMap a b -> RMap a b+adjust f k ~(RMap rs m) = build (RS.id rs) (M.adjust f k m)++-- | prop> RM.get (RM.adjustWithKey (applyFun2 f) k m) === M.adjustWithKey (applyFun2 f) k (RM.get m)+adjustWithKey :: Ord a => (a -> b -> b) -> a -> RMap a b -> RMap a b+adjustWithKey f k ~(RMap rs m) = build (RS.id rs) (M.adjustWithKey f k m)++-- | prop> RM.get (RM.union m1 m2) === M.union (RM.get m1) (RM.get m2)+union :: Ord a => RMap a b -> RMap a b -> RMap a b+union ~(RMap rs1 m1) ~(RMap rs2 m2) = build (RS.union rs1 rs2) (M.union m1 m2)++-- | prop> RM.get (RM.unionWith (applyFun2 f) m1 m2) === M.unionWith (applyFun2 f) (RM.get m1) (RM.get m2)+unionWith :: Ord a => (b -> b -> b) -> RMap a b -> RMap a b -> RMap a b+unionWith f ~(RMap rs1 m1) ~(RMap rs2 m2) = build (RS.union rs1 rs2) (M.unionWith f m1 m2)++-- | prop> RM.get (RM.unionWithKey (applyFun3 f) m1 m2) === M.unionWithKey (applyFun3 f) (RM.get m1) (RM.get m2)+unionWithKey :: Ord a => (a -> b -> b -> b) -> RMap a b -> RMap a b -> RMap a b+unionWithKey f ~(RMap rs1 m1) ~(RMap rs2 m2) = build (RS.union rs1 rs2) (M.unionWithKey f m1 m2)++-- | prop> RM.get (RM.intersection m1 m2) === M.intersection (RM.get m1) (RM.get m2)+intersection :: Ord a => RMap a b -> RMap a b -> RMap a b+intersection ~(RMap rs1 m1) ~(RMap rs2 m2) = build (RS.intersection rs1 rs2) (M.intersection m1 m2)++-- | prop> RM.get (RM.intersectionWith (applyFun2 f) m1 m2) === M.intersectionWith (applyFun2 f) (RM.get m1) (RM.get m2)+intersectionWith :: Ord a => (b -> b -> b) -> RMap a b -> RMap a b -> RMap a b+intersectionWith f ~(RMap rs1 m1) ~(RMap rs2 m2) = build (RS.intersection rs1 rs2) (M.intersectionWith f m1 m2)++-- | prop> RM.get (RM.intersectionWithKey (applyFun3 f) m1 m2) === M.intersectionWithKey (applyFun3 f) (RM.get m1) (RM.get m2)+intersectionWithKey :: Ord a => (a -> b -> b -> b) -> RMap a b -> RMap a b -> RMap a b+intersectionWithKey f ~(RMap rs1 m1) ~(RMap rs2 m2) = build (RS.intersection rs1 rs2) (M.intersectionWithKey f m1 m2)+++-- | prop> RM.get (RM.singleton k v) === M.singleton k v+fromSet :: (a -> b) -> RS.RSet a -> RMap a b+fromSet f s = RMap s (M.fromSet f (RS.get s))++-- | prop> RS.get (RM.keysSet m) === M.keysSet (RM.get m)+keysSet :: RMap a b -> RS.RSet a+keysSet ~(RMap rs m) = RS.id rs+ -- better use RS.id either here or in fromSet, to avoid unproductive loops++-- | prop> RM.get (RM.restrictKeys m s) === M.restrictKeys (RM.get m) (RS.get s)+restrictKeys :: Ord a => RMap a b -> RS.RSet a -> RMap a b+restrictKeys ~(RMap rs m) s2 =+ build (rs `RS.intersection` s2) (M.restrictKeys m (RS.get s2))++-- | prop> RB.get (RM.member k m) === M.member k (RM.get m)+member :: Ord a => a -> RMap a b -> RBool+member x ~(RMap rs m) = RS.member x rs++-- | prop> RDB.get (RM.notMember n r1) === M.notMember n (RM.get r1)+notMember :: Ord a => a -> RMap a b -> RDualBool+notMember x ~(RMap rs m) = RS.notMember x rs++-- | prop> RDB.get (RM.disjoint m1 m2) === M.disjoint (RM.get m1) (RM.get m2)+disjoint :: Ord a => RMap a b -> RMap a b -> RDualBool+disjoint ~(RMap rs1 _ ) ~(RMap rs2 m2) = RS.disjoint rs1 rs2++-- | prop> RDB.get (RM.null m) === M.null (RM.get m)+null :: Ord a => RMap a b -> RDualBool+null ~(RMap rs m) = RS.null rs
− Data/Recursive/Propagator/Class.hs
@@ -1,55 +0,0 @@-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE FunctionalDependencies #-}---- | This module provides the 'Propagator' and 'HasPropagator' classes.-module Data.Recursive.Propagator.Class where--import Data.Monoid (Dual(..))-import qualified Data.Set as S-import Data.Coerce--import qualified Data.Recursive.Propagator.Naive as Naive-import Data.Recursive.Propagator.P2-import Data.POrder---- | The Propagator class defines some functions shared by different propagator--- implementations. This backs the generic "Data.Recursive.R.Internal" wrapper.-class Propagator p x | p -> x where- -- | The type of values inside the propagator- newProp :: IO p- newConstProp :: x -> IO p- readProp :: p -> IO x--instance Bottom x => Propagator (Naive.Prop x) x where- newProp = Naive.newProp bottom- newConstProp = Naive.newProp- readProp = Naive.readProp--instance Propagator PBool Bool where- newProp = coerce newP2- newConstProp False = coerce newP2- newConstProp True = coerce newTopP2- readProp = coerce isTop--instance Propagator PDualBool (Dual Bool) where- newProp = coerce newP2- newConstProp (Dual True) = coerce newP2- newConstProp (Dual False) = coerce newTopP2- readProp = coerce $ fmap not . isTop---- | The HasPropagator class is used to pick a propagator implementation for a--- particular value type.-class Propagator (Prop x) x => HasPropagator x where- type Prop x--instance HasPropagator Bool where- type Prop Bool = PBool--instance HasPropagator (Dual Bool) where- type Prop (Dual Bool) = PDualBool--instance Eq a => HasPropagator (S.Set a) where- type Prop (S.Set a) = Naive.Prop (S.Set a)
− Data/Recursive/Propagator/Naive.hs
@@ -1,110 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}---- | A very naive propagator library.------ This propagator implementation keeps updating the values accoring to their--- definitions as other values change, until a fixed-point is reached.------ It is a naive implementation and not very clever. Much more efficient--- propagator implementations are possible, and may be used by this library in--- the future.-module Data.Recursive.Propagator.Naive- ( Prop- , newProp- , readProp- , watchProp- , setProp- , lift1- , lift2- , liftList- )- where--import Control.Monad---- I want to test this code with dejafu, without carrying it as a dependency--- of the main library. So here is a bit of CPP to care for that.--#ifdef DEJAFU--#define Ctxt MonadConc m =>-#define Prop_ Prop m-#define IORef_ IORef m-#define MVar_ MVar m-#define M m--import Control.Concurrent.Classy--#else--#define Ctxt-#define Prop_ Prop-#define IORef_ IORef-#define MVar_ MVar-#define M IO--import Control.Concurrent.MVar-import Data.IORef--#endif---- | A cell in a propagator network-data Prop_ a = Prop- { val :: IORef_ a- , lock :: MVar_ ()- , onChange :: IORef_ (M ())- }---- | Creates a cell, given an initial value-newProp :: Ctxt a -> M (Prop_ a)-newProp x = do- m <- newIORef x- l <- newMVar ()- notify <- newIORef (pure ())- pure $ Prop m l notify---- | Reads the current value of the cell-readProp :: Ctxt Prop_ a -> M a-readProp (Prop m _ _ ) = readIORef m---- | Sets a new value calculated from the given action. The action is executed atomically.------ If the value has changed, all watchers are notified afterwards (not atomically).-setProp :: Ctxt Eq a => Prop_ a -> M a -> M ()-setProp (Prop m l notify) getX = do- () <- takeMVar l- old <- readIORef m- new <- getX- writeIORef m new- putMVar l ()- unless (new == old) $ join (readIORef notify)---- | Watch a cell: If the value changes, the given action is executed-watchProp :: Ctxt Prop_ a -> M () -> M ()-watchProp (Prop _ _ notify) f =- atomicModifyIORef notify $ \a -> (f >> a, ())---- | Whenever the first cell changes, update the second, using the given function-lift1 :: Ctxt Eq b => (a -> b) -> Prop_ a -> Prop_ b -> M ()-lift1 f p1 p = do- let update = setProp p $ f <$> readProp p1- watchProp p1 update- update---- | Whenever any of the first two cells change, update the third, using the given function-lift2 :: Ctxt Eq c => (a -> b -> c) -> Prop_ a -> Prop_ b -> Prop_ c -> M ()-lift2 f p1 p2 p = do- let update = setProp p $ f <$> readProp p1 <*> readProp p2- watchProp p1 update- watchProp p2 update- update---- | Whenever any of the cells in the list change, update the other, using the given function-liftList :: Ctxt Eq b => ([a] -> b) -> [Prop_ a] -> Prop_ b -> M ()-liftList f ps p = do- let update = setProp p $ f <$> mapM readProp ps- mapM_ (\p' -> watchProp p' update) ps- update
− Data/Recursive/Propagator/P2.hs
@@ -1,101 +0,0 @@-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE CPP #-}---- | A propagator for the two-point lattice----module Data.Recursive.Propagator.P2- ( P2- , newP2- , newTopP2- , setTop- , whenTop- , implies- , isTop- , PBool(..)- , PDualBool(..)- )- where---- I want to test this code with dejafu, without carrying it as a dependency--- of the main library. So here is a bit of CPP to care for that.--#ifdef DEJAFU--#define Ctxt MonadConc m =>-#define MaybeTop_ (MaybeTop m)-#define P2_ (P2 m)-#define PBool_ PBool m-#define PDualBool_ PDualBool m-#define IORef_ IORef m-#define MVar_ MVar m-#define M m--import Control.Concurrent.Classy--#else--#define Ctxt-#define MaybeTop_ MaybeTop-#define P2_ P2-#define PBool_ PBool-#define PDualBool_ PDualBool-#define IORef_ IORef-#define MVar_ MVar-#define M IO--import Control.Concurrent.MVar-import Data.IORef--#endif--data MaybeTop_- = StillBottom (M ()) -- ^ Just act: Still bottom, run act (once!) when triggered- | SurelyTop -- ^ Definitely top---- | A type for propagators for the two-point lattice, consisting of bottom and top-newtype P2_ = P2 (MVar_ MaybeTop_)---- | A new propagator, initialized at bottom-newP2 :: Ctxt M P2_-newP2 = P2 <$> newMVar (StillBottom (pure()))---- | A new propagator, already set to top-newTopP2 :: Ctxt M P2_-newTopP2 = P2 <$> newMVar SurelyTop---- | @whenTop p act@ runs @act@ if @p@ is already top, or after @setTop p@ is run-whenTop :: Ctxt P2_ -> M () -> M ()-whenTop (P2 p1) act = takeMVar p1 >>= \case- SurelyTop -> putMVar p1 SurelyTop >> act- StillBottom act' -> putMVar p1 (StillBottom (act >> act'))----- | Set a propagator to top.------ If it was bottom before, runs the actions queued with 'whenTop'. It does so--- _after_ setting the propagator to top, so that cycles are broken.-setTop :: Ctxt P2_ -> M ()-setTop (P2 p) = takeMVar p >>= \case- SurelyTop -> putMVar p SurelyTop- StillBottom act -> do- -- Do this first, this breaks cycles- putMVar p SurelyTop- -- Now notify the dependencies- act---- | @p1 `implies` p2@ chains propagators: If @p1@ becomes top, then so does @p2@.-implies :: Ctxt P2_ -> P2_ -> M ()-implies p1 p2 = whenTop p1 (setTop p2)---- | Queries the current state of the propagator. All related calls to @setTop@--- that have executed so far are taken into account.-isTop :: Ctxt P2_ -> M Bool-isTop (P2 p) = readMVar p >>= \case- SurelyTop -> pure True- StillBottom _ -> pure False---- | A newtype around 'P2' to denote that bottom is 'False' and top is 'True'-newtype PBool_ = PBool P2_---- | A newtype around 'P2' to denote that bottom is 'True' and top is 'False'-newtype PDualBool_ = PDualBool P2_
− Data/Recursive/R.hs
@@ -1,8 +0,0 @@--- |--- This module re-exports the safe parts of "Data.Recursive.R.Internal".------ If you import a module like "Data.Recursive.Bool" you do not need to import--- this module here directly.-module Data.Recursive.R (R, mkR, getR, getRDual) where--import Data.Recursive.R.Internal
− Data/Recursive/R/Internal.hs
@@ -1,113 +0,0 @@-{-# OPTIONS_HADDOCK not-home #-}--{-# LANGUAGE GADTs #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE AllowAmbiguousTypes #-}---- |------ This module provides the 'R' data type, which wraps an imperative propagator (e.g. "Data.Recursive.Propagator.Naive") in a pure and (if done right) safe data structure.------ The result of 'getR' is always a solution of the given equations, but for it--- to be deterministic (and hence for this API to be safe), the following--- should hold:------ * The @a@ in @R a@ should be partially orderd ('Data.POrder.POrder')--- * That partial order must respect equality on @a@--- * It must have a bottom element 'Data.POrder.bottom' ('Data.POrder.Bottom').--- * The function passed to 'defR1', 'defR2' etc. must be a monotonic function--- between these partial orders.------ If this does not hold, then the result of 'getR' may not be deterministic.------ Termination depends on whether a soluiton can be found iteratively. This is--- guaranteed if all partial orders involved satisfy the Ascending Chain Condition.--module Data.Recursive.R.Internal- ( R- , getR, getRDual- , mkR, defR1, defR2, defRList- )-where--import System.IO.Unsafe-import Control.Monad.ST-import Data.Monoid-import Data.Coerce--import Data.Recursive.Propagator.Class-import System.IO.RecThunk---- | A value of type @R a@ is a @a@, but defined using only specific operations--- (which you will find in the corresponding module, e.g.--- "Data.Recursive.Bool"), which allow recursive definitions.------ You can use 'getR' to extract the value.------ Do not use the extracted value in the definition of that value, this will--- loop just like a recursive definition with plain values would.-data R a = R (Prop a) Thunk---- | Any value of type @a@ is also a value of type @r a@.-mkR :: HasPropagator a => a -> R a-mkR x = unsafePerformIO $ do- p <- newConstProp x- t <- doneThunk- pure (R p t)--newR :: HasPropagator a => (Prop a -> IO [Thunk]) -> R a-newR act = unsafePerformIO $ do- p <- newProp- t <- thunk (act p)- pure (R p t)---- | Defines a value of type @R b@ to be a function of the values of @R a@.------ The action passed it should declare that relation to the underlying propagator.------ The @Prop a@ propagator must only be used for reading values _from_.-defR1 :: (HasPropagator a, HasPropagator b) =>- (Prop a -> Prop b -> IO ()) ->- R a -> R b-defR1 def r1 = newR $ \p -> do- let R p1 t1 = r1- def p1 p- pure [t1]---- | Defines a value of type @R c@ to be a function of the values of @R a@ and @R b@.------ The action passed it should declare that relation to the underlying propagator.------ The @Prop a@ and @Prop b@ propagators must only be used for reading values _from_.-defR2 :: (HasPropagator a, HasPropagator b, HasPropagator c) =>- (Prop a -> Prop b -> Prop c -> IO ()) ->- R a -> R b -> R c-defR2 def r1 r2 = newR $ \p -> do- let R p1 t1 = r1- let R p2 t2 = r2- def p1 p2 p- pure [t1, t2]---- | Defines a value of type @R b@ to be a function of the values of a list of @R a@ values.------ The action passed it should declare that relation to the underlying propagator.------ The @Prop a@ propagators must only be used for reading values _from_.-defRList :: (HasPropagator a, HasPropagator b) =>- ([Prop a] -> Prop b -> IO ()) ->- [R a] -> R b-defRList def rs = newR $ \p -> do- def [ p' | R p' _ <- rs] p- pure [ t | R _ t <- rs]---- | Extract the value from a @R a@. This must not be used when _defining_ that value.-getR :: HasPropagator a => R a -> a-getR (R p t) = unsafePerformIO $ do- force t- readProp p---- | Convenience variant of 'getR' to also remove the 'Dual' newtype wrapper, mostly for use with "Data.Recursive.DualBool".-getRDual :: HasPropagator (Dual a) => R (Dual a) -> a-getRDual = getDual . getR
Data/Recursive/Set.hs view
@@ -1,90 +1,128 @@ {-# LANGUAGE TypeFamilies #-}-{- | The type @R (Dual Bool)@ is ike 'Bool', but allows recursive definitions:+{- | The type @RS.RSet a@ is like 'S.Set' @a@, but allows recursive definitions: >>> :{- let s1 = rInsert 23 s2- s2 = rInsert 42 s1- in getR s1+ let s1 = RS.insert 23 s2+ s2 = RS.insert 42 s1+ in RS.get s1 :} fromList [23,42] -}-module Data.Recursive.Set- ( R- , mkR- , getR- , module Data.Recursive.Set- ) where+module Data.Recursive.Set (RSet, module Data.Recursive.Set) where import qualified Data.Set as S import Data.Coerce import Data.Monoid import Control.Monad -import Data.Recursive.R.Internal-import Data.Recursive.Propagator.Naive-import Data.Recursive.Propagator.P2+import Data.Recursive.Internal+import qualified Data.Propagator.Purify as Purify+import Data.Propagator.Naive+import Data.Propagator.P2 -- $setup+-- >>> :load Data.Recursive.Set Data.Recursive.Bool Data.Recursive.DualBool+-- >>> :module - Data.Recursive.Set Data.Recursive.Bool Data.Recursive.DualBool+-- >>> import qualified Data.Recursive.Set as RS+-- >>> import qualified Data.Recursive.Bool as RB+-- >>> import qualified Data.Recursive.DualBool as RDB+-- >>> import qualified Data.Set as S -- >>> :set -XFlexibleInstances -- >>> :set -XScopedTypeVariables -- >>> import Test.QuickCheck--- >>> instance (Ord a, Arbitrary a) => Arbitrary (R (S.Set a)) where arbitrary = mkR <$> arbitrary--- >>> instance (Eq a, Show a) => Show (R (S.Set a)) where show = show . getR+-- >>> instance (Ord a, Arbitrary a) => Arbitrary (RS.RSet a) where arbitrary = RS.mk <$> arbitrary+-- >>> instance (Ord a, Show a) => Show (RS.RSet a) where show = show . RS.get --- | prop> getR rEmpty === S.empty-rEmpty :: Eq a => R (S.Set a)-rEmpty = mkR S.empty+-- | Extracts the value of a 'RSet a'+get :: RSet a -> S.Set a+get (RSet p) = Purify.get p --- | prop> getR (rInsert n r1) === S.insert n (getR r1)-rInsert :: Ord a => a -> R (S.Set a) -> R (S.Set a)-rInsert x = defR1 $ lift1 $ S.insert x+-- | prop> RB.get (RB.mk s) === s+mk :: S.Set a -> RSet a+mk s = RSet $ Purify.mk s --- | prop> getR (rDelete n r1) === S.delete n (getR r1)-rDelete :: Ord a => a -> R (S.Set a) -> R (S.Set a)-rDelete x = defR1 $ lift1 $ S.delete x+-- | prop> RS.get RS.empty === S.empty+empty :: RSet a+empty = RSet $ Purify.mk S.empty --- | prop> \(Fun _ p) -> getR (rFilter p r1) === S.filter p (getR r1)-rFilter :: Ord a => (a -> Bool) -> R (S.Set a) -> R (S.Set a)-rFilter f = defR1 $ lift1 $ S.filter f+-- | prop> RS.get (RS.singleton x) === S.singleton x+singleton :: a -> RSet a+singleton x = RSet $ Purify.mk $ S.singleton x --- | prop> getR (rUnion r1 r2) === S.union (getR r1) (getR r2)-rUnion :: Ord a => R (S.Set a) -> R (S.Set a) -> R (S.Set a)-rUnion = defR2 $ lift2 S.union+-- | prop> RS.get (RS.insert n r1) === S.insert n (RS.get r1)+insert :: Ord a => a -> RSet a -> RSet a+insert x = coerce $ Purify.def1 $ lift1 $ S.insert x --- | prop> getR (rUnions rs) === S.unions (map getR rs)-rUnions :: Ord a => [R (S.Set a)] -> R (S.Set a)-rUnions = defRList $ liftList S.unions+-- | prop> RS.get (RS.delete n r1) === S.delete n (RS.get r1)+delete :: Ord a => a -> RSet a -> RSet a+delete x = coerce $ Purify.def1 $ lift1 $ S.delete x --- | prop> getR (rIntersection r1 r2) === S.intersection (getR r1) (getR r2)-rIntersection :: Ord a => R (S.Set a) -> R (S.Set a) -> R (S.Set a)-rIntersection = defR2 $ lift2 S.intersection+-- | prop> \(Fun _ p) -> RS.get (RS.filter p r1) === S.filter p (RS.get r1)+filter :: Ord a => (a -> Bool) -> RSet a -> RSet a+filter f = coerce $ Purify.def1 $ lift1 $ S.filter f --- | prop> getR (rMember n r1) === S.member n (getR r1)-rMember :: Ord a => a -> R (S.Set a) -> R Bool-rMember x = defR1 $ \ps pb -> do+-- | prop> RS.get (RS.union r1 r2) === S.union (RS.get r1) (RS.get r2)+union :: Ord a => RSet a -> RSet a -> RSet a+union = coerce $ Purify.def2 $ lift2 S.union++-- | prop> RS.get (RS.unions rs) === S.unions (map RS.get rs)+unions :: Ord a => [RSet a] -> RSet a+unions = coerce $ Purify.defList $ liftList S.unions++-- | prop> RS.get (RS.intersection r1 r2) === S.intersection (RS.get r1) (RS.get r2)+intersection :: Ord a => RSet a -> RSet a -> RSet a+intersection = coerce $ Purify.def2 $ lift2 S.intersection++-- | prop> RB.get (RS.member n r1) === S.member n (RS.get r1)+member :: Ord a => a -> RSet a -> RBool+member x = coerce $ Purify.def1 $ \ps pb -> do let update = do s <- readProp ps- when (S.member x s) $ coerce setTop pb+ when (S.member x s) $ setTop pb watchProp ps update update --- | prop> getRDual (rNotMember n r1) === S.notMember n (getR r1)-rNotMember :: Ord a => a -> R (S.Set a) -> R (Dual Bool)-rNotMember x = defR1 $ \ps pb -> do+-- | prop> RDB.get (RS.notMember n r1) === S.notMember n (RS.get r1)+notMember :: Ord a => a -> RSet a -> RDualBool+notMember x = coerce $ Purify.def1 $ \ps pb -> do let update = do s <- readProp ps- when (S.member x s) $ coerce setTop pb+ when (S.member x s) $ setTop pb watchProp ps update update --- | prop> getRDual (rDisjoint r1 r2) === S.disjoint (getR r1) (getR r2)-rDisjoint :: Ord a => R (S.Set a) -> R (S.Set a) -> R (Dual Bool)-rDisjoint = defR2 $ \ps1 ps2 (PDualBool pb) -> do+-- | prop> RDB.get (RS.null s) === S.null (RS.get s)+null :: RSet a -> RDualBool+null = coerce $ Purify.def1 $ \ps pb -> do let update = do+ s <- readProp ps+ unless (S.null s) $ setTop pb+ watchProp ps update+ update++-- | prop> RDB.get (RS.disjoint r1 r2) === S.disjoint (RS.get r1) (RS.get r2)+disjoint :: Ord a => RSet a -> RSet a -> RDualBool+disjoint = coerce $ Purify.def2 $ \ps1 ps2 pb -> do+ let update = do s1 <- readProp ps1 s2 <- readProp ps2- unless (S.disjoint s1 s2) $ coerce setTop pb+ unless (S.disjoint s1 s2) $ setTop pb watchProp ps1 update watchProp ps2 update update++-- | The identity function. This is useful when tying the knot, to avoid a loop that bottoms out:+--+-- > let x = x in RS.get x+--+-- will not work, but+--+-- >>> let x = RS.id x in RS.get x+-- fromList []+--+-- does.+--+-- | prop> RS.get (RS.id s) === RS.get s+id :: RSet a -> RSet a+id = coerce $ Purify.def1 $ lift1 (Prelude.id :: S.Set a -> S.Set a)
README.md view
@@ -5,15 +5,16 @@ recursively, and still get a result out: >>> :{- let s1 = rInsert 23 s2- s2 = rInsert 42 s1- in getR s1+ let s1 = RS.insert 23 s2+ s2 = RS.insert 42 s1+ in RS.get s1 :} fromList [23,42] See the [`examples.hs`](examples.hs) file for more examples. -It also provides (unsafe) building blocks to build such APIs, see `Data.Recursive.R.Internal`.+It also provides (unsafe) building blocks to build such APIs, see+`Data.Propagator.Purify`. Related work ------------
System/IO/RecThunk.hs view
@@ -7,7 +7,7 @@ * 'thunk' is lazy in its argument, and does not run it directly * the first 'force' triggers execution of the action passed to thunk-* that action is run at most once, and returuns a list of other thunks+* that action is run at most once, and returns a list of other thunks * 'force' forces these thunks as well, and does not return before all of them have executed * Cycles are allowed: The action passed to 'thunk' may return a thunk whose action returns the first thunk. @@ -46,16 +46,17 @@ #ifdef DEJAFU -#define Ctxt MonadConc m =>+#define Ctxt (MonadConc m, MonadIO m) => #define Thunk_ (Thunk m) #define ResolvingState_ (ResolvingState m) #define KickedThunk_ (KickedThunk m)-#define ThreadId_ (ThreadId m) #define IORef_ IORef m #define MVar_ MVar m #define M m import Control.Concurrent.Classy hiding (wait)+import Data.Unique+import Control.Monad.IO.Class #else @@ -63,7 +64,6 @@ #define Thunk_ Thunk #define ResolvingState_ ResolvingState #define KickedThunk_ KickedThunk-#define ThreadId_ ThreadId #define IORef_ IORef #define MVar_ MVar #define M IO@@ -71,14 +71,14 @@ import Control.Concurrent.MVar import Control.Concurrent import Data.IORef+import Data.Unique+import Control.Monad.IO.Class #endif -- -- | An @IO@ action that is to be run at most once newtype Thunk_ = Thunk (MVar_ (Either (M [Thunk_]) KickedThunk_))-data ResolvingState_ = NotStarted | ProcessedBy ThreadId_ (MVar_ ()) | Done+data ResolvingState_ = NotStarted | ProcessedBy Unique (MVar_ ()) | Done -- | A 'Thunk' that is being evaluated data KickedThunk_ = KickedThunk (MVar_ [KickedThunk_]) (MVar_ ResolvingState_) @@ -118,9 +118,8 @@ putMVar t (Right kt) pure kt -wait :: Ctxt KickedThunk_ -> M ()-wait (KickedThunk mv_deps mv_s) = do- my_id <- myThreadId+wait :: Ctxt Unique -> KickedThunk_ -> M ()+wait my_id (KickedThunk mv_deps mv_s) = do s <- takeMVar mv_s case s of -- Thunk and all dependences are done@@ -138,7 +137,7 @@ done_mv <- newEmptyMVar putMVar mv_s (ProcessedBy my_id done_mv) ts <- readMVar mv_deps- mapM_ wait ts+ mapM_ (wait my_id) ts -- Mark kicked thunk as done _ <- swapMVar mv_s Done -- Wake up waiting threads@@ -150,4 +149,5 @@ force :: Ctxt Thunk_ -> M () force t = do rt <- kick t- wait rt+ my_id <- liftIO newUnique+ wait my_id rt
− dejafu.hs
@@ -1,203 +0,0 @@-import Test.DejaFu-import Control.Concurrent.Classy-import Control.Concurrent.Classy.Async-import qualified Data.Set as S-import System.Random-import Control.Monad-import Test.Tasty-import Test.Tasty.DejaFu--import Data.Recursive.Propagator.Naive-import Data.Recursive.Propagator.P2-import System.IO.RecThunk--t n = testGroup n . pure . testAuto--tr n = testGroup n . pure . testAutoWay (randomly (mkStdGen 0) 1000) defaultMemType--main = defaultMain $ testGroup "tests" $- [ t "prop 1" $ do- p1 <- newProp (S.singleton 1)- readProp p1-- , t "prop 2" $ do- p1 <- newProp (S.singleton 1)- p2 <- newProp S.empty- lift1 (S.insert 3) p1 p2- mapConcurrently readProp [p1, p2]-- , tr "prop 2 rec" $ withSetup (do- p1 <- newProp S.empty- p2 <- newProp S.empty- pure (p1, p2)) $ \(p1, p2) -> do- mapConcurrently id- [ lift1 (S.insert 3) p1 p2- , lift1 (S.insert 4) p2 p1- ]- mapConcurrently readProp [p1, p2]-- , tr "prop 2 rec plus" $ withSetup (do- p1 <- newProp S.empty- p2 <- newProp S.empty- p3 <- newProp S.empty- pure (p1, p2, p3)) $ \(p1, p2, p3) -> do- mapConcurrently id- [ lift1 (S.insert 3) p1 p2- , lift1 (S.insert 4) p2 p1- ]- mapConcurrently id- [ readProp p1- , readProp p2- , lift1 (S.insert 5) p2 p3 >> readProp p3- ]--- , tr "prop 3 rec" $ withSetup (do- p1 <- newProp S.empty- p2 <- newProp S.empty- p3 <- newProp S.empty- pure (p1, p2, p3)) $ \(p1, p2, p3) -> do- mapConcurrently id- [ lift1 (S.insert 3) p1 p2- , lift1 (S.insert 4) p2 p1- , lift1 (S.insert 5) p2 p3- ]- mapConcurrently readProp [p1, p2, p3]-- , tr "prop 3 rec variant" $ withSetup (do- p1 <- newProp S.empty- p2 <- newProp S.empty- p3 <- newProp S.empty- pure (p1, p2, p3)) $ \(p1, p2, p3) -> do- mapConcurrently id- [ lift1 (S.insert 4) p1 p2- , lift1 (S.insert 5) p2 p3- , lift2 (S.union) p2 p3 p1- ]- mapConcurrently readProp [p1, p2, p3]-- , tr "prop 4 rec" $ withSetup (do- p1 <- newProp S.empty- p2 <- newProp S.empty- p3 <- newProp S.empty- p4 <- newProp S.empty- pure (p1, p2, p3, p4)) $ \(p1, p2, p3, p4) -> do- mapConcurrently id- [ lift1 (S.insert 4) p1 p2- , lift2 (S.union) p1 p2 p3- , liftList (S.unions) [p1,p2,p3] p4- , lift1 (S.insert 5) p4 p1- ]- mapConcurrently readProp [p1, p2, p3, p4]- , t "thunk 1" $ do- obs1 <- newIORef 0- t1 <- thunk $ do- atomicModifyIORef' obs1 (\x -> (succ x, ()))- pure []- force t1- readIORef obs1- , t "thunk 1 rec" $ do- obs1 <- newIORef 0- t1ref <- newIORef undefined- t1 <- thunk $ do- atomicModifyIORef' obs1 (\x -> (succ x, ()))- t1 <- readIORef t1ref- pure [t1]- writeIORef t1ref t1- force t1- readIORef obs1- , t "thunk 2 rec 12" $ do- obs1 <- newIORef 0- obs2 <- newIORef 0- t2ref <- newIORef undefined- t1 <- thunk $ do- atomicModifyIORef' obs1 (\x -> (succ x, ()))- t2 <- readIORef t2ref- pure [t2]- t2 <- thunk $ do- atomicModifyIORef' obs1 (\x -> (succ x, ()))- pure [t1]- writeIORef t2ref t2- mapConcurrently id- [ force t1 >> mapM readIORef [obs1, obs2]- , force t2 >> mapM readIORef [obs1, obs2]- ]- , tr "thunk 2 rec 112" $ do- obs1 <- newIORef 0- obs2 <- newIORef 0- t2ref <- newIORef undefined- t1 <- thunk $ do- atomicModifyIORef' obs1 (\x -> (succ x, ()))- t2 <- readIORef t2ref- pure [t2]- t2 <- thunk $ do- atomicModifyIORef' obs1 (\x -> (succ x, ()))- pure [t1]- writeIORef t2ref t2- mapConcurrently id- [ force t1 >> mapM readIORef [obs1, obs2]- , force t1 >> mapM readIORef [obs1, obs2]- , force t2 >> mapM readIORef [obs1, obs2]- ]- , tr "thunk 2 all-rec 112" $ do- obs1 <- newIORef 0- obs2 <- newIORef 0- t1ref <- newIORef undefined- t2ref <- newIORef undefined- t1 <- thunk $ do- atomicModifyIORef' obs1 (\x -> (succ x, ()))- t1 <- readIORef t1ref- t2 <- readIORef t2ref- pure [t2,t1]- writeIORef t1ref t1- t2 <- thunk $ do- atomicModifyIORef' obs1 (\x -> (succ x, ()))- t2 <- readIORef t2ref- pure [t1,t2]- writeIORef t2ref t2- mapConcurrently id- [ force t1 >> mapM readIORef [obs1, obs2]- , force t1 >> mapM readIORef [obs1, obs2]- , force t2 >> mapM readIORef [obs1, obs2]- ]- , t "P2 1" $ do- p1 <- newP2- False <- isTop p1- setTop p1- True <- isTop p1- pure ()- , t "P2 2" $ do- p1 <- newP2- p2 <- newP2- mapConcurrently id- [ do- False <- isTop p1- setTop p1- True <- isTop p1- pure ()- , do- False <- isTop p2- p1 `implies` p2- ]- True <- isTop p2- pure ()- , t "P2 2 rec bottom" $ do- p1 <- newP2- p2 <- newP2- mapConcurrently id- [ p1 `implies` p2- , p2 `implies` p1- ]- [False, False] <- mapM isTop [p1,p2]- pure ()- , t "P2 2 rec top" $ do- p1 <- newP2- p2 <- newP2- mapConcurrently id- [ p1 `implies` p2- , p2 `implies` p1- , setTop p1- ]- [True, True] <- mapM isTop [p1,p2]- pure ()- ]
− doctests.hs
@@ -1,2 +0,0 @@-import Test.DocTest-main = doctest ["--fast", "-package=QuickCheck", "Data/"]
examples.hs view
@@ -18,37 +18,40 @@ This library provides data types where this works. You can write the equations in that way just fine, and still get a result. -For example, the @R Bool@ type comes with functions that look quite like their+For example, the 'Data.Recursive.Bool.RBool' type comes with functions that look quite like their ordinary counterparts acting on 'Bool'. ->>> :t rTrue-rTrue :: R Bool->>> :t rFalse-rFalse :: R Bool->>> :t (|||)-(|||) :: R Bool -> R Bool -> R Bool->>> :t (&&&)-(&&&) :: R Bool -> R Bool -> R Bool->>> getR rTrue+>>> import Data.Recursive.Bool (RBool)+>>> import qualified Data.Recursive.Bool as RB++>>> :t RB.true+RB.true :: RBool+>>> :t RB.false+RB.false :: RBool+>>> :t (RB.||)+(RB.||) :: RBool -> RBool -> RBool+>>> :t (RB.&&)+(RB.&&) :: RBool -> RBool -> RBool+>>> RB.get RB.true True->>> getR rFalse+>>> RB.get RB.false False->>> getR (rFalse &&& rTrue)+>>> RB.get (RB.false RB.&& RB.true) False->>> getR (rTrue &&& rTrue)+>>> RB.get (RB.true RB.&& RB.true) True->>> getR (ror [rTrue, rFalse, rTrue])+>>> RB.get (RB.or [RB.true, RB.false, RB.true]) True So far so good, lets see what happens when we try something recursive: ->>> let x = ror [y]; y = rand [x, rFalse] in getR x+>>> let x = RB.or [y]; y = RB.and [x, RB.false] in RB.get x False->>> let x = ror [y]; y = ror [x, rFalse] in getR x+>>> let x = RB.or [y]; y = RB.or [x, RB.false] in RB.get x False->>> let x = ror [y]; y = ror [x, rTrue] in getR x+>>> let x = RB.or [y]; y = RB.or [x, RB.true] in RB.get x True->>> let x = ror [y]; y = ror [x] in getR x+>>> let x = RB.or [y]; y = RB.or [x] in RB.get x False == Least or greatest solution@@ -60,42 +63,45 @@ We (arbitrary) choose to find the least solution, i.e. prefer @False@ and only find @True@ if we have to. This is useful, for example, if you check something recursive for errors. -Sometimes you want the other one. Then you can use @R (Dual Bool)@. The module-"Data.Recursive.DualBool" exports all the functions for that type too. Because-of the name class we have imported it qualified here. We can run run the same-quations, and get different answers:+Sometimes you want the other one. Then you can use @RDualBool@. The module+"Data.Recursive.DualBool" exports all the functions for that type too. We can+run the same equations, and get different answers: ->>> let x = DB.ror [y]; y = DB.rand [x, DB.rFalse] in getRDual x+>>> import Data.Recursive.DualBool (RDualBool)+>>> import qualified Data.Recursive.DualBool as RDB+++>>> let x = RDB.or [y]; y = RDB.and [x, RDB.false] in RDB.get x False->>> let x = DB.ror [y]; y = DB.ror [x, DB.rFalse] in getRDual x+>>> let x = RDB.or [y]; y = RDB.or [x, RDB.false] in RDB.get x True->>> let x = DB.ror [y]; y = DB.ror [x, DB.rTrue] in getRDual x+>>> let x = RDB.or [y]; y = RDB.or [x, RDB.true] in RDB.get x True->>> let x = DB.ror [y]; y = DB.ror [x] in getRDual x+>>> let x = RDB.or [y]; y = RDB.or [x] in RDB.get x True The negation function is also available, and goes from can-be-true to must-be-true and back: ->>> :t rnot-rnot :: R (Dual Bool) -> R Bool->>> :t DB.rnot-DB.rnot :: R Bool -> R (Dual Bool)+>>> :t RB.not+RB.not :: RDualBool -> RBool+>>> :t RDB.not+RDB.not :: RBool -> RDualBool This allows us to mix the different types in the same computation: >>> :{- let x = rnot y ||| rnot z- y = DB.rnot x DB.&&& z- z = DB.rTrue- in (getR x, getRDual y, getRDual z)+ let x = RB.not y RB.|| RB.not z+ y = RDB.not x RDB.&& z+ z = RDB.true+ in (RB.get x, RDB.get y, RDB.get z) :} (False,True,True) >>> :{- let x = rnot y ||| rnot z- y = DB.rnot x DB.&&& z- z = DB.rFalse- in (getR x, getRDual y, getRDual z)+ let x = RB.not y RB.|| RB.not z+ y = RDB.not x RDB.&& z+ z = RDB.false+ in (RB.get x, RDB.get y, RDB.get z) :} (True,False,False) @@ -104,27 +110,29 @@ We do not have to stop with booleans, and can define similar APIs for other data stuctures, e.g. sets: -Again we can describe sets recursively, using the monotone functions 'rEmpty',-'rInsert' and 'rUnion'+>>> import qualified Data.Recursive.Set as RS +Again we can describe sets recursively, using the monotone functions 'RS.empty',+'RS.insert' and 'RS.union'+ >>> :{- let s1 = rInsert 23 s2- s2 = rInsert 42 s1- in getR s1+ let s1 = RS.insert 23 s2+ s2 = RS.insert 42 s1+ in RS.get s1 :} fromList [23,42] -Here is a slightly larger example, where we can can use this API to elegantly+Here is a slightly larger example, where we can use this API to elegantly calculate the reachable nodes in a graph (represented as a map from vertices to their successors), using a typical knot-tying approach. But unless with plain 'S.Set', it now works even if the graph has cycles: >>> :{ reachable :: M.Map Int [Int] -> M.Map Int (S.Set Int)- reachable g = fmap getR sets+ reachable g = fmap RS.get sets where- sets :: M.Map Int (R (S.Set Int))- sets = M.mapWithKey (\v vs -> rInsert v (rUnions [ sets ! v' | v' <- vs ])) g+ sets :: M.Map Int (RS.RSet Int)+ sets = M.mapWithKey (\v vs -> RS.insert v (RS.unions [ sets ! v' | v' <- vs ])) g :} >>> let graph = M.fromList [(1,[2,3]),(2,[1]),(3,[])]@@ -137,37 +145,37 @@ Of course, the magic stops somewhere: Just like with the usual knot-tying tricks, you still have to make sure to be lazy enough. In particular, you should-not peek at the value (e.g. using 'getR') while you are building the graph:+not peek at the value (e.g. using 'RB.get') while you are building the graph: >>> :{ withTimeout $- let x = rand [x, if getR y then z else rTrue]- y = rand [x, rTrue]- z = rFalse- in getR y+ let x = RB.and [x, if RB.get y then z else RB.true]+ y = RB.and [x, RB.true]+ z = RB.false+ in RB.get y :} *** Exception: timed out Similarly, you have to make sure you recurse through one of these functions; @let x = x@ still does not work: ->>> withTimeout $ let x = x :: R Bool in getR x+>>> withTimeout $ let x = x :: RBool in RB.get x *** Exception: timed out->>> withTimeout $ let x = x &&& x in getR x+>>> withTimeout $ let x = x RB.&& x in RB.get x False We belive that the APIs provided here are still “pure”: evaluation order does not affect the results, and you can replace equals with equals, in the sense that -> let s = rInsert 42 s in s+> let s = RS.insert 42 s in s is the same as -> let s = rInsert 42 s in rInsert 42 s+> let s = RS.insert 42 s in RS.insert 42 s However, the the following two expressions are not equivalent: ->>> withTimeout $ S.toList $ let s = rInsert 42 s in getR s+>>> withTimeout $ S.toList $ let s = RS.insert 42 s in RS.get s [42]->>> withTimeout $ S.toList $ let s () = rInsert 42 (s ()) in getR (s ())+>>> withTimeout $ S.toList $ let s () = RS.insert 42 (s ()) in RS.get (s ()) *** Exception: timed out It is debatable if that is a problem.@@ -175,11 +183,11 @@ -} module Data.Recursive.Examples () where -import Data.Recursive.R-import Data.Recursive.Bool-import qualified Data.Recursive.DualBool as DB-import Data.Recursive.Set-import Data.Monoid+-- Imports for haddock++import qualified Data.Recursive.Bool as RB+import qualified Data.Recursive.DualBool as RDB+import qualified Data.Recursive.Set as RS -- $setup --
rec-def.cabal view
@@ -1,14 +1,14 @@ cabal-version: 2.4 name: rec-def-version: 0.1-synopsis: Recusively defined values+version: 0.2+synopsis: Recursively defined values description: This library provides safe APIs that allow you to define and calculate values recursively, and still get a result out: .- > let s1 = rInsert 23 s2- > s2 = rInsert 42 s1- > in getR s1+ > let s1 = RS.insert 23 s2+ > s2 = RS.insert 42 s1+ > in RS.get s1 . will not loop, but rather produces the set @fromList [23,42]@ .@@ -16,18 +16,19 @@ . * "Data.Recursive.Bool" * "Data.Recursive.Set"+ * "Data.Recursive.Map" * "Data.Recursive.DualBool" .- More APIs (e.g. for 'Natural') can be added over time, as need and good+ More APIs (e.g. for maps or 'Natural') can be added over time, as need and good use-cases arise. . For the (unsafe) building blocks to build such APIs, see .- * "Data.Recursive.R.Internal" for the wrapper that turns an IO-implemented+ * "Data.Propagator.Purify" for the wrapper that turns an IO-implemented propagator into a pure data structure- * "Data.Recursive.Propagator.Naive" for a naive propagator implementation- * "Data.Recursive.Propagator.P2" for a smarter propagator implementation for+ * "Data.Propagator.Naive" for a naive propagator implementation+ * "Data.Propagator.P2" for a smarter propagator implementation for the two-point lattice, i.e. 'Bool' . The library is not (yet) focussed on performance, and uses a rather naive@@ -56,13 +57,14 @@ exposed-modules: Data.Recursive.Bool exposed-modules: Data.Recursive.DualBool exposed-modules: Data.Recursive.Set+ exposed-modules: Data.Recursive.Map+ exposed-modules: Data.Recursive.Internal exposed-modules: Data.POrder exposed-modules: System.IO.RecThunk- exposed-modules: Data.Recursive.R- exposed-modules: Data.Recursive.R.Internal- exposed-modules: Data.Recursive.Propagator.Naive- exposed-modules: Data.Recursive.Propagator.Class- exposed-modules: Data.Recursive.Propagator.P2+ exposed-modules: Data.Propagator.Purify+ exposed-modules: Data.Propagator.Naive+ exposed-modules: Data.Propagator.Class+ exposed-modules: Data.Propagator.P2 build-depends: base >= 4.9 && < 5 build-depends: containers >= 0.5.11 && < 0.7@@ -74,6 +76,7 @@ main-is: doctests.hs default-language: Haskell2010 ghc-options: -threaded+ hs-source-dirs: tests build-depends: rec-def build-depends: base >= 4.9 && < 5@@ -81,13 +84,24 @@ build-depends: QuickCheck build-depends: template-haskell +test-suite spaceleak+ type: exitcode-stdio-1.0+ main-is: spaceleak.hs+ hs-source-dirs: tests+ default-language: Haskell2010+ build-depends: rec-def+ build-depends: base >= 4.9 && < 5+ build-depends: containers >= 0.5.11 && < 0.7 test-suite dejafu type: exitcode-stdio-1.0 other-modules: System.IO.RecThunk- other-modules: Data.Recursive.Propagator.Naive- other-modules: Data.Recursive.Propagator.P2+ other-modules: Data.POrder+ other-modules: Data.Propagator.Class+ other-modules: Data.Propagator.Naive+ other-modules: Data.Propagator.P2 main-is: dejafu.hs+ hs-source-dirs: tests . default-language: Haskell2010 ghc-options: -threaded cpp-options: -DDEJAFU@@ -97,7 +111,7 @@ build-depends: concurrency ^>= 1.11.0.2 build-depends: dejafu ^>= 2.4.0.3 build-depends: tasty- build-depends: tasty-dejafu+ build-depends: tasty-dejafu ^>= 2.1.0.0 build-depends: random source-repository head
+ tests/dejafu.hs view
@@ -0,0 +1,203 @@+import Test.DejaFu+import Control.Concurrent.Classy+import Control.Concurrent.Classy.Async+import qualified Data.Set as S+import System.Random+import Control.Monad+import Test.Tasty+import Test.Tasty.DejaFu++import Data.Propagator.Naive+import Data.Propagator.P2+import System.IO.RecThunk++t n = testAuto n++tr n = testAutoWay (randomly (mkStdGen 0) 1000) defaultMemType n++main = defaultMain $ testGroup "tests" $+ [ t "prop 1" $ do+ p1 <- newProp (S.singleton 1)+ readProp p1++ , t "prop 2" $ do+ p1 <- newProp (S.singleton 1)+ p2 <- newProp S.empty+ lift1 (S.insert 3) p1 p2+ mapConcurrently readProp [p1, p2]++ , tr "prop 2 rec" $ withSetup (do+ p1 <- newProp S.empty+ p2 <- newProp S.empty+ pure (p1, p2)) $ \(p1, p2) -> do+ mapConcurrently id+ [ lift1 (S.insert 3) p1 p2+ , lift1 (S.insert 4) p2 p1+ ]+ mapConcurrently readProp [p1, p2]++ , tr "prop 2 rec plus" $ withSetup (do+ p1 <- newProp S.empty+ p2 <- newProp S.empty+ p3 <- newProp S.empty+ pure (p1, p2, p3)) $ \(p1, p2, p3) -> do+ mapConcurrently id+ [ lift1 (S.insert 3) p1 p2+ , lift1 (S.insert 4) p2 p1+ ]+ mapConcurrently id+ [ readProp p1+ , readProp p2+ , lift1 (S.insert 5) p2 p3 >> readProp p3+ ]+++ , tr "prop 3 rec" $ withSetup (do+ p1 <- newProp S.empty+ p2 <- newProp S.empty+ p3 <- newProp S.empty+ pure (p1, p2, p3)) $ \(p1, p2, p3) -> do+ mapConcurrently id+ [ lift1 (S.insert 3) p1 p2+ , lift1 (S.insert 4) p2 p1+ , lift1 (S.insert 5) p2 p3+ ]+ mapConcurrently readProp [p1, p2, p3]++ , tr "prop 3 rec variant" $ withSetup (do+ p1 <- newProp S.empty+ p2 <- newProp S.empty+ p3 <- newProp S.empty+ pure (p1, p2, p3)) $ \(p1, p2, p3) -> do+ mapConcurrently id+ [ lift1 (S.insert 4) p1 p2+ , lift1 (S.insert 5) p2 p3+ , lift2 (S.union) p2 p3 p1+ ]+ mapConcurrently readProp [p1, p2, p3]++ , tr "prop 4 rec" $ withSetup (do+ p1 <- newProp S.empty+ p2 <- newProp S.empty+ p3 <- newProp S.empty+ p4 <- newProp S.empty+ pure (p1, p2, p3, p4)) $ \(p1, p2, p3, p4) -> do+ mapConcurrently id+ [ lift1 (S.insert 4) p1 p2+ , lift2 (S.union) p1 p2 p3+ , liftList (S.unions) [p1,p2,p3] p4+ , lift1 (S.insert 5) p4 p1+ ]+ mapConcurrently readProp [p1, p2, p3, p4]+ , t "thunk 1" $ do+ obs1 <- newIORef 0+ t1 <- thunk $ do+ atomicModifyIORef' obs1 (\x -> (succ x, ()))+ pure []+ force t1+ readIORef obs1+ , t "thunk 1 rec" $ do+ obs1 <- newIORef 0+ t1ref <- newIORef undefined+ t1 <- thunk $ do+ atomicModifyIORef' obs1 (\x -> (succ x, ()))+ t1 <- readIORef t1ref+ pure [t1]+ writeIORef t1ref t1+ force t1+ readIORef obs1+ , t "thunk 2 rec 12" $ do+ obs1 <- newIORef 0+ obs2 <- newIORef 0+ t2ref <- newIORef undefined+ t1 <- thunk $ do+ atomicModifyIORef' obs1 (\x -> (succ x, ()))+ t2 <- readIORef t2ref+ pure [t2]+ t2 <- thunk $ do+ atomicModifyIORef' obs1 (\x -> (succ x, ()))+ pure [t1]+ writeIORef t2ref t2+ mapConcurrently id+ [ force t1 >> mapM readIORef [obs1, obs2]+ , force t2 >> mapM readIORef [obs1, obs2]+ ]+ , tr "thunk 2 rec 112" $ do+ obs1 <- newIORef 0+ obs2 <- newIORef 0+ t2ref <- newIORef undefined+ t1 <- thunk $ do+ atomicModifyIORef' obs1 (\x -> (succ x, ()))+ t2 <- readIORef t2ref+ pure [t2]+ t2 <- thunk $ do+ atomicModifyIORef' obs1 (\x -> (succ x, ()))+ pure [t1]+ writeIORef t2ref t2+ mapConcurrently id+ [ force t1 >> mapM readIORef [obs1, obs2]+ , force t1 >> mapM readIORef [obs1, obs2]+ , force t2 >> mapM readIORef [obs1, obs2]+ ]+ , tr "thunk 2 all-rec 112" $ do+ obs1 <- newIORef 0+ obs2 <- newIORef 0+ t1ref <- newIORef undefined+ t2ref <- newIORef undefined+ t1 <- thunk $ do+ atomicModifyIORef' obs1 (\x -> (succ x, ()))+ t1 <- readIORef t1ref+ t2 <- readIORef t2ref+ pure [t2,t1]+ writeIORef t1ref t1+ t2 <- thunk $ do+ atomicModifyIORef' obs1 (\x -> (succ x, ()))+ t2 <- readIORef t2ref+ pure [t1,t2]+ writeIORef t2ref t2+ mapConcurrently id+ [ force t1 >> mapM readIORef [obs1, obs2]+ , force t1 >> mapM readIORef [obs1, obs2]+ , force t2 >> mapM readIORef [obs1, obs2]+ ]+ , t "P2 1" $ do+ p1 <- newP2+ False <- isTop p1+ setTop p1+ True <- isTop p1+ pure ()+ , t "P2 2" $ do+ p1 <- newP2+ p2 <- newP2+ mapConcurrently id+ [ do+ False <- isTop p1+ setTop p1+ True <- isTop p1+ pure ()+ , do+ False <- isTop p2+ p1 `implies` p2+ ]+ True <- isTop p2+ pure ()+ , t "P2 2 rec bottom" $ do+ p1 <- newP2+ p2 <- newP2+ mapConcurrently id+ [ p1 `implies` p2+ , p2 `implies` p1+ ]+ [False, False] <- mapM isTop [p1,p2]+ pure ()+ , t "P2 2 rec top" $ do+ p1 <- newP2+ p2 <- newP2+ mapConcurrently id+ [ p1 `implies` p2+ , p2 `implies` p1+ , setTop p1+ ]+ [True, True] <- mapM isTop [p1,p2]+ pure ()+ ]
+ tests/doctests.hs view
@@ -0,0 +1,8 @@+import Test.DocTest+main = do+ -- Why do I have to call them separately?+ doctest ["--fast", "-package=QuickCheck","Data/Recursive/Bool.hs"]+ doctest ["--fast", "-package=QuickCheck","Data/Recursive/DualBool.hs"]+ doctest ["--fast", "-package=QuickCheck","Data/Recursive/Set.hs"]+ doctest ["--fast", "-package=QuickCheck","Data/Recursive/Map.hs"]+ doctest ["--fast", "-package=QuickCheck","Data/Recursive/Examples.hs"]
+ tests/spaceleak.hs view
@@ -0,0 +1,105 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NumericUnderscores #-}++{-|+This test checks that resolved cells do no longer hold on to references to+dependent cells, to avoid space leaks, especially with the “constant global”+cells like 'RS.empty'.+-}++module Main where++import qualified Data.Set as S+import qualified Data.Recursive.Set as RS+import Data.Recursive.Internal+import Data.Propagator.Purify++import Data.IORef+import System.Mem.Weak+import System.Mem+import System.Exit+import System.Environment+import Control.Concurrent++main = do+ n <- length <$> getArgs++ putStrLn "Test 1: Normal GC (sanity check)"+ gc <- newIORef False+ let x = 1000_000_001 + n+ addFinalizer x $ do+ putStrLn "Finalizer running"+ writeIORef gc True+ let s = RS.insert x s+ print (RS.get s)++ putStrLn "Running GC"+ performMajorGC+ threadDelay 1_000_000++ readIORef gc >>= \case+ True -> putStrLn "GC seems to be working"+ False -> putStrLn "This really ought to work" >> exitFailure+++ putStrLn "Test 2: Dependency on RS.empty"+ gc <- newIORef False+ let x = 1000_000_002 + n+ addFinalizer x $ do+ putStrLn "Finalizer running"+ writeIORef gc True+ let s = RS.insert x RS.empty+ print (RS.get s)++ putStrLn "Running GC"+ performMajorGC+ threadDelay 1_000_000++ readIORef gc >>= \case+ True -> putStrLn "Good!"+ False -> putStrLn "We got a leak" >> exitFailure++ putStrLn "Test 3: Dependency on constant set"+ gc <- newIORef False+ let x0 = 1000_000_003 + n+ let s' = RS.mk (S.singleton x0)+ let x1 = 1000_000_004 + n+ addFinalizer x1 $ do+ putStrLn "Finalizer running"+ writeIORef gc True+ let s = RS.insert x1 s'+ print (RS.get s)++ putStrLn "Running GC"+ performMajorGC+ threadDelay 1_000_000++ readIORef gc >>= \case+ True -> putStrLn "Good!"+ False -> putStrLn "We got a leak" >> exitFailure++ putStrLn "Test 4: Dependency on recursive set"+ gc <- newIORef False+ let x0 = 1000_000_005 + n+ let sr = RS.insert x0 sr+ let x1 = 1000_000_007 + n+ addFinalizer x1 $ do+ putStrLn "Finalizer running"+ writeIORef gc True+ let s = RS.insert x1 sr+ print (RS.get s)++ putStrLn "Running GC"+ performMajorGC+ threadDelay 1_000_000++ readIORef gc >>= \case+ True -> putStrLn "Good!"+ False -> putStrLn "We got a leak" >> exitFailure++ -- This is needed, else RS.empty itself is GC’ed+ putStrLn "Keeping a few things alive"+ print (RS.get s')+ print (RS.get sr)+ print (RS.get RS.empty :: S.Set Int)+