@@ -1,308 +0,0 @@
1−module Effects
2−
3−import Language.Reflection
4−import Control.Catchable
5−
6−%access public
7−
8−---- Effects
9−
10−Effect : Type
11−Effect = Type -> Type -> Type -> Type
12−
13−%error_reverse
14−data EFFECT : Type where
15− MkEff : Type -> Effect -> EFFECT
16−
17−class Handler (e : Effect) (m : Type -> Type) where
18− handle : res -> (eff : e res res' t) -> (res' -> t -> m a) -> m a
19−
20−---- Properties and proof construction
21−
22−using (xs : List a, ys : List a)
23− data SubList : List a -> List a -> Type where
24− SubNil : SubList {a} [] []
25− Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
26− Drop : SubList xs ys -> SubList xs (x :: ys)
27−
28− subListId : SubList xs xs
29− subListId {xs = Nil} = SubNil
30− subListId {xs = x :: xs} = Keep subListId
31−
32−data Env : (m : Type -> Type) -> List EFFECT -> Type where
33− Nil : Env m Nil
34− (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
35−
36−data EffElem : (Type -> Type -> Type -> Type) -> Type ->
37− List EFFECT -> Type where
38− Here : EffElem x a (MkEff a x :: xs)
39− There : EffElem x a xs -> EffElem x a (y :: xs)
40−
41−-- make an environment corresponding to a sub-list
42−dropEnv : Env m ys -> SubList xs ys -> Env m xs
43−dropEnv [] SubNil = []
44−dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
45−dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
46−
47−updateWith : (ys' : List a) -> (xs : List a) ->
48− SubList ys xs -> List a
49−updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
50−updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
51−updateWith [] [] SubNil = []
52−updateWith (y :: ys) [] SubNil = y :: ys
53−updateWith [] (x :: xs) (Keep rest) = []
54−
55−-- put things back, replacing old with new in the sub-environment
56−rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
57− Env m xs -> Env m (updateWith ys' xs prf)
58−rebuildEnv [] SubNil env = env
59−rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
60−rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
61−rebuildEnv (x :: xs) SubNil [] = x :: xs
62−
63−---- The Effect EDSL itself ----
64−
65−-- some proof automation
66−
67−%reflection
68−reflectListEffElem : List a -> Tactic
69−reflectListEffElem [] = Refine "Here" `Seq` Solve
70−reflectListEffElem (x :: xs)
71− = Try (Refine "Here" `Seq` Solve)
72− (Refine "There" `Seq` (Solve `Seq` reflectListEffElem xs))
73−-- TMP HACK! FIXME!
74−-- The evaluator needs a 'function case' to know its a reflection function
75−-- until we propagate that information! Without this, the _ case won't get
76−-- matched.
77−reflectListEffElem (x ++ y) = Refine "Here" `Seq` Solve
78−reflectListEffElem _ = Refine "Here" `Seq` Solve
79−
80−%reflection
81−reflectSubList : List a -> Tactic
82−reflectSubList [] = Refine "SubNil" `Seq` Solve
83−reflectSubList (x :: xs)
84− = Try (Refine "subListId" `Seq` Solve)
85− (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))
86− (Refine "Drop" `Seq` (Solve `Seq` reflectSubList xs)))
87−reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve
88−reflectSubList _ = Refine "subListId" `Seq` Solve
89−
90−%reflection
91−reflectEff : (P : Type) -> Tactic
92−reflectEff (EffElem m a xs)
93− = reflectListEffElem xs `Seq` Solve
94−reflectEff (SubList xs ys)
95− = reflectSubList ys `Seq` Solve
96−
97−updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->
98− List EFFECT
99−updateResTy {b} (MkEff a e :: xs) Here n = (MkEff b e) :: xs
100−updateResTy (x :: xs) (There p) n = x :: updateResTy xs p n
101−
102−updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
103− List EFFECT
104−updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
105−updateResTyImm (x :: xs) (There p) b = x :: updateResTyImm xs p b
106−
107−infix 5 :::, :-, :=
108−
109−data LRes : lbl -> Type -> Type where
110− (:=) : (x : lbl) -> res -> LRes x res
111−
112−(:::) : lbl -> EFFECT -> EFFECT
113−(:::) {lbl} x (MkEff r eff) = MkEff (LRes x r) eff
114−
115−private
116−unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
117−unlabel {m} {x = MkEff a eff} [l := v] = [v]
118−
119−private
120−relabel : (l : ty) -> Env m [x] -> Env m [l ::: x]
121−relabel {x = MkEff a eff} l [v] = [l := v]
122−
123−-- the language of Effects
124−
125−data EffM : (m : Type -> Type) ->
126− List EFFECT -> List EFFECT -> Type -> Type where
127− value : a -> EffM m xs xs a
128− ebind : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
129− effect : (prf : EffElem e a xs) ->
130− (eff : e a b t) ->
131− EffM m xs (updateResTy xs prf eff) t
132− lift : (prf : SubList ys xs) ->
133− EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
134− new : Handler e m =>
135− res -> EffM m (MkEff res e :: xs) (MkEff res' e :: xs') a ->
136− EffM m xs xs' a
137− test : (prf : EffElem e (Either l r) xs) ->
138− EffM m (updateResTyImm xs prf l) xs' t ->
139− EffM m (updateResTyImm xs prf r) xs' t ->
140− EffM m xs xs' t
141− test_lbl : {x : lbl} ->
142− (prf : EffElem e (LRes x (Either l r)) xs) ->
143− EffM m (updateResTyImm xs prf (LRes x l)) xs' t ->
144− EffM m (updateResTyImm xs prf (LRes x r)) xs' t ->
145− EffM m xs xs' t
146− catch : Catchable m err =>
147− EffM m xs xs' a -> (err -> EffM m xs xs' a) ->
148− EffM m xs xs' a
149− (:-) : (l : ty) -> EffM m [x] [y] t -> EffM m [l ::: x] [l ::: y] t
150−
151−syntax [tag] ":!" [val] = !(tag :- val)
152−
153−-- Eff : List (EFFECT m) -> Type -> Type
154−
155−-- For making proofs implicitly for 'test' and 'test_lbl'
156−
157−syntax if_valid then [e] else [t] =
158− test (tactics { byReflection reflectEff; }) t e
159−
160−syntax if_valid [lbl] then [e] else [t] =
161− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
162−
163−syntax if_error then [t] else [e] =
164− test (tactics { byReflection reflectEff; }) t e
165−
166−syntax if_error [lbl] then [t] else [e] =
167− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
168−
169−-- These may read better in some contexts
170−
171−syntax if_right then [e] else [t] =
172− test (tactics { byReflection reflectEff; }) t e
173−
174−syntax if_right [lbl] then [e] else [t] =
175− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
176−
177−syntax if_left then [t] else [e] =
178− test (tactics { byReflection reflectEff; }) t e
179−
180−syntax if_left [lbl] then [t] else [e] =
181− test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e
182−
183−
184−-- for 'do' notation
185−
186−return : a -> EffM m xs xs a
187−return x = value x
188−
189−(>>=) : EffM m xs xs' a -> (a -> EffM m xs' xs'' b) -> EffM m xs xs'' b
190−(>>=) = ebind
191−
192−-- for idiom brackets
193−
194−infixl 2 <$>
195−
196−pure : a -> EffM m xs xs a
197−pure = value
198−
199−(<$>) : EffM m xs xs (a -> b) -> EffM m xs xs a -> EffM m xs xs b
200−(<$>) prog v = do fn <- prog
201− arg <- v
202− return (fn arg)
203−
204−-- an interpreter
205−
206−private
207−execEff : Env m xs -> (p : EffElem e res xs) ->
208− (eff : e res b a) ->
209− (Env m (updateResTy xs p eff) -> a -> m t) -> m t
210−execEff (val :: env) Here eff' k
211− = handle val eff' (\res, v => k (res :: env) v)
212−execEff {e} {res} {b} {a} (val :: env) (There p) eff k
213− = execEff {e} {res} {b} {a} env p eff (\env', v => k (val :: env') v)
214−
215−private
216−testEff : Env m xs -> (p : EffElem e (Either l r) xs) ->
217− (Env m (updateResTyImm xs p l) -> m b) ->
218− (Env m (updateResTyImm xs p r) -> m b) ->
219− m b
220−testEff (Left err :: env) Here lk rk = lk (err :: env)
221−testEff (Right ok :: env) Here lk rk = rk (ok :: env)
222−testEff (val :: env) (There p) lk rk
223− = testEff env p (\envk => lk (val :: envk))
224− (\envk => rk (val :: envk))
225−
226−private
227−testEffLbl : {x : lblTy} ->
228− Env m xs -> (p : EffElem e (LRes x (Either l r)) xs) ->
229− (Env m (updateResTyImm xs p (LRes x l)) -> m b) ->
230− (Env m (updateResTyImm xs p (LRes x r)) -> m b) ->
231− m b
232−testEffLbl ((lbl := Left err) :: env) Here lk rk = lk ((lbl := err) :: env)
233−testEffLbl ((lbl := Right ok) :: env) Here lk rk = rk ((lbl := ok) :: env)
234−testEffLbl (val :: env) (There p) lk rk
235− = testEffLbl env p (\envk => lk (val :: envk))
236− (\envk => rk (val :: envk))
237−
238−-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
239−-- updates can be propagated even through failing computations?
240−
241−eff : Env m xs -> EffM m xs xs' a -> (Env m xs' -> a -> m b) -> m b
242−eff env (value x) k = k env x
243−eff env (prog `ebind` c) k
244− = eff env prog (\env', p' => eff env' (c p') k)
245−eff env (effect prf effP) k = execEff env prf effP k
246−eff env (lift prf effP) k
247− = let env' = dropEnv env prf in
248− eff env' effP (\envk, p' => k (rebuildEnv envk prf env) p')
249−eff env (new r prog) k
250− = eff (r :: env) prog (\(v :: envk), p' => k envk p')
251−eff env (test prf l r) k
252− = testEff env prf (\envk => eff envk l k) (\envk => eff envk r k)
253−eff env (test_lbl prf l r) k
254− = testEffLbl env prf (\envk => eff envk l k) (\envk => eff envk r k)
255−eff env (catch prog handler) k
256− = catch (eff env prog k)
257− (\e => eff env (handler e) k)
258−-- FIXME:
259−-- xs is needed explicitly because otherwise the pattern binding for
260−-- 'l' appears too late. Solution seems to be to reorder patterns at the
261−-- end so that everything is in scope when it needs to be.
262−eff {xs = [l ::: x]} env (l :- prog) k
263− = let env' = unlabel env in
264− eff env' prog (\envk, p' => k (relabel l envk) p')
265−
266−implicit
267−lift' : EffM m ys ys' t ->
268− {default tactics { byReflection reflectEff; }
269− prf : SubList ys xs} ->
270− EffM m xs (updateWith ys' xs prf) t
271−lift' e {prf} = lift prf e
272−
273−implicit
274−effect' : {a, b: _} -> {e : Effect} ->
275− (eff : e a b t) ->
276− {default tactics { byReflection reflectEff; }
277− prf : EffElem e a xs} ->
278− EffM m xs (updateResTy xs prf eff) t
279−effect' e {prf} = effect prf e
280−
281−
282−run : Applicative m => Env m xs -> EffM m xs xs' a -> m a
283−run env prog = eff env prog (\env, r => pure r)
284−
285−runEnv : Applicative m => Env m xs -> EffM m xs xs' a -> m (Env m xs', a)
286−runEnv env prog = eff env prog (\env, r => pure (env, r))
287−
288−runPure : Env id xs -> EffM id xs xs' a -> a
289−runPure env prog = eff env prog (\env, r => r)
290−
291−-- runPureEnv : Env id xs -> EffM id xs xs' a -> (Env id xs', a)
292−-- runPureEnv env prog = eff env prog (\env, r => (env, r))
293−
294−runWith : (a -> m a) -> Env m xs -> EffM m xs xs' a -> m a
295−runWith inj env prog = eff env prog (\env, r => inj r)
296−
297−Eff : (Type -> Type) -> List EFFECT -> Type -> Type
298−Eff m xs t = EffM m xs xs t
299−
300−-- some higher order things
301−
302−mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)
303−mapE f [] = pure []
304−mapE f (x :: xs) = [| f x :: mapE f xs |]
305−
306−when : Applicative m => Bool -> Lazy (Eff m xs ()) -> Eff m xs ()
307−when True e = e
308−when False e = pure ()