Type safe message passing concurrency

CHANGELOG

@@ -9,7 +9,7 @@ User visible changes:
     elaborating their definitions
 * Implicit arguments will be added automatically only if their initial
   letter is lower case, or they are in a using declaration
-* System.Concurrency modules
+* Added System.Concurrency modules
 
 New in 0.9.5:
 -------------

lib/System/Concurrency/Process.idr

@@ -0,0 +1,62 @@
+-- WARNING: No guarantees that this works properly yet! 
+
+module System.Concurrency.Process
+
+import System.Concurrency.Raw
+
+%access public
+
+abstract 
+data ProcID msg = MkPID Ptr
+
+-- Type safe message passing programs. Parameterised over the type of
+-- message which can be send, and the return type.
+
+data Process : (msgType : Set) -> Set -> Set where
+     lift : IO a -> Process msg a
+
+instance Monad (Process msg) where
+     return = lift . return
+     (lift io) >>= k = lift (do x <- io
+                                case k x of
+                                     lift v => v)
+
+run : Process msg x -> IO x
+run (lift prog) = prog
+
+-- Get current process ID
+
+myID : Process msg (ProcID msg)
+myID = lift (return (MkPID prim__vm))
+
+-- Send a message to another process
+
+send : ProcID msg -> msg -> Process msg ()
+send (MkPID p) m = lift (sendToThread p (prim__vm, m))
+
+-- Return whether a message is waiting in the queue
+
+msgWaiting : Process msg Bool
+msgWaiting = lift checkMsgs 
+
+-- Receive a message - blocks if there is no message waiting
+
+recv : Process msg msg
+recv {msg} = do (senderid, m) <- lift get
+                return m
+  where get : IO (Ptr, msg)
+        get = getMsg
+
+-- receive a message, and return with the sender's process ID.
+
+recvWithSender : Process msg (ProcID msg, msg)
+recvWithSender {msg} 
+     = do (senderid, m) <- lift get
+          return (MkPID senderid, m)
+  where get : IO (Ptr, msg)
+        get = getMsg
+
+create : |(thread : Process msg ()) -> Process msg (ProcID msg)
+create (lift p) = do ptr <- lift (fork p)
+                     return (MkPID ptr)
+

lib/System/Concurrency/Raw.idr

@@ -1,3 +1,5 @@
+-- WARNING: No guarantees that this works properly yet! 
+
 module System.Concurrency.Raw
 
 -- Raw (i.e. not type safe) message passing

lib/base.ipkg

@@ -10,7 +10,7 @@ modules = Builtins, Prelude, IO, System,
 
           Network.Cgi,
 
-          System.Concurrency.Raw,
+          System.Concurrency.Raw, System.Concurrency.Process,
 
           Language.Reflection,
 

rts/idris_gc.c

