// ************************************************************************** //
//                                                                            //
//    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 module implements an algorithm for evaluation of expression trees that//
// runs in time O(log(N)) for expression trees with O(N) leaf nodes. The      //
// algorithm is based on tree contraction that is based on the SHUNT operation//
// as described in [KaRa88,Meta97]. Expressions may consist of constants and  //
// addition and multiplication operations of a ring.                          //
// Expressions are stored as arrays of tuples having the following components://
// (opc,parent,sibling,val,isLeft,a,b,bsy) with the following meaning:        //
//  * opc indicates either the root node, a constant value CST or an operation//
//  * parent is the index of the parent node                                  //
//  * sibling is the index of the sibling node                                //
//  * val is the value of a leaf which must have opcode opc=CST               //
//  * isLeft: if opc=CST holds, then this indicates whether its a left leaf   //
//  * a,b are integers that specify the meaning of the expression so that if  //
//    the expression is recursively evaluated to a value v, the the value is  //
//    a*v+b                                                                   //
// In addition to the expression tree, the algorithm requires also an array   //
// that contains the indices of the leaf nodes from left to right.            //
// ************************************************************************** //


// the following are components of a node in the expression tree:
macro opc     = 0;  // indicates the operation associated with this node
macro parent  = 1;  // index of the parent node in the expression array
macro sibling = 2;  // index of the sibling in the expression array
macro val     = 3;  // value of a constant (if opc indicates a constant)
macro isLeft  = 4;  // if opc=CST holds, then this indicates whether its a left leaf
macro a       = 5;  // value a of a pair (a,b) labeling a partially evaluated edge 
macro b       = 6;  // value b of a pair (a,b) labeling a partially evaluated edge
macro bsy     = 7;  // boolean value bsy indicating whether node is in use

// the following are possible op-codes
macro OpNo = 4;     // number of different operations
macro ROOT = 0;     // tag indicating the root node
macro CST  = 1;     // tag indicating constants
macro ADD  = 2;     // tag indicating addition
macro MUL  = 3;     // tag indicating multiplication

macro N = 20;       // number of possible expression nodes
macro L =  8;       // number of possible leaves of the expression


