= A2ML Language Server Protocol (LSP) Implementation
:toc: preamble
:toclevels: 2
:icons: font

LSP server for A2ML editor integration with VS Code, Neovim, Emacs, and other LSP-compatible editors.

== Overview

The A2ML LSP server provides:

- **Syntax highlighting** - A2ML-specific token types
- **Diagnostics** - Real-time validation errors
- **Auto-completion** - Directive and ID completion
- **Go-to-definition** - Jump to ID definitions
- **Find references** - Find all uses of an ID
- **Hover information** - Show ID/reference details
- **Document symbols** - Outline view
- **Code actions** - Quick fixes for common issues

== Architecture

[source]
----
┌─────────────────┐
│  Editor Client  │ (VS Code, Neovim, etc.)
│  (JavaScript)   │
└────────┬────────┘
         │ LSP Protocol (JSON-RPC)
         │
┌────────▼────────┐
│   A2ML LSP      │
│   Server        │
│   (Idris2)      │
└────────┬────────┘
         │
┌────────▼────────┐
│  A2ML Parser    │ (A2ML.Parser)
│  + Validator    │ (A2ML.Proofs)
└─────────────────┘
----

== LSP Server Implementation

=== Server Capabilities

[source,json]
----
{
  "capabilities": {
    "textDocumentSync": {
      "openClose": true,
      "change": 2,  // Incremental
      "save": true
    },
    "completionProvider": {
      "resolveProvider": false,
      "triggerCharacters": ["@", "#"]
    },
    "hoverProvider": true,
    "definitionProvider": true,
    "referencesProvider": true,
    "documentSymbolProvider": true,
    "codeActionProvider": true,
    "diagnosticProvider": {
      "interFileDependencies": false,
      "workspaceDiagnostics": false
    }
  }
}
----

=== Message Handlers

==== textDocument/didOpen

When a document is opened:

1. Parse the document
2. Run validation
3. Send diagnostics

[source,idris]
----
handleDidOpen : TextDocumentItem -> IO ()
handleDidOpen item = do
  let content = item.text
  case parseAndValidate content of
    Right _ =>
      sendDiagnostics item.uri []  -- No errors
    Left errors =>
      sendDiagnostics item.uri (map errorToDiagnostic errors)
----

==== textDocument/didChange

When a document changes:

1. Apply incremental changes
2. Reparse affected sections
3. Update diagnostics

[source,idris]
----
handleDidChange : VersionedTextDocumentIdentifier ->
                  List TextDocumentContentChangeEvent ->
                  IO ()
handleDidChange docId changes = do
  content <- applyChanges docId changes
  -- Validate and send diagnostics
  validateAndDiagnose docId.uri content
----

==== textDocument/completion

Provide completions at cursor position:

[source,idris]
----
handleCompletion : TextDocumentPositionParams ->
                   IO (List CompletionItem)
handleCompletion params = do
  let doc = getDocument params.textDocument.uri
  let pos = params.position

  -- Check context
  if isAfter "@" pos then
    -- Directive completion
    pure directiveCompletions
  else if isAfter "#" pos then
    -- Section ID completion (from document)
    ids <- extractIds doc
    pure (map idToCompletion ids)
  else
    pure []

directiveCompletions : List CompletionItem
directiveCompletions = [
  { label = "@abstract:", kind = Snippet },
  { label = "@refs:", kind = Snippet },
  { label = "@figure:", kind = Snippet },
  { label = "@table:", kind = Snippet },
  { label = "@opaque:", kind = Snippet },
  { label = "@end", kind = Keyword }
]
----

==== textDocument/hover

Show information on hover:

[source,idris]
----
handleHover : TextDocumentPositionParams -> IO (Maybe Hover)
handleHover params = do
  let doc = getDocument params.textDocument.uri
  let word = getWordAtPosition doc params.position

  -- Check if word is an ID
  ids <- extractIds doc
  case find (\id => id.raw == word) ids of
    Just id => do
      refs <- findReferences doc id
      let info = "ID: " ++ id.raw ++ "\n" ++
                 "References: " ++ show (length refs)
      pure (Just (Hover info))
    Nothing => pure Nothing
----

==== textDocument/definition

Go to ID definition:

[source,idris]
----
handleDefinition : TextDocumentPositionParams ->
                   IO (Maybe Location)
handleDefinition params = do
  let doc = getDocument params.textDocument.uri
  let word = getWordAtPosition doc params.position

  -- Find definition location
  case findIdDefinition doc word of
    Just location => pure (Just location)
    Nothing => pure Nothing
----

==== textDocument/references

