9724992 · Idris-dev · git.iko.soy

effects/Effect/Exception.idr+3

compare with master

unifiedsplit

@@ -17,6 +17,9 @@ instance Show a => Handler (Exception a) IO where

17instance Handler (Exception a) (IOExcept a) where

18 handle _ (Raise e) k = ioM (return (Left e))

19

20+instance Handler (Exception a) (Either a) where

21+ handle _ (Raise e) k = Left e

22+

20EXCEPTION : Type -> EFFECT

23EXCEPTION : Type -> EFFECT

21EXCEPTION t = MkEff () (Exception t)

24EXCEPTION t = MkEff () (Exception t)

22

25

effects/Effect/StdIO.idr+5−4

@@ -19,9 +19,6 @@ instance Handler StdIO (IOExcept a) where

19

20data IOStream a = MkStream (List String -> (a, List String))

21

22−injStream : a -> IOStream a

23−injStream v = MkStream (\x => (v, []))

24−

25instance Handler StdIO IOStream where

22instance Handler StdIO IOStream where

26 handle () (PutStr s) k

23 handle () (PutStr s) k

27 = MkStream (\x => case k () () of

24 = MkStream (\x => case k () () of

@@ -55,5 +52,9 @@ mkStrFn : Env IOStream xs ->

55 List String -> (a, List String)

52 List String -> (a, List String)

56mkStrFn {a} env p input = case mkStrFn' of

53mkStrFn {a} env p input = case mkStrFn' of

57 MkStream f => f input

54 MkStream f => f input

55+ where injStream : a -> IOStream a

56+ injStream v = MkStream (\x => (v, []))

58− where mkStrFn' : IOStream a

57+ mkStrFn' : IOStream a

59 mkStrFn' = runWith injStream env p

58 mkStrFn' = runWith injStream env p

59+

60+

effects/Effects.idr+1−2

@@ -100,8 +100,7 @@ data EffM : (m : Type -> Type) ->

100 List EFFECT -> List EFFECT -> Type -> Type where

101 value : a -> EffM m xs xs a

102 ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b

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

104− (prf : EffElem e a xs) ->

103+ effect : (prf : EffElem e a xs) ->

105 (eff : e a b t) ->

104 (eff : e a b t) ->

106 EffM m xs (updateResTy xs prf eff) t

105 EffM m xs (updateResTy xs prf eff) t

107 lift : (prf : SubList ys xs) ->

106 lift : (prf : SubList ys xs) ->