Skip to content

RFC-6: full words for clause keywords, and the effect row on the arrow #128

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.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We鈥檒l occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
maxinelevesque wants to merge 1 commit into
base: rfc/process-and-migration
Choose a base branch
from
Open

RFC-6: full words for clause keywords, and the effect row on the arrow #128

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
96 changes: 96 additions & 0 deletions .design/reqs/registry.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17757,3 +17757,99 @@ note = "registry reader"
kind = "file"
target = ".design/reqs/registry.toml"
note = "the registry the link resolves against"

[[requirement]]
id = "REQ-SYNTAX-CLAUSE-FULL-WORDS"
title = "Clause keywords are full words"
owner = ".design/rfcs"
status = "not_started"
scope = "syntax"
summary = "req/ens/inv/dec are spelled requires/ensures/keeps/measures, so a clause keyword carries the pretraining prior its meaning deserves."
remaining_scope = "Rename five entries in keyword_kind, keeping the TokKind variant names so downstream references do not move, and rename the clause names carried as strings in parser diagnostics. Proposed by RFC-6; not accepted."
contributors = [".design/rfcs/0006-full-words.md"]
generated_to = ["status"]

[[requirement.evidence]]
kind = "doc"
target = ".design/rfcs/0006-full-words.md"
note = "the proposal, with the rename table and the clause-grammar rule that chose keeps and measures"

[[requirement]]
id = "REQ-SYNTAX-EFFECT-ROW-LEADING"
title = "The effect row leads the contract, spelled `!`"
owner = ".design/rfcs"
status = "not_started"
scope = "syntax"
summary = "fx E becomes ! E at the head of the contract, marking the row as part of the arrow rather than a claim about behaviour."
remaining_scope = "Accept the row first in parse_contract and drop fx as a keyword; `!` already lexes as TokKind::Bang, so no new token is needed. Proposed by RFC-6; not accepted."
contributors = [".design/rfcs/0006-full-words.md"]
generated_to = ["status"]

[[requirement.evidence]]
kind = "doc"
target = ".design/rfcs/0006-full-words.md"
note = "the position argument, and the measurement that 142 lines open with a row and none open with a `!` that is not one"

[[requirement]]
id = "REQ-SYNTAX-CLAUSE-ORDER"
title = "Clause order: row, bare clauses, measures last"
owner = ".design/rfcs"
status = "not_started"
scope = "syntax"
summary = "The contract is ordered the effect row, then the bare clauses, then measures, and one or more requires is accepted to match ensures."
remaining_scope = "Reorder the parse_contract state machine. Today it enforces req x1, ens x1+, fx x1, with a recursive fn carrying dec after the row. Proposed by RFC-6; not accepted."
contributors = [".design/rfcs/0006-full-words.md"]
generated_to = ["status"]

[[requirement.evidence]]
kind = "doc"
target = ".design/rfcs/0006-full-words.md"
note = "the ordering rule, checkable without knowing anything semantic"

[[requirement]]
id = "REQ-SYNTAX-CLAUSE-CONJUNCTS"
title = "A clause body may be a block of conjuncts"
owner = ".design/rfcs"
status = "not_started"
scope = "syntax"
summary = "requires { a; b; } desugars to repeated clauses, with the bare single-expression form as sugar, so a per-obligation proof hint has somewhere to attach."
remaining_scope = "Add the production and desugar it in the parser; nothing downstream of the AST needs to know about it. This is the only part of RFC-6 that adds a production rather than renaming a token. Proposed by RFC-6; not accepted."
contributors = [".design/rfcs/0006-full-words.md"]
generated_to = ["status"]

[[requirement.evidence]]
kind = "doc"
target = ".design/rfcs/0006-full-words.md"
note = "the production, and why it belongs in a syntax-only change"

[[requirement]]
id = "REQ-SYNTAX-CLAUSE-TRIVIAL"
title = "`requires nothing` for a trivial clause"
owner = ".design/rfcs"
status = "not_started"
scope = "syntax"
summary = "requires nothing is clause-level sugar for requires true, leaving true legal inside expressions."
remaining_scope = "Accept the keyword in clause position. Adoption across the 100 existing req true sites is a second pass rather than a correctness condition, since a naive rewriter emits requires true and that stays legal. Proposed by RFC-6; not accepted."
contributors = [".design/rfcs/0006-full-words.md"]
generated_to = ["status"]

[[requirement.evidence]]
kind = "doc"
target = ".design/rfcs/0006-full-words.md"
note = "the sugar, and the note that ensures nothing parses and is then refused by 7.1(a) as EnsIsTrivial"

