Skip to content

Commit ca22cf2

Browse files
hyperpolymathclaude
andcommitted
feat(lol): add V-triple — Idris2 ABI, Zig FFI, V-lang API for i18n service
LOL is called as a service for i18n across 1500+ languages. This adds the complete V-triple stack: - Idris2 ABI (src/abi/): Types, Layout, Foreign with formal proofs (result round-trips, handle non-null, struct alignment, plural bounds) - Zig FFI (ffi/zig/): BCP 47 parsing, CLDR plural rules, corpus lookup, locale fallback chains, thread-safe errors - V-lang API (api/v-lol/): idiomatic Service wrapper with error handling - Generated C header (generated/abi/lol.h) - ABI-FFI-README.md documenting the triple architecture No believe_me, assert_total, or dangerous patterns used. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent f4cc66a commit ca22cf2

12 files changed

Lines changed: 2996 additions & 0 deletions

File tree

lol/ABI-FFI-README.md

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
1+
# LOL i18n Service — ABI/FFI/API V-Triple Documentation
2+
3+
## Overview
4+
5+
The LOL (Language of Languages) i18n service follows the **Hyperpolymath V-Triple Standard**:
6+
7+
- **ABI (Application Binary Interface)** defined in **Idris2** with formal proofs
8+
- **FFI (Foreign Function Interface)** implemented in **Zig** for C compatibility
9+
- **API** exposed in **V-lang** for idiomatic high-level access
10+
11+
LOL is always called as a service, never embedded. Consumers initialise with
12+
`lol_init()`, perform translation lookups and plural form selection across
13+
1500+ languages, then clean up with `lol_free()`.
14+
15+
## Architecture
16+
17+
```
18+
┌─────────────────────────────────────────────────┐
19+
│ ABI Definitions (Idris2) │
20+
│ 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) │
27+
└─────────────────┬───────────────────────────────┘
28+
29+
│ generates
30+
31+
┌─────────────────────────────────────────────────┐
32+
│ C Headers (auto-generated) │
33+
│ generated/abi/lol.h │
34+
│ - lol_result_t, lol_plural_category_t │
35+
│ - lol_locale_t, lol_translation_result_t │
36+
│ - lol_language_info_t, lol_plural_rule_t │
37+
│ - All function prototypes │
38+
└─────────────────┬───────────────────────────────┘
39+
40+
│ implemented by
41+
42+
┌─────────────────────────────────────────────────┐
43+
│ 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 │
50+
└─────────────────┬───────────────────────────────┘
51+
52+
│ linked by (-llol)
53+
54+
┌─────────────────────────────────────────────────┐
55+
│ V-lang API (idiomatic wrapper) │
56+
│ api/v-lol/src/ │
57+
│ - lol.v (Service struct, public methods) │
58+
│ - ffi.v (Raw C bindings) │
59+
│ - types.v (V types: Locale, PluralCategory, │
60+
│ TranslationResult, LanguageInfo) │
61+
└─────────────────────────────────────────────────┘
62+
```
63+
64+
## Directory Structure
65+
66+
```
67+
lol/
68+
├── src/
69+
│ └── abi/ # ABI definitions (Idris2)
70+
│ ├── Types.idr # Core types with formal proofs
71+
│ ├── Layout.idr # Memory layout verification
72+
│ └── Foreign.idr # FFI function declarations
73+
├── ffi/
74+
│ └── zig/ # FFI implementation (Zig)
75+
│ ├── build.zig # Build configuration
76+
│ ├── src/main.zig # Implementation
77+
│ └── test/integration_test.zig# Integration tests
78+
├── generated/
79+
│ └── abi/
80+
│ └── lol.h # Auto-generated C header
81+
├── api/
82+
│ ├── v-lol/ # V-lang API wrapper
83+
│ │ ├── v.mod # V module definition
84+
│ │ └── src/
85+
│ │ ├── lol.v # Public API (Service struct)
86+
│ │ ├── ffi.v # Raw C bindings
87+
│ │ └── types.v # V types and enums
88+
│ └── v-gateway/ # Existing triple API gateway
89+
│ └── src/ # REST + gRPC + GraphQL
90+
└── ABI-FFI-README.md # This file
91+
```
92+
93+
## Key Types
94+
95+
| Type | Idris2 | C | V |
96+
|------|--------|---|---|
97+
| Result codes | `Result` | `lol_result_t` | `LolError` |
98+
| Plural category | `PluralCategory` | `lol_plural_category_t` | `PluralCategory` |
99+
| Locale | `Locale` | `lol_locale_t` | `Locale` |
100+
| Translation | `TranslationResult` | `lol_translation_result_t` | `TranslationResult` |
101+
| Language info | `LanguageInfo` | `lol_language_info_t` | `LanguageInfo` |
102+
| Plural rule | `PluralRule` | `lol_plural_rule_t` | `PluralRule` |
103+
104+
## Formal Proofs (Idris2 ABI)
105+
106+
The Idris2 ABI layer provides the following compile-time guarantees:
107+
108+
1. **Result code round-trip**: `resultFromInt (resultToInt r) = Just r` for all `r`
109+
2. **Plural category round-trip**: `pluralFromInt (pluralToInt p) = Just p` for all `p`
110+
3. **Result code injectivity**: distinct results map to distinct integer codes
111+
4. **Handle non-null**: the `Handle` type cannot wrap a null pointer (enforced by `So`)
112+
5. **Struct alignment**: all C struct layouts are proven to have correctly aligned fields
113+
6. **Plural form count bounds**: `PluralRule.formCount` is proven to be in range 1-6
114+
115+
No `believe_me`, `assert_total`, or other escape hatches are used.
116+
117+
## Building
118+
119+
### Zig FFI
120+
121+
```bash
122+
cd ffi/zig
123+
zig build # Builds liblol.so and liblol.a
124+
zig build test # Runs unit tests
125+
zig build test-integration # Runs integration tests
126+
```
127+
128+
### V-lang API
129+
130+
```bash
131+
cd api/v-lol
132+
v -cflags "-L../../ffi/zig/zig-out/lib" src/ # Build with liblol
133+
```
134+
135+
## Usage (V-lang)
136+
137+
```v
138+
import lol
139+
140+
fn main() {
141+
// Open the service with a corpus data directory
142+
mut svc := lol.open('/path/to/corpus') or { panic(err) }
143+
defer svc.close()
144+
145+
// Translate a key
146+
result := svc.translate('en-US', 'app.greeting') or {
147+
println('Translation not found, using default')
148+
lol.TranslationResult{ text: 'Hello!', resolved_locale: 'en' }
149+
}
150+
println(result.text)
151+
152+
// Select plural form
153+
cat := svc.select_plural('ar', 5)
154+
println('Arabic plural for 5: ${cat}') // "few"
155+
156+
// Get language metadata
157+
info := svc.get_language('eng') or { panic(err) }
158+
println('${info.name} (${info.native_name}): ${info.verse_count} verses')
159+
160+
// Get plural rule
161+
rule := svc.get_plural_rule('ru') or { panic(err) }
162+
println('Russian has ${rule.form_count} plural forms')
163+
}
164+
```
165+
166+
## License
167+
168+
SPDX-License-Identifier: PMPL-1.0-or-later
169+
170+
Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)

