Fixpoint3.Phase.Hoisting

The purpose of this phase is to hoist If ops as much as possible and merge them with Search into Query when possible/relevant. Additionally, guards are added at the top of Insert statements that only perform the operations if none of the involved relations are empty. For example, the following

search a ∈ A do
    search b ∈ B do
        search c ∈ C do
            if (b[0] = a[0] ∧ c[0] = a[0]) then
                project (a[0]) into R
            end
        end
    end
end

is hoisted to

if (not (A = ∅) ∧ not (B = ∅) not (C = ∅)) then
    search a ∈ A do
        query {b ∈ B | b[0] = a[0]} do
            query {c ∈ C | c[0] = a[0]} do
                project (a[0]) into R
            end
        end
    end
end

One hard dependency of the current implementation is that for BoolExp.Eq(x, y), x and y must either be Lit or RowLoad(_ ,_, _).

The hoisting in general happens with a MutDisjointSets, called equalitySets, which is populated by BoolExp.Eq(RowLoad, RowLoad). In this way, all RowLoad's which are equal will be treated as one.

termMap contains a map from the representing RowLoad, with respect to equalitySets, to the RamTerm highest in the AST where the value of Rep is known.

For example, given:

search a ∈ A do
    search b ∈ B do
        search c ∈ C do
            if (b[0] = a[0] ∧ c[0] = a[0], b[1] = 1, b[2] = c[1]) then
                project (a[0]) into R
            end
        end
    end
end

equalitySets could be {a[0] => a[0], b[0] => a[0], c[0] => a[0], b[1] => b[1], b[2] => c[1], c[1] => c[1]}.

Since equalitySets is only used to get representatives for loads, the exact value of the representative load is irrelevant. As long as a[0], b[0] and c[0] get the same representative, the actual value could be any of them. Also note that b[1] only points to itself, not 1. The fact that b[1] = 1 would be maintained by termMap.

termMap will be initialized with {b[1] => 1}.

When arriving at search b ∈ B, termMap will be {b[1] => 1, a[0] => a[0]}.

When arriving at search c ∈ C, termMap will be {b[1] => 1, a[0] => a[0], c[1] => b[2]}.

When arriving at if (...) and project(...) termMap will remain unchanged.