Do not let Parser.Parse edit the default module
#4059
Conversation
keyboardDrummer
force-pushed
the
pureParseFunction
branch
from
2b835b5
to
3f0b3c5
Compare
…eDefinition into Program
… pureParseFunction
keyboardDrummer
changed the title
keyboardDrummer
changed the title
Parser.Parse edit the default module
| // private static string ParseFile(DafnyFile dafnyFile, Include include, BuiltIns builtIns, ErrorReporter errorReporter) { | ||
| // var fn = builtIns.Options.UseBaseNameForFileName ? Path.GetFileName(dafnyFile.FilePath) : dafnyFile.FilePath; | ||
| // try { | ||
| // var parseResult = ParseUtils.Parse(dafnyFile.Content, dafnyFile.Uri, builtIns, errorReporter); | ||
| // var errorCount = parseResult.ErrorCount; | ||
| // if (errorCount != 0) { | ||
| // return $"{errorCount} parse errors detected in {fn}"; | ||
| // } | ||
| // } catch (IOException e) { | ||
| // IToken tok = include == null ? Token.NoToken : include.tok; | ||
| // errorReporter.Error(MessageSource.Parser, tok, "Unable to open included file"); | ||
| // return $"Error opening file \"{fn}\": {e.Message}"; | ||
| // } | ||
| // | ||
| // return null; // Success | ||
| // } |
There was a problem hiding this comment.
Ugh, woops. Will remove in the follow-up PR (#4083)
| @@ -147,7 +147,6 @@ ensures true | |||
| } | |||
|
|
|||
| AreAllTokensOwned(program); | |||
| Assert.Equal(9, count); // Sanity check | |||
There was a problem hiding this comment.
Why does this need to be removed?
There was a problem hiding this comment.
Because the DefaultModule now has a filename in its StartToken, the traversal doesn't go deeper than that Node and count only gets up to 1. This is fine though. I'm not sure why Assert.Equal(9, count) was in there because it wasn't asserting any required behavior.
| } else { | ||
| Reporter.Error(MessageSource.RefinementTransformer, nw, commonMsg, nw.WhatKind, nw.Name); | ||
| } | ||
| } else if (nw is DefaultClassDecl) { | ||
| if (d is DefaultClassDecl) { | ||
| m.TopLevelDecls[index] = MergeClass((DefaultClassDecl)nw, (DefaultClassDecl)d); | ||
| m.DefaultClass = (DefaultClassDecl)MergeClass((DefaultClassDecl)nw, (DefaultClassDecl)d); |
There was a problem hiding this comment.
I'm not very familiar with this part of the code, but is it not necessary to nwPointer.Set(m.DefaultClass) here?
There was a problem hiding this comment.
This will work as well, since there's only one DefaultClass field so assigning to it will do the same as using the Set of that field's pointer, but what you suggest looks better. I will change that in the follow-up PR.
The pure moves are just |
Follow-up of #4059 ### Changes - No longer let the error message "Error: the included file <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`. ### Testing - Updated existing test expect files for the change in included file error reporting <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>
Parser.Parseno longer takes the default module as an argument which it then appends to, but instead returns a new typeFileModuleDefinition, which acts as a container for file contents.SourceProcessor.ProcessDirectivesnow makes sure not to remove or add newlines at the end of the file.Clonerand into the module classes.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.