module EvalRingExpr([N](nat{OpNo} * nat{N} * nat{N} * int * bool * int * int * bool) ?e, 
                    [L]nat{N} ?lf,
                    int !y,event !rdy) {
    [N](nat{OpNo} * nat{N} * nat{N} * int * bool * int * int * bool) expr; 
    [L]nat{N} leaf;  // list of leafs
    
    // copy the inputs to local variables that can be read and written
    for(i=0..N-1) expr[i] = e[i];
    for(i=0..L-1) leaf[i] = lf[i];

    // the following loops perform the evaluation in time O(log(L))
    for(i=0..log(L)-1) {
        // the two iterations of the next loop eliminate the leafs with even index
        // that are left/right operands of their parent node 
        for(shuntLeft=0..1) {
            // the next loop enumerates all leafs with even index and eliminates
            // those that are left/right operands depending on shuntLeft
            for(j=0..(L-1)/exp(2,i+1)) {
                let(lj = leaf[2*j])
                let(l = expr[lj])
                // Eliminate (shunt) leaf nodes with even indices in alternating rounds where
                // in one round either left or right operand leafs are eliminated
                // thus, the number of leafs is divided by two after two rounds
                if(lj!=0 & l.bsy & ((shuntLeft==0) <-> l.isLeft)) {
                    let(a1 = l.a)
                    let(b1 = l.b)
                    let(a2 = expr[l.sibling].a)
                    let(b2 = expr[l.sibling].b)
                    let(a3 = expr[l.parent].a)
                    let(b3 = expr[l.parent].b)
                    let(x  = l.val) {
                        next(l.bsy) = false;               // delete leaf l
                        next(expr[l.parent].bsy) = false;  // delete parent of leaf l
                        next(expr[l.sibling].parent)  = expr[l.parent].parent;
                        next(expr[l.sibling].sibling) = expr[l.parent].sibling;
                        next(expr[l.sibling].isLeft)  = !expr[expr[l.parent].sibling].isLeft;
                        next(expr[expr[l.parent].sibling].sibling) = l.sibling;
                        if (expr[l.parent].opc==ADD) {
                            next(expr[l.sibling].a) = a2 * a3;
                            next(expr[l.sibling].b) = b3 + a3 * (a1 * x + b1 + b2);
                        } else {
                            next(expr[l.sibling].a) = a2 * a3 * (a1 * x + b1);
                            next(expr[l.sibling].b) = b3 + a3 * b2 * (a1 * x + b1);
                        }
                    }
                }
            }   
            // if all leafs with even indices have been eliminated, we relabel the remaining
            // leafs on the odd indices so that leafs are again enumerated from 0..L/exp(2,i)
            if(shuntLeft==1) 
                for(j=0..(L/exp(2,i+1))-1)
                    next(leaf[j]) = leaf[2*j+1];
            pause;
        }
    }
    // finally, one leaf is left
    let(root = expr[leaf[0]])
    y = root.val * root.a + root.b;
    emit(rdy);
}
drivenby LeftSpine {
    int va,vb,vc,vd,ve,vf,vg,vh;
    // The assignments below encode the following expression tree:
    //
    //      [1]  [3]  [5]  [7]  [9]  [11] [13] 
    //    <- * <- + <- * <- + <- * <- + <- * <- 8 [15] <7>
    //       ^    ^    ^    ^    ^    ^    ^    
    //       |    |    |    |    |    |    |    
    //       1    2    3    4    5    6    7    
    //      [2]  [4]  [6]  [8] [10] [12] [14]
    //      <0>  <1>  <2>  <3> <4>  <5>  <6>
    //
    // where all edges are labelled with (a,b)=(1,0) and where the numbers
    // in square brackets are the indices in the expr array and the numbers
    // in brackets <> denote the indices in the leaf array. The first round
    // of SHUNT operations should reduce this tree to the following one:
    // 
    //     (1,0) [3] (3,0) [7] (5,0) [11] (7,0) 
    //    <------ + <------ + <------ + <------- 8 [15] <3>
    //            ^         ^         ^ 
    //            |(1,0)    |(1,0)    |(1,0)
    //            2         4         6
    //           [4]       [8]       [12]
    //           <0>       <1>       <2>
    // 
    // next, we obtain:
    //
    //     (3,2) [7]  (35,30) 
    //    <------ + <-------- 8 [15] <1>
    //            ^  
    //            |(1,0)
    //            4
    //           [8]
    //           <0>
    // 
    // and finally:
    //
    //     (105,104) 
    //    <--------- 8 [15] <0>

    va = 1;
    vb = 2;
    vc = 3;
    vd = 4;
    ve = 5;
    vf = 6;
    vg = 7;
    vh = 8;
    // syntax tree of 1*(2+3*(4+5*(6+7*8)))
     e[0] = (ROOT, 0, 0,00,false,1,0,true);
     e[1] = (MUL, 0, 0,00,false,1,0,true);
     e[2] = (CST, 1, 3,va,true, 1,0,true);
     e[3] = (ADD, 1, 2,00,false,1,0,true);
     e[4] = (CST, 3, 5,vb,true, 1,0,true);
     e[5] = (MUL, 3, 4,00,false,1,0,true);
     e[6] = (CST, 5, 7,vc,true, 1,0,true);
     e[7] = (ADD, 5, 6,00,false,1,0,true);
     e[8] = (CST, 7, 9,vd,true, 1,0,true);
     e[9] = (MUL, 7, 8,00,false,1,0,true);
    e[10] = (CST, 9,11,ve,true, 1,0,true);
    e[11] = (ADD, 9,10,00,false,1,0,true);
    e[12] = (CST,11,13,vf,true, 1,0,true);
    e[13] = (MUL,11,12,00,false,1,0,true);
    e[14] = (CST,13,15,vg,true, 1,0,true);
    e[15] = (CST,13,14,vh,false,1,0,true);
    // operand leafs
    lf[0] = 2;
    lf[1] = 4;
    lf[2] = 6;
    lf[3] = 8;
    lf[4] = 10;
    lf[5] = 12;
    lf[6] = 14;
    lf[7] = 15;
    await(rdy);
    assert(y==944);
}
drivenby RightSpine {
    int va,vb,vc,vd,ve,vf,vg,vh;
    // The assignments below encode the following expression tree:
    //
    //      <7>  <6>  <5>  <4> <3>  <2>  <1>
    //      [2]  [4]  [6]  [8] [10] [12] [14]
    //       1    2    3    4    5    6    7    
    //       |    |    |    |    |    |    |    
    //       v    v    v    v    v    v    v    
    //    <- * <- + <- * <- + <- * <- + <- * <- 8 [15] <0>
    //      [1]  [3]  [5]  [7]  [9]  [11] [13] 
    //
    // where all edges are labelled with (a,b)=(1,0) and where the numbers
    // in square brackets are the indices in the expr array and the numbers
    // in brackets <> denote the indices in the leaf array. The reduction
    // is as follows:
    //
    //      <7>  <6>  <5>  <4> <3>  <2>
    //      [2]  [4]  [6]  [8] [10] [12]
    //       1    2    3    4    5    6   
    //       |    |    |    |    |    |   
    //       v    v    v    v    v    v  (8,0)
    //    <- * <- + <- * <- + <- * <- + <------ 7 [14] <1>
    //      [1]  [3]  [5]  [7]  [9]  [11] 
    //
    //
    //      <3>       <2>       <1> 
    //      [2]       [6]       [10]
    //       1         3         5   
    //       |         |         |
    //       v  (1,2)  v  (5,6)  v  (8,6)     
    //    <- * <------ * <------ * <------ 7 [14] <0>
    //      [1]       [5]       [9] 
    //
    //
    //      <3>       <2>
    //      [2]       [6]
    //       1         3   
    //       |         |
    //       v  (1,2)  v  (62,4)     
    //    <- * <------ * <------ 5 [10] <1>
    //      [1]       [5]
    //
    //
    //      <1>
    //      [2]
    //       1 
    //       | 
    //       v  (186,14)     
    //    <- * <--------- 5 [10] <0>
    //      [1]
    //
    //
    //      (944,0)     
    //    <--------- 1 [2] <1>
    //
    va = 1;
    vb = 2;
    vc = 3;
    vd = 4;
    ve = 5;
    vf = 6;
    vg = 7;
    vh = 8;
    // syntax tree of (((7*8+6)*5+4)*3)+2
     e[0] = (ROOT,0, 0,00,false,1,0,true);
     e[1] = (MUL, 0, 0,00,false,1,0,true);
     e[2] = (CST, 1, 3,va,false,1,0,true);
     e[3] = (ADD, 1, 2,00,false,1,0,true);
     e[4] = (CST, 3, 5,vb,false,1,0,true);
     e[5] = (MUL, 3, 4,00,false,1,0,true);
     e[6] = (CST, 5, 7,vc,false,1,0,true);
     e[7] = (ADD, 5, 6,00,false,1,0,true);
     e[8] = (CST, 7, 9,vd,false,1,0,true);
     e[9] = (MUL, 7, 8,00,false,1,0,true);
    e[10] = (CST, 9,11,ve,false,1,0,true);
    e[11] = (ADD, 9,10,00,false,1,0,true);
    e[12] = (CST,11,13,vf,false,1,0,true);
    e[13] = (MUL,11,12,00,false,1,0,true);
    e[14] = (CST,13,15,vg,false,1,0,true);
    e[15] = (CST,13,14,vh,true, 1,0,true);
    // operand leafs
    lf[0] = 15;
    lf[1] = 14;
    lf[2] = 12;
    lf[3] = 10;
    lf[4] = 8;
    lf[5] = 6;
    lf[6] = 4;
    lf[7] = 2;
    await(rdy);
    assert(y==944);
}
drivenby TreeExpr {
    int va,vb,vc,vd,ve,vf,vg,vh;
    va = 2;
    vb = 3;
    vc = 4;
    vd = 5;
    ve = 6;
    vf = 7;
    vg = 8;
    vh = 9;
    // syntax tree of (2+3*4)*(5*6+7*(8+9))
     e[0] = (ROOT,0, 0,00,false,1,0,true);
     e[1] = (MUL, 0, 0,00,false,1,0,true);
     e[2] = (ADD, 1, 7,00,false,1,0,true);
     e[3] = (CST, 2, 4,va,true, 1,0,true);
     e[4] = (MUL, 2, 3,00,false,1,0,true);
     e[5] = (CST, 4, 6,vb,true, 1,0,true);
     e[6] = (CST, 4, 5,vc,false,1,0,true);
     e[7] = (ADD, 1, 2,00,false,1,0,true);
     e[8] = (MUL, 7,11,00,false,1,0,true);
     e[9] = (CST, 8,10,vd,true, 1,0,true);
    e[10] = (CST, 8, 9,ve,false,1,0,true);
    e[11] = (MUL, 7, 8,00,false,1,0,true);
    e[12] = (CST,11,13,vf,true, 1,0,true);
    e[13] = (ADD,11,12,00,false,1,0,true);
    e[14] = (CST,13,15,vg,true, 1,0,true);
    e[15] = (CST,13,14,vh,false,1,0,true);
    // operand leafs
    lf[0] = 3;
    lf[1] = 5;
    lf[2] = 6;
    lf[3] = 9;
    lf[4] = 10;
    lf[5] = 12;
    lf[6] = 14;
    lf[7] = 15;
    await(rdy);
    assert(y==2086);
}