Skip to content

Complete canonical goal parsing - #137

Merged
alexlopashev merged 5 commits into
mainfrom
codex/complete-goal-parser
Jul 20, 2026
Merged

Complete canonical goal parsing#137
alexlopashev merged 5 commits into
mainfrom
codex/complete-goal-parser

Conversation

@alexlopashev

@alexlopashev alexlopashev commented Jul 20, 2026

Copy link
Copy Markdown
Contributor

Closes #101

Outcome

  • parse complete S7 goal headers, facts, contracts, authority, preferences, verifier bindings, executable cases, and standalone goal calls into closed canonical AST
  • retain full Goal<...> refinement types, typed arguments, quantifiers, recursive references, nested composition, source order, and exact spans
  • reject duplicate or incomplete new syntax atomically while preserving the existing executable all/any/none/chain/gate and explicit-compose routes
  • fail closed before executable IR for syntax whose checking, ownership/effect, recursion, graph, or planning semantics belong to later roadmap issues

Red-to-green evidence

Initial focused test:

cargo test --test goal_parser complete_goal_forms_build_a_closed_ordered_schema_valid_ast -- --exact

failed with BHCP1001: expected "{", found "<" at the goal type-parameter boundary. After implementation, cargo test --test goal_parser passes all 4 positive, compatibility, and malformed-boundary tests.

A compatibility regression was also caught during development: enriching legacy fact AST type attributes changed the pinned canonical AST bytes. The implementation now retains the existing byte shape for the executable slice and emits structured type shapes only for newly supported goal syntax; the pinned byte test is green.

Focused validation

  • cargo test --test goal_parser --test pipeline --test self_hosted_all --test self_hosted_chain --test self_hosted_gate --test verification
  • existing all/any/none/chain/gate suites were exercised again by the complete all-target gate

Full validation

  • cargo fmt --check
  • cargo clippy --all-targets -- -D warnings
  • cargo test --all-targets
  • cargo build --release
  • cargo test --test schema_fixtures

All pass at head 6201c9ddcd61fbf1c068a96817581d854b1ab2fc.

Documentation impact

README now distinguishes complete goal parsing from deferred checking/lowering. The conformance index maps the parser fixture to the authored prerequisites for KRN-11, REC-01..03, and PLN-03..05 without claiming their later semantics.

Residual risk

The complete parser intentionally does not claim static finiteness, name/type checking, ownership/effects, decreasing recursion proofs, graph construction, planning, or runtime behavior. Those remain fail-closed and are owned by subsequent blocked roadmap issues. The parser’s lookahead preserves the old executable route only for its exact simple-reference argument subset; general argument expressions take the new syntax-only route.

Review identity

Exact head submitted for independent review: 6201c9ddcd61fbf1c068a96817581d854b1ab2fc.

Comment thread src/parser.rs
Comment thread src/parser.rs Outdated
Comment thread src/parser.rs Outdated

@alexlopashev alexlopashev left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

[P1] Legacy composition still accepts duplicate branch tags and duplicate named arguments at src/parser.rs:2986 and src/parser.rs:3005; for example §all { same = example/C@0(); same = example/C@0(); }; parses successfully, unlike the new extended route. Apply the same duplicate and reserved-name validation without changing valid legacy bytes.

[P2] The preference parser at src/parser.rs:3264 does not match the S7 signed-integer grammar: §prefer -1: true; is rejected, while the non-EBNF label-before-priority form §prefer "p": 1: true; is accepted. Parse an optional sign and enforce priority-before-label order.

Independent exact-head review by /root/review_pr_88 on 26c4d3f. This review remains blocking together with the three inline threads until all counterexamples are covered.

Comment thread src/parser.rs Outdated
Comment thread src/parser.rs Outdated

@alexlopashev alexlopashev left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

[P2] src/parser.rs:3210 still unconditionally consumes the token after the last legacy composition argument instead of requiring ). §chain { child = example/C@0(value = source]; }; therefore consumes the mismatched ] and parses successfully. Replace it with expect(")")? and add the malformed-close regression; valid legacy bytes do not change.

Independent exact-head follow-up by /root/review_pr_88 on f257465. This and the literal-source inline P1 keep the head blocked.

@alexlopashev alexlopashev left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Independent exact-head approval by /root/review_pr_88 for 6201c9d: no remaining actionable findings.

Re-reviewed S7 goal headers, all clause payloads, labels and observable bindings, preferences, verifier/case forms, standalone calls, quantified and nested composition, legacy executable compatibility, and malformed boundaries. An independent adversarial matrix covering every reported counterexample passed. Focused parser, pipeline, algebra, and verification suites passed; the full canonical local gate passed; git diff-check is clean; all hosted checks including aggregate Tests are green; and all five review threads are resolved on the unchanged head.

The shared GitHub account cannot formally approve its own PR, so this comment records the independent reviewer task identity and exact reviewed head required by the repository workflow.

@alexlopashev
alexlopashev merged commit 3b3770a into main Jul 20, 2026
12 checks passed
@alexlopashev
alexlopashev deleted the codex/complete-goal-parser branch July 20, 2026 20:35
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.

Parse complete goals, clauses, nested composition, cases, and recursion

1 participant