Skip to content

Conversation

@joehendrix
Copy link
Contributor

@joehendrix joehendrix commented Sep 26, 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 joehendrix force-pushed the jhx/position_prep branch 5 times, most recently from d37a2e1 to 30088ad Compare September 26, 2025 08:28
@joehendrix joehendrix force-pushed the jhx/position_prep branch 4 times, most recently from ee4cd41 to ce6d583 Compare September 30, 2025 21:18
@joehendrix joehendrix force-pushed the jhx/position_prep branch 4 times, most recently from 099cabe to bd39758 Compare October 7, 2025 18:23
@joehendrix joehendrix marked this pull request as ready for review October 16, 2025 09:36
@joehendrix joehendrix requested review from a team, aqjune-aws and shigoel as code owners October 16, 2025 09:36
Copy link
Contributor

@aqjune-aws aqjune-aws left a comment

Choose a reason for hiding this comment

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

It seems the files in Examples/Lean have a few broken examples - should we fix these?

@aqjune-aws
Copy link
Contributor

I could confirm that the BoogieLite example is now fixed. :)

@shigoel shigoel added this pull request to the merge queue Oct 21, 2025
Merged via the queue into main with commit 3de5e26 Oct 21, 2025
10 checks passed
@shigoel shigoel deleted the jhx/position_prep branch October 21, 2025 14:30
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.

3 participants