union <'a> rlist with nat {
 Empty(0);
 {n:pos} Even(n+n) of <'a * 'a> rlist(n);
 {n:nat} Odd(n+n+1) of 'a * <'a * 'a> rlist(n)
}

('a){n:nat}
<'a> rlist(n+1) cons (x: 'a, xs: <'a> rlist(n)) {
  var: y: 'a; ys: <'a * 'a> rlist;;

  switch (xs) {
    case Empty: return Odd (x, Empty);
    case Even (ys): return Odd (x, ys);
    case Odd (y, ys): return Even (cons((x, y), ys));
  }
  exit;
}

('a){n:nat}
bool(n=0) isEmpty (xs: <'a> rlist(n)) {
  switch (xs) {
    case Empty: return true;
    case Even(_): return false;
    case Odd(_): return false;
  }
}

('a){n:pos}
'a * <'a> rlist(n-1) uncons (xs: <'a> rlist(n)) {
  var: 'a x, y; ys: <'a * 'a> rlist;;

  switch (xs) {
    case Even (ys): ((x, y), ys) = uncons (ys); return (x, Odd (y, ys));
    case Odd (y, Empty): return (y, Empty);
    case Odd (y, ys as Even (_)): return (y, Even (ys));
    case Odd (y, ys as Odd (_)): return (y, Even (ys));
  }
  exit;
}

/*
('a){n:pos}
'a * <'a> rlist(n-1) uncons (xs: <'a> rlist(n)) {
  var: 'a x, y; ys: <'a * 'a> rlist;;

  switch (xs) {
    case Even (ys): ((x, y), ys) = uncons (ys); return (x, Odd (y, ys));
    case Odd (y, ys):
      if (isEmpty(ys)) { return (y, Empty); }
      else { return (y, Even (ys)); }
  }
  exit;
}
*/

('a){n:nat}
int(n) length (xs: <'a> rlist(n)) {
  var: ys: <'a * 'a> rlist;;

  switch (xs) {
    case Empty: return 0;
    case Even (ys): return 2 * length (ys);
    case Odd (_, ys): return 2 * length (ys) + 1;
  }
}

('a){n:nat, i:nat | i < n}
'a lookup (i: int(i), xs: <'a> rlist(n)) {
  var: 'a x, y; ys: <'a * 'a> rlist;;

  switch (xs) {
    case Even (ys):
      switch (lookup (i/2, ys)) {
        case (x, y): if (i % 2 == 0) return x; else return y;
      }
    case Odd (y, ys):
      if (i==0) return y;
      else {
        switch (lookup ((i-1)/2, ys)) {
          case (x, y): if (i % 2 == 0) return y; else return x;
        }
      }
  }
}

('a){n:nat, i:nat | i < n}
<'a> rlist(n) update (i: int(i), x: 'a, xs: <'a> rlist(n)) {
  var: int j; 'a y, y0, y1; ys: <'a * 'a> rlist;;
  
  switch (xs) {
    case Even (ys):
      j = i / 2;
      switch (lookup (i/2, ys)) {
        case (y0, y1):
          if (i == 2 * j) return Even (update (j, (x, y1), ys));
          else return Even (update (j, (y0, x), ys));
      }
    case Odd (y, ys):
      if (i == 0) return Odd (x, ys);
      else {
        i = i - 1; j = i / 2;
        switch (lookup (i/2, ys)) {
          case (y0, y1):
            if (i == 2 * j) return Odd (y, update (j, (x, y1), ys));
            else return Odd (y, update (j, (y0, x), ys));
        }
      }
  }
}

('a){n:nat}
<'a> list(n) list_of_rlist (xs: <'a> rlist(n)) {
  var: x: 'a;;
  switch (xs) {
    case Empty: return Nil;
    case Even(_):
      (x, xs) = uncons(xs);
      return Cons (x, list_of_rlist (xs));
    case Odd(_):
      (x, xs) = uncons(xs);
      return Cons (x, list_of_rlist (xs));
  }
}

('a){n:nat}
<'a> rlist(n) rlist_of_list (xs: <'a> list(n)) {
  var: x: 'a;;
  switch (xs) {
    case Nil: return Empty;
    case Cons (x, xs): return cons (x, rlist_of_list (xs));
  }
}

unit print_list (l: <int> list) {
  var: int x;;

  while (true) {
    switch (l) {
      case Nil: print_string ("[]"); break;
      case Cons (x, l): print_int (x); print_string ("::");
    }
  }
}

unit print_rlist (rl: <int> rlist) {
   print_list (list_of_rlist (rl));
}

unit main () {
  var: nat i, len; rl: <int> rlist;;
 
  len = 100; rl = Empty;

/*
  invariant: [i:nat | i <= 100] (i: int(i), rl: <int> rlist(i))
  for (i = 0; i < len; i = i+1) {
    rl = cons (i, rl);
  } withinv (rl: <int> rlist (100))

  print_rlist (rl); print_newline ();

  invariant: (rl: <int> rlist(100))
  for (i = 0; i < len; i = i+1) {
    rl = update (i, i, rl);
  }
*/

  for (i = 0; i < len; i = i+1) {
    rl = cons (i, rl);
  }

  print_rlist (rl); print_newline ();

  for (i = 0; i < length (rl); i = i+1) {
    rl = update (i, i, rl);
  }

  print_rlist (rl); print_newline ();
}