Fix remaining examples

RLE/README

@@ -1 +1 @@
-Run length encodin of lists or vects of characters
+Run length encoding of lists or vects of characters

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")
 

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,16 +156,21 @@ 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)
 
 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)