@@ -162,26 +162,28 @@ relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
162data Eff : (m : Type -> Type) ->
162data Eff : (m : Type -> Type) ->
163 (x : Type) ->
163 (x : Type) ->
164 List EFFECT -> (x -> List EFFECT) -> Type where
164 List EFFECT -> (x -> List EFFECT) -> Type where
165− value : a -> Eff m a xs (\v => xs)
165+ value : a -> Eff m a xs (\v => xs)
166+ with_val : (val : a) -> Eff m () xs (\v => xs' val) ->
166− ebind : Eff m a xs xs' ->
168+ ebind : Eff m a xs xs' ->
167− ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
169+ ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
168− effect : (prf : EffElem e a xs) ->
170+ effect : (prf : EffElem e a xs) ->
169− (eff : e t a b) ->
171+ (eff : e t a b) ->
170− Eff m t xs (\v => updateResTy v xs prf eff)
172+ Eff m t xs (\v => updateResTy v xs prf eff)
172− lift : (prf : SubList ys xs) ->
174+ lift : (prf : SubList ys xs) ->
173− Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
175+ Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
174− newInit : Handler e m =>
176+ newInit : Handler e m =>
176− Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
178+ Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
177− Eff m a xs (\v => xs')
179+ Eff m a xs (\v => xs')
178− catch : Catchable m err =>
180+ catch : Catchable m err =>
179− Eff m a xs xs' -> (err -> Eff m a xs xs') ->
181+ Eff m a xs xs' -> (err -> Eff m a xs xs') ->
180− Eff m a xs xs'
182+ Eff m a xs xs'
182− (:-) : (l : ty) ->
184+ (:-) : (l : ty) ->
183− Eff m t [x] xs' -> -- [x] (\v => xs) ->
185+ Eff m t [x] xs' -> -- [x] (\v => xs) ->
184− Eff m t [l ::: x] (\v => map (l :::) (xs' v))
186+ Eff m t [l ::: x] (\v => map (l :::) (xs' v))
186(>>=) : Eff m a xs xs' ->
188(>>=) : Eff m a xs xs' ->
187 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
189 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
@@ -197,6 +199,8 @@ infixl 2 <$>
197pure : a -> Eff m a xs (\v => xs)
199pure : a -> Eff m a xs (\v => xs)
198pure = value
200pure = value
202+syntax pureM [val] = with_val val (pure ())
200(<$>) : Eff m (a -> b) xs (\v => xs) ->
204(<$>) : Eff m (a -> b) xs (\v => xs) ->
201 Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
205 Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
202(<$>) prog v = do fn <- prog
206(<$>) prog v = do fn <- prog
@@ -220,6 +224,7 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
221eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
225eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
222eff env (value x) k = k x env
226eff env (value x) k = k x env
227+eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
223eff env (prog `ebind` c) k
228eff env (prog `ebind` c) k
224 = eff env prog (\p', env' => eff env' (c p') k)
229 = eff env prog (\p', env' => eff env' (c p') k)
225eff env (effect prf effP) k = execEff env prf effP k
230eff env (effect prf effP) k = execEff env prf effP k