Fixpoint3.Phase.Lowering

This phase lowers a high-level Ram.RamProgram into a low-level ExecutableRam.RamProgram executable by the Interpreter.

Concretely:

All Boxed values are replaced with representative Int64 values according to the Boxing.

For relations with multiple indexes,

MergeInto(newRel, otherRel)

becomes:

MergeInto(newRel, otherRelIndex1)
MergeInto(newRel, otherRelIndex2)
...

This ensures that all indexes are updated.

Similarly:

Purge(rel)

becomes:

Purge(relIndex1)
Purge(relIndex2)
...

For:

Swap(newRel, deltaRel)

it is transformed into:

Purge(deltaRelIndex2), Purge(deltaRelIndex3), ...
MergeInto(newRel, deltaRelIndex2), MergeInto(newRel, deltaRelIndex3), ...
Swap(newRel, deltaRelIndex1)

The above transformation relies on newRel having exactly one index.

Statements that previously referenced a RelSym are instead augmented with explicit index information (currently as Int32) indicating which index to use.

NotBots are removed entirely from the AST. The interpreter handles this explicitly whenever it encounters a Search or Query with Latticenal.

Every RowVar is assigned a unique position in memory (though not strictly necessary).

Finally instead of a query evaluating terms the terms are written to an array which is kept up to date with the current query values.

As an example the program:

search a ∈ A do
    query {b ∈ B | b[0] = a[0]} do
        project (a[0]) into R
    end
end

would be transformed to

search a ∈ A | [lookupArrForB[0] := a[0]] do
    query {b ∈ B | lookupArrForB } do
        project (a[0]) into R
    end
end

Whenever we bind a we update the query-value of B.

An alternative approach would be to have query of the form query {b ∈ B | searchTerms }. Then searchTerms would be evaluated to generate the restriction for the query. This would create a new object every time the query is met. Furthermore it would have to be evaluated every time query {b ∈ B | lookupArrForB } is met. If the query is deeply nested with some values bound higher up in the nesting, we do not need to evaluate these every time.