0

在其他 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

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

4

1 回答 1

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.

于 2017-12-23T11:15:11.607 回答