git.iko.soy/Idris-dev
on master help sign in
Changed <$ and $> to <* and *>
commit2d563b02789c4d9100d8e37c48229fa5c1b911b1 authorTenor Biel <tenorbiel@gmail.com> dateWed 18 Feb 2015, 15:16 (12 years ago) parentb5f2e4d
3 files changed+20−20
compare with master
unifiedsplit
libs/effects/Effect/Memory.idr+12−12 libs/prelude/Prelude/Applicative.idr+6−6 libs/prelude/Prelude/Traversable.idr+2−2
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/prelude/Prelude/Applicative.idr+6−6
@@ -30,13 +30,13 @@ class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Typ
3030 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
3131 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
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_