6b69961 · Idris-dev · git.iko.soy

libs/effects/Effect/Exception.idr+1−1

compare with master

unifiedsplit

@@ -27,7 +27,7 @@ EXCEPTION : Type -> EFFECT

27EXCEPTION t = MkEff () (Exception t)

28

29raise : a -> { [EXCEPTION a ] } Eff m b

30−raise err = effect $ Raise err

30+raise err = call $ Raise err

31

32

33

libs/effects/Effect/File.idr+5−5

@@ -107,27 +107,27 @@ open : Handler FileIO e =>

107 -> { [FILE_IO ()] ==> [FILE_IO (if result

108 then OpenFile m

109 else ())] } Eff e Bool

110−open f m = effect $ Open f m

110+open f m = call $ Open f m

111

112

113||| Close a file.

114close : Handler FileIO e =>

115 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()

116−close = effect $ Close

116+close = call $ Close

117

118||| Read a line from the file.

119readLine : Handler FileIO e =>

120 { [FILE_IO (OpenFile Read)] } Eff e String

121−readLine = effect $ ReadLine

121+readLine = call $ ReadLine

122

123||| Write a line to a file.

124writeLine : Handler FileIO e =>

125 String -> { [FILE_IO (OpenFile Write)] } Eff e ()

126−writeLine str = effect $ WriteLine str

126+writeLine str = call $ WriteLine str

127

128||| End of file?

129eof : Handler FileIO e =>

130 { [FILE_IO (OpenFile Read)] } Eff e Bool

131−eof = effect $ EOF

131+eof = call $ EOF

132

133-- --------------------------------------------------------------------- [ EOF ]

libs/effects/Effect/Memory.idr+7−7

@@ -102,7 +102,7 @@ RAW_MEMORY t = MkEff t RawMemory

102

103allocate : (n : Nat) ->

104 Eff m () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])

105−allocate size = effect $ Allocate size

105+allocate size = call $ Allocate size

106

107initialize : {i : Nat} ->

108 {n : Nat} ->

@@ -111,17 +111,17 @@ initialize : {i : Nat} ->

111 so (i + size <= n) ->

112 Eff m () [RAW_MEMORY (MemoryChunk n i)]

113 (\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

115

116free : Eff m () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])

117−free = effect Free

117+free = call Free

118

119peek : {i : Nat} ->

120 (offset : Nat) ->

121 (size : Nat) ->

122 so (offset + size <= i) ->

