Module naming scheme pollutes top-level namespace

[markrtuttle]

I'd like to require that

• Modules in the Dafny library insert themselves into the Dafny namespace. Examples would be Dafny.JSON, Dafny.FileIO, and Dafny.Math.
• Langauge-specific code in the Dafny library insert themselves into the DafnyLibraries namespace. An example currently is DafnyLibraries.FileIO.

The current library pollutes the top-level namespace in ways that potentially clashes with the namespace of a target language. For example, now we have the Dafny Math module defining abs, min, and max that conflicts with the Java Math module and JavaScript Math module. The library modules should insert themselves into their own namespace to avoid conflicts.

The current FileIO library establishes the practice of inserting language-specific implementations into DafnyLibraries. Using DafnyLibraries for code and Dafny for modules works well. Dafny seems to dislike a module under Dafny externing out to external code that is also under Dafny (yielding "not found" error messages).

[robin-aws]

Thanks for the proposal. Definitely a known issue, and you'll notice that there is a second copy of several libraries under src/dafny that do place all modules underneath Dafny. That turned out to conflict with target language code in some Dafny runtimes, however.

More importantly though, we're in the process of moving lots of this code into the Dafny distribution itself, and Dafny 4.4 will bundle many standard libraries so that all you have to do to depend on them is pass the --standard-libraries flag. These will be qualified under DafnyStdLibs instead to avoid the above collision. More details here: https://github.com/dafny-lang/dafny/tree/master/Source/DafnyStandardLibraries.

I'm also working on the Dafny change to support language-specific implementations in the standard libraries right now, so I'll link the PR here once I cut it. :)