@robin-aws I think it's possible for the file I/O externs to support both --unicode-char options at the same time. The exposed methods use string only for the file path parameter and the error message types (the read/written bytes are seq<bv8> and not string). Does the following approach make sense to you?
In target languages that support method overloading, like Java and C#, define a method overload for each compiled char type (char and Dafny.Rune in C#, or char and Dafny.CodePoint in Java)
In target languages that don't support method overloading but are dynamically typed, like JS and Python, branch on the path argument's type and return the error message (if applicable) as the same type
In Golang, define a union interface of the _dafny.Char and _dafny.CodePoint wrappers, and (like the JS/Python approach) branch on the argument's actual types (returning an appropriate error message type)
(Python and Golang aren't supported yet, but I want to check that this approach is feasible so we don't have to change our minds when we do add support.)
@robin-aws I think it's possible for the file I/O externs to support both
--unicode-char
options at the same time. The exposed methods usestring
only for the file path parameter and the error message types (the read/written bytes areseq<bv8>
and notstring
). Does the following approach make sense to you?char
type (char
andDafny.Rune
in C#, orchar
andDafny.CodePoint
in Java)path
argument's type and return the error message (if applicable) as the same type_dafny.Char
and_dafny.CodePoint
wrappers, and (like the JS/Python approach) branch on the argument's actual types (returning an appropriate error message type)(Python and Golang aren't supported yet, but I want to check that this approach is feasible so we don't have to change our minds when we do add support.)