|
| 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 | +-- AffinescriptMcp.SafeCompiler — Type-safe ABI for affinescript-mcp cartridge. |
| 5 | +-- |
| 6 | +-- Dependent-type state machine governing AffineScript compiler invocations. |
| 7 | +-- Encodes type checking, parsing, formatting, error explanation, |
| 8 | +-- stdlib browsing, syntax reference, and snippet evaluation |
| 9 | +-- as compile-time invariants. |
| 10 | +-- Local compiler: `affinescript` CLI (OCaml) |
| 11 | +-- No auth required — local tool invocation. |
| 12 | + |
| 13 | +module AffinescriptMcp.SafeCompiler |
| 14 | + |
| 15 | +%default total |
| 16 | + |
| 17 | +-- --------------------------------------------------------------------------- |
| 18 | +-- Session state machine |
| 19 | +-- --------------------------------------------------------------------------- |
| 20 | + |
| 21 | +||| Session state for AffineScript MCP operations. |
| 22 | +||| Ready: compiler available, ready for invocations. |
| 23 | +||| Busy: compiler invocation in progress. |
| 24 | +||| Error: compiler not found or crashed. |
| 25 | +public export |
| 26 | +data SessionState |
| 27 | + = Ready |
| 28 | + | Busy |
| 29 | + | Error |
| 30 | + |
| 31 | +||| Proof that a state transition is valid. |
| 32 | +public export |
| 33 | +data ValidTransition : SessionState -> SessionState -> Type where |
| 34 | + StartInvocation : ValidTransition Ready Busy |
| 35 | + FinishSuccess : ValidTransition Busy Ready |
| 36 | + FinishError : ValidTransition Busy Error |
| 37 | + Recover : ValidTransition Error Ready |
| 38 | + |
| 39 | +-- --------------------------------------------------------------------------- |
| 40 | +-- C-ABI integer encoding |
| 41 | +-- --------------------------------------------------------------------------- |
| 42 | + |
| 43 | +||| Encode session state as C-compatible integer for FFI boundary. |
| 44 | +export |
| 45 | +sessionStateToInt : SessionState -> Int |
| 46 | +sessionStateToInt Ready = 0 |
| 47 | +sessionStateToInt Busy = 1 |
| 48 | +sessionStateToInt Error = 2 |
| 49 | + |
| 50 | +||| Decode integer back to session state. |
| 51 | +export |
| 52 | +intToSessionState : Int -> Maybe SessionState |
| 53 | +intToSessionState 0 = Just Ready |
| 54 | +intToSessionState 1 = Just Busy |
| 55 | +intToSessionState 2 = Just Error |
| 56 | +intToSessionState _ = Nothing |
| 57 | + |
| 58 | +||| Check if a state transition is valid (C-ABI export). |
| 59 | +export |
| 60 | +afs_mcp_can_transition : Int -> Int -> Int |
| 61 | +afs_mcp_can_transition from to = |
| 62 | + case (intToSessionState from, intToSessionState to) of |
| 63 | + (Just Ready, Just Busy) => 1 |
| 64 | + (Just Busy, Just Ready) => 1 |
| 65 | + (Just Busy, Just Error) => 1 |
| 66 | + (Just Error, Just Ready) => 1 |
| 67 | + _ => 0 |
| 68 | + |
| 69 | +-- --------------------------------------------------------------------------- |
| 70 | +-- Compiler actions |
| 71 | +-- --------------------------------------------------------------------------- |
| 72 | + |
| 73 | +||| Actions available through the AffineScript MCP cartridge. |
| 74 | +public export |
| 75 | +data CompilerAction |
| 76 | + = Check |
| 77 | + | Parse |
| 78 | + | Format |
| 79 | + | ExplainError |
| 80 | + | StdlibSearch |
| 81 | + | SyntaxRef |
| 82 | + | EvalSnippet |
| 83 | + |
| 84 | +||| Whether an action requires authentication. |
| 85 | +||| Local compiler — no auth needed. |
| 86 | +export |
| 87 | +actionRequiresAuth : CompilerAction -> Bool |
| 88 | +actionRequiresAuth _ = False |
| 89 | + |
| 90 | +||| Whether an action mutates state. |
| 91 | +||| All actions are read-only compiler queries. |
| 92 | +export |
| 93 | +actionIsMutating : CompilerAction -> Bool |
| 94 | +actionIsMutating _ = False |
| 95 | + |
| 96 | +||| Whether an action invokes the external compiler. |
| 97 | +||| Some actions (ExplainError, StdlibSearch, SyntaxRef) are pure lookups. |
| 98 | +export |
| 99 | +actionNeedsCompiler : CompilerAction -> Bool |
| 100 | +actionNeedsCompiler Check = True |
| 101 | +actionNeedsCompiler Parse = True |
| 102 | +actionNeedsCompiler Format = False |
| 103 | +actionNeedsCompiler ExplainError = False |
| 104 | +actionNeedsCompiler StdlibSearch = False |
| 105 | +actionNeedsCompiler SyntaxRef = False |
| 106 | +actionNeedsCompiler EvalSnippet = True |
| 107 | + |
| 108 | +||| Encode action as C-compatible integer for FFI. |
| 109 | +export |
| 110 | +actionToInt : CompilerAction -> Int |
| 111 | +actionToInt Check = 0 |
| 112 | +actionToInt Parse = 1 |
| 113 | +actionToInt Format = 2 |
| 114 | +actionToInt ExplainError = 3 |
| 115 | +actionToInt StdlibSearch = 4 |
| 116 | +actionToInt SyntaxRef = 5 |
| 117 | +actionToInt EvalSnippet = 6 |
| 118 | + |
| 119 | +||| Decode integer to compiler action. |
| 120 | +export |
| 121 | +intToAction : Int -> Maybe CompilerAction |
| 122 | +intToAction 0 = Just Check |
| 123 | +intToAction 1 = Just Parse |
| 124 | +intToAction 2 = Just Format |
| 125 | +intToAction 3 = Just ExplainError |
| 126 | +intToAction 4 = Just StdlibSearch |
| 127 | +intToAction 5 = Just SyntaxRef |
| 128 | +intToAction 6 = Just EvalSnippet |
| 129 | +intToAction _ = Nothing |
| 130 | + |
| 131 | +-- --------------------------------------------------------------------------- |
| 132 | +-- MCP tool declarations |
| 133 | +-- --------------------------------------------------------------------------- |
| 134 | + |
| 135 | +||| Tools exposed via MCP protocol. |
| 136 | +public export |
| 137 | +data McpTool |
| 138 | + = ToolCheck |
| 139 | + | ToolParse |
| 140 | + | ToolFormat |
| 141 | + | ToolExplainError |
| 142 | + | ToolStdlib |
| 143 | + | ToolSyntaxRef |
| 144 | + | ToolSnippet |
| 145 | + |
| 146 | +||| Check if a tool needs the compiler subprocess. |
| 147 | +export |
| 148 | +toolNeedsCompiler : McpTool -> Bool |
| 149 | +toolNeedsCompiler ToolCheck = True |
| 150 | +toolNeedsCompiler ToolParse = True |
| 151 | +toolNeedsCompiler ToolFormat = False |
| 152 | +toolNeedsCompiler ToolExplainError = False |
| 153 | +toolNeedsCompiler ToolStdlib = False |
| 154 | +toolNeedsCompiler ToolSyntaxRef = False |
| 155 | +toolNeedsCompiler ToolSnippet = True |
| 156 | + |
| 157 | +||| Total tool count for this cartridge. |
| 158 | +export |
| 159 | +toolCount : Nat |
| 160 | +toolCount = 7 |
| 161 | + |
| 162 | +||| Total action count. |
| 163 | +export |
| 164 | +actionCount : Nat |
| 165 | +actionCount = 7 |
0 commit comments