@@ -3,6 +3,7 @@ module Effects
33import Language.Reflection
44import public Effect.Default
55import Data.Vect
6+import public Data.List
67
78--- Effectful computations are described as algebraic data types that
89--- explain how an effect is interpreted in some underlying context.
@@ -89,7 +90,7 @@ public export
8990data SubElem : a -> List a -> Type where
9091 Z : SubElem a (a :: as)
9192 S : SubElem a as -> SubElem a (b :: as)
92−
93+
9394public export
9495data SubList : List a -> List a -> Type where
9596 SubNil : SubList [] xs
@@ -142,13 +143,6 @@ namespace Env
142143 Nil : Env m Nil
143144 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
144145
145−namespace EffElem
146− public export
147− data EffElem : Effect -> Type ->
148− List EFFECT -> Type where
149− Here : EffElem x a (MkEff a x :: xs)
150− There : EffElem x a xs -> EffElem x a (y :: xs)
151−
152146total envElem : SubElem x xs -> Env m xs -> Env m [x]
153147envElem Z (x :: xs) = [x]
154148envElem (S k) (x :: xs) = envElem k xs
@@ -158,7 +152,7 @@ total dropEnv : Env m ys -> SubList xs ys -> Env m xs
158152dropEnv [] SubNil = []
159153dropEnv [] (InList idx rest) = absurd idx
160154dropEnv (y::ys) SubNil = []
161−dropEnv e@(y::ys) (InList idx rest) =
155+dropEnv e@(y::ys) (InList idx rest) =
162156 let [x] = envElem idx e
163157 in x :: dropEnv e rest
164158
@@ -191,13 +185,13 @@ total rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
191185rebuildEnv [] SubNil env = env
192186rebuildEnv (x :: xs) SubNil env = env
193187rebuildEnv [] (InList w s) env = env
194−rebuildEnv (x :: xs) (InList idx rest) env = replaceEnvAt x idx (rebuildEnv xs rest env)
188+rebuildEnv (x :: xs) (InList idx rest) env = replaceEnvAt x idx (rebuildEnv xs rest env)
195189
196190-- -------------------------------------------------- [ The Effect EDSL itself ]
197191
198192public export
199193total updateResTy : (val : t) ->
200− (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
194+ (xs : List EFFECT) -> with List Elem (MkEff a e) xs -> e t a b ->
201195 List EFFECT
202196updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
203197updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
@@ -238,7 +232,7 @@ data EffM : (m : Type -> Type) -> (x : Type)
238232 Value : (val : a) -> EffM m a (xs val) xs
239233 EBind : EffM m a xs xs' ->
240234 ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
241− CallP : (prf : EffElem e a xs) ->
235+ CallP : (prf : with List Elem (MkEff a e) xs) ->
242236 (eff : e t a b) ->
243237 EffM m t xs (\v => updateResTy v xs prf eff)
244238
@@ -327,7 +321,7 @@ pureM = Value
327321(<*>) prog v = do fn <- prog
328322 arg <- v
329323 return (fn arg)
330−
324+
331325(<$>) : (a -> b) ->
332326 EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)
333327(<$>) f v = pure f <*> v
@@ -336,7 +330,7 @@ pureM = Value
336330 EffM m b xs (\v => xs) -> EffM m b xs (\v => xs)
337331a *> b = do a
338332 b
339−
333+
340334new : Handler e' m => (e : EFFECT) -> resTy ->
341335 {auto prf : e = MkEff resTy e'} ->
342336 EffM m t (e :: es) (\v => e :: es) ->
@@ -346,7 +340,7 @@ new = New
346340-- ---------------------------------------------------------- [ an interpreter ]
347341
348342private
349−execEff : Env m xs -> (p : EffElem e res xs) ->
343+execEff : Env m xs -> (p : with List Elem (MkEff res e) xs) ->
350344 (eff : e a res resk) ->
351345 ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
352346execEff (val :: env) Here eff' k
@@ -387,7 +381,7 @@ syntax MkDefaultEnv = with Env
387381%no_implicit
388382call : {a, b: _} -> {e : Effect} ->
389383 (eff : e t a b) ->
390− {auto prf : EffElem e a xs} ->
384+ {auto prf : with List Elem (MkEff a e) xs} ->
391385 EffM m t xs (\v => updateResTy v xs prf eff)
392386call e {prf} = CallP prf e
393387