/ concept-collection / proofery
Sign in
concept-collection / proofery
proofery / src / parser.ts
191 lines · 5.7 KBBlameHistoryRaw
1/**
2 * Parser for .prf files.
3 */
5import { Block } from './block.js';
6import { Expression, parseExpression } from './expression.js';
7import { ParseError } from './errors.js';
9interface ParsedLine {
10 lineNum: number;
11 level: number;
12 text: string;
15/**
16 * Parse .prf content and return a list of top-level blocks.
17 * This is the main parsing function that works in both browser and Node.js.
18 */
19export function parseContent(content: string): Block[] {
20 const lines = content.split('\n');
22 // Parse lines with their indentation levels
23 const parsedLines: ParsedLine[] = [];
24 let indentUnit: string | null = null;
26 for (let i = 0; i < lines.length; i++) {
27 const lineNum = i + 1;
28 let line = lines[i];
30 // Remove trailing newline/carriage return
31 line = line.replace(/\r?\n?$/, '');
33 // Skip empty lines and comments
34 if (!line.trim() || line.trim().startsWith('#')) {
35 continue;
36 }
38 // Detect indentation
39 let indentLevel = 0;
40 const stripped = line.trimStart();
41 const indentStr = line.substring(0, line.length - stripped.length);
43 if (indentStr) {
44 // Detect indent unit from first indented line
45 if (indentUnit === null) {
46 indentUnit = indentStr;
47 indentLevel = 1;
48 } else {
49 // Check if indentation is consistent
50 if (indentStr.length % indentUnit.length !== 0) {
51 throw new ParseError(`Line ${lineNum}: Inconsistent indentation`);
52 }
53 indentLevel = indentStr.length / indentUnit.length;
54 }
55 }
57 parsedLines.push({ lineNum, level: indentLevel, text: stripped });
58 }
60 // Build block tree
61 return buildBlocks(parsedLines, 0, 0).blocks;
64interface BuildResult {
65 blocks: Block[];
66 nextIdx: number;
69/**
70 * Recursively build block tree from parsed lines.
71 */
72function buildBlocks(parsedLines: ParsedLine[], startIdx: number, expectedLevel: number): BuildResult {
73 const blocks: Block[] = [];
74 let idx = startIdx;
76 while (idx < parsedLines.length) {
77 const { lineNum, level, text } = parsedLines[idx];
79 // If we've gone back to a lower level, return to parent
80 if (level < expectedLevel) {
81 break;
82 }
84 // Skip lines at deeper levels (they'll be processed as children)
85 if (level > expectedLevel) {
86 throw new ParseError(`Line ${lineNum}: Unexpected indentation`);
87 }
89 // Parse the block
90 const block = parseBlock(lineNum, text);
92 // Process children at the next level
93 if (idx + 1 < parsedLines.length) {
94 const nextLevel = parsedLines[idx + 1].level;
95 if (nextLevel > level) {
96 const result = buildBlocks(parsedLines, idx + 1, level + 1);
97 block.children = result.blocks;
98 blocks.push(block);
99 idx = result.nextIdx;
100 continue;
101 }
102 }
104 blocks.push(block);
105 idx++;
106 }
108 return { blocks, nextIdx: idx };
111/**
112 * Parse a single block line into a Block object.
113 */
114function parseBlock(lineNum: number, lineText: string): Block {
115 // Split the line into tokens
116 const tokens = tokenize(lineText, lineNum);
118 if (tokens.length === 0) {
119 throw new ParseError(`Line ${lineNum}: Empty block`);
120 }
122 const blockType = tokens[0];
123 const remainingTokens = tokens.slice(1);
125 // Handle blocks with "name : type" pattern at the argument level
126 // For suppose, assert, define, we-have, case: expect 3 tokens (name, :, type)
127 let args: Expression[];
128 if (['suppose', 'assert', 'define', 'we-have', 'case'].includes(blockType)) {
129 if (remainingTokens.length === 3 && remainingTokens[1] === ':') {
130 const varName = remainingTokens[0];
131 const varTypeText = remainingTokens[2];
132 const varType = parseExpression(varTypeText, lineNum);
133 args = [new Expression('var', [new Expression(varName), varType])];
134 } else {
135 throw new ParseError(`Line ${lineNum}: '${blockType}' must have format 'name : type'`);
136 }
137 } else {
138 // Parse the remaining tokens as expressions
139 args = remainingTokens.map(token => parseExpression(token, lineNum));
140 }
142 return new Block(lineNum, blockType, args);
145/**
146 * Tokenize a line, respecting parentheses and colons.
147 */
148function tokenize(line: string, lineNum: number): string[] {
149 const tokens: string[] = [];
150 let currentToken = '';
151 let depth = 0;
153 for (const ch of line) {
154 if (ch === '(' && depth === 0) {
155 // Start of arguments
156 currentToken += ch;
157 depth++;
158 } else if (ch === '(') {
159 currentToken += ch;
160 depth++;
161 } else if (ch === ')') {
162 currentToken += ch;
163 depth--;
164 } else if (ch === ':' && depth === 0) {
165 // Colon outside parentheses - token separator and also a token
166 if (currentToken.trim()) {
167 tokens.push(currentToken.trim());
168 currentToken = '';
169 }
170 tokens.push(':');
171 } else if (ch === ' ' && depth === 0) {
172 // Space outside parentheses - token separator
173 if (currentToken.trim()) {
174 tokens.push(currentToken.trim());
175 currentToken = '';
176 }
177 } else {
178 currentToken += ch;
179 }
180 }
182 if (currentToken.trim()) {
183 tokens.push(currentToken.trim());
184 }
186 if (depth !== 0) {
187 throw new ParseError(`Line ${lineNum}: Mismatched parentheses`);
188 }
190 return tokens.filter(t => t.length > 0);
moveopenescclose