// ************************************************************************** //
//                                                                            //
//    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 Quartz file can be used to test the parser and type-checker for tools //
// using the Quartz language.                                                 //
// ************************************************************************** //

macro minmax(x,y) = ((x<y)?(x,y):(y,x));

module Expressions(
    bool   xbl,ybl,zbl,
    bv{1}  xbv1,ybv1,zbv1,
    bv{4}  xbv4,ybv4,zbv4,
    bv{12} xbv,ybv,zbv,
    nat{4} xn4,yn4,zn4,
    int{4} xi4,yi4,zi4,
    nat    xn,yn,zn,
    int    xi,yi,zi,
    real   xr,yr,zr,
    (int * int) t,
    [4]bool xa
) {

    // ---- boolean constants
    xbl = instant;
    xbl = inside;
    xbl = terminate;
    xbl = true;
    xbl = false;

    xbv1 = true;
    xbv1 = xbl;

    // ---- bitvector constants
    xbv = 0b101011110000;
    xbv = 0o1752;
    xbv = 0xAFD;

    // ---- nat constants
    xn = 3;
    
    // ---- int constants
    xi = 3;
    xi = +3;
    xi = -3;
    
    // ---- real constants
    xr =  0.23;
    xr = +0.23;
    xr = -424.43243;
    xr =  3213.4324e-12;
    xr =  3213.4324e+12;
    xr = +3213.4324e-12;
    xr = +3213.4324e+12;
    xr = -3213.4324e-12;
    xr = -3213.4324e+12;
    
    // ---- (bitwise) boolean boperators
    zbl = !ybl;
    zbl = xbl & ybl;
    zbl = xbl | ybl;
    zbl = xbl -> ybl;
    zbl = xbl <-> ybl;

    zbv = !ybv;
    zbv = xbv & ybv;
    zbv = xbv | ybv;
    zbv = xbv -> ybv;
    zbv = xbv <-> ybv;

    zbv1 = !ybl;
    zbv1 = xbv1 & ybl;
    zbv1 = xbv1 | ybl;
    zbv1 = xbv1 -> ybl;
    zbv1 = xbv1 <-> ybl;

    zbl = !ybl;
    zbl = xbv1 & ybl;
    zbl = xbv1 | ybl;
    zbl = xbv1 -> ybl;
    zbl = xbv1 <-> ybl;
    
    // ---- equalities and inequalities
    zbl = (xbl == ybl);
    zbl = (xbv == ybv);
    zbl = (xbl == ybv1);
    zbl = (xn == yn);
    zbl = (xi == yi);
    zbl = (xi == yn);
    zbl = (xr == yr);

    zbl = (xbl != ybl);
    zbl = (xbv != ybv);
    zbl = (xbl != ybv1);
    zbl = (xn != yn);
    zbl = (xi != yi);
    zbl = (xi != yn);
    zbl = (xr != yr);

    // ---- arithmetic operators
    zn = xn + yn;
    zn = xn - yn;
    zn = xn * yn;
    zn = xn / yn;
    zn = xn % yn;

    zi = xi + yi;
    zi = xi - yi;
    zi = xi * yi;
    zi = xi / yi;
    zi = xi % yi;
    
    zi = xn + yi;
    zi = xn - yi;
    zi = xn * yi;
    zi = xn / yi;
    zi = xn % yi;

    zi = xi + yn;
    zi = xi - yn;
    zi = xi * yn;
    zi = xi / yn;
    zi = xi % yn;
    
    // ---- special arithmetic operators
    zn = abs(xi);
    zn = sat{3}(xn);
    // zi = sat{4}(xi+yi);

    // ---- bitvector operators
    zbl = xbv{2};                // bit access
    zbv = xbv4@ybv4@zbv4;        // bitvector append
    zbv4 = xbv{5:2};             // bitvector segment extraction
    zbv4 = xbv{-2:7};            // bitvector segment extraction
    zbv4 = xbv{-2:-5};           // bitvector segment extraction
    zbv4 = xbv{10:-5};           // bitvector segment extraction
    zbv = reverse(xbv);          // reverse of bitvector
    zbv4 = {xbl::4};             // replicating a boolean
    
    // ---- tuple expressions
    t = minmax(xn,yn);
    t = (t.1,t.0);
    t.1 = xn+yn;
    xn = t.1 + t.0 + (minmax(xn,yn)).0;
    t = (xn,yn);
    
    //  ------- explicit type converters --------------------------
    zbv1 = xbl;                          // bool2bv is inserted by type-checker
    zbv4 = nat2bv(xn4,2)@nat2bv(yn4,2);
    zbv4 = int2bv(xn4,3)@xbl;
    zbv4 = arr2bv(xa);
    zbv4 = tup2bv((xbl,ybl,zbl,xbl));    // tup2bv required double delimiters
    zn4  = bv2nat(xbv4);                  // generates assertion bv2nat(xbv4)<4
    zi4  = bv2int(xbv4);                  // generates assertion bv2int(xbv4)<4 & -4<=bv2int(xbv4)
    zn4  = bv2int(xbv4);                  // generates assertion bv2int(xbv4)<4 & 0<=bv2int(xbv4)
    zr   = nat2real(xn);
    zr   = int2real(xi);

    //  ------- special real-expressions --------------------------
    zr = cos(xr) + sin(yr);
    zr = exp(xr,yr);
    zr = log(xr);
    zr = drv(yr);

}