SUS impls

You can try out the algorithm by running the binary and giving it an input. Example:

cargo run "all(any(a, b, c), any(d, e, f))"

Output:

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

How it works

This rather long section explains how the algorithm works.

First, initial implementations are generated from the input. Then, possible logical input conflicts are rejected. Finally, type system conflicts are fixed.

Initial implementations

Number of initial implementations

The number of initial implementations n_init can be calculated recursively:

• A field a requires one initial implementation: n_init(a) = 1.
• n_init(any(arg_0, …, arg_n)) = n_init(arg_0) + … + n_init(arg_n) (sum)
• n_init(all(arg_0, …, arg_n)) = n_init(arg_0) * … * n_init(arg_n) (product)
• n_init(not(arg)) = n_init(arg)

Example:

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

Setting initial implementations

First, an implementation matrix impls represented as a vector of vectors of S for "set", U for "unset" or _ for "generic" is created. The number of rows is n_init. The number of columns is the number of fields. The matrix is initialized with _ at the beginning.

Example all(any(a, b), any(c, d)) with n_init = 4:

a b c d
_ _ _ _
_ _ _ _
_ _ _ _
_ _ _ _

This matrix will be filled with a function set_init that takes the following arguments:

1. impls: The mutable matrix (or part of it).
2. A group (all(…), any(…), not(…) or just a field).
3. invert: Whether to set U instead of S. Needed to support not.

This function is implemented recursively and will be explained for all four possible cases in the next subsections.

Field

For a field a, set_init(impls, a, invert) sets the column a for every row in impls to U if invert is true, otherwise to S.

We have to set every row, not only the first one. This will be clear in the example all(any(a, b), all(c, d)) when the case all is explained.

Example a:

a
S

Not

not inverts the argument invert.

set_init(impls, not(GROUP), invert)
= set_init(impls, GROUP, !invert)

Example not(a):

a
U

All

set_init(impls, all(arg_0, …, arg_n), invert) is implemented in the following way:

1. Call set_init(impls, arg_0, invert).
2. Divide the rows of impls in sections section_i with n_init(all(arg_1, …, arg_n)) rows (without arg_0).
3. Call set_init(section_i, all(arg_1, …, arg_n), invert) for every i.

Example all(a, b):

a b
S S

The reason behind the sections section_i will be clear in the next section when any is nested inside all.

Any

The naive way to implement set_init(impls, any(arg_0, …, arg_n), invert) is the following:

1. Divide the rows of impls into sections section_i such that the first section is the first n_init(arg_0) rows, the second section is the n_init(arg_1) rows after the first section and so on.
2. Call set_init(section_i, arg_i, arg_n) for every i.

Example any(a, b):

a b
S _
_ S

But what if impls has more rows than n_init(arg_0) + … + n_init(arg_n)?

This can be the case if any is nested inside of all. In that case, the number of rows in impls can be a multiple mult of n_init(arg_0) + … + n_init(arg_n).

Therefore, we have to build the sections such that the first section is the first mult * n_init(arg_0) rows and so on.

Example all(any(a, b), any(b, c)):

a b c d
S _ S _
S _ _ S
_ S S _
_ S _ S

The first step in the example is set_init(impls, any(a, b), false):

a b c d
S _ _ _
S _ _ _
_ S _ _
_ S _ _

The second step set_init(impls[..2], any(c, d), false):

a b c d
S _ S _
S _ _ S
_ S _ _
_ S _ _

The last step set_init(impls[2..], any(c, d), false):

a b c d
S _ S _
S _ _ S
_ S S _
_ S _ S

Logical input conflicts

The algorithm searches for logical input conflicts in the matrix with initial implementations.

I call these conflicts logical to distinguish them from the type system conflicts in the next sections.

Two initial implementations have no logical conflicts in the following two cases:

1. The first implementation has a generic where the other has a non-generic AND the first has a non-generic where the other has a generic.
2. The first implementation has S where the other has U OR the first has U where the other has S.

The first case makes sure that any(all(a_0, …, a_n), all(b_0, …, b_m)) is logically non-conflicting if there is at least one i where a_i != b_j for all j AND at least one i where b_i != b_j for all j. One of the two conditions are not enough! Example: any(all(a, b), all(a)). Here, we have one condition b != a, but it is not enough. We need something like any(all(a, b), all(a, c)) where we also have c != b.

The second case makes sure that any(all(a_0, …, a_n), all(b_0, …, b_m)) is logically non-conflicting if there is at least one i and j where b_i = not(a_j).

An example with a logical conflict related to the first case: any(all(a, b), a)

a b
S S
S _

An example without logical conflicts related to the first case: any(all(a, b), all(a, c))

a b c
S S _
S _ S

An example with a logical conflict related to the second case: any(all(a, b), all(a, b))

a b
S S
S S

An example without logical conflicts related to the second case: any(all(a, b), all(not(a), b))

a b
S S
U S

Although the last example can be simplified to only require b, it has no logical conflicts. The simplified matrix would be:

a b
_ S

This algorithm does not make such simplifications. The user is responsible for such an optimization.

Sorting

After the initial implementations are set, it is worth it to sort the implementations by the number of non-generics.

This can be explained using the following example any(all(a, b), c):

