speckl/compiler/dist/parser.js
Scott Scoble d16df7581a fix: resolve all TypeScript codegen bugs for zero tsc --noEmit errors
Parser fixes:
- Fixed multiline state/init block parsing: trailing commas no longer
  treated as continuation markers, merging all state vars into one
- Added splitFields() function for comma-aware emit field splitting
  that respects parenthesized groups and quoted strings
- Fixed interface block parsing: enum-style interfaces (name-only
  values like 'Idle, Parsing, Parsed, ...') now correctly parsed as
  methods instead of being skipped (methods.length was 0)

TypeScript generator fixes:
- String[] array type syntax now correctly maps to string[] in output
- collectIdents filters out names containing brackets
- Duplicate event interfaces deduplicated (implicit emit events
  filtered when explicit events already declare them)
- join(X, Y) translates to X + Y (string concatenation) instead of
  X.join(Y) which is wrong for string args
- now() generates new Date().toISOString() instead of Date.now()
  to match String/string type annotations
- decisionLog type uses proper union: (A | B | C)[] instead of A[]
- String literals protected from this.-prefixing during identifier
  replacement (fixes 'leader' inside quotes becoming 'this.leader')
- Removed debug console.log from enum generation

Both TigerBeetleLedger.speck and speckl-compile.speckdl now generate
TypeScript that passes tsc --noEmit with zero errors.

Closes #9
2026-05-13 14:34:51 -07:00

