Repository navigation
Add design brief for for/while loop sugar over Loop - #12085
Merged
Merged
Conversation
…efault Adds gunbc.plans.for_while_loop_sugar, a hand-off design brief in the shape of the blackjack onboarding brief, registered in batch_g. for and while add no core behavior: carrier-free for lowers to map, a carrier lowers to fold through the existing fold seam, a decreasing while lowers to Loop with a proven measure or refuses, and while true reuses the existing loop N form with std.computation forever_iteration_bound. Iterations are independent unless a carrier or an effect couples them; parallel realization stays a separate, later change. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QBhtZJTkWo5Lf2TmCDJP35
for lowers to a carrier-less Loop, not through list_map, whose fold_list_right body installs the carrier the design exists to avoid. A range index is a coordinate, not state. while is an explicit state transition with a Bool guard and a proven measure; while(xs) and while(true) are refused with named alternatives; repeat ... up_to: N is the explicit budget with a typed exhaustion arm; long-lived services are a separate lifecycle design. Results and diagnostics are ordered by domain position under every permitted schedule. reduce and scan are named as gated frontiers rather than minted. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QBhtZJTkWo5Lf2TmCDJP35
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8252dd86e1
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…erence docs/plans/for-while-loop-sugar.md is the gunbc.plan expected_plan_md projection of gunbc.plans.for_while_loop_sugar. The spelling decision points at section 12 Q2 rather than the deviations table, and the admitted/refused table no longer carries an empty cell. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QBhtZJTkWo5Lf2TmCDJP35
Ledger-Repair-Judged: docs/design-rung-drops.md Heal-Candidate-Run: 35798178176
Review held the brief because it described a Loop the substrate cannot represent. This cut adds S0: one optional ^loop_domain_edge on Loop (no seventh behavior), the carrier edge keeps its single binder meaning with initial state from an enclosing Bind, and result assembly is fixed by which edges are present. The existing state is stated honestly: the grammar is unary loop <expr>, both Loop interpreters reject, and the fold seam carries neither the list nor init (its migration is S3). repeat is withdrawn (no budget path, uninhabited completed arm). The per-loop termination proof gets four named joins and one producer in v2.std.cardinality that loop_multiplicity and inferred_facts_descent both read. S1 admits List<T> only. The construct guarantees no implicit positional edge; independence is derived, and unresolved coupling is refused for parallelism rather than serialized. The unauthorable reduction-shaped-body diagnostic is deleted, and EffectPlanStep.For gets a stated divergence beside While's conformance. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QBhtZJTkWo5Lf2TmCDJP35
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This adds a design brief for implementing
forandwhileas frontend sugar over the existingLoopbehavior. It is a hand-off document in the shape of the blackjack onboarding brief, and it implements nothing.dag/gunbc/plans/for_while_loop_sugar.dagis the authority, registered ingunbc.plan_registry_batch_g.docs/plans/for-while-loop-sugar.mdis its projection, rendered bygunbc.planexpected_plan_md. Its.gitattributesmerge-driver row is included.The design, as of the third cut
^loop_domain_edgeonLoopinstead of a seventh behavior. The carrier edge stays a binder, and initial state comes from an enclosingBind. Result assembly is fixed by which edges are present. The brief states the current substrate as it is:loop <expr>;Loopinterpreters reject;init.foroverList<T>only. It lowers directly to the domain encoding, never throughlist_map. The body must be pure. The construct contributes no implicit positional edge between members.while. It needs aBoolguard and a measure proven to decrease on a domain that can't decrease forever. The brief names four pieces the termination proof needs and one producer inv2.std.cardinality, whichloop_multiplicityandinferred_facts_descentboth read.EffectPlanStep.Whileshares the same measure.EffectPlanStep.Forgets a stated divergence.while (xs)andwhile (true).Review history
forthroughlist_map, which is built onfold_list_rightand would have installed a carrier.Loopshape the substrate cannot represent;repeatthat could not execute;🤖 Generated with Claude Code
https://claude.ai/code/session_01QBhtZJTkWo5Lf2TmCDJP35