6b46ffc · Idris-dev · git.iko.soy

idris.cabal+1−1

compare with master

unifiedsplit

@@ -78,7 +78,7 @@ Executable idris

78

79 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline<0.7,

80 containers, process, transformers, filepath, directory,

81− binary, bytestring, epic>=0.9.3.1, pretty

81+ binary, bytestring, epic>=0.9.3.2, pretty

82

83 Extensions: MultiParamTypeClasses, FunctionalDependencies,

84 FlexibleInstances, TemplateHaskell

lib/prelude.idr+2−2

@@ -194,7 +194,7 @@ print : Show a => a -> IO ()

194print x = putStrLn (show x)

195

196getLine : IO String

197−getLine = mkForeign (FFun "readStr" Nil FString)

197+getLine = return (prim__readString prim__stdin)

198

199putChar : Char -> IO ()

200putChar c = mkForeign (FFun "putchar" [FChar] FUnit) c

@@ -230,7 +230,7 @@ closeFile : File -> IO ()

230closeFile (FHandle h) = do_fclose h

231

232do_fread : Ptr -> IO String

233−do_fread h = mkForeign (FFun "freadStr" [FPtr] FString) h

233+do_fread h = return (prim__readString h)

234

235fread : File -> IO String

236fread (FHandle h) = do_fread h

rts/idris_gc.c+26−6

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

1#include "idris_rts.h"

2#include "idris_gc.h"

3+#include <assert.h>

3

4

4VAL copy(VM* vm, VAL x) {

5VAL copy(VM* vm, VAL x) {

5 int i;

6 int i;

@@ -34,8 +35,7 @@ VAL copy(VM* vm, VAL x) {

34 cl = MKPTR(vm, x->info.ptr);

35 cl = MKPTR(vm, x->info.ptr);

35 break;

36 break;

36 case FWD:

37 case FWD:

37− cl = x->info.ptr;

38+ return x->info.ptr;

38− break;

39 }

40 x->ty = FWD;

41 x->info.ptr = cl;

@@ -46,25 +46,31 @@ void cheney(VM *vm) {

46 VAL* argptr;

47 int i;

48 char* scan = vm->heap;

49−

49+

50 while(scan < vm->heap_next) {

51 size_t inc = *((size_t*)scan);

52− VAL heap_item = (VAL)(scan+sizeof(size_t)*2);

52+ VAL heap_item = (VAL)(scan+sizeof(size_t));

53 // If it's a CON, copy its arguments

54 switch(heap_item->ty) {

55 case CON:

56 argptr = (VAL*)(heap_item->info.c.args);

57 for(i = 0; i < heap_item->info.c.arity; ++i) {

58+ printf("Copying %d %p\n", heap_item->info.c.tag, *argptr);

58− *argptr = copy(vm, *argptr);

59+ VAL newptr = copy(vm, *argptr);

60+ printf("Got %p\t\t%p %p\n", newptr, scan, vm->heap_next);

61+ *argptr = newptr;

59 argptr++;

62 argptr++;

60 }

63 }

61 break;

64 break;

62 }

65 }

63 scan += inc;

66 scan += inc;

64 }

67 }

68+ assert(scan == vm->heap_next);

65}

69}

66

70

