Add 'with' syntax to pattern matching equations.

[developedby]

We can now write a with clause in a pattern matching equation and continue to match on its result.

For example, this function

HVM/link : HVM/RTerm -> HVM/RTerm -> (HVM Unit)
| a b =
  match a {
    #RTerm{at al}: match (HVM/RTag/is-sub at) {
      #True  : do HVM { ask x = (HVM/swap al #Some{b}) (HVM/link-sub al x) }
      #False : match b {
        #RTerm{bt bl}: match (HVM/RTag/is-var bt) {
          #True  : do HVM { ask x = (HVM/swap bl #Some{a}) (HVM/link-var bl x) }
          #False : do HVM { ask (HVM/push-redex #Pair{a b}) ret #Unit }
        }
      }
    }
  }

Could now be written as

HVM/link : HVM/RTerm -> HVM/RTerm -> (HVM Unit)
| a b with a
. | #RTerm{at al} with (HVM/RTag/is-sub at)
. . | #True  = do HVM { ask x = (HVM/swap al #Some{b}) (HVM/link-sub al x) }
. . | #False with b
. . . | #RTerm{bt bl} with (HVM/RTag/is-var bt)
. . . . | #True  = do HVM { ask x = (HVM/swap bl #Some{a}) (HVM/link-var bl x) }
. . . . | #False = do HVM { ask (HVM/push-redex #Pair{a b}) ret #Unit }

With the caveat that

1. Only one term per with clause, otherwise the type checker complains in the current implementation.
2. The equations inside the 'with' must be complete, there is no fallthrough of an equation to a smaller depth of withs.

So, for example, this will not work properly

HVM/link : HVM/RTerm -> HVM/RTerm -> (HVM Unit)
| a b with a b
. | #RTerm{at al} #RTerm{bt bl} with (HVM/RTag/is-sub at) (HVM/RTag/is-var bt)
. . | #True  _      = do HVM { ask x = (HVM/swap al #Some{b}) (HVM/link-sub al x) }
. . | #False #True  = do HVM { ask x = (HVM/swap bl #Some{a}) (HVM/link-var bl x) }
. . | #False #False = do HVM { ask (HVM/push-redex #Pair{a b}) ret #Unit }