git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3876 from Synthetica9/Reader
3bd9687Niklas Larsson
CHANGELOG.md+5−1
compare with master
unifiedsplit
@@ -4,7 +4,11 @@
4
4
5+ Added `Text.Lexer` and `Text.Parser` to `contrib`. These are small libraries
5+ Added `Text.Lexer` and `Text.Parser` to `contrib`. These are small libraries
6 for implementing total lexical analysers and parsers.
6 for implementing total lexical analysers and parsers.
7−
7++ New instances:
8+ + Added `Catchable` for `ReaderT`, `WriterT`, and `RWST`.
9+ + Added `MonadTrans` for `RWST`.
10++ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),
11+ most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
8+ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),
12+ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),
9 most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
13 most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)
10
14
libs/base/Control/Catchable.idr+22
@@ -1,6 +1,10 @@
1module Control.Catchable
1module Control.Catchable
2
2
3import Control.IOExcept
3import Control.IOExcept
4+import Control.Monad.Reader
5+import Control.Monad.Writer
6+import Control.Monad.RWS
7+import Control.Monad.Trans
4
8
5%access public export
9%access public export
6
10
@@ -32,3 +36,21 @@ implementation Catchable List () where
32 catch xs h = xs
36 catch xs h = xs
33
37
34 throw () = []
38 throw () = []
39+
40+||| Adapted from https://hackage.haskell.org/package/mtl-2.2.1/docs/src/Control.Monad.Error.Class.html#line-138
41+implementation (Monad m, Catchable m t) => Catchable (ReaderT r m) t where
42+ -- TODO: rewrite this with apply2way combinator when implemented
43+ catch m h = RD $ \ r => catch (runReaderT m r) (\ e => runReaderT (h e) r)
44+ -- catch m h = RD $ \ r => catch (runReaderT m r) (\ e => runReaderT (h e) r)
45+
46+ throw = lift . throw
47+
48+||| Adapted from https://hackage.haskell.org/package/transformers-0.5.4.0/docs/src/Control.Monad.Trans.Writer.Lazy.html#local-6989586621679059673
49+implementation (Monad m, Monoid w, Catchable m t) => Catchable (WriterT w m) t where
50+ catch m h = WR $ runWriterT m `catch` runWriterT . h
51+ throw = lift . throw
52+
53+||| Adapted from https://hackage.haskell.org/package/mtl-2.2.1/docs/src/Control.Monad.Error.Class.html#line-138
54+implementation (Monad m, Monoid w, Catchable m t) => Catchable (RWST r w s m) t where
55+ catch m h = MkRWST $ \ r, s => runRWST m r s `catch` \ e => runRWST (h e) r s
56+ throw = lift . throw
libs/base/Control/Monad/RWS.idr+7−1
@@ -14,7 +14,7 @@ interface (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadR
14record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
14record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
15 constructor MkRWST
15 constructor MkRWST
16 runRWST : r -> s -> m (a, s, w)
16 runRWST : r -> s -> m (a, s, w)
17−
17+
18implementation Monad m => Functor (RWST r w s m) where
18implementation Monad m => Functor (RWST r w s m) where
19 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s
19 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s
20 pure (f a, s', w)
20 pure (f a, s', w)
@@ -48,6 +48,12 @@ implementation (Monoid w, Monad m) => MonadState s (RWST r w s m) where
48
48
49implementation (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}
49implementation (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}
50
50
51+||| Adapted from https://hackage.haskell.org/package/transformers-0.5.4.0/docs/src/Control-Monad-Trans-RWS-Lazy.html
52+implementation Monoid w => MonadTrans (RWST r w s) where
53+ lift x = MkRWST $ \ _, s => do
54+ a <- x
55+ pure (a, s, neutral)
56+
51||| The RWS monad. See the MonadRWS interface
57||| The RWS monad. See the MonadRWS interface
52RWS : Type -> Type -> Type -> Type -> Type
58RWS : Type -> Type -> Type -> Type -> Type
53RWS r w s a = RWST r w s Identity a
59RWS r w s a = RWST r w s Identity a