所以，今天我想我找到了一个方法，可以仅枚举线性项，同时仍然懒惰地修剪死分支。这将大大加快 SupGen 的速度，但它没有成功 :( 所以我们又回到了枚举完整的 λ-项。 好的一面是，我了解到我们可以枚举任意数据类型的所有项，而无需拆分标签，只需将其构建为带孔的累加器。看起来似乎不是很有用，但无论如何，这里是 HVM3 源代码：