Comments (10)
For consistency, it seems we should go with your first PR. Please capture our discussion and reasoning above in code comments so that our future self will know why the change was made?
from pluspy.
Thanks for your contribution!
from pluspy.
Hallo! Can I do this one?
from pluspy.
Sure, please go ahead and open a PR.
from pluspy.
Thanks! Here it is. #8
Edit: WIP
from pluspy.
I have pushed two PRs with two different solutions.
I am new to this stuff and do not have wisdom to choose the right solution. Please, help. :-)
-
Discard preamble after lexing
https://github.com/tlaplus/PlusPy/pull/8/files -
Add optional preamble matching rule in the parser
https://github.com/tlaplus/PlusPy/pull/9/files
PS: I am happy to discard them both if they are wrong. Apologies for the spam. 🙏
from pluspy.
Please explain the difference between the two PRs in more detail.
from pluspy.
Hallo!
As usual, the lexer scans the string, produces tokens, and feeds them to the parser.
Parser expects the first four tokens to be tok("----")
, tok("MODULE")
, Name()
and tok("----")
(the module start tokens).
When there is a preamble, the parser fails with ..."tok: no match with '----'"...
, because the lexer's output has words from the preamble as the first tokens.
This gives us two options.
- Fix the lexer's output.
The first PR removes all the tokens before the module start tokens at the end of lexing. This will satisfy the parser's expectations.
The lexer skips over the comments. We can treat the preamble like comments because it is
not useful later. (Q1) Why forward its tokens to the parser and complicate the code there?
- Fix the parser's expectations.
The second PR changes the parser's expectations. It makes parser expect optional preamble tokens before the module start tokens. It does exactly the same thing as the other PR (to discard any tokens before the module start tokens) but in the parsing phase instead of doing it at end of the lexing phase.
(Q2) Why should we give any more intelligence to the lexer other than what it needs to just make the tokens?
Because of the questions Q1 and Q2, I do not know how to choose.
Hope this helps. Thanks!
from pluspy.
Do you know how the rest of the PlusPy lexer/parser handle comments that are inside the TLA+ module?
from pluspy.
Lexer ignores all the comments inside or outside of the module so the parser doesn't have to deal with them at all.
In lexer code,
For example, comments in the foo.tla
don't have any tokens in the lexer output.
foo.tla
\* No tokens for this
---- MODULE Foo -----
\* No tokens for this
\* Not a token sir!
VARIABLE x
(* This is a box comment
and it will be ignored too.
*)
(**********************************************************************)
(* This too should be ingored by the lexer. *)
(**********************************************************************)
TypeOK ==
/\ x < 10
Init ==
/\ x = 0
\* and this too don't generate no tokens
Next ==
/\ x' = x + 1
Spec == Init /\ [][TypeOK /\ Next]_<<x>>
====
Lexer output:
[('----', ('./tests/foo.tla', 4), 1, True), ('MODULE', ('./tests/foo.tla', 4), 6, False), ('Foo', ('./tests/foo.tla', 4), 13, False), ('----', ('./tests/foo.tla', 4), 17, False), ('VARIABLE', ('./tests/foo.tla', 9), 1, True), ('x', ('./tests/foo.tla', 9), 10, False), ('TypeOK', ('./tests/foo.tla', 19), 1, True), ('==', ('./tests/foo.tla', 19), 8, False), ('/\\', ('./tests/foo.tla', 20), 5, True), ('x', ('./tests/foo.tla', 20), 8, False), ('<', ('./tests/foo.tla', 20), 10, False), ('10', ('./tests/foo.tla', 20), 12, False), ('Init', ('./tests/foo.tla', 22), 1, True), ('==', ('./tests/foo.tla', 22), 6, False), ('/\\', ('./tests/foo.tla', 23), 5, True), ('x', ('./tests/foo.tla', 23), 8, False), ('=', ('./tests/foo.tla', 23), 10, False), ('0', ('./tests/foo.tla', 23), 12, False), ('Next', ('./tests/foo.tla', 28), 1, True), ('==', ('./tests/foo.tla', 28), 6, False), ('/\\', ('./tests/foo.tla', 29), 5, True), ('x', ('./tests/foo.tla', 29), 8, False), ("'", ('./tests/foo.tla', 29), 9, False), ('=', ('./tests/foo.tla', 29), 11, False), ('x', ('./tests/foo.tla', 29), 13, False), ('+', ('./tests/foo.tla', 29), 15, False), ('1', ('./tests/foo.tla', 29), 17, False), ('Spec', ('./tests/foo.tla', 31), 1, True), ('==', ('./tests/foo.tla', 31), 6, False), ('Init', ('./tests/foo.tla', 31), 9, False), ('/\\', ('./tests/foo.tla', 31), 14, False), ('[]', ('./tests/foo.tla', 31), 17, False), ('[', ('./tests/foo.tla', 31), 19, False), ('TypeOK', ('./tests/foo.tla', 31), 20, False), ('/\\', ('./tests/foo.tla', 31), 27, False), ('Next', ('./tests/foo.tla', 31), 30, False), (']_', ('./tests/foo.tla', 31), 34, False), ('<<', ('./tests/foo.tla', 31), 36, False), ('x', ('./tests/foo.tla', 31), 38, False), ('>>', ('./tests/foo.tla', 31), 39, False), ('====', ('./tests/foo.tla', 32), 1, True)]
from pluspy.
Related Issues (3)
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from pluspy.