Skip to content

Conversation

@SergioBenitez
Copy link

This PR (which revives #127) 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