Add position info to DDM. #112
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
joehendrix
force-pushed
the
jhx/position_info
branch
9 times, most recently
from
ea232b3 to
338c03d
Compare
joehendrix
force-pushed
the
jhx/position_info
branch
5 times, most recently
from
f8f0277 to
18af9f2
Compare
joehendrix
force-pushed
the
jhx/position_info
branch
2 times, most recently
from
39fa709 to
8fabcd1
Compare
joehendrix
force-pushed
the
jhx/position_info
branch
2 times, most recently
from
6fb9ea4 to
9c54839
Compare
github-merge-queue bot
pushed a commit
that referenced
this pull request
Oct 6, 2025
This introduces a datatype for a range of characters in a source file. It will be used for embedding source information in the AST for #112 , but is currently only being added to info trees. This PR also removes the extra syntax elements from error handling as messages contain source information. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
joehendrix
force-pushed
the
jhx/position_info
branch
2 times, most recently
from
b29241e to
898ec58
Compare
joehendrix
force-pushed
the
jhx/position_info
branch
from
898ec58 to
a2b89bb
Compare
github-merge-queue bot
pushed a commit
that referenced
this pull request
Oct 21, 2025
This is a large PR that makes DDM changes to support source location information in #112. * Updates SyntaxCat to use a structure instead of algebraic data type. This improves efficiency of accessing head. * ArgDecls is a singleton structure instead of type abbreviation and coercisions with array no longer allowed. This will allow additional invariants to be added such as uniqueness of names. * There is additional checking for undefined names to reduce spurious errors when module imports cannot be found. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
joehendrix
force-pushed
the
jhx/position_info
branch
from
a2b89bb to
b424444
Compare
joehendrix
requested review from
andrewmwells-amazon,
aqjune-aws,
atomb and
shigoel
as code owners
aqjune-aws
reviewed
Oct 24, 2025
There was a problem hiding this comment.
-
I checked that
byteIdxis correctly appearing by probing a random example, specifically by running#eval Command.ofAst example1.commands[0]at StrataTest/DDM/Comment.lean . However, I found that thebyteIdxis counted from the beginning of the .lean file, not from the beginning of#strata. Which option should we choose? -
I found that Examples/Lean/BoogieLite.lean was breaking again. Should we add
lake build StrataExamples..? On my Mac, this command seems to fail for other reasons as well, however.
aqjune-aws
approved these changes
Oct 27, 2025
shigoel
approved these changes
Oct 27, 2025
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a large PR that adds the ability to attach annotations to DDM subterms. This is used for source location information. This is inherently a large change since many operators need an additional argument and type level parameters are needed.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.