diff --git a/CHANGELOG.md b/CHANGELOG.md index 579cd748a..75196a1b1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -26,6 +26,9 @@ Library changes: + Anything in `Data.Linear` in `contrib`, just like the rest of `contrib`, should be considered experimental with the API able to change at any time! Further experiments in `Data.Linear` are welcome :). +* Added `Control.Monad.ST`, for update in-place via `STRef` (which is like + `IORef`, but can escape from `IO`). Also added `Data.Ref` which provides an + interface to both `IORef` and `STRef`. Command-line options changes: diff --git a/libs/base/Control/Monad/ST.idr b/libs/base/Control/Monad/ST.idr new file mode 100644 index 000000000..8b9157612 --- /dev/null +++ b/libs/base/Control/Monad/ST.idr @@ -0,0 +1,56 @@ +module Control.Monad.ST + +import Data.IORef + +export +data STRef : Type -> Type -> Type where + MkSTRef : IORef a -> STRef s a + +export +data ST : Type -> Type -> Type where + MkST : IO a -> ST s a + +export +runST : (forall s . ST s a) -> a +runST p + = let MkST prog = p {s = ()} in -- anything will do :) + unsafePerformIO prog + +mutual + export + Functor (ST s) where + map fn st = pure $ fn !st + + export + Applicative (ST s) where + pure = MkST . pure + (<*>) f a = pure $ !f !a + + export + Monad (ST s) where + MkST p >>= k + = MkST $ do p' <- p + let MkST kp = k p' + kp + +export +newSTRef : a -> ST s (STRef s a) +newSTRef val + = MkST $ do r <- newIORef val + pure (MkSTRef r) + +%inline +export +readSTRef : STRef s a -> ST s a +readSTRef (MkSTRef r) = MkST $ readIORef r + +%inline +export +writeSTRef : STRef s a -> (val : a) -> ST s () +writeSTRef (MkSTRef r) val = MkST $ writeIORef r val + +export +modifySTRef : STRef s a -> (a -> a) -> ST s () +modifySTRef ref f + = do val <- readSTRef ref + writeSTRef ref (f val) diff --git a/libs/base/Data/Ref.idr b/libs/base/Data/Ref.idr new file mode 100644 index 000000000..7d3439248 --- /dev/null +++ b/libs/base/Data/Ref.idr @@ -0,0 +1,22 @@ +module Data.Ref + +import public Data.IORef +import public Control.Monad.ST + +public export +interface Ref m (r : Type -> Type) | m where + newRef : a -> m (r a) + readRef : r a -> m a + writeRef : r a -> a -> m () + +export +Ref IO IORef where + newRef = newIORef + readRef = readIORef + writeRef = writeIORef + +export +Ref (ST s) (STRef s) where + newRef = newSTRef + readRef = readSTRef + writeRef = writeSTRef diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg index 9d7e0bbdc..115140d38 100644 --- a/libs/base/base.ipkg +++ b/libs/base/base.ipkg @@ -5,6 +5,7 @@ modules = Control.App, Control.App.FileIO, Control.Monad.Identity, + Control.Monad.ST, Control.Monad.State, Control.Monad.Trans, Control.WellFounded, @@ -27,6 +28,7 @@ modules = Control.App, Data.Nat, Data.Nat.Views, Data.Primitives.Views, + Data.Ref, Data.So, Data.Stream, Data.Strings, diff --git a/tests/Main.idr b/tests/Main.idr index 6bff484c0..101401e01 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -114,6 +114,7 @@ chezTests "chez007", "chez008", "chez009", "chez010", "chez011", "chez012", "chez013", "chez014", "chez015", "chez016", "chez017", "chez018", "chez019", "chez020", "chez021", "chez022", "chez023", "chez024", + "chez025", "reg001"] ideModeTests : List String diff --git a/tests/chez/chez025/expected b/tests/chez/chez025/expected new file mode 100644 index 000000000..5d2a00c21 --- /dev/null +++ b/tests/chez/chez025/expected @@ -0,0 +1,3 @@ +500500 +1/1: Building runst (runst.idr) +Main> Main> Bye for now! diff --git a/tests/chez/chez025/input b/tests/chez/chez025/input new file mode 100644 index 000000000..a49cdbb44 --- /dev/null +++ b/tests/chez/chez025/input @@ -0,0 +1,2 @@ +:exec printLn (stsum [1..1000]) +:q diff --git a/tests/chez/chez025/run b/tests/chez/chez025/run new file mode 100755 index 000000000..de7d06ee0 --- /dev/null +++ b/tests/chez/chez025/run @@ -0,0 +1,3 @@ +$1 --no-banner runst.idr < input + +rm -rf build diff --git a/tests/chez/chez025/runst.idr b/tests/chez/chez025/runst.idr new file mode 100644 index 000000000..1416b1999 --- /dev/null +++ b/tests/chez/chez025/runst.idr @@ -0,0 +1,15 @@ +import Data.Ref + +stsum : Num a => List a -> a +stsum xs + = runST $ + do acc <- newRef 0 + add xs acc + readRef acc + where + add : List a -> STRef s a -> ST s () + add [] ref = pure () + add (x :: xs) ref + = do acc <- readRef ref + writeRef ref (acc + x) + add xs ref