> Instead of using φ nodes, MLIR uses a functional form of SSA where terminators pass values into block arguments defined by the successor block.

Does anyone know if this equivalent (or very similar) to SSI (static single information) form? It would be cool to see something like this in a real-world compiler, since it is strictly more powerful than SSA. For example:

    if (x == 0) { f(x); } else { g(x); }

Here SSA doesn't help you express "x == 0, but only in the first branch, and x != 0, but only in the second branch", while with the automatic renaming you get with SSI/"functional form" you can express this as something like (ugly syntax I made up on the spot):

    if (x == 0)
        { f(x1); }[x1 = x]
    else
        { g(x2); }[x2 = x]

and then just record the (now flow-insensitive) facts that x1 == 0 and x2 != 0.