67void gc(VM* vm) {

71void gc(VM* vm) {

72+ printf("Collecting\n");

73+

68 char* newheap = malloc(vm -> heap_size);

74 char* newheap = malloc(vm -> heap_size);

69 char* oldheap = vm -> heap;

75 char* oldheap = vm -> heap;

70 if (vm->oldheap != NULL) free(vm->oldheap);

76 if (vm->oldheap != NULL) free(vm->oldheap);

@@ -81,6 +87,8 @@ void gc(VM* vm) {

81 *root = copy(vm, *root);

87 *root = copy(vm, *root);

82 }

88 }

83 vm->ret = copy(vm, vm->ret);

89 vm->ret = copy(vm, vm->ret);

90+ vm->reg1 = copy(vm, vm->reg1);

91+

84 cheney(vm);

92 cheney(vm);

85

93

86 // After reallocation, if we've still more than half filled the new heap, grow the heap

94 // After reallocation, if we've still more than half filled the new heap, grow the heap

@@ -88,6 +96,18 @@ void gc(VM* vm) {

88

96

89 if ((vm->heap_next - vm->heap) > vm->heap_size >> 1) {

97 if ((vm->heap_next - vm->heap) > vm->heap_size >> 1) {

90 vm->heap_size += vm->heap_growth;

98 vm->heap_size += vm->heap_growth;

91− }

99+ }

92 vm->oldheap = oldheap;

100 vm->oldheap = oldheap;

101+

102+ gcInfo(vm, 0);

103+}

104+

105+void gcInfo(VM* vm, int doGC) {

106+ printf("\nStack: %p %p\n", vm->valstack, vm->valstack_top);

107+ printf("Total allocations: %d\n", vm->allocations);

108+ printf("GCs: %d\n", vm->collections);

109+ printf("Final heap size %d\n", (int)(vm->heap_size));

110+ printf("Final heap use %d\n", (int)(vm->heap_next - vm->heap));

111+ if (doGC) { gc(vm); }

112+ printf("Final heap use after GC %d\n", (int)(vm->heap_next - vm->heap));

93}

113}

rts/idris_gc.h+1

@@ -4,5 +4,6 @@

4#include "idris_rts.h"

5

6void gc(VM* vm);

7+void gcInfo(VM* vm, int doGC);

7

8

8#endif

9#endif

rts/idris_main.c+2−8

@@ -1,14 +1,8 @@

1int main(int argc, char* argv[]) {

2− VM* vm = init_vm(1024000, 1024000);

2+ VM* vm = init_vm(4096000, 20480); // 1024000);

3 _idris__123_runMain0_125_(vm, NULL);

4 //_idris_main(vm, NULL);

5#ifdef IDRIS_TRACE

6− printf("\nStack: %p %p\n", vm->valstack, vm->valstack_top);

6+ gcInfo(vm, 1);

7− printf("Total allocations: %d\n", vm->allocations);

8− printf("GCs: %d\n", vm->collections);

9− printf("Final heap size %d\n", (int)(vm->heap_size));

10− printf("Final heap use %d\n", (int)(vm->heap_next - vm->heap));

11− gc(vm);

12− printf("Final heap use after GC %d\n", (int)(vm->heap_next - vm->heap));

13#endif

7#endif

14}

8}

rts/idris_rts.c+45−15

@@ -20,7 +20,7 @@ VM* init_vm(int stack_size, size_t heap_size) {

20 vm -> intstack_ptr = intstack;

21 vm -> floatstack = floatstack;

22 vm -> floatstack_ptr = floatstack;

23− vm -> stack_max = stack_size;

23+ vm -> stack_max = valstack + stack_size;

24 vm -> heap = malloc(heap_size);

25 vm -> oldheap = NULL;

26 vm -> heap_next = vm -> heap;

@@ -30,18 +30,21 @@ VM* init_vm(int stack_size, size_t heap_size) {

30 vm -> allocations = 0;

31 vm -> heap_growth = heap_size;

32 vm -> ret = NULL;

33+ vm -> reg1 = NULL;

33 return vm;

34 return vm;

34}

35}

35

36

