Boolean pattern matching in Why3ML

Question

In other ML-variants (such as SML) it is possible to do something like this:

case l of
   (true, _) => false
 | (false,true) => false
 | (false,false) => true

However, doing a similar thing using the Why3ML match declaration raises a syntax error:

match l with
 | (true, _) -> false
 | (false,true) -> false
 | (false,false) -> true
end

How do I correctly do value-based pattern matching inside a tuple?

Answer 1

Yes, it's possible:

module Test
  let unpack_demo () =
    let tup = (true, false) in (* parens required here! *)
    match tup with
    | True, False -> true  (* pattern must use bool's constructor tags *)
    | _           -> false
    end

  let ex2 () = match true, false with (* parens not required here *)
    | True, x      -> x
    | False, True  -> false
    | False, False -> true
    end
end

hayai[cygwin64][1155]:~/prog/why3$ why3 execute test.mlw Test.unpack_demo
Execution of Test.unpack_demo ():
     type: bool
   result: true
  globals:

hayai[cygwin64][1156]:~/prog/why3$ why3 execute test.mlw Test.ex2
Execution of Test.ex2 ():
     type: bool
   result: false
  globals:

Why3's pattern language is quite basic compared to SML or OCaml. The only values permitted in patterns in Why3 are constructors (not even e.g. integer constants are allowed), and only tuples can be destructured. This is why True and False are used in the patterns above; they are in fact the proper constructors for bool--true and false exist for convenience, but they won't work in patterns. See figure 7.2 in the grammar reference and take a look at the definition of pattern.