@@ -0,0 +1,156 @@
1+module resimp
2+
3+-- IO operations which read a resource
4+data Reader : Set -> Set where
5+ MkReader : IO a -> Reader a
6+
7+getReader : Reader a -> IO a
8+getReader (MkReader x) = x
9+
10+ior : IO a -> Reader a
11+ior = MkReader
12+
13+-- IO operations which update a resource
14+data Updater : Set -> Set where
15+ MkUpdater : IO a -> Updater a
16+
17+getUpdater : Updater a -> IO a
18+getUpdater (MkUpdater x) = x
19+
20+iou : IO a -> Updater a
21+iou = MkUpdater
22+
23+-- IO operations which create a resource
24+data Creator : Set -> Set where
25+ MkCreator : IO a -> Creator a
26+
27+getCreator : Creator a -> IO a
28+getCreator (MkCreator x) = x
29+
30+ioc : IO a -> Creator a
31+ioc = MkCreator
32+
33+infixr 5 :->
34+
35+using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)
36+
37+ data Ty = R Set
38+ | Val Set
39+ | Choice Set Set
40+ | (:->) Set Ty
41+
42+ interpTy : Ty -> Set
43+ interpTy (R t) = IO t
44+ interpTy (Val t) = t
45+ interpTy (Choice x y) = Either x y
46+ interpTy (a :-> b) = a -> interpTy b
47+
48+ data HasType : Vect Ty n -> Fin n -> Ty -> Set where
49+ stop : HasType (a :: gam) fO a
50+ pop : HasType gam i b -> HasType (a :: gam) (fS i) b
51+
52+ data Env : Vect Ty n -> Set where
53+ Nil : Env Nil
54+ (::) : interpTy a -> Env gam -> Env (a :: gam)
55+
56+ envLookup : HasType gam i a -> Env gam -> interpTy a
57+ envLookup stop (x :: xs) = x
58+ envLookup (pop k) (x :: xs) = envLookup k xs
59+
60+ update : (gam : Vect Ty n) -> HasType gam i b -> Ty -> Vect Ty n
61+ update (x :: xs) stop y = y :: xs
62+ update (x :: xs) (pop k) y = x :: update xs k y
63+
64+ envUpdate : (p:HasType gam i a) -> (val:interpTy b) ->
65+ Env gam -> Env (update gam p b)
66+ envUpdate stop val (x :: xs) = val :: xs
67+ envUpdate (pop k) val (x :: xs) = x :: envUpdate k val xs
68+
69+ envTail : Env (a :: gam) -> Env gam
70+ envTail (x :: xs) = xs
71+
72+ data Args : Vect Ty n -> List Set -> Set where
73+ ANil : Args gam []
74+ ACons : HasType gam i a ->
75+ Args gam as -> Args gam (interpTy a :: as)
76+
77+ funTy : List Set -> Ty -> Ty
78+ funTy list.Nil t = t
79+ funTy (a :: as) t = a :-> funTy as t
80+
81+ data Res : Vect Ty n -> Vect Ty n -> Ty -> Set where
82+
83+{-- Resource creation and usage. 'Let' creates a resource - the type
84+ at the end means that the resource must have been consumed by the time
85+ it goes out of scope, where "consumed" simply means that it has been
86+ replaced with a value of type '()'. --}
87+
88+ Let : Creator (interpTy a) ->
89+ Res (a :: gam) (Val () :: gam') (R t) ->
90+ Res gam gam' (R t)
91+ Update : (a -> Updater b) -> (p:HasType gam i (Val a)) ->
92+ Res gam (update gam p (Val b)) (R ())
93+ Use : (a -> Reader b) -> HasType gam i (Val a) ->
94+ Res gam gam (R b)
95+
96+{-- Control structures --}
97+
98+ Lift : IO a -> Res gam gam (R a)
99+ Check : (p:HasType gam i (Choice (interpTy a) (interpTy b))) ->
100+ (failure:Res (update gam p a) (update gam p c) T) ->
101+ (success:Res (update gam p b) (update gam p c) T) ->
102+ Res gam (update gam p c) T
103+ While : Res gam gam (R Bool) ->
104+ Res gam gam (R ()) -> Res gam gam (R ())
105+ Return : a -> Res gam gam (R a)
106+ (>>=) : Res gam gam' (R a) -> (a -> Res gam' gam'' (R t)) ->
107+ Res gam gam'' (R t)
108+
109+
110+ interp : Env gam -> {static} Res gam gam' t ->
111+ (Env gam' -> interpTy t -> IO u) -> IO u
112+
113+ interp env (Let val scope) k
114+ = do x <- getCreator val
115+ interp (x :: env) scope
116+ (\env', scope' => k (envTail env') scope')
117+ interp env (Update method x) k
118+ = do x' <- getUpdater (method (envLookup x env))
119+ k (envUpdate x x' env) (return ())
120+ interp env (Use method x) k
121+ = do x' <- getReader (method (envLookup x env))
122+ k env (return x')
123+ interp env (Lift io) k
124+ = k env io
125+ interp env (Check x left right) k =
126+ either (envLookup x env)
127+ (\a => interp (envUpdate x a env) left k)
128+ (\b => interp (envUpdate x b env) right k)
129+ interp env (While test body) k
130+ = interp env test
131+ (\env', result =>
132+ do r <- result
133+ if (not r)
134+ then (k env' (return ()))
135+ else (interp env' body
136+ (\env'', body' =>
137+ do v <- body' -- make sure it's evalled
138+ interp env'' (While test body) k )))
139+ interp env (Return v) k = k env (return v)
140+ interp env (v >>= f) k
141+ = interp env v (\env', v' => do n <- v'
142+ interp env' (f n) k)
143+
144+-- run : {static} Res [] [] (R t) -> IO t
145+-- run prog = interp [] prog (\env, res => res)
146+
147+syntax run [prog] = interp [] prog (\env, res => res)
148+
149+dsl res
150+ variable = id
151+ let = Let
152+ index_first = stop
153+ index_next = pop
154+
155+syntax RES [x] = {gam:Vect Ty n} -> Res gam gam (R x)
156+