-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathtest_cli.py
More file actions
executable file
ยท336 lines (274 loc) ยท 11.5 KB
/
Copy pathtest_cli.py
File metadata and controls
executable file
ยท336 lines (274 loc) ยท 11.5 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
#!/usr/bin/env python3
"""
CLI tool to test Idris2 MCP Server functions directly
No MCP dependency required - tests the core logic
"""
import sys
import asyncio
from pathlib import Path
# Add parent directory to path
sys.path.insert(0, str(Path(__file__).parent))
# Import guideline functions (simulated, no MCP needed)
BASE_DIR = Path(__file__).parent
OFFICIAL_GUIDELINES_DIR = BASE_DIR / "guidelines"
def simulate_search_guidelines(query: str, category: str = "all"):
"""Simulate search_guidelines tool"""
search_files = []
if category == "all":
search_files = list(OFFICIAL_GUIDELINES_DIR.glob("*.md"))
elif category == "syntax":
search_files = [OFFICIAL_GUIDELINES_DIR / "01-SYNTAX-BASICS.md"]
elif category == "types":
search_files = [OFFICIAL_GUIDELINES_DIR / "02-TYPE-SYSTEM.md"]
elif category == "modules":
search_files = [OFFICIAL_GUIDELINES_DIR / "03-MODULES-NAMESPACES.md"]
elif category == "advanced":
search_files = [OFFICIAL_GUIDELINES_DIR / "04-ADVANCED-PATTERNS.md"]
elif category == "pragmas":
search_files = [OFFICIAL_GUIDELINES_DIR / "05-PRAGMAS-REFERENCE.md"]
results = []
for file_path in search_files:
if not file_path.exists():
continue
content = file_path.read_text(encoding='utf-8')
lines = content.split('\n')
for i, line in enumerate(lines):
if query.lower() in line.lower():
start = max(0, i - 2)
end = min(len(lines), i + 5)
context = '\n'.join(lines[start:end])
results.append({
'file': file_path.name,
'line': i + 1,
'context': context
})
if len([r for r in results if r['file'] == file_path.name]) >= 3:
break
return results[:10]
def simulate_get_guideline_section(topic: str):
"""Simulate get_guideline_section tool"""
section_map = {
"multiplicities": (OFFICIAL_GUIDELINES_DIR / "02-TYPE-SYSTEM.md", "Multiplicities"),
"dependent_types": (OFFICIAL_GUIDELINES_DIR / "02-TYPE-SYSTEM.md", "Dependent Types"),
"interfaces": (OFFICIAL_GUIDELINES_DIR / "02-TYPE-SYSTEM.md", "Interfaces"),
"modules": (OFFICIAL_GUIDELINES_DIR / "03-MODULES-NAMESPACES.md", "Module Structure"),
"views": (OFFICIAL_GUIDELINES_DIR / "04-ADVANCED-PATTERNS.md", "Views"),
"proofs": (OFFICIAL_GUIDELINES_DIR / "04-ADVANCED-PATTERNS.md", "Theorem Proving"),
"ffi": (OFFICIAL_GUIDELINES_DIR / "04-ADVANCED-PATTERNS.md", "Foreign Function Interface"),
"pragmas_inline": (OFFICIAL_GUIDELINES_DIR / "05-PRAGMAS-REFERENCE.md", "%inline"),
"pragmas_foreign": (OFFICIAL_GUIDELINES_DIR / "05-PRAGMAS-REFERENCE.md", "%foreign"),
"totality": (OFFICIAL_GUIDELINES_DIR / "02-TYPE-SYSTEM.md", "Totality"),
}
if topic not in section_map:
return None, f"Unknown topic: {topic}"
file_path, section_name = section_map[topic]
if not file_path.exists():
return None, f"Guidelines not found at {file_path}"
content = file_path.read_text(encoding='utf-8')
lines = content.split('\n')
section_lines = []
in_section = False
section_level = 0
for line in lines:
if section_name.lower() in line.lower() and line.startswith('#'):
in_section = True
section_level = len(line) - len(line.lstrip('#'))
section_lines.append(line)
elif in_section:
if line.startswith('#'):
current_level = len(line) - len(line.lstrip('#'))
if current_level <= section_level:
break
section_lines.append(line)
if section_lines:
return '\n'.join(section_lines), None
else:
return None, f"Section '{section_name}' not found"
def read_resource(uri: str):
"""Simulate resource reading"""
resource_map = {
"idris2://guidelines/syntax": OFFICIAL_GUIDELINES_DIR / "01-SYNTAX-BASICS.md",
"idris2://guidelines/types": OFFICIAL_GUIDELINES_DIR / "02-TYPE-SYSTEM.md",
"idris2://guidelines/modules": OFFICIAL_GUIDELINES_DIR / "03-MODULES-NAMESPACES.md",
"idris2://guidelines/advanced": OFFICIAL_GUIDELINES_DIR / "04-ADVANCED-PATTERNS.md",
"idris2://guidelines/pragmas": OFFICIAL_GUIDELINES_DIR / "05-PRAGMAS-REFERENCE.md",
"idris2://guidelines/index": OFFICIAL_GUIDELINES_DIR / "README.md",
}
if uri in resource_map:
file_path = resource_map[uri]
if file_path.exists():
return file_path.read_text(encoding='utf-8')
else:
return f"Guidelines not found at {file_path}"
else:
return f"Unknown resource: {uri}"
def test_search():
"""Test search_guidelines"""
print("=" * 70)
print("TEST: search_guidelines")
print("=" * 70)
queries = [
("dependent types", "types"),
("linear", "all"),
("%inline", "pragmas"),
]
for query, category in queries:
print(f"\n๐ Query: '{query}' (category: {category})")
print("-" * 70)
results = simulate_search_guidelines(query, category)
print(f"Found {len(results)} results:")
for i, r in enumerate(results[:3], 1):
print(f"\n [{i}] {r['file']} (line {r['line']})")
context_preview = r['context'].replace('\n', '\n ')[:200]
print(f" {context_preview}...")
def test_section():
"""Test get_guideline_section"""
print("\n" + "=" * 70)
print("TEST: get_guideline_section")
print("=" * 70)
topics = [
"parser_constraints",
"multiplicities",
"dependent_types",
]
for topic in topics:
print(f"\n๐ Topic: '{topic}'")
print("-" * 70)
content, error = simulate_get_guideline_section(topic)
if error:
print(f"โ Error: {error}")
else:
lines = content.split('\n')
print(f"โ
Extracted {len(lines)} lines")
preview = '\n'.join(lines[:15])
print(f"\nPreview:\n{preview}")
if len(lines) > 15:
print(f"... ({len(lines) - 15} more lines)")
def test_resources():
"""Test resource reading"""
print("\n" + "=" * 70)
print("TEST: read_resource")
print("=" * 70)
resources = [
"idris2://guidelines/project",
"idris2://guidelines/syntax",
"idris2://guidelines/types",
]
for uri in resources:
print(f"\n๐ Resource: {uri}")
print("-" * 70)
content = read_resource(uri)
lines = content.split('\n')
print(f"โ
Loaded {len(lines)} lines ({len(content)} bytes)")
# Show first header
for line in lines[:20]:
if line.startswith('#'):
print(f" First header: {line}")
break
def interactive_mode():
"""Interactive CLI for testing"""
print("\n" + "=" * 70)
print("๐ฎ INTERACTIVE MODE")
print("=" * 70)
print("\nCommands:")
print(" search <query> [category] - Search guidelines")
print(" section <topic> - Get guideline section")
print(" resource <uri> - Read resource")
print(" list - List all topics/resources")
print(" help - Show this help")
print(" quit - Exit")
print()
while True:
try:
cmd = input("idris2-mcp> ").strip()
if not cmd:
continue
if cmd == "quit":
print("๐ Goodbye!")
break
elif cmd == "help":
print("\nCommands:")
print(" search <query> [category]")
print(" section <topic>")
print(" resource <uri>")
print(" list")
print(" quit")
elif cmd == "list":
print("\n๐ Available Topics:")
topics = ["parser_constraints", "multiplicities", "dependent_types",
"interfaces", "modules", "views", "proofs", "ffi",
"pragmas_inline", "pragmas_foreign", "totality"]
for t in topics:
print(f" - {t}")
print("\n๐ Available Resources:")
resources = ["idris2://guidelines/project", "idris2://guidelines/syntax",
"idris2://guidelines/types", "idris2://guidelines/modules",
"idris2://guidelines/advanced", "idris2://guidelines/pragmas",
"idris2://guidelines/index"]
for r in resources:
print(f" - {r}")
elif cmd.startswith("search "):
parts = cmd.split(maxsplit=2)
query = parts[1] if len(parts) > 1 else ""
category = parts[2] if len(parts) > 2 else "all"
if query:
results = simulate_search_guidelines(query, category)
print(f"\n๐ Found {len(results)} results for '{query}':")
for i, r in enumerate(results[:5], 1):
print(f"\n[{i}] {r['file']} (line {r['line']})")
print(r['context'][:200] + "...")
else:
print("โ Usage: search <query> [category]")
elif cmd.startswith("section "):
topic = cmd.split(maxsplit=1)[1] if len(cmd.split()) > 1 else ""
if topic:
content, error = simulate_get_guideline_section(topic)
if error:
print(f"โ {error}")
else:
lines = content.split('\n')
print(f"\n๐ Section '{topic}' ({len(lines)} lines):\n")
print('\n'.join(lines[:30]))
if len(lines) > 30:
print(f"\n... ({len(lines) - 30} more lines)")
else:
print("โ Usage: section <topic>")
elif cmd.startswith("resource "):
uri = cmd.split(maxsplit=1)[1] if len(cmd.split()) > 1 else ""
if uri:
content = read_resource(uri)
lines = content.split('\n')
print(f"\n๐ Resource '{uri}' ({len(lines)} lines):\n")
print('\n'.join(lines[:30]))
if len(lines) > 30:
print(f"\n... ({len(lines) - 30} more lines)")
else:
print("โ Usage: resource <uri>")
else:
print(f"โ Unknown command: {cmd}")
print(" Type 'help' for available commands")
except KeyboardInterrupt:
print("\n\n๐ Goodbye!")
break
except EOFError:
print("\n\n๐ Goodbye!")
break
except Exception as e:
print(f"โ Error: {e}")
def main():
"""Main entry point"""
if len(sys.argv) > 1 and sys.argv[1] == "--interactive":
interactive_mode()
else:
print("๐งช Idris2 MCP Server - CLI Test Suite")
print("=" * 70)
test_search()
test_section()
test_resources()
print("\n" + "=" * 70)
print("โ
All tests completed!")
print("=" * 70)
print("\nTip: Run with --interactive for interactive mode")
print(" python test_cli.py --interactive")
if __name__ == "__main__":
main()