union <'a> list with nat {
 Nil(0);
 {n:nat} Cons(n+1) of 'a * <'a> list(n)
}

{n:nat}
float
list_vec_mult (xs: <[i:int | 0 <= i < n] (int(i) * float)> list, vec[n]: float) {
  var: int i; float f, sum;;

  sum = 0.0;

  invariant: (xs: <[i:int | 0 <= i < n] (int(i) * float)> list)
  while (true) {
    switch (xs) {
      case Nil: return sum;
      case Cons((i, f), xs): sum = sum +. f *. vec[i];      
    }
  }
  exit;    
}

/*

union natural with nat {
 Z(0);
 {a:nat} S(a+1) of natural(a)
}

global x: int = 0

unit inc () {
  x = x + 1;
}

{m:nat,n:nat}
int(min(m,n)) min(x:natural(m), y:natural(n)) {
  switch (x, y) {
    case (S(x), S(y)): return 1+min(x,y);
  }
}

('a){m:nat,n:nat}
<'a> list(m+n) append (xs: <'a> list(m), ys: <'a> list(n)) {
   var: 'a x;;
 
   switch (xs) {
     case Nil: return ys;
     case Cons(x, xs): return Cons(x, append(xs, ys));
   }
}

('a){n:nat}
[i:nat] <'a> list(i) flatten (xss: <[i:nat] <'a> list(i)> list(n)) {
   var: <'a> list xs, ys;;

   switch (xss) {
     case Nil: return Nil;
     case Cons(xs, xss): ys = flatten (xss); return append(xs, ys);
   }
}

('a,'b){n:nat}
<'a> list(n) * <'b> list(n) split (xs: <'a * 'b> list(n)) {
  var: 'a y; 'b z; <'a> list ys; <'b> list zs;;

  switch (xs) {
    case Cons((y, z), xs):
      switch (split(xs)) {
        case (ys, zs): return(Cons(y, ys), Cons(z, zs));
      }
  }
}

('a){m:nat,n:nat | n < m}
'a nth (xs: <'a> list(m), n: int(n)) {
   var: 'a x; int y;;

   y = n;

   invariant: [m:nat, n:nat | n < m] (xs: <'a> list(m), y: int(n))
   while (true) {
     switch (xs) {
       case Cons(x, xs): if (y == 0) return x;
     }
   }
   exit (1);
}

[n: int | n >= 0] int(n) 
foo () {
  var: int i;;

  i = -100;

  while (i < 0) {
    i = i + 1;
  }

  return i;
}

unit foo () {
  var: int n, n4, i0, i1, i2, i3;;

  i0 = 0; i1 = 0; i2 = 0; i3 = 0;
  n = 16; n4 = 4;

  invariant:
    [i0:nat,i1:nat,i2:nat,i3:nat | i0 <= i1 <= i2 <= i3]
    (i0: int(i0), i1: int(i1), i2: int(i2), i3: int(i3))
  while (i3 <= n) {
    i0 = i0 + n4; i1 = i1 + n4; i2 = i2 + n4; i3 = i3 + n4;
  }
}

int foo () {
  var: [n:nat] int(n) i;;

  i = 0;
  while (true) {
    i = i + 1;
  }
  
  i = i;
  return i;
}

int int_add (x: int, y: int) {
  return x + y ;
}

{a:nat}
[m:int | m < a] int(m)
foo (x: int(a)) {
  return (x - 1);
}

{b:nat}
[n:int | n < b] int(n)
bar (x: int(b)) {
  return foo (x);
}

{size:nat, i:nat, j:nat, k:nat | i < size, j < size, k < size}
[n:nat | n < size] int(n)
median(i:int(i), j:int(j), k:int(k), vec[size]: float) {
  var: float x, y, z;;

  x = vec[i]; y = vec[j]; z = vec[k];

  if (x >. y) {
     if (y >. z) return j; else { if (x >. z) return k; else return i; }
  } else {
    if (y >. z) { if (x >. z) return i; else return k; } else return j;
  }
}

{size:nat, start:nat, end:nat | start < end <= size}
[n:nat | n < size] int(n)
get_pivot (start: int(start), end: int(end), vec[size]: float) {
  var: int diff, d;
       int i, j, k;;

  diff = end - start;
  
  if (diff < 7) return start + (diff / 2);
  else {
    i = start; j = start + diff / 2; k = end - 1;
    if (diff < 40) return median(i, j, k, vec);
    else {
      d = diff / 8;
      i = median(i, i + d, i + 2 * d, vec);
      j = median(j - d, j, j + d, vec);
      k = median(k - 2 * d, k - d, k, vec);
      return median(i, j, k, vec);
    }
  }
}

{size:nat, start: nat, end: nat | start < end <= size}
[n:nat | start <= n < end] int(n)
split(start: int(start), end: int(end), vec[size]: float) {
  var: int pivot;
       float x, temp;
       l: [i:int | start <= i <= end] int(i);
       h: [j:int | start <= j < end] int(j);;

  pivot = get_pivot(start, end, vec);
  l = start; h = end - 1;

  x = vec[pivot];

  while (true) {
    while (l < end) { if (vec[l] <=. x) l = l + 1; else break; }
    while (start < h) { if (vec[h] >. x) h = h - 1; else break; }
    if (l < h) {
      temp = vec[l]; vec[l] = vec[h]; vec[h] = temp;
      l = l + 1; h = h - 1;
    } else return h;
  } 
}
*/