Add if-then-else introduction IL pass

[nomeata]

This pass recongizes when multiple subsequent clauses of a definition share the pattern and have only boolean premises, and rewrites that to a single clause using if-then-else on the right-hand side.

[nomeata]

Here is the impact of introducing this pass as a diff:

https://gist.github.com/nomeata/daa2b72a365a781431dfeefe2f27535b

It seems it also removes otherwise premises from clauses that are not precended by identical pattern. This seems reasonable if we assume seqential matching semantics anyways.

[nomeata]

@DCupello1, guess you can review this now :-)

[DCupello1]

Overall happy with this pass, just some questions regarding extra steps that can be done in the pass.

[DCupello1]

Would we maybe want a little weaker of a condition? (i.e. if the preceding clause pattern matches to the next clause)

i.e for a function as such:

def $foo(nat) : nat
def $foo(5) = 10
  -- if cond
def $foo(n) = 20

Could technically group up as well. (But would need to add n = 5 to the condition)

Though this might be too tricky for such a pass.

[nomeata]

Right, I thought about this, but didn't necessarily want it in the first version. I would actually say that should be a separate pass that runs first, an overlap-removal pass, after which all patterns are either the same or clearly apart. This would compose well, I think.

[DCupello1]

Do we want NegPr here? Later on we filter it out anyways. Could we convert to UnE neg?

What about IterPrs with a bool premise? Could we convert these to IterEs? (Should be possible since they have the same structure).

[nomeata]

Good points. Do we have examples for them? (There is a tension with writing complete powerful passes vs avoiding to write code that isn't actually exercised and thus more likely broken)

[DCupello1]

Thats a good point. Though if we want it to be possible to write say wasm 4.0 in a robust manner, then we should go for more complete passes. Maybe its worth thinking about making tests for such passes then? To try to cover most of the cases.

Technically this function is an example of IterPr with a boolean (though it would not group up in the strong definition that you have at the moment):

def $growtable(tableinst, n, r) = tableinst'
  -- if tableinst = { TYPE (at `[i .. j?] rt), REFS r'* }
  -- if tableinst' = { TYPE (at `[i' .. j?] rt), REFS r'* r^n }
  -- if $(i' = |r'*| + n)
  -- (if i' <= j)?

[nomeata]

We have the test spec file in the middle end directory to dump artificial examples of tricky cases. We could use that more. Ideally with comments what's being tested :-)

[DCupello1]

Do we want NegPr here? Later on we filter it out anyways. Could we convert to UnE neg?

What about IterPrs with a bool premise? Could we convert these to IterEs? (Should be possible since they have the same structure).

Actually we need to be more careful with IterPrs with bools, since we would want to convert it to the ocaml equivalent to List.for_all, instead of List.map which is what is currently what is done for Rocq with IterEs.

[nomeata]

Added NegPr.

Yeah, I’ll leave IterPr out of this for now, else I’d have to think about whether the side-condition that the lengths are the same (if its iterating over multiple sequences) should be added before or after, and how that affects sequencing.

Hmm, now that I say that, this is a problem already now, isn't it? If I have

def $f(n) = 1 -- if n > 42
def $f(n) = 2 -- if partialFun(n) = 23
def $f(n) = 3 -- else

then it’s important to introduce whatever sideconditions are implicit in the second case, because if we do it after this pass then the side-condition would be added to the combined clauses?

Well, we’ll fix that when we get there :-)

[DCupello1]

Happy to leave IterPr for now.

Hmm yeah that seems like it could be an issue. We can discuss this once we have a better picture of the order of the passes (given we are introducing many new ones).