git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1970 from david-christiansen/operator-renames

The Great Operator Rename

commit5e1ef78b78c40af6fc066f51064806ed49dac83b authorDavid Christiansen <david@davidchristiansen.dk> dateMon 2 Mar 2015, 12:28 (12 years ago) parent41711c76f25fbe
37 files changed+161−147
compare with master
unifiedsplit
CHANGELOG+6 contribs/lib/SQLite3/Sqlite3.idr+1−1 contribs/lib/SimpleParser/SimpleParser.idr+1−1 libs/base/Control/Arrow.idr+1−1 libs/base/Control/IOExcept.idr+2−2 libs/base/Control/Monad/Identity.idr+1−1 libs/base/Control/Monad/RWS.idr+1−1 libs/base/Control/Monad/Reader.idr+1−1 libs/base/Control/Monad/State.idr+1−1 libs/base/Control/Monad/Writer.idr+1−1 libs/base/Data/Erased.idr+1−1 libs/base/Data/Matrix.idr+29−29 libs/base/Data/Morphisms.idr+1−1 libs/base/Data/VectType.idr+1−1 libs/base/Network/Cgi.idr+1−1 libs/base/Providers.idr+3−3 libs/base/System/Concurrency/Process.idr+1−1 libs/effects/Effect/Memory.idr+12−12 libs/effects/Effect/Monad.idr+1−1 libs/effects/Effects.idr+3−3 libs/oldeffects/Effect/Monad.idr+1−1 libs/oldeffects/Effects.idr+3−3 libs/prelude/Language/Reflection/Tactical.idr+1−1 libs/prelude/Prelude.idr+8−8 libs/prelude/Prelude/Algebra.idr+37−37 libs/prelude/Prelude/Applicative.idr+17−17 libs/prelude/Prelude/Functor.idr+8 libs/prelude/Prelude/Monad.idr+1−1 libs/prelude/Prelude/Stream.idr+1−1 libs/prelude/Prelude/Traversable.idr+2−2 samples/interp.idr+2−2 src/Idris/AbsSyntaxTree.hs+1−1 test/reg027/reg027.idr+1−1 test/reg050/expected+6−6 test/reg053/four.idr+1−1 test/sugar001/test007.idr+1−1 test/tutorial003/tutorial003.idr+1−1
CHANGELOG+6
@@ -8,6 +8,12 @@ New in 0.9.17:
88* Quasiquotation supports the generation of Language.Reflection.Raw terms
99 in addition to Language.Reflection.TT. Types are used for disambiguation,
1010 defaulting to TT at the REPL.
11+* Library operators have been renamed for consistency with Haskell. In
12+ particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is
13+ now an alias for Functor.map. Correspondingly, ($>) and (<$) have
14+ been renamed to (<*) and (*>). The cascading effects of this rename
15+ are that Algebra.(<*>) has been renamed to Algebra.(<.>) and
16+ Matrix.(<.>) is now Matrix.(<:>).
1117
1218New in 0.9.16:
1319--------------
contribs/lib/SQLite3/Sqlite3.idr+1−1
@@ -48,7 +48,7 @@ instance Functor DB where
4848
4949instance Applicative DB where
5050 pure = MkDB . return . Right
51− (MkDB f) <$> (MkDB x) = MkDB (do f' <- f
51+ (MkDB f) <*> (MkDB x) = MkDB (do f' <- f
5252 case f' of
5353 Left err => return (Left err)
5454 Right op => x >>= (return . map op))
contribs/lib/SimpleParser/SimpleParser.idr+1−1
@@ -30,7 +30,7 @@ instance Functor Parser where
3030
3131instance Applicative Parser where
3232 pure v = P (\inp => Right (v, inp))
33− a <$> b = P (\inp => do (f, rest) <- parse a inp
33+ a <*> b = P (\inp => do (f, rest) <- parse a inp
3434 (x, rest') <- parse b rest
3535 pure ((f x), rest'))
3636
libs/base/Control/Arrow.idr+1−1
@@ -95,7 +95,7 @@ instance Arrow a => Functor (ArrowMonad a) where
9595
9696instance Arrow a => Applicative (ArrowMonad a) where
9797 pure x = MkArrowMonad $ arrow $ \_ => x
98− (MkArrowMonad f) <$> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)
98+ (MkArrowMonad f) <*> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)
9999
100100instance ArrowApply a => Monad (ArrowMonad a) where
101101 (MkArrowMonad m) >>= f =
libs/base/Control/IOExcept.idr+2−2
@@ -10,8 +10,8 @@ instance Functor (IOExcept e) where
1010
1111instance Applicative (IOExcept e) where
1212 pure x = ioM (pure (pure x))
13− (ioM f) <$> (ioM a) = ioM (do f' <- f; a' <- a
14− return (f' <$> a'))
13+ (ioM f) <*> (ioM a) = ioM (do f' <- f; a' <- a
14+ return (f' <*> a'))
1515
1616instance Monad (IOExcept e) where
1717 (ioM x) >>= k = ioM (do x' <- x;
libs/base/Control/Monad/Identity.idr+1−1
@@ -9,7 +9,7 @@ instance Functor Identity where
99instance Applicative Identity where
1010 pure x = Id x
1111
12− (Id f) <$> (Id g) = Id (f g)
12+ (Id f) <*> (Id g) = Id (f g)
1313
1414instance Monad Identity where
1515 (Id x) >>= k = k x
libs/base/Control/Monad/RWS.idr+1−1
@@ -21,7 +21,7 @@ instance Monad m => Functor (RWST r w s m) where
2121
2222instance (Monoid w, Monad m) => Applicative (RWST r w s m) where
2323 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
2525 (fn, ss, w') <- f r s
2626 return (fn a, ss, w <+> w)
2727
libs/base/Control/Monad/Reader.idr+1−1
@@ -27,7 +27,7 @@ instance Functor f => Functor (ReaderT r f) where
2727
2828instance Applicative m => Applicative (ReaderT r m) where
2929 pure = liftReaderT . pure
30− (RD f) <$> (RD v) = RD $ \r => f r <$> v r
30+ (RD f) <*> (RD v) = RD $ \r => f r <*> v r
3131
3232instance Alternative m => Alternative (ReaderT r m) where
3333 empty = liftReaderT empty
libs/base/Control/Monad/State.idr+1−1
@@ -25,7 +25,7 @@ instance Functor f => Functor (StateT s f) where
2525instance Monad f => Applicative (StateT s f) where
2626 pure x = ST (\st => pure (x, st))
2727
28− (ST f) <$> (ST a) = ST (\st => do (g, r) <- f st
28+ (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st
2929 (b, t) <- a r
3030 return (g b, t))
3131
libs/base/Control/Monad/Writer.idr+1−1
@@ -25,7 +25,7 @@ instance Functor f => Functor (WriterT w f) where
2525
2626instance (Monoid w, Applicative m) => Applicative (WriterT w m) where
2727 pure a = WR $ pure (a, neutral)
28− (WR f) <$> (WR v) = WR $ liftA2 merge f v where
28+ (WR f) <*> (WR v) = WR $ liftA2 merge f v where
2929 merge (fn, w) (a, w') = (fn a, w <+> w')
3030
3131instance (Monoid w, Alternative m) => Alternative (WriterT w m) where
libs/base/Data/Erased.idr+1−1
@@ -16,7 +16,7 @@ instance Functor Erased where
1616
1717instance Applicative Erased where
1818 pure = Erase
19− (<$>) (Erase f) (Erase x) = Erase (f x)
19+ (<*>) (Erase f) (Erase x) = Erase (f x)
2020
2121instance Monad Erased where
2222 (>>=) (Erase x) f = f x
libs/base/Data/Matrix.idr+29−29
@@ -7,13 +7,13 @@ import Data.Vect
77
88%default total
99
10−infixr 2 <.> -- vector inner product
10+infixr 2 <:> -- vector inner product
1111infixr 2 >< -- vector outer product
1212infixr 2 <<>> -- matrix commutator
1313infixr 2 >><< -- matrix anticommutator
1414infixl 3 <\> -- row times a matrix
1515infixr 4 </> -- matrix times a column
16−infixr 5 <> -- matrix multiplication
16+infixr 5 <> -- matrix multiplication
1717infixr 7 \&\ -- vector tensor product
1818infixr 7 <&> -- matrix tensor product
1919
@@ -26,14 +26,14 @@ instance Semigroup a => Semigroup (Vect n a) where
2626
2727instance Monoid a => Monoid (Vect n a) where
2828 neutral {n} = replicate n neutral
29−
29+
3030instance Group a => Group (Vect n a) where
3131 inverse = map inverse
3232
3333instance AbelianGroup a => AbelianGroup (Vect n a) where {}
3434
3535instance Ring a => Ring (Vect n a) where
36− (<*>) v w = zipWith (<*>) v w
36+ (<.>) v w = zipWith (<.>) v w
3737
3838instance RingWithUnity a => RingWithUnity (Vect n a) where
3939 unity {n} = replicate n unity
@@ -42,7 +42,7 @@ instance Field a => Field (Vect n a) where
4242 inverseM = map inverseM
4343
4444instance RingWithUnity a => Module a (Vect n a) where
45− (<#>) r v = map (r <*>) v
45+ (<#>) r v = map (r <.>) v
4646
4747instance RingWithUnity a => Module a (Vect n (Vect l a)) where
4848 (<#>) r m = map (r <#>) m
@@ -53,12 +53,12 @@ instance RingWithUnity a => Module a (Vect n (Vect l a)) where
5353-----------------------------------------------------------------------
5454
5555||| Inner product of ring vectors
56−(<.>) : Ring a => Vect n a -> Vect n a -> a
57−(<.>) w v = foldr (<+>) neutral (zipWith (<*>) w v)
56+(<:>) : Ring a => Vect n a -> Vect n a -> a
57+(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)
5858
5959||| Tensor multiply (⊗) ring vectors
6060(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
61−(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where
61+(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where
6262 orep : (n : Nat) -> Vect m a -> Vect (n * m) a
6363 orep n v = concat $ replicate n v
6464 oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
@@ -90,15 +90,15 @@ indices f1 f2 m = index f2 (index f1 m)
9090
9191||| Matrix times a column vector
9292(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
93−(</>) m v = map (v <.>) m
93+(</>) m v = map (v <:>) m
9494
9595||| Matrix times a row vector
9696(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
97−(<\>) r m = map (r <.>) $ transpose m
97+(<\>) r m = map (r <:>) $ transpose m
9898
9999||| Matrix multiplication
100−(<>) : Ring a => Matrix n k a ->
101− Matrix k m a ->
100+(<>) : Ring a => Matrix n k a ->
101+ Matrix k m a ->
102102 Matrix n m a
103103(<>) m1 m2 = map (<\> m2) m1
104104
@@ -110,11 +110,11 @@ indices f1 f2 m = index f2 (index f1 m)
110110 stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
111111 stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2
112112
113−||| Cast a vector from a standard Vect to a proper n x 1 matrix
113+||| Cast a vector from a standard Vect to a proper n x 1 matrix
114114col : Vect n a -> Matrix n 1 a
115115col v = map (\x => [x]) v
116116
117−||| Cast a row from a standard Vect to a proper 1 x n matrix
117+||| Cast a row from a standard Vect to a proper 1 x n matrix
118118row : Vect n a -> Matrix 1 n a
119119row r = [r]
120120
@@ -157,11 +157,11 @@ instance Monoid Integer where
157157
158158instance Group Integer where
159159 inverse = (* -1)
160−
160+
161161instance AbelianGroup Integer
162162
163−instance Ring Integer where
164− (<*>) = (*)
163+instance Ring Integer where
164+ (<.>) = (*)
165165
166166instance RingWithUnity Integer where
167167 unity = 1
@@ -175,11 +175,11 @@ instance Monoid Int where
175175
176176instance Group Int where
177177 inverse = (* -1)
178−
178+
179179instance AbelianGroup Int
180180
181−instance Ring Int where
182− (<*>) = (*)
181+instance Ring Int where
182+ (<.>) = (*)
183183
184184instance RingWithUnity Int where
185185 unity = 1
@@ -193,11 +193,11 @@ instance Monoid Float where
193193
194194instance Group Float where
195195 inverse = (* -1)
196−
196+
197197instance AbelianGroup Float
198198
199−instance Ring Float where
200− (<*>) = (*)
199+instance Ring Float where
200+ (<.>) = (*)
201201
202202instance RingWithUnity Float where
203203 unity = 1
@@ -211,7 +211,7 @@ instance Semigroup Nat where
211211
212212instance Monoid Nat where
213213 neutral = 0
214−
214+
215215instance VerifiedSemigroup Nat where
216216 semigroupOpIsAssociative = plusAssociative
217217
@@ -228,12 +228,12 @@ instance Monoid ZZ where
228228
229229instance Group ZZ where
230230 inverse = (* -1)
231−
231+
232232instance AbelianGroup ZZ
233233
234−instance Ring ZZ where
235− (<*>) = (*)
236−
234+instance Ring ZZ where
235+ (<.>) = (*)
236+
237237instance RingWithUnity ZZ where
238238 unity = 1
239239
@@ -250,7 +250,7 @@ instance Group a => Group (Complex a) where
250250instance Ring a => AbelianGroup (Complex a) where {}
251251
252252instance Ring a => Ring (Complex a) where
253− (<*>) (a :+ b) (c :+ d) = (a <*> c <-> b <*> d) :+ (a <*> d <+> b <*> c)
253+ (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
254254
255255instance RingWithUnity a => RingWithUnity (Complex a) where
256256 unity = (unity :+ neutral)
libs/base/Data/Morphisms.idr+1−1
@@ -25,7 +25,7 @@ instance Functor (Morphism r) where
2525
2626instance Applicative (Morphism r) where
2727 pure a = Mor $ const a
28− (Mor f) <$> (Mor a) = Mor $ \r => f r $ a r
28+ (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r
2929
3030instance Monad (Morphism r) where
3131 (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r
libs/base/Data/VectType.idr+1−1
@@ -529,7 +529,7 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)
529529instance Applicative (Vect k) where
530530 pure = replicate _
531531
532− fs <$> vs = zipWith apply fs vs
532+ fs <*> vs = zipWith apply fs vs
533533
534534instance Monad (Vect n) where
535535 m >>= f = diag (map f m)
libs/base/Network/Cgi.idr+1−1
@@ -36,7 +36,7 @@ instance Functor CGI where
3636instance Applicative CGI where
3737 pure v = MkCGI (\s => return (v, s))
3838
39− (MkCGI a) <$> (MkCGI b) = MkCGI (\s => do (f, i) <- a s
39+ (MkCGI a) <*> (MkCGI b) = MkCGI (\s => do (f, i) <- a s
4040 (c, j) <- b i
4141 return (f c, j))
4242
libs/base/Providers.idr+3−3
@@ -17,9 +17,9 @@ instance Functor Provider where
1717 map f (Error err) = Error err
1818
1919instance Applicative Provider where
20− (Provide f) <$> (Provide x) = Provide (f x)
21− (Provide f) <$> (Error err) = Error err
22− (Error err) <$> _ = Error err
20+ (Provide f) <*> (Provide x) = Provide (f x)
21+ (Provide f) <*> (Error err) = Error err
22+ (Error err) <*> _ = Error err
2323 pure = Provide
2424
2525instance Monad Provider where
libs/base/System/Concurrency/Process.idr+1−1
@@ -19,7 +19,7 @@ instance Functor (Process msg) where
1919
2020instance Applicative (Process msg) where
2121 pure = Lift . return
22− (Lift f) <$> (Lift a) = Lift (f <$> a)
22+ (Lift f) <*> (Lift a) = Lift (f <*> a)
2323
2424instance Monad (Process msg) where
2525 (Lift io) >>= k = Lift (do x <- io
libs/effects/Effect/Memory.idr+12−12
@@ -24,11 +24,11 @@ data RawMemory : Effect where
2424 (size : Nat) ->
2525 So (offset + size <= i) ->
2626 RawMemory (Vect size Bits8)
27− (MemoryChunk n i) (\v => MemoryChunk n i)
27+ (MemoryChunk n i) (\v => MemoryChunk n i)
2828 Poke : (offset : Nat) ->
2929 (Vect size Bits8) ->
3030 So (offset <= i && offset + size <= n) ->
31− RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))
31+ RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))
3232 Move : (src : MemoryChunk src_size src_init) ->
3333 (dst_offset : Nat) ->
3434 (src_offset : Nat) ->
@@ -36,8 +36,8 @@ data RawMemory : Effect where
3636 So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
3737 So (src_offset + size <= src_init) ->
3838 RawMemory () (MemoryChunk dst_size dst_init)
39− (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
40− GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)
39+ (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
40+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)
4141
4242private
4343do_malloc : Nat -> IOExcept String Ptr
@@ -84,9 +84,9 @@ instance Handler RawMemory (IOExcept String) where
8484 = do ptr <- do_malloc n
8585 k () (CH ptr)
8686 handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k
87− = ioe_lift (do_memset ptr i c size) $> k () (CH ptr)
87+ = ioe_lift (do_memset ptr i c size) *> k () (CH ptr)
8888 handle (CH ptr) (Free) k
89− = ioe_lift (do_free ptr) $> k () ()
89+ = ioe_lift (do_free ptr) *> k () ()
9090 handle (CH ptr) (Peek offset size _) k
9191 = do res <- ioe_lift (do_peek ptr offset size)
9292 k res (CH ptr)
@@ -102,7 +102,7 @@ instance Handler RawMemory (IOExcept String) where
102102RAW_MEMORY : Type -> EFFECT
103103RAW_MEMORY t = MkEff t RawMemory
104104
105−allocate : (n : Nat) ->
105+allocate : (n : Nat) ->
106106 Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
107107allocate size = call $ Allocate size
108108
@@ -111,7 +111,7 @@ initialize : {i : Nat} ->
111111 Bits8 ->
112112 (size : Nat) ->
113113 So (i + size <= n) ->
114− Eff () [RAW_MEMORY (MemoryChunk n i)]
114+ Eff () [RAW_MEMORY (MemoryChunk n i)]
115115 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
116116initialize c size prf = call $ Initialize c size prf
117117
@@ -122,7 +122,7 @@ peek : {i : Nat} ->
122122 (offset : Nat) ->
123123 (size : Nat) ->
124124 So (offset + size <= i) ->
125− { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
125+ { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
126126peek offset size prf = call $ Peek offset size prf
127127
128128poke : {n : Nat} ->
@@ -130,12 +130,12 @@ poke : {n : Nat} ->
130130 (offset : Nat) ->
131131 Vect size Bits8 ->
132132 So (offset <= i && offset + size <= n) ->
133− Eff () [RAW_MEMORY (MemoryChunk n i)]
133+ Eff () [RAW_MEMORY (MemoryChunk n i)]
134134 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
135135poke offset content prf = call $ Poke offset content prf
136136
137137private
138−getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)
138+getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)
139139getRawPtr = call $ GetRawPtr
140140
141141private
@@ -173,5 +173,5 @@ move : {dst_size : Nat} ->
173173move dst_offset src_offset size dst_bounds src_bounds
174174 = do src_ptr <- Src :- getRawPtr
175175 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds
176− return ()
176+ return ()
177177
libs/effects/Effect/Monad.idr+1−1
@@ -11,7 +11,7 @@ using (xs : List EFFECT, m : Type -> Type)
1111
1212 instance Applicative (\a => EffM m a xs (\v => xs)) where
1313 pure = value
14− (<$>) f a = do f' <- f
14+ (<*>) f a = do f' <- f
1515 a' <- a
1616 value (f' a')
1717
libs/effects/Effects.idr+3−3
@@ -174,7 +174,7 @@ return x = value x
174174
175175-- ------------------------------------------------------ [ for idiom brackets ]
176176
177−infixl 2 <$>
177+infixl 2 <*>
178178
179179pure : a -> Eff a xs (\v => xs)
180180pure = value
@@ -182,9 +182,9 @@ pure = value
182182pureM : (val : a) -> Eff a (xs val) xs
183183pureM = value
184184
185−(<$>) : Eff (a -> b) xs (\v => xs) ->
185+(<*>) : Eff (a -> b) xs (\v => xs) ->
186186 Eff a xs (\v => xs) -> Eff b xs (\v => xs)
187−(<$>) prog v = do fn <- prog
187+(<*>) prog v = do fn <- prog
188188 arg <- v
189189 return (fn arg)
190190
libs/oldeffects/Effect/Monad.idr+1−1
@@ -11,7 +11,7 @@ using (xs : List EFFECT, m : Type -> Type)
1111
1212 instance Applicative (\a => EffM m a xs (\v => xs)) where
1313 pure = value
14− (<$>) f a = do f' <- f
14+ (<*>) f a = do f' <- f
1515 a' <- a
1616 value (f' a')
1717
libs/oldeffects/Effects.idr+3−3
@@ -185,16 +185,16 @@ return x = value x
185185
186186-- ------------------------------------------------------ [ for idiom brackets ]
187187
188−infixl 2 <$>
188+infixl 2 <*>
189189
190190pure : a -> Eff m a xs (\v => xs)
191191pure = value
192192
193193syntax pureM [val] = with_val val (pure ())
194194
195−(<$>) : Eff m (a -> b) xs (\v => xs) ->
195+(<*>) : Eff m (a -> b) xs (\v => xs) ->
196196 Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
197−(<$>) prog v = do fn <- prog
197+(<*>) prog v = do fn <- prog
198198 arg <- v
199199 return (fn arg)
200200
libs/prelude/Language/Reflection/Tactical.idr+1−1
@@ -44,7 +44,7 @@ instance Functor Tactical where
4444
4545instance Applicative Tactical where
4646 pure x = prim__PureTactical x
47− f <$> x = prim__BindTactical f $ \g =>
47+ f <*> x = prim__BindTactical f $ \g =>
4848 prim__BindTactical x $ \y =>
4949 prim__PureTactical $ g y
5050
libs/prelude/Prelude.idr+8−8
@@ -249,31 +249,31 @@ instance Functor (Either e) where
249249instance Applicative PrimIO where
250250 pure = prim_io_return
251251
252− am <$> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
252+ am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
253253
254254instance Applicative (IO' ffi) where
255255 pure x = io_return x
256− f <$> a = io_bind f (\f' =>
256+ f <*> a = io_bind f (\f' =>
257257 io_bind a (\a' =>
258258 io_return (f' a')))
259259
260260instance Applicative Maybe where
261261 pure = Just
262262
263− (Just f) <$> (Just a) = Just (f a)
264− _ <$> _ = Nothing
263+ (Just f) <*> (Just a) = Just (f a)
264+ _ <*> _ = Nothing
265265
266266instance Applicative (Either e) where
267267 pure = Right
268268
269− (Left a) <$> _ = Left a
270− (Right f) <$> (Right r) = Right (f r)
271− (Right _) <$> (Left l) = Left l
269+ (Left a) <*> _ = Left a
270+ (Right f) <*> (Right r) = Right (f r)
271+ (Right _) <*> (Left l) = Left l
272272
273273instance Applicative List where
274274 pure x = [x]
275275
276− fs <$> vs = concatMap (\f => map f vs) fs
276+ fs <*> vs = concatMap (\f => map f vs) fs
277277
278278---- Alternative instances
279279
libs/prelude/Prelude/Algebra.idr+37−37
@@ -5,7 +5,7 @@ import Builtins
55-- XXX: change?
66infixl 6 <->
77infixl 6 <+>
8−infixl 6 <*>
8+infixl 6 <.>
99infixl 5 <#>
1010
1111%access public
@@ -96,18 +96,18 @@ class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
9696||| + Inverse for `<+>`:
9797||| forall a, a <+> inverse a == neutral
9898||| forall a, inverse a <+> a == neutral
99−||| + Associativity of `<*>`:
100−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
101−||| + Distributivity of `<*>` and `<->`:
102−||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
103−||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
99+||| + Associativity of `<.>`:
100+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
101+||| + Distributivity of `<.>` and `<->`:
102+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
103+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
104104class AbelianGroup a => Ring a where
105− (<*>) : a -> a -> a
105+ (<.>) : a -> a -> a
106106
107107class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
108− total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
109− total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
110− total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (c <*> r)
108+ total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
109+ total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
110+ total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
111111
112112||| Sets equipped with two binary operations, one associative and commutative
113113||| supplied with a neutral element, and the other associative supplied with a
@@ -124,20 +124,20 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
124124||| + Inverse for `<+>`:
125125||| forall a, a <+> inverse a == neutral
126126||| forall a, inverse a <+> a == neutral
127−||| + Associativity of `<*>`:
128−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
129−||| + Neutral for `<*>`:
130−||| forall a, a <*> unity == a
131−||| forall a, unity <*> a == a
132−||| + Distributivity of `<*>` and `<->`:
133−||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
134−||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
127+||| + Associativity of `<.>`:
128+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
129+||| + Neutral for `<.>`:
130+||| forall a, a <.> unity == a
131+||| forall a, unity <.> a == a
132+||| + Distributivity of `<.>` and `<->`:
133+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
134+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
135135class Ring a => RingWithUnity a where
136136 unity : a
137137
138138class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
139− total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l
140− total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r
139+ total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
140+ total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
141141
142142||| Sets equipped with a binary operation that is commutative, associative and
143143||| idempotent. Must satisfy the following laws:
@@ -281,31 +281,31 @@ class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, Verif
281281||| + Inverse for `<+>`:
282282||| forall a, a <+> inverse a == neutral
283283||| forall a, inverse a <+> a == neutral
284−||| + Associativity of `<*>`:
285−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
286−||| + Unity for `<*>`:
287−||| forall a, a <*> unity == a
288−||| forall a, unity <*> a == a
289−||| + InverseM of `<*>`:
290−||| forall a, a <*> inverseM a == unity
291−||| forall a, inverseM a <*> a == unity
292−||| + Distributivity of `<*>` and `<->`:
293−||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
294−||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
284+||| + Associativity of `<.>`:
285+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
286+||| + Unity for `<.>`:
287+||| forall a, a <.> unity == a
288+||| forall a, unity <.> a == a
289+||| + InverseM of `<.>`:
290+||| forall a, a <.> inverseM a == unity
291+||| forall a, inverseM a <.> a == unity
292+||| + Distributivity of `<.>` and `<->`:
293+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
294+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
295295class RingWithUnity a => Field a where
296296 inverseM : a -> a
297297
298298class (VerifiedRing a, Field a) => VerifiedField a where
299− total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
300− total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
299+ total fieldInverseIsInverseL : (l : a) -> l <.> inverseM l = unity
300+ total fieldInverseIsInverseR : (r : a) -> inverseM r <.> r = unity
301301
302302||| A module over a ring is an additive abelian group of 'vectors' endowed with a
303−||| scale operation multiplying vectors by ring elements, and distributivity laws
304−||| relating the scale operation to both ring addition and module addition.
303+||| scale operation multiplying vectors by ring elements, and distributivity laws
304+||| relating the scale operation to both ring addition and module addition.
305305||| Must satisfy the following laws:
306306|||
307307||| + Compatibility of scalar multiplication with ring multiplication:
308−||| forall a b v, a <#> (b <#> v) = (a <*> b) <#> v
308+||| forall a b v, a <#> (b <#> v) = (a <.> b) <#> v
309309||| + Ring unity is the identity element of scalar multiplication:
310310||| forall v, unity <#> v = v
311311||| + Distributivity of `<#>` and `<+>`:
@@ -315,7 +315,7 @@ class (RingWithUnity a, AbelianGroup b) => Module a b where
315315 (<#>) : a -> b -> b
316316
317317class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
318− total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <*> y) <#> v
318+ total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v
319319 total moduleScalarUnityIsUnity : (v : b) -> unity <#> v = v
320320 total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
321321 total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
libs/prelude/Prelude/Applicative.idr+17−17
@@ -9,46 +9,46 @@ import Prelude.Functor
99
1010---- Applicative functors/Idioms
1111
12−infixl 2 <$>
12+infixl 2 <*>
1313
1414class Functor f => Applicative (f : Type -> Type) where
1515 pure : a -> f a
16− (<$>) : f (a -> b) -> f a -> f b
16+ (<*>) : f (a -> b) -> f a -> f b
1717
1818instance Applicative id where
1919 pure a = a
20− f <$> a = f a
20+ f <*> a = f a
2121
2222class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
2323 applicativeMap : (x : f a) -> (g : a -> b) ->
24− map g x = pure g <$> x
25− applicativeIdentity : (x : f a) -> pure id <$> x = x
24+ map g x = pure g <*> x
25+ applicativeIdentity : (x : f a) -> pure id <*> x = x
2626 applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->
27− ((pure (.) <$> g2) <$> g1) <$> x = g2 <$> (g1 <$> x)
27+ ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)
2828 applicativeHomomorphism : (x : a) -> (g : a -> b) ->
29− (<$>) {f} (pure g) (pure x) = pure {f} (g x)
29+ (<*>) {f} (pure g) (pure x) = pure {f} (g x)
3030 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
31− g <$> pure x = pure (\g' : a -> b => g' x) <$> g
31+ g <*> pure x = pure (\g' : a -> b => g' x) <*> g
3232
33−infixl 2 <$
34−(<$) : Applicative f => f a -> f b -> f a
35−a <$ b = map const a <$> b
33+infixl 2 <*
34+(<*) : Applicative f => f a -> f b -> f a
35+a <* b = map const a <*> b
3636
37−infixl 2 $>
38−($>) : Applicative f => f a -> f b -> f b
39−a $> b = map (const id) a <$> b
37+infixl 2 *>
38+(*>) : Applicative f => f a -> f b -> f b
39+a *> b = map (const id) a <*> b
4040
4141||| Lift a function to an applicative
4242liftA : Applicative f => (a -> b) -> f a -> f b
43−liftA f a = pure f <$> a
43+liftA f a = pure f <*> a
4444
4545||| Lift a two-argument function to an applicative
4646liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c
47−liftA2 f a b = (map f a) <$> b
47+liftA2 f a b = (map f a) <*> b
4848
4949||| Lift a three-argument function to an applicative
5050liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
51−liftA3 f a b c = (map f a) <$> b <$> c
51+liftA3 f a b c = (map f a) <*> b <*> c
5252
5353infixl 3 <|>
5454class Applicative f => Alternative (f : Type -> Type) where
libs/prelude/Prelude/Functor.idr+8
@@ -10,6 +10,14 @@ class Functor (f : Type -> Type) where
1010 ||| @ m the morphism
1111 map : (m : a -> b) -> f a -> f b
1212
13+infixl 4 <$>
14+
15+||| An infix alias for `map`: the action of a functor on morphisms.
16+||| @ f the functor
17+||| @ m the morphism
18+(<$>) : Functor f => (m : a -> b) -> f a -> f b
19+m <$> x = map m x
20+
1321class Functor f => VerifiedFunctor (f : Type -> Type) where
1422 functorIdentity : {a : Type} -> (x : f a) -> map id x = id x
1523 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
libs/prelude/Prelude/Monad.idr+1−1
@@ -16,7 +16,7 @@ class Applicative m => Monad (m : Type -> Type) where
1616
1717class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
1818 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
19− mf <$> mx = mf >>= \f =>
19+ mf <*> mx = mf >>= \f =>
2020 mx >>= \x =>
2121 pure (f x)
2222 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x
libs/prelude/Prelude/Stream.idr+1−1
@@ -111,7 +111,7 @@ scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs
111111
112112instance Applicative Stream where
113113 pure = repeat
114− (<$>) = zipWith apply
114+ (<*>) = zipWith apply
115115
116116instance Monad Stream where
117117 s >>= f = diag (map f s)
libs/prelude/Prelude/Traversable.idr+2−2
@@ -8,10 +8,10 @@ import Prelude.Foldable
88import Prelude.Functor
99
1010traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
11−traverse_ f = foldr (($>) . f) (pure ())
11+traverse_ f = foldr ((*>) . f) (pure ())
1212
1313sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
14−sequence_ = foldr ($>) (pure ())
14+sequence_ = foldr (*>) (pure ())
1515
1616for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
1717for_ = flip traverse_
samples/interp.idr+2−2
@@ -37,8 +37,8 @@ using (G : Vect n Ty)
3737 index_first = stop
3838 index_next = pop
3939
40− (<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
41− (<$>) = \f, a => App f a
40+ (<*>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
41+ (<*>) = \f, a => App f a
4242
4343 pure : Expr G a -> Expr G a
4444 pure = id
src/Idris/AbsSyntaxTree.hs+1−1
@@ -1157,7 +1157,7 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
11571157
11581158initDSL = DSL (PRef f (sUN ">>="))
11591159 (PRef f (sUN "return"))
1160− (PRef f (sUN "<$>"))
1160+ (PRef f (sUN "<*>"))
11611161 (PRef f (sUN "pure"))
11621162 Nothing
11631163 Nothing
test/reg027/reg027.idr+1−1
@@ -14,7 +14,7 @@ instance Functor IntFn where -- (\x => Int -> x) where
1414
1515instance Applicative (\x => Int -> x) where
1616 pure v = \x => v
17− (<$>) f a = \x => f x (a x)
17+ (<*>) f a = \x => f x (a x)
1818
1919instance Monad IntFn where
2020 f >>= k = \x => k (f x) x
test/reg050/expected+6−6
@@ -12,13 +12,13 @@ When elaborating an application of function Prelude.Monad.>>=:
1212 \{uv0} => argTy -> uv
1313./baddoublebang.idr:6:26: error: not
1414 a terminator, expected: "$",
15− "$>", "&&", "*", "+", "++", "-",
15+ "&&", "*", "*>", "+", "++", "-",
1616 "->", ".", "/", "/=", "::", ";",
17− "<", "<#>", "<$", "<$>", "<*>",
18− "<+>", "<->", "<<", "<=", "<|>",
19− "=", "==", ">", ">=", ">>",
20− ">>=", "\\\\", "`", "in", "||",
21− "~=~",
17+ "<", "<#>", "<$>", "<*", "<*>",
18+ "<+>", "<->", "<.>", "<<", "<=",
19+ "<|>", "=", "==", ">", ">=",
20+ ">>", ">>=", "\\\\", "`", "in",
21+ "||", "~=~",
2222 ambiguous use of a left-associative operator,
2323 ambiguous use of a non-associative operator,
2424 ambiguous use of a right-associative operator,
test/reg053/four.idr+1−1
@@ -5,5 +5,5 @@ data FourFunctor y = Four y y y y
55traverseFourFunctor : Applicative f ->
66 (x -> f b) -> FourFunctor x -> f (FourFunctor b)
77traverseFourFunctor constr f (Four w x y z)
8− = pure Four <$> (f w) <$> (f x) <$> (f y) <$> (f z)
8+ = pure Four <*> (f w) <*> (f x) <*> (f y) <*> (f z)
99
test/sugar001/test007.idr+1−1
@@ -19,7 +19,7 @@ instance Functor Eval where
1919instance Applicative Eval where
2020 pure x = MkEval (\e => Just x)
2121
22− (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where
22+ (<*>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where
2323 appAux : Maybe (a -> b) -> Maybe a -> Maybe b
2424 appAux (Just fx) (Just gx) = Just (fx gx)
2525 appAux _ _ = Nothing
test/tutorial003/tutorial003.idr+1−1
@@ -19,7 +19,7 @@ instance Functor Eval where
1919instance Applicative Eval where
2020 pure x = MkEval (\e => Just x)
2121
22− (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
22+ (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
2323 app : Maybe (a -> b) -> Maybe a -> Maybe b
2424 app (Just fx) (Just gx) = Just (fx gx)
2525 app _ _ = Nothing