Consider a "join" operation, which is perhaps similar to a full outer join or a junction table from database theory.

The high-level idea is that, when two predicates are "joined", both predicates would constrain the memory locations in question, except that the predicate which is "applied second" would take priority if there are any conflicts ("applied second" in a similar sense that the f in the function composition f . g is "applied second"). So, if the first predicate has x :-> y and the second has x :-> z then x :-> z will take priority and the x :-> y will not be included in the generated predicate definition.

In addition to the new special form called join, there would be a couple of new syntax forms: _ meaning something like "use whatever is passed in at the call-site for this argument" and ?... for introducing a new variable which is fresh w.r.t. the predicate definitions. Crucially, the variables introduced by the ?... form can be shared between the two "arguments" of a usage of the join operation. See below.

To give a smaller example to just illustrate what these forms mean and what the corresponding transformations do syntactically, if we have

predicate example(loc x, int a, int b, pred p) {
| true => { p(a, b) ; [x, 2] ** x :-> a ** (x+1) :-> b }
}

synonym s_example(loc y, int c, int d, pred q) {
  example(y, c, d, q(_, ?freshVar))
}

this would translate to

predicate s_example_generated(loc x, int a, int b, pred p) {
| true => { p(a, freshVar) ; [x, 2] ** x :-> a ** (x+1) :-> b }
}

Note this example is only to demonstrate how these two new syntactic forms are translated and does not make much sense in practical terms. To give a more practical example, we look at using _ and ?... when combining predicates with join.

This example code:

synonym foldMap(loc x, set s, int acc, int z, pred mapFn, pred foldFn) {
  join( constrained_list(x, s, mapFn(_, ?mapResult))
      , fold(x, s, acc, z, foldFn(_, ?mapResult, _))
      )
}

predicate constrained_list(loc x, set s, pred p) {
|  x == null        => { s =i {} ; emp }
|  not (x == null)  => {
    s =i {v} ++ s1 && p(v, r)
      ;
    [x, 2] ** x :-> r ** (x + 1) :-> nxt ** constrained_list(nxt, s1, p) }
}

predicate fold(loc x, set s, int acc, int z, pred p) {
|  x == null => { acc == z; emp }
|  not (x == null) => {
    s =i {v} ++ s1 && p(acc, v, acc1)
      ;
    [x, 2] ** x :-> v ** (x + 1) :-> nxt ** fold(nxt, s1, acc1, z, p) }
}

could get translated into

predicate foldMap_generated(loc x, set s, int acc, int z, pred mapFn, pred foldFn) {
| x == null => { acc == z && s =i {} ; emp }
| not (x == null) => {
     s =i {v} ++ s1 && mapFn(v, mapResult)
     && foldFn(acc, mapResult, acc1)
       ;
     [x, 2] ** x :-> mapResult ** (x + 1) :-> nxt ** foldMap_generated(nxt, s1, acc1, z, mapFn, foldFn)
  }
}

^{(TODO: There seems to be a subtlety regarding the various s =i {v} ++ s1 constraints in the example above. All three of them coincide in this example, but how should this be handled in general? If a constraint isn't used, because its only use was eliminated due to the other predicate taking priority, as could be the case above, should this be the only deciding factor?)}

This seems to be equivalent to the foldMap that is currently working, except that the results of the map are being stored rather than keeping the original list. In both cases, though, "acc" should have the fold-mapped result.

Branches with matching conditions get combined, such that the second predicate takes priority if there is a "conflict," as mentioned earlier. This combination could be done by a simple syntactic check on the conditions and, later on, we could consider whether it makes sense to combine branches if their conditions are logically equivalent to each other.

Notice that the ?... allows you to "link" parts of the two predicates.