Skip to content

Add information required for LSP features to Parse AST#764

Merged
marcoeilers merged 43 commits into
masterfrom
sem-highlight
Feb 11, 2024
Merged

Add information required for LSP features to Parse AST#764
marcoeilers merged 43 commits into
masterfrom
sem-highlight

Conversation

@JonasAlaif

Copy link
Copy Markdown
Contributor

There are still some failing tests

@marcoeilers

Copy link
Copy Markdown
Contributor

I really feel like the code is mixing things that should not be mixed.
IMO most of the lsp package should not be in Silver, and the ParseAST should not extend LSP-related classes or traits.
Couldn't you define the connection between the ParseAST classes and the LSP classes separately?
Or, if that would be a problem for plugins or extensions or something like that: Can't we define a couple of classes that provide general, high-level semantic information about PAST nodes, which plugins or extensions could then also use, and which one could then translate into LST concepts?

@JonasAlaif

Copy link
Copy Markdown
Contributor Author

Alright @marcoeilers this is pretty much final and ready to be merged (will require some small changes of tests in the silicon repo)

@JonasAlaif

Copy link
Copy Markdown
Contributor Author

@marcoeilers baring any bugs this is now final

@JonasAlaif

JonasAlaif commented Feb 9, 2024

Copy link
Copy Markdown
Contributor Author

I really don't understand why the carbon tests are failing though...

[info] - all/issues/silver/0165.vpr [carbon-Silver] *** FAILED *** (2 milliseconds)
[info]   2 errors
[info]   
[info]   The following output occurred during testing, but should not have according to the test annotations:
[info]     [parser.error] Parse error: Expected (annotation | fail | StringIn("import", "define", "field", "method", "domain", "function", "predicate") | adtDecl):4:21, found "b () { }". Occurred while parsing: annotated:4:21 (0165.vpr@5.21)
[info]   
[info]   The following outputs were expected according to the test annotations, but did not occur during testing:
[info]     parser.error (0165.vpr:5) (AnnotationBasedTestSuite.scala:63)
[info]   + Verifier used: carbon 1.0. 
[info]   + Time required: 1 msec (Parsing), 0 msec (Semantic Analysis), 0 msec (Translation), 0 msec (Consistency Check), 0 msec (Verification). 

Like expected parser.error (0165.vpr:5) and got [parser.error] ... (0165.vpr@5.21) why do these two no longer match...?

@marcoeilers

marcoeilers commented Feb 9, 2024

Copy link
Copy Markdown
Contributor

The problem seems to be that the reported error has a FilePosition but the code (isSameLine in SilOutput) that compares positions expects a SourcePosition.

@marcoeilers marcoeilers left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Few small questions and some comments that can be dropped

Comment thread src/main/scala/viper/silver/ast/Program.scala
Comment thread src/main/scala/viper/silver/ast/utility/Consistency.scala Outdated
Comment thread src/main/scala/viper/silver/ast/utility/Expressions.scala Outdated
Comment thread src/main/scala/viper/silver/ast/utility/lsp/Builtin.scala Outdated
Comment thread src/main/scala/viper/silver/parser/ParseAst.scala Outdated
Comment thread src/main/scala/viper/silver/parser/ParseAst.scala
Comment thread src/main/scala/viper/silver/parser/ParseAst.scala Outdated
Comment thread src/main/scala/viper/silver/parser/ParseAst.scala Outdated
Comment thread src/main/scala/viper/silver/parser/ParseAst.scala Outdated
Comment thread src/main/scala/viper/silver/parser/ParseAst.scala Outdated
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants