否定正常形式深度模式匹配

模式匹配允许解构复杂值，并且它决不限于值的表示的最外层级别。为了说明这一点，我们实现了将布尔表达式转换为布尔表达式的函数，其中所有否定仅在原子上，所谓的否定正规形式和以这种形式识别表达式的谓词：

我们定义布尔表达式的类型，其原子由字符串标识为

type expr =
| Atom of string
| Not of expr
| And of expr * expr
| Or of expr * expr

让我们首先定义一个以否定正规形式识别表达式的谓词 ：

let rec is_nnf = function
| (Atom(_) | Not(Atom(_))) -> true
| Not(_) -> false
| (And(expr1, expr2) | Or(expr1, expr2)) -> is_nnf expr1 && is_nnf expr2

如你所见，可以匹配像 Not(Atom(_)) 这样的嵌套模式。现在我们实现一个函数，将布尔表达式映射为否定正规形式的等效布尔表达式：

let rec nnf = function
| (Atom(_) | Not(Atom(_))) as expr -> expr
| Not(And(expr1, expr2)) -> Or(nnf(Not(expr1)),nnf(Not(expr2)))
| Not(Or(expr1, expr2)) -> And(nnf(Not(expr1)),nnf(Not(expr2)))
| And(expr1, expr2) -> And(nnf expr1, nnf expr2)
| Or(expr1, expr2) -> Or(nnf expr1, nnf expr2)
| Not(Not(expr)) -> nnf expr

第二个函数更多地使用了嵌套模式。我们最终可以在对含义的否定中测试我们的代码：

# let impl a b =
Or(Not(a), b);;
  val impl : expr -> expr -> expr = <fun>
# let expr = Not(impl (Atom "A") (Atom "B"));;
val expr : expr = Not (Or (Not (Atom "A"), Atom "B"))
# nnf expr;;
- : expr = And (Atom "A", Not (Atom "B"))
# is_nnf (nnf expr);;
- : bool = true

OCaml 类型系统能够验证模式匹配的穷举性。例如，如果我们省略 nnf 函数中的 Not(Or(expr1, expr2)) 情况，编译器会发出警告：

# let rec non_exhaustive_nnf = function
| (Atom(_) | Not(Atom(_))) as expr -> expr
| Not(And(expr1, expr2)) -> Or(nnf(Not(expr1)),nnf(Not(expr2)))
| And(expr1, expr2) -> And(nnf expr1, nnf expr2)
| Or(expr1, expr2) -> Or(nnf expr1, nnf expr2)
| Not(Not(expr)) -> nnf expr;;
          Characters 14-254:
  ..............function
  | (Atom(_) | Not(Atom(_))) as expr -> expr
  | Not(And(expr1, expr2)) -> Or(nnf(Not(expr1)),nnf(Not(expr2)))
  | And(expr1, expr2) -> And(nnf expr1, nnf expr2)
  | Or(expr1, expr2) -> Or(nnf expr1, nnf expr2)
  | Not(Not(expr)) -> nnf expr..
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Not (Or (_, _))
val non_exhaustive_nnf : expr -> expr = <fun>

（在调用编译器或解释器时，可以将此警告视为 -w @8 选项的错误。）

此功能可提高编译器接受的程序的安全性和正确性。然而，它具有其他用途，并且可以例如用于探索性编程。将转换写入普通表单非常有趣，从处理简单案例的函数的原始版本开始，并使用编译器提供的非匹配案例的示例来优化处理。