Pure parse function #4083

keyboardDrummer · 2023-05-25T13:53:37Z

Follow-up of #4059

NOTE: please review the first 4 commits separately from the rest, since they contain code moves and renames.

Changes

No longer let the error message "Error: the included file contains error(s)" appear when using the CLI. This error is not useful on the CLI because the actual errors of the included file are shown as well.
No longer let ParseFile.ParseFile take and modify an ErrorReporter, but instead let it return one.
No longer let Parser.Parse take and modify a Builtins, but instead let it return a list of actions that can modify a Builtin.
Moved subclasses of Document into their own file
Moved Include class into its own file.

Testing

Updated existing test expect files for the change in included file error reporting

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

alex-chew · 2023-05-26T14:42:34Z

Source/DafnyCore/AST/BuiltIns.cs

  }
-  public UserDefinedType ArrayType(IToken tok, int dims, List<Type> optTypeArgs, bool allowCreationOfNewClass, bool useClassNameType = false) {
+
+  public static (UserDefinedType type, Action<BuiltIns> ModifyBuiltins) ArrayType(IToken tok, int dims, List<Type> optTypeArgs, bool allowCreationOfNewClass, bool useClassNameType = false) {


Can we document the difference between this ArrayType and the previous one?

There is some implicit documentation in the fact that this one is static. I'll add documentation to the non-static one saying it updates the instance.

alex-chew · 2023-05-26T14:49:55Z

Source/DafnyCore/Dafny.atg

+                                        var eeCopy = ee;
+                                        BuiltinsModifiers.Add(b => b.ArrayType(eeCopy.Count, new IntType(), true));


Do we need a full copy or just the count?

Suggested change

var eeCopy = ee;

BuiltinsModifiers.Add(b => b.ArrayType(eeCopy.Count, new IntType(), true));

var eeCount = ee.Count; // ee might be modified later, but we want the original array dims

BuiltinsModifiers.Add(b => b.ArrayType(eeCount, new IntType(), true));

The eventual list size determines the required array type. The list size shouldn't be edited from this point on, unless ArrayType is called again with the new size, so I think either is fine.

alex-chew · 2023-05-26T14:54:58Z

Source/DafnyCore/Dafny.atg

How large can BuiltinsModifiers get, and could it be a performance concern that we store all these lambdas instead of modifying the BuiltIns immediately?

It'll be much smaller than the parsed AST, so I don't think there is a concern. We could dedupe the list, but I feel right now that would be premature optimization.

alex-chew · 2023-05-26T14:58:17Z

Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs

+        BuiltIns.ArrayType(Token.NoToken, dims,
+          new List<Type> { new InferredTypeProxy() }, true).ModifyBuiltins(resolver.builtIns);


I might be missing something, but how does this compile when BuiltIns.ArrayType(IToken, int, List<Type>, bool, bool = false) returns a tuple?

It returns a tuple with named members, and .ModifyBuiltins accesses one those, similar to what .ItemX would do.

alex-chew · 2023-05-26T15:01:48Z

Source/DafnyCore/Generic/Reporting.cs

-      // TODO move this out of ErrorReporter together with OuterModule. Let Program have a list of FileModuleDefinitions as constructor input and create its default module there.
-      if (tok.FromIncludeDirective(OuterModule) && OuterModule != null) {
-        var include = OuterModule.Includes.First(i => i.IncludedFilename == tok.Uri);
-        if (!include.ErrorReported) {
-          Message(source, ErrorLevel.Error, null, include.tok, "the included file " + Path.GetFileName(tok.ActualFilename) + " contains error(s)");
-          include.ErrorReported = true;
-        }
-      }


I'm all for this change, but we should be sure to mention this in the CHANGELOG since I know there are users (including myself) who are accustomed to the behavior, and might be confused if we change it silently.

alex-chew

I left a few comments above, none blocking. Thanks for making this one easier to review.

### Changes - Let the Dafny language server use a cache for parsing. The cache stores items as long as they were used in the previous compilation. This means that commenting out an include can cause a large piece of cache to be pruned, leading to a possibly unexpected slowdown when it's uncommented again. ### Caveats I've decided not to add an option to turn off caching, since I don't see the use-case. Of course caching is a computation vs storage trade-off, and we could provide many options to configure the caching behavior, but I think the current caching is cheap enough (at most storing two sets of parse results at a time) that there is no reason to want to turn it off. Please carefully review the code that determines the cache key, since a bug in that would lead to outdated compilation results. ### Testing - Add a test that checks if parsing is cached, and that the cache prunes entries when they're not hit. - Add test for included file has error message for indirect includes, something that was still missing from #4083 <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

keyboardDrummer requested a review from alex-chew May 25, 2023 14:20

keyboardDrummer marked this pull request as ready for review May 25, 2023 14:22

keyboardDrummer mentioned this pull request May 25, 2023

Do not let Parser.Parse edit the default module #4059

Merged

keyboardDrummer enabled auto-merge (squash) May 26, 2023 08:48

Moved some classes into their own files

b536ca5

keyboardDrummer force-pushed the reallyPureParseFunction branch from b6c457c to 05bb8ff Compare May 26, 2023 08:56

keyboardDrummer added 4 commits May 26, 2023 11:00

Move code within ParseUtils

b1424b6

Rename AllMessages to AllMessagesByLevel

caf6e8f

Rename Document.Diagnostics to AllFileDiagnostics

c7c8c2f

Make ParseUtils.ParseFile pure

81c8cec

keyboardDrummer force-pushed the reallyPureParseFunction branch from 05bb8ff to 81c8cec Compare May 26, 2023 09:02

alex-chew reviewed May 26, 2023

View reviewed changes

alex-chew approved these changes May 26, 2023

View reviewed changes

keyboardDrummer merged commit a8d2cfd into dafny-lang:master May 26, 2023
19 checks passed

keyboardDrummer mentioned this pull request May 26, 2023

Cache parsing #4085

Merged

ZhongRuoyu mentioned this pull request Jul 20, 2023

dafny 4.2.0 Homebrew/homebrew-core#137130

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Pure parse function #4083

Pure parse function #4083

keyboardDrummer commented May 25, 2023 •

edited

Loading

alex-chew May 26, 2023

keyboardDrummer May 26, 2023

alex-chew May 26, 2023

keyboardDrummer May 26, 2023

alex-chew May 26, 2023

keyboardDrummer May 26, 2023

alex-chew May 26, 2023

keyboardDrummer May 26, 2023

alex-chew May 26, 2023

alex-chew left a comment

		var eeCopy = ee;
		BuiltinsModifiers.Add(b => b.ArrayType(eeCopy.Count, new IntType(), true));

		BuiltIns.ArrayType(Token.NoToken, dims,
		new List<Type> { new InferredTypeProxy() }, true).ModifyBuiltins(resolver.builtIns);

Pure parse function #4083

Pure parse function #4083

Conversation

keyboardDrummer commented May 25, 2023 • edited Loading

Changes

Testing

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alex-chew left a comment

Choose a reason for hiding this comment

keyboardDrummer commented May 25, 2023 •

edited

Loading