search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.91k stars 262 forks source link

Module/File scoping #1490

Open smswz opened 3 years ago

smswz commented 3 years ago

Is it possible to have a module defined across multiple files? It would be nice to be able to split a module into multiple files to prevent having unwieldy files. Verification of methods can quickly overcome the length computation within the methods, leading to very long files that are difficult to visually parse and make it more likely to have merge conflicts.

robin-aws commented 3 years ago

Verification of methods can quickly overcome the length computation within the methods

Ironically I'm having a bit of trouble visually parsing this clause :) Length computation?

smswz commented 3 years ago

That's what I get for not proofreading well 😞 That sentence was supposed to mean that the verification clauses and other formal validation clauses can overwhelm the length of the imperative, to-be-transpiled code.

robin-aws commented 3 years ago

Got it, thanks for clarifying.

From an implementation perspective, this wouldn't be hard. We wouldn't be changing the fact that modules are verified together as a whole. include statements are already mostly equivalent to just concatenating file contents together, and we would likely just be concatenating together the parsed contents of each module fragment before proceeding with the rest of the pipeline.

My bigger concern would be whether this would tie our hands for future improvements. We already want to move away from using include statements and would rather have something like a "Dafny classpath" (see also this RFC around some initial support for packaging libraries: https://github.com/dafny-lang/rfcs/pull/5). There are pretty fundamental decisions to make there about how to resolve a symbol to a source file or files: Java and C# have completely opposing strategies, for example. I would want to have at least a firm plan there first before supporting this feature through include statements.

smswz commented 3 years ago

If moving to a classpath and file directory <=> package, then this would probably be able to rolled into those changes then? If using a classpath approach, would it be necessary to declare a module with braces or would it be declared with a statement and the beginning of the file? For example:

module org.dafny.std;

Because likely with a classpath approach, I don't think it'd be possible for multiple modules to be in a directory (and also a file).