Else simplification pass

[DCupello1]

This pass is towards a better representation of otherwise when the only concern are boolean premises. This simply takes the original premises of the generated relations and negates them.

The pass performs the following steps:

• It collects all of the generated relations from the otherwise removal pass (Else pass #187) and makes a mapping (original relation -> generated relations).
• It then goes through each rule of the original relation and checks if there is a negated relational premise.
• If there is, then we grab the boolean premises of the generated relation and negate them.

Some restrictions of this pass:

• If any premise contains a quantifier that was not present in the original rule's conclusion (the one that had the otherwise), then we do not simplify it. This is due to the quantification being flipped when negating the premise.
• Only works for boolean premises. (Iterated boolean premises would again flip quantification)

Example:

relation Step_pure: admininstr* ~> admininstr*
rule Step_pure/br_if-true:
  (CONST I32 c) (BR_IF l)  ~>  (BR l)
  -- if c =/= 0

rule Step_pure/br_if-false:
  (CONST I32 c) (BR_IF l)  ~>  eps
  -- otherwise

From else pass (omitting wf premises):

relation `Step_pure_before_br_if-false`: `%`(admininstr*)
  rule `br_if-true_0`{c : val_, l : labelidx}:
    `%`([CONST_admininstr(I32_valtype, c) BR_IF_admininstr(l)])
    -- if (!($proj_val__0(c))!`%`_uN.0 =/= 0)
    
relation Step_pure: `%~>%`(admininstr*, admininstr*)
  rule `br_if-true`{c : val_, l : labelidx}:
    `%~>%`([CONST_admininstr(I32_valtype, c) BR_IF_admininstr(l)], [BR_admininstr(l)])
    -- if (!($proj_val__0(c))!`%`_uN.0 =/= 0)

  rule `br_if-false`{c : val_, l : labelidx}:
    `%~>%`([CONST_admininstr(I32_valtype, c) BR_IF_admininstr(l)], [])
    -- ~ `Step_pure_before_br_if-false`: `%`([CONST_admininstr(I32_valtype, c) BR_IF_admininstr(l)])

From else simplification pass:

relation Step_pure: `%~>%`(admininstr*, admininstr*)
  rule `br_if-true`{c : val_, l : labelidx}:
    `%~>%`([CONST_admininstr(I32_valtype, c) BR_IF_admininstr(l)], [BR_admininstr(l)])
    -- if (!($proj_val__0(c))!`%`_uN.0 =/= 0)

  rule `br_if-false`{c : val_, l : labelidx}:
    `%~>%`([CONST_admininstr(I32_valtype, c) BR_IF_admininstr(l)], [])
    -- if (!($proj_val__0(c))!`%`_uN.0 = 0)

[DCupello1]

This one should also be ready to be reviewed. @rossberg or @zilinc can you take a look? Let me know if you have any questions! (Of course if you have time, I know its a pretty busy week!)

[rossberg]

Generally looks good to me. I defer to @zilinc for details. :)

One meta comment, though: I see you writing all these excellent and helpful descriptions of passes in respective PRs. But those all go into oblivion after merging! I think it would make sense to have some version of these as documentation in the code, e.g., the MLI files.

[DCupello1]

Generally looks good to me. I defer to @zilinc for details. :)

One meta comment, though: I see you writing all these excellent and helpful descriptions of passes in respective PRs. But those all go into oblivion after merging! I think it would make sense to have some version of these as documentation in the code, e.g., the MLI files.

Ah yeah, you are right! I for some reason stop putting the description in the actual code itself. I used to put at the top of the ML file instead of the MLI file, do you think I should do the latter instead? I'll add it now for the newer passes (and modify some of the existing descriptions).

[rossberg]

I think the MLI files would be more fitting, since they're describing the "contract".

[DCupello1]

I think the MLI files would be more fitting, since they're describing the "contract".

I see! Makes sense, I'll only change it for else-simp for now, and will make a PR to change the description of the other passes.