fix: Java --unicode-char mode coercion improvements (#3630)

Fixes #3413.

Addresses the issues uncovered during #2818 by adding a `--unicode-char`
mode version of `Test/comp/Arrays.dfy`, which all stem from incomplete
handling of manual boxing/unboxing of the `CodePoint` type at various
Java code generation points. Note this is still incomplete as there must
be other spots that do not handle coercion correctly in general, but
these changes at least cover `Arrays.dfy`.

It turned out that handling arrow coercion as in the Go compiler was not
necessary for Java, because the initial casting of a function reference
as a lambda is where the necessary boxing/unboxing needs to happen
instead anyway. That is, a reference to a Dafny `function f(x: char):
char` has to end up as a Java `Function<CodePoint, CodePoint>` and
therefore be eta expanded from the start.

Also removed the fail-fast behavior from `%testDafnyForEachCompiler` as
I found it more useful for debugging that way.

Also implemented `ConcreteSyntaxTree.Comma` as part of an initial
implementation of Java arrow conversion, which ended up not directly
used but seems useful enough to keep (and I refactored one spot to use
it as an example).

Edit: I've also added a few more similar cases exposed as part of
enabling `/unicodeChar:1` by default for Dafny 4.0:
#3635

Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Fabio Madge <[email protected]>
Co-authored-by: Aaron Tomb <[email protected]>

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -2874,6 +2874,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -2884,6 +2885,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.EqCommon: {
@@ -3015,7 +3017,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
 
         default:
           base.CompileBinOp(op, e0, e1, tok, resultType,
-            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int,
+            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int, out coerceE1,
             errorWr);
           break;
       }
@@ -3037,8 +3039,14 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
           ConvertFromChar(e.E, wr, inLetExprBody, wStmts);
           wr.Write(", BigInteger.One)");
         } else if (e.ToType.IsCharType) {
-          wr.Write($"({CharTypeName})");
-          TrParenExpr(e.E, wr, inLetExprBody, wStmts);
+          if (UnicodeCharEnabled) {
+            wr.Write($"new {CharTypeName}((int)");
+            TrParenExpr(e.E, wr, inLetExprBody, wStmts);
+            wr.Write(")");
+          } else {
+            wr.Write($"({CharTypeName})");
+            TrParenExpr(e.E, wr, inLetExprBody, wStmts);
+          }
         } else {
           // (int or bv or char) -> (int or bv or ORDINAL)
           var fromNative = AsNativeType(e.E.Type);

Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs

@@ -2053,6 +2053,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -2063,6 +2064,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.Iff:

Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs

@@ -529,6 +529,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -539,6 +540,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.Iff:

Source/DafnyCore/Compilers/GoLang/Compiler-go.cs

@@ -3114,6 +3114,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       out bool reverseArguments,
       out bool truncateResult,
       out bool convertE1_to_int,
+      out bool coerceE1,
       ConcreteSyntaxTree errorWr) {
 
       opString = null;
@@ -3124,6 +3125,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       reverseArguments = false;
       truncateResult = false;
       convertE1_to_int = false;
+      coerceE1 = false;
 
       switch (op) {
         case BinaryExpr.ResolvedOpcode.BitwiseAnd:
@@ -3368,7 +3370,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
 
         default:
           base.CompileBinOp(op, e0, e1, tok, resultType,
-            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int,
+            out opString, out preOpString, out postOpString, out callString, out staticCallString, out reverseArguments, out truncateResult, out convertE1_to_int, out coerceE1,
             errorWr);
           break;
       }
@@ -3659,7 +3661,7 @@ protected override void EmitCollectionDisplay(CollectionType ct, IToken tok, Lis
           wr.Write("_dafny.SeqOf");
         }
       }
-      TrExprList(elements, wr, inLetExprBody, wStmts, type: ct.TypeArgs[0]);
+      TrExprList(elements, wr, inLetExprBody, wStmts, typeAt: _ => ct.TypeArgs[0]);
     }
 
     protected override void EmitMapDisplay(MapType mt, IToken tok, List<ExpressionPair> elements,