// -----------------------------------------------------------------------------
// IntAdd is a ripple carry adder for B-complement numbers
// -----------------------------------------------------------------------------

function IntAdd([8]nat x1,x2,[9]nat sum) : [9]nat {
    nat c,g,p,s,i;
    // first perform NatAdd up to the highest digits of x1 and x2
    c = 0;
    for(i=0..6) {
        g,s = x1[i] + x2[i];
        p,sum[i] = s + c;
        c = (nat) ((bool) g | (bool) p);
    }
    // rightmost digits have to be treated differently (namely as int)
    g,s = (nat)((int) x1[7] + (int) x2[7]);
    p,sum[8] = (nat)((int) s + (int) c);
    sum[9] = (nat) ((bool) g | (bool) p);
    return sum;
}


// -----------------------------------------------------------------------------
// a little main thread to test the procedures
// -----------------------------------------------------------------------------

thread test {
    [8]nat a,b;
    [9]nat sm;
    sm = IntAdd(a,b,sm);
}