@@ -79,7 +79,12 @@ findSubList (S n) ctxt goal
7979updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
8080 List EFFECT
8181updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs
82−updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n
82+updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n
83+
84+updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
85+ List EFFECT
86+updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
87+updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b
8388
8489infix 5 :::, :-, :=
8590
@@ -111,6 +116,15 @@ data EffM : (m : Type -> Type) ->
111116 new : Handler e m =>
112117 res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->
113118 EffM m xs xs' a
119+ test : (prf : EffElem e (Either l r) xs) ->
120+ EffM m (updateResTyImm xs prf l) xs' t ->
121+ EffM m (updateResTyImm xs prf r) xs' t ->
122+ EffM m xs xs' t
123+ test_lbl : {x : lbl} ->
124+ (prf : EffElem e (LRes x (Either l r)) xs) ->
125+ EffM m (updateResTyImm xs prf (LRes x l)) xs' t ->
126+ EffM m (updateResTyImm xs prf (LRes x r)) xs' t ->
127+ EffM m xs xs' t
114128 catch : Catchable m err =>
115129 EffM m xs xs' a -> (err -> EffM m xs xs' a) ->
116130 EffM m xs xs' a
@@ -132,6 +146,27 @@ effect' : {a, b: _} -> {e : Effect} ->
132146 EffM m xs (updateResTy xs prf eff) t
133147effect' {prf} e = effect prf e
134148
149+data WrapEffM : (m : Type -> Type) ->
150+ List EFFECT -> List EFFECT -> Type -> Type where
151+ WEffM : EffM m xs xs' t -> WrapEffM m xs xs' t
152+
153+-- wrap subprograms to prevent lifting (need to guarantee same effects as
154+-- parent!)
155+
156+test_lbl' : {x : lbl} ->
157+ {default tactics { applyTactic findEffElem 20; solve; }
158+ prf : EffElem e (LRes x (Either l r)) xs} ->
159+ WrapEffM m (updateResTyImm xs prf (LRes x l)) xs' t ->
160+ WrapEffM m (updateResTyImm xs prf (LRes x r)) xs' t ->
161+ EffM m xs xs' t
162+test_lbl' {prf} (WEffM l) (WEffM r) = test_lbl prf l r
163+
164+test' : {default tactics { applyTactic findEffElem 20; solve; }
165+ prf : EffElem e (Either l r) xs} ->
166+ EffM m (updateResTyImm xs prf l) xs' t ->
167+ EffM m (updateResTyImm xs prf r) xs' t ->
168+ EffM m xs xs' t
169+test' {prf} l r = test prf l r
135170
136171-- for 'do' notation
137172
@@ -164,6 +199,29 @@ execEff (val :: env) Here eff' k
164199execEff (val :: env) (There p) eff k
165200 = execEff env p eff (\env', v => k (val :: env') v)
166201
202+private
203+testEff : Env m xs -> (p : EffElem e (Either l r) xs) ->
204+ (Env m (updateResTyImm xs p l) -> m b) ->
205+ (Env m (updateResTyImm xs p r) -> m b) ->
206+ m b
207+testEff (Left err :: env) Here lk rk = lk (err :: env)
208+testEff (Right ok :: env) Here lk rk = rk (ok :: env)
209+testEff (val :: env) (There p) lk rk
210+ = testEff env p (\envk => lk (val :: envk))
211+ (\envk => rk (val :: envk))
212+
213+private
214+testEffLbl : {x : lbl} ->
215+ Env m xs -> (p : EffElem e (LRes x (Either l r)) xs) ->
216+ (Env m (updateResTyImm xs p (LRes x l)) -> m b) ->
217+ (Env m (updateResTyImm xs p (LRes x r)) -> m b) ->
218+ m b
219+testEffLbl ((lbl := Left err) :: env) Here lk rk = lk ((lbl := err) :: env)
220+testEffLbl ((lbl := Right ok) :: env) Here lk rk = rk ((lbl := ok) :: env)
221+testEffLbl (val :: env) (There p) lk rk
222+ = testEffLbl env p (\envk => lk (val :: envk))
223+ (\envk => rk (val :: envk))
224+
167225-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
168226-- updates can be propagated even through failing computations?
169227
@@ -178,6 +236,10 @@ eff env (lift prf effP) k
178236eff env (new r prog) k
179237 = let env' = r :: env in
180238 eff env' prog (\(v :: envk), p' => k envk p')
239+eff env (test prf l r) k
240+ = testEff env prf (\envk => eff envk l k) (\envk => eff envk r k)
241+eff env (test_lbl prf l r) k
242+ = testEffLbl env prf (\envk => eff envk l k) (\envk => eff envk r k)
181243eff env (catch prog handler) k
182244 = catch (eff env prog k)
183245 (\e => eff env (handler e) k)