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
31 changes: 13 additions & 18 deletions cli/debugger.affine
Original file line number Diff line number Diff line change
@@ -1,45 +1,42 @@
// SPDX-License-Identifier: MPL-2.0
// Ported via Harvard Engine mechanical processor
// Ported via Harvard Engine (Semantic pass)

module debugger;

// TODO: Complete semantic implementation

/* === ORIGINAL TYPESCRIPT CONTEXT ===
// SPDX-License-Identifier: MPL-2.0
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (@hyperpolymath)
//
// GQL-DT Debugger with Dependent Type Inspection
// Step through query execution with proof obligation visualization

interface DebugState {
struct DebugState {
query: string;
position: number;
variables: Map<string, TypedValue>;
proofs: ProofObligation[];
typeConstraints: TypeConstraint[];
}

interface TypedValue {
struct TypedValue {
type: string; // e.g., "BoundedNat 0 100"
value: unknown;
proofStatus: "proven" | "assumed" | "failed";
}

interface ProofObligation {
struct ProofObligation {
id: string;
description: string;
status: "pending" | "proven" | "failed";
location: { line: number; column: number };
}

interface TypeConstraint {
struct TypeConstraint {
variable: string;
constraint: string;
satisfied: boolean;
}

class GQLDTDebugger {
struct GQLDTDebugger {
private state: DebugState;
private breakpoints: Set<number> = new Set();

Expand Down Expand Up @@ -76,7 +73,7 @@ class GQLDTDebugger {

// Inspect variable with type information
inspect(variable: string): TypedValue | undefined {
const value = this.state.variables.get(variable);
let value = this.state.variables.get(variable);
if (value) {
console.log(`Variable: ${variable}`);
console.log(` Type: ${value.type}`);
Expand All @@ -99,7 +96,7 @@ class GQLDTDebugger {
showConstraints(): void {
console.log("\n=== Type Constraints ===");
for (const constraint of this.state.typeConstraints) {
const status = constraint.satisfied ? "✓" : "✗";
let status = constraint.satisfied ? "✓" : "✗";
console.log(`${status} ${constraint.variable}: ${constraint.constraint}`);
}
}
Expand All @@ -114,25 +111,23 @@ class GQLDTDebugger {
}

private getCurrentLine(): number {
const textBeforePosition = this.state.query.substring(0, this.state.position);
let textBeforePosition = this.state.query.substring(0, this.state.position);
return textBeforePosition.split("\n").length;
}
}

// Export debugger
export { GQLDTDebugger, DebugState, TypedValue, ProofObligation, TypeConstraint };
{ GQLDTDebugger, DebugState, TypedValue, ProofObligation, TypeConstraint };

// CLI interface
if (import.meta.main) {
// CLI struct if (import.meta.main) {
console.log("GQL-DT Debugger v1.0.0");
console.log("Commands: step, continue, breakpoint <line>, inspect <var>, proofs, constraints, quit");

const query = Deno.args[0] || "SELECT * FROM evidence WHERE score > 50 RATIONALE 'test'";
const debugger = new GQLDTDebugger(query);
let query = Deno.args[0] || "SELECT * FROM evidence WHERE score > 50 RATIONALE 'test'";
let debugger = new GQLDTDebugger(query);

console.log(`\nDebugging query:\n${query}\n`);
debugger.showProofs();
debugger.showConstraints();
}

==================================== */
57 changes: 26 additions & 31 deletions cli/lsp-server.affine
Original file line number Diff line number Diff line change
@@ -1,11 +1,8 @@
// SPDX-License-Identifier: MPL-2.0
// Ported via Harvard Engine mechanical processor
// Ported via Harvard Engine (Semantic pass)

module lsp-server;

// TODO: Complete semantic implementation

