git.iko.soy/Idris-dev
on master help sign in
Allow reading files in executor
1f5ff74David Christiansen
rts/idris_stdfgn.c+24
compare with master
unifiedsplit
@@ -25,6 +25,30 @@ int fileError(void* h) {
25 return ferror(f);
25 return ferror(f);
26}
26}
27
27
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+
28void fputStr(void* h, char* str) {
52void fputStr(void* h, char* str) {
29 FILE* f = (FILE*)h;
53 FILE* f = (FILE*)h;
30 fputs(str, f);
54 fputs(str, f);
rts/idris_stdfgn.h+1−1
@@ -8,7 +8,7 @@ void putStr(char* str);
8
8
9void* fileOpen(char* f, char* mode);
9void* fileOpen(char* f, char* mode);
10void fileClose(void* h);
10void fileClose(void* h);
11−//char* freadStr(void* h);
11+char* freadStr(void* h);
12void fputStr(void*h, char* str);
12void fputStr(void*h, char* str);
13
13
14int isNull(void* ptr);
14int isNull(void* ptr);
src/Core/Execute.hs+15−1
@@ -98,7 +98,8 @@ doExec env ctxt Impossible = fail "Tried to execute an impossible case"
98doExec env ctxt (TType u) = return (TType u)
98doExec env ctxt (TType u) = return (TType u)
99
99
100execApp :: Env -> Context -> (Term, [Term]) -> Idris Term
100execApp :: Env -> Context -> (Term, [Term]) -> Idris Term
101+execApp env ctxt (f, args) = trace ("Reducing " ++ show f) $
101−execApp env ctxt (f, args) = do newF <- doExec env ctxt f
102+ do newF <- doExec env ctxt f
102 newArgs <- mapM (doExec env ctxt) args
103 newArgs <- mapM (doExec env ctxt) args
103 execApp' env ctxt newF newArgs
104 execApp' env ctxt newF newArgs
104
105
@@ -117,6 +118,19 @@ execApp' env ctxt (P _ (UN "prim__readString") _) [P _ (UN "prim__stdin") _] =
117execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
118execApp' env ctxt (P _ (UN "prim__concat") _) [(Constant (Str s1)), (Constant (Str s2))] =
118 return $ Constant (Str (s1 ++ s2))
119 return $ Constant (Str (s1 ++ s2))
119
120
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+
120execApp' env ctxt f@(P _ n _) args =
134execApp' env ctxt f@(P _ n _) args =
121 do let val = lookupDef Nothing n ctxt
135 do let val = lookupDef Nothing n ctxt
122 case val of
136 case val of