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

idris.cabal+1−1

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

7878

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

8080 containers, process, transformers, filepath, directory,

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

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

8282

8383 Extensions: MultiParamTypeClasses, FunctionalDependencies,

8484 FlexibleInstances, TemplateHaskell

lib/prelude.idr+2−2

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

194194print x = putStrLn (show x)

195195

196196getLine : IO String

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

197+getLine = return (prim__readString prim__stdin)

198198

199199putChar : Char -> IO ()

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

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

230230closeFile (FHandle h) = do_fclose h

231231

232232do_fread : Ptr -> IO String

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

233+do_fread h = return (prim__readString h)

234234

235235fread : File -> IO String

236236fread (FHandle h) = do_fread h

rts/idris_gc.c+26−6

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

11#include "idris_rts.h"

22#include "idris_gc.h"

3+#include <assert.h>

34

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

56 int i;

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

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

3536 break;

3637 case FWD:

37− cl = x->info.ptr;

38− break;

38+ return x->info.ptr;

3939 }

4040 x->ty = FWD;

4141 x->info.ptr = cl;

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

4646 VAL* argptr;

4747 int i;

4848 char* scan = vm->heap;

49−

49+

5050 while(scan < vm->heap_next) {

5151 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));

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

5454 switch(heap_item->ty) {

5555 case CON:

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

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

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

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

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

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

61+ *argptr = newptr;

5962 argptr++;

6063 }

6164 break;

6265 }

6366 scan += inc;

6467 }

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

6569}

6670

6771void gc(VM* vm) {

72+ printf("Collecting\n");

73+

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

6975 char* oldheap = vm -> heap;

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

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

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

8288 }

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

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

91+

8492 cheney(vm);

8593

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

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

8896

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

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

91− }

99+ }

92100 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));

93113}

rts/idris_gc.h+1

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

44#include "idris_rts.h"

55

66void gc(VM* vm);

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

78

89#endif

rts/idris_main.c+2−8

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

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

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

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

33 _idris__123_runMain0_125_(vm, NULL);

44 //_idris_main(vm, NULL);

55#ifdef IDRIS_TRACE

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

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

6+ gcInfo(vm, 1);

137#endif

148}

rts/idris_rts.c+45−15

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

2020 vm -> intstack_ptr = intstack;

2121 vm -> floatstack = floatstack;

2222 vm -> floatstack_ptr = floatstack;

23− vm -> stack_max = stack_size;

23+ vm -> stack_max = valstack + stack_size;

2424 vm -> heap = malloc(heap_size);

2525 vm -> oldheap = NULL;

2626 vm -> heap_next = vm -> heap;

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

3030 vm -> allocations = 0;

3131 vm -> heap_growth = heap_size;

3232 vm -> ret = NULL;

33+ vm -> reg1 = NULL;

3334 return vm;

3435}

3536

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

38+// return malloc(size);

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

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

3941 }

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

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

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

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

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

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

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

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

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

47+ bzero(ptr, size);

4548 return ptr;

4649 } else {

4750 gc(vm);

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

5760 } else {

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

5962 }

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

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

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

6066 return (void*)cl;

6167}

6268

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

8490 return cl;

8591}

8692

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

88− Closure* cl;

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

8994 int i;

9095 va_list args;

9196

9297 va_start(args, arity);

9398

94− cl = allocCon(vm, arity);

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

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

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

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

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

98104

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

100106 VAL v = va_arg(args, VAL);

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

102108 argptr++;

103109 }

104110 va_end(args);

105−

106111 return cl;

107112}

108113

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

122127 }

123128}

124129

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+

125145void dumpVal(VAL v) {

146+ if (v==NULL) return;

126147 int i;

127148 if (ISINT(v)) {

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

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

137158 }

138159 printf("] ");

139160 break;

161+ case FWD:

162+ printf("FWD ");

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

164+ break;

140165 default:

141166 printf("val");

142167 }

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

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

155180 char *end;

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

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

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

183+ return MKINT(v);

184+ else

185+ return MKINT(0);

158186}

159187

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

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

170198}

171199

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

173− char *ls = GETSTR(l);

174201 char *rs = GETSTR(r);

202+ char *ls = GETSTR(l);

203+ // dumpVal(l);

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

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

176206 cl -> ty = STRING;

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

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

246276

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

248278 char *xstr = GETSTR(xs);

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

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

250280 strlen(xstr) + 2);

251281 cl -> ty = STRING;

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

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

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

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

255285 return cl;

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

261291

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

263293 char *xstr = GETSTR(str);

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

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

265295 strlen(xstr) + 1);

266296 cl -> ty = STRING;

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

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

268298 int y = 0;

269299 int x = strlen(xstr);

270300

rts/idris_rts.h+10−3

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

4444 char* oldheap;

4545 char* heap_next;

4646 char* heap_end;

47− int stack_max;

47+ VAL* stack_max;

4848 size_t heap_size;

