Merge pull request #340 from edwinb/strefs

Control.Monad.ST and Refs interface

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:
 

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)

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

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,

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

tests/chez/chez025/expected

@@ -0,0 +1,3 @@
+500500
+1/1: Building runst (runst.idr)
+Main> Main> Bye for now!

tests/chez/chez025/input

@@ -0,0 +1,2 @@
+:exec printLn (stsum [1..1000])
+:q

tests/chez/chez025/run

@@ -0,0 +1,3 @@
+$1 --no-banner runst.idr < input
+
+rm -rf build

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