@@ -11,7 +11,7 @@ VAL copy(VM* vm, VAL x) {
     }
     switch(GETTY(x)) {
     case CON:
-        cl = allocCon(vm, x->info.c.arity);
+        cl = allocCon(vm, x->info.c.arity, 1);
         cl->info.c.tag = x->info.c.tag;
         cl->info.c.arity = x->info.c.arity;
 
@@ -23,16 +23,16 @@ VAL copy(VM* vm, VAL x) {
         }
         break;
     case FLOAT:
-        cl = MKFLOAT(vm, x->info.f);
+        cl = MKFLOATc(vm, x->info.f);
         break;
     case STRING:
-        cl = MKSTR(vm, x->info.str);
+        cl = MKSTRc(vm, x->info.str);
         break;
     case BIGINT:
-        cl = MKBIGM(vm, x->info.ptr);
+        cl = MKBIGMc(vm, x->info.ptr);
         break;
     case PTR:
-        cl = MKPTR(vm, x->info.ptr);
+        cl = MKPTRc(vm, x->info.ptr);
         break;
     case FWD:
         return x->info.ptr;
@@ -72,7 +72,7 @@ void cheney(VM *vm) {
     assert(scan == vm->heap_next);
 }
 
-void gc(VM* vm) {
+void idris_gc(VM* vm) {
     // printf("Collecting\n");
 
     char* newheap = malloc(vm -> heap_size);
@@ -108,16 +108,16 @@ void gc(VM* vm) {
         vm->heap_size += vm->heap_growth;
     } 
     vm->oldheap = oldheap;
-
+    
     // gcInfo(vm, 0);
 }
 
-void gcInfo(VM* vm, int doGC) {
+void idris_gcInfo(VM* vm, int doGC) {
     printf("\nStack: %p %p\n", vm->valstack, vm->valstack_top); 
     printf("Total allocations: %d\n", vm->allocations);
     printf("GCs: %d\n", vm->collections);
     printf("Final heap size %d\n", (int)(vm->heap_size));
     printf("Final heap use %d\n", (int)(vm->heap_next - vm->heap));
-    if (doGC) { gc(vm); }
+    if (doGC) { idris_gc(vm); }
     printf("Final heap use after GC %d\n", (int)(vm->heap_next - vm->heap));
 }

rts/idris_gc.h

@@ -3,7 +3,7 @@
 
 #include "idris_rts.h"
 
-void gc(VM* vm);
-void gcInfo(VM* vm, int doGC);
+void idris_gc(VM* vm);
+void idris_gcInfo(VM* vm, int doGC);
 
 #endif

rts/idris_gmp.c

@@ -9,8 +9,9 @@ VAL MKBIGI(int val) {
 
 VAL MKBIGC(VM* vm, char* val) {
     mpz_t* bigint;
-    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));
-    bigint = allocate(vm, sizeof(mpz_t));
+    // FIXME! what if GC happens after cl allocation?
+    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);
+    bigint = allocate(vm, sizeof(mpz_t), 0);
 
     mpz_init(*bigint);
     mpz_set_str(*bigint, val, 10);
@@ -23,8 +24,23 @@ VAL MKBIGC(VM* vm, char* val) {
 
 VAL MKBIGM(VM* vm, void* big) {
     mpz_t* bigint;
-    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));
-    bigint = allocate(vm, sizeof(mpz_t));
+    // FIXME! what if GC happens after cl allocation?
+    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);
+    bigint = allocate(vm, sizeof(mpz_t), 0);
+
+    mpz_init(*bigint);
+    mpz_set(*bigint, *((mpz_t*)big));
+
+    SETTY(cl, BIGINT);
+    cl -> info.ptr = (void*)bigint;
+
+    return cl;
+}
+
+VAL MKBIGMc(VM* vm, void* big) {
+    mpz_t* bigint;
+    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 1);
+    bigint = allocate(vm, sizeof(mpz_t), 1);
 
     mpz_init(*bigint);
     mpz_set(*bigint, *((mpz_t*)big));
@@ -38,8 +54,8 @@ VAL MKBIGM(VM* vm, void* big) {
 VAL GETBIG(VM * vm, VAL x) {
     if (ISINT(x)) {
         mpz_t* bigint;
-        VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));
-        bigint = allocate(vm, sizeof(mpz_t));
+        VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);
+        bigint = allocate(vm, sizeof(mpz_t), 0);
 
         mpz_init(*bigint);
         mpz_set_si(*bigint, GETINT(x));
@@ -55,8 +71,8 @@ VAL GETBIG(VM * vm, VAL x) {
 
 VAL bigAdd(VM* vm, VAL x, VAL y) {
     mpz_t* bigint;
-    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));
-    bigint = allocate(vm, sizeof(mpz_t));
+    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);
+    bigint = allocate(vm, sizeof(mpz_t), 0);
     mpz_add(*bigint, GETMPZ(x), GETMPZ(y));
     SETTY(cl, BIGINT);
     cl -> info.ptr = (void*)bigint;
@@ -65,8 +81,8 @@ VAL bigAdd(VM* vm, VAL x, VAL y) {
 
 VAL bigSub(VM* vm, VAL x, VAL y) {
     mpz_t* bigint;
-    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));
-    bigint = allocate(vm, sizeof(mpz_t));
+    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);
+    bigint = allocate(vm, sizeof(mpz_t), 0);
     mpz_sub(*bigint, GETMPZ(x), GETMPZ(y));
     SETTY(cl, BIGINT);
     cl -> info.ptr = (void*)bigint;