123 { [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

125

126poke : {n : Nat} ->

127 {i : Nat} ->

@@ -130,11 +130,11 @@ poke : {n : Nat} ->

130 so (offset <= i && offset + size <= n) ->

131 Eff m () [RAW_MEMORY (MemoryChunk n i)]

132 (\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

134

135private

136getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff m (MemoryChunk n i)

137−getRawPtr = effect $ GetRawPtr

137+getRawPtr = call $ GetRawPtr

138

139private

140move' : {dst_size : Nat} ->

@@ -149,7 +149,7 @@ move' : {dst_size : Nat} ->

149 Eff m () [RAW_MEMORY (MemoryChunk dst_size dst_init)]

150 (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])

151move' 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

153

154data MoveDescriptor = Dst | Src

155

libs/effects/Effect/Random.idr+3−3

@@ -18,14 +18,14 @@ RND = MkEff Integer Random

18

19||| Generates a random Integer in a given range

20rndInt : Integer -> Integer -> { [RND] } Eff m Integer

21−rndInt lower upper = do v <- effect $ getRandom

21+rndInt lower upper = do v <- call $ getRandom

22 return (v `prim__sremBigInt` (upper - lower) + lower)

23

24||| Generate a random number in Fin (S `k`)

25|||

26||| Note that rndFin k takes values 0, 1, ..., k.

27rndFin : (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))

29 return (toFin v)

30 where toFin : Integer -> Fin (S k)

31 toFin x = case integerToFin x (S k) of

@@ -43,5 +43,5 @@ rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

43

44||| Sets the random seed

45srand : Integer -> { [RND] } Eff m ()

46−srand n = effect $ setSeed n

46+srand n = call $ setSeed n

47

libs/effects/Effect/Select.idr+1−1

@@ -19,5 +19,5 @@ SELECT : EFFECT

19SELECT = MkEff () Selection

20

21select : List a -> { [SELECT] } Eff m a

22−select xs = effect $ Select xs

22+select xs = call $ Select xs

23

libs/effects/Effect/State.idr+3−3

@@ -17,13 +17,13 @@ STATE : Type -> EFFECT

17STATE t = MkEff t State

18

19get : { [STATE x] } Eff m x

20−get = effect $ Get

20+get = call $ Get

21

22put : x -> { [STATE x] } Eff m ()

23−put val = effect $ Put val

23+put val = call $ Put val

24

25putM : y -> { [STATE x] ==> [STATE y] } Eff m ()

26−putM val = effect $ Put val

26+putM val = call $ Put val

27

28update : (x -> x) -> { [STATE x] } Eff m ()

29update f = put (f !get)

libs/effects/Effect/StdIO.idr+4−4

@@ -40,11 +40,11 @@ STDIO = MkEff () StdIO

40

41||| Write a string to standard output.

42putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()

43−putStr s = effect $ PutStr s

43+putStr s = call $ PutStr s

44

45||| Write a character to standard output.

46putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()

47−putChar c = effect $ PutCh c

47+putChar c = call $ PutCh c

48

49||| Write a string to standard output, terminating with a newline.

50putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()

@@ -52,9 +52,9 @@ putStrLn s = putStr (s ++ "\n")

52

53||| Read a string from standard input.

54getStr : Handler StdIO e => { [STDIO] } Eff e String

55−getStr = effect $ GetStr

55+getStr = call $ GetStr

56

57||| Read a character from standard input.

58getChar : Handler StdIO e => { [STDIO] } Eff e Char

59−getChar = effect $ GetCh

59+getChar = call $ GetCh

60

libs/effects/Effect/System.idr+3−3

@@ -28,11 +28,11 @@ SYSTEM : EFFECT

28SYSTEM = MkEff () System

29

30getArgs : Handler System e => { [SYSTEM] } Eff e (List String)

31−getArgs = effect Args

31+getArgs = call Args

32

33time : Handler System e => { [SYSTEM] } Eff e Int

34−time = effect Time

34+time = call Time

35

36getEnv : Handler System e => String -> { [SYSTEM] } Eff e (Maybe String)

37−getEnv s = effect $ GetEnv s

37+getEnv s = call $ GetEnv s

38

libs/effects/Effects.idr+8−8

@@ -144,7 +144,7 @@ data Eff : (m : Type -> Type)

144 Eff m a xs xs'

145 ebind : Eff m a xs xs' ->

146 ((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) ->

148 (eff : e t a b) ->

149 Eff m t xs (\v => updateResTy v xs prf eff)

150

@@ -204,7 +204,7 @@ eff env (value x) k = k x env

204eff env (with_val x prog) k = eff env prog (\p', env' => k x env')

205eff env (prog `ebind` c) k

206 = 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

208eff env (liftP prf effP) k

209 = let env' = dropEnv env prf in

210 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

@@ -233,12 +233,12 @@ syntax MkDefaultEnv = with Env

233 [default, default, default, default, default, default, default],

234 [default, default, default, default, default, default, default, default] |)

235

236−effect : {a, b: _} -> {e : Effect} ->

236+call : {a, b: _} -> {e : Effect} ->

237− (eff : e t a b) ->

237+ (eff : e t a b) ->

238− {default tactics { search 100; }

238+ {default tactics { search 100; }

239− prf : EffElem e a xs} ->

239+ prf : EffElem e a xs} ->

240− Eff m t xs (\v => updateResTy v xs prf eff)

240+ Eff m t xs (\v => updateResTy v xs prf eff)

241−effect e {prf} = effectP prf e

241+call e {prf} = callP prf e

242

243implicit

244lift : Eff m t ys ys' ->