a b c
S S _
_ _ S

The solution of this matrix with initial implementations that fixes type system conflicts is the following:

a b c
S S _
U _ S
S U S

The details of this solution will be discussed in the next section.

If we start with the following matrix:

a b c
_ _ S
S S _

Then the solution includes only two instead of three implementations:

a b c
_ _ S
S S U

Since the algorithm to fix type system conflicts (see next section) works from top to bottom, this sorting makes sure that upper implementations have a lower potential of conflicts than lower implementations by having more generic fields.

Fixing type system conflicts

Steps motivation

In this section, the steps of the algorithm to fix type system conflicts are motivated to be presented in the next section.

After sorting initial implementations without logical conflicts, we have to fix conflicts for the type system.

Let's say that we have any(a, b). Then we have the following two implementations:

a b
S _
_ S

What would happen when both a and b are S? Which implementation should be used then? This can not be determined and Rust throws a conflict error at compile time.

One solution is the following:

a b
S U
U S
S S

We did specify that the first two implementations can be used when only a or b is S. Then we added a third implementation for the case that both a and b are S.

To remove the additional implementation, we could merge it with only one of the first two using a generic.

Either

a b
S U
_ S

or

a b
S _
U S

We want to develop an algorithm that fixes such issues from top to bottom. Therefore, we choose the second variant.

Let's take a look at another example and use our oberservation while solving the last one.

The example is any(a, b, c):

a b c
S _ _
_ S _
_ _ S

Let's add a U below every S as we did in the last example:

a b c
S _ _
U S _
_ U S

The first and last implementations are still conflicting!

We need to add another U in the last implementation:

a b c
S _ _
U S _
U U S

I call this observed strategy "casting shadows" because it looks like S casting a U shadow to all implementations below it.

What if there is an S somewhere below an S? For example any(all(a, b), all(a, c), all(b, c)):

a b c
S S _
S _ S
_ S S

We don't overwrite any S. We cast the shadow ignoring any S on the way:

a b c
S S _
S U S
U S S

Now, let's take a look at the example any(all(a, b), all(c, d)):

a b c d
S S _ _
_ _ S S

If we just cast a shadow like in the examples above, we get the following:

a b c d
S S _ _
U U S S

The conflicts are fixed. But we don't have any implementation for the case where c, d and (a XOR b) are S although the condition of having all(c, d) is fulfilled.

The solution for this issue is motivated by any(a, b, c). We cast a diagonal shadow of U with S under it adding additional implementations as required:

a b c d
S S _ _
U _ S S
-------
S U S S

We separate initial implementations from additional ones with --- which is relevant for later.

Another example with a longer diagonal shadow any(all(a, b, c), 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

If we find a U in a lower implementation while we are trying to cast a U shadow, we don't change anything in that implementation. There is no conflict since there is already a U in the column where the higher implementation has S. Therefore we can move to the next lower implementation.

Example any(all(a, b), all(a, c), all(d, e)):

a b c d e
S S _ _ _
S _ S _ _
_ _ _ S S

First, we cast the shadow of the first implementation:

a b c d e
S S _ _ _
S U S _ _
U _ _ S S
---------
S U _ S S

Now, we cast the shadow of the second implementation:

a b c d e
S S _ _ _
S U S _ _
U _ _ S S
---------
S U U S S

We didn't write U in c of the third implementation because there is U under one S of the second implementation.

Dealing with not

not introduces a new class of problems.

An example is any(all(a, c), all(not(a), b), all(b, c)):

a b c
S _ S
U S _
_ S S

The algorithm so far does only one step by adding one U to the third implementation:

a b c
S _ S
U S _
U S S

But now, the second and third implementations are conflicting!

The solution is to remove the less generic implementation which is the third one:

a b c
S _ S
U S _

This means that we have to fix possible conflicting implementations in the mutated initial implementations when we have a not. This requires looping through the mutated initial implementations, searching for conflicts, and only keeping the more generic implementations.

Cleaning up additional implementations

Sometimes, the algorithm so far generates additional implementations that are conflicting with the (mutated) initial implementations.

Example all(any(a, b), any(c, d)):

a b c d
S _ S _
S _ _ S
_ S S _
_ S _ S

The result is:

a b c d
S _ S _
S _ U S
U S S _
U S U S
-------
S U U S

But the additional implementation is conflicting with the second implementation and has to be removed!

Therefore, the algorithm has to clean up additional implementations at the end.

Steps

1. For every implementation, find the indices of all S naming the vector focus_indices.
2. Iterate through each lower implementation and find the indices of all _ that overlap with focus_indices naming the vector generic_indices. If you find at least one U that overlaps with focus_indices, skip this lower implementation.
3. Set the first U as the first index in generic_indices by mutating the lower implementation.
4. Set the rest of the diagonal U shadow with S under it in generic_indices while adding additional implementations if generic_indices has more than one index.
5. If a not exists in the input:
   1. Repeat steps 1-4 while swapping every mention of S with U and every mention of U with S. This step is needed to fix U conflicts. In step 1, find only the indices of U from the original unmutated initial implementations. This means that all U set in steps 3-4 don't count.
   2. Remove possible less generic implementations from the mutated initial implementations.
6. Remove additional implementations that conflict with the mutated initial implementations.