// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// This file implements the well-known insertion sort procedure. The main idea
// is to sort prefixes x[0..i-1] of the array x[0..N-1] and then store x[i] in
// a separate variable y so that all entries x[j+1..i-1] can be moved one place
// to the right and y can be stored at x[j+1].
//   Note in many textbooks the while loop has condition (j>=0 & x[j]>y) and
// no other code than x[j+1]=y is put after the loop. However, if conjunction
// is commutative (as in MiniC and Quartz unlike in C), then in case of j==0,
// the evaluation of this condition will not stop after j>=0 is seen false,
// and instead also x[j]>y is evaluated which leads to a runtime error.
// ************************************************************************** //

thread InsertionSort {
    [10]nat x;
    nat i,j,y;
    // first create a test array in reverse order
    for(i=0..9) {
        x[i] = 10-i;
    }
    // now apply insertion sort
    for(i=1..9) {
        y = x[i];   // for element x[i], find its place in
        j = i-1;    // already sorted list x[0..i-1]
        while(j>0 & x[j]>y) {
            x[j+1] = x[j];
            j = j-1;
        }
        // now j==0 or x[j]<=y
        if(x[j]>y) {
            // note that this implies j==0
            x[j+1] = x[j];
            x[j] = y;
        } else {
            // here we have x[j]<=y, so that y must be placed at j+1
            x[j+1] = y;
        }
    }
}