1092 lines
No EOL
42 KiB
JavaScript
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import fs from 'fs';
/**
* Parse a .speck file and return the AST
*/
export function parseSpeckFile(filePath) {
const content = fs.readFileSync(filePath, 'utf-8');
return parseSpeckContent(content, filePath);
}
/**
* Parse SpeckDL content and return the AST
*/
export function parseSpeckContent(content, filePath) {
const specks = [];
const lines = content.split('\n');
let i = 0;
while (i < lines.length) {
const line = lines[i].trim();
// Skip empty lines and comments
if (!line || line.startsWith('//') || line.startsWith('/*')) {
i++;
continue;
}
// Handle import statements
if (line.startsWith('import ')) {
const importNode = parseImportStatement(line);
// Import is a special case - it's not part of a speck
// We'll handle it separately in a future update
i++;
continue;
}
// Handle speck definitions
if (line.startsWith('speck ')) {
const speck = parseSpeck(lines, i);
if (speck) {
specks.push(speck);
// Move index past the speck we just parsed
i++; // Increment by 1, the loop will continue from next line
}
else {
i++;
}
continue;
}
i++;
}
return { specks };
}
function parseSpeck(lines, startIndex) {
const headerMatch = lines[startIndex].match(/^speck\s+([\w-]+)\s*{/);
if (!headerMatch)
return null;
const name = headerMatch[1];
const members = [];
let i = startIndex + 1;
let braceCount = 1;
while (i < lines.length && braceCount > 0) {
const rawLine = lines[i];
const line = rawLine.trim();
if (!line || line.startsWith('//') || line.startsWith('/*')) {
i++;
continue;
}
// Count braces on this line first
const openCount = (rawLine.match(/{/g) || []).length;
const closeCount = (rawLine.match(/}/g) || []).length;
// Check for block-opening members (those that open braces on the same line)
const blockStarters = ['state:', 'init:', 'action ', 'event ', 'provenance ', 'bom ', 'interface ',
'state {', 'init {', 'verify ', 'constraint '];
const isBlockStarter = blockStarters.some(s => line.startsWith(s));
if (isBlockStarter && openCount > 0) {
// Multi-line block: parse it and skip to its end
const member = parseMemberBlock(lines, i);
if (member) {
members.push(member);
}
// Skip past this block if it spans multiple lines
if (closeCount < openCount) {
const endIdx = findBlockEnd(lines, i + 1, braceCount + openCount);
i = endIdx + 1;
}
else {
i++;
}
continue;
}
// Handle constraint/verify blocks that may span multiple lines without braces
// (e.g. constraint Name: forall r in [0..4]:)
if (line.startsWith('constraint ') || line.startsWith('verify ')) {
const member = parseMultiLineConstraintVerify(lines, i);
if (member) {
members.push(member);
// Skip past the consumed continuation lines
while (i + 1 < lines.length) {
const nextLine = lines[i + 1].trim();
if (!nextLine || nextLine.startsWith('//') || nextLine.startsWith('/*') ||
nextLine.startsWith('constraint ') || nextLine.startsWith('verify ') ||
nextLine.startsWith('constraint:') || nextLine.startsWith('verify:') ||
nextLine.startsWith('state') || nextLine.startsWith('init') ||
nextLine.startsWith('action ') || nextLine.startsWith('event ') ||
nextLine.startsWith('interface ') || nextLine.startsWith('provenance ') ||
nextLine.startsWith('bom ') || nextLine.startsWith('}') ||
nextLine.startsWith('next:') || nextLine.startsWith('invariant ')) {
break;
}
i++;
}
}
i++;
continue;
}
// Single-line: update brace count, then parse if still inside
braceCount += openCount - closeCount;
if (braceCount <= 0) {
i++;
break;
}
const member = parseMember(line);
if (member) {
members.push(member);
}
i++;
}
return { type: 'speck', name, members };
}
function findBlockEnd(lines, startIndex, startBraceCount) {
let braceCount = startBraceCount;
let i = startIndex;
while (i < lines.length) {
const line = lines[i];
for (const ch of line) {
if (ch === '{')
braceCount++;
if (ch === '}') {
braceCount--;
if (braceCount < startBraceCount) {
return i;
}
}
}
i++;
}
return i;
}
// Check if an expression has balanced braces, parens, and brackets
function isExpressionComplete(expr) {
let braces = 0, parens = 0, brackets = 0;
for (const char of expr) {
if (char === '{')
braces++;
else if (char === '}')
braces--;
else if (char === '(')
parens++;
else if (char === ')')
parens--;
else if (char === '[')
brackets++;
else if (char === ']')
brackets--;
}
return braces === 0 && parens === 0 && brackets === 0;
}
function parseMemberBlock(lines, startIndex) {
const firstLine = lines[startIndex].trim();
const startBraceCount = (firstLine.match(/{/g) || []).length;
if (firstLine.startsWith('state:')) {
return parseStateBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('state {') || firstLine === 'state') {
return parseStateBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('init:')) {
return parseInitBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('init {') || firstLine === 'init') {
return parseInitBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('action ')) {
return parseActionBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('event ')) {
return parseEventBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('interface ')) {
return parseInterfaceBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('provenance ')) {
return { type: 'provenance', clauses: [] };
}
if (firstLine.startsWith('bom ')) {
return { type: 'bom' };
}
if (firstLine.startsWith('verify ')) {
return parseVerifyBlockMultiline(lines, startIndex, startBraceCount);
}
if (firstLine.startsWith('constraint ')) {
return parseConstraintBlockMultiline(lines, startIndex, startBraceCount);
}
return null;
}
function parseMember(line) {
// input:
if (line.startsWith('input:')) {
const typeExpr = parseTypeExpr(line.substring(6).trim());
return { type: 'input', typeExpr };
}
// output:
if (line.startsWith('output:')) {
const typeExpr = parseTypeExpr(line.substring(7).trim());
return { type: 'output', typeExpr };
}
// constraint Name: expr (single-line named constraint)
if (line.startsWith('constraint ')) {
const match = line.match(/^constraint\s+(\w+):\s*(.+)$/);
if (match) {
return { type: 'constraint', name: match[1], expr: match[2].trim() };
}
return null; // multi-line constraint block (handled by parseMemberBlock)
}
// constraint: expr (unnamed, single-line)
if (line.startsWith('constraint:')) {
return { type: 'constraint', expr: line.substring(11).trim() };
}
// verify Always(Name) { depth N } or verify Always(Name) (single-line forms)
if (line.startsWith('verify ')) {
return parseVerifySingleLine(line);
}
// verify: expr (old unnamed single-line)
if (line.startsWith('verify:')) {
return { type: 'verify', name: 'unnamed', temporalExpr: line.substring(7).trim() };
}
// interface:
if (line.startsWith('interface ')) {
return parseInterface(line);
}
// event:
if (line.startsWith('event ')) {
return parseEvent(line);
}
// provenance {
if (line.startsWith('provenance ')) {
return { type: 'provenance', clauses: [] };
}
// review:
if (line.startsWith('review:')) {
const kind = line.substring(7).trim();
return { type: 'review', kind };
}
// derives from:
if (line.startsWith('derives from ')) {
return parseDerives(line);
}
// satisfies:
if (line.startsWith('satisfies ')) {
return parseSatisfies(line);
}
// author:
if (line.startsWith('author:')) {
return parseAuthor(line);
}
// source:
if (line.startsWith('source:')) {
return parseSource(line);
}
// state: or state {
if (line.startsWith('state:')) {
const varsStr = line.substring(6).trim();
// state: { ... } - single-line form
if (varsStr.startsWith('{') && varsStr.endsWith('}')) {
const inner = varsStr.slice(1, -1).trim();
return parseStateBlock(inner);
}
// state: { - multi-line opening (handled by parseStateMultiline)
return { type: 'state', variables: [] };
}
if (line.startsWith('state {') || line === 'state') {
// state { ... } inline or state { on its own line (handled by parseMemberBlock)
if (line.startsWith('state {')) {
const inner = line.substring(6).trim();
const content = inner.startsWith('{') ? inner.slice(1).trim() : inner;
if (content.endsWith('}')) {
return parseStateBlock(content.slice(0, -1).trim());
}
}
return { type: 'state', variables: [] };
}
// init: or init {
if (line.startsWith('init:')) {
const initStr = line.substring(5).trim();
if (initStr.startsWith('{') && initStr.endsWith('}')) {
const inner = initStr.slice(1, -1).trim();
return parseInitBlock(inner);
}
return { type: 'init', assignments: [] };
}
if (line.startsWith('init {') || line === 'init') {
// init { ... } inline
if (line.startsWith('init {')) {
const inner = line.substring(5).trim();
const content = inner.startsWith('{') ? inner.slice(1).trim() : inner;
if (content.endsWith('}')) {
return parseInitBlock(content.slice(0, -1).trim());
}
}
return { type: 'init', assignments: [] };
}
// action keyword
if (line.startsWith('action ')) {
return parseActionHeader(line);
}
// bom {
if (line.startsWith('bom ')) {
// Simplified - full BOM block parsing would need multi-line context
return {
type: 'bom',
};
}
return null;
}
function parseStateBlock(inner) {
const variables = [];
if (!inner.trim())
return { type: 'state', variables };
const varStrs = inner.split(/;|\n/).map(s => s.trim()).filter(Boolean);
for (const vStr of varStrs) {
const withDefault = vStr.match(/^(\w+)\s*:\s*(.+?)\s*:=\s*(.+)$/);
if (withDefault) {
// Strip trailing comments from type expression
let typeStr = withDefault[2].trim();
const commentIdx = typeStr.indexOf('//');
if (commentIdx >= 0)
typeStr = typeStr.substring(0, commentIdx).trim();
variables.push({
name: withDefault[1],
typeExpr: parseTypeExpr(typeStr),
defaultInit: withDefault[3].trim(),
});
continue;
}
const withoutDefault = vStr.match(/^(\w+)\s*:\s*(.+)$/);
if (withoutDefault) {
// Strip trailing comments from type expression
let typeStr = withoutDefault[2].trim();
const commentIdx = typeStr.indexOf('//');
if (commentIdx >= 0)
typeStr = typeStr.substring(0, commentIdx).trim();
variables.push({
name: withoutDefault[1],
typeExpr: parseTypeExpr(typeStr),
});
}
}
return { type: 'state', variables };
}
function parseInitBlock(inner) {
const assignments = [];
if (!inner.trim())
return { type: 'init', assignments };
const assignStrs = inner.split(/;|\n/).map(s => s.trim()).filter(Boolean);
for (const aStr of assignStrs) {
const match = aStr.match(/^(\w+)\s*:=\s*(.+)$/);
if (match) {
assignments.push({ name: match[1], expr: match[2].trim() });
}
}
return { type: 'init', assignments };
}
function parseActionHeader(line) {
const match = line.match(/^action\s+(\w+)\s*(?:\(([^)]*)\))?\s*\{/);
if (!match)
return null;
const name = match[1];
const paramsStr = match[2] || '';
const params = [];
if (paramsStr.trim()) {
const paramPairs = paramsStr.split(',').map(s => s.trim()).filter(Boolean);
for (const p of paramPairs) {
const pMatch = p.match(/^(\w+)\s*:\s*(.+)$/);
if (pMatch) {
params.push({ name: pMatch[1], type: parseTypeExpr(pMatch[2].trim()) });
}
}
}
return { type: 'action', name, params, statements: [] };
}
function parseImportStatement(line) {
const match = line.match(/^import\s+(['"])(.+?)\1(?:\s+as\s+(\w+))?(?:\s+version\s+(['"])(.+?)\4)?(?:\s+hash\s+(['"])(.+?)\6)?/);
if (!match) {
throw new Error(`Failed to parse import statement: ${line}`);
}
const [, , path, , alias, , version, , hash] = match;
return {
type: 'import',
path,
alias,
version: version || undefined,
hash: hash || undefined,
};
}
function parseTypeExpr(expr) {
expr = expr.trim();
// Primitive types
const primitives = ['Nat', 'Int', 'Real', 'Bool', 'String', 'Bytes'];
if (primitives.includes(expr)) {
return { type: 'primitive', name: expr };
}
// List<T>
if (expr.startsWith('List<') && expr.endsWith('>')) {
const inner = expr.substring(5, expr.length - 1).trim();
return { type: 'list', elementType: parseTypeExpr(inner) };
}
// Set<T>
if (expr.startsWith('Set<') && expr.endsWith('>')) {
const inner = expr.substring(4, expr.length - 1).trim();
return { type: 'set', elementType: parseTypeExpr(inner) };
}
// Map<K, V>
if (expr.startsWith('Map<') && expr.endsWith('>')) {
const inner = expr.substring(4, expr.length - 1);
// Find the first-level comma (not inside nested generics or record literals)
let depth = 0;
let braceDepth = 0;
let commaIdx = -1;
for (let i = 0; i < inner.length; i++) {
if (inner[i] === '<' || inner[i] === '(')
depth++;
else if (inner[i] === '>' || inner[i] === ')')
depth--;
else if (inner[i] === '{')
braceDepth++;
else if (inner[i] === '}')
braceDepth--;
else if (inner[i] === ',' && depth === 0 && braceDepth === 0) {
commaIdx = i;
break;
}
}
if (commaIdx !== -1) {
const keyStr = inner.substring(0, commaIdx).trim();
const valStr = inner.substring(commaIdx + 1).trim();
return { type: 'map', keyType: parseTypeExpr(keyStr), valueType: parseTypeExpr(valStr) };
}
// Fallback: treat as ident if malformed
return { type: 'ident', name: expr };
}
// List(T) — parenthetical syntax (SpeckDL canonical form)
if (expr.startsWith('List(') && expr.endsWith(')')) {
const inner = expr.substring(5, expr.length - 1).trim();
return { type: 'list', elementType: parseTypeExpr(inner) };
}
// Set(T) — parenthetical syntax (SpeckDL canonical form)
if (expr.startsWith('Set(') && expr.endsWith(')')) {
const inner = expr.substring(4, expr.length - 1).trim();
return { type: 'set', elementType: parseTypeExpr(inner) };
}
// Map(K, V) — parenthetical syntax (SpeckDL canonical form)
if (expr.startsWith('Map(') && expr.endsWith(')')) {
const inner = expr.substring(4, expr.length - 1);
let depth = 0;
let braceDepth = 0;
let commaIdx = -1;
for (let i = 0; i < inner.length; i++) {
if (inner[i] === '(' || inner[i] === '<')
depth++;
else if (inner[i] === ')' || inner[i] === '>')
depth--;
else if (inner[i] === '{')
braceDepth++;
else if (inner[i] === '}')
braceDepth--;
else if (inner[i] === ',' && depth === 0 && braceDepth === 0) {
commaIdx = i;
break;
}
}
if (commaIdx !== -1) {
const keyStr = inner.substring(0, commaIdx).trim();
const valStr = inner.substring(commaIdx + 1).trim();
return { type: 'map', keyType: parseTypeExpr(keyStr), valueType: parseTypeExpr(valStr) };
}
// Fallback: treat as ident if malformed
return { type: 'ident', name: expr };
}
// List type: [T]
if (expr.startsWith('[') && expr.endsWith(']')) {
const elementType = parseTypeExpr(expr.substring(1, expr.length - 1));
return { type: 'list', elementType };
}
// Record type: { ... }
if (expr.startsWith('{') && expr.endsWith('}')) {
const content = expr.substring(1, expr.length - 1).trim();
const fields = [];
if (content) {
// Split by comma and parse each field
const fieldStrs = content.split(',').map(s => s.trim());
for (const fieldStr of fieldStrs) {
const fieldMatch = fieldStr.match(/^(\w+)\s*:\s*(.+)$/);
if (fieldMatch) {
const [, name, typeStr] = fieldMatch;
fields.push({ name, type: parseTypeExpr(typeStr.trim()) });
}
}
}
return { type: 'record', fields };
}
// Identifier (for interface references, etc.)
return { type: 'ident', name: expr };
}
function parseInterface(line) {
// interface Name {
const match = line.match(/^interface\s+(\w+)\s*{/);
if (!match) {
throw new Error(`Failed to parse interface: ${line}`);
}
const name = match[1];
// This is a simplified parser - in a real implementation, we'd need to handle multi-line interfaces
return {
type: 'interface',
name,
methods: [],
};
}
function parseEvent(line) {
// event Name {
const match = line.match(/^event\s+(\w+)\s*{/);
if (!match) {
throw new Error(`Failed to parse event: ${line}`);
}
const name = match[1];
return {
type: 'event',
name,
fields: [],
};
}
function parseProvenanceBlock(lines, line) {
// This is a simplified parser - in a real implementation, we'd parse the full block
return {
type: 'provenance',
clauses: [],
};
}
function parseDerives(line) {
// derives from Name via "rationale"
const match = line.match(/^derives\s+from\s+(\w+(?:-\w+)*)(?:\s+via\s+(['"])(.+?)\2)?/);
if (!match) {
console.warn(`Failed to parse derives statement: ${line}`);
return { type: 'derives', from: 'unknown' };
}
const [, from, , via] = match;
return {
type: 'derives',
from,
via: via || undefined,
};
}
function parseSatisfies(line) {
// satisfies Name [clause "X.Y.Z"]
// e.g., satisfies RESILIENCE-REQ-01 clause "3.1.2"
// e.g., satisfies RESILIENCE-REQ-02
const match = line.match(/^satisfies\s+([\w-]+(?:-[\w]+)*)(?:\s+clause\s+(['"])(.+?)\2)?/);
if (!match) {
console.warn(`Failed to parse satisfies statement: ${line}`);
return { type: 'satisfies', requirement: 'unknown' };
}
const [, requirement, , clause] = match;
return {
type: 'satisfies',
requirement,
clause: clause || undefined,
};
}
function parseAuthor(line) {
// author: "Name" <"email">
// e.g., author: "Scott Scoble" <"scott@scoble.me">
const match = line.match(/^author:\s+(['"])(.+?)\1(?:\s+<(['"])(.+?)\3>)?/);
if (!match) {
// Try without angle brackets or with different format
console.warn(`Failed to parse author statement: ${line}`);
return { type: 'author', name: 'unknown' };
}
const [, , name, , email] = match;
return {
type: 'author',
name,
email: email || undefined,
};
}
function parseSource(line) {
// source: kind ref "identifier"
// e.g., source: architecture_review ref "AR-2024-0215"
const match = line.match(/^source:\s+(\w+)(?:\s+ref\s+(['"])(.+?)\2)?/);
if (!match) {
console.warn(`Failed to parse source statement: ${line}`);
return { type: 'source', kind: 'document' };
}
const [, kind, , ref] = match;
const validKinds = [
'conversation', 'meeting', 'document', 'regulation',
'architecture_review', 'threat_model', 'compliance_audit'
];
if (!validKinds.includes(kind)) {
console.warn(`Invalid source kind: ${kind}, defaulting to document`);
return { type: 'source', kind: 'document', ref: ref || undefined };
}
return {
type: 'source',
kind: kind,
ref: ref || undefined,
};
}
function parseStateBlockMultiline(lines, startIndex, startBraceCount) {
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
// State blocks separate fields with commas or newlines/semicolons.
// Strip trailing commas (they are field separators, not continuations)
// then join with semicolons between complete variable declarations.
const cleanedLines = innerLines.map(l => l.replace(/,+\s*$/, ''));
const inner = cleanedLines.reduce((acc, line, i) => {
if (i === 0)
return line;
const prevLine = cleanedLines[i - 1];
// Check if this line starts a new variable declaration (name: type)
const isNewVar = /^\w+\s*:/.test(line);
// Check if prev line ends with a continuation character (brace or paren, NOT comma)
const prevIsContinuation = /[{(]\s*$/.test(prevLine);
if (isNewVar && !prevIsContinuation) {
return acc + '; ' + line;
}
return acc + ' ' + line;
}, '');
return parseStateBlock(inner);
}
function parseInitBlockMultiline(lines, startIndex, startBraceCount) {
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
// Init blocks separate fields with commas or newlines/semicolons.
// Strip trailing commas and join with semicolons.
const cleanedLines = innerLines.map(l => l.replace(/,+\s*$/, ''));
const inner = cleanedLines.reduce((acc, line, i) => {
if (i === 0)
return line;
const prevLine = cleanedLines[i - 1];
const isNewVar = /^\w+\s*:/.test(line);
const prevIsContinuation = /[{(]\s*$/.test(prevLine);
if (isNewVar && !prevIsContinuation) {
return acc + '; ' + line;
}
return acc + ' ' + line;
}, '');
return parseInitBlock(inner);
}
function parseActionBlockMultiline(lines, startIndex, startBraceCount) {
const firstLine = lines[startIndex].trim();
const header = parseActionHeader(firstLine);
if (!header)
return null;
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
// Keep blank lines as null to separate statements, filter only comments
const bodyLinesRaw = lines.slice(startIndex + 1, endIndex).map(l => {
const trimmed = l.trim();
if (!trimmed || trimmed.startsWith('//') || trimmed.startsWith('/*'))
return null;
return trimmed;
});
// Collapse consecutive nulls and strip trailing nulls
const bodyLines = [];
for (const line of bodyLinesRaw) {
if (line !== null || (bodyLines.length > 0 && bodyLines[bodyLines.length - 1] !== null)) {
bodyLines.push(line);
}
}
// Remove trailing nulls
while (bodyLines.length > 0 && bodyLines[bodyLines.length - 1] === null) {
bodyLines.pop();
}
const statements = [];
for (let i = 0; i < bodyLines.length; i++) {
const stmtOrNull = bodyLines[i];
// Skip blank line separators
if (stmtOrNull === null)
continue;
const stmt = stmtOrNull;
// precondition: expr
if (stmt.startsWith('precondition:')) {
let expr = stmt.substring(13).trim();
// support 'or' continuation lines
while (i + 1 < bodyLines.length) {
const nextLine = bodyLines[i + 1];
if (nextLine === null || !nextLine.startsWith('or '))
break;
i++;
expr += ' || ' + nextLine.substring(3).trim();
}
statements.push({ type: 'precondition', expr });
continue;
}
// postcondition: expr
if (stmt.startsWith('postcondition:')) {
let expr = stmt.substring(14).trim();
// support 'or' continuation lines
while (i + 1 < bodyLines.length) {
const nextLine = bodyLines[i + 1];
if (nextLine === null || !nextLine.startsWith('or '))
break;
i++;
expr += ' || ' + nextLine.substring(3).trim();
}
statements.push({ type: 'postcondition', expr });
continue;
}
// require expr
if (stmt.startsWith('require ')) {
let expr = stmt.substring(8).trim();
// support multi-line continuation (forall, or, etc.)
while (i + 1 < bodyLines.length) {
const nextLine = bodyLines[i + 1];
if (nextLine === null)
break;
// Stop if next line starts a new statement keyword
if (nextLine.startsWith('precondition:') || nextLine.startsWith('postcondition:') ||
nextLine.startsWith('require ') || nextLine.startsWith('return ') ||
nextLine.startsWith('emit ') || nextLine.startsWith('let ') ||
nextLine.includes(':=')) {
break;
}
i++;
expr += ' ' + nextLine;
}
statements.push({ type: 'require', expr });
continue;
}
// return expr
if (stmt.startsWith('return ')) {
statements.push({ type: 'return', expr: stmt.substring(7).trim() });
continue;
}
// emit Event { fields }
const emitMatch = stmt.match(/^emit\s+(\w+)\s*\{\s*(.*)\s*\}$/);
if (emitMatch) {
const eventName = emitMatch[1];
const fieldsStr = emitMatch[2];
const fields = [];
if (fieldsStr) {
const fieldPairs = splitFields(fieldsStr);
for (const fp of fieldPairs) {
const colonIdx = fp.indexOf(':');
if (colonIdx > 0) {
fields.push({
name: fp.substring(0, colonIdx).trim(),
value: fp.substring(colonIdx + 1).trim(),
});
}
}
}
statements.push({ type: 'emit', event: eventName, fields });
continue;
}
// if condition { ... } else if condition { ... } else { ... }
// SpeckDL conditional blocks - parse as a special statement type
if (stmt.startsWith('if ')) {
// Find matching } for this if block (may span multiple bodyLines entries)
let braceDepth = 0;
let j = i;
const blockLines = [];
while (j < bodyLines.length) {
const line = bodyLines[j];
if (line === null) {
j++;
continue;
}
blockLines.push(line);
for (const ch of line) {
if (ch === '{')
braceDepth++;
else if (ch === '}')
braceDepth--;
}
j++;
if (braceDepth === 0)
break;
}
// For now, treat as a raw 'ifblock' statement that the generator can handle
statements.push({ type: 'ifblock', raw: blockLines.join(' ') });
i = j - 1; // skip to end of if block
continue;
}
// let name := expr
const letMatch = stmt.match(/^let\s+(\w+)\s*:=\s*(.+)$/);
if (letMatch) {
statements.push({ type: 'let', name: letMatch[1], expr: letMatch[2].trim() });
continue;
}
// assignment: target := expr (may span multiple lines)
const assignMatch = stmt.match(/^(\w+(?:\[.*?\])?)\s*:=\s*(.+)$/);
if (assignMatch) {
let target = assignMatch[1];
let expr = assignMatch[2].trim();
// Handle multiline expressions: join subsequent lines until braces/parens are balanced
while (i + 1 < bodyLines.length && !isExpressionComplete(expr)) {
i++;
expr += ' ' + bodyLines[i];
}
statements.push({ type: 'assign', target, expr });
}
}
return { ...header, statements };
}
function parseEventBlockMultiline(lines, startIndex, startBraceCount) {
const firstLine = lines[startIndex].trim();
const header = parseEvent(firstLine);
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const fields = [];
for (const line of innerLines) {
const match = line.match(/^(\w+)\s*:\s*(.+?),?$/);
if (match) {
fields.push({ name: match[1], type: parseTypeExpr(match[2].replace(/,$/, '').trim()) });
}
}
return { ...header, fields };
}
function parseInterfaceBlockMultiline(lines, startIndex, startBraceCount) {
const firstLine = lines[startIndex].trim();
const header = parseInterface(firstLine);
const endIndex = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIndex).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const methods = [];
for (const line of innerLines) {
// name-only: enum-style values (e.g., "Idle", "Idle, Parsing" comma-separated)
// Split on comma and take each trimmed token
const tokens = line.split(',').map(s => s.trim()).filter(Boolean);
for (const token of tokens) {
// Check if it’s a name(params) -> returnType method signature
const methodMatch = token.match(/^(\w+)\s*\(([^)]*)\)\s*->\s*(.+?),?$/);
if (methodMatch) {
const name = methodMatch[1];
const paramsStr = methodMatch[2];
const returnTypeStr = methodMatch[3].replace(/,$/, '').trim();
const params = [];
if (paramsStr.trim()) {
const paramPairs = paramsStr.split(',').map(s => s.trim()).filter(Boolean);
for (const p of paramPairs) {
const pMatch = p.match(/^(\w+)\s*:\s*(.+)$/);
if (pMatch) {
params.push({ name: pMatch[1], type: parseTypeExpr(pMatch[2].trim()) });
}
}
}
methods.push({ name, params, returnType: parseTypeExpr(returnTypeStr) });
}
else if (/^\w+$/.test(token)) {
// Name-only (enum-style) — treat as a method with no params and void return
methods.push({ name: token, params: [], returnType: parseTypeExpr('Void') });
}
}
}
return { ...header, methods };
}
// --- Multi-line constraint/verify parsing (no braces needed) ---
/**
* Parse a constraint or verify that may span multiple lines without braces.
* Used for forall-style constraints like:
* constraint Name: forall r in [0..4]:
* (expr)
*
* and verify blocks like:
* verify Always(Name)
* verify Always(Name) { depth N }
*/
function parseMultiLineConstraintVerify(lines, startIndex) {
const line = lines[startIndex].trim();
if (line.startsWith('verify ')) {
return parseVerifyAnyForm(lines, startIndex);
}
if (line.startsWith('constraint ')) {
return parseConstraintAnyForm(lines, startIndex);
}
return null;
}
function parseConstraintAnyForm(lines, startIndex) {
const line = lines[startIndex].trim();
const namedMatch = line.match(/^constraint\s+(\w+):(.*)$/);
if (!namedMatch)
return null;
const name = namedMatch[1];
let expr = namedMatch[2].trim();
// If opens a brace, treat as block
if (expr.startsWith('{')) {
const afterBrace = expr.substring(1).trim();
const openCount = (line.match(/{/g) || []).length;
const endIdx = findBlockEnd(lines, startIndex + 1, openCount);
const innerLines = lines.slice(startIndex + 1, endIdx).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const inner = innerLines.join(' ');
expr = (afterBrace + ' ' + inner).trim();
}
else {
// No braces — but might span multiple lines (forall continuation)
const continuationLines = [];
for (let j = startIndex + 1; j < lines.length; j++) {
const nl = lines[j].trim();
if (!nl || nl.startsWith('//') || nl.startsWith('/*') ||
nl.startsWith('constraint ') || nl.startsWith('verify ') ||
nl.startsWith('constraint:') || nl.startsWith('verify:') ||
nl.startsWith('state') || nl.startsWith('init') ||
nl.startsWith('action ') || nl.startsWith('event ') ||
nl.startsWith('interface ') || nl.startsWith('provenance ') ||
nl.startsWith('bom ') || nl.startsWith('}') ||
nl.startsWith('next:') || nl.startsWith('invariant ')) {
break;
}
continuationLines.push(nl);
}
if (continuationLines.length > 0) {
expr = expr + ' ' + continuationLines.join(' ');
}
}
return { type: 'constraint', name, expr: expr.trim() };
}
function parseVerifyAnyForm(lines, startIndex) {
const line = lines[startIndex].trim();
// Single-line: verify Always(Name) { depth N }
const fullMatch = line.match(/^verify\s+((?:Always|always|Eventually|eventually)\s*\(\s*(\w+)\s*\))\s*\{\s*depth\s+(\d+)\s*\}/);
if (fullMatch) {
return {
type: 'verify',
name: fullMatch[2],
temporalExpr: fullMatch[1].trim(),
depth: parseInt(fullMatch[3], 10),
};
}
// Multi-line: verify Always(Name) { ... }
if (line.includes('{')) {
const headerMatch = line.match(/^verify\s+((?:Always|always|Eventually|eventually)\s*\(\s*(\w+)\s*\))\s*\{/);
if (headerMatch) {
const temporalExpr = headerMatch[1].trim();
const name = headerMatch[2];
const openCount = (line.match(/{/g) || []).length;
const endIdx = findBlockEnd(lines, startIndex + 1, openCount);
const innerLines = lines.slice(startIndex + 1, endIdx).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const inner = innerLines.join(' ');
const afterBrace = line.substring(line.indexOf('{') + 1).trim();
const combined = (afterBrace + ' ' + inner).trim();
const depthMatch = combined.match(/\bdepth\s+(\d+)\b/);
const depth = depthMatch ? parseInt(depthMatch[1], 10) : undefined;
return { type: 'verify', name, temporalExpr, depth };
}
}
// Simple: verify Always(Name)
const simpleMatch = line.match(/^verify\s+((?:Always|always|Eventually|eventually)\s*\(\s*(\w+)\s*\))\s*$/);
if (simpleMatch) {
return {
type: 'verify',
name: simpleMatch[2],
temporalExpr: simpleMatch[1].trim(),
};
}
return null;
}
// --- Verify/Constraint block parsing ---
/**
* Parse a verify block opened with `verify Always(Name) { ... }` or similar.
* The first line already contains the header; we need to parse the body inside { }.
*/
function parseVerifyBlockMultiline(lines, startIndex, startBraceCount) {
const firstLine = lines[startIndex].trim();
// Match: verify Always(Name) { depth N } or verify Always(Name) {
const headerMatch = firstLine.match(/^verify\s+((?:Always|always|Eventually|eventually)\s*\(\s*(\w+)\s*\))\s*\{/);
if (!headerMatch)
return null;
const temporalExpr = headerMatch[1].trim();
const name = headerMatch[2];
// Check if the brace closes on the same line (single-line form)
const openBraceCount = (firstLine.match(/{/g) || []).length;
const closeBraceCount = (firstLine.match(/}/g) || []).length;
if (closeBraceCount >= openBraceCount) {
// Single-line: parse depth from same line
const afterBrace = firstLine.substring(firstLine.indexOf('{') + 1);
const beforeClose = afterBrace.substring(0, afterBrace.lastIndexOf('}')).trim();
const depthMatch = beforeClose.match(/\bdepth\s+(\d+)\b/);
const depth = depthMatch ? parseInt(depthMatch[1], 10) : undefined;
return { type: 'verify', name, temporalExpr, depth };
}
// Multi-line block
let depth;
const endIdx = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIdx).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const inner = innerLines.join(' ');
const afterBrace = firstLine.substring(firstLine.indexOf('{') + 1).trim();
const depthMatch = (afterBrace + ' ' + inner).match(/\bdepth\s+(\d+)\b/);
if (depthMatch) {
depth = parseInt(depthMatch[1], 10);
}
return { type: 'verify', name, temporalExpr, depth };
}
/**
* Parse a single-line verify statement: verify Always(Name) { depth N }
*/
function parseVerifySingleLine(line) {
// verify Always(Name) { depth N }
const fullMatch = line.match(/^verify\s+((?:Always|always|Eventually|eventually)\s*\(\s*(\w+)\s*\))\s*\{\s*depth\s+(\d+)\s*\}/);
if (fullMatch) {
return {
type: 'verify',
name: fullMatch[2],
temporalExpr: fullMatch[1].trim(),
depth: parseInt(fullMatch[3], 10),
};
}
// verify Always(Name) (no depth, no braces — just a statement)
const simpleMatch = line.match(/^verify\s+((?:Always|always|Eventually|eventually)\s*\(\s*(\w+)\s*\))\s*$/);
if (simpleMatch) {
return {
type: 'verify',
name: simpleMatch[2],
temporalExpr: simpleMatch[1].trim(),
};
}
return null;
}
/**
* Parse a constraint block opened with `constraint Name: ...` which may
* be multi-line (e.g. forall spanning multiple lines).
*/
function parseConstraintBlockMultiline(lines, startIndex, startBraceCount) {
const firstLine = lines[startIndex].trim();
// Match: constraint Name: expr (possibly opening a {} block, or just a forall on next line)
// For the SQLiteWAL style: constraint Name: expr (single line, no braces needed)
const namedMatch = firstLine.match(/^constraint\s+(\w+):(.*)$/);
if (namedMatch) {
const name = namedMatch[1];
let expr = namedMatch[2].trim();
// If the expression opens a brace, collect the block
if (expr.startsWith('{')) {
const endIdx = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIdx).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
const inner = innerLines.join(' ');
// Combine: content after { on first line + content from inner lines
const afterBrace = expr.substring(1).trim();
expr = (afterBrace + ' ' + inner).trim();
}
else {
// No braces, but might still be multiline (forall spanning multiple lines)
// Check if next line(s) continue the expression
const endIdx = findBlockEnd(lines, startIndex + 1, startBraceCount);
const innerLines = lines.slice(startIndex + 1, endIdx).map(l => l.trim()).filter(l => l && !l.startsWith('//') && !l.startsWith('/*'));
if (innerLines.length > 0) {
expr = expr + ' ' + innerLines.join(' ');
}
}
return { type: 'constraint', name, expr: expr.trim() };
}
return null;
}
/** Split on commas while respecting parenthesized groups and quoted strings */
function splitFields(s) {
const result = [];
let depth = 0;
let inDouble = false;
let inSingle = false;
let start = 0;
for (let i = 0; i < s.length; i++) {
const ch = s[i];
if (ch === '"' && !inSingle) {
inDouble = !inDouble;
continue;
}
if (ch === "'" && !inDouble) {
inSingle = !inSingle;
continue;
}
if (inDouble || inSingle)
continue;
if (ch === '(' || ch === '{') {
depth++;
continue;
}
if (ch === ')' || ch === '}') {
depth--;
continue;
}
if (ch === ',' && depth === 0) {
result.push(s.substring(start, i).trim());
start = i + 1;
}
}
const last = s.substring(start).trim();
if (last)
result.push(last);
return result;
}
//# sourceMappingURL=parser.js.map