Skip to content

Parse proc declarations and specification clauses#977

Merged
jsiek merged 1 commit into
mainfrom
codex/issue-962-proc-declarations
Jun 13, 2026
Merged

Parse proc declarations and specification clauses#977
jsiek merged 1 commit into
mainfrom
codex/issue-962-proc-declarations

Conversation

@jsiek

@jsiek jsiek commented Jun 13, 2026

Copy link
Copy Markdown
Owner

Summary

  • Add Proc/ProcParam/ProcSpec AST nodes that preserve typed and ghost params, optional returns, and repeated specification clauses.
  • Parse proc declarations in both RD and LALR, including requires, labeled/unlabeled ensures, reads, modifies, and decreases clauses with an empty body placeholder.
  • Reject proc declarations during checking with a clear parser/AST-only unsupported diagnostic, plus fixture and parser round-trip coverage.

Closes #962

Tests

  • make tests

Codex session
codex://threads/019ebf56-ac4d-7e61-8d30-b6fc4873c945

open 'codex://threads/019ebf56-ac4d-7e61-8d30-b6fc4873c945'

@jsiek jsiek force-pushed the codex/issue-962-proc-declarations branch from e21a21a to 898ca42 Compare June 13, 2026 17:50
@jsiek jsiek marked this pull request as ready for review June 13, 2026 17:52
@jsiek jsiek merged commit 4d5e159 into main Jun 13, 2026
9 checks passed
@jsiek jsiek deleted the codex/issue-962-proc-declarations branch June 13, 2026 17:58
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.

Phase 1c: Parse proc declarations and specification clauses

1 participant