Balancing a red-black tree with pattern matching

static RBNode balance(int color, int value, RBTree left, RBTree right)
{
  if (color == BLACK) {
    switch (value,left,right) {
      case int z,
           RBNode(RED,int y,RBNode(RED,int x,RBTree a,RBTree b),RBTree c),
           RBTree d:
      case z, RBNode(RED,x,a,RBNode(RED,y,b,c)),d:
      case x, a, RBNode(RED,z,RBNode(RED,y,b,c),d):
      case x, a, RBNode(RED,y,b,RBNode(RED,z,c,d)):
        return RBNode(RED,y,RBNode(BLACK,x,a,b),RBNode(BLACK,z,c,d));
    }
  }
  return RBNode(color, value, left, right);
}

A modal abstraction
Containment predicate is also a tree iterator

boolean contains(Object elem) {
  if (left != null && value < elem) return left.contains(elem);
  if (value.equals(elem)) return true;
  if (right != null && value > elem) return right.contains(elem);
} iterates(elem) {
  foreach (left != null && left.contains(Object e)) yield e;
  yield value;
  foreach (right != null && right.contains(Object e)) yield e;
}

One formula implements both modes: concise, ensures consistency

boolean contains(Object elem) iterates(elem) (
  (left != null && elem < value && left.contains(elem)) ||
  elem = value ||
  (right != null && elem > value && right.contains(elem))
)

A client loop selecting elements matching a pattern

Set t = new RedBlackTree(); ...
foreach (t.contains(Point(int x, x*2))) { 
    // get all objects in set that are points (x,y) where y is twice x; bind x
    print(x);
}

Invertible CPS conversion using pattern matching

// Forward: convert(e) is the CPS conversion of e.
// Backward: e is the expression for which result is the CPS conversion.
static public Expr convert(Expr e) returns(e) (
  Var k = fresh("k", e) && (
    e = Var(String v1) &&
    result = Lambda(k, Apply(k, e))
  else
    e = Lambda(Var v2, Expr body) &&
    result = Lambda(k, Apply(k,
               Lambda(v2,
                 Lambda(k, Apply(convert(body), k)))))
  else
    e = Apply(Expr fn, Expr arg) &&
    Var f = fresh("f", arg) &&
    result = Lambda(k, Apply(convert(fn),
               Lambda(f, Apply(convert(arg),
                 Lambda(Var("v"), Apply(Apply(f, Var("v")), k))))))
  )
)

// Forward: whether v is free in e.
// Backward: all v's that are free in e.
static boolean FV(Expr e, String v) iterates(v) (
  e = Var(v) ||
  e = Lambda(String v1, Expr body) && FV(body, v) && !(v = v1) ||
  e = Apply(Expr fn, Expr arg) && (FV(fn, v) || FV(arg, v))
)

// Forward: a variable name that is fresh in e and starts with x.
// Backward: whether result is not free in e.
static Var fresh(String base, Expr e) {
  boolean dummy = true;
  for (int i = 0; dummy; i++) {
      String var = base + i;
      if (!FV(e, var)) return Var(var);
  }
}
  returns() ( !FV(e, result.name) )
...
Expr church_one = lambda("f", lambda("x", apply("f", "x")));
Expr cps_one = CPS.convert(church_one);
let CPS.convert(Expr e) = cps_one // e equals church_one!