git.iko.soy/Idris-dev
on master help sign in
Rename 'effect' to 'call'

Sorry for breaking code again! But... "effect" is too overloaded, and this really does just mean calling a single effectful operation. "Effect" and "EFFECT" still refer to effect signatures and concrete effects respectively. This only affects effect definitions, not user code which uses an effectful library.

commit6b69961fab397560dee2c7378c3232c618cb9791 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 28 May 2014, 15:30 (12 years ago) parentf15aaef
9 files changed+35−35
compare with master
unifiedsplit
libs/effects/Effect/Exception.idr+1−1 libs/effects/Effect/File.idr+5−5 libs/effects/Effect/Memory.idr+7−7 libs/effects/Effect/Random.idr+3−3 libs/effects/Effect/Select.idr+1−1 libs/effects/Effect/State.idr+3−3 libs/effects/Effect/StdIO.idr+4−4 libs/effects/Effect/System.idr+3−3 libs/effects/Effects.idr+8−8
libs/effects/Effect/Exception.idr+1−1
@@ -27,7 +27,7 @@ EXCEPTION : Type -> EFFECT
2727EXCEPTION t = MkEff () (Exception t)
2828
2929raise : a -> { [EXCEPTION a ] } Eff m b
30−raise err = effect $ Raise err
30+raise err = call $ Raise err
3131
3232
3333
libs/effects/Effect/File.idr+5−5
@@ -107,27 +107,27 @@ open : Handler FileIO e =>
107107 -> { [FILE_IO ()] ==> [FILE_IO (if result
108108 then OpenFile m
109109 else ())] } Eff e Bool
110−open f m = effect $ Open f m
110+open f m = call $ Open f m
111111
112112
113113||| Close a file.
114114close : Handler FileIO e =>
115115 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
116−close = effect $ Close
116+close = call $ Close
117117
118118||| Read a line from the file.
119119readLine : Handler FileIO e =>
120120 { [FILE_IO (OpenFile Read)] } Eff e String
121−readLine = effect $ ReadLine
121+readLine = call $ ReadLine
122122
123123||| Write a line to a file.
124124writeLine : Handler FileIO e =>
125125 String -> { [FILE_IO (OpenFile Write)] } Eff e ()
126−writeLine str = effect $ WriteLine str
126+writeLine str = call $ WriteLine str
127127
128128||| End of file?
129129eof : Handler FileIO e =>
130130 { [FILE_IO (OpenFile Read)] } Eff e Bool
131−eof = effect $ EOF
131+eof = call $ EOF
132132
133133-- --------------------------------------------------------------------- [ EOF ]
libs/effects/Effect/Memory.idr+7−7
@@ -102,7 +102,7 @@ RAW_MEMORY t = MkEff t RawMemory
102102
103103allocate : (n : Nat) ->
104104 Eff m () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])
105−allocate size = effect $ Allocate size
105+allocate size = call $ Allocate size
106106
107107initialize : {i : Nat} ->
108108 {n : Nat} ->
@@ -111,17 +111,17 @@ initialize : {i : Nat} ->
111111 so (i + size <= n) ->
112112 Eff m () [RAW_MEMORY (MemoryChunk n i)]
113113 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])
114−initialize c size prf = effect $ Initialize c size prf
114+initialize c size prf = call $ Initialize c size prf
115115
116116free : Eff m () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])
117−free = effect Free
117+free = call Free
118118
119119peek : {i : Nat} ->
120120 (offset : Nat) ->
121121 (size : Nat) ->
122122 so (offset + size <= i) ->
123123 { [RAW_MEMORY (MemoryChunk n i)] } Eff m (Vect size Bits8)
124−peek offset size prf = effect $ Peek offset size prf
124+peek offset size prf = call $ Peek offset size prf
125125
126126poke : {n : Nat} ->
127127 {i : Nat} ->
@@ -130,11 +130,11 @@ poke : {n : Nat} ->
130130 so (offset <= i && offset + size <= n) ->
131131 Eff m () [RAW_MEMORY (MemoryChunk n i)]
132132 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])
133−poke offset content prf = effect $ Poke offset content prf
133+poke offset content prf = call $ Poke offset content prf
134134
135135private
136136getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff m (MemoryChunk n i)
137−getRawPtr = effect $ GetRawPtr
137+getRawPtr = call $ GetRawPtr
138138
139139private
140140move' : {dst_size : Nat} ->
@@ -149,7 +149,7 @@ move' : {dst_size : Nat} ->
149149 Eff m () [RAW_MEMORY (MemoryChunk dst_size dst_init)]
150150 (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])
151151move' src_ptr dst_offset src_offset size dst_bounds src_bounds
152− = effect $ Move src_ptr dst_offset src_offset size dst_bounds src_bounds
152+ = call $ Move src_ptr dst_offset src_offset size dst_bounds src_bounds
153153
154154data MoveDescriptor = Dst | Src
155155
libs/effects/Effect/Random.idr+3−3
@@ -18,14 +18,14 @@ RND = MkEff Integer Random
1818
1919||| Generates a random Integer in a given range
2020rndInt : Integer -> Integer -> { [RND] } Eff m Integer
21−rndInt lower upper = do v <- effect $ getRandom
21+rndInt lower upper = do v <- call $ getRandom
2222 return (v `prim__sremBigInt` (upper - lower) + lower)
2323
2424||| Generate a random number in Fin (S `k`)
2525|||
2626||| Note that rndFin k takes values 0, 1, ..., k.
2727rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
28−rndFin k = do let v = assert_total $ !(effect getRandom) `prim__sremBigInt` (cast (S k))
28+rndFin k = do let v = assert_total $ !(call getRandom) `prim__sremBigInt` (cast (S k))
2929 return (toFin v)
3030 where toFin : Integer -> Fin (S k)
3131 toFin x = case integerToFin x (S k) of
@@ -43,5 +43,5 @@ rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))
4343
4444||| Sets the random seed
4545srand : Integer -> { [RND] } Eff m ()
46−srand n = effect $ setSeed n
46+srand n = call $ setSeed n
4747
libs/effects/Effect/Select.idr+1−1
@@ -19,5 +19,5 @@ SELECT : EFFECT
1919SELECT = MkEff () Selection
2020
2121select : List a -> { [SELECT] } Eff m a
22−select xs = effect $ Select xs
22+select xs = call $ Select xs
2323
libs/effects/Effect/State.idr+3−3
@@ -17,13 +17,13 @@ STATE : Type -> EFFECT
1717STATE t = MkEff t State
1818
1919get : { [STATE x] } Eff m x
20−get = effect $ Get
20+get = call $ Get
2121
2222put : x -> { [STATE x] } Eff m ()
23−put val = effect $ Put val
23+put val = call $ Put val
2424
2525putM : y -> { [STATE x] ==> [STATE y] } Eff m ()
26−putM val = effect $ Put val
26+putM val = call $ Put val
2727
2828update : (x -> x) -> { [STATE x] } Eff m ()
2929update f = put (f !get)
libs/effects/Effect/StdIO.idr+4−4
@@ -40,11 +40,11 @@ STDIO = MkEff () StdIO
4040
4141||| Write a string to standard output.
4242putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()
43−putStr s = effect $ PutStr s
43+putStr s = call $ PutStr s
4444
4545||| Write a character to standard output.
4646putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()
47−putChar c = effect $ PutCh c
47+putChar c = call $ PutCh c
4848
4949||| Write a string to standard output, terminating with a newline.
5050putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()
@@ -52,9 +52,9 @@ putStrLn s = putStr (s ++ "\n")
5252
5353||| Read a string from standard input.
5454getStr : Handler StdIO e => { [STDIO] } Eff e String
55−getStr = effect $ GetStr
55+getStr = call $ GetStr
5656
5757||| Read a character from standard input.
5858getChar : Handler StdIO e => { [STDIO] } Eff e Char
59−getChar = effect $ GetCh
59+getChar = call $ GetCh
6060
libs/effects/Effect/System.idr+3−3
@@ -28,11 +28,11 @@ SYSTEM : EFFECT
2828SYSTEM = MkEff () System
2929
3030getArgs : Handler System e => { [SYSTEM] } Eff e (List String)
31−getArgs = effect Args
31+getArgs = call Args
3232
3333time : Handler System e => { [SYSTEM] } Eff e Int
34−time = effect Time
34+time = call Time
3535
3636getEnv : Handler System e => String -> { [SYSTEM] } Eff e (Maybe String)
37−getEnv s = effect $ GetEnv s
37+getEnv s = call $ GetEnv s
3838
libs/effects/Effects.idr+8−8
@@ -144,7 +144,7 @@ data Eff : (m : Type -> Type)
144144 Eff m a xs xs'
145145 ebind : Eff m a xs xs' ->
146146 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
147− effectP : (prf : EffElem e a xs) ->
147+ callP : (prf : EffElem e a xs) ->
148148 (eff : e t a b) ->
149149 Eff m t xs (\v => updateResTy v xs prf eff)
150150
@@ -204,7 +204,7 @@ eff env (value x) k = k x env
204204eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
205205eff env (prog `ebind` c) k
206206 = eff env prog (\p', env' => eff env' (c p') k)
207−eff env (effectP prf effP) k = execEff env prf effP k
207+eff env (callP prf effP) k = execEff env prf effP k
208208eff env (liftP prf effP) k
209209 = let env' = dropEnv env prf in
210210 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
@@ -233,12 +233,12 @@ syntax MkDefaultEnv = with Env
233233 [default, default, default, default, default, default, default],
234234 [default, default, default, default, default, default, default, default] |)
235235
236−effect : {a, b: _} -> {e : Effect} ->
237− (eff : e t a b) ->
238− {default tactics { search 100; }
239− prf : EffElem e a xs} ->
240− Eff m t xs (\v => updateResTy v xs prf eff)
241−effect e {prf} = effectP prf e
236+call : {a, b: _} -> {e : Effect} ->
237+ (eff : e t a b) ->
238+ {default tactics { search 100; }
239+ prf : EffElem e a xs} ->
240+ Eff m t xs (\v => updateResTy v xs prf eff)
241+call e {prf} = callP prf e
242242
243243implicit
244244lift : Eff m t ys ys' ->