@@ -0,0 +1,156 @@
3+-- IO operations which read a resource
4+data Reader : Set -> Set where
5+ MkReader : IO a -> Reader a
7+getReader : Reader a -> IO a
8+getReader (MkReader x) = x
10+ior : IO a -> Reader a
13+-- IO operations which update a resource
14+data Updater : Set -> Set where
15+ MkUpdater : IO a -> Updater a
17+getUpdater : Updater a -> IO a
18+getUpdater (MkUpdater x) = x
20+iou : IO a -> Updater a
23+-- IO operations which create a resource
24+data Creator : Set -> Set where
25+ MkCreator : IO a -> Creator a
27+getCreator : Creator a -> IO a
28+getCreator (MkCreator x) = x
30+ioc : IO a -> Creator a
35+using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)
43+ interpTy (R t) = IO t
45+ interpTy (Choice x y) = Either x y
46+ interpTy (a :-> b) = a -> interpTy b
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
52+ data Env : Vect Ty n -> Set where
54+ (::) : interpTy a -> Env gam -> Env (a :: gam)
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
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
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
69+ envTail : Env (a :: gam) -> Env gam
70+ envTail (x :: xs) = xs
72+ data Args : Vect Ty n -> List Set -> Set where
74+ ACons : HasType gam i a ->
75+ Args gam as -> Args gam (interpTy a :: as)
77+ funTy : List Set -> Ty -> Ty
79+ funTy (a :: as) t = a :-> funTy as t
81+ data Res : Vect Ty n -> Vect Ty n -> Ty -> Set where
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 '()'. --}
88+ Let : Creator (interpTy a) ->
89+ Res (a :: gam) (Val () :: 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) ->
96+{-- Control structures --}
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)) ->
110+ interp : Env gam -> {static} Res gam gam' t ->
111+ (Env gam' -> interpTy t -> IO u) -> IO u
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))
123+ interp env (Lift io) k
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
134+ then (k env' (return ()))
135+ else (interp 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)
144+-- run : {static} Res [] [] (R t) -> IO t
145+-- run prog = interp [] prog (\env, res => res)
147+syntax run [prog] = interp [] prog (\env, res => res)
155+syntax RES [x] = {gam:Vect Ty n} -> Res gam gam (R x)