Skip to content

add support for rocq 9.0#132

Open
SergioBenitez wants to merge 15 commits intoott-lang:masterfrom
formalstack:roq-9.0
Open

add support for rocq 9.0#132
SergioBenitez wants to merge 15 commits intoott-lang:masterfrom
formalstack:roq-9.0

Conversation

@SergioBenitez
Copy link

Closes #126.

SergioBenitez and others added 14 commits March 27, 2025 00:07
Co-authored-by: Joey Eremondi <joey.eremondi@gmail.com>
This fixes issues with subrules in the Menhir backend by:
1. Adding a syntaxdefn field to pp_menhir_opts in types.ml
2. Modifying suppress_rule to check if a nonterminal is non-maximal in
   the subrule hierarchy in lex_menhir_pp.ml
3. Adding a skip_subrule_validation parameter to check_and_disambiguate
   in grammar_typecheck.ml
4. Passing the appropriate flag when generating Menhir output in main.ml

The Menhir backend should 'only take the maximal elements from the
subrule order' as documented in the comments. This implementation
correctly suppresses non-maximal elements to ensure the generated parser
works properly with subrules.
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.

Add support for Rocq 9.0.0

2 participants