Find all references to an ID:

[source,idris]
----
handleReferences : ReferenceParams -> IO (List Location)
handleReferences params = do
  let doc = getDocument params.textDocument.uri
  let word = getWordAtPosition doc params.position

  -- Find all references
  findAllReferences doc word
----

==== textDocument/codeAction

Provide quick fixes:

[source,idris]
----
handleCodeAction : CodeActionParams -> IO (List CodeAction)
handleCodeAction params = do
  let diagnostics = params.context.diagnostics

  concatMap diagnosticToAction diagnostics
  where
    diagnosticToAction : Diagnostic -> List CodeAction
    diagnosticToAction diag =
      case diag.code of
        "unresolved-ref" =>
          [{ title = "Create missing section",
             kind = QuickFix,
             edit = createSectionEdit diag }]
        "duplicate-id" =>
          [{ title = "Rename duplicate ID",
             kind = QuickFix,
             edit = renameIdEdit diag }]
        _ => []
----

=== Diagnostic Conversion

Convert validation errors to LSP diagnostics:

[source,idris]
----
errorToDiagnostic : ValidationError -> Diagnostic
errorToDiagnostic (DuplicateId id) =
  { range = findIdRange id,
    severity = Error,
    code = "duplicate-id",
    source = "a2ml",
    message = "Duplicate ID: " ++ id.raw }

errorToDiagnostic (UnresolvedRef id) =
  { range = findRefRange id,
    severity = Error,
    code = "unresolved-ref",
    source = "a2ml",
    message = "Unresolved reference: " ++ id.raw }

errorToDiagnostic (MissingRequired msg) =
  { range = defaultRange,
    severity = Warning,
    code = "missing-required",
    source = "a2ml",
    message = msg }
----

== Client Configuration

=== VS Code Extension

**package.json:**

[source,json]
----
{
  "name": "a2ml-vscode",
  "displayName": "A2ML Language Support",
  "version": "0.7.0",
  "engines": { "vscode": "^1.70.0" },
  "categories": ["Programming Languages"],
  "activationEvents": ["onLanguage:a2ml"],
  "main": "./out/extension.js",
  "contributes": {
    "languages": [{
      "id": "a2ml",
      "extensions": [".a2ml"],
      "aliases": ["A2ML", "a2ml"],
      "configuration": "./language-configuration.json"
    }],
    "grammars": [{
      "language": "a2ml",
      "scopeName": "source.a2ml",
      "path": "./syntaxes/a2ml.tmLanguage.json"
    }],
    "configuration": {
      "type": "object",
      "title": "A2ML",
      "properties": {
        "a2ml.server.path": {
          "type": "string",
          "default": "a2ml-lsp",
          "description": "Path to A2ML LSP server"
        },
        "a2ml.validation.strictMode": {
          "type": "boolean",
          "default": false,
          "description": "Enable strict validation mode"
        }
      }
    }
  }
}
----

**extension.ts:**

[source,typescript]
----
import * as vscode from 'vscode';
import {
  LanguageClient,
  LanguageClientOptions,
  ServerOptions
} from 'vscode-languageclient/node';

let client: LanguageClient;

export function activate(context: vscode.ExtensionContext) {
  const serverPath = vscode.workspace
    .getConfiguration('a2ml')
    .get<string>('server.path', 'a2ml-lsp');

  const serverOptions: ServerOptions = {
    command: serverPath,
    args: ['--stdio']
  };

  const clientOptions: LanguageClientOptions = {
    documentSelector: [{ scheme: 'file', language: 'a2ml' }],
    synchronize: {
      fileEvents: vscode.workspace.createFileSystemWatcher('**/*.a2ml')
    }
  };

  client = new LanguageClient(
    'a2ml',
    'A2ML Language Server',
    serverOptions,
    clientOptions
  );

  client.start();
}

export function deactivate(): Thenable<void> | undefined {
  return client ? client.stop() : undefined;
}
----

=== Neovim Configuration

**init.lua:**

[source,lua]
----
-- A2ML LSP configuration for Neovim

local lspconfig = require('lspconfig')
local configs = require('lspconfig.configs')

-- Register A2ML LSP
if not configs.a2ml_lsp then
  configs.a2ml_lsp = {
    default_config = {
      cmd = {'a2ml-lsp', '--stdio'},
      filetypes = {'a2ml'},
      root_dir = lspconfig.util.root_pattern('.git', '.a2ml-root'),
      settings = {
        a2ml = {
          validation = {
            strictMode = false
          }
        }
      }
    }
  }
end

