@@ -1,63 +0,0 @@
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−