git.iko.soy/Idris-dev
on master help sign in
Minor tinkering with effects
commit97249925ad515814f15d8f0f5963c79657d78b93 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 20 Mar 2013, 12:08 (14 years ago) parent8cf25fc
3 files changed+9−6
compare with master
unifiedsplit
effects/Effect/Exception.idr+3 effects/Effect/StdIO.idr+5−4 effects/Effects.idr+1−2
effects/Effect/Exception.idr+3
@@ -17,6 +17,9 @@ instance Show a => Handler (Exception a) IO where
1717instance Handler (Exception a) (IOExcept a) where
1818 handle _ (Raise e) k = ioM (return (Left e))
1919
20+instance Handler (Exception a) (Either a) where
21+ handle _ (Raise e) k = Left e
22+
2023EXCEPTION : Type -> EFFECT
2124EXCEPTION t = MkEff () (Exception t)
2225
effects/Effect/StdIO.idr+5−4
@@ -19,9 +19,6 @@ instance Handler StdIO (IOExcept a) where
1919
2020data IOStream a = MkStream (List String -> (a, List String))
2121
22−injStream : a -> IOStream a
23−injStream v = MkStream (\x => (v, []))
24−
2522instance Handler StdIO IOStream where
2623 handle () (PutStr s) k
2724 = MkStream (\x => case k () () of
@@ -55,5 +52,9 @@ mkStrFn : Env IOStream xs ->
5552 List String -> (a, List String)
5653mkStrFn {a} env p input = case mkStrFn' of
5754 MkStream f => f input
58− where mkStrFn' : IOStream a
55+ where injStream : a -> IOStream a
56+ injStream v = MkStream (\x => (v, []))
57+ mkStrFn' : IOStream a
5958 mkStrFn' = runWith injStream env p
59+
60+
effects/Effects.idr+1−2
@@ -100,8 +100,7 @@ data EffM : (m : Type -> Type) ->
100100 List EFFECT -> List EFFECT -> Type -> Type where
101101 value : a -> EffM m xs xs a
102102 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) ->
105104 (eff : e a b t) ->
106105 EffM m xs (updateResTy xs prf eff) t
107106 lift : (prf : SubList ys xs) ->