|
| 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 | +-- ArangoMcp.SafeDatabase — Type-safe ABI for the arango-mcp cartridge. |
| 5 | +-- |
| 6 | +-- Provides a formally verified state machine for ArangoDB multi-model |
| 7 | +-- database connections. Dependent-type proofs ensure only valid transitions |
| 8 | +-- can occur at the FFI boundary. ArangoDB actions cover the full REST API |
| 9 | +-- surface for documents, graphs, key-value, and AQL queries. |
| 10 | +-- Auth via Bearer token or Basic auth (self-hosted, configurable base URL). |
| 11 | + |
| 12 | +module ArangoMcp.SafeDatabase |
| 13 | + |
| 14 | +%default total |
| 15 | + |
| 16 | +-- --------------------------------------------------------------------------- |
| 17 | +-- Connection state machine |
| 18 | +-- --------------------------------------------------------------------------- |
| 19 | + |
| 20 | +||| Connection state for ArangoDB operations. |
| 21 | +||| Disconnected is the natural resting state for self-hosted instances. |
| 22 | +public export |
| 23 | +data ConnState = Disconnected | Connected | QueryRunning | Error |
| 24 | + |
| 25 | +||| Proof that a state transition is valid. |
| 26 | +public export |
| 27 | +data ValidTransition : ConnState -> ConnState -> Type where |
| 28 | + Connect : ValidTransition Disconnected Connected |
| 29 | + StartQuery : ValidTransition Connected QueryRunning |
| 30 | + FinishQuery : ValidTransition QueryRunning Connected |
| 31 | + Disconnect : ValidTransition Connected Disconnected |
| 32 | + QueryFail : ValidTransition QueryRunning Error |
| 33 | + ErrorRecover : ValidTransition Error Disconnected |
| 34 | + |
| 35 | +-- --------------------------------------------------------------------------- |
| 36 | +-- C-ABI integer encoding |
| 37 | +-- --------------------------------------------------------------------------- |
| 38 | + |
| 39 | +||| Encode connection state as C-compatible integer. |
| 40 | +export |
| 41 | +connStateToInt : ConnState -> Int |
| 42 | +connStateToInt Disconnected = 0 |
| 43 | +connStateToInt Connected = 1 |
| 44 | +connStateToInt QueryRunning = 2 |
| 45 | +connStateToInt Error = 3 |
| 46 | + |
| 47 | +||| Decode integer back to connection state. |
| 48 | +export |
| 49 | +intToConnState : Int -> Maybe ConnState |
| 50 | +intToConnState 0 = Just Disconnected |
| 51 | +intToConnState 1 = Just Connected |
| 52 | +intToConnState 2 = Just QueryRunning |
| 53 | +intToConnState 3 = Just Error |
| 54 | +intToConnState _ = Nothing |
| 55 | + |
| 56 | +||| Check if a state transition is valid (C-ABI export). |
| 57 | +||| Returns 1 for valid, 0 for invalid. |
| 58 | +export |
| 59 | +arango_mcp_can_transition : Int -> Int -> Int |
| 60 | +arango_mcp_can_transition from to = |
| 61 | + case (intToConnState from, intToConnState to) of |
| 62 | + (Just Disconnected, Just Connected) => 1 |
| 63 | + (Just Connected, Just QueryRunning) => 1 |
| 64 | + (Just QueryRunning, Just Connected) => 1 |
| 65 | + (Just Connected, Just Disconnected) => 1 |
| 66 | + (Just QueryRunning, Just Error) => 1 |
| 67 | + (Just Error, Just Disconnected) => 1 |
| 68 | + _ => 0 |
| 69 | + |
| 70 | +-- --------------------------------------------------------------------------- |
| 71 | +-- ArangoDB actions (full REST API surface) |
| 72 | +-- --------------------------------------------------------------------------- |
| 73 | + |
| 74 | +||| Actions supported by the ArangoDB MCP cartridge. |
| 75 | +||| Covers databases, collections, documents, AQL queries, and graphs. |
| 76 | +public export |
| 77 | +data ArangoAction |
| 78 | + = ListDatabases |
| 79 | + | CreateDatabase |
| 80 | + | DropDatabase |
| 81 | + | ListCollections |
| 82 | + | CreateCollection |
| 83 | + | DropCollection |
| 84 | + | GetDocument |
| 85 | + | InsertDocument |
| 86 | + | UpdateDocument |
| 87 | + | RemoveDocument |
| 88 | + | AqlQuery |
| 89 | + | ExplainQuery |
| 90 | + | TraverseGraph |
| 91 | + | ListGraphs |
| 92 | + | CreateGraph |
| 93 | + | DropGraph |
| 94 | + |
| 95 | +||| Encode action as C-compatible integer. |
| 96 | +export |
| 97 | +arangoActionToInt : ArangoAction -> Int |
| 98 | +arangoActionToInt ListDatabases = 0 |
| 99 | +arangoActionToInt CreateDatabase = 1 |
| 100 | +arangoActionToInt DropDatabase = 2 |
| 101 | +arangoActionToInt ListCollections = 3 |
| 102 | +arangoActionToInt CreateCollection = 4 |
| 103 | +arangoActionToInt DropCollection = 5 |
| 104 | +arangoActionToInt GetDocument = 6 |
| 105 | +arangoActionToInt InsertDocument = 7 |
| 106 | +arangoActionToInt UpdateDocument = 8 |
| 107 | +arangoActionToInt RemoveDocument = 9 |
| 108 | +arangoActionToInt AqlQuery = 10 |
| 109 | +arangoActionToInt ExplainQuery = 11 |
| 110 | +arangoActionToInt TraverseGraph = 12 |
| 111 | +arangoActionToInt ListGraphs = 13 |
| 112 | +arangoActionToInt CreateGraph = 14 |
| 113 | +arangoActionToInt DropGraph = 15 |
| 114 | + |
| 115 | +||| Decode integer back to action. |
| 116 | +export |
| 117 | +intToArangoAction : Int -> Maybe ArangoAction |
| 118 | +intToArangoAction 0 = Just ListDatabases |
| 119 | +intToArangoAction 1 = Just CreateDatabase |
| 120 | +intToArangoAction 2 = Just DropDatabase |
| 121 | +intToArangoAction 3 = Just ListCollections |
| 122 | +intToArangoAction 4 = Just CreateCollection |
| 123 | +intToArangoAction 5 = Just DropCollection |
| 124 | +intToArangoAction 6 = Just GetDocument |
| 125 | +intToArangoAction 7 = Just InsertDocument |
| 126 | +intToArangoAction 8 = Just UpdateDocument |
| 127 | +intToArangoAction 9 = Just RemoveDocument |
| 128 | +intToArangoAction 10 = Just AqlQuery |
| 129 | +intToArangoAction 11 = Just ExplainQuery |
| 130 | +intToArangoAction 12 = Just TraverseGraph |
| 131 | +intToArangoAction 13 = Just ListGraphs |
| 132 | +intToArangoAction 14 = Just CreateGraph |
| 133 | +intToArangoAction 15 = Just DropGraph |
| 134 | +intToArangoAction _ = Nothing |
| 135 | + |
| 136 | +||| Check whether an action requires an active connection. |
| 137 | +export |
| 138 | +actionRequiresConnection : ArangoAction -> Bool |
| 139 | +actionRequiresConnection AqlQuery = True |
| 140 | +actionRequiresConnection ExplainQuery = True |
| 141 | +actionRequiresConnection GetDocument = True |
| 142 | +actionRequiresConnection InsertDocument = True |
| 143 | +actionRequiresConnection UpdateDocument = True |
| 144 | +actionRequiresConnection RemoveDocument = True |
| 145 | +actionRequiresConnection TraverseGraph = True |
| 146 | +actionRequiresConnection _ = False |
| 147 | + |
| 148 | +||| Total number of actions exposed by this cartridge. |
| 149 | +export |
| 150 | +actionCount : Nat |
| 151 | +actionCount = 16 |
| 152 | + |
| 153 | +-- --------------------------------------------------------------------------- |
| 154 | +-- Auth configuration |
| 155 | +-- --------------------------------------------------------------------------- |
| 156 | + |
| 157 | +||| Authentication methods for ArangoDB REST API. |
| 158 | +||| Supports both Bearer token (JWT) and Basic auth (username/password). |
| 159 | +public export |
| 160 | +data ArangoAuth = BearerToken | BasicAuth |
| 161 | + |
| 162 | +||| Base URL placeholder for ArangoDB REST API (self-hosted, configurable). |
| 163 | +export |
| 164 | +arangoApiBase : String |
| 165 | +arangoApiBase = "https://{host}:8529/_api/" |
0 commit comments