Why3ML中的布尔模式匹配

Question

在其他ML-变体(如SML)中，可以这样做：

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

但是，使用Why3ML match声明做类似的事情会引发语法错误：

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

如何正确地在元组中进行基于值的模式匹配？

Answer 1

是的，有可能：

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:

与SML或OCaml相比，Why3的模式语言是相当基础的。在Why3中，模式中唯一允许的值是构造函数(甚至不允许整数常量)，并且只有元组可以被解构。这就是为什么在上面的模式中使用True和False的原因；它们实际上是bool的适当构造函数--true和false是为了方便而存在的，但它们不能在模式中工作。参见语法参考中的图7.2，并查看pattern的定义。