Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
516 changes: 148 additions & 368 deletions LICENSE

Large diffs are not rendered by default.

58 changes: 58 additions & 0 deletions MOVED.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
# This Repository Has Moved

**GQLdt is now part of the [Lithoglyph monorepo](https://github.com/hyperpolymath/lith).**

## New Location

- **Monorepo:** https://github.com/hyperpolymath/lith
- **Query Language:** https://github.com/hyperpolymath/lith/tree/main/query

## Why the Move?

GQLdt (Lithoglyph Query Language with dependent types) is the query interface for Lithoglyph. To improve discoverability and maintenance, we've consolidated the Lithoglyph ecosystem into a single monorepo:

```
lith/
β”œβ”€β”€ query/ # GQLdt (this repo)
β”œβ”€β”€ database/ # Form.Model + Form.Blocks (Forth core)
β”œβ”€β”€ bridge/ # Zig FFI bridge
β”œβ”€β”€ studio/ # Web-based GUI
└── debugger/ # Proof-carrying debugger
```

## Benefits of the Monorepo

- **Single source of truth** for all Lithoglyph components
- **Coordinated versioning** across query language, database, and tools
- **Unified documentation** and examples
- **Shared CI/CD** and dependency management
- **Easier cross-component refactoring**

## Migration Guide

### For Users

Update your imports/dependencies:

**Before:**
```bash
git clone https://github.com/hyperpolymath/gql-dt
```

**After:**
```bash
git clone https://github.com/hyperpolymath/lith
cd lith/query
```

### For Contributors

Submit PRs to the [lith monorepo](https://github.com/hyperpolymath/lith) instead.

## This Repository's Future

This repository (`gql-dt`) will be archived and remain as a historical reference. All active development happens in the monorepo.

---

**See you at [github.com/hyperpolymath/lith](https://github.com/hyperpolymath/lith)!** πŸš€
51 changes: 51 additions & 0 deletions bridge/zig/build.zig
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
// SPDX-License-Identifier: MPL-2.0
// SPDX-FileCopyrightText: 2026 hyperpolymath
//
// Zig FFI Bridge for GQLdt
// Provides C-compatible ABI for Lean 4 integration

const std = @import("std");

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

// Static library for FFI bridge
const lib = b.addStaticLibrary(.{
.name = "lith_bridge",
.root_source_file = b.path("src/main.zig"),
.target = target,
.optimize = optimize,
});

// Export C ABI
lib.linkLibC();

b.installArtifact(lib);

// Tests
const main_tests = b.addTest(.{
.root_source_file = b.path("src/main.zig"),
.target = target,
.optimize = optimize,
});

const run_main_tests = b.addRunArtifact(main_tests);

const test_step = b.step("test", "Run library tests");
test_step.dependOn(&run_main_tests.step);

// Integration tests
const integration_tests = b.addTest(.{
.root_source_file = b.path("test/integration_test.zig"),
.target = target,
.optimize = optimize,
});

integration_tests.linkLibrary(lib);

const run_integration_tests = b.addRunArtifact(integration_tests);

const integration_step = b.step("test-integration", "Run integration tests");
integration_step.dependOn(&run_integration_tests.step);
}
142 changes: 142 additions & 0 deletions bridge/zig/src/main.zig
Original file line number Diff line number Diff line change
@@ -0,0 +1,142 @@
// SPDX-License-Identifier: MPL-2.0
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (@hyperpolymath)
//
// Zig FFI Bridge - Main Module
// Bidirectional FFI: Lean 4 ↔ Zig ↔ Lith Forth core

const std = @import("std");

/// Status code for FFI operations
pub const LithStatus = enum(i32) {
ok = 0,
error_null_pointer = 1,
error_invalid_proof = 2,
error_type_mismatch = 3,
error_constraint_violation = 4,
error_out_of_memory = 5,

pub fn toC(self: LithStatus) c_int {
return @intFromEnum(self);
}
};

/// Opaque database handle (non-null guaranteed by Lean 4 types)
pub const LithDb = opaque {};

/// FFI-safe string view (non-owning)
pub const LithString = struct {
data: [*]const u8,
len: usize,

pub fn fromSlice(slice: []const u8) LithString {
return .{ .data = slice.ptr, .len = slice.len };
}

pub fn toSlice(self: LithString) []const u8 {
return self.data[0..self.len];
}
};

/// Forward: Lean 4 β†’ Zig β†’ Lith
/// Insert operation with proof blob
export fn lith_insert(
db: *LithDb,
collection: [*:0]const u8,
document: [*]const u8,
doc_len: usize,
proof_blob: [*]const u8,
proof_len: usize,
) callconv(.C) c_int {
_ = db;
_ = collection;
_ = document;
_ = doc_len;
_ = proof_blob;
_ = proof_len;

// TODO: Implement actual insertion
// 1. Deserialize proof blob (CBOR)
// 2. Verify proof against schema
// 3. Insert into Lith via Forth FFI
// 4. Return status

return LithStatus.ok.toC();
}

/// Reverse: Lith β†’ Zig β†’ Lean 4
/// Register constraint checker callback
export fn lith_register_constraint_checker(
db: *LithDb,
checker: *const fn (doc: [*]const u8, len: usize) callconv(.C) bool,
) callconv(.C) c_int {
_ = db;
_ = checker;

// TODO: Implement callback registration
// Store function pointer for later invocation
// When Lith validates data, call this Lean 4 checker

return LithStatus.ok.toC();
}

/// Get discovered functional dependencies
export fn lith_get_discovered_fds(
db: *LithDb,
collection: [*:0]const u8,
out_fds: *[*]u8,
out_len: *usize,
) callconv(.C) c_int {
_ = db;
_ = collection;
_ = out_fds;
_ = out_len;

// TODO: Implement FD discovery
// 1. Query Lith for collection statistics
// 2. Run FD discovery algorithm (DFD, TANE, etc.)
// 3. Serialize FDs to CBOR
// 4. Return pointer + length

return LithStatus.ok.toC();
}

/// Verify normalization proof
export fn lith_verify_normalization_proof(
db: *LithDb,
step_blob: [*]const u8,
step_len: usize,
proof_blob: [*]const u8,
proof_len: usize,
) callconv(.C) c_int {
_ = db;
_ = step_blob;
_ = step_len;
_ = proof_blob;
_ = proof_len;

// TODO: Implement proof verification
// 1. Deserialize normalization step
// 2. Deserialize Lean 4 proof
// 3. Verify proof is valid for step
// 4. Return status

return LithStatus.ok.toC();
}

/// Free memory allocated by FFI functions
export fn lith_free(ptr: [*]u8, len: usize) callconv(.C) void {
const allocator = std.heap.c_allocator;
const slice = ptr[0..len];
allocator.free(slice);
}

test "LithStatus roundtrip" {
const status = LithStatus.ok;
try std.testing.expectEqual(@as(c_int, 0), status.toC());
}

test "LithString conversion" {
const str = "Hello, Lith!";
const lith_str = LithString.fromSlice(str);
try std.testing.expectEqualSlices(u8, str, lith_str.toSlice());
}
45 changes: 45 additions & 0 deletions bridge/zig/test/integration_test.zig
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
// SPDX-License-Identifier: MPL-2.0
// SPDX-FileCopyrightText: 2026 hyperpolymath
//
// Integration tests for Zig FFI bridge

const std = @import("std");
const main = @import("main");

test "lith_insert stub returns ok" {
// Mock database handle (in production, would be created by Lith)
var db: main.LithDb = undefined;
const db_ptr = @as(*main.LithDb, @ptrCast(&db));

const collection = "test_collection";
const document = "{\"id\": 1, \"value\": 42}";
const proof = "{}"; // Empty proof for stub

const status = main.lith_insert(
db_ptr,
collection,
document.ptr,
document.len,
proof.ptr,
proof.len,
);

try std.testing.expectEqual(@as(c_int, 0), status);
}

test "lith_register_constraint_checker stub" {
var db: main.LithDb = undefined;
const db_ptr = @as(*main.LithDb, @ptrCast(&db));

const checker = struct {
fn check(doc: [*]const u8, len: usize) callconv(.C) bool {
_ = doc;
_ = len;
return true;
}
}.check;

const status = main.lith_register_constraint_checker(db_ptr, checker);

try std.testing.expectEqual(@as(c_int, 0), status);
}
51 changes: 51 additions & 0 deletions ffi/zig/build.zig
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
// SPDX-License-Identifier: MPL-2.0
// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell (@hyperpolymath)
//
// build.zig - GQL-DT FFI Build Configuration (Zig 0.15.2+)
//
// Builds the libgqldt shared library (C ABI) and unit tests.

const std = @import("std");

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

// Static library (libgqldt.a)
const static_lib = b.addLibrary(.{
.name = "gqldt",
.root_module = b.createModule(.{
.root_source_file = b.path("src/main.zig"),
.target = target,
.optimize = optimize,
}),
.linkage = .static,
});
b.installArtifact(static_lib);

// Shared library (libgqldt.so / libgqldt.dylib)
const shared_lib = b.addLibrary(.{
.name = "gqldt",
.root_module = b.createModule(.{
.root_source_file = b.path("src/main.zig"),
.target = target,
.optimize = optimize,
}),
.linkage = .dynamic,
});
b.installArtifact(shared_lib);

// Unit tests (from main.zig internal tests)
const unit_tests = b.addTest(.{
.name = "gqldt-tests",
.root_module = b.createModule(.{
.root_source_file = b.path("src/main.zig"),
.target = target,
.optimize = optimize,
}),
});

const run_unit_tests = b.addRunArtifact(unit_tests);
const test_step = b.step("test", "Run unit tests");
test_step.dependOn(&run_unit_tests.step);
}
Loading
Loading