Skip to content

Commit 68446ad

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat: add V-lang API triple (Idris2 ABI + Zig FFI + V API) for i18n service
Adds the complete V-triple architecture: Idris2 ABI (src/abi/): - Locale.idr: BCP-47 locale type with validation proofs - TranslationKey.idr: Type-safe dot-separated key with segment proofs - PluralForm.idr: CLDR plural rules with coverage proofs - I18nStore.idr: Store interface with guaranteed lookup contract - Fix createHandle to use choose for So proof (Types.idr) Zig FFI (ffi/zig/src/): - locale.zig: Parse, validate, normalise BCP 47 tags - store.zig: Thread-safe HashMap store with fallback chains - plural.zig: CLDR plural selection for common language families - ffi.zig: Module re-exports and FFI surface documentation - build.zig: Updated for Zig 0.15 API (addLibrary, createModule) Also adds lol-abi.ipkg, Idris2 module symlinks, and build artifacts to .gitignore. All new Idris2 modules type-check. Zig builds and all tests pass. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 9793c1e commit 68446ad

20 files changed

Lines changed: 1735 additions & 43 deletions

‎lol/.gitignore‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,17 @@ __pycache__/
5555
/.stack-work/
5656
/dist-newstyle/
5757

58+
# Zig
59+
zig-cache/
60+
.zig-cache/
61+
zig-out/
62+
63+
# Idris2
64+
build/
65+
*.ibc
66+
*.ttc
67+
*.ttm
68+
5869
# Chapel
5970
*.chpl.tmp.*
6071

‎lol/ABI-FFI-README.md‎

Lines changed: 36 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -18,12 +18,13 @@ LOL is always called as a service, never embedded. Consumers initialise with
1818
┌─────────────────────────────────────────────────┐
1919
│ ABI Definitions (Idris2) │
2020
│ src/abi/ │
21-
│ - Types.idr (Result, Locale, PluralCategory,│
22-
│ LanguageInfo, TranslationResult)│
23-
│ - Layout.idr (Memory layout proofs for each │
24-
│ C struct that crosses the FFI) │
25-
│ - Foreign.idr (FFI function declarations with │
26-
│ safe wrappers) │
21+
│ - Types.idr (Result, Handle, enums) │
22+
│ - Layout.idr (Memory layout proofs) │
23+
│ - Locale.idr (BCP-47 validated locale) │
24+
│ - TranslationKey.idr (Type-safe key proofs) │
25+
│ - PluralForm.idr (CLDR rules + coverage) │
26+
│ - I18nStore.idr (Store interface + proofs)│
27+
│ - Foreign.idr (FFI declarations) │
2728
└─────────────────┬───────────────────────────────┘
2829
│
2930
│ generates
@@ -41,12 +42,12 @@ LOL is always called as a service, never embedded. Consumers initialise with
4142
▼
4243
┌─────────────────────────────────────────────────┐
4344
│ FFI Implementation (Zig) │
44-
│ ffi/zig/src/main.zig │
45-
│ - BCP 47 locale parsing │
46-
│ - CLDR plural rule engine │
47-
│ - Corpus data directory access │
48-
│ - Translation lookup with fallback chains │
49-
│ - Thread-safe error handling │
45+
│ ffi/zig/src/ │
46+
│ - main.zig (C ABI exports, service state) │
47+
│ - locale.zig (BCP 47 parse, validate, norm) │
48+
│ - store.zig (HashMap store, fallback chains) │
49+
│ - plural.zig (CLDR plural rule engine) │
50+
│ - ffi.zig (Module re-exports, FFI index) │
5051
└─────────────────┬───────────────────────────────┘
5152
│
5253
│ linked by (-llol)
@@ -69,11 +70,20 @@ lol/
6970
│ └── abi/ # ABI definitions (Idris2)
7071
│ ├── Types.idr # Core types with formal proofs
7172
│ ├── Layout.idr # Memory layout verification
73+
│ ├── Locale.idr # BCP-47 locale with validation proofs
74+
│ ├── TranslationKey.idr # Type-safe translation key proofs
75+
│ ├── PluralForm.idr # CLDR plural rules + coverage proofs
76+
│ ├── I18nStore.idr # Store interface with lookup proofs
7277
│ └── Foreign.idr # FFI function declarations
7378
├── ffi/
7479
│ └── zig/ # FFI implementation (Zig)
7580
│ ├── build.zig # Build configuration
76-
│ ├── src/main.zig # Implementation
81+
│ ├── src/
82+
│ │ ├── main.zig # C ABI exports + service state
83+
│ │ ├── locale.zig # Locale parse/validate/normalise
84+
│ │ ├── store.zig # Translation store with fallback
85+
│ │ ├── plural.zig # CLDR plural rule engine
86+
│ │ └── ffi.zig # Module re-exports + FFI index
7787
│ └── test/integration_test.zig# Integration tests
7888
├── generated/
7989
│ └── abi/
@@ -111,11 +121,24 @@ The Idris2 ABI layer provides the following compile-time guarantees:
111121
4. **Handle non-null**: the `Handle` type cannot wrap a null pointer (enforced by `So`)
112122
5. **Struct alignment**: all C struct layouts are proven to have correctly aligned fields
113123
6. **Plural form count bounds**: `PluralRule.formCount` is proven to be in range 1-6
124+
7. **BCP-47 validation**: `ValidLocale` proves tag structure at construction (Locale.idr)
125+
8. **Translation key validity**: `ValidKey` proves non-empty dot-separated segments (TranslationKey.idr)
126+
9. **Plural coverage**: `eastAsianPluralConstant` proves East Asian always returns Other (PluralForm.idr)
127+
10. **Plural FFI bounds**: `pluralToIntBounded` proves category integers stay in 0-5 range
128+
11. **Store lookup guarantee**: `CorrectStore` interface proves key-exists implies non-empty result (I18nStore.idr)
129+
12. **Fallback chain contract**: `lookupWithFallback` walks chain with locale/key pair, resolves or returns Nothing
114130

