Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Minor tweaks

  • Loading branch information...
commit bcefa05ba7b496fcaee990dd5685ddaa3a9ecd27 1 parent 77da2a7
Edwin Brady authored
Showing with 17 additions and 10 deletions.
  1. +9 −8 resfile.idr
  2. +8 −2 resimp.idr
View
17 resfile.idr
@@ -29,24 +29,25 @@ syntax reof h = Use eof h;
syntax rputStrLn s = Lift (putStrLn s);
-readH : RESFN (FILE Reading :-> R ());
-readH = res (\h => Fn (While (do { end <- reof h;
- return (not end); })
- (do { str <- rreadLine h;
- rputStrLn str; }) ));
+readH : String -> RESFN (FILE Reading :-> R ());
+readH intro = resfn (\h => Fn (res
+ (While (do { end <- reof h;
+ return (not end); })
+ (do { str <- rreadLine h;
+ rputStrLn (intro ++ str); }) )));
-syntax rreadH h = Call readH (ACons h ANil);
+syntax rreadH i h = Call (readH i) (ACons h ANil);
testprog : String -> RES ();
testprog filename
= res do { let h = open filename Reading;
Check h
(rputStrLn "File open error")
- (do { rreadH h;
+ (do { rreadH "Line: " h;
rclose h;
rputStrLn "DONE"; });
};
main : IO ();
main = do { x <- run (testprog "Test");
- return x; };
+ return x; };
View
10 resimp.idr
@@ -91,7 +91,7 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n) {
replaced with a value of type '()'. --}
Let : Creator (interpTy a) ->
- Res (a :: gam) (Val () :: gam') (R t) -> Res gam gam' (R t)
+ 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) ->
@@ -182,7 +182,13 @@ dsl res {
let = Let
index_first = stop
index_next = pop
- outer_lambda = Lam
+}
+
+dsl resfn {
+ lambda = Lam
+ variable = id
+ 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.