Desugar loops

[matthewhammer]

In the Desugar module, transform each for loop, while loop and loop ... while loop into an equivalent unconditional loop form, with compensating labels and breaks.

[matthewhammer]

I could use another pair of eyes on this now, or two: I can't see the cause of the current issue.

All the (non-dfinity) tests pass for me, save for this one (part of control.as):

// Triggers IR type error
  testLoopWhile() {
    label l loop {
      if true break l
      else continue l;
    } while (condition());
  };

In particular, I get an IR type error saying that () is not a subtype of Non. I'm a bit stumped. Other variations of this loop do not trigger this error; for example, these are each fine:

// Does not trigger IR type error
  testLoopWhile2() {
    loop { } while (false);
  };

  testLoopWhile3() {
    label l {
      loop { }
      while (false and true)
    };
  };

Strangely, when I remove the "extra block" in testLoopWhile3 above, I get a similar IR type error after my transformation, as in this example:

// Triggers IR type error
  testLoopWhile4() {
    label l loop {
    } while (true and false);
  };

I'm not exactly sure why yet.

I noticed that the parser does some pattern-matching on the case where a label immediately contains a loop; that seems related to me, but I can't yet see how. Maybe it's a red herring; I'm not yet sure.

[nomeata]

None of the variations use break. Might that be the problem?

[nomeata]

According to the stack trace Check_IR, fails while checking the type of the expression in LabelE:

    check_exp (add_lab env id.it t0) exp1;

The IR (dumped by asc) has three labels, but likely it is the inner one, the one that was already in the source:

                      (LabelE
                        continue l
                        ()
                        (IfE
                          (LitE (BoolLit true))
                          (BreakE l (TupE))
                          (BreakE continue l (TupE))
                        )
                      )

And indeed: It has a type () when the body contains two breaks, so never terminates, so returns Non.

Now I regret having asked for this to be merged into desugar (at least for debugging) ;-)

Just checking …The bug is not yet in master.

Hmm, Construct.labelE is wrong (didn’t we fix this before?); it should annotate the label with the type typ. But that does not fix this issue.

Construct.breakE and Construct.returnE as well, they annotate with type Non, as they don’t return.

Ok, there are a bunch of bugs in Construct. And one in Typing. That did id. Will create a separate PR for the fix to typing and check_ir, and push my other fixes to this branch.

[nomeata]

Pushed to #193 (please review, so that we can merge this first) and also merged into this PR, so that you can continue your work.

[matthewhammer]

Thank you @nomeata!

So, I'm a bit confused about the next steps to get this totally sorted. Are my transformations incorrect in some way, or are they merely using some (still) buggy Construct helpers, or both? (If you're not sure, that's okay, I'll investigate; just let me know what you suspect now).

Aside: I know that we want the OCaml source to stand in for a LaTeX document with inference rules (for stepping and typing judgements); I had a difficult time imagining the typing rules from looking at these cases. I submit that it may have been easier to have these bugs here because they were obscured by the (mostly minor) OCaml syntactical noise. Perhaps they would have been more apparent if we had some inference rules to stare at and compare against? Would it be worth writing these out sometime soon? The IR is fairly small, and it shouldn't take more than part of an afternoon. I think it would help me a lot in the future, and cement the IR's static semantics more in my mind.
(cc @crusso @rossberg).

[nomeata]

Well, I sorted out one problem (and the fix is both in #193 and this branch is in master). I did not investigate the remaining problem.

Would it be worth writing these out sometime soon?

Not sure. There is too much risk of it going stale if they cannot be executed in some way. Check_ir isn’t too bad to read; if you want to learn the rules better by working with them, maybe invest time to make Check_ir even more declarative?

[matthewhammer]

Sounds good. In a more ideal world, Check_ir would optionally produce a typing derivation, even if it's written in the current imperative style.

[nomeata]

Sounds good. In a more ideal world, Check_ir would optionally produce a typing derivation, even if it's written in the current imperative style.

The AST is typed, so there it is a typing derivation of sorts. You can write a pretty-printer for it that includes all the annotations. Also see https://dfinity.atlassian.net/browse/AST-61

[matthewhammer]

Cool. I added a comment there (on Jira) with my thoughts; I wish I could give you a direct link, but that's either missing as a Jira feature, or I haven't yet found it.

[nomeata]

Just looked at the Jenkins output again. It seems there are merely IR dumps in the expected test output that need to be updated. Let me do that for you.

[nomeata]

Done. I guess what is left to do now is to reap the benefit of the exercise and remove all those loop forms from ir.ml that are no longer needed, leaving only LoopE of exp. I’ll leave that enjoyable part to you :-)

[nomeata]

Very minor nit: Can you just write Type.unit here? I find it easier to read if I don’t have to see what ty1 is.

[matthewhammer]

Yep, will do.

[matthewhammer]

Awesome; thanks again, @nomeata!

Shall we do that refactoring/simplification of Ir to another PR? I'd prefer that, if possible.

Assuming you agree, can we merge this now? (I think you have the ability to approve, right?)

[matthewhammer]

I mean now, after fixing that nit. :)

[nomeata]

Let’s remove these comments and if true statements, and then merge. The IR cleanup may happen separately, if you want.

(Also, I am experimenting with GithHub’s “suggested change” feature.)

[matthewhammer]

Oops: I forgot about that temp stuff; thanks!

Aside: That new feature (suggested changes) was somewhat nice. I clicked a button, and the change was made for me.

How hard was it to propose these changes? You didn't need to do the edits in your browser, did you?

[nomeata]

How hard was it to propose these changes? You didn't need to do the edits in your browser, did you?

See https://help.github.com/en/articles/commenting-on-a-pull-request#adding-line-comments-to-a-pull-request point 6.

You can also apply the changes in a batch commit: https://help.github.com/en/articles/incorporating-feedback-in-your-pull-request (but less important if we squash before merging, or if we simply don’t care too much about the tidynes of master)

[nomeata]

Look like master has changed, and you’ll have to merge master into this branch before you can merge the PR.