git.iko.soy/Idris-dev
on master help sign in
Allow reading files in executor
commit1f5ff741678c8e17a42e07a9d6e8cea0901984d5 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 5 Apr 2013, 15:08 (14 years ago) parent62be419
3 files changed+40−2
compare with master
unifiedsplit
rts/idris_stdfgn.c+24 rts/idris_stdfgn.h+1−1 src/Core/Execute.hs+15−1
rts/idris_stdfgn.c+24
@@ -25,6 +25,30 @@ int fileError(void* h) {
2525 return ferror(f);
2626}
2727
28+char* freadStr(void* h) {
29+ FILE* f = (FILE*)h;
30+ char* str;
31+ printf("foo");
32+ if (f != NULL) {
33+ fseek(f, 0L, SEEK_END);
34+ size_t size = ftell(f);
35+ rewind(f);
36+ printf("bar");
37+ str = malloc(size + sizeof(char));
38+ if (str != NULL && fread(str, size, 1, f)) {
39+ (*(str + size)) = '\0';
40+ printf("asf");
41+ } else {
42+ printf("Failed to allocate string from file\n");
43+ exit(1);
44+ }
45+ } else {
46+ str = malloc(sizeof(char));
47+ str[0] = '\0';
48+ }
49+ return str;
50+}
51+
2852void fputStr(void* h, char* str) {
2953 FILE* f = (FILE*)h;
3054 fputs(str, f);
rts/idris_stdfgn.h+1−1
@@ -8,7 +8,7 @@ void putStr(char* str);
88
99void* fileOpen(char* f, char* mode);
1010void fileClose(void* h);
11−//char* freadStr(void* h);
11+char* freadStr(void* h);
1212void fputStr(void*h, char* str);
1313
1414int isNull(void* ptr);
src/Core/Execute.hs+15−1
@@ -98,7 +98,8 @@ doExec env ctxt Impossible = fail "Tried to execute an impossible case"
9898doExec env ctxt (TType u) = return (TType u)
9999
100100execApp :: Env -> Context -> (Term, [Term]) -> Idris Term
101−execApp env ctxt (f, args) = do newF <- doExec env ctxt f
101+execApp env ctxt (f, args) = trace ("Reducing " ++ show f) $
102+ do newF <- doExec env ctxt f
102103 newArgs <- mapM (doExec env ctxt) args
103104 execApp' env ctxt newF newArgs
104105
@@ -117,6 +118,19 @@ execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
117118execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
118119 return $ Constant (Str (s1 ++ s2))
119120
121+execApp' env ctxt (P _ (UN "prim__eqInt") _) [(Constant (I i1)), (Constant (I i2))] =
122+ return $ if i1 == i2 then Constant (I 1) else Constant (I 0)
123+
124+execApp' env ctxt (P _ (UN "prim__readString") _) [ptr] | Just p <- unPtr ptr =
125+ do fn <- findForeign "freadStr"
126+ case fn of
127+ Just (Fun _ freadStr) -> do
128+ res <- lift $ callFFI freadStr retCString [argPtr p]
129+ str <- lift $ peekCString res
130+ trace ("Found " ++ str) $ return ()
131+ return $ Constant (Str str)
132+ Nothing -> fail "Could not load freadStr"
133+
120134execApp' env ctxt f@(P _ n _) args =
121135 do let val = lookupDef Nothing n ctxt
122136 case val of