Skip to content
Merged
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -1643,7 +1643,7 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IOrigin tok,
private string CharTypeDescriptorName => DafnyHelpersClass + (UnicodeCharEnabled ? ".RUNE" : ".CHAR");

private void ConvertFromChar(Expression e, ConcreteSyntaxTree wr, bool inLetExprBody, ConcreteSyntaxTree wStmts) {
if (e.Type.IsCharType && UnicodeCharEnabled) {
if (GetRuntimeType(e.Type).IsCharType && UnicodeCharEnabled) {
wr.Write("(");
TrParenExpr(e, wr, inLetExprBody, wStmts);
wr.Write(".Value)");
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ method Main() {
AutoInit.Test();
RefinementB.Test(2.0, 3.0);
SimpleNewtypeWitness.Test();
CharToInt.Test();
}

module Numerics {
Expand Down Expand Up @@ -659,3 +660,15 @@ module SimpleNewtypeWitness {
print a, " ", b, " ", c, "\n"; // 102 103 104
}
}

module CharToInt {
newtype char16 = c: char | c as int < 65536

method Test() {
var c: char := 'c';
var d: char16 := 'd';

print c, " (", c as int, ", ", c as char as int, "), ";
print d, " (", d as int, ", ", d as char as int, ")\n";
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -66,3 +66,4 @@ false true | true
7
2.0 3.0
102 103 104
'c' (99, 99), 'd' (100, 100)
1 change: 1 addition & 0 deletions docs/dev/news/6296.fix
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Compilation of type conversion from a `newtype`-based on `char` to `int`
Loading