36void* allocate(VM* vm, size_t size) {

37void* allocate(VM* vm, size_t size) {

38+// return malloc(size);

37 if ((size & 7)!=0) {

39 if ((size & 7)!=0) {

38 size = 8 + ((size >> 3) << 3);

40 size = 8 + ((size >> 3) << 3);

39 }

41 }

40− vm->allocations += size+sizeof(size_t)*2;

42+ vm->allocations += size + sizeof(size_t);

41 if (vm -> heap_next + size < vm -> heap_end) {

43 if (vm -> heap_next + size < vm -> heap_end) {

42− void* ptr = (void*)(((size_t*)(vm->heap_next))+2);

44+ void* ptr = (void*)(vm->heap_next + sizeof(size_t));

43− *((size_t*)(vm->heap_next)) = size+sizeof(size_t)*2;

45+ *((size_t*)(vm->heap_next)) = size + sizeof(size_t);

44− vm -> heap_next += size+sizeof(size_t)*2;

46+ vm -> heap_next += size + sizeof(size_t);

47+ bzero(ptr, size);

45 return ptr;

48 return ptr;

46 } else {

49 } else {

47 gc(vm);

50 gc(vm);

@@ -57,6 +60,9 @@ void* allocCon(VM* vm, int arity) {

57 } else {

60 } else {

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

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

59 }

62 }

63+ cl -> info.c.arity = arity;

64+// cl -> info.c.tag = 42424242;

65+// printf("%p\n", cl);

60 return (void*)cl;

66 return (void*)cl;

61}

67}

62

68

@@ -84,17 +90,17 @@ VAL MKPTR(VM* vm, void* ptr) {

84 return cl;

90 return cl;

85}

91}

86

92

87−VAL MKCON(VM* vm, int tag, int arity, ...) {

93+VAL MKCON(VM* vm, VAL cl, int tag, int arity, ...) {

88− Closure* cl;

89 int i;

94 int i;

90 va_list args;

95 va_list args;

91

96

92 va_start(args, arity);

97 va_start(args, arity);

93

98

94− cl = allocCon(vm, arity);

99+// Closure* cl = allocCon(vm, arity);

95 cl -> info.c.tag = tag;

100 cl -> info.c.tag = tag;

96 cl -> info.c.arity = arity;

101 cl -> info.c.arity = arity;

97 VAL* argptr = (VAL*)(cl -> info.c.args);

102 VAL* argptr = (VAL*)(cl -> info.c.args);

103+ printf("... %p %p\n", cl, argptr);

98

104

99 for (i = 0; i < arity; ++i) {

105 for (i = 0; i < arity; ++i) {

100 VAL v = va_arg(args, VAL);

106 VAL v = va_arg(args, VAL);

@@ -102,7 +108,6 @@ VAL MKCON(VM* vm, int tag, int arity, ...) {

102 argptr++;

108 argptr++;

103 }

109 }

104 va_end(args);

110 va_end(args);

105−

106 return cl;

111 return cl;

107}

112}

108

113

@@ -122,7 +127,23 @@ void SLIDE(VM* vm, int args) {

122 }

127 }

123}

128}

124

129

130+void dumpStack(VM* vm) {

131+ int i = 0;

132+ VAL* root;

133+

134+ for (root = vm->valstack; root < vm->valstack_top; ++root, ++i) {

135+ printf("%d: ", i);

136+ dumpVal(*root);

137+ if (*root >= (VAL)(vm->heap) && *root < (VAL)(vm->heap_end)) { printf("OK"); }

138+ printf("\n");

139+ }

140+ printf("RET: ");

141+ dumpVal(vm->ret);

142+ printf("\n");

143+}

144+

125void dumpVal(VAL v) {

145void dumpVal(VAL v) {

146+ if (v==NULL) return;

126 int i;

147 int i;

127 if (ISINT(v)) {

148 if (ISINT(v)) {

128 printf("%ld ", GETINT(v));

149 printf("%ld ", GETINT(v));

@@ -137,6 +158,10 @@ void dumpVal(VAL v) {

137 }

158 }

138 printf("] ");

159 printf("] ");

139 break;

160 break;

161+ case FWD:

162+ printf("FWD ");

163+ dumpVal((VAL)(v->info.ptr));

164+ break;

140 default:

165 default:

141 printf("val");

166 printf("val");

142 }

167 }

@@ -154,7 +179,10 @@ VAL idris_castIntStr(VM* vm, VAL i) {

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

179VAL idris_castStrInt(VM* vm, VAL i) {

155 char *end;

180 char *end;

156 i_int v = strtol(GETSTR(i), &end, 10);

181 i_int v = strtol(GETSTR(i), &end, 10);

182+ if (*end == '\0' || *end == '\n' || *end == '\r')

157− if (*end != '\0') return MKINT(0); else return MKINT(v);

183+ return MKINT(v);

184+ else

185+ return MKINT(0);

158}

186}

159

187

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

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

@@ -170,8 +198,10 @@ VAL idris_castStrFloat(VM* vm, VAL i) {

170}

198}

