§ PR-γ : iccombs toy-harness (U-K-prelude ; TOY ; ¬ PD-binding) [stacked on PR-β]#10
§ PR-γ : iccombs toy-harness (U-K-prelude ; TOY ; ¬ PD-binding) [stacked on PR-β]#10Apocky wants to merge 1 commit into
Conversation
Lands the iccombs experimental demo-harness per IMPL_06_CORRIGENDUM § U-K-prelude : cssl-iccombs-toy-elab : surface λ-calculus → cssl-hgraph + grade-context + toy effect-row cssl-lower-iccombs : LINEAR fragment → cssl-iccombs interaction net (Lafont/Mackie SIC) cssl-iccombs-toy-cli : S-exp frontend + bin cssl-iccombs-toy INVARIANTS (per corrigendum) : ✗ NOT a production elaborator (production = cssl-hir per Wave U-B revised) ✗ NOT a production driver (production = csslc) ✗ NOT a PD-discipline gate (PD = cssl-caps + cssl-effects + cssl-ifc per Wave U-G revised) ✓ doc-headers + Cargo descriptions + bin-name carry TOY warning + corrigendum link GATES : cargo check ✓ · cargo test ✓ · cargo clippy --all-targets ✓ (3 toy crates + their deps) Stacks on : pr-beta/foundation-baseline (depends on cssl-cas + cssl-hgraph + cssl-grades + cssl-iccombs)
![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: 9e59c7a6d0
ℹ️ 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".
| Term::Var(name) => env | ||
| .get(name) | ||
| .copied() | ||
| .ok_or_else(|| LowerError::UnboundVar(name.clone())), |
There was a problem hiding this comment.
When cssl_lower_iccombs::lower is called directly on a malformed linear term such as (lam x L (app x x)), every occurrence gets the same saved PortRef, so the second occurrence reuses and relinks the binder port instead of being rejected; Net::link then overwrites one side of the previous connection and leaves stale one-way links in the net. Since lower is a public API advertised as lowering the linear fragment, it should consume/check the binding rather than returning the same port for repeated uses, or require a prior elaboration check in the API contract.
Useful? React with 👍 / 👎.
1 participant
§ Scope
Per
IMPL_06_CORRIGENDUM § U-K-prelude— iccombs experimental toy-harness. ‼ Not PD-binding. Explicitly TOY.‼ STACKED on PR-β
Base =
pr-beta/foundation-baseline(not target). Merge PR-β first. GitHub will re-target this tocssl/session-11/T11-W18-L8-DXIL-DIRECTautomatically once β lands.§ Deliverables (3 new crates)
cssl-iccombs-toy-elab— toy elaborator ; inlinedEffectRow { labels: BTreeSet<String> }withempty/singleton/union/is_pure/contains. ✗ Not the productioncssl-effectsrow. Header points at U-K-prelude.cssl-lower-iccombs— lowering pass from toy-elab IR → iccombs runtime. Doc + dep +userebrandedcssl_elab→cssl_iccombs_toy_elab. PD-discipline phrased as reference tocssl-caps+cssl-effects+cssl-ifc.cssl-iccombs-toy-cli(bin =cssl-iccombs-toy) — full rewrite. Drops all consent/grant/PD code. Keeps elab + optional--lower-iccombs/--reduce/--stdin.--helpprints "TOY ; not PD-binding".§ Invariants
cssl-caps+cssl-effects+cssl-ifc(see PR-β)-toy-infix +-iccombs-namespace)§ Gates
cargo checkcargo test— 10 passed / 0 failedcargo clippy --all-targets— zero warnings§ Dependencies