use ST from base
This commit is contained in:
parent
ebde478adc
commit
80b1b3581a
8 changed files with 80 additions and 121 deletions
64
lib/Control/Monad/ST/Extra.idr
Normal file
64
lib/Control/Monad/ST/Extra.idr
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
106
lib/Quox/ST.idr
106
lib/Quox/ST.idr
|
|
@ -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
|
||||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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))}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue