Skip to content

Conversation

@SergioBenitez
Copy link

Closes #126.

SergioBenitez and others added 14 commits March 27, 2025 00:07
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