Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

New notation

  • Loading branch information...
commit 64e33f66546f998131c043ad5eb133c727bf9b7a 1 parent a3a340a
Edwin Brady authored
Showing with 209 additions and 0 deletions.
  1. +49 −0 resfilenew.idr
  2. +160 −0 resimpnew.idr
49 resfilenew.idr
View
@@ -0,0 +1,49 @@
+module main
+
+import resimpnew
+
+data Purpose = Reading | Writing
+
+pstring : Purpose -> String
+pstring Reading = "r"
+pstring Writing = "w"
+
+data FILE : Purpose -> Set where
+ OpenH : File -> FILE p
+
+syntax ifM [test] then [t] else [e]
+ = test >>= (\b => if b then t else e)
+
+open : String -> (p:Purpose) -> Creator (Either () (FILE p))
+open fn p = ioc (do h <- fopen fn (pstring p)
+ ifM (validFile h) then (return (Right (OpenH h)))
+ else (return (Left ())))
+
+close : FILE p -> Updater ()
+close (OpenH h) = iou (closeFile h)
+
+readLine : FILE Reading -> Reader String
+readLine (OpenH h) = ior (fread h)
+
+eof : FILE Reading -> Reader Bool
+eof (OpenH h) = ior (feof h)
+
+syntax rclose [h] = Update close h
+syntax rreadLine [h] = Use readLine h
+syntax reof [h] = Use eof h
+
+syntax rputStrLn [s] = Lift (putStrLn s)
+
+syntax if opened [f] then [t] else [e] = Check f t e
+
+readH : String -> RES ()
+readH fn = res (do let x = open fn Reading
+ if opened x
+ then rputStrLn "Error"
+ else do str <- rreadLine stop
+ rputStrLn str
+ rclose stop)
+
+main : IO ()
+main = run (readH "Test")
+
160 resimpnew.idr
View
@@ -0,0 +1,160 @@
+module resimp
+
+-- IO operations which read a resource
+data Reader : Set -> Set where
+ MkReader : IO a -> Reader a
+
+getReader : Reader a -> IO a
+getReader (MkReader x) = x
+
+ior : IO a -> Reader a
+ior = MkReader
+
+-- IO operations which update a resource
+data Updater : Set -> Set where
+ MkUpdater : IO a -> Updater a
+
+getUpdater : Updater a -> IO a
+getUpdater (MkUpdater x) = x
+
+iou : IO a -> Updater a
+iou = MkUpdater
+
+-- IO operations which create a resource
+data Creator : Set -> Set where
+ MkCreator : IO a -> Creator a
+
+getCreator : Creator a -> IO a
+getCreator (MkCreator x) = x
+
+ioc : IO a -> Creator a
+ioc = MkCreator
+
+infixr 5 :->
+
+using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)
+
+ data Ty = R Set
+ | Val Set
+ | Choice Set Set
+ | (:->) Set Ty
+
+ interpTy : Ty -> Set
+ interpTy (R t) = IO t
+ interpTy (Val t) = t
+ interpTy (Choice x y) = Either x y
+ interpTy (a :-> b) = a -> interpTy b
+
+ data HasType : Vect Ty n -> Fin n -> Ty -> Set where
+ stop : HasType (a :: gam) fO a
+ pop : HasType gam i b -> HasType (a :: gam) (fS i) b
+
+ data Env : Vect Ty n -> Set where
+ Nil : Env Nil
+ (::) : interpTy a -> Env gam -> Env (a :: gam)
+
+ envLookup : HasType gam i a -> Env gam -> interpTy a
+ envLookup stop (x :: xs) = x
+ envLookup (pop k) (x :: xs) = envLookup k xs
+
+ update : (gam : Vect Ty n) -> HasType gam i b -> Ty -> Vect Ty n
+ update (x :: xs) stop y = y :: xs
+ update (x :: xs) (pop k) y = x :: update xs k y
+
+ envUpdate : (p:HasType gam i a) -> (val:interpTy b) ->
+ Env gam -> Env (update gam p b)
+ envUpdate stop val (x :: xs) = val :: xs
+ envUpdate (pop k) val (x :: xs) = x :: envUpdate k val xs
+
+ envTail : Env (a :: gam) -> Env gam
+ envTail (x :: xs) = xs
+
+ data Args : Vect Ty n -> List Set -> Set where
+ ANil : Args gam []
+ ACons : HasType gam i a ->
+ Args gam as -> Args gam (interpTy a :: as)
+
+ funTy : List Set -> Ty -> Ty
+ funTy list.Nil t = t
+ funTy (a :: as) t = a :-> funTy as t
+
+-- applyArgs : {as : List Set} ->
+-- Env gam -> interpTy (funTy as t) -> Args gam as -> interpTy t
+-- -- applyArgs env f ANil = f
+-- applyArgs env f (ACons x xs) = ?appArgs --applyArgs env (f (envLookup x env)) xs
+
+ data Res : Vect Ty n -> Vect Ty n -> Ty -> Set where
+
+{-- Resource creation and usage. 'Let' creates a resource - the type
+ at the end means that the resource must have been consumed by the time
+ it goes out of scope, where "consumed" simply means that it has been
+ replaced with a value of type '()'. --}
+
+ Let : Creator (interpTy a) ->
+ Res (a :: gam) (Val () :: gam') (R t) ->
+ Res gam gam' (R t)
+ Update : (a -> Updater b) -> (p:HasType gam i (Val a)) ->
+ Res gam (update gam p (Val b)) (R ())
+ Use : (a -> Reader b) -> HasType gam i (Val a) ->
+ Res gam gam (R b)
+
+{-- Control structures --}
+
+ Lift : IO a -> Res gam gam (R a)
+ Check : (p:HasType gam i (Choice (interpTy a) (interpTy b))) ->
+ (failure:Res (update gam p a) (update gam p c) T) ->
+ (success:Res (update gam p b) (update gam p c) T) ->
+ Res gam (update gam p c) T
+ While : Res gam gam (R Bool) ->
+ Res gam gam (R ()) -> Res gam gam (R ())
+ Return : a -> Res gam gam (R a)
+ (>>=) : Res gam gam' (R a) -> (a -> Res gam' gam'' (R t)) ->
+ Res gam gam'' (R t)
+
+
+ interp : Env gam -> Res gam gam' t ->
+ (Env gam' -> interpTy t -> IO u) -> IO u
+
+ interp env (Let val scope) k
+ = do x <- getCreator val;
+ interp (x :: env) scope
+ (\env', scope' => k (envTail env') scope')
+ interp env (Update method x) k
+ = do x' <- getUpdater (method (envLookup x env))
+ k (envUpdate x x' env) (return ())
+ interp env (Use method x) k
+ = do x' <- getReader (method (envLookup x env))
+ k env (return x')
+ interp env (Lift io) k
+ = k env io
+ interp env (Check x left right) k =
+ either (envLookup x env)
+ (\a => interp (envUpdate x a env) left k)
+ (\b => interp (envUpdate x b env) right k)
+ interp env (While test body) k
+ = interp env test
+ (\env', result =>
+ do r <- result;
+ if (not r)
+ then (k env' (return ()))
+ else (interp env' body
+ (\env'', body' =>
+ do v <- body' -- make sure it's evalled
+ interp env'' (While test body) k ))
+ )
+ interp env (Return v) k = k env (return v)
+ interp env (v >>= f) k
+ = interp env v (\env', v' => do n <- v'
+ interp env' (f n) k)
+
+ run : Res [] [] (R t) -> IO t
+ run prog = interp [] prog (\env, res => res)
+
+dsl res
+ variable = id
+ let = Let
+ index_first = stop
+ index_next = pop
+
+syntax RES [x] = {gam:Vect Ty n} -> Res gam gam (R x)
+
Please sign in to comment.
Something went wrong with that request. Please try again.