8000 [parser] initialization based on Loc.t rather than Loc.source by gares · Pull Request #9830 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

[parser] initialization based on Loc.t rather than Loc.source #9830

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Mar 29, 2019

Conversation

gares
Copy link
Member
@gares gares commented Mar 25, 2019

In this way one can also set the current offsets in a file,
useful if you are parsing a Coq fragment within a file instead
of a full file starting from the first line.

@gares gares requested review from ejgallego, mattam82 and a team as code owners March 25, 2019 16:32
@gares
Copy link
Member Author
gares commented Mar 25, 2019

This PR is orthogonal to #9733 but complements the feature it provides. In particular to parse anti quotations and get errors with the right Loc.t, one needs to tell Coq where the text begins.

For the reviewers: The old code was storing the file name (Loc.source) in the lexer state and was using it only to generate the initial_loc from which the tokenizing function was starting. I removed this global data, and pass the initial loc to the tokenizing function factory, that grabs it in its closure. No need to have the file name as part of the imperative lexer state anymore.

@gares gares added this to the 8.10+beta1 milestone Mar 25, 2019
@gares gares added the kind: cleanup Code removal, deprecation, refactorings, etc. label Mar 25, 2019
@gares gares force-pushed the parser-init-loc branch from 69f1e66 to 4768b53 Compare March 25, 2019 16:40
@ejgallego ejgallego self-assigned this Mar 25, 2019
@ejgallego ejgallego added the kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. label Mar 25, 2019
Copy link
Member
@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

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

This is without a doubt very useful; I think the current interface should play well with the state; even if cLexer is exposing unfortunately unsafe primitives.

The initial location should be factored to an utility function tho.

I'll let some time for @ppedrot @herbelin to comment, otherwise I'll merge.

@ejgallego ejgallego requested review from ppedrot and herbelin March 25, 2019 18:04
@gares gares force-pushed the parser-init-loc branch 2 times, most recently from 391ecc0 to 4016af2 Compare March 26, 2019 09:51
@gares
Copy link
Member Author
gares commented Mar 28, 2019

ping

@ejgallego
Copy link
Member

We got a conflict, please rebase; will merge this WE.

@ejgallego ejgallego added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Mar 28, 2019
In this way one can also set the current offsets in a file,
useful if you are parsing a Coq fragment within a file instead
of a full file starting from the first line.
@gares gares force-pushed the parser-init-loc branch from 4016af2 to 7eba2df Compare March 29, 2019 10:05
@gares gares removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Mar 29, 2019
@gares
Copy link
Member Author
gares commented Mar 29, 2019

done.

The conflicts was trivial, I think we could avoid the ping pong between author and assignee in these cases.
I'll try to talk about that at the next WG.

@ejgallego ejgallego merged commit 7eba2df into rocq-prover:master Mar 29, 2019
ejgallego added a commit that referenced this pull request Mar 29, 2019
…c.source

Reviewed-by: ejgallego
Ack-by: gares
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: cleanup Code removal, deprecation, refactorings, etc. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants
0