@@ -75,8 +91,8 @@ VAL bigSub(VM* vm, VAL x, VAL y) {
 
 VAL bigMul(VM* vm, VAL x, VAL y) {
     mpz_t* bigint;
-    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));
-    bigint = allocate(vm, sizeof(mpz_t));
+    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);
+    bigint = allocate(vm, sizeof(mpz_t), 0);
     mpz_mul(*bigint, GETMPZ(x), GETMPZ(y));
     SETTY(cl, BIGINT);
     cl -> info.ptr = (void*)bigint;
@@ -85,8 +101,8 @@ VAL bigMul(VM* vm, VAL x, VAL y) {
 
 VAL bigDiv(VM* vm, VAL x, VAL y) {
     mpz_t* bigint;
-    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*));
-    bigint = allocate(vm, sizeof(mpz_t));
+    VAL cl = allocate(vm, sizeof(ClosureType) + sizeof(void*), 0);
+    bigint = allocate(vm, sizeof(mpz_t), 0);
     mpz_div(*bigint, GETMPZ(x), GETMPZ(y));
     SETTY(cl, BIGINT);
     cl -> info.ptr = (void*)bigint;

rts/idris_gmp.h

@@ -4,6 +4,7 @@
 VAL MKBIGI(int val);
 VAL MKBIGC(VM* vm, char* bigint);
 VAL MKBIGM(VM* vm, void* bigint);
+VAL MKBIGMc(VM* vm, void* bigint);
 
 VAL idris_bigPlus(VM*, VAL x, VAL y);
 VAL idris_bigMinus(VM*, VAL x, VAL y);

rts/idris_main.c

@@ -3,7 +3,7 @@ int main(int argc, char* argv[]) {
     _idris__123_runMain0_125_(vm, NULL);
     //_idris_main(vm, NULL);
 #ifdef IDRIS_TRACE
-    gcInfo(vm, 1);
+    idris_gcInfo(vm, 1);
 #endif
     terminate(vm);
 }

rts/idris_rts.c

