~ubuntu-branches/ubuntu/trusty/agda/trusty

« back to all changes in this revision

Viewing changes to src/full/Agda/Utils/Tuple.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, Kiwamu Okabe, Iain Lane
  • Date: 2013-04-10 11:46:43 UTC
  • mfrom: (4.1.5 experimental)
  • Revision ID: package-import@ubuntu.com-20130410114643-prunhsz59f0fhrdn
Tags: 2.3.2-1
[ Kiwamu Okabe ]
* New patch: Extend haskell-src-exts dependency and fix type miss.

[ Iain Lane ]
* [dfbca48] Imported Upstream version 2.3.2
* [7746bcc] Remove all patches — all upstream.
* [2cdb691] Update build-deps to match control file
* [868ebf4] agda-mode no longer depends on haskell-mode or GHCi.
  Remove dependency and update .el file accordingly
* [9e0ba22] Add agda-bin package here, as the separate package has been
  removed
* [75a240f] agda-mode needs to depend on agda-bin
* [d290f95] Allow Quickcheck up to 2.7. Fix haskeline build-dep.
* [79190e6] Add missing geniplate and parallel BDs

Show diffs side-by-side

added added

removed removed

Lines of Context:
 
1
{-# LANGUAGE TupleSections, GeneralizedNewtypeDeriving, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
1
2
 
2
3
module Agda.Utils.Tuple where
3
4
 
 
5
import Control.Applicative
 
6
 
 
7
import Data.Foldable
 
8
import Data.Traversable
 
9
 
4
10
infix 2 -*-
5
11
infix 3 /\ -- backslashes at EOL interacts badly with CPP...
6
12
 
 
13
-- | Bifunctoriality for pairs.
7
14
(-*-) :: (a -> c) -> (b -> d) -> (a,b) -> (c,d)
8
 
(f -*- g) (x,y) = (f x, g y)
9
 
 
 
15
(f -*- g) ~(x,y) = (f x, g y)
 
16
 
 
17
-- | @mapFst f = f -*- id@
 
18
mapFst :: (a -> c) -> (a,b) -> (c,b)
 
19
mapFst f ~(x,y) = (f x, y)
 
20
 
 
21
-- | @mapSnd g = id -*- g@
 
22
mapSnd :: (b -> d) -> (a,b) -> (a,d)
 
23
mapSnd g ~(x,y) = (x, g y)
 
24
 
 
25
-- | Lifted pairing.
10
26
(/\) :: (a -> b) -> (a -> c) -> a -> (b,c)
11
27
(f /\ g) x = (f x, g x)
12
28
 
 
29
-- * Triple (stolen from Data.Tuple.HT)
 
30
 
 
31
{-# INLINE fst3 #-}
 
32
fst3 :: (a,b,c) -> a
 
33
fst3 ~(x,_,_) = x
 
34
 
 
35
{-# INLINE snd3 #-}
 
36
snd3 :: (a,b,c) -> b
 
37
snd3 ~(_,x,_) = x
 
38
 
 
39
{-# INLINE thd3 #-}
 
40
thd3 :: (a,b,c) -> c
 
41
thd3 ~(_,_,x) = x
 
42
 
 
43
{-# INLINE uncurry3 #-}
13
44
uncurry3 :: (a -> b -> c -> d) -> (a,b,c) -> d
14
 
uncurry3 f (x,y,z) = f x y z
 
45
uncurry3 f ~(x,y,z) = f x y z
 
46
 
 
47
uncurry4 :: (a -> b -> c -> d -> e) -> (a,b,c,d) -> e
 
48
uncurry4 f ~(w,x,y,z) = f w x y z
 
49
 
 
50
-- | Monadic version of '-*-'.
 
51
mapPairM :: (Applicative m) => (a -> m c) -> (b -> m d) -> (a,b) -> m (c,d)
 
52
mapPairM f g ~(a,b) = (,) <$> f a <*> g b
 
53
 
 
54
-- | Monadic 'mapFst'.
 
55
mapFstM :: (Applicative m) => (a -> m c) -> (a,b) -> m (c,b)
 
56
mapFstM f ~(a,b) = (,b) <$> f a
 
57
 
 
58
-- | Monadic 'mapSnd'.
 
59
mapSndM :: (Applicative m) => (b -> m d) -> (a,b) -> m (a,d)
 
60
mapSndM f ~(a,b) = (a,) <$> f b
 
61
 
 
62
newtype List2 a = List2 { list2 :: (a,a) }
 
63
  deriving (Eq, Functor, Foldable, Traversable)