git.iko.soy/Idris-dev
on master help sign in
Replace EffElem with Data.List.Elem
7d0fd03Eric Weinstein
libs/effects/Effects.idr+10−16
compare with master
unifiedsplit
@@ -3,6 +3,7 @@ module Effects
3import Language.Reflection
3import Language.Reflection
4import public Effect.Default
4import public Effect.Default
5import Data.Vect
5import Data.Vect
6+import public Data.List
6
7
7--- Effectful computations are described as algebraic data types that
8--- Effectful computations are described as algebraic data types that
8--- explain how an effect is interpreted in some underlying context.
9--- explain how an effect is interpreted in some underlying context.
@@ -89,7 +90,7 @@ public export
89data SubElem : a -> List a -> Type where
90data SubElem : a -> List a -> Type where
90 Z : SubElem a (a :: as)
91 Z : SubElem a (a :: as)
91 S : SubElem a as -> SubElem a (b :: as)
92 S : SubElem a as -> SubElem a (b :: as)
92−
93+
93public export
94public export
94data SubList : List a -> List a -> Type where
95data SubList : List a -> List a -> Type where
95 SubNil : SubList [] xs
96 SubNil : SubList [] xs
@@ -142,13 +143,6 @@ namespace Env
142 Nil : Env m Nil
143 Nil : Env m Nil
143 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
144 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
144
145
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−
152total envElem : SubElem x xs -> Env m xs -> Env m [x]
146total envElem : SubElem x xs -> Env m xs -> Env m [x]
153envElem Z (x :: xs) = [x]
147envElem Z (x :: xs) = [x]
154envElem (S k) (x :: xs) = envElem k xs
148envElem (S k) (x :: xs) = envElem k xs
@@ -158,7 +152,7 @@ total dropEnv : Env m ys -> SubList xs ys -> Env m xs
158dropEnv [] SubNil = []
152dropEnv [] SubNil = []
159dropEnv [] (InList idx rest) = absurd idx
153dropEnv [] (InList idx rest) = absurd idx
160dropEnv (y::ys) SubNil = []
154dropEnv (y::ys) SubNil = []
161−dropEnv e@(y::ys) (InList idx rest) =
155+dropEnv e@(y::ys) (InList idx rest) =
162 let [x] = envElem idx e
156 let [x] = envElem idx e
163 in x :: dropEnv e rest
157 in x :: dropEnv e rest
164
158
@@ -191,13 +185,13 @@ total rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
191rebuildEnv [] SubNil env = env
185rebuildEnv [] SubNil env = env
192rebuildEnv (x :: xs) SubNil env = env
186rebuildEnv (x :: xs) SubNil env = env
193rebuildEnv [] (InList w s) env = env
187rebuildEnv [] (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)
195
189
196-- -------------------------------------------------- [ The Effect EDSL itself ]
190-- -------------------------------------------------- [ The Effect EDSL itself ]
197
191
198public export
192public export
199total updateResTy : (val : t) ->
193total 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 ->
201 List EFFECT
195 List EFFECT
202updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
196updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
203updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
197updateResTy val (x :: xs) (There p) n = x :: updateResTy val xs p n
@@ -238,7 +232,7 @@ data EffM : (m : Type -> Type) -> (x : Type)
238 Value : (val : a) -> EffM m a (xs val) xs
232 Value : (val : a) -> EffM m a (xs val) xs
239 EBind : EffM m a xs xs' ->
233 EBind : EffM m a xs xs' ->
240 ((val : a) -> EffM m b (xs' val) xs'') -> EffM m b xs xs''
234 ((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) ->
242 (eff : e t a b) ->
236 (eff : e t a b) ->
243 EffM m t xs (\v => updateResTy v xs prf eff)
237 EffM m t xs (\v => updateResTy v xs prf eff)
244
238
@@ -327,7 +321,7 @@ pureM = Value
327(<*>) prog v = do fn <- prog
321(<*>) prog v = do fn <- prog
328 arg <- v
322 arg <- v
329 return (fn arg)
323 return (fn arg)
330−
324+
331(<$>) : (a -> b) ->
325(<$>) : (a -> b) ->
332 EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)
326 EffM m a xs (\v => xs) -> EffM m b xs (\v => xs)
333(<$>) f v = pure f <*> v
327(<$>) f v = pure f <*> v
@@ -336,7 +330,7 @@ pureM = Value
336 EffM m b xs (\v => xs) -> EffM m b xs (\v => xs)
330 EffM m b xs (\v => xs) -> EffM m b xs (\v => xs)
337a *> b = do a
331a *> b = do a
338 b
332 b
339−
333+
340new : Handler e' m => (e : EFFECT) -> resTy ->
334new : Handler e' m => (e : EFFECT) -> resTy ->
341 {auto prf : e = MkEff resTy e'} ->
335 {auto prf : e = MkEff resTy e'} ->
342 EffM m t (e :: es) (\v => e :: es) ->
336 EffM m t (e :: es) (\v => e :: es) ->
@@ -346,7 +340,7 @@ new = New
346-- ---------------------------------------------------------- [ an interpreter ]
340-- ---------------------------------------------------------- [ an interpreter ]
347
341
348private
342private
349−execEff : Env m xs -> (p : EffElem e res xs) ->
343+execEff : Env m xs -> (p : with List Elem (MkEff res e) xs) ->
350 (eff : e a res resk) ->
344 (eff : e a res resk) ->
351 ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
345 ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
352execEff (val :: env) Here eff' k
346execEff (val :: env) Here eff' k
@@ -387,7 +381,7 @@ syntax MkDefaultEnv = with Env
387%no_implicit
381%no_implicit
388call : {a, b: _} -> {e : Effect} ->
382call : {a, b: _} -> {e : Effect} ->
389 (eff : e t a b) ->
383 (eff : e t a b) ->
390− {auto prf : EffElem e a xs} ->
384+ {auto prf : with List Elem (MkEff a e) xs} ->
391 EffM m t xs (\v => updateResTy v xs prf eff)
385 EffM m t xs (\v => updateResTy v xs prf eff)
392call e {prf} = CallP prf e
386call e {prf} = CallP prf e
393
387