4949 size_t heap_growth;

5050 int allocations;

5151 int collections;

5252 VAL ret;

53+ VAL reg1;

5354} VM;

5455

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

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

6364#define RVAL (vm->ret)

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

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

67+#define REG1 (vm->reg1)

6668

6769// Retrieving values

6870

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

9092

9193#define INITFRAME VAL* myoldbase

9294#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)); }

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

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

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

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

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

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

106109

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))

108114

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

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

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

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

114120

115121void dumpVal(VAL r);

122+void dumpStack(VM* vm);

116123

117124// Casts

118125

src/Core/Evaluate.hs+2−1

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

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

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

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

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

219+ = -- trace (show n) $

220+ do let val = lookupDefAcc Nothing n atRepl ctxt

220221 case val of

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

222223 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)],

2626 Injs, Fails)

2727unify ctxt env topx topy

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

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

30− let topxn = normalise ctxt env topx

31− topyn = normalise ctxt env topy in

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

33− (UI 0 [] []) of

34− 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− Error e -> tfail e

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

30+ -- _ ->

31+ let topxn = normalise ctxt env topx

32+ topyn = normalise ctxt env topy in

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

34+ (UI 0 [] []) of

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

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

37+ Error e -> tfail e

3738 where

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

3940 notTrivial _ = True

src/IRTS/Bytecode.hs+2−2

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

1919

2020-}

2121

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

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

2323 deriving (Show, Eq)

2424

2525data BC = ASSIGN Reg Reg

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

5656 [BC]

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

5858bc 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

6060 = RESERVE (length vs) : moveReg 0 vs

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

6262 assign reg RVal ++ clean r

src/IRTS/CodegenC.hs+21−6

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

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

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

5454

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

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

6969creg RVal = "RVAL"

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

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

72+creg Tmp = "REG1"

7273

7374toDecl :: Name -> String

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

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

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

9495 mkConst _ = "MKINT(42424242)"

9596bcc i (MKCON l tag args)

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

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

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+

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

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

98104 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+

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

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

101111bcc i (CASE r code def)

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

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

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

137147 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);"

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

140150

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

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

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

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

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

144154c_irts FUnit l x = x

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

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

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

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

223233doOp 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+

224239doOp v LNoOp [x] = ""

225240doOp _ _ _ = "FAIL"

226241

src/IRTS/Compiler.hs+10−7

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

2828 defsIn <- mkDecls tm (concat used)

2929 maindef <- irMain tm

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

31− iputStrLn (show defs)

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

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

3333 let ctxtIn = addAlist tagged emptyContext

3434 let defuns = defunctionalise nexttag ctxtIn

35−-- print defuns

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

3636 let checked = checkDefs defuns (toAlist defuns)

37−-- print checked

3837 case checked of

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

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

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

4040 Error e -> fail $ show e

4141 where checkMVs = do i <- get

4242 case idris_metavars i \\ primDefs of

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

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

6262mkDecls t used

6363 = 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)

6565 decls <- mapM build ds

6666 return decls

6767

68+isCon (TyDecl _ _) = True

69+isCon _ = False

70+

6871class ToIR a where

6972 ir :: a -> Idris LExp

7073

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

8992 return (declArgs [] n e)

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

9194mkLDecl 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)))

9396

9497instance ToIR (TT Name) where

9598 ir tm = ir' [] tm where

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

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

131134 v' <- ir' env v

132135 return $ LLet n v' sc'

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

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

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

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

136139

src/IRTS/Lang.hs+1

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

3333 | LFSqrt | LFFloor | LFCeil

3434

36+ | LStdIn | LStdOut | LStdErr

3637 | LNoOp

3738 deriving Show

3839

src/IRTS/Simplified.hs+1−1

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

104104 return xs'

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

106106 = 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)

108108 xs' <- checkDefs ctxt xs

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

110110

src/Idris/Primitives.hs+13

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

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

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

7878

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+

7984total = Total []

8085partial = Partial NotCovering

8186

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

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

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

220225 (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,

221232

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

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

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

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

323334p_strRev _ = Nothing

324335

336+p_cantreduce _ = Nothing

337+

325338elabPrim :: Prim -> Idris ()

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

327340 = do updateContext (addOperator n ty i def)

src/Idris/REPL.hs+8−8

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

171171-- [pexp t])

172172 (tmpn, tmph) <- liftIO tempfile

173173 liftIO $ hClose tmph

174− compile tmpn tm

174+ compileC tmpn tm

175175 liftIO $ system tmpn

176176 return ()

177177 where fc = FC "(input)" 0

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

268268 liftIO $ system tmpn

269269 return ()

270270 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

277271process 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)

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

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

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

281− compileC f m

281+ compile f m

282282 where fc = FC "main" 0

283283process fn (LogLvl i) = setLogLevel i

284284process 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],

55 x*x + y*y == z*z ]

66

77main : IO ()

8−main = print (pythag 50)

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

99