171

199

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

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

173− char *ls = GETSTR(l);

174 char *rs = GETSTR(r);

201 char *rs = GETSTR(r);

202+ char *ls = GETSTR(l);

203+ // dumpVal(l);

204+ // printf("\n");

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

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

176 cl -> ty = STRING;

206 cl -> ty = STRING;

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

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

@@ -246,10 +276,10 @@ VAL idris_strTail(VM* vm, VAL str) {

246

276

247VAL idris_strCons(VM* vm, VAL x, VAL xs) {

277VAL idris_strCons(VM* vm, VAL x, VAL xs) {

248 char *xstr = GETSTR(xs);

278 char *xstr = GETSTR(xs);

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

279+ Closure* cl = allocate(vm, sizeof(Closure) +

250 strlen(xstr) + 2);

280 strlen(xstr) + 2);

251 cl -> ty = STRING;

281 cl -> ty = STRING;

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

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

253 cl -> info.str[0] = (char)(GETINT(x));

283 cl -> info.str[0] = (char)(GETINT(x));

254 strcpy(cl -> info.str+1, xstr);

284 strcpy(cl -> info.str+1, xstr);

255 return cl;

285 return cl;

@@ -261,10 +291,10 @@ VAL idris_strIndex(VM* vm, VAL str, VAL i) {

261

291

262VAL idris_strRev(VM* vm, VAL str) {

292VAL idris_strRev(VM* vm, VAL str) {

263 char *xstr = GETSTR(str);

293 char *xstr = GETSTR(str);

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

294+ Closure* cl = allocate(vm, sizeof(Closure) +

265 strlen(xstr) + 1);

295 strlen(xstr) + 1);

266 cl -> ty = STRING;

296 cl -> ty = STRING;

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

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

268 int y = 0;

298 int y = 0;

269 int x = strlen(xstr);

299 int x = strlen(xstr);

270

300

rts/idris_rts.h+10−3

@@ -44,12 +44,13 @@ typedef struct {

44 char* oldheap;

45 char* heap_next;

46 char* heap_end;

47− int stack_max;

47+ VAL* stack_max;

48 size_t heap_size;

49 size_t heap_growth;

50 int allocations;

51 int collections;

52 VAL ret;

53+ VAL reg1;

53} VM;

54} VM;

54

55

55VM* init_vm(int stack_size, size_t heap_size);

56VM* init_vm(int stack_size, size_t heap_size);

@@ -63,6 +64,7 @@ typedef void(*func)(VM*, VAL*);

63#define RVAL (vm->ret)

64#define RVAL (vm->ret)

64#define LOC(x) (*(vm->valstack_base + (x)))

65#define LOC(x) (*(vm->valstack_base + (x)))

65#define TOP(x) (*(vm->valstack_top + (x)))

66#define TOP(x) (*(vm->valstack_top + (x)))

67+#define REG1 (vm->reg1)

66

68

67// Retrieving values

69// Retrieving values

68

70

@@ -90,7 +92,8 @@ typedef intptr_t i_int;

90

92

91#define INITFRAME VAL* myoldbase

93#define INITFRAME VAL* myoldbase

92#define REBASE vm->valstack_base = oldbase

94#define REBASE vm->valstack_base = oldbase

93−#define RESERVE(x)

95+#define RESERVE(x) if (vm->valstack_top+(x) > vm->stack_max) { stackOverflow(); } \

96+ else { bzero(vm->valstack_top, (x)); }

94#define ADDTOP(x) vm->valstack_top += (x)

97#define ADDTOP(x) vm->valstack_top += (x)

95#define TOPBASE(x) vm->valstack_top = vm->valstack_base + (x)

98#define TOPBASE(x) vm->valstack_top = vm->valstack_base + (x)

96#define BASETOP(x) vm->valstack_base = vm->valstack_top + (x)

99#define BASETOP(x) vm->valstack_base = vm->valstack_top + (x)

@@ -104,7 +107,10 @@ VAL MKFLOAT(VM* vm, double val);

104VAL MKSTR(VM* vm, char* str);

107VAL MKSTR(VM* vm, char* str);

105VAL MKPTR(VM* vm, void* ptr);

108VAL MKPTR(VM* vm, void* ptr);

106

109

107−VAL MKCON(VM* vm, int tag, int arity, ...);

110+VAL MKCON(VM* vm, VAL cl, int tag, int arity, ...);

111+

112+#define SETTAG(x, a) (x)->info.c.tag = (a)

113+#define SETARG(x, i, a) ((VAL*)((x)->info.c.args))[i] = ((VAL)(a))

108

114

109void PROJECT(VM* vm, VAL r, int loc, int arity);

115void PROJECT(VM* vm, VAL r, int loc, int arity);

110void SLIDE(VM* vm, int args);

116void SLIDE(VM* vm, int args);

@@ -113,6 +119,7 @@ void* allocate(VM* vm, size_t size);

113void* allocCon(VM* vm, int arity);

119void* allocCon(VM* vm, int arity);

114

120

115void dumpVal(VAL r);

121void dumpVal(VAL r);

122+void dumpStack(VM* vm);

116

123

117// Casts

124// Casts

118

125

src/Core/Evaluate.hs+2−1

@@ -216,7 +216,8 @@ eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

216-- | spec = specApply ntimes stk env f args

217 apply ntimes_in stk top env f@(VP Ref n ty) args

218 | (True, ntimes) <- usable n ntimes_in

219+ = -- trace (show n) $

219− = do let val = lookupDefAcc Nothing n atRepl ctxt

220+ do let val = lookupDefAcc Nothing n atRepl ctxt

220 case val of

221 case val of

221 [(CaseOp inl _ _ ns tree _ _, Public)] ->

222 [(CaseOp inl _ _ ns tree _ _, Public)] ->

222 if simpl && (not inl || elem n stk)

223 if simpl && (not inl || elem n stk)

src/Core/Unify.hs+9−8

@@ -26,14 +26,15 @@ unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

26 Injs, Fails)

27unify ctxt env topx topy

28 = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of

29− -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

29+ -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

30+ -- _ ->

30− let topxn = normalise ctxt env topx

31+ let topxn = normalise ctxt env topx

31− topyn = normalise ctxt env topy in

32+ topyn = normalise ctxt env topy in

32− case runStateT (un' False [] topxn topyn)

33+ case runStateT (un' False [] topxn topyn)

33− (UI 0 [] []) of

34+ (UI 0 [] []) of

34− OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)

35+ OK (v, UI _ inj fails) -> return (filter notTrivial v, inj, reverse fails)

35−-- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s

36+-- OK (_, UI s _ ((_,_,f):fs)) -> tfail $ CantUnify topx topy f s

36− Error e -> tfail e

37+ Error e -> tfail e

37 where

38 where

38 notTrivial (x, P _ x' _) = x /= x'

39 notTrivial (x, P _ x' _) = x /= x'

39 notTrivial _ = True

40 notTrivial _ = True

src/IRTS/Bytecode.hs+2−2

@@ -19,7 +19,7 @@ returns) are stored.

19

20-}

21

22−data Reg = RVal | L Int | T Int

22+data Reg = RVal | L Int | T Int | Tmp

23 deriving (Show, Eq)

24

25data BC = ASSIGN Reg Reg

@@ -56,7 +56,7 @@ bc :: Reg -> SExp -> Bool -> -- returning

56 [BC]

57bc reg (SV (Glob n)) r = bc reg (SApp False n []) r

58bc reg (SV (Loc i)) r = assign reg (L i) ++ clean r

59−bc reg (SApp _ f vs) r

59+bc reg (SApp False f vs) r

60 = RESERVE (length vs) : moveReg 0 vs

61 ++ [STOREOLD, BASETOP 0, ADDTOP (length vs), CALL f] ++

62 assign reg RVal ++ clean r

src/IRTS/CodegenC.hs+21−6

@@ -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#include <idris_stdfgn.h>\n"

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

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

54

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

@@ -69,6 +69,7 @@ indent i = take (i * 4) (repeat ' ')

69creg RVal = "RVAL"

70creg (L i) = "LOC(" ++ show i ++ ")"

71creg (T i) = "TOP(" ++ show i ++ ")"

72+creg Tmp = "REG1"

72

73

73toDecl :: Name -> String

74toDecl :: Name -> String

74toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n"

75toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n"

@@ -93,9 +94,18 @@ bcc i (ASSIGNCONST l c)

93 mkConst (Str s) = "MKSTR(vm, " ++ show s ++ ")"

94 mkConst (Str s) = "MKSTR(vm, " ++ show s ++ ")"

94 mkConst _ = "MKINT(42424242)"

95 mkConst _ = "MKINT(42424242)"

95bcc i (MKCON l tag args)

96bcc i (MKCON l tag args)

97+ = indent i ++ creg Tmp ++ " = allocCon(vm, " ++ show (length args) ++

98+ "); " ++ "SETTAG(" ++ creg Tmp ++ ", " ++ show tag ++ ");\n" ++

99+ indent i ++ setArgs 0 args ++ "\n" ++

100+ indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"

101+

96− = indent i ++ creg l ++ " = MKCON(vm, " ++ show tag ++ ", " ++

102+-- "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " ++

97− show (length args) ++ concatMap showArg args ++ ");\n"

103+-- show (length args) ++ concatMap showArg args ++ ");\n"

98 where showArg r = ", " ++ creg r

104 where showArg r = ", " ++ creg r

105+ setArgs i [] = ""

106+ setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++

107+ "); " ++ setArgs (i + 1) xs

108+

99bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++

109bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++

100 ", " ++ show a ++ ");\n"

110 ", " ++ show a ++ ");\n"

101bcc i (CASE r code def)

111bcc i (CASE r code def)

@@ -135,11 +145,11 @@ bcc i (FOREIGNCALL l LANG_C rty fn args)

135 c_irts rty (creg l ++ " = ")

145 c_irts rty (creg l ++ " = ")

136 (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"

146 (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"

137 where fcall (t, arg) = irts_c t (creg arg)

147 where fcall (t, arg) = irts_c t (creg arg)

138−bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); exit(-1);"

148+bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); assert(0); exit(-1);"

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

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

140

150

141−c_irts FInt l x = l ++ "MKINT((i_int)(" ++ x ++ ")"

151+c_irts FInt l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

142−c_irts FChar l x = l ++ "MKINT((i_int)(" ++ x ++ ")"

152+c_irts FChar l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

143c_irts FString l x = l ++ "MKSTR(" ++ x ++ ")"

153c_irts FString l x = l ++ "MKSTR(" ++ x ++ ")"

144c_irts FUnit l x = x

154c_irts FUnit l x = x

145c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"

155c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"

@@ -221,6 +231,11 @@ doOp v LStrTail [x] = v ++ "idris_strTail(vm, " ++ creg x ++ ")"

221doOp v LStrCons [x, y] = v ++ "idris_strCons(vm, " ++ creg x ++ "," ++ creg y ++ ")"

231doOp v LStrCons [x, y] = v ++ "idris_strCons(vm, " ++ creg x ++ "," ++ creg y ++ ")"

222doOp v LStrIndex [x, y] = v ++ "idris_strIndex(vm, " ++ creg x ++ "," ++ creg y ++ ")"

232doOp v LStrIndex [x, y] = v ++ "idris_strIndex(vm, " ++ creg x ++ "," ++ creg y ++ ")"

223doOp v LStrRev [x] = v ++ "idris_strRev(vm, " ++ creg x ++ ")"

233doOp v LStrRev [x] = v ++ "idris_strRev(vm, " ++ creg x ++ ")"

234+

235+doOp v LStdIn [] = v ++ "MKPTR(vm, stdin)"

236+doOp v LStdOut [] = v ++ "MKPTR(vm, stdout)"

237+doOp v LStdErr [] = v ++ "MKPTR(vm, stderr)"

238+

224doOp v LNoOp [x] = ""

239doOp v LNoOp [x] = ""

225doOp _ _ _ = "FAIL"

240doOp _ _ _ = "FAIL"

226

241

src/IRTS/Compiler.hs+10−7

@@ -28,15 +28,15 @@ compileC f tm = do checkMVs

28 defsIn <- mkDecls tm (concat used)

29 maindef <- irMain tm

30 let defs = defsIn ++ [(MN 0 "runMain", maindef)]

31− iputStrLn (show defs)

31+ -- iputStrLn $ showSep "\n" (map show defs)

32 let (nexttag, tagged) = addTags 0 (liftAll defs)

33 let ctxtIn = addAlist tagged emptyContext

34 let defuns = defunctionalise nexttag ctxtIn

35−-- print defuns

35+-- iputStrLn $ showSep "\n" (map show (toAlist defuns))

36 let checked = checkDefs defuns (toAlist defuns)

37−-- print checked

38 case checked of

37 case checked of

38+ OK c -> do -- iputStrLn $ showSep "\n" (map show c)

39− OK c -> liftIO $ codegenC c f True [] "" TRACE

39+ liftIO $ codegenC c f True [] "" TRACE

40 Error e -> fail $ show e

41 where checkMVs = do i <- get

42 case idris_metavars i \\ primDefs of

@@ -61,10 +61,13 @@ allNames ns n = do i <- get

61mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]

62mkDecls t used

63 = do i <- getIState

64− let ds = filter (\ (n, d) -> n `elem` used) $ ctxtAlist (tt_ctxt i)

64+ let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)

65 decls <- mapM build ds

66 return decls

67

68+isCon (TyDecl _ _) = True

69+isCon _ = False

70+

68class ToIR a where

71class ToIR a where

69 ir :: a -> Idris LExp

72 ir :: a -> Idris LExp

70

73

@@ -89,7 +92,7 @@ mkLDecl n (CaseOp _ _ pats _ _ args sc) = do e <- ir (args, sc)

89 return (declArgs [] n e)

92 return (declArgs [] n e)

90mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n (-1) a

93mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n (-1) a

91mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

94mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

92−mkLDecl n _ = return (LFun n [] (LError "Impossible"))

95+mkLDecl n _ = return (LFun n [] (LError ("Impossible declaration " ++ show n)))

93

96

94instance ToIR (TT Name) where

97instance ToIR (TT Name) where

95 ir tm = ir' [] tm where

98 ir tm = ir' [] tm where

@@ -130,7 +133,7 @@ instance ToIR (TT Name) where

130 = do sc' <- ir' (n : env) sc

133 = do sc' <- ir' (n : env) sc

131 v' <- ir' env v

134 v' <- ir' env v

132 return $ LLet n v' sc'

135 return $ LLet n v' sc'

133− ir' env (Bind _ _ _) = return $ LError "Impossible"

136+ ir' env (Bind _ _ _) = return $ LConst (I 424242)

134 ir' env (Constant c) = return $ LConst c

137 ir' env (Constant c) = return $ LConst c

135 ir' env _ = return $ LError "Impossible"

138 ir' env _ = return $ LError "Impossible"

136

139

src/IRTS/Lang.hs+1

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

33 | LFSqrt | LFFloor | LFCeil

34

36+ | LStdIn | LStdOut | LStdErr

36 | LNoOp

37 | LNoOp

37 deriving Show

38 deriving Show

38

39

src/IRTS/Simplified.hs+1−1

@@ -104,7 +104,7 @@ checkDefs ctxt (con@(n, LConstructor _ _ _) : xs)

104 return xs'

105checkDefs ctxt ((n, LFun n' args exp) : xs)

106 = do let sexp = evalState (simplify True exp) (ctxt, 0)

107− (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (-1)

107+ (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (length args)

108 xs' <- checkDefs ctxt xs

109 return ((n, SFun n' args ((locs + 1) - length args) exp') : xs')

110

src/Idris/Primitives.hs+13

@@ -76,6 +76,11 @@ strRev x = foreign_ tyString "strrev" [(x, tyString)]

76strEq x y = foreign_ tyInt "streq" [(x, tyString), (y, tyString)]

77strLt x y = foreign_ tyInt "strlt" [(x, tyString), (y, tyString)]

78

79+readStr x = foreign_ tyString "freadStr" [(x, tyPtr)]

80+

81+stream_stdin = let args :: [(ETm, E.Type)] = [] in

82+ foreign_ tyPtr "get_stdin" args

83+

79total = Total []

84total = Total []

80partial = Partial NotCovering

85partial = Partial NotCovering

81

86

@@ -218,6 +223,12 @@ primitives =

218 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

223 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

219 ([E.name "x"], strRev (fun "x"))

224 ([E.name "x"], strRev (fun "x"))

220 (1, LStrRev) total,

225 (1, LStrRev) total,

226+ Prim (UN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)

227+ ([E.name "h"], readStr (fun "h")) (1, LReadStr) partial,

228+

229+ -- Streams

230+ Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

231+ ([], stream_stdin) (0, LStdIn) partial,

221

232

222 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)

233 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)

223 ([E.name "a", E.name "b", E.name "x"], fun "x")

234 ([E.name "a", E.name "b", E.name "x"], fun "x")

@@ -322,6 +333,8 @@ p_strCons _ = Nothing

322p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))

333p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))