lol/api/v-lol/src/ffi.v

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
//
4+
// LOL i18n Service — V-lang FFI Bindings
5+
//
6+
// Raw C function declarations that link against liblol (the Zig FFI).
7+
// These are not intended for direct use; the public API in lol.v wraps
8+
// them with idiomatic V types and error handling.
9+
10+
module lol
11+
12+
// C struct types (opaque pointers in V)
13+
struct C.lol_locale_t {
14+
tag &char
15+
language &char
16+
script &char
17+
region &char
18+
}
19+
20+
struct C.lol_translation_result_t {
21+
text &char
22+
resolved_locale &char
23+
is_fallback u32
24+
_padding u32
25+
}
26+
27+
struct C.lol_language_info_t {
28+
iso639_3 &char
29+
name &char
30+
native_name &char
31+
family &char
32+
scripts &char
33+
source_count u32
34+
verse_count u32
35+
quality f64
36+
}
37+
38+
struct C.lol_plural_rule_t {
39+
language &char
40+
form_count u32
41+
categories [6]u32
42+
_padding u32
43+
}
44+
45+
// Lifecycle
46+
fn C.lol_init(data_dir &char) voidptr
47+
fn C.lol_free(handle voidptr)
48+
fn C.lol_is_initialized(handle voidptr) u32
49+
50+
// Locale resolution
51+
fn C.lol_resolve_locale(handle voidptr, tag &char) &C.lol_locale_t
52+
fn C.lol_free_locale(locale &C.lol_locale_t)
53+
54+
// Translation
55+
fn C.lol_translate(handle voidptr, locale_tag &char, key &char) &C.lol_translation_result_t
56+
fn C.lol_free_translation(result &C.lol_translation_result_t)
57+
fn C.lol_translation_text(result &C.lol_translation_result_t) &char
58+
59+
// Plural
60+
fn C.lol_select_plural(handle voidptr, locale_tag &char, quantity u64) u32
61+
fn C.lol_translate_plural(handle voidptr, locale_tag &char, key &char, quantity u64) &C.lol_translation_result_t
62+
63+
// Language metadata
64+
fn C.lol_language_count(handle voidptr) u32
65+
fn C.lol_get_language(handle voidptr, code &char) &C.lol_language_info_t
66+
fn C.lol_free_language(info &C.lol_language_info_t)
67+
68+
// Plural rules
69+
fn C.lol_get_plural_rule(handle voidptr, lang_code &char) &C.lol_plural_rule_t
70+
fn C.lol_free_plural_rule(rule &C.lol_plural_rule_t)
71+
72+
// Fallback chain
73+
fn C.lol_fallback_chain_len(handle voidptr, locale_tag &char) u32
74+
75+
// Error handling
76+
fn C.lol_last_error() &char
77+
78+
// Version
79+
fn C.lol_version() &char
80+
fn C.lol_build_info() &char
81+
82+
// --- Internal helpers ---
83+
84+
// c_str_to_v converts a C null-terminated string to a V string.
85+
// Returns empty string if the pointer is null.
86+
fn c_str_to_v(ptr &char) string {
87+
if ptr == unsafe { nil } {
88+
return ''
89+
}
90+
return unsafe { cstring_to_vstring(ptr) }
91+
}

0 commit comments

Comments
 (0)