@@ -136,9 +136,7 @@ relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
136data Eff : (x : Type)
136data Eff : (x : Type)
137 -> (es : List EFFECT)
137 -> (es : List EFFECT)
138 -> (ce : x -> List EFFECT) -> Type where
138 -> (ce : x -> List EFFECT) -> Type where
139− value : a -> Eff a xs (\v => xs)
140− with_val : (val : a) -> Eff () xs (\v => xs' val) ->
139+ value : (val : a) -> Eff a (xs val) xs
142 ebind : Eff a xs xs' ->
140 ebind : Eff a xs xs' ->
143 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
141 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
144 callP : (prf : EffElem e a xs) ->
142 callP : (prf : EffElem e a xs) ->
@@ -182,7 +180,7 @@ pure : a -> Eff a xs (\v => xs)
182pure = value
180pure = value
184pureM : (val : a) -> Eff a (xs val) xs
182pureM : (val : a) -> Eff a (xs val) xs
185−pureM val = with_val val (pure ())
183+pureM = value
187(<$>) : Eff (a -> b) xs (\v => xs) ->
185(<$>) : Eff (a -> b) xs (\v => xs) ->
188 Eff a xs (\v => xs) -> Eff b xs (\v => xs)
186 Eff a xs (\v => xs) -> Eff b xs (\v => xs)
@@ -207,7 +205,6 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
208eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
206eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
209eff env (value x) k = k x env
207eff env (value x) k = k x env
210−eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
211eff env (prog `ebind` c) k
208eff env (prog `ebind` c) k
212 = eff env prog (\p', env' => eff env' (c p') k)
209 = eff env prog (\p', env' => eff env' (c p') k)
213eff env (callP prf effP) k = execEff env prf effP k
210eff env (callP prf effP) k = execEff env prf effP k