Request: basic File I/O needs to work for --unicode-char:true

[davidcok]

No description provided.

[alex-chew]

@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.)

[davidcok]

OK - though the proof is in the doing.