Comments (2)
@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
andDafny.Rune
in C#, orchar
andDafny.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.)
from libraries.
OK - though the proof is in the doing.
from libraries.
Related Issues (20)
- Request: ordered maps HOT 1
- Request: connecting Unicode logic to the string type HOT 1
- Request: LemmaUniqueMaximum as analagous to LemmaUniqueMinimum
- Ensure `src` libraries in sync with `src/dafny` libraries, deprecate the former
- Get JSON to work on Java HOT 1
- Additions for JSON
- Add MapWithResult for maps
- MutableMap for C#
- forall statement with no bound variables is deprecated in `ModInternals` HOT 1
- Request (I/O): AppendBytesToFile to complement WriteBytesToFile
- Request: append-to-file support in FileIO library HOT 1
- Readme.md needs code duplication explanation HOT 1
- The two Math.dfy files seem to cause problems
- "Warning: deprecated style: a semi-colon is not needed here" HOT 1
- Top-level `Dafny` namespace collides with Dafny runtime HOT 2
- JSON regression test fails HOT 2
- Example FileIO libary fails to complile HOT 1
- Module naming scheme pollutes top-level namespace HOT 1
- Question: Motivation behind trigger in LemmaMaxOfConcat
- Standard Library documentation is broken
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from libraries.