3 个不稳定版本
| 0.2.1 | 2023年6月23日 |
|---|---|
| 0.2.0 | 2023年6月22日 |
| 0.1.0 | 2023年6月22日 |
#1 in #impls
31KB
388 行
SUS 实现
您可以通过运行二进制文件并提供输入来尝试该算法。示例
cargo run "all(any(a, b, c), any(d, e, f))"
输出
a b c d e f
S _ _ S _ _
S _ _ U S _
S _ _ U U S
U S _ S _ _
U S _ U S _
U S _ U U S
U U S S _ _
U U S U S _
U U S U U S
工作原理
这一相当长的部分解释了算法是如何工作的。
首先，从输入生成初始实现。然后，拒绝可能存在的逻辑输入冲突。最后，修复类型系统冲突。
初始实现
初始实现的数量
初始实现的数量 n_init 可以递归计算
- 字段
a需要一个初始实现：n_init(a) = 1。 n_init(any(arg_0, …, arg_n)) = n_init(arg_0) + … + n_init(arg_n)（求和）n_init(all(arg_0, …, arg_n)) = n_init(arg_0) * … * n_init(arg_n)（乘积）n_init(not(arg)) = n_init(arg)
示例
n_init(all(any(a, b), any(c, d)))
= n_init(any(a, b)) * n_init(any(c, d))
= (n_init(a) + n_init(b)) * (n_init(c) + n_init(d))
= (1 + 1) * (1 + 1)
= 2 * 2
= 4
设置初始实现
首先，创建一个表示为 impls 的实现矩阵，它是一个向量向量，其中 S 表示 "设置"，U 表示 "未设置"，或 _ 表示 "通用"。该矩阵的行数为 n_init。列数为字段数。矩阵以 _ 初始化。
示例 all(any(a, b), any(c, d))，其中 n_init = 4
a b c d
_ _ _ _
_ _ _ _
_ _ _ _
_ _ _ _
此矩阵将通过以下参数填充一个函数 set_init
impls：可变矩阵（或其部分）。- 一组（
all(…)，any(…)，not(…)或仅一个字段）。 invert：是否设置U而不是S。需要支持not。
此函数通过递归实现，将在下一小节中解释所有四种可能的情形。
字段
对于一个字段 a，set_init(impls, a, invert) 将 impls 中每一行的列 a 设置为 U（如果 invert 是 true），否则设置为 S。
我们必须设置每一行，而不仅仅是第一行。这将在下一个示例 all(any(a, b), all(c, d)) 中解释 all 情况时变得清楚。
示例 a
a
S
非
not 反转参数 invert。
set_init(impls, not(GROUP), invert)
= set_init(impls, GROUP, !invert)
示例 not(a)
a
U
所有
set_init(impls, all(arg_0, …, arg_n), invert) 的实现方式如下
- 调用
set_init(impls, arg_0, invert)。 - 将
impls的行分为section_i部分，每个部分有n_init(all(arg_1, …, arg_n))行（不包括arg_0）。 - 对于每个
i，调用set_init(section_i, all(arg_1, …, arg_n), invert)。
示例 all(a, b)
a b
S S
section_i 部分的理由将在下一节中解释，当时 any 被嵌套在 all 中。
任何
实现 set_init(impls, any(arg_0, …, arg_n), invert) 的直观方法是以下内容
- 将
impls的行划分为多个部分section_i，使得第一个部分包含前n_init(arg_0)行，第二个部分是第一个部分之后的n_init(arg_1)行，依此类推。 - 对于每个
i调用set_init(section_i, arg_i, arg_n)。
示例 any(a, b)
a b
S _
_ S
但如果 impls 的行数多于 n_init(arg_0) + … + n_init(arg_n) 呢？
这可能是当 any 被嵌套在 all 里面时的情况。在这种情况下，impls 的行数可以是 n_init(arg_0) + … + n_init(arg_n) 的一个 mult 倍。
因此，我们必须构建这些部分，使得第一个部分包含前 mult * n_init(arg_0) 行，依此类推。
示例 all(any(a, b), any(b, c))
a b c d
S _ S _
S _ _ S
_ S S _
_ S _ S
示例中的第一步是 set_init(impls, any(a, b), false)
a b c d
S _ _ _
S _ _ _
_ S _ _
_ S _ _
第二步是 set_init(impls[..2], any(c, d), false)
a b c d
S _ S _
S _ _ S
_ S _ _
_ S _ _
最后一步是 set_init(impls[2..], any(c, d), false)
a b c d
S _ S _
S _ _ S
_ S S _
_ S _ S
逻辑输入冲突
算法在初始实现矩阵中搜索逻辑输入冲突。
我将这些冲突称为 逻辑 冲突，以区分下一节中类型系统冲突。
以下两种情况下，两个初始实现之间没有逻辑冲突
- 第一个实现有一个泛型，而另一个没有，并且第一个有一个非泛型，而另一个有泛型。
- 第一个实现有
S，而另一个有U，或者第一个有U，而另一个有S。
第一种情况确保当存在至少一个索引 i 使得对于所有 j 有 a_i != b_j，并且至少存在一个索引 i 使得对于所有 j 有 b_i != b_j 时，any(all(a_0, …, a_n), all(b_0, …, b_m)) 在逻辑上不冲突。两个条件中任一都不足以满足要求！例如：any(all(a, b), all(a))。在这里，我们有一个条件 b != a，但这不足以满足。我们需要类似 any(all(a, b), all(a, c)) 的条件，其中我们也有 c != b。
第二种情况确保当存在至少一个索引 i 和 j 使得 b_i = not(a_j) 时，any(all(a_0, …, a_n), all(b_0, …, b_m)) 在逻辑上不冲突。
与第一种情况相关的逻辑冲突的例子：any(all(a, b), a)
a b
S S
S _
与第一种情况无关的逻辑冲突的例子：any(all(a, b), all(a, c))
a b c
S S _
S _ S
与第二种情况相关的逻辑冲突的例子：any(all(a, b), all(a, b))
a b
S S
S S
与第二种情况无关的逻辑冲突的例子：any(all(a, b), all(not(a), b))
a b
S S
U S
尽管最后一个例子可以简化为只需要 b，但它没有 逻辑冲突。简化的矩阵将是
a b
_ S
此算法不进行此类简化。用户负责此类优化。
排序
初始实现设置完毕后，按非泛型数量对实现进行排序是值得的。
以下是一个例子来解释这一点 any(all(a, b), c)
a b c
S S _
_ _ S
此矩阵的解决方案是以下修复类型系统冲突的初始实现
a b c
S S _
U _ S
S U S
此解决方案的详细信息将在下一节中讨论。
如果我们从以下矩阵开始
a b c
_ _ S
S S _
那么解决方案只包括两个实现，而不是三个
a b c
_ _ S
S S U
由于修复类型系统冲突的算法（见下一节）从上到下工作，这种排序确保了上层实现由于具有更多泛型字段，其潜在的冲突比下层实现低。
修复类型系统冲突
步骤动机
在本节中，为了在下一节中展示，对修复类型系统冲突的算法步骤进行了动机。
在排序无逻辑冲突的初始实现后，我们必须修复类型系统的冲突。
假设我们有一个 any(a, b)。那么我们有两个以下实现
a b
S _
_ S
当 a 和 b 都为 S 时会发生什么？那时应该使用哪个实现？这是无法确定的，并且 Rust 在编译时会抛出冲突错误。
一个解决方案如下
a b
S U
U S
S S
我们确实指定，当只有 a 或 b 为 S 时，可以使用前两个实现。然后我们添加了第三个实现，以处理 a 和 b 都为 S 的情况。
为了删除额外的实现，我们可以使用泛型将其与 第一个 或 第二个 中的一个合并。
或者
a b
S U
_ S
或者
a b
S _
U S
我们希望开发一个从上到下修复此类问题的算法。因此，我们选择了第二种变体。
让我们看看另一个例子，并使用我们在解决上一个例子时的观察结果。
这个例子是 any(a, b, c)
a b c
S _ _
_ S _
_ _ S
让我们在每个 S 下方添加一个 U，就像我们在上一个例子中做的那样
a b c
S _ _
U S _
_ U S
第一个和最后一个实现仍然有冲突！
我们需要在最后一个实现中添加另一个 U
a b c
S _ _
U S _
U U S
我把这种观察到的策略称为“投射阴影”，因为它看起来像 S 向所有下方的实现投射了一个 U 阴影。
如果在某个地方下面有一个 S，那会怎样？例如 any(all(a, b), all(a, c), all(b, c), all(a, b))
a b c
S S _
S _ S
_ S S
我们不覆盖任何 S。我们忽略路径上的任何 S 来投射阴影
a b c
S S _
S U S
U S S
现在，让我们看看这个例子 any(all(a, b), all(c, d))
a b c d
S S _ _
_ _ S S
如果我们像上面的例子一样投射阴影，我们得到以下结果
a b c d
S S _ _
U U S S
冲突得到了解决。但是，我们没有对 c、d 和 (a XOR b) 是 S 的情况进行实现，尽管满足了 all(c, d) 的条件。
这个问题的解决方案受到 any(a, b, c) 的启发。我们使用 S 在下面添加所需的额外实现来投射 U 的对角阴影
a b c d
S S _ _
U _ S S
-------
S U S S
我们使用 --- 将初始实现与附加实现分开，这在以后是相关的
另一个带有更长对角阴影的例子 any(all(a, b), all(c, d), all(d, e, f))
a b c d e f
S S S _ _ _
U _ _ S S S
-----------
S U _ S S S
S S U S S S
如果我们尝试投射 U 阴影时在较低实现中找到一个 U，我们不会在该实现中做任何更改。由于较高实现中的 S 所在列已经有一个 U，因此不存在冲突。因此，我们可以移动到下一个较低实现。
例子 any(all(a, b), all(a, c), all(d, e))
a b c d e
S S _ _ _
S _ S _ _
_ _ _ S S
首先，我们投射第一个实现的阴影
a b c d e
S S _ _ _
S U S _ _
U _ _ S S
---------
S U _ S S
现在，我们投射第二个实现的阴影
a b c d e
S S _ _ _
S U S _ _
U _ _ S S
---------
S U U S S
由于第二个实现的某个 S 下面有一个 U，我们没有在第三个实现的 c 中写入 U
处理 not
not 引入了一类新问题。
一个例子是 any(all(a, c), all(not(a), b), all(b, c))
a b c
S _ S
U S _
_ S S
目前的算法只通过在第三个实现中添加一个 U 来执行一个步骤
a b c
S _ S
U S _
U S S
但是，现在第二个和第三个实现存在冲突！
解决方案是删除更不一般的实现，即第三个实现
a b c
S _ S
U S _
这意味着当我们有一个 not 时，我们必须修复可能存在冲突的初始实现中的实现。这需要遍历突变初始实现，寻找冲突，并且只保留更一般的实现。
清理额外的实现
有时，目前的算法会生成一些额外的实现，这些实现与（突变）初始实现冲突。
例如 all(any(a, b), any(c, d))
a b c d
S _ S _
S _ _ S
_ S S _
_ S _ S
结果是
a b c d
S _ S _
S _ U S
U S S _
U S U S
-------
S U U S
但是，额外的实现与第二个实现冲突，必须删除！
因此，算法必须在最后清理额外的实现。
步骤
- 对于每个实现，找到所有命名向量
focus_indices的S的索引。 - 遍历每个较低实现，找到所有与
focus_indices相叠的_的索引，命名向量generic_indices。如果你找到一个与focus_indices相叠的U，则跳过此较低实现。 - 通过突变较低实现，将第一个
U设置为generic_indices中的第一个索引。 - 当
generic_indices有多个索引时，将generic_indices中其余的对角线U用其下的S遮挡，同时添加额外的实现。 - 如果输入中存在
not- 在将每个
S与U互换，将每个U与S互换的同时，重复步骤 1-4。此步骤需要修复U冲突。在第 1 步中，只找到原始未突变初始实现中U的索引。这意味着在步骤 3-4 中设置的所有的U都不计入。 - 从突变初始实现中删除可能的较不一般的实现。
- 在将每个
- 删除与突变初始实现冲突的额外实现。
依赖关系
~245–670KB
~16K SLoC