From 0d3d89988a6d6eff4080efac779174a9a54bff2c Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 20 Jan 2016 17:22:49 +0000 Subject: [PATCH] Fix remaining examples --- RLE/README | 2 +- ResDSL/FileDSL.idr | 38 ++++++++++++++++++++++++++------------ ResDSL/Resimp.idr | 44 +++++++++++++++++++++++--------------------- 3 files changed, 50 insertions(+), 34 deletions(-) diff --git a/RLE/README b/RLE/README index ac8459a..4f97cd7 100644 --- a/RLE/README +++ b/RLE/README @@ -1 +1 @@ -Run length encodin of lists or vects of characters +Run length encoding of lists or vects of characters diff --git a/ResDSL/FileDSL.idr b/ResDSL/FileDSL.idr index f5a89f5..eeb135a 100644 --- a/ResDSL/FileDSL.idr +++ b/ResDSL/FileDSL.idr @@ -11,41 +11,55 @@ pstring Writing = "w" data FILE : Purpose -> Type where OpenH : File -> FILE p -syntax ifM [test] then [t] else [e] +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 ())) +open fn p = ioc (do Right h <- fopen fn (pstring p) + | Left err => return (Left ()) + return (Right (OpenH h))) close : FILE p -> Updater () close (OpenH h) = iou (closeFile h) readLine : FILE Reading -> Reader String -readLine (OpenH h) = ior (fread h) +readLine (OpenH h) = ior (do Right str <- fGetLine h + | return "" + return str) eof : FILE Reading -> Reader Bool -eof (OpenH h) = ior (feof h) +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 rputStr [s] = Lift (putStr s) + +syntax "if" "opened" [f] "then" [e] "else" [t] = Check f t e + + + + + + + + + + + + + -syntax if opened [f] then [e] else [t] = Check f t e -------- readH : String -> RES () readH fn = res (do let x = open fn Reading if opened x then - do While (do e <- reof x - Return (not e)) - (do str <- rreadLine x - Lift (putStr str)) + do str <- rreadLine x + rputStr str rclose x else rputStrLn "Error") diff --git a/ResDSL/Resimp.idr b/ResDSL/Resimp.idr index 49b7190..c043e18 100644 --- a/ResDSL/Resimp.idr +++ b/ResDSL/Resimp.idr @@ -1,7 +1,7 @@ module Resimp +import public Data.Vect import public Data.Fin -import Data.Vect -- IO operations which read a resource data Reader : Type -> Type where @@ -49,35 +49,35 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty) interpTy (a :-> b) = a -> interpTy b data HasType : Vect n Ty -> Fin n -> Ty -> Type where - stop : HasType (a :: gam) FZ a - pop : HasType gam i b -> HasType (a :: gam) (FS i) b + Stop : HasType (a :: gam) FZ a + Pop : HasType gam i b -> HasType (a :: gam) (FS i) b data Env : Vect n Ty -> Type 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 + envLookup Stop (x :: xs) = x + envLookup (Pop k) (x :: xs) = envLookup k xs update : (gam : Vect n Ty) -> HasType gam i b -> Ty -> Vect n Ty - update (x :: xs) stop y = y :: xs - update (x :: xs) (pop k) y = x :: update xs k y - update Nil stop _ impossible + update (x :: xs) Stop y = y :: xs + update (x :: xs) (Pop k) y = x :: update xs k y + update Nil Stop _ impossible total 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 - envUpdate stop _ Nil impossible + envUpdate Stop val (x :: xs) = val :: xs + envUpdate (Pop k) val (x :: xs) = x :: envUpdate k val xs + envUpdate Stop _ Nil impossible total envUpdateVal : (p:HasType gam i a) -> (val:b) -> Env gam -> Env (update gam p (Val b)) - envUpdateVal stop val (x :: xs) = val :: xs - envUpdateVal (pop k) val (x :: xs) = x :: envUpdateVal k val xs - envUpdateVal stop _ Nil impossible + envUpdateVal Stop val (x :: xs) = val :: xs + envUpdateVal (Pop k) val (x :: xs) = x :: envUpdateVal k val xs + envUpdateVal Stop _ Nil impossible envTail : Env (a :: gam) -> Env gam envTail (x :: xs) = xs @@ -122,10 +122,7 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty) ioret : a -> IO a ioret = return - iolift : IO a -> Res gam gam (R a) - iolift = Lift - - interp : Env gam -> (e : Res gam gam' t) -> + interp : Env gam -> [static] (e : Res gam gam' t) -> (Env gam' -> interpTy t -> IO u) -> IO u interp env (Let val scope) k @@ -159,6 +156,11 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty) = interp env v (\env', v' => do n <- v' interp env' (f n) k) + let_ : _ -> Creator (interpTy a) -> + Res (a :: gam) (Val () :: gam') (R t) -> + Res gam gam' (R t) + let_ _ = Let + -- run : {static} Res [] [] (R t) -> IO t -- run prog = interp [] prog (\env, res => res) @@ -166,9 +168,9 @@ syntax run [prog] = interp [] prog (\env, res => res) dsl res variable = id - let = Let - index_first = stop - index_next = pop + let = let_ + index_first = Stop + index_next = Pop syntax RES [x] = {gam:Vect n Ty} -> Res gam gam (R x)