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 的存在是为了方便，但它们在模式中不起作用。参见the grammar reference中的图7.2，看看pattern.

的定义

Why3ML 中的布尔模式匹配

Boolean pattern matching in Why3ML

why3

why3ml