-- Enable A2ML LSP
lspconfig.a2ml_lsp.setup{
  on_attach = function(client, bufnr)
    -- Keybindings
    local opts = { noremap=true, silent=true, buffer=bufnr }
    vim.keymap.set('n', 'gd', vim.lsp.buf.definition, opts)
    vim.keymap.set('n', 'gr', vim.lsp.buf.references, opts)
    vim.keymap.set('n', 'K', vim.lsp.buf.hover, opts)
    vim.keymap.set('n', '<leader>ca', vim.lsp.buf.code_action, opts)
  end
}

-- Filetype detection
vim.filetype.add({
  extension = {
    a2ml = 'a2ml'
  }
})
----

=== Emacs Configuration

**a2ml-mode.el:**

[source,elisp]
----
;;; a2ml-mode.el --- Major mode for A2ML files

(require 'lsp-mode)

(defgroup a2ml nil
  "A2ML language support."
  :group 'languages)

(defcustom a2ml-lsp-server-command '("a2ml-lsp" "--stdio")
  "Command to start A2ML LSP server."
  :type '(repeat string)
  :group 'a2ml)

(defvar a2ml-mode-syntax-table
  (let ((table (make-syntax-table)))
    (modify-syntax-entry ?# "<" table)
    (modify-syntax-entry ?\n ">" table)
    (modify-syntax-entry ?@ "'" table)
    table))

(define-derived-mode a2ml-mode text-mode "A2ML"
  "Major mode for editing A2ML files."
  :syntax-table a2ml-mode-syntax-table
  (setq-local comment-start "#")
  (setq-local comment-end ""))

;; LSP integration
(with-eval-after-load 'lsp-mode
  (lsp-register-client
   (make-lsp-client
    :new-connection (lsp-stdio-connection a2ml-lsp-server-command)
    :major-modes '(a2ml-mode)
    :server-id 'a2ml-lsp)))

(add-to-list 'auto-mode-alist '("\\.a2ml\\'" . a2ml-mode))

(provide 'a2ml-mode)
----

== Build and Deployment

=== Building the LSP Server

[source,bash]
----
cd a2ml/lsp
idris2 --build a2ml-lsp.ipkg

# Install
sudo cp build/exec/a2ml-lsp /usr/local/bin/
----

=== Package Distribution

**NPM (VS Code):**

[source,bash]
----
cd a2ml-vscode
npm install
npm run compile
vsce package
----

**GitHub Releases:**

[source,bash]
----
# Create release with binaries
gh release create v0.7.0 \
  --title "A2ML v0.7.0" \
  --notes "LSP server + CLI tools" \
  a2ml-lsp-linux-x64 \
  a2ml-lsp-macos-x64 \
  a2ml-lsp-windows-x64.exe
----

== Testing

=== LSP Protocol Test

[source,bash]
----
# Test initialization
echo '{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"capabilities":{}}}' | a2ml-lsp --stdio

# Test document validation
echo '{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///test.a2ml","text":"# Test"}}}' | a2ml-lsp --stdio
----

=== Integration Test

[source,typescript]
----
import { suite, test } from 'mocha';
import * as assert from 'assert';
import { LanguageClient } from 'vscode-languageclient/node';

suite('A2ML LSP Tests', () => {
  let client: LanguageClient;

  setup(async () => {
    // Start LSP server
    client = startLSPServer();
    await client.onReady();
  });

  test('Validation errors', async () => {
    const doc = '# Test\n@ref:missing';
    const diagnostics = await validate(client, doc);
    assert.strictEqual(diagnostics.length, 1);
    assert.strictEqual(diagnostics[0].code, 'unresolved-ref');
  });

  test('Auto-completion', async () => {
    const completions = await getCompletions(client, '@');
    assert.ok(completions.some(c => c.label === '@abstract:'));
  });
});
----

== Status

[cols="2,1,3"]
|===
|Feature |Status |Notes

|Diagnostics
|🟡 Partial
|Basic validation works

|Auto-completion
|⏳ Planned
|Directive + ID completion

|Go-to-definition
|⏳ Planned
|Jump to ID definitions

|Find references
|⏳ Planned
|Find all ID uses

|Hover info
|⏳ Planned
|Show ID details

|Code actions
|⏳ Planned
|Quick fixes
|===

== Future Work

1. **Incremental parsing** - Only reparse changed sections
2. **Workspace support** - Multi-file validation
3. **Refactoring** - Rename ID across references
4. **Snippets** - Common A2ML patterns
5. **Semantic tokens** - Better syntax highlighting

---

**Created:** 2026-01-30
**Author:** Jonathan D.A. Jewell
