git.iko.soy/Idris-dev
on master help sign in
Changed <$ and $> to <* and *>
2d563b0Tenor Biel
libs/effects/Effect/Memory.idr+12−12
compare with master
unifiedsplit
@@ -24,11 +24,11 @@ data RawMemory : Effect where
24 (size : Nat) ->
24 (size : Nat) ->
25 So (offset + size <= i) ->
25 So (offset + size <= i) ->
26 RawMemory (Vect size Bits8)
26 RawMemory (Vect size Bits8)
27− (MemoryChunk n i) (\v => MemoryChunk n i)
27+ (MemoryChunk n i) (\v => MemoryChunk n i)
28 Poke : (offset : Nat) ->
28 Poke : (offset : Nat) ->
29 (Vect size Bits8) ->
29 (Vect size Bits8) ->
30 So (offset <= i && offset + size <= n) ->
30 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)))
32 Move : (src : MemoryChunk src_size src_init) ->
32 Move : (src : MemoryChunk src_size src_init) ->
33 (dst_offset : Nat) ->
33 (dst_offset : Nat) ->
34 (src_offset : Nat) ->
34 (src_offset : Nat) ->
@@ -36,8 +36,8 @@ data RawMemory : Effect where
36 So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
36 So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->
37 So (src_offset + size <= src_init) ->
37 So (src_offset + size <= src_init) ->
38 RawMemory () (MemoryChunk dst_size dst_init)
38 RawMemory () (MemoryChunk dst_size dst_init)
39− (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
39+ (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))
40− GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)
40+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)
41
41
42private
42private
43do_malloc : Nat -> IOExcept String Ptr
43do_malloc : Nat -> IOExcept String Ptr
@@ -84,9 +84,9 @@ instance Handler RawMemory (IOExcept String) where
84 = do ptr <- do_malloc n
84 = do ptr <- do_malloc n
85 k () (CH ptr)
85 k () (CH ptr)
86 handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k
86 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)
88 handle (CH ptr) (Free) k
88 handle (CH ptr) (Free) k
89− = ioe_lift (do_free ptr) $> k () ()
89+ = ioe_lift (do_free ptr) *> k () ()
90 handle (CH ptr) (Peek offset size _) k
90 handle (CH ptr) (Peek offset size _) k
91 = do res <- ioe_lift (do_peek ptr offset size)
91 = do res <- ioe_lift (do_peek ptr offset size)
92 k res (CH ptr)
92 k res (CH ptr)
@@ -102,7 +102,7 @@ instance Handler RawMemory (IOExcept String) where
102RAW_MEMORY : Type -> EFFECT
102RAW_MEMORY : Type -> EFFECT
103RAW_MEMORY t = MkEff t RawMemory
103RAW_MEMORY t = MkEff t RawMemory
104
104
105−allocate : (n : Nat) ->
105+allocate : (n : Nat) ->
106 Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
106 Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
107allocate size = call $ Allocate size
107allocate size = call $ Allocate size
108
108
@@ -111,7 +111,7 @@ initialize : {i : Nat} ->
111 Bits8 ->
111 Bits8 ->
112 (size : Nat) ->
112 (size : Nat) ->
113 So (i + size <= n) ->
113 So (i + size <= n) ->
114− Eff () [RAW_MEMORY (MemoryChunk n i)]
114+ Eff () [RAW_MEMORY (MemoryChunk n i)]
115 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
115 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
116initialize c size prf = call $ Initialize c size prf
116initialize c size prf = call $ Initialize c size prf
117
117
@@ -122,7 +122,7 @@ peek : {i : Nat} ->
122 (offset : Nat) ->
122 (offset : Nat) ->
123 (size : Nat) ->
123 (size : Nat) ->
124 So (offset + size <= i) ->
124 So (offset + size <= i) ->
125− { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
125+ { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)
126peek offset size prf = call $ Peek offset size prf
126peek offset size prf = call $ Peek offset size prf
127
127
128poke : {n : Nat} ->
128poke : {n : Nat} ->
@@ -130,12 +130,12 @@ poke : {n : Nat} ->
130 (offset : Nat) ->
130 (offset : Nat) ->
131 Vect size Bits8 ->
131 Vect size Bits8 ->
132 So (offset <= i && offset + size <= n) ->
132 So (offset <= i && offset + size <= n) ->
133− Eff () [RAW_MEMORY (MemoryChunk n i)]
133+ Eff () [RAW_MEMORY (MemoryChunk n i)]
134 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
134 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
135poke offset content prf = call $ Poke offset content prf
135poke offset content prf = call $ Poke offset content prf
136
136
137private
137private
138−getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)
138+getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)
139getRawPtr = call $ GetRawPtr
139getRawPtr = call $ GetRawPtr
140
140
141private
141private
@@ -173,5 +173,5 @@ move : {dst_size : Nat} ->
173move dst_offset src_offset size dst_bounds src_bounds
173move dst_offset src_offset size dst_bounds src_bounds
174 = do src_ptr <- Src :- getRawPtr
174 = do src_ptr <- Src :- getRawPtr
175 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds
175 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds
176− return ()
176+ return ()
177
177
libs/prelude/Prelude/Applicative.idr+6−6
@@ -30,13 +30,13 @@ class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Typ
30 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
30 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
32
32
33−infixl 2 <$
33+infixl 2 <*
34−(<$) : Applicative f => f a -> f b -> f a
34+(<*) : Applicative f => f a -> f b -> f a
35−a <$ b = map const a <*> b
35+a <* b = map const a <*> b
36
36
37−infixl 2 $>
37+infixl 2 *>
38−($>) : Applicative f => f a -> f b -> f b
38+(*>) : Applicative f => f a -> f b -> f b
39−a $> b = map (const id) a <*> b
39+a *> b = map (const id) a <*> b
40
40
41||| Lift a function to an applicative
41||| Lift a function to an applicative
42liftA : Applicative f => (a -> b) -> f a -> f b
42liftA : Applicative f => (a -> b) -> f a -> f b
libs/prelude/Prelude/Traversable.idr+2−2
@@ -8,10 +8,10 @@ import Prelude.Foldable
8import Prelude.Functor
8import Prelude.Functor
9
9
10traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
10traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
11−traverse_ f = foldr (($>) . f) (pure ())
11+traverse_ f = foldr ((*>) . f) (pure ())
12
12
13sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
13sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
14−sequence_ = foldr ($>) (pure ())
14+sequence_ = foldr (*>) (pure ())
15
15
16for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
16for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
17for_ = flip traverse_
17for_ = flip traverse_