/* === ORIGINAL TYPESCRIPT CONTEXT ===
// SPDX-License-Identifier: MPL-2.0
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (@hyperpolymath)
//
Expand All @@ -24,11 +21,11 @@ import {
import { TextDocument } from "npm:vscode-languageserver-textdocument";

// Create LSP connection
const connection = createConnection(ProposedFeatures.all);
const documents = new TextDocuments(TextDocument);
let connection = createConnection(ProposedFeatures.all);
let documents = new TextDocuments(TextDocument);

// GQL-DT keywords for syntax validation
const GQL_KEYWORDS = new Set([
let GQL_KEYWORDS = new Set([
"SELECT", "INSERT", "UPDATE", "DELETE", "FROM", "WHERE", "INTO", "VALUES",
"SET", "ORDER", "BY", "LIMIT", "ASC", "DESC", "AND", "OR", "NOT",
"RATIONALE", "AS", "NORMALIZE", "WITH",
Expand Down Expand Up @@ -70,24 +67,23 @@ documents.onDidOpen((event) => {
validateDocument(event.document);
});

// Validation function
function validateDocument(textDocument: TextDocument): void {
const text = textDocument.getText();
// Validation fn function validateDocument(textDocument: TextDocument): void {
let text = textDocument.getText();
const diagnostics: Diagnostic[] = [];

// Check for missing RATIONALE clauses (critical in GQL-DT)
const insertMatch = /INSERT\s+INTO/gi;
const updateMatch = /UPDATE\s+\w+\s+SET/gi;
const deleteMatch = /DELETE\s+FROM/gi;
let insertMatch = /INSERT\s+INTO/gi;
let updateMatch = /UPDATE\s+\w+\s+SET/gi;
let deleteMatch = /DELETE\s+FROM/gi;

let match;
while ((match = insertMatch.exec(text)) !== null) {
const startPos = match.index;
const endPos = text.indexOf(";", startPos);
const statement = text.substring(startPos, endPos === -1 ? text.length : endPos);
let startPos = match.index;
let endPos = text.indexOf(";", startPos);
let statement = text.substring(startPos, endPos === -1 ? text.length : endPos);

if (!statement.match(/RATIONALE\s+/i)) {
const line = text.substring(0, startPos).split("\n").length - 1;
let line = text.substring(0, startPos).split("\n").length - 1;
diagnostics.push({
severity: DiagnosticSeverity.Error,
range: {
Expand All @@ -101,11 +97,11 @@ function validateDocument(textDocument: TextDocument): void {
}

// Check for type annotations in GQL-DT mode (explicit types)
const columnListMatch = /\(([^)]+)\)/g;
let columnListMatch = /\(([^)]+)\)/g;
while ((match = columnListMatch.exec(text)) !== null) {
const columns = match[1];
let columns = match[1];
if (columns.includes(":") && !columns.match(/:\s*(Nat|Int|String|Bool|BoundedNat|NonEmptyString)/)) {
const line = text.substring(0, match.index).split("\n").length - 1;
let line = text.substring(0, match.index).split("\n").length - 1;
diagnostics.push({
severity: DiagnosticSeverity.Warning,
range: {
Expand All @@ -119,12 +115,12 @@ function validateDocument(textDocument: TextDocument): void {
}

// Check for BoundedNat bounds
const boundedNatMatch = /BoundedNat\s+(\d+)\s+(\d+)/g;
let boundedNatMatch = /BoundedNat\s+(\d+)\s+(\d+)/g;
while ((match = boundedNatMatch.exec(text)) !== null) {
const min = parseInt(match[1]);
const max = parseInt(match[2]);
let min = parseInt(match[1]);
let max = parseInt(match[2]);
if (min >= max) {
const line = text.substring(0, match.index).split("\n").length - 1;
let line = text.substring(0, match.index).split("\n").length - 1;
diagnostics.push({
severity: DiagnosticSeverity.Error,
range: {
Expand All @@ -143,12 +139,12 @@ function validateDocument(textDocument: TextDocument): void {

// Hover provider - show type information
connection.onHover((params) => {
const document = documents.get(params.textDocument.uri);
let document = documents.get(params.textDocument.uri);
if (!document) return null;

const text = document.getText();
const offset = document.offsetAt(params.position);
const word = getWordAtOffset(text, offset);
let text = document.getText();
let offset = document.offsetAt(params.position);
let word = getWordAtOffset(text, offset);

if (GQL_KEYWORDS.has(word.toUpperCase())) {
return {
Expand All @@ -164,7 +160,7 @@ connection.onHover((params) => {

// Completion provider - suggest keywords and types
connection.onCompletion((params) => {
const keywords = Array.from(GQL_KEYWORDS).map((kw) => ({
let keywords = Array.from(GQL_KEYWORDS).map((kw) => ({
label: kw,
kind: 14, // Keyword
detail: "GQL-DT keyword",
Expand All @@ -174,7 +170,7 @@ connection.onCompletion((params) => {
});

// Helper: get word at offset
function getWordAtOffset(text: string, offset: number): string {
fn getWordAtOffset(text: string, offset: number): string {
let start = offset;
let end = offset;

Expand All @@ -190,4 +186,3 @@ connection.listen();

console.error("[GQL-DT LSP] Language server started, listening for requests");

==================================== */
Loading