这是算法的草图。这也是Lennart
Augustsson著名的有效编译模式匹配技术的基础。（本文是在点击率如此之高的令人难以置信的FPCA程序（LNCS
201）中提出的。）该想法是通过将最一般的模式重复分解为构造函数案例来构造详尽的，非冗余的分析。

通常，问题在于您的程序可能有一堆空的“实际”模式{p 1，..，p n
}，您想知道它们是否覆盖了给定的“理想”模式q。首先，将q设为变量x。不变，最初满足并随后保持，是每个p 我是σ 我一些替代σq 我将变量映射到图案。

如何进行。如果n = 0，则束为空，因此您可能遇到q未被模式覆盖的情况。抱怨ps并不详尽。如果σ 1是一个射 重命名 的变量，则P
1个捕获任何情况下匹配Q，所以我们很热情：如果n = 1，我们赢了; 如果n> 1然后oop，就不可能有p 2的需要。否则，我们有一些变量x，σ 1
x是一个构造模式。在那种情况下，将问题分为多个子问题，每个子问题对应x类型的构造函数c j。也就是说，将原始q分成多个理想模式q j = [x：= c j
y 1 .. y arity（c j） ] q，并为每个q j相应地优化模式以保持不变，删除不匹配的模式。

让我们以{[], x :: y :: zs}（::用于cons）为例。我们从

  xs covering  {[], x :: y :: zs}

并且我们有[xs：= []]使第一个模式成为理想实例。所以我们拆分xs，得到

  [] covering {[]}
  x :: ys covering {x :: y :: zs}

这些中的第一个是通过空的内射性重命名来证明的，所以可以。第二个花费[x：= x，ys：= y :: zs]，所以我们又离开了，分裂ys，得到。

  x :: [] covering {}
  x :: y :: zs covering {x :: y :: zs}

从第一个子问题中我们可以看出来。

重叠的情况更加微妙，并且可以进行变化，具体取决于您是要标记任何重叠，还是只是按照从上到下的优先级顺序完全冗余的模式。您的基本摇滚乐是相同的。例如，从

  xs covering {[], ys}

用[xs：= []]证明其中第一个的正确性，因此拆分。请注意，我们必须使用构造函数的情况来完善y，以保持不变性。

  [] covering {[], []}
  x :: xs covering {y :: ys}

显然，第一种情况严格是重叠的。另一方面，当我们注意到需要细化实际的程序模式以保持不变性时，我们可以过滤掉那些多余的严格细化，并检查至少有一个幸存者（如此处的::情况）。

因此，该算法以实际程序模式p激励的方式构建了一组理想的穷举重叠模式q。只要实际模式需要特定变量的更多细节，就可以将理想模式分为构造器案例。如果幸运的话，每个实际模式都由不相交的非空理想模式集所覆盖，而每个理想模式仅被一个实际模式所覆盖。生成理想模式的案例分割树为您提供了有效的跳转表驱动的实际模式编译方法。

我提出的算法显然是终止的，但是如果存在没有构造函数的数据类型，则它可能无法接受空模式集是详尽无遗的。在依赖类型的语言中，这是一个严重的问题，在传统语言中，不确定传统模式的详尽程度是无法确定的：明智的方法是允许“反驳”以及方程式。在Agda中，您可以在无法进行构造函数优化的任何地方编写（），发音为“
my Aunt Fanny”，这使您免除了使用返回值完成方程式的要求。通过添加足够多的引用，可以使每个详尽的模式集都可以被 识别为 详尽无遗。

无论如何，这就是基本情况。