Skip to content
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

subrule fixes and Menhir backend improvements #127

Open
wants to merge 14 commits into
base: master
Choose a base branch
from

Conversation

SergioBenitez
Copy link

This PR includes several commits that collectively address various issues with subrule handling across backends, improve the Menhir backend's correctness, and update regression testing infrastructure. Changes include:

  1. Subrule Fixes
  • Coalesce subrule bounds/conditions to eliminate redundant constraints (d3acdac).
  • Fix treatment of subrule aliasing which resulted in missing subrule checks in generated code (803bce7).
  • In general, these are fixes to how subrules are handled in proof assistant backends to properly handle aliases and hierarchies, resolving cases where Ott generated entirely incorrect code (missing subrules/invalid types).
  1. Menhir Backend Fixes
  • Properly handle subrules by keeping only the maximal element in a subrule hierarchy (e89b0a4).
  • Fix generation of non-string type parsing (int/float/bool) that caused invalid code generation (cb0c678).
  • Adds tests for subrules and primitive types, including previously failing cases (b887eac, 8506ddc).
  1. Infrastructure & Testing
  • Pin Coq to 8.20 in CI and update regression baselines.
  • Use proper exit codes on regression test failure (f7ca37b)
  • Update regression tester for OCaml 5.3 and Coq 8.19+ compatibility (ede3291, b2b9863)
  • Fix incorrect parsing in test21.1.ott

All regression tests pass, including those newly added.

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.

2 participants