115131
No `believe_me`, `assert_total`, or other escape hatches are used.
116132

117133
## Building
118134

135+
### Idris2 ABI
136+
137+
```bash
138+
idris2 --check lol-abi.ipkg # Type-check all ABI definitions and proofs
139+
idris2 --build lol-abi.ipkg # Build (optional, ABI is specification-only)
140+
```
141+
119142
### Zig FFI
120143

121144
```bash

‎lol/ffi/zig/build.zig‎

Lines changed: 78 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1,62 +1,112 @@
11
// LOL i18n Service — FFI Build Configuration
22
// SPDX-License-Identifier: PMPL-1.0-or-later
33
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
4+
//
5+
// Builds liblol as both shared and static libraries.
6+
// The library implements the C ABI declared in src/abi/Foreign.idr
7+
// and specified in generated/abi/lol.h.
8+
//
9+
// Modules:
10+
// src/main.zig — C ABI exports and service state
11+
// src/locale.zig — BCP 47 locale parsing, validation, normalisation
12+
// src/store.zig — Thread-safe translation store with fallback
13+
// src/plural.zig — CLDR plural rule selection per language
14+
// src/ffi.zig — Module re-exports and FFI surface documentation
415

516
const std = @import("std");
617

718
pub fn build(b: *std.Build) void {
819
const target = b.standardTargetOptions(.{});
920
const optimize = b.standardOptimizeOption(.{});
1021

22+
const root_source = b.path("src/main.zig");
23+
1124
// Shared library (liblol.so / liblol.dylib / lol.dll)
12-
const lib = b.addSharedLibrary(.{
25+
const lib = b.addLibrary(.{
1326
.name = "lol",
14-
.root_source_file = b.path("src/main.zig"),
15-
.target = target,
16-
.optimize = optimize,
27+
.root_module = b.createModule(.{
28+
.root_source_file = root_source,
29+
.target = target,
30+
.optimize = optimize,
31+
.link_libc = true,
32+
}),
33+
.linkage = .dynamic,
1734
});
18-
19-
lib.version = .{ .major = 0, .minor = 1, .patch = 0 };
20-
2135
// Static library (liblol.a)
22-
const lib_static = b.addStaticLibrary(.{
36+
const lib_static = b.addLibrary(.{
2337
.name = "lol",
24-
.root_source_file = b.path("src/main.zig"),
25-
.target = target,
26-
.optimize = optimize,
38+
.root_module = b.createModule(.{
39+
.root_source_file = root_source,
40+
.target = target,
41+
.optimize = optimize,
42+
.link_libc = true,
43+
}),
44+
.linkage = .static,
2745
});
2846

2947
// Install artifacts
3048
b.installArtifact(lib);
3149
b.installArtifact(lib_static);
3250

33-
// Install the generated C header
34-
const header = b.addInstallHeader(
35-
b.path("../../generated/abi/lol.h"),
36-
"lol.h",
37-
);
38-
b.getInstallStep().dependOn(&header.step);
51+
// Install the generated C header alongside the library.
52+
b.installFile("../../generated/abi/lol.h", "include/lol.h");
3953

40-
// Unit tests
54+
// Unit tests (main module — needs libc for c_allocator)
4155
const lib_tests = b.addTest(.{
42-
.root_source_file = b.path("src/main.zig"),
43-
.target = target,
44-
.optimize = optimize,
56+
.root_module = b.createModule(.{
57+
.root_source_file = root_source,
58+
.target = target,
59+
.optimize = optimize,
60+
.link_libc = true,
61+
}),
4562
});
46-
4763
const run_lib_tests = b.addRunArtifact(lib_tests);
4864

49-
const test_step = b.step("test", "Run library tests");
65+
// Sub-module tests: locale
66+
const locale_tests = b.addTest(.{
67+
.root_module = b.createModule(.{
68+
.root_source_file = b.path("src/locale.zig"),
69+
.target = target,
70+
.optimize = optimize,
71+
}),
72+
});
73+
const run_locale_tests = b.addRunArtifact(locale_tests);
74+
75+
// Sub-module tests: plural
76+
const plural_tests = b.addTest(.{
77+
.root_module = b.createModule(.{
78+
.root_source_file = b.path("src/plural.zig"),
79+
.target = target,
80+
.optimize = optimize,
81+
}),
82+
});
83+
const run_plural_tests = b.addRunArtifact(plural_tests);
84+
85+
// Sub-module tests: store
86+
const store_tests = b.addTest(.{
87+
.root_module = b.createModule(.{
88+
.root_source_file = b.path("src/store.zig"),
89+
.target = target,
90+
.optimize = optimize,
91+
}),
92+
});
93+
const run_store_tests = b.addRunArtifact(store_tests);
94+
95+
const test_step = b.step("test", "Run all library tests");
5096
test_step.dependOn(&run_lib_tests.step);
97+
test_step.dependOn(&run_locale_tests.step);
98+
test_step.dependOn(&run_plural_tests.step);
99+
test_step.dependOn(&run_store_tests.step);
51100

52101
// Integration tests
53102
const integration_tests = b.addTest(.{
54-
.root_source_file = b.path("test/integration_test.zig"),
55-
.target = target,
56-
.optimize = optimize,
103+
.root_module = b.createModule(.{
104+
.root_source_file = b.path("test/integration_test.zig"),
105+
.target = target,
106+
.optimize = optimize,
107+
}),
57108
});
58-
59-
integration_tests.linkLibrary(lib);
109+
integration_tests.root_module.linkLibrary(lib);
60110

61111
const run_integration_tests = b.addRunArtifact(integration_tests);
62112

‎lol/ffi/zig/src/ffi.zig‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
// LOL i18n Service — C ABI Exports
2+
//
3+
// Re-exports all public C ABI functions from the main module.
4+
// This file serves as the documentation index for the FFI surface area.
5+
// The actual implementations are in main.zig, which imports locale.zig,
6+
// store.zig, and plural.zig for modular implementation.
7+
//
8+
// See generated/abi/lol.h for the C header that consumers include.
9+
// See src/abi/Foreign.idr for the Idris2 FFI declarations.
10+
//
11+
// SPDX-License-Identifier: PMPL-1.0-or-later
12+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
13+
14+
/// Re-export the sub-modules for use by main.zig and tests.
15+
pub const locale = @import("locale.zig");
16+
pub const store = @import("store.zig");
17+
pub const plural = @import("plural.zig");
18+
19+
// ---------------------------------------------------------------------------
20+
// FFI Function Index
21+
// ---------------------------------------------------------------------------
22+
//
23+
// The following C ABI functions are exported by main.zig:
24+
//
25+
// Lifecycle:
26+
// lol_init(data_dir) -> handle
27+
// lol_free(handle)
28+
// lol_is_initialized(handle) -> u32
29+
//
30+
// Locale Resolution:
31+
// lol_resolve_locale(handle, tag) -> *Locale
32+
// lol_free_locale(*Locale)
33+
//
34+
// Translation Lookup:
35+
// lol_translate(handle, locale, key) -> *TranslationResult
36+
// lol_free_translation(*TranslationResult)
37+
// lol_translation_text(*TranslationResult) -> *c_char
38+
//
39+
// Plural Selection:
40+
// lol_select_plural(handle, locale, quantity) -> u32
41+
// lol_translate_plural(handle, locale, key, quantity) -> *TranslationResult
42+
//
43+
// Language Metadata:
44+
// lol_language_count(handle) -> u32
45+
// lol_get_language(handle, code) -> *LanguageInfo
46+
// lol_free_language(*LanguageInfo)
47+
// lol_list_languages(handle, out_array) -> u32
48+
//
49+
// Plural Rules:
50+
// lol_get_plural_rule(handle, lang) -> *PluralRule
51+
// lol_free_plural_rule(*PluralRule)
52+
//
53+
// Fallback Chain:
54+
// lol_fallback_chain_len(handle, locale) -> u32
55+
// lol_fallback_chain(handle, locale) -> **c_char
56+
// lol_free_fallback_chain(**c_char)
57+
//
58+
// Error Handling:
59+
// lol_last_error() -> *c_char
60+
//
61+
// Version:
62+
// lol_version() -> *c_char
63+
// lol_build_info() -> *c_char

0 commit comments

Comments
 (0)