53de817 · Idris-dev · git.iko.soy

Makefile+1−1

compare with master

unifiedsplit

@@ -19,7 +19,7 @@ relib: .PHONY

19 make -C lib IDRIS=../dist/build/idris/idris

20

21linecount : .PHONY

22− wc -l src/Idris/*.hs src/Core/*.hs src/RTS/*.hs

22+ wc -l src/Idris/*.hs src/Core/*.hs src/IRTS/*.hs

23

24.PHONY:

25

idris.cabal+2−1

@@ -40,7 +40,8 @@ Description: Idris is a general purpose language with full dependent types.

40Cabal-Version: >= 1.6

41Build-type: Custom

42

43−Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_main.c

43+Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h

44+ rts/idris_stdfgn.h rts/idris_main.c rts/idris_gmp.h

44Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr

45Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr

45 lib/control/monad/*.idr lib/language/*.idr

46 lib/control/monad/*.idr lib/language/*.idr

46 tutorial/examples/*.idr

47 tutorial/examples/*.idr

rts/Makefile+2−2

@@ -1,5 +1,5 @@

1−OBJS = idris_rts.o idris_gc.o idris_gmp.o

1+OBJS = idris_rts.o idris_gc.o idris_gmp.o idris_stdfgn.o

2−HDRS = idris_rts.h idris_gc.h idris_gmp.h

2+HDRS = idris_rts.h idris_gc.h idris_gmp.h idris_stdfgn.h

3CFLAGS = -g

4

5LIBTARGET = libidris_rts.a

rts/idris_gmp.c+1−1

@@ -196,7 +196,7 @@ VAL idris_bigLt(VM* vm, VAL x, VAL y) {

196

197VAL idris_bigLe(VM* vm, VAL x, VAL y) {

198 if (ISINT(x) && ISINT(y)) {

199− return MKINT((i_int)GETINT(x) <= GETINT(y));

199+ return MKINT((i_int)(GETINT(x) <= GETINT(y)));

200 } else {

201 return bigLe(vm, x, y);

202 }

rts/idris_rts.c+13−15

@@ -50,36 +50,35 @@ void* allocate(VM* vm, size_t size) {

50}

51

52void* allocCon(VM* vm, int arity) {

53− Closure* cl = allocate(vm, sizeof(ClosureType) +

53+ Closure* cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*arity);

54− sizeof(con) + sizeof(VAL)*arity);

55 cl -> ty = CON;

54 cl -> ty = CON;

56 if (arity == 0) {

55 if (arity == 0) {

57 cl -> info.c.args = NULL;

56 cl -> info.c.args = NULL;

58 } else {

57 } else {

59− cl -> info.c.args = (void*)((char*)cl + sizeof(ClosureType)

58+ cl -> info.c.args = (void*)((char*)cl + sizeof(Closure));

60− + sizeof(con));

61 }

59 }

62 return (void*)cl;

60 return (void*)cl;

63}

61}

64

62

65VAL MKFLOAT(VM* vm, double val) {

63VAL MKFLOAT(VM* vm, double val) {

66− Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(double));

64+ Closure* cl = allocate(vm, sizeof(Closure));

67 cl -> ty = FLOAT;

65 cl -> ty = FLOAT;

68 cl -> info.f = val;

66 cl -> info.f = val;

69 return cl;

67 return cl;

70}

68}

71

69

72VAL MKSTR(VM* vm, char* str) {

70VAL MKSTR(VM* vm, char* str) {

73− Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(char*) +

71+ Closure* cl = allocate(vm, sizeof(Closure) + // Type) + sizeof(char*) +

74 sizeof(char)*strlen(str)+1);

72 sizeof(char)*strlen(str)+1);

75 cl -> ty = STRING;

73 cl -> ty = STRING;

76− cl -> info.str = (char*)cl + sizeof(ClosureType) + sizeof(char*);

74+ cl -> info.str = (char*)cl + sizeof(Closure);

75+

77 strcpy(cl -> info.str, str);

76 strcpy(cl -> info.str, str);

78 return cl;

77 return cl;

79}

78}

80

79

81VAL MKPTR(VM* vm, void* ptr) {

80VAL MKPTR(VM* vm, void* ptr) {

82− Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));

81+ Closure* cl = allocate(vm, sizeof(Closure));

83 cl -> ty = PTR;

82 cl -> ty = PTR;

84 cl -> info.ptr = ptr;

83 cl -> info.ptr = ptr;

85 return cl;

84 return cl;

@@ -138,9 +137,9 @@ void dumpVal(VAL v) {

138}

137}

139

138

140VAL idris_castIntStr(VM* vm, VAL i) {

139VAL idris_castIntStr(VM* vm, VAL i) {

141− Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(char*) + sizeof(char)*16);

140+ Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16);

142 cl -> ty = STRING;

141 cl -> ty = STRING;

143− cl -> info.str = (char*)cl + sizeof(ClosureType) + sizeof(char*);

142+ cl -> info.str = (char*)cl + sizeof(Closure);

144 sprintf(cl -> info.str, "%ld", GETINT(i));

143 sprintf(cl -> info.str, "%ld", GETINT(i));

145 return cl;

144 return cl;

146}

145}

@@ -152,9 +151,9 @@ VAL idris_castStrInt(VM* vm, VAL i) {

152}

151}

153

152

154VAL idris_castFloatStr(VM* vm, VAL i) {

153VAL idris_castFloatStr(VM* vm, VAL i) {

155− Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(char*) + sizeof(char)*32);

154+ Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*32);

156 cl -> ty = STRING;

155 cl -> ty = STRING;

157− cl -> info.str = (char*)cl + sizeof(ClosureType) + sizeof(char*);

156+ cl -> info.str = (char*)cl + sizeof(Closure);

158 sprintf(cl -> info.str, "%g", GETFLOAT(i));

157 sprintf(cl -> info.str, "%g", GETFLOAT(i));

159 return cl;

158 return cl;

160}

159}

@@ -166,10 +165,9 @@ VAL idris_castStrFloat(VM* vm, VAL i) {

166VAL idris_concat(VM* vm, VAL l, VAL r) {

165VAL idris_concat(VM* vm, VAL l, VAL r) {

167 char *ls = GETSTR(l);

166 char *ls = GETSTR(l);

168 char *rs = GETSTR(r);

167 char *rs = GETSTR(r);

169− Closure* cl = allocate(vm, sizeof(ClosureType) + sizeof(char*) +

168+ Closure* cl = allocate(vm, sizeof(Closure) + strlen(ls) + strlen(rs) + 1);

170− strlen(ls) + strlen(rs) + 1);

171 cl -> ty = STRING;

169 cl -> ty = STRING;

172− cl -> info.str = (char*)cl + sizeof(ClosureType) + sizeof(char*);

170+ cl -> info.str = (char*)cl + sizeof(Closure);

173 strcpy(cl -> info.str, ls);

171 strcpy(cl -> info.str, ls);

174 strcat(cl -> info.str, rs);

172 strcat(cl -> info.str, rs);

175 return cl;

173 return cl;

rts/idris_stdfgn.cnew file+30

@@ -0,0 +1,30 @@

1+#include "idris_stdfgn.h"

2+#include "idris_rts.h"

3+

4+void putStr(char* str) {

5+ printf("%s", str);

6+}

7+

8+void* fileOpen(char* name, char* mode) {

9+ FILE* f = fopen(name, mode);

10+ return (void*)f;

11+}

12+

13+void fileClose(void* h) {

14+ FILE* f = (FILE*)h;

15+ fclose(f);

16+}

17+

18+void fputStr(void* h, char* str) {

19+ FILE* f = (FILE*)h;

20+ fputs(str, f);

21+}

22+

23+int isNull(void* ptr) {

24+ return ptr==NULL;

25+}

26+

27+void* idris_stdin() {

28+ return (void*)stdin;

29+}

30+

rts/idris_stdfgn.hnew file+17

@@ -0,0 +1,17 @@

1+#ifndef _IDRISSTDFGN_H

2+#define _IDRISSTDFGN_H

3+

4+// A collection of useful standard functions to be used by the prelude.

5+

6+void putStr(char* str);

7+//char* readStr();

8+

9+void* fileOpen(char* f, char* mode);

10+void fileClose(void* h);

11+//char* freadStr(void* h);

12+void fputStr(void*h, char* str);

13+

14+int isNull(void* ptr);

15+void* idris_stdin();

16+

17+#endif

src/IRTS/CodegenC.hs+5−3

@@ -49,7 +49,7 @@ codegenC defs out exec incs libs dbg

49 when (exit /= ExitSuccess) $

50 putStrLn ("FAILURE: " ++ gcc)

51

52−headers [] = "#include <idris_rts.h>\n\n"

52+headers [] = "#include <idris_rts.h>\n#include <idris_stdfgn.h>\n"

53headers (x : xs) = "#include <" ++ x ++ ">\n" ++ headers xs

54

55debug TRACE = "#define IDRIS_TRACE\n\n"

@@ -137,13 +137,15 @@ bcc i (FOREIGNCALL l LANG_C rty fn args)

137-- bcc i _ = indent i ++ "// not done yet\n"

138

139c_irts FInt x = "MKINT((i_int)(" ++ x ++ ")"

140+c_irts FChar x = "MKINT((i_int)(" ++ x ++ ")"

140c_irts FString x = "MKSTR(" ++ x ++ ")"

141c_irts FString x = "MKSTR(" ++ x ++ ")"

141c_irts FUnit x = "MKINT(42424242)"

142c_irts FUnit x = "MKINT(42424242)"

142−c_irts FPtr x = "MKPTR(" ++ x ++ ")"

143+c_irts FPtr x = "MKPTR(vm, " ++ x ++ ")"

143c_irts FDouble x = "MKFLOAT(vm, " ++ x ++ ")"

144c_irts FDouble x = "MKFLOAT(vm, " ++ x ++ ")"

144c_irts FAny x = x

145c_irts FAny x = x

145

146

146irts_c FInt x = "GETINT(" ++ x ++ ")"

147irts_c FInt x = "GETINT(" ++ x ++ ")"

148+irts_c FChar x = "GETINT(" ++ x ++ ")"

147irts_c FString x = "GETSTR(" ++ x ++ ")"

149irts_c FString x = "GETSTR(" ++ x ++ ")"

148irts_c FUnit x = x

150irts_c FUnit x = x

149irts_c FPtr x = "GETPTR(" ++ x ++ ")"

151irts_c FPtr x = "GETPTR(" ++ x ++ ")"

@@ -196,7 +198,7 @@ doOp LBigStr [x] = "idris_castBigStr(vm, " ++ creg x ++ ")"

196doOp LFloatStr [x] = "idris_castFloatStr(vm, " ++ creg x ++ ")"

198doOp LFloatStr [x] = "idris_castFloatStr(vm, " ++ creg x ++ ")"

197doOp LStrFloat [x] = "idris_castStrFloat(vm, " ++ creg x ++ ")"

199doOp LStrFloat [x] = "idris_castStrFloat(vm, " ++ creg x ++ ")"

198

200

199−doOp LReadStr [] = "idris_readStr(vm, stdin)"

201+doOp LReadStr [x] = "idris_readStr(vm, GETPTR(" ++ creg x ++ "))"

200doOp LPrintNum [x] = creg x ++ "; printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"

202doOp LPrintNum [x] = creg x ++ "; printf(\"%ld\\n\", GETINT(" ++ creg x ++ "))"

201doOp LPrintStr [x] = creg x ++ "; fputs(GETSTR(" ++ creg x ++ "), stdout)"

203doOp LPrintStr [x] = creg x ++ "; fputs(GETSTR(" ++ creg x ++ "), stdout)"

202

204

src/IRTS/LParser.hs+2−1

@@ -204,7 +204,8 @@ pPrim = do reserved "StrEq"; lchar '(';

204 return (LOp LStrLt [e, e'])

205 <|> do reserved "StrLen"; lchar '('; e <- pLExp; lchar ')';

206 return (LOp LStrLen [e])

207+ <|> do reserved "ReadString"; lchar '('; e <- pLExp; lchar ')';

207− <|> do reserved "ReadString"; return (LOp LReadStr [])

208+ return (LOp LReadStr [e])

208 <|> do reserved "WriteString"; lchar '(';

209 <|> do reserved "WriteString"; lchar '(';

209 e <- pLExp; lchar ')'

210 e <- pLExp; lchar ')'

210 return (LOp LPrintStr [e])

211 return (LOp LPrintStr [e])

src/IRTS/Lang.hs+1−1

@@ -38,7 +38,7 @@ data PrimFn = LPlus | LMinus | LTimes | LDiv | LEq | LLt | LLe | LGt | LGe

38data FLang = LANG_C

39 deriving Show

40

42 deriving Show

43

44data LAlt = LConCase Int Name [Name] LExp