Skip to content

chore(abi): move api/v/src/abi/Types.idr → ffi/zig/abi/Types.idr #73

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’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
May 28, 2026
Merged

chore(abi): move api/v/src/abi/Types.idr → ffi/zig/abi/Types.idr #73

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
18 changes: 11 additions & 7 deletions api/v/src/abi/Types.idr → ffi/zig/abi/Types.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,18 +1,22 @@
-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
--
-- 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
Expand All @@ -21,15 +25,15 @@ 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
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
Expand Down
Loading