@@ -37,15 +37,18 @@ VM* init_vm(int stack_size, size_t heap_size,
     vm->reg1 = NULL;
 
     vm->inbox = malloc(1024*sizeof(VAL));
+    memset(vm->inbox, 0, 1024*sizeof(VAL));
     vm->inbox_end = vm->inbox + 1024;
     vm->inbox_ptr = vm->inbox;
     vm->inbox_write = vm->inbox;
 
     pthread_mutex_init(&(vm->inbox_lock), NULL);
     pthread_mutex_init(&(vm->inbox_block), NULL);
+    pthread_mutex_init(&(vm->alloc_lock), NULL);
     pthread_cond_init(&(vm->inbox_waiting), NULL);
 
     vm->max_threads = max_threads;
+    vm->processes = 0;
 
     int i;
     // Assumption: there's enough space for this in the initial heap.
@@ -73,8 +76,14 @@ void terminate(VM* vm) {
     free(vm);
 }
 
-void* allocate(VM* vm, size_t size) {
+void* allocate(VM* vm, size_t size, int outerlock) {
 //    return malloc(size);
+    int lock = vm->processes > 0 && !outerlock;
+
+    if (lock) { // not message passing
+       pthread_mutex_lock(&vm->alloc_lock); 
+    }
+
     if ((size & 7)!=0) {
 	size = 8 + ((size >> 3) << 3);
     }
@@ -84,15 +93,23 @@ void* allocate(VM* vm, size_t size) {
         *((size_t*)(vm->heap_next)) = size + sizeof(size_t);
         vm -> heap_next += size + sizeof(size_t);
         memset(ptr, 0, size);
+        if (lock) { // not message passing
+           pthread_mutex_unlock(&vm->alloc_lock); 
+        }
         return ptr;
     } else {
-        gc(vm);
-        return allocate(vm, size);
+        idris_gc(vm);
+        if (lock) { // not message passing
+           pthread_mutex_unlock(&vm->alloc_lock); 
+        }
+        return allocate(vm, size, 0);
     }
+
 }
 
-void* allocCon(VM* vm, int arity) {
-    Closure* cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*arity);
+void* allocCon(VM* vm, int arity, int outer) {
+    Closure* cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*arity,
+                               outer);
     SETTY(cl, CON);
     if (arity == 0) {
        cl -> info.c.args = NULL;
@@ -106,7 +123,7 @@ void* allocCon(VM* vm, int arity) {
 }
 
 VAL MKFLOAT(VM* vm, double val) {
-    Closure* cl = allocate(vm, sizeof(Closure));
+    Closure* cl = allocate(vm, sizeof(Closure), 0);
     SETTY(cl, FLOAT);
     cl -> info.f = val;
     return cl;
@@ -114,7 +131,7 @@ VAL MKFLOAT(VM* vm, double val) {
 
 VAL MKSTR(VM* vm, char* str) {
     Closure* cl = allocate(vm, sizeof(Closure) + // Type) + sizeof(char*) +
-                               sizeof(char)*strlen(str)+1);
+                               sizeof(char)*strlen(str)+1, 0);
     SETTY(cl, STRING);
     cl -> info.str = (char*)cl + sizeof(Closure);
 
@@ -123,7 +140,31 @@ VAL MKSTR(VM* vm, char* str) {
 }
 
 VAL MKPTR(VM* vm, void* ptr) {
-    Closure* cl = allocate(vm, sizeof(Closure));
+    Closure* cl = allocate(vm, sizeof(Closure), 0);
+    SETTY(cl, PTR);
+    cl -> info.ptr = ptr;
+    return cl;
+}
+
+VAL MKFLOATc(VM* vm, double val) {
+    Closure* cl = allocate(vm, sizeof(Closure), 1);
+    SETTY(cl, FLOAT);
+    cl -> info.f = val;
+    return cl;
+}
+
+VAL MKSTRc(VM* vm, char* str) {
+    Closure* cl = allocate(vm, sizeof(Closure) + // Type) + sizeof(char*) +
+                               sizeof(char)*strlen(str)+1, 1);
+    SETTY(cl, STRING);
+    cl -> info.str = (char*)cl + sizeof(Closure);
+
+    strcpy(cl -> info.str, str);
+    return cl;
+}
+
+VAL MKPTRc(VM* vm, void* ptr) {
+    Closure* cl = allocate(vm, sizeof(Closure), 1);
     SETTY(cl, PTR);
     cl -> info.ptr = ptr;
     return cl;
@@ -211,7 +252,7 @@ void dumpVal(VAL v) {
 }
 
 VAL idris_castIntStr(VM* vm, VAL i) {
-    Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16);
+    Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16, 0);
     SETTY(cl, STRING);
     cl -> info.str = (char*)cl + sizeof(Closure);
     sprintf(cl -> info.str, "%d", (int)(GETINT(i)));
@@ -228,7 +269,7 @@ VAL idris_castStrInt(VM* vm, VAL i) {
 }
 
 VAL idris_castFloatStr(VM* vm, VAL i) {
-    Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*32);
+    Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*32, 0);
     SETTY(cl, STRING);
     cl -> info.str = (char*)cl + sizeof(Closure);
     sprintf(cl -> info.str, "%g", GETFLOAT(i));
@@ -244,7 +285,8 @@ VAL idris_concat(VM* vm, VAL l, VAL r) {
     char *ls = GETSTR(l);
     // dumpVal(l);
     // printf("\n");
-    Closure* cl = allocate(vm, sizeof(Closure) + strlen(ls) + strlen(rs) + 1);
+    Closure* cl = allocate(vm, sizeof(Closure) + strlen(ls) + strlen(rs) + 1,
+                               0);
     SETTY(cl, STRING);
     cl -> info.str = (char*)cl + sizeof(Closure);
     strcpy(cl -> info.str, ls);
@@ -319,7 +361,7 @@ VAL idris_strTail(VM* vm, VAL str) {
 VAL idris_strCons(VM* vm, VAL x, VAL xs) {
     char *xstr = GETSTR(xs);
     Closure* cl = allocate(vm, sizeof(Closure) +
-                               strlen(xstr) + 2);
+                               strlen(xstr) + 2, 0);
     SETTY(cl, STRING);
     cl -> info.str = (char*)cl + sizeof(Closure);
     cl -> info.str[0] = (char)(GETINT(x));
@@ -334,7 +376,7 @@ VAL idris_strIndex(VM* vm, VAL str, VAL i) {
 VAL idris_strRev(VM* vm, VAL str) {
     char *xstr = GETSTR(str);
     Closure* cl = allocate(vm, sizeof(Closure) +
-                               strlen(xstr) + 1);
+                               strlen(xstr) + 1, 0);
     SETTY(cl, STRING);
     cl -> info.str = (char*)cl + sizeof(Closure);
     int y = 0;
@@ -348,7 +390,8 @@ VAL idris_strRev(VM* vm, VAL str) {
 }
 
 typedef struct {
-    VM* vm;
+    VM* vm; // thread's VM
+    VM* callvm; // calling thread's VM
     func fn;
     VAL arg;
 } ThreadData;
@@ -356,13 +399,16 @@ typedef struct {
 void* runThread(void* arg) {
     ThreadData* td = (ThreadData*)arg;
     VM* vm = td->vm;
+    VM* callvm = td->callvm;
 
     TOP(0) = td->arg;
     BASETOP(0);
     ADDTOP(1);
     td->fn(vm, NULL);
+    callvm->processes--;
 
     free(td);
+    terminate(vm);
     return NULL;
 }
 
@@ -370,6 +416,7 @@ void* vmThread(VM* callvm, func f, VAL arg) {
     VM* vm = init_vm(callvm->stack_max - callvm->valstack, callvm->heap_size, 
                      callvm->max_threads,
                      0, NULL);
+    vm->processes=1; // since it can send and receive messages
     pthread_t t;
     pthread_attr_t attr;
 //    size_t stacksize;
@@ -380,16 +427,18 @@ void* vmThread(VM* callvm, func f, VAL arg) {
 
     ThreadData *td = malloc(sizeof(ThreadData));
     td->vm = vm;
+    td->callvm = callvm;
     td->fn = f;
     td->arg = copyTo(vm, arg);
+    
+    callvm->processes++;
 
     pthread_create(&t, &attr, runThread, td);
 //    usleep(100);
     return vm;
 }
 
-// VM is assumed to be a different vm from the one x lives on (so we don't need
-// to worry about gc moving things, as the VM x is on will not be allocating)
+// VM is assumed to be a different vm from the one x lives on 
 
 VAL copyTo(VM* vm, VAL x) {
     int i;
@@ -400,7 +449,7 @@ VAL copyTo(VM* vm, VAL x) {
     }
     switch(GETTY(x)) {
     case CON:
-        cl = allocCon(vm, x->info.c.arity);
+        cl = allocCon(vm, x->info.c.arity, 1);
         cl->info.c.tag = x->info.c.tag;
         cl->info.c.arity = x->info.c.arity;
 
@@ -411,16 +460,16 @@ VAL copyTo(VM* vm, VAL x) {
         }
         break;
     case FLOAT:
-        cl = MKFLOAT(vm, x->info.f);
+        cl = MKFLOATc(vm, x->info.f);
         break;
     case STRING:
-        cl = MKSTR(vm, x->info.str);
+        cl = MKSTRc(vm, x->info.str);
         break;
     case BIGINT:
-        cl = MKBIGM(vm, x->info.ptr);
+        cl = MKBIGMc(vm, x->info.ptr);
         break;
     case PTR:
-        cl = MKPTR(vm, x->info.ptr);
+        cl = MKPTRc(vm, x->info.ptr);
         break;
     default:
         assert(0); // We're in trouble if this happens...
@@ -433,12 +482,26 @@ void idris_sendMessage(VM* sender, VM* dest, VAL msg) {
     // FIXME: If GC kicks in in the middle of the copy, we're in trouble.
     // Probably best check there is enough room in advance. (How?)
 
+    // Also a problem if we're allocating at the same time as the 
+    // destination thread (which is very likely)
+    // Should the inbox be a different memory space?
+    
+    // So: we try to copy, if a collection happens, we do the copy again
+    // under the assumption there's enough space this time.
+
+    int gcs = dest->collections;
+    pthread_mutex_lock(&dest->alloc_lock); 
     VAL dmsg = copyTo(dest, msg);
+    pthread_mutex_unlock(&dest->alloc_lock); 
 
+    if (dest->collections>gcs) {
+        // a collection will have invalidated the copy
+        pthread_mutex_lock(&dest->alloc_lock); 
+        dmsg = copyTo(dest, msg); // try again now there's room...
+        pthread_mutex_unlock(&dest->alloc_lock); 
+    }
 
-//    printf("Sending [lock]...\n");
     pthread_mutex_lock(&(dest->inbox_lock));
-
     *(dest->inbox_write) = dmsg;
    
     dest->inbox_write++;

rts/idris_rts.h

@@ -51,6 +51,7 @@ typedef struct {
    
     pthread_mutex_t inbox_lock;
     pthread_mutex_t inbox_block;
+    pthread_mutex_t alloc_lock;
     pthread_cond_t inbox_waiting;
 
     VAL* inbox; // Block of memory for storing messages
@@ -59,6 +60,7 @@ typedef struct {
     VAL* inbox_ptr; // Next message to read
     VAL* inbox_write; // Location of next message to write
 
+    int processes; // Number of child processes
     int max_threads; // maximum number of threads to run in parallel
 
     int argc;
@@ -140,6 +142,11 @@ VAL MKFLOAT(VM* vm, double val);
 VAL MKSTR(VM* vm, char* str);
 VAL MKPTR(VM* vm, void* ptr);
 
+// following versions don't take a lock when allocating
+VAL MKFLOATc(VM* vm, double val);
+VAL MKSTRc(VM* vm, char* str);
+VAL MKPTRc(VM* vm, void* ptr);
+
 VAL MKCON(VM* vm, VAL cl, int tag, int arity, ...);
 
 #define SETTAG(x, a) (x)->info.c.tag = (a)
@@ -149,8 +156,8 @@ VAL MKCON(VM* vm, VAL cl, int tag, int arity, ...);
 void PROJECT(VM* vm, VAL r, int loc, int arity); 
 void SLIDE(VM* vm, int args);
 
-void* allocate(VM* vm, size_t size);
-void* allocCon(VM* vm, int arity);
+void* allocate(VM* vm, size_t size, int outerlock);
+void* allocCon(VM* vm, int arity, int outerlock);
 
 void* vmThread(VM* callvm, func f, VAL arg);
 

src/Core/CaseTree.hs

@@ -58,18 +58,18 @@ type Clause   = ([Pat], (Term, Term))
 type CS = ([Term], Int)
 
 instance TermSize SC where
-    termsize (Case n as) = termsize as
-    termsize (STerm t) = termsize t
-    termsize _ = 1
+    termsize n (Case n' as) = termsize n as
+    termsize n (STerm t) = termsize n t
+    termsize n _ = 1
 
 instance TermSize CaseAlt where
-    termsize (ConCase _ _ _ s) = termsize s
-    termsize (ConstCase _ s) = termsize s
-    termsize (DefaultCase s) = termsize s
+    termsize n (ConCase _ _ _ s) = termsize n s
+    termsize n (ConstCase _ s) = termsize n s
+    termsize n (DefaultCase s) = termsize n s
 
 -- simple terms can be inlined trivially - good for primitives in particular
-small :: SC -> Bool
-small t = False -- termsize t < 150
+small :: Name -> SC -> Bool
+small n t = False -- termsize n t < 10
 
 namesUsed :: SC -> [Name]
 namesUsed sc = nub $ nu' [] sc where

src/Core/Evaluate.hs

@@ -707,7 +707,7 @@ addCasedef n alwaysInline tcase covering ps_in ps psrt ty uctxt
           ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps, 
                         simpleCase tcase covering RunTime (FC "" 0) psrt) of
                     (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) -> 
-                       let inl = alwaysInline || small sc' in
+                       let inl = alwaysInline || small n sc' in
                            addDef n (CaseOp inl ty ps_in ps args sc args' sc',
                                       access, Unchecked) ctxt in
           uctxt { definitions = ctxt' }

src/Core/TT.hs

@@ -434,18 +434,22 @@ deriving instance Binary TT
 !-}
 
 class TermSize a where
-  termsize :: a -> Int
+  termsize :: Name -> a -> Int
 
 instance TermSize a => TermSize [a] where
-    termsize [] = 0
-    termsize (x : xs) = termsize x + termsize xs
+    termsize n [] = 0
+    termsize n (x : xs) = termsize n x + termsize n xs
 
-instance TermSize (TT a) where
-    termsize (P _ _ _) = 1
-    termsize (V _) = 1
-    termsize (Bind n (Let t v) sc) = termsize v + termsize sc
-    termsize (App f a) = termsize f + termsize a
-    termsize _ = 1
+instance TermSize (TT Name) where
+    termsize n (P _ x _) 
+       | x == n = 1000000 -- recursive => really big
+       | otherwise = 1
+    termsize n (V _) = 1
+    termsize n (Bind n' (Let t v) sc) 
+       = let rn = if n == n' then MN 0 "noname" else n in
+             termsize rn v + termsize rn sc
+    termsize n (App f a) = termsize n f + termsize n a
+    termsize n _ = 1
 
 instance Sized a => Sized (TT a) where
   size (P name n trm) = 1 + size name + size n + size trm

src/IRTS/CodegenC.hs

@@ -100,7 +100,7 @@ bcc i (ASSIGNCONST l c)
     mkConst _ = "MKINT(42424242)"
 bcc i (MKCON l tag args)
     = indent i ++ creg Tmp ++ " = allocCon(vm, " ++ show (length args) ++ 
-         "); " ++ "SETTAG(" ++ creg Tmp ++ ", " ++ show tag ++ ");\n" ++
+         ", 0); " ++ "SETTAG(" ++ creg Tmp ++ ", " ++ show tag ++ ");\n" ++
       indent i ++ setArgs 0 args ++ "\n" ++ 
       indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
          

test/test018/expected

@@ -13,3 +13,503 @@ Hello!
 Received
 Hello to you too!
 Finished
+100
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+99
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+98
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+97
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+96
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+95
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+94
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+93
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+92
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+91
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+90
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+89
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+88
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+87
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+86
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+85
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+84
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+83
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+82
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+81
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+80
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+79
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+78
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+77
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+76
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+75
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+74
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+73
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+72
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+71
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+70
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+69
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+68
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+67
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+66
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+65
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+64
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+63
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+62
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+61
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+60
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+59
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+58
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+57
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+56
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+55
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+54
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+53
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+52
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+51
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+50
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+49
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+48
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+47
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+46
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+45
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+44
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+43
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+42
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+41
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+40
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+39
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+38
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+37
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+36
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+35
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+34
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+33
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+32
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+31
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+30
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+29
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+28
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+27
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+26
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+25
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+24
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+23
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+22
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+21
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+20
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+19
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+18
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+17
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+16
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+15
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+14
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+13
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+12
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+11
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+10
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+9
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+8
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+7
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+6
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+5
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+4
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+3
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+2
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!
+1
+Waiting for message
+Sent ping
+Received Hello!
+Reply: Hello back!

test/test018/run

@@ -1,4 +1,6 @@
 #!/bin/bash
 idris test018.idr -o test018
+idris test018a.idr -o test018a
 ./test018
-rm -f test018 *.ibc
+./test018a
+rm -f test018 test018a *.ibc