forked from Lorenzobattistela/agda-check
-
Notifications
You must be signed in to change notification settings - Fork 1
/
agda-cli.js
executable file
·376 lines (336 loc) · 11.2 KB
/
agda-cli.js
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
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
#!/usr/bin/env node
const { spawn } = require("child_process");
const readline = require("readline");
const fs = require("fs");
const path = require("path");
const command = process.argv[2];
const filePath = process.argv[3];
function simplifyAgdaOutput(output) {
// Regular expression to match module paths
const modulePathRegex = /([A-Za-z0-9]+\.)+([A-Za-z0-9]+)(?=[\s\n])/g;
// Replace full module paths with just the last part
return output.replace(modulePathRegex, (match) => {
const parts = match.split('.');
return parts[parts.length - 1];
});
}
// Execute an Agda command and return the output as a Promise
function executeAgdaCommand(command) {
return new Promise((resolve, reject) => {
const agda = spawn("agda", ["--interaction-json", "--no-allow-incomplete-matches", "--no-termination-check", "--no-libraries", "--allow-unsolved-metas"]);
let output = "";
agda.stdout.on("data", (data) => output += data.toString());
agda.stderr.on("data", (data) => console.error(`Agda Error: ${data}`));
agda.on("close", (code) => {
if (code !== 0) {
reject(`Agda process exited with code ${code}`);
} else {
resolve(output);
}
});
agda.stdin.write(command);
agda.stdin.end();
});
}
// Gets all '{!!}' holes in an Agda file
function getFileHoles(filePath) {
let holeId = 0;
let holes = [];
// Read the file content
const fileContent = fs.readFileSync(filePath, "utf-8");
const lines = fileContent.split("\n");
lines.forEach((line, index) => {
const row = index + 1;
const regex = /\{\!(.*?)\!\}/g;
let match;
while ((match = regex.exec(line)) !== null) {
const col = match.index + 1;
const content = match[1].trim() || "?";
holes.push([holeId, row, col, content]);
holeId++;
}
});
return holes;
}
// Sends an Agda command and executes it
async function sendCommand(arg, quiet=false, interact=false) {
return await executeAgdaCommand(`IOTCM "${filePath}" ${interact ? "Interactive" : "None"} Direct (${arg})\nx\n`);
}
// Checks the Agda file and prints hole information
async function agdaCheck() {
var output = "";
// Sends the Load command
output += await sendCommand(`Cmd_load "${filePath}" []`) + "\n";
// Iterate through holes and send Cmd_goal_type_context_infer command for each
try {
let holes = getFileHoles(filePath);
for (const hole of holes) {
let holeId = hole[0];
let content = hole[3];
if (holeId != null) {
output += await sendCommand(`Cmd_goal_type_context_infer Normalised ${holeId} noRange "${content.trim()}"`) + "\n";
}
}
} catch (error) {
console.error("Error:", error);
}
return output;
}
// Runs the Agda program and returns the output
async function agdaRun() {
var output = "";
// Load the file first
output += await sendCommand(`Cmd_load "${filePath}" []`) + "\n";
// Then, execute the 'main' function
output += await sendCommand(`Cmd_compute_toplevel DefaultCompute "main"`) + "\n";
return output;
}
// Parses JSON objects from the Agda output string
function parseJsonObjects(str) {
const jsonObjects = [];
const lines = str.split('\n');
for (let line of lines) {
if (line.startsWith('JSON>')) {
line = line.substring(6).trim();
}
if (line) {
try {
jsonObjects.push(JSON.parse(line));
} catch (e) {
// Ignore non-JSON lines
}
}
}
return jsonObjects;
}
// Extracts hole information from a JSON object
function extractHoleInfo(obj) {
if (obj.kind === 'DisplayInfo' && obj.info && obj.info.kind === 'GoalSpecific') {
const holeInfo = obj.info;
return {
type : 'hole',
id : holeInfo.interactionPoint.id,
range : holeInfo.interactionPoint.range[0],
goal : holeInfo.goalInfo.type,
context: holeInfo.goalInfo.entries
};
}
return null;
}
// Extracts error information from a JSON object
function extractErrorInfo(obj) {
if (obj.kind === 'DisplayInfo' && obj.info && (obj.info.error || obj.info.errors)) {
let errors = [];
if (obj.info.error) {
// Single error case
errors.push({
type: 'error',
message: obj.info.error.message
});
} else if (obj.info.errors) {
// Multiple errors case
errors = obj.info.errors.map(error => ({
type: 'error',
message: error.message
}));
}
return errors;
}
return null;
}
// Formats hole information for pretty printing
function formatHoleInfo(hole, fileContent) {
const bold = '\x1b[1m';
const dim = '\x1b[2m';
const underline = '\x1b[4m';
const reset = '\x1b[0m';
let result = `${bold}Goal: ${hole.goal}${reset}\n`;
for (let entry of hole.context) {
result += `- ${entry.originalName} : ${entry.binding}\n`;
}
result += `${dim}${underline}${filePath}${reset}\n`;
result += highlightCode(fileContent, hole.range.start.line, hole.range.start.col, hole.range.end.col - 1, hole.range.start.line, 'green');
return simplifyAgdaOutput(result);
}
// Formats error information for pretty printing
function formatErrorInfo(error, fileContent) {
const prettifiedError = prettifyError(error.message);
if (prettifiedError) {
return prettifiedError + '\n' + extractCodeFromError(error.message, fileContent, 'red');
} else {
const bold = '\x1b[1m';
const dim = '\x1b[2m';
const underline = '\x1b[4m';
const reset = '\x1b[0m';
let result = `${bold}Error:${reset} ${error.message}\n`;
const fileInfo = error.message.split(':')[0];
result += `${dim}${underline}${fileInfo}${reset}\n`;
result += extractCodeFromError(error.message, fileContent, 'red');
return result;
}
}
// Attempts to prettify error messages
function prettifyError(errorMessage) {
return prettify_TypeMismatch(errorMessage) || prettify_UnboundVariable(errorMessage);
}
// Prettifies type mismatch errors
function prettify_TypeMismatch(errorMessage) {
const lines = errorMessage.split('\n');
const fileInfo = lines[0].split(':')[0];
const typeMismatchRegex = /(.+) (!=<|!=) (.+)/;
const match = errorMessage.match(typeMismatchRegex);
if (match) {
const detected = match[1].trim();
const expected = match[3].trim();
const bold = '\x1b[1m';
const dim = '\x1b[2m';
const underline = '\x1b[4m';
const reset = '\x1b[0m';
return `${bold}TypeMismatch:${reset}\n- expected: ${expected}\n- detected: ${detected}\n${dim}${underline}${fileInfo}${reset}`;
}
return null;
}
// Prettifies unbound variable errors
function prettify_UnboundVariable(errorMessage) {
const notInScopeRegex = /Not in scope:\n\s+(\w+) at/;
const match = errorMessage.match(notInScopeRegex);
if (match) {
const varName = match[1];
const bold = '\x1b[1m';
const dim = '\x1b[2m';
const underline = '\x1b[4m';
const reset = '\x1b[0m';
const fileInfo = errorMessage.split(':')[0];
return `${bold}Unbound:${reset} '${varName}'\n${dim}${underline}${fileInfo}${reset}`;
}
return null;
}
// Extracts and highlights the affected code from the error message
function extractCodeFromError(errorMessage, fileContent, color) {
const lines = errorMessage.split('\n');
const match = lines[0].match(/(\d+),(\d+)-(?:(\d+),)?(\d+)/);
if (match) {
const iniLine = parseInt(match[1]);
const iniCol = parseInt(match[2]);
const endLine = match[3] ? parseInt(match[3]) : iniLine;
const endCol = parseInt(match[4]);
return highlightCode(fileContent, iniLine, iniCol, endCol - 1, endLine, color);
}
return '';
}
// Highlights the specified code section
function highlightCode(fileContent, startLine, startCol, endCol, endLine, color) {
try {
const lines = fileContent.split('\n');
const dim = '\x1b[2m';
const reset = '\x1b[0m';
const underline = '\x1b[4m';
const colorCode = color === 'red' ? '\x1b[31m' : '\x1b[32m';
let result = '';
const maxLineNumberLength = endLine.toString().length;
for (let i = startLine - 1; i <= endLine - 1; i++) {
const line = lines[i];
const lineNumber = (i + 1).toString().padStart(maxLineNumberLength, ' ');
result += `${dim}${lineNumber} | ${reset}`;
if (i === startLine - 1 && i === endLine - 1) {
result += dim + line.substring(0, startCol - 1);
result += colorCode + underline + line.substring(startCol - 1, endCol) + reset;
result += dim + line.substring(endCol) + reset + '\n';
} else if (i === startLine - 1) {
result += dim + line.substring(0, startCol - 1);
result += colorCode + underline + line.substring(startCol - 1) + reset + '\n';
} else if (i === endLine - 1) {
result += colorCode + underline + line.substring(0, endCol) + reset;
result += dim + line.substring(endCol) + reset + '\n';
} else {
result += colorCode + underline + line + reset + '\n';
}
}
return result;
} catch (e) {
return fileContent;
}
}
// Reads the content of the Agda file
function readFileContent(filePath) {
try {
return fs.readFileSync(filePath, 'utf-8');
} catch (error) {
console.error('Error reading file:', error);
return '';
}
}
// This function processes Agda output to generate a pretty-printed result.
function prettyPrintOutput(out) {
const jsonObjects = parseJsonObjects(out);
const items = [];
const seenErrors = new Set();
for (let obj of jsonObjects) {
const holeInfo = extractHoleInfo(obj);
const errorInfo = extractErrorInfo(obj);
if (holeInfo) {
items.push(holeInfo);
} else if (errorInfo) {
errorInfo.forEach(error => {
if (!seenErrors.has(error.message)) {
items.push(error);
seenErrors.add(error.message);
}
});
}
}
// Generate pretty-printed output
const fileContent = readFileContent(filePath);
let prettyOut = '';
let hasError = false;
for (let item of items) {
if (item.type === 'hole') {
prettyOut += formatHoleInfo(item, fileContent);
} else if (item.type === 'error') {
hasError = true;
prettyOut += formatErrorInfo(item, fileContent);
}
prettyOut += '\n';
}
if (hasError) {
console.error(prettyOut.trim());
} else {
console.log(simplifyAgdaOutput(prettyOut.trim()) || "Checked.");
}
}
// Parses the output of the run command
function parseRunOutput(output) {
const jsonObjects = parseJsonObjects(output);
for (let obj of jsonObjects) {
if (obj.kind === 'DisplayInfo' && obj.info && obj.info.kind === 'NormalForm') {
return simplifyAgdaOutput(obj.info.expr);
}
}
return "No output";
}
async function main() {
if (!filePath || !filePath.endsWith(".agda")) {
console.error("Usage: agda-cli [check|run] <file.agda>");
process.exit(1);
}
switch (command) {
case "check": {
prettyPrintOutput(await agdaCheck());
const output = await agdaRun();
const result = parseRunOutput(output);
console.log(result);
break;
}
case "run": {
const output = await agdaRun();
const result = parseRunOutput(output);
console.log(result);
break;
}
default: {
console.error("Invalid command. Use 'check' or 'run'.");
process.exit(1);
}
}
}
(async () => await main())();