[[requirement]]
id = "REQ-SYNTAX-ADDRESS-CLAUSE-SEGMENTS"
title = "Address segments follow the clause rename"
owner = ".design/rfcs"
status = "not_started"
scope = "syntax"
summary = "validate_segments matches the renamed clause keywords, keeping a semantic address and a clause keyword the same word."
remaining_scope = "Rename the segments in the two fixed allowlists in address.rs. This is also why a clause keyword must be one word: a space-bearing segment is rejected as malformed before any lookup. Proposed by RFC-6; not accepted."
contributors = [".design/rfcs/0006-full-words.md"]
generated_to = ["status"]

[[requirement.evidence]]
kind = "doc"
target = ".design/rfcs/0006-full-words.md"
note = "the allowlist lines, and the address-segment constraint that ruled out `terminates by`"
6 changes: 6 additions & 0 deletions .design/reqs/status.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -441,6 +441,7 @@ Source: `.design/reqs/registry.toml`
| REQ-STRING-SUBSTRING-PREDICATES | shipped | `thermite-lower/src/lower.rs` | `.design/basis/07-strings.md`, `thermite-spec/src/validator.rs`, `forge/tests/string_search_conformance.rs` | lower | String substring predicates | symbol: `emit_string_search_methods` - substring predicate method emitter<br>symbol: `emit_string_search_defs` - substring predicate spec emitter<br>test: `forge/tests/string_search_conformance.rs` - substring predicate conformance | |
| REQ-STRING-TRIM | shipped | `thermite-lower/src/lower.rs` | `.design/basis/07-strings.md`, `thermite-spec/src/validator.rs`, `forge/tests/string_search_conformance.rs` | lower | String trim operation | symbol: `emit_string_search_methods` - trim method emitter<br>symbol: `GENERATED_SPEC_FNS` - validator admits `is_space`<br>test: `forge/tests/string_search_conformance.rs` - trim conformance | |
| REQ-STRING-U64-TO-STRING | shipped | `thermite-lower/src/lower.rs` | `.design/basis/07-strings.md`, `thermite-spec/src/validator.rs`, `forge/tests/string_format_conformance.rs`, `forge/tests/divergence_numfmt_display_order.rs` | lower | u64 decimal formatting with round-trip contract | symbol: `emit_numfmt_defs` - decimal formatter and round-trip spec emitter<br>symbol: `GENERATED_SPEC_FNS` - validator admits generated parse/format spec functions<br>test: `forge/tests/string_format_conformance.rs` - formatting L3 conformance<br>test: `forge/tests/divergence_numfmt_display_order.rs` - MSB-first display regression tooth | |
| REQ-SYNTAX-ADDRESS-CLAUSE-SEGMENTS | not_started | `.design/rfcs` | `.design/rfcs/0006-full-words.md` | syntax | Address segments follow the clause rename | doc: `.design/rfcs/0006-full-words.md` - the allowlist lines, and the address-segment constraint that ruled out `terminates by` | Rename the segments in the two fixed allowlists in address.rs. This is also why a clause keyword must be one word: a space-bearing segment is rejected as malformed before any lookup. Proposed by RFC-6; not accepted. |
| REQ-SYNTAX-ADDRESS-DEC | shipped | `thermite-syntax/src/address.rs` | `.design/syntax/semantic-addressing.md`, `thermite-syntax/tests/conformance.rs` | syntax | Semantic address dec segment | symbol: `emit_loop` - emits dec address entries<br>symbol: `AddrKind::Dec` - dec address kind<br>test: `thermite-syntax/tests/conformance.rs` - semantic address oracle | |
| REQ-SYNTAX-ADDRESS-DETERMINISTIC-RESOLVE | shipped | `thermite-syntax/src/address.rs` | `.design/syntax/semantic-addressing.md`, `thermite-syntax/tests/conformance.rs` | syntax | Semantic address bidirectional resolution | symbol: `resolve` - address-to-node resolver<br>symbol: `AddressError` - structured resolution error<br>test: `thermite-syntax/tests/conformance.rs` - bidirectional address conformance | |
| REQ-SYNTAX-ADDRESS-GRAMMAR | shipped | `thermite-syntax/src/address.rs` | `.design/syntax/semantic-addressing.md`, `thermite-syntax/tests/conformance.rs` | syntax | Semantic address grammar | symbol: `AddressEntry` - address entry carrier<br>symbol: `validate_segments` - address segment grammar validator<br>test: `thermite-syntax/tests/conformance.rs` - semantic address conformance | |
Expand Down Expand Up @@ -468,7 +469,12 @@ Source: `.design/reqs/registry.toml`
| REQ-SYNTAX-AST-PATTERN-TYPE-EFFECT | shipped | `thermite-syntax/src/ast.rs` | `.design/syntax/ast.md`, `thermite-syntax/src/parser.rs` | syntax | Pattern, type, and effect AST nodes | symbol: `Pattern` - pattern AST enum<br>symbol: `EffectRow` - effect row AST enum | |
| REQ-SYNTAX-AST-SLAG | shipped | `thermite-syntax/src/ast.rs` | `.design/syntax/ast.md`, `thermite-syntax/src/parser.rs` | syntax | Slag attribute AST node | symbol: `SlagAttr` - slag attribute node<br>symbol: `parse_slag_body` - slag parser arm | |
| REQ-SYNTAX-AST-SPANS | shipped | `thermite-syntax/src/ast.rs` | `.design/syntax/ast.md`, `thermite-syntax/src/address.rs` | syntax | Span-bearing AST boundary stability | symbol: `Span` - source span type<br>symbol: `Clause` - span and verbatim text carrier | |
| REQ-SYNTAX-CLAUSE-CONJUNCTS | not_started | `.design/rfcs` | `.design/rfcs/0006-full-words.md` | syntax | A clause body may be a block of conjuncts | doc: `.design/rfcs/0006-full-words.md` - the production, and why it belongs in a syntax-only change | Add the production and desugar it in the parser; nothing downstream of the AST needs to know about it. This is the only part of RFC-6 that adds a production rather than renaming a token. Proposed by RFC-6; not accepted. |
| REQ-SYNTAX-CLAUSE-FULL-WORDS | not_started | `.design/rfcs` | `.design/rfcs/0006-full-words.md` | syntax | Clause keywords are full words | doc: `.design/rfcs/0006-full-words.md` - the proposal, with the rename table and the clause-grammar rule that chose keeps and measures | Rename five entries in keyword_kind, keeping the TokKind variant names so downstream references do not move, and rename the clause names carried as strings in parser diagnostics. Proposed by RFC-6; not accepted. |
| REQ-SYNTAX-CLAUSE-ORDER | not_started | `.design/rfcs` | `.design/rfcs/0006-full-words.md` | syntax | Clause order: row, bare clauses, measures last | doc: `.design/rfcs/0006-full-words.md` - the ordering rule, checkable without knowing anything semantic | Reorder the parse_contract state machine. Today it enforces req x1, ens x1+, fx x1, with a recursive fn carrying dec after the row. Proposed by RFC-6; not accepted. |
| REQ-SYNTAX-CLAUSE-TRIVIAL | not_started | `.design/rfcs` | `.design/rfcs/0006-full-words.md` | syntax | `requires nothing` for a trivial clause | doc: `.design/rfcs/0006-full-words.md` - the sugar, and the note that ensures nothing parses and is then refused by 7.1(a) as EnsIsTrivial | Accept the keyword in clause position. Adoption across the 100 existing req true sites is a second pass rather than a correctness condition, since a naive rewriter emits requires true and that stays legal. Proposed by RFC-6; not accepted. |
| REQ-SYNTAX-COLLECTIONS-VEC | shipped | `thermite-syntax/src/ast.rs` | `.design/basis/04-collections.md`, `thermite-syntax/src/parser.rs`, `thermite-lower/tests/collections_conformance.rs` | syntax | Vec type surface AST | symbol: `Type::Vec` - Vec type node<br>test: `thermite-lower/tests/collections_conformance.rs` - collection conformance | |
| REQ-SYNTAX-EFFECT-ROW-LEADING | not_started | `.design/rfcs` | `.design/rfcs/0006-full-words.md` | syntax | The effect row leads the contract, spelled `!` | doc: `.design/rfcs/0006-full-words.md` - the position argument, and the measurement that 142 lines open with a row and none open with a `!` that is not one | Accept the row first in parse_contract and drop fx as a keyword; `!` already lexes as TokKind::Bang, so no new token is needed. Proposed by RFC-6; not accepted. |
| REQ-SYNTAX-ERGONOMICS-FOR | shipped | `thermite-syntax/src/parser.rs` | `.design/basis/11-ergonomics.md`, `thermite-syntax/src/ast.rs`, `forge/tests/ergonomics_conformance.rs` | syntax | For-loop desugar | symbol: `parse_for` - for-loop parser desugar<br>test: `forge/tests/ergonomics_conformance.rs` - for-loop conformance | |
| REQ-SYNTAX-ERGONOMICS-IF-WHILE-LET | shipped | `thermite-syntax/src/parser.rs` | `.design/basis/11-ergonomics.md`, `thermite-syntax/src/ast.rs`, `forge/tests/ergonomics_conformance.rs` | syntax | If-let and while-let desugars | symbol: `parse_if_let` - if-let parser desugar<br>symbol: `parse_while_let` - while-let parser desugar<br>test: `forge/tests/ergonomics_conformance.rs` - if-let and while-let conformance | |
| REQ-SYNTAX-ERGONOMICS-MATCH-GUARD | shipped | `thermite-syntax/src/ast.rs` | `.design/basis/11-ergonomics.md`, `thermite-syntax/src/parser.rs`, `forge/tests/ergonomics_conformance.rs` | syntax | Match guard surface AST | symbol: `MatchArm.guard` - optional match guard<br>test: `forge/tests/ergonomics_conformance.rs` - match guard conformance | |
Expand Down
Loading
Loading