Skip to content

Parse complete v0 definitions - #136

Merged
alexlopashev merged 2 commits into
mainfrom
codex/definition-source-parser
Jul 20, 2026
Merged

Parse complete v0 definitions#136
alexlopashev merged 2 commits into
mainfrom
codex/definition-source-parser

Conversation

@alexlopashev

@alexlopashev alexlopashev commented Jul 20, 2026

Copy link
Copy Markdown
Contributor

Closes #100

Outcome

  • parse §type, general §function, §predicate, and standalone §refines definitions into closed deterministic canonical AST
  • retain definition order, exact spans, generic bounds, parameter binders, nominal references, algebraic and collection types, handles, refinements, effect rows, and verifier arguments
  • reject duplicate, malformed, reserved-binder, and unsupported forms before artifact emission while keeping executable lowering explicitly closed for Implement the complete v0 value, type, subtyping, and refinement checker #103Elaborate general functions, predicates, and canonical verifier bindings #105
  • preserve existing canonical fixture bytes, the historical duplicate-policy diagnostic, profile-selected formatting, and the reference-program unsupported-syntax boundary

Red-to-green evidence

Initial red: mise exec -- cargo test --test pipeline complete_definition_forms_build_a_closed_schema_valid_ast -- --exact failed at definitions.bhcp:1:58 with BHCP0001 unexpected character ?.

Review red: generic Text and value true could be declared as binders but resolved as a primitive/literal instead. Exact regression cases now reject both declarations with BHCP1001 reserved-spelling diagnostics, while ordinary T retains a parameter-shaped result AST.

Green focused:

  • mise exec -- cargo test --test pipeline — 8 passed
  • mise exec -- cargo test --test policy_parser — 8 passed
  • mise exec -- cargo test --test profile_formatting — 6 passed
  • mise exec -- cargo test --test v0_completion_contract — 4 passed

Full validation

  • mise exec -- cargo fmt --check
  • mise exec -- cargo clippy --all-targets -- -D warnings
  • mise exec -- cargo test --all-targets
  • mise exec -- cargo build --release
  • mise exec -- cargo test --test schema_fixtures — 7 passed

All passed on exact head c078e4a.

Documentation impact

README now distinguishes complete parser/AST coverage from the deliberately deferred checker and semantic-IR elaboration work.

Residual risk

The complete expression and pattern calculus, general checking, and function/predicate/verifier elaboration remain intentionally blocked into #104, #103, and #105. Newly parsed definitions therefore fail closed with BHCP2004 if executable lowering is requested.

Comment thread src/parser.rs
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.

Independent review task identity: /root/review_pr_88

Reviewed exact head 73a33c6b48c2f3aee12dd74740b0388ab1076044 against SEMANTICS.md S3–S7, issue #100, the canonical AST boundary, existing profile/policy compatibility, and the full PR diff.

The focused parser/policy/profile/completion suites pass, the complete canonical local gate passes, git diff --check is clean, all hosted checks are green, and the remote head remained exact. However, adversarial binder probes show two accepted sources whose local binders are silently captured by built-in/literal parsing, violating alpha-renaming and reserved-keyword requirements. The inline P1 findings are merge blockers. I did not approve or merge; the shared GitHub account cannot supply author-independent approval.

@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 re-review by /root/review_pr_88 at c078e4a: no remaining actionable findings.

Verified both prior P1 findings are fixed by the closed reserved-binder check. Independent probes reject built-in/literal capture in type parameters, function and predicate parameters, verifier argument names, refinement binders, and effect-row tails with BHCP1001; an ordinary <T>(value: T): T = value case succeeds and retains parameter-shaped AST nodes.

Focused parser, policy parser, profile-formatting, and v0 completion-contract tests pass. The complete canonical local gate passes (cargo fmt --check, strict all-target Clippy, all-target tests, release build, and schema fixtures), git diff --check is clean, and all hosted checks are green for this exact head.

@alexlopashev
alexlopashev merged commit 1bc5a8d into main Jul 20, 2026
12 checks passed
@alexlopashev
alexlopashev deleted the codex/definition-source-parser branch July 20, 2026 19:39
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 type, function, predicate, and refinement definitions

1 participant