Support assignment in conditional parts of an expression

[keyboardDrummer]

Depends on #358

Changes

• Support assignment in conditional parts of an expression

Testing

• Added conditionalAssignmentInExpression test-case to test-file T2_ImpureExpressions

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[atomb]

This looks nice. My one comment could be addressed in a future PR, if at all.

[atomb]

Given the DDM-defined syntax for Laurel, is this function strictly needed?

[keyboardDrummer]

Yes because the DDM grammar builds a parser/printer for a different type than the Laurel Lean type. There is only a transformation for the DDM type to the Lean type, but not vice versa, similar to Core.

[joscoh]

This seems to have a lot of overlap with #358. What is the difference between them?

[keyboardDrummer]

This seems to have a lot of overlap with #358. What is the difference between them?

This is stacked on top of that PR so it includes all the changes from that one, which sadly GH does not support well. Best to review this after that is merged.

From a user perspective, this PR enables this test:

procedure conditionalAssignmentInExpression(x: int) {
  var y: int := 0;
  var z: int := (if (x > 0) { y := y + 1; } else { 0 }) + y;
  if (x > 0) {
    assert y == 1;
    assert z == 2;
  } else {
    assert z == 0;
    assert y == 0;
  }
}