Fix: Emit constraints for compiled quantifier expressions, and nested subset types

[MikaelMayer]

Fixes #1604

Previously, the test
https://github.com/dafny-lang/dafny/pull/1997/files#diff-3650380410d4f90c335dd7eaf17caf895d7630fe4720fdc0a58889666ac58fdf
would verify, compile, but none of the generated code of JavaScript, C#, Go or Java would work. Go, C# and Java would crash, and JavaScript would fail silently
Now everything works correctly.

I also fixed another soundness issue never reported. The compiler wasn't emitting nested constraints for nested subset types, so this file was crashing at run-time.
https://github.com/dafny-lang/dafny/pull/1997/files#diff-2a4f58bf9ce20437d573ece58c942499118c4b9745c7784373725b9302b78caf
Now it works correctly.

Changes in the backend-compiler

• I had to remove the intricate method CreateForeachLoop that was responsible for both iterating over a collection and ensuring subtype constraint. First, the compilation of forall expressions was relying on a library method and a lambda, so these subtype constraints were not checked, which was the root cause of the soundness issue Reference types in comprehension soundness issue #1604. But second and this is most important, it was putting the specification of doing these checks to the overridden method CreateForeachLoop, which makes it impossible to reuse somewhere else (such as these lambda), to add language-independent checks (such as the ones brought by this PR for subset types whose constraint is compilable) and of course not at all friendly if we want to make an intermediate language for compilation.
  • This method has been replaced by the compiler'sCreateGuardedForeachLoop that emits the loops and the constraints. It also integrates MaybeInjectSubtypeConstraint defined here which optionally test the type using EmitSubtypeCondition (see below for the definition). It also injects MaybeInjectSubsetConstraint defined here. This method that inlines compilable constraints now takes correctly care of nested subset types as tested here.
• I split the old CreateForeachLoop into three methods that every compiler needs to implement.
  • A new method CreateForeachLoop that only creates the loop structure. Refactored for C#, C++, Go, Java, JavaScript, Python (to be implemented of course).
  • A new method EmitSubtypeCondition that check if a variable satisfies the subtype constraint needed by the loop. That way, we can just reuse every compiler's if rather than hard-coding it as it was done previously. Refactored in C#, C++, Go, Java and JavaScript.
  • A new method EmitDowncastVariableAssignment, that is now executed after the subtype constraint check has been validated, both for forall and exists expressions as well as for set and map comprehensions and assign-such-that statements. Refactored in C#, C++, Go, Java, and JavaScript.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[keyboardDrummer]

Ok, one of the tests revealed why this PR was intricated with the previous PR. Here is the link:

type Small = x: int | 0 <= x < 100 && x != 3

function method F(x: int): int
  requires x != 3
{
  if x == 3 then 1/0 else 100
}

method Main() {
  var b := !exists n: Small :: F(n) != 100;
  assert b;
  print b;
}

The "exists", typechecks and verifies, but crashes at run-time, even with this PR. The reason for that is that "n" is wrongly inferred of type "Small", so the compiler doesn't think there is something which needs to be done. To really solve that problem, one has to consider type-checking "n" differently in the range, but doing so would break existing tests, because wto determine whether to type check "n" differently, we need to know if we are in a ghost context, which is exactly what #1702 does.

For now, in this PR, I will ensure the compiler always emit the type constraint when it's compilable. I will remove this check in the other PR because it'll no longer needed.

If we're compiling a comprehension, then we're never in a ghost context right? Shouldn't BoundedPool have a Type field that returns the type of values created by CompileCollection(BoundedPool ..), so we could assign var collectionElementType = boundedPool.Type ?

[MikaelMayer]

If we're compiling a comprehension, then we're never in a ghost context right? Shouldn't BoundedPool have a Type field that returns the type of values created by CompileCollection(BoundedPool ..), so we could assign var collectionElementType = boundedPool.Type ?

Right, and after your remark, I saw that this bounded pool ought to be better computed for integer pools as well, else the subset type was taken instead. I refactored the code so that now ElementType is a method of a pool to ensure it's implemented by every pool

[keyboardDrummer]

Returned? The return type is void

[MikaelMayer]

* "[[bodyWriter]]" is where the writer wr's position will be next

[keyboardDrummer]

What does option mean? Neither of the two following parameters are optional right?

[MikaelMayer]

    /// <summary>
    /// Emit an (already verified) downcast assignment like:
    /// 
    ///     var boundVarName:boundVarType := tmpVarName as boundVarType;
    ///     [[bodyWriter]]
    /// 
    /// where
    ///   * "[[bodyWriter]]" is where the writer wr's position will be next
    /// </summary>
    /// <param name="boundVarName">Name of the variable after casting</param>
    /// <param name="boundVarType">Expected variable type</param>
    /// <param name="tmpVarName">The collection's variable name</param>
    /// <param name="collectionElementType">type this variable is casted from, in case it is useful</param>
    /// <param name="introduceBoundVar">Whether or not to declare the variable, in languages requiring declarations</param>
    /// <param name="tok">A position in the AST</param>
    /// <param name="wr">The concrete syntax tree writer</param>
    ```