From 80b1b3581a409c2549275ad6df87edfbef21d064 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Tue, 19 Sep 2023 00:41:47 +0200 Subject: [PATCH] use ST from base --- lib/Control/Monad/ST/Extra.idr | 64 ++++++++++++++++++++ lib/Quox/EffExtra.idr | 6 +- lib/Quox/Parser/FromParser.idr | 10 ++-- lib/Quox/Pretty.idr | 4 +- lib/Quox/ST.idr | 106 --------------------------------- lib/quox-lib.ipkg | 2 +- tests/Tests/Reduce.idr | 5 +- tests/TypingImpls.idr | 4 +- 8 files changed, 80 insertions(+), 121 deletions(-) create mode 100644 lib/Control/Monad/ST/Extra.idr delete mode 100644 lib/Quox/ST.idr diff --git a/lib/Control/Monad/ST/Extra.idr b/lib/Control/Monad/ST/Extra.idr new file mode 100644 index 0000000..52e16ee --- /dev/null +++ b/lib/Control/Monad/ST/Extra.idr @@ -0,0 +1,64 @@ +module Control.Monad.ST.Extra + +import public Control.Monad.ST +import Data.IORef +import Control.MonadRec + +%default total + +export %inline +MonadRec (ST s) where + tailRecM seed (Access rec) st f = MkST $ do + let MkST io = f seed st + case !io of + Done res => pure res + Cont seed2 prf vst => + let MkST io = tailRecM seed2 (rec seed2 prf) vst f in io + + +public export +interface HasST (0 m : Type -> Type -> Type) where + liftST : ST s a -> m s a + +export %inline HasST ST where liftST = id + + +public export +record STErr e s a where + constructor STE + fromSTErr : ST s (Either e a) + +export +Functor (STErr e s) where + map f (STE e) = STE $ map f <$> e + +export +Applicative (STErr e s) where + pure x = STE $ pure $ pure x + STE f <*> STE x = STE [|f <*> x|] + +export +Monad (STErr e s) where + STE m >>= k = STE $ do + case !m of + Left err => pure $ Left err + Right x => fromSTErr $ k x + +export +MonadRec (STErr e s) where + tailRecM s (Access r) x k = STE $ do + let STE m = k s x + case !m of + Left err => pure $ Left err + Right (Cont s' p y) => fromSTErr $ tailRecM s' (r s' p) y k + Right (Done y) => pure $ Right y + +export +runSTErr : (forall s. STErr e s a) -> Either e a +runSTErr ste = runST $ fromSTErr ste + +export %inline HasST (STErr e) where liftST = STE . map Right + +export +stLeft : e -> STErr e s a +stLeft e = STE $ pure $ Left e diff --git a/lib/Quox/EffExtra.idr b/lib/Quox/EffExtra.idr index 85420f7..d3c3692 100644 --- a/lib/Quox/EffExtra.idr +++ b/lib/Quox/EffExtra.idr @@ -2,7 +2,7 @@ module Quox.EffExtra import public Control.Eff -import Quox.ST +import Control.Monad.ST.Extra import Data.IORef @@ -43,8 +43,8 @@ handleStateIORef r (Put s) = writeIORef r s export handleStateSTRef : HasST m => STRef s st -> StateL lbl st a -> m s a -handleStateSTRef r Get = readRef r -handleStateSTRef r (Put s) = writeRef r s +handleStateSTRef r Get = liftST $ readSTRef r +handleStateSTRef r (Put s) = liftST $ writeSTRef r s diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index 63f8055..9c2fdcd 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -12,7 +12,7 @@ import Data.List import Data.Maybe import Data.SnocVect import Quox.EffExtra -import Quox.ST +import Control.Monad.ST.Extra import System.File import System.Path @@ -346,14 +346,14 @@ fromParserPure : NameSuf -> Definitions -> Eff FromParserPure a -> Either Error (a, NameSuf, Definitions) fromParserPure suf defs act = runSTErr $ do - suf <- newRef suf - defs <- newRef defs + suf <- liftST $ newSTRef suf + defs <- liftST $ newSTRef defs res <- runEff act $ with Union.(::) [handleExcept (\e => stLeft e), handleStateSTRef defs, - handleStateSTRef !(newRef [<]), + handleStateSTRef !(liftST $ newSTRef [<]), handleStateSTRef suf] - pure (res, !(readRef suf), !(readRef defs)) + pure (res, !(liftST $ readSTRef suf), !(liftST $ readSTRef defs)) export covering diff --git a/lib/Quox/Pretty.idr b/lib/Quox/Pretty.idr index 7d8c80c..6a8f011 100644 --- a/lib/Quox/Pretty.idr +++ b/lib/Quox/Pretty.idr @@ -3,7 +3,7 @@ module Quox.Pretty import Quox.Loc import Quox.Name -import Quox.ST +import Control.Monad.ST.Extra import public Text.PrettyPrint.Bernardy import public Text.PrettyPrint.Bernardy.Core.Decorate import public Quox.EffExtra @@ -68,7 +68,7 @@ runPrettyWith : PPrec -> Flavor -> (HL -> Highlight) -> Nat -> runPrettyWith prec flavor highlight indent act = runST $ do runEff act $ with Union.(::) - [handleStateSTRef !(newRef prec), + [handleStateSTRef !(newSTRef prec), handleReaderConst flavor, handleReaderConst highlight, handleReaderConst indent] diff --git a/lib/Quox/ST.idr b/lib/Quox/ST.idr deleted file mode 100644 index a900c7f..0000000 --- a/lib/Quox/ST.idr +++ /dev/null @@ -1,106 +0,0 @@ -module Quox.ST - -import Data.IORef -import Control.MonadRec - - -export -Tag : Type -Tag = () -- shhh don't tell anyone - -export -record ST (s : Tag) a where - constructor MkST - action : IO a -%name ST st - -export -runST : (forall s. ST s a) -> a -runST st = unsafePerformIO (st {s = ()}).action - -export %inline Functor (ST s) where map f st = MkST $ map f st.action - -export %inline -Applicative (ST s) where - pure = MkST . pure - f <*> x = MkST $ f.action <*> x.action - -export %inline Monad (ST s) where m >>= k = MkST $ m.action >>= action . k - -export %inline -MonadRec (ST s) where - tailRecM s (Access r) x k = MkST $ do - let MkST yy = k s x - case !yy of - Done y => pure y - Cont s2 p y => let MkST z = tailRecM s2 (r s2 p) y k in z - - -public export -interface HasST (0 m : Tag -> Type -> Type) where - liftST : ST s a -> m s a - -export %inline HasST ST where liftST = id - -export -record STRef (s : Tag) a where - constructor MkSTRef - ref : IORef a -%name STRef r - -export %inline -newRef : HasST m => a -> m s (STRef s a) -newRef x = liftST $ MkST $ MkSTRef <$> newIORef x - -export %inline -readRef : HasST m => STRef s a -> m s a -readRef r = liftST $ MkST $ readIORef r.ref - -export %inline -writeRef : HasST m => STRef s a -> a -> m s () -writeRef r x = liftST $ MkST $ writeIORef r.ref x - -export %inline -modifyRef : HasST m => STRef s a -> (a -> a) -> m s () -modifyRef r f = liftST $ MkST $ modifyIORef r.ref f - - -public export -record STErr e (s : Tag) a where - constructor STE - fromSTErr : ST s (Either e a) - -export -Functor (STErr e s) where - map f (STE e) = STE $ map f <$> e - -export -Applicative (STErr e s) where - pure x = STE $ pure $ pure x - STE f <*> STE x = STE [|f <*> x|] - -export -Monad (STErr e s) where - STE m >>= k = STE $ do - case !m of - Left err => pure $ Left err - Right x => fromSTErr $ k x - -export -MonadRec (STErr e s) where - tailRecM s (Access r) x k = STE $ do - let STE m = k s x - case !m of - Left err => pure $ Left err - Right (Cont s' p y) => fromSTErr $ tailRecM s' (r s' p) y k - Right (Done y) => pure $ Right y - -export -runSTErr : (forall s. STErr e s a) -> Either e a -runSTErr ste = runST $ fromSTErr ste - -export %inline HasST (STErr e) where liftST = STE . map Right - -export -stLeft : e -> STErr e s a -stLeft e = STE $ pure $ Left e diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg index 41cc4cd..3a2e124 100644 --- a/lib/quox-lib.ipkg +++ b/lib/quox-lib.ipkg @@ -9,12 +9,12 @@ depends = base, contrib, elab-util, sop, snocvect, eff, prettier modules = Text.PrettyPrint.Bernardy.Core.Decorate, + Control.Monad.ST.Extra, Quox.BoolExtra, Quox.CharExtra, Quox.NatExtra, Quox.EffExtra, Quox.Decidable, - Quox.ST, Quox.No, Quox.Loc, Quox.OPE, diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr index 6da572d..b63d498 100644 --- a/tests/Tests/Reduce.idr +++ b/tests/Tests/Reduce.idr @@ -2,7 +2,7 @@ module Tests.Reduce import Quox.Syntax as Lib import Quox.Equal -import Quox.ST +import Control.Monad.ST.Extra import TypingImpls import AstExtra import TAP @@ -14,7 +14,8 @@ import Control.Eff runWhnf : Eff Whnf a -> Either Error a runWhnf act = runSTErr $ do - runEff act [handleStateSTRef !(newRef 0), handleExcept (\e => stLeft e)] + runEff act [handleStateSTRef !(liftST $ newSTRef 0), + handleExcept (\e => stLeft e)] parameters {0 isRedex : RedexTest tm} {auto _ : CanWhnf tm isRedex} {d, n : Nat} {auto _ : (Eq (tm d n), Show (tm d n))} diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr index e149f50..34c889a 100644 --- a/tests/TypingImpls.idr +++ b/tests/TypingImpls.idr @@ -5,7 +5,7 @@ import public Quox.Typing import public Quox.Pretty import Quox.Equal import Quox.Typechecker -import Quox.ST +import Control.Monad.ST.Extra import PrettyExtra import Derive.Prelude @@ -25,7 +25,7 @@ runEqual defs act = runSTErr $ do runEff act [handleExcept (\e => stLeft e), handleReaderConst defs, - handleStateSTRef !(newRef 0)] + handleStateSTRef !(liftST $ newSTRef 0)] export runTC : Definitions -> Eff TC a -> Either Error a