323p_strRev _ = Nothing

334p_strRev _ = Nothing

324

335

336+p_cantreduce _ = Nothing

337+

325elabPrim :: Prim -> Idris ()

338elabPrim :: Prim -> Idris ()

326elabPrim (Prim n ty i def epic sc tot)

339elabPrim (Prim n ty i def epic sc tot)

327 = do updateContext (addOperator n ty i def)

340 = do updateContext (addOperator n ty i def)

src/Idris/REPL.hs+8−8

@@ -171,7 +171,7 @@ process fn (ExecVal t)

171-- [pexp t])

172 (tmpn, tmph) <- liftIO tempfile

173 liftIO $ hClose tmph

174− compile tmpn tm

174+ compileC tmpn tm

175 liftIO $ system tmpn

176 return ()

177 where fc = FC "(input)" 0

@@ -268,17 +268,17 @@ process fn Execute = do (m, _) <- elabVal toplevel False

268 liftIO $ system tmpn

269 return ()

270 where fc = FC "main" 0

271−process fn (Compile f) = do (m, _) <- elabVal toplevel False

272− (PApp fc

273− (PRef fc (UN "run__IO"))

274− [pexp $ PRef fc (NS (UN "main") ["main"])])

275− compile f m

276− where fc = FC "main" 0

277process fn (NewCompile f)

271process fn (NewCompile f)

272+ = do (m, _) <- elabVal toplevel False

273+ (PApp fc (PRef fc (UN "run__IO"))

274+ [pexp $ PRef fc (NS (UN "main") ["main"])])

275+ compileC f m

276+ where fc = FC "main" 0

277+process fn (Compile f)

278 = do (m, _) <- elabVal toplevel False

279 (PApp fc (PRef fc (UN "run__IO"))

280 [pexp $ PRef fc (NS (UN "main") ["main"])])

281− compileC f m

281+ compile f m

282 where fc = FC "main" 0

283process fn (LogLvl i) = setLogLevel i

284process fn Metavars

test/test009/test009.idr+1−1

@@ -5,5 +5,5 @@ pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],

5 x*x + y*y == z*z ]

6

7main : IO ()

8−main = print (pythag 50)

8+main = putStrLn (show (pythag 50))

9