83b839f · Idris-dev · git.iko.soy

20

21 EXCEPTION : Type -> EFFECT

22

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

23+ raise : a -> Eff b [EXCEPTION a]

24

25 instance Handler (Exception a) Maybe

26 instance Handler (Exception a) List

42

43 data OpenFile : Mode -> Type

44

45− open : Handler FileIO e => String -> (m : Mode) ->

45+ open : (fname : String)

46− { [FILE_IO ()] ==>

46+ -> (m : Mode)

47− {ok} [FILE_IO (if ok then OpenFile m else ())] } Eff e Bool

47+ -> Eff Bool [FILE_IO ()]

48− close : Handler FileIO e =>

48+ (\res => [FILE_IO (case res of

49+ True => OpenFile m

50+ False => ())])

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

51+ close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]

50

52

51− readLine : Handler FileIO e =>

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

53+ readLine : Eff String [FILE_IO (OpenFile Read)]

53− writeLine : Handler FileIO e => String ->

54− { [FILE_IO (OpenFile Write)] } Eff e ()

54+ writeLine : String -> Eff () [FILE_IO (OpenFile Write)]

55− eof : Handler FileIO e =>

55+ eof : Eff Bool [FILE_IO (OpenFile Read)]

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

57

56

58 instance Handler FileIO IO

57 instance Handler FileIO IO

59

58

70

69

71 RND : EFFECT

70 RND : EFFECT

72

71

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

72+ srand : Integer -> Eff m () [RND]

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

73+ rndInt : Integer -> Integer -> Eff m Integer [RND]

75− rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))

74+ rndFin : (k : Nat) -> Eff m (Fin (S k)) [RND]

76

75

77 instance Handler Random m

76 instance Handler Random m

78

77

87

86

88 SELECT : EFFECT

87 SELECT : EFFECT

89

88

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

89+ select : List a -> Eff m a [SELECT]

91

90

92 instance Handler Selection Maybe

91 instance Handler Selection Maybe

93 instance Handler Selection List

92 instance Handler Selection List

103

102

104 STATE : Type -> EFFECT

103 STATE : Type -> EFFECT

105

104

106− get : { [STATE x] } Eff m x

105+ get : Eff m x [STATE x]

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

106+ put : x -> Eff m () [STATE x]

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

107+ putM : y -> Eff m () [STATE x] [STATE y]

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

108+ update : (x -> x) -> Eff m () [STATE x]

110

109

111 instance Handler State m

110 instance Handler State m

112

111

122

121

123 STDIO : EFFECT

122 STDIO : EFFECT

124

123

125− putChar : Handler StdIO m => Char -> { [STDIO] } Eff m ()

124+ putChar : Handler StdIO m => Char -> Eff m () [STDIO]

126− putStr : Handler StdIO m => String -> { [STDIO] } Eff m ()

125+ putStr : Handler StdIO m => String -> Eff m () [STDIO]

127− putStrLn : Handler StdIO m => String -> { [STDIO] } Eff m ()

126+ putStrLn : Handler StdIO m => String -> Eff m () [STDIO]

128

127

129− getStr : Handler StdIO m => { [STDIO] } Eff m String

128+ getStr : Handler StdIO m => Eff m String [STDIO]

130− getChar : Handler StdIO m => { [STDIO] } Eff m Char

129+ getChar : Handler StdIO m => Eff m Char [STDIO]

131

130

132 instance Handler StdIO IO

131 instance Handler StdIO IO

133 instance Handler StdIO (IOExcept a)

132 instance Handler StdIO (IOExcept a)

145

144

146 SYSTEM : EFFECT

145 SYSTEM : EFFECT

147

146

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

147+ getArgs : Handler System e => Eff e (List String) [SYSTEM]

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

148+ time : Handler System e => Eff e Int [SYSTEM]

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

149+ getEnv : Handler System e => String -> Eff e (Maybe String) [SYSTEM]

151

150

152 instance Handler System IO

151 instance Handler System IO

153 instance Handler System (IOExcept a)

152 instance Handler System (IOExcept a)