@@ -0,0 +1,63 @@
1+module Effect.Protocols
2+
3+-- Helpers for writing and using effects that implement protocols with
4+-- state transitions
5+
6+import public Effects
7+
8+infix 5 :=>
9+
10+-- 'sig' gives the signature for an effect. There are three versions
11+-- depending on whether there is no state change, a non-dependent change,
12+-- or a dependent change. These are easily disambiguated by type.
13+
14+namespace NoUpdateEffect
15+ sig : Effect -> Type -> Type -> Type
16+ sig e r e_in = e r e_in (\v => e_in)
17+
18+namespace UpdateEffect
19+ sig : Effect -> Type -> Type -> Type -> Type
20+ sig e r e_in e_out = e r e_in (\v => e_out)
21+
22+namespace DepUpdateEffect
23+ sig : Effect -> (x : Type) -> Type -> (x -> Type) -> Type
24+ sig e r e_in e_out = e r e_in e_out
25+
26+
27+-- a single effect transition.
28+
29+data EffTrans : Type -> Type -> Type where
30+ (:=>) : a -> b -> EffTrans a b
31+
32+-- 'trans' gives a single effect transition. Again three versions, for
33+-- no transition, non-dependent transition and dependent transition, again
34+-- disambiguated by type, but the one with no update can be implicit.
35+
36+namespace NoUpdateTrans
37+ implicit
38+ trans : a -> EffTrans a (x -> a)
39+ trans t = t :=> (\v => t)
40+
41+namespace UpdateTrans
42+ trans : a -> b -> EffTrans a (x -> b)
43+ trans s t = s :=> (\v => t)
44+
45+namespace DepUpdateTrans
46+ trans : a -> b -> EffTrans a b
47+ trans s t = s :=> t
48+
49+Proto : (x : Type) ->
50+ List (EffTrans EFFECT (x -> EFFECT)) ->
51+ Type
52+Proto x xs = Eff x (proto_in xs) (\val : x => proto_out xs val)
53+ where
54+ proto_out : List (EffTrans EFFECT (x -> EFFECT)) -> x -> List EFFECT
55+ proto_out [] val = []
56+ proto_out ((e_in :=> e_out) :: xs) val
57+ = let rec = proto_out xs val in e_out val :: rec
58+
59+ proto_in : List (EffTrans EFFECT (x -> EFFECT)) -> List EFFECT
60+ proto_in [] = []
61+ proto_in ((e_in :=> e_out) :: xs)
62+ = let rec = proto_in xs in e_in :: rec
63+