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

模式匹配允許解構複雜值，並且它決不限於值的表示的最外層級別。為了說明這一點，我們實現了將布林表示式轉換為布林表示式的函式，其中所有否定僅在原子上，所謂的否定正規形式和以這種形式識別表示式的謂詞：

我們定義布林表示式的型別，其原子由字串標識為

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 選項的錯誤。）

此功能可提高編譯器接受的程式的安全性和正確性。然而，它具有其他用途，並且可以例如用於探索性程式設計。將轉換寫入普通表單非常有趣，從處理簡單案例的函式的原始版本開始，並使用編譯器提供的非匹配案例的示例來優化處理。