git.iko.soy/Idris-dev
on master help sign in
Changing all lambdas to use comma separated style (e.g. '\x => \y =>' to '\x,y =>')
dc5298fjohnny-john
libs/base/Control/Monad/RWS.idr+19−19
compare with master
unifiedsplit
@@ -16,35 +16,35 @@ record RWST : Type -> Type -> Type -> (Type -> Type) -> Type -> Type where
16 (runRWST : r -> s -> m (a, s, w)) -> RWST r w s m a
16 (runRWST : r -> s -> m (a, s, w)) -> RWST r w s m a
17
17
18instance Monad m => Functor (RWST r w s m) where
18instance 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− return (f a, s', w)
20+ return (f a, s', w)
21
21
22instance (Monoid w, Monad m) => Applicative (RWST r w s m) where
22instance (Monoid w, Monad m) => Applicative (RWST r w s m) where
23− pure a = MkRWST $ \_ => \s => return (a, s, neutral)
23+ pure a = MkRWST $ \_,s => return (a, s, neutral)
24− (MkRWST f) <$> (MkRWST v) = MkRWST $ \r => \s => do (a, s', w) <- v r s
24+ (MkRWST f) <$> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s
25− (fn, ss, w') <- f r s
25+ (fn, ss, w') <- f r s
26− return (fn a, ss, w <+> w)
26+ return (fn a, ss, w <+> w)
27
27
28instance (Monoid w, Monad m) => Monad (RWST r w s m) where
28instance (Monoid w, Monad m) => Monad (RWST r w s m) where
29− (MkRWST m) >>= k = MkRWST $ \r => \s => do (a, s', w) <- m r s
29+ (MkRWST m) >>= k = MkRWST $ \r,s => do (a, s', w) <- m r s
30− let MkRWST ka = k a
30+ let MkRWST ka = k a
31− (b, ss, w') <- ka r s'
31+ (b, ss, w') <- ka r s'
32− return (b, ss, w <+> w')
32+ return (b, ss, w <+> w')
33
33
34instance (Monoid w, Monad m) => MonadReader r (RWST r w s m) where
34instance (Monoid w, Monad m) => MonadReader r (RWST r w s m) where
35− ask = MkRWST $ \r => \s => return (r, s, neutral)
35+ ask = MkRWST $ \r,s => return (r, s, neutral)
36− local f (MkRWST m) = MkRWST $ \r => \s => m (f r) s
36+ local f (MkRWST m) = MkRWST $ \r,s => m (f r) s
37
37
38instance (Monoid w, Monad m) => MonadWriter w (RWST r w s m) where
38instance (Monoid w, Monad m) => MonadWriter w (RWST r w s m) where
39− tell w = MkRWST $ \_ => \s => return ((), s, w)
39+ tell w = MkRWST $ \_,s => return ((), s, w)
40− listen (MkRWST m) = MkRWST $ \r => \s => do (a, s', w) <- m r s
40+ listen (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s
41− return ((a, w), s', w)
41+ return ((a, w), s', w)
42− pass (MkRWST m) = MkRWST $ \r => \s => do ((a, f), s', w) <- m r s
42+ pass (MkRWST m) = MkRWST $ \r,s => do ((a, f), s', w) <- m r s
43− return (a, s', f w)
43+ return (a, s', f w)
44
44
45instance (Monoid w, Monad m) => MonadState s (RWST r w s m) where
45instance (Monoid w, Monad m) => MonadState s (RWST r w s m) where
46− get = MkRWST $ \_ => \s => return (s, s, neutral)
46+ get = MkRWST $ \_,s => return (s, s, neutral)
47− put s = MkRWST $ \_ => \_ => return ((), s, neutral)
47+ put s = MkRWST $ \_,_ => return ((), s, neutral)
48
48
49instance (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}
49instance (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}
50
50
libs/prelude/Prelude/Foldable.idr+2−2
@@ -38,13 +38,13 @@ or = foldl (||) False
38||| predicate to all elements of a structure. `any` short-circuits
38||| predicate to all elements of a structure. `any` short-circuits
39||| from left to right.
39||| from left to right.
40any : Foldable t => (a -> Bool) -> t a -> Bool
40any : Foldable t => (a -> Bool) -> t a -> Bool
41−any p = foldl (\x => \y => x || p y) False
41+any p = foldl (\x,y => x || p y) False
42
42
43||| The disjunction of the collective results of applying a
43||| The disjunction of the collective results of applying a
44||| predicate to all elements of a structure. `all` short-circuits
44||| predicate to all elements of a structure. `all` short-circuits
45||| from left to right.
45||| from left to right.
46all : Foldable t => (a -> Bool) -> t a -> Bool
46all : Foldable t => (a -> Bool) -> t a -> Bool
47−all p = foldl (\x => \y => x && p y) True
47+all p = foldl (\x,y => x && p y) True
48
48
49||| Add together all the elements of a structure
49||| Add together all the elements of a structure
50sum : (Foldable t, Num a) => t a -> a
50sum : (Foldable t, Num a) => t a -> a
libs/prelude/Prelude/List.idr+2−2
@@ -275,12 +275,12 @@ zipWith3 f (x::xs) (y::ys) (z::zs) p q =
275
275
276||| Combine two lists elementwise into pairs
276||| Combine two lists elementwise into pairs
277zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
277zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
278−zip = zipWith (\x => \y => (x, y))
278+zip = zipWith (\x,y => (x, y))
279
279
280||| Combine three lists elementwise into tuples
280||| Combine three lists elementwise into tuples
281zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->
281zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->
282 (length y = length z) -> List (a, b, c)
282 (length y = length z) -> List (a, b, c)
283−zip3 = zipWith3 (\x => \y => \z => (x, y, z))
283+zip3 = zipWith3 (\x,y,z => (x, y, z))
284
284
285||| Split a list of pairs into two lists
285||| Split a list of pairs into two lists
286unzip : List (a, b) -> (List a, List b)
286unzip : List (a, b) -> (List a, List b)
libs/prelude/Prelude/Vect.idr+1−1
@@ -207,7 +207,7 @@ zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
207
207
208||| Combine two equal-length vectors pairwise
208||| Combine two equal-length vectors pairwise
209zip : Vect n a -> Vect n b -> Vect n (a, b)
209zip : Vect n a -> Vect n b -> Vect n (a, b)
210−zip = zipWith (\x => \y => (x,y))
210+zip = zipWith (\x,y => (x,y))
211
211
212||| Convert a vector of pairs to a pair of vectors
212||| Convert a vector of pairs to a pair of vectors
213unzip : Vect n (a, b) -> (Vect n a, Vect n b)
213unzip : Vect n (a, b) -> (Vect n a, Vect n b)