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

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:edwinb/Idris-dev

Conflicts: rts/idris_rts.c

commit53de8179a1e7515856f68c4bf5573fa297746fe3 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 6 Sep 2012, 17:49 (14 years ago) parent7ab5216 0433650

10 files changed+74−25

compare with master

unifiedsplit

Makefile+1−1 idris.cabal+2−1 rts/Makefile+2−2 rts/idris_gmp.c+1−1 rts/idris_rts.c+13−15 rts/idris_stdfgn.c+30 rts/idris_stdfgn.h+17 src/IRTS/CodegenC.hs+5−3 src/IRTS/LParser.hs+2−1 src/IRTS/Lang.hs+1−1

Makefile+1−1

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

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

2020

2121linecount : .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

2323

2424.PHONY:

2525

idris.cabal+2−1

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

4040Cabal-Version: >= 1.6

4141Build-type: Custom

4242

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

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

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

4647 tutorial/examples/*.idr

rts/Makefile+2−2

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

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

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

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 idris_stdfgn.h

33CFLAGS = -g

55LIBTARGET = libidris_rts.a

rts/idris_gmp.c+1−1

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

196196

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

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

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

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

200200 } else {

201201 return bigLe(vm, x, y);

202202 }

rts/idris_rts.c+13−15

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

5050}

5151

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

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

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

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

5554 cl -> ty = CON;

5655 if (arity == 0) {

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

5857 } else {

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

60− + sizeof(con));

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

6159 }

6260 return (void*)cl;

6361}

6462

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

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

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

6765 cl -> ty = FLOAT;

6866 cl -> info.f = val;

6967 return cl;

7068}

7169

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

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

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

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

7573 cl -> ty = STRING;

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

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

75+

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

7877 return cl;

7978}

8079

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

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

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

8382 cl -> ty = PTR;

8483 cl -> info.ptr = ptr;

8584 return cl;

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

138137}

139138

140139VAL 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);

142141 cl -> ty = STRING;

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

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

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

145144 return cl;

146145}

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

152151}

153152

154153VAL 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);

156155 cl -> ty = STRING;

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

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

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

159158 return cl;

160159}

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

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

167166 char *ls = GETSTR(l);

168167 char *rs = GETSTR(r);

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

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

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

171169 cl -> ty = STRING;

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

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

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

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

175173 return cl;

rts/idris_stdfgn.cnew file+30

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

1+#include "idris_stdfgn.h"

2+#include "idris_rts.h"

4+void putStr(char* str) {

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

6+}

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

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

6+void putStr(char* str);

7+//char* readStr();

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

4949 when (exit /= ExitSuccess) $

5050 putStrLn ("FAILURE: " ++ gcc)

5151

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

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

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

5454

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

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

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

138138

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

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

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

141142c_irts FUnit x = "MKINT(42424242)"

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

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

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

144145c_irts FAny x = x

145146

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

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

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

148150irts_c FUnit x = x

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

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

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

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

198200

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

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

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

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

202204

src/IRTS/LParser.hs+2−1

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

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

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

206206 return (LOp LStrLen [e])

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

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

208+ return (LOp LReadStr [e])

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

209210 e <- pLExp; lchar ')'

210211 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

3838data FLang = LANG_C

3939 deriving Show

4040

4242 deriving Show

4343

4444data LAlt = LConCase Int Name [Name] LExp