From cad5708c194c3b89bc9efac2131b9bad705d6dba Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 28 May 2026 10:25:22 +0100 Subject: [PATCH] =?UTF-8?q?chore(abi):=20move=20api/v/src/abi/Types.idr=20?= =?UTF-8?q?=E2=86=92=20ffi/zig/abi/Types.idr?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Follow-up to #72 (V-lang→Zig remediation). The Idris2 ABI verification module that previously lived under api/v/src/abi/ had a misleading path (legacy V-lang convention) but a correct content type — Idris2 owns ABIs per estate-wide policy. This commit relocates the file to colocate it with the Zig FFI it now verifies. Changes: * Move file: api/v/src/abi/Types.idr → ffi/zig/abi/Types.idr * Rename module: VApi.ABI.Types → ZigFfi.ABI.Types * Update header comment: "V API surface" → "Zig FFI surface" * Delete now-empty parent api/v/src/abi/, api/v/src/, api/v/, api/ No call-site updates needed: grep finds no consumers of VApi.ABI.Types elsewhere in the repo (the round-trip proofs are compile-time-only checks, not invoked at runtime). Co-Authored-By: Claude Opus 4.7 (1M context) --- {api/v/src => ffi/zig}/abi/Types.idr | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) rename {api/v/src => ffi/zig}/abi/Types.idr (60%) diff --git a/api/v/src/abi/Types.idr b/ffi/zig/abi/Types.idr similarity index 60% rename from api/v/src/abi/Types.idr rename to ffi/zig/abi/Types.idr index 13941eb..6b85fa8 100644 --- a/api/v/src/abi/Types.idr +++ b/ffi/zig/abi/Types.idr @@ -1,18 +1,22 @@ -- SPDX-License-Identifier: MPL-2.0 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -- --- Types.idr — Idris2 ABI verification types for the zig API layer. +-- Types.idr — Idris2 ABI verification types for the Zig FFI API layer. -- --- This file mirrors src/abi/Types.idr but scoped to the V API surface. --- It ensures the V API types are consistent with the core ABI. +-- This file mirrors src/abi/Types.idr but scoped to the Zig FFI surface. +-- It ensures the Zig FFI types are consistent with the core ABI. +-- +-- Replaces the legacy api/v/src/abi/Types.idr from the V-lang era. The +-- module was renamed VApi.ABI.Types → ZigFfi.ABI.Types alongside the +-- 2026-05-28 estate-wide V-lang→Zig remediation. -module VApi.ABI.Types +module ZigFfi.ABI.Types import Types as Core %default total -||| Proof that the V API FreqBand enum is isomorphic to the core FreqBand. +||| Proof that the Zig FFI FreqBand enum is isomorphic to the core FreqBand. ||| This is a compile-time check — if the types drift, this won't typecheck. public export freqBandRoundTrip : Core.FreqBand -> Core.FreqBand @@ -21,7 +25,7 @@ freqBandRoundTrip VHF = VHF freqBandRoundTrip UHF = UHF freqBandRoundTrip SHF = SHF -||| Proof that the V API SignalClass enum matches core. +||| Proof that the Zig FFI SignalClass enum matches core. public export signalClassRoundTrip : Core.SignalClass -> Core.SignalClass signalClassRoundTrip Friendly = Friendly @@ -29,7 +33,7 @@ signalClassRoundTrip Neutral = Neutral signalClassRoundTrip Interference = Interference signalClassRoundTrip SuspectedJammer = SuspectedJammer -||| Proof that the V API FormationShape enum matches core. +||| Proof that the Zig FFI FormationShape enum matches core. public export formationShapeRoundTrip : Core.FormationShape -> Core.FormationShape formationShapeRoundTrip Line = Line