From 758e1e1d848d8f76194ceaca2870665b1a1202b6 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 19 Jun 2026 23:08:50 +0000 Subject: [PATCH] feat(typecheck): detect duplicate function / type / agent declarations MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Roadmap item 1 (parser/typecheck gap-fill). Extends the `DuplicateDefinition` check from locale/choreography to the remaining name-bearing top-level decls. `fn`, `type`, and `agent` declarations were *gathered* but silently *last-win* on redefinition — two `fn f`, two `type T`, or two `agent A` were accepted with the second quietly shadowing the first. They now error. Detection is per parsed top-level declaration and within-kind, so an `agent Name(args)` reference inside a `supervisor children:` list (the agent-creates-agent pattern used by several examples) is NOT a declaration and is correctly not flagged. Verified against every example — zero false positives. 4 new typechecker tests (duplicate fn / type / agent, and the agent-reference-in-supervisor regression). 901 oo7-core lib tests pass; fmt + clippy clean. https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We --- .machine_readable/6a2/STATE.a2ml | 4 +- .machine_readable/session-log.txt | 2 + CHANGELOG.md | 1 + crates/oo7-core/src/typechecker.rs | 14 ++++-- crates/oo7-core/src/typechecker_tests.rs | 56 ++++++++++++++++++++++++ 5 files changed, 72 insertions(+), 5 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index dfac8b1..d9a4d43 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -6,8 +6,8 @@ @state(version="2.0"): phase: "implementation" -next_action: "Layer-10 rung 3b (cross-handler residues via agent state — partly runtime, ResidueCell/takeForReverse:Maybe). Also: extend duplicate-definition detection to the other name-bearing decls (functions/types/agents currently last-wins on redefinition). Rocq-9 proof-stack install in progress (see below) to run the rocq canonical-proof-suite locally." -last_action: "Governance + handover artifacts (branch claude/affirmation-and-handover): added AFFIRMATION.adoc (root, RSR-convention timestamped attestation of current standing — musts met, intends in_progress, blocked/open declared honestly), docs/status/must-intend-wish-2026-06-19.adoc (the full Echidna + 007 must/intend/wish tables), and docs/handover/NEXT-CLAUDE-PROMPT.md (paste-ready handoff with env gotchas). Followed confirmed RSR conventions (SPDX+AsciiDoc+a2ml attestation+contractile vocab); standards-repo AFFIRMATION template not retrievable (standards public but out of session MCP scope; web search 0 results). Banned-token-clean (reworded the believe_me/sorry/etc. examples). PRIOR completed this session: runner awk POSIX-portability fix \\s->[[:space:]] (PR #47 merged) — suite now runs locally; ROCQ 9.0 installed locally (OPAMROOT=/root/.opam3 switch rocq9, via github opam-repository mirror) → 35/37 canonical .v compile; last 3 (mathcomp chain + Coquelicot) walled by github-only network (menhir@gitlab.inria.fr, cmdliner@erratique.ch, coq-released@coq.inria.fr all 403) — CI-only. Echidna = unspecified ecosystem placeholder (no spec). Prior PRs: #46 (import+locale+choreography dup-detection), #45 (just gate), #43 (L10 proofs gated), #42 (rung-3a)." +next_action: "User roadmap (in order): (1) parser/typecheck gap-fill [DONE: function/type/agent dup-detection this branch] — remaining gap-fill candidates: the `trace { }` standalone-statement parse gap (semantic_analysis_example.007:71 fails), and extend dup-detection to protocols/behaviours/supervisors if wanted. (2) L10 RUNG 3b — cross-handler residues via agent state (partly runtime: residue cell in agent state + evaluator Holding/Spent, ResidueCell/takeForReverse:Maybe). (3) FULL PROOF SUITE GREEN — write M5-yoneda.agda (only agda entry, not-started/stub); the 3 rocq holdouts (M2 mathcomp, E1_ndim+S3_ndim Coquelicot) are CI-only by network policy. (4) CONSOLIDATE." +last_action: "Roadmap item 1 — extended DuplicateDefinition to FUNCTION/TYPE/AGENT (branch claude/dup-detection-fn-type-agent). These were gathered but silently last-win on redefinition; check_duplicate_definitions now flags two top-level fn/type/agent of the same name (within-kind, per parsed decl, so an `agent Name(args)` ref in a supervisor children: list is NOT a duplicate — verified no false positives across all examples). 4 new tests; 901 oo7-core lib pass; fmt+clippy clean. Also re-verified machine-checking with the local toolchain: ROCQ 35/38 .v compile (3 network-walled), AGDA 0/1 (M5-yoneda not-started), IDRIS2 16/16 incl L10 (EchoResidue+EchoResidueLinear). Prior this session: governance/handover docs (#48), runner awk fix (#47), Rocq 9 local (35/37), #46 import+locale+choreography dup-detection, #45 just gate. Echidna still unspecified placeholder." updated: 2026-06-19T21:45:00Z @blockers: diff --git a/.machine_readable/session-log.txt b/.machine_readable/session-log.txt index c92797c..653d1ef 100644 --- a/.machine_readable/session-log.txt +++ b/.machine_readable/session-log.txt @@ -41,3 +41,5 @@ [2026-06-18 13:20:34] Gap-fill (a): LOCALE + CHOREOGRAPHY duplicate-name detection on the same branch (extends PR #46 to "duplicate detection for the silently-skipped decls"). Added TypeErrorKind::DuplicateDefinition{kind,name} + check_duplicate_definitions pass (Pass 1c in check_program + _snapshot) flagging two same-named locale or choreography decls; agent_api DUPLICATE_DEFINITION (rename_or_remove). 3 tests (dup-locale, dup-choreography, distinct-locales-OK); 897 oo7-core lib pass; fmt+clippy clean; locales.007/choreography.007/imports.007 all still check OK. Ran cargo test directly (NOT just gate) to avoid assail polluting session-log. ROCQ-9 install attempt 3 progressing in background (/tmp/rocq3.log, OPAMROOT=/root/.opam3): github-mirror opam init succeeded, rocq9 switch building OCaml 4.14.2 then coq.9.0.0+mathcomp from github source; Coquelicot blocked (gitlab.inria.fr 403). [2026-06-19 21:47:43] Governance + handover artifacts (branch claude/affirmation-and-handover, off latest main 2c52cf6). User asked to (1) store the must/intend/wish status tables in-repo, (2) write a paste-ready prompt for the next 007 Claude, (3) make an AFFIRMATION.adoc per standards-repo guidance, timestamped. Delivered: AFFIRMATION.adoc (root) — RSR-convention attestation (SPDX+AsciiDoc+a2ml attestation ethos+contractile must/intend/wish vocab), timestamp 2026-06-19T21:43:26Z, commit 2c52cf6; affirms musts met (Harvard, L1-L10, honest proofs, RSR hygiene), labels intends in_progress (rung 3b, gap-fill, full suite) and the two owner-side blocks (Actions billing, github-only network) honestly. docs/status/must-intend-wish-2026-06-19.adoc — the full Echidna (thin: placeholder, no spec) + 007 tables. docs/handover/NEXT-CLAUDE-PROMPT.md — paste-ready handoff incl. env gotchas (billing-blocked CI+admin-merge, github-only network, OPAMROOT=/root/.opam3 rocq9 switch, assail-pollutes-session-log, branch/gate discipline). standards-repo AFFIRMATION template NOT retrievable (public but out of session MCP scope; web search 0 results; tree listings errored) so followed confirmed conventions + said so in the doc. Reworded believe_me/sorry/etc. examples out of the docs to stay banned-token-clean. Doc-only; A2ML 6a2 clean. Pushing -> draft PR. + +[2026-06-19 23:08:35] Roadmap item 1 (parser/typecheck gap-fill) — extend DuplicateDefinition to FUNCTION/TYPE/AGENT (branch claude/dup-detection-fn-type-agent off main). These three are gathered (gather_function/type/agent_decl) but silently last-win on redefinition; added Function/TypeDecl/Agent arms to check_duplicate_definitions (within-kind, keyed on (kind,name), per parsed top-level decl). SAFETY: text-grep flagged apparent dup agent names in 5 examples, but inspection showed the 2nd occurrence is always `agent Name(args)` in a supervisor children: list (a REFERENCE, not a top-level decl) — so the per-decl check ignores them; confirmed empirically (oo7 check on every example → zero false positives). 4 tests (dup fn/type/agent + agent-reference-in-supervisor-not-a-dup); fixed the regression snippet after learning `agent Name(args)` is only valid in supervisor children:, not as a control_stmt. 901 oo7-core lib pass (was 897); fmt+clippy clean. Also (answering user q on "done intra-body"): re-verified machine-checking with local provers — ROCQ 35/38 .v (3 walled: M2 mathcomp, E1_ndim+S3_ndim Coquelicot), AGDA 0/1 (M5-yoneda not-started), IDRIS2 16/16 incl L10. User roadmap remaining: (2) L10 rung 3b, (3) full proof suite green (write M5 agda; rocq holdouts CI-only), (4) consolidate. Pushing -> draft PR. diff --git a/CHANGELOG.md b/CHANGELOG.md index 2baea5d..5590787 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,6 +13,7 @@ All notable changes to this project will be documented in this file. - **`just gate` — one-command, billing-independent local green-check.** Runs every locally-faithful CI stage in sequence (rustfmt, clippy, `cargo test`, grammar-check, verify-harvard, e2e, `idris2 --check` of all 12 Idris proofs), continues past failures, and prints a per-stage PASS/FAIL/SKIP summary with a non-zero exit on any FAIL. Stages needing an absent toolchain (idris2) or an external GitHub action (A2ML/K9 validators, security scans) self-skip with a notice rather than failing, so it runs anywhere; the rocq canonical-proof-suite (needs Rocq 9) and external manifest/security scans stay CI/nightly-only. Verified GREEN on `main`. Distinct from `just ci` (build/test/lint/verify simulation) and `just check` (fast fmt/lint/test pre-commit). - **Import binding-collision detection.** The type checker now validates `import` declarations: every binding an import introduces — an `as` alias, each selective `from … import` item, or a bare `import a.b.c`'s last segment (`c`) — must be unique across the program. A collision (e.g. `import a as x` + `import b as x`, or `from m import abs, abs`) is now a `DuplicateImport` error instead of being silently accepted (imports were previously skipped by the gather pass entirely). Surfaced to agents via `agent_api` code `IMPORT_DUPLICATE_BINDING` (+`rename_import`/`remove_duplicate` remediations). Complements the existing `import_resolver` (which only detects *circular* imports). 4 new typechecker tests (894 `oo7-core` lib tests passing); `examples/imports.007` and the other import-bearing examples are unaffected. - **Duplicate locale / choreography detection.** `locale` and `choreography` declarations were likewise silently skipped by the gather pass, so two declarations sharing a name were accepted. Two `locale x = …` (or two `choreography y(…) { … }`) now raise a `DuplicateDefinition` error (agent_api code `DUPLICATE_DEFINITION`). 3 new typechecker tests (897 `oo7-core` lib tests passing); `examples/locales.007` and `examples/choreography.007` are unaffected. +- **Duplicate function / type / agent detection.** Extends `DuplicateDefinition` to the name-bearing decls that were *gathered but silently last-win* on redefinition: two top-level `fn f`, two `type T`, or two `agent A` now error. Detection is per parsed top-level declaration and within-kind, so an `agent Name(args)` reference in a `supervisor children:` list (the agent-creates-agent pattern) is correctly *not* a duplicate. Verified against every example (no false positives). 4 new typechecker tests (901 `oo7-core` lib tests passing; fmt + clippy clean). - **752 tests** (up from 207 at 0.5.0). CRG-C achieved 2026-04-04 for `oo7-core`. - **31 multi-language backends** via `mk2_bridge::create_backend_registry()`. Real dispatch to `elixir`, `idris2`, `gleam`, `rescript`, `nickel`, `guile`, `psql`, etc. Tier-5 coprocessor backends (CUDA/Vulkan/Metal/OpenCL/FPGA/TPU/DSP) do phase-1 device discovery with documented "kernel launch is future work" status. - **Metainterpreter** (`metainterpreter.rs`, ~3,075 LOC): reify/reflect/step/replay, four modes, 40 inline tests, 18 benches. diff --git a/crates/oo7-core/src/typechecker.rs b/crates/oo7-core/src/typechecker.rs index 42c2be8..1c7ba18 100644 --- a/crates/oo7-core/src/typechecker.rs +++ b/crates/oo7-core/src/typechecker.rs @@ -4674,15 +4674,23 @@ fn check_import_bindings(program: &Program, env: &mut TypeEnv) { } /// Validate that no two top-level declarations of the same kind share a name. -/// Covers `locale` and `choreography` declarations — previously skipped by the -/// gather pass, so duplicates were silently accepted. A collision makes the -/// name ambiguous and is reported as a `DuplicateDefinition` error. +/// Covers `locale`, `choreography`, `function`, `type`, and `agent` +/// declarations. The locale/choreography kinds were skipped by the gather pass +/// entirely; the function/type/agent kinds were gathered but last-win on +/// redefinition (silently). A within-kind collision makes the name ambiguous +/// and is reported as a `DuplicateDefinition` error. Detection is per parsed +/// top-level declaration, so an `agent Name(args)` spawn/instantiation inside a +/// body is not a declaration and never collides with the `agent Name { … }` +/// that declares it. fn check_duplicate_definitions(program: &Program, env: &mut TypeEnv) { let mut seen: HashSet<(&'static str, String)> = HashSet::new(); for decl in &program.declarations { let (kind, name) = match decl { TopLevelDecl::Locale(ld) => ("locale", ld.name.clone()), TopLevelDecl::Choreography(cd) => ("choreography", cd.name.clone()), + TopLevelDecl::Function(fd) => ("function", fd.name.clone()), + TopLevelDecl::TypeDecl(td) => ("type", td.name.clone()), + TopLevelDecl::Agent(ad) => ("agent", ad.name.clone()), _ => continue, }; if !seen.insert((kind, name.clone())) { diff --git a/crates/oo7-core/src/typechecker_tests.rs b/crates/oo7-core/src/typechecker_tests.rs index 281a275..66eb7c9 100644 --- a/crates/oo7-core/src/typechecker_tests.rs +++ b/crates/oo7-core/src/typechecker_tests.rs @@ -2096,3 +2096,59 @@ fn distinct_locales_are_not_an_error() { ); } } + +// ── Duplicate function / type / agent detection ────────────────────── +// +// These were gathered but silently last-win on redefinition. Two top-level +// declarations of the same kind sharing a name now raise DuplicateDefinition. +// An `agent Name(args)` spawn inside a body is NOT a declaration and must not +// collide with the `agent Name { … }` that declares it. + +#[test] +fn duplicate_function_is_error() { + let src = "@impure fn f() { let x = 1 }\n@impure fn f() { let y = 2 }"; + let errs = parse_and_check(src).expect_err("expected a duplicate-function error"); + assert!( + has_duplicate_definition(&errs), + "two `fn f` must collide, got: {:?}", + errs + ); +} + +#[test] +fn duplicate_type_is_error() { + let src = "type Url = String\ntype Url = Int"; + let errs = parse_and_check(src).expect_err("expected a duplicate-type error"); + assert!( + has_duplicate_definition(&errs), + "two `type Url` must collide, got: {:?}", + errs + ); +} + +#[test] +fn duplicate_agent_is_error() { + let src = "agent A { control { on receive(x: Int) { let y = x } } }\nagent A { control { on receive(x: Int) { let z = x } } }"; + let errs = parse_and_check(src).expect_err("expected a duplicate-agent error"); + assert!( + has_duplicate_definition(&errs), + "two `agent A` must collide, got: {:?}", + errs + ); +} + +#[test] +fn agent_reference_in_supervisor_is_not_a_duplicate() { + // `agent Name(args)` in a supervisor `children:` list references the agent; + // it is not a second top-level declaration and must not collide with the + // `agent Name { … }` that declares it. (This is the real shape that the + // examples use — agent_creates_agent.007, full_language.007, etc.) + let src = "agent Worker(caps: Cap[reason]) { control { on receive(x: Int) { let y = x } } }\nsupervisor Sup {\n strategy: one_for_all\n max_restarts: 3 per 60 s\n children: [\n agent Worker(caps: [reason]),\n ]\n}"; + if let Err(errs) = parse_and_check(src) { + assert!( + !has_duplicate_definition(&errs), + "an agent reference in a supervisor must NOT raise DuplicateDefinition, got: {:?}", + errs + ); + } +}