Add support for nested pattern matching on enums

[marsella]

With some frequency in implementations of rejection sampling, I need to do pattern matching on a pair of enums. Right now it requires nested case statements, which add a lot of indentation and are a bit hard to read. It would be nice to have support for case statements over tuples of enums, like:

case (maybe_a, maybe_b) of
    (Some a, Some b) -> a + b
    (Some a, None) -> a
    (None, Some b) -> b
    (None, None) -> 0

Three use cases I haven't encountered but have thought about are:

• Pairs where the two values don't have the same type
• Short circuit evaluation / wildcard only one of the ticks, like (Some a, _) -> error "shouldn't be some"
• Wildcard on all tuple members, like _ -> error "this case shouldn't happen"

[yav]

For these kinds of things in Haskell sometimes I define functions like this, and we could perhaps also do that in Cryptol:

fromSome: {a} a -> Option a -> a
fromSome dflt mb =
  case mb of
    Some a -> a
    None -> dflt

ifBoth: {a,b,c} (a -> b -> c) -> Option a -> Option b -> Option c
ifBoth f x y =
  case x of
    Some a ->
      case y of
        Some b -> Some (f a b)
        None -> None
    None -> None

ifEither: {a} (a -> a -> a) -> Option a -> Option a -> Option a
ifEither f x y =
  case x of
    Some a ->
      case y of
        Some b -> Some (f a b)
        None -> Some a
    None ->
      case y of
        Some b -> Some b
        None -> None
 

It's also reasonable to have the argument of ifBoth and ifEither return an Option value, which is useful if you want to allow combining only certain values.