dead can reach the musical.rs

// .decl subset(R1, R2, P)
        //
        // At the point P, R1 <= R2.
        //
        // subset(R1, R2, P) :- outlives(R1, R2, P).
        // Already loaded; outlives is static.

        // .decl requires(R, B, P) -- at the point, things with region R
        // may depend on data from borrow B
        //
        // requires(R, B, P) :- borrow_region(R, B, P).
        // Already loaded; borrow_region is static.

        // .decl live_to_dead_regions(R1, R2, P, Q)
        //
        // The regions `R1` and `R2` are "live to dead"
        // on the edge `P -> Q` if:
        //
        // - In P, `R1` <= `R2`
        // - In Q, `R1` is live but `R2` is dead.
        //
        // In that case, `Q` would like to add all the
        // live things reachable from `R2` to `R1`.
        //
        // live_to_dead_regions(R1, R2, P, Q) :-
        //   subset(R1, R2, P),
        //   cfg_edge(P, Q),
        //   region_live_at(R1, Q),
        //   !region_live_at(R2, Q).

        // mechanization
        // step 1:
        // subset(R1, R2, P) x cfg_edge(P, Q)
        // subset map to (P, (R1, R2)) -- index subset on P ?
        // join to cfg_edge -- semijoin ?
        // result: live_to_dead_regions_1 (P, (R1, R2), Q)
        // next step: live_to_dead_regions_1 map to ((R1, Q), (P, R2))

        live_to_dead_regions_1.from_join(&subset_p, &cfg_edge, |&p, &(r1,r2), &q| ((r1, q), (p, r2)));

        // step 2:
        // live_to_dead_regions_1((R1, Q), (P, R2)) x region_live_at(R1, Q)
        // join to region_live_at -- semijoin ?
        // result: live_to_dead_regions_2 ((R1, Q), (P, R2))
        // next step: live_to_dead_regions_2 map to ((R2, Q), (R1, P))
        live_to_dead_regions_2.from_join(&live_to_dead_regions_1, &region_live_at_1, |&(r1, q), &(p, r2), &()| ((r2, q), (r1, p)));

        // step 3:
        // live_to_dead_regions_2((R2, Q), (R1, P)) x !region_live_at(R2, Q)
        // antijoin to region_live_at
        // result: live_to_dead_regions_3 ((R2, Q), (R1, P))
        // next step: live_to_dead_regions_3 map to (R1, R2, P, Q)
        live_to_dead_regions.from_antijoin(&live_to_dead_regions_2, &region_live_at, |&(r2, q), &(r1, p)| (r1, r2, p, q));

        // .decl dead_region_requires(R, B, P, Q)
        //
        // The region `R` requires the borrow `B`, but the
        // region `R` goes dead along the edge `P -> Q`
        //
        // dead_region_requires(R, B, P, Q) :-
        //   requires(R, B, P),
        //   !killed(B, P),
        //   cfg_edge(P, Q),
        //   !region_live_at(R, Q).

        // step 1
        // requires(R, B, P) x !killed(B, P)
        // requires map to ((B, P), R) -- indexed
        // antijoin to killed
        // results in ((B, P), R)
        // next_step: dead_region_requires_1 map to (P, (B, R))
        dead_region_requires_1.from_antijoin(&requires_bp, &killed, |&(b, p), &r| (p, (b, r)));

        // step 2
        // dead_region_requires_1(P, (B, R)) x cfg_edge(P, Q)
        // semijoin to cfg_edge
        // results in (P, (B, R), Q)
        // next step: dead_region_ map to ((R, Q), (P, B))
        dead_region_requires_2.from_join(&dead_region_requires_1, &cfg_edge, |&p, &(b, r), &q| ((r, q),( p, b)));

        // step 3
        // dead_region_requires_2((R, Q), (P, B)) x !region_live_at(R, Q)
        // antijoin to region_live_at
        // results in ((R, Q), (P, B))
        // returns (R, B, P, Q)
        dead_region_requires.from_antijoin(&dead_region_requires_2, &region_live_at, |&(r, q), &(p, b)| (r, b, p, q));

        // .decl dead_can_reach_origins(R, P, Q)
        //
        // Contains dead regions where we are interested
        // in computing the transitive closure of things they
        // can reach.

        dead_can_reach_origins.from_map(&live_to_dead_regions, |&(_r1, r2, p, q)| ((r2, p), q));
        dead_can_reach_origins.from_map(&dead_region_requires, |&(r, _b, p, q)| ((r, p), q));