e6f95ddf0b
Multi-line `input: { ... }` and `output: { ... }` blocks fell through
to parseMember which returned `{ type: 'ident', name: '{' }` instead of
a record with fields. Broke RetryHandler.speck and similar real specks.
Fix: add `input:`/`output:` to blockStarters, dispatch to new
parseInputOutputBlock() that brace-counts across newlines, strips
line comments, and delegates to parseTypeExpr's record branch.
CoS-verified-live-close (cycle 126 pattern): subagent hit max_iterations
on the brace-count edge case. CoS applied focused fix + 2 new tests.
39/39 vitest pass.
Test evidence:
- RetryHandler.speck: input typeExpr.type='record' 4 fields
- 37 prior tests + 2 new = 39 passing
1521 lines
49 KiB
TypeScript
1521 lines
49 KiB
TypeScript
import fs from 'fs';
|
||
import path from 'path';
|
||
|
||
// AST node types for SpeckDL
|
||
export interface SpeckNode {
|
||
type: 'speck';
|
||
name: string;
|
||
members: MemberNode[];
|
||
}
|
||
|
||
export interface ImportNode {
|
||
type: 'import';
|
||
path: string;
|
||
alias?: string;
|
||
version?: string;
|
||
hash?: string;
|
||
}
|
||
|
||
export interface InputNode {
|
||
type: 'input';
|
||
typeExpr: TypeExpr;
|
||
}
|
||
|
||
export interface OutputNode {
|
||
type: 'output';
|
||
typeExpr: TypeExpr;
|
||
}
|
||
|
||
export interface ConstraintNode {
|
||
type: 'constraint';
|
||
name?: string;
|
||
expr: string;
|
||
}
|
||
|
||
export interface VerifyNode {
|
||
type: 'verify';
|
||
name: string;
|
||
temporalExpr: string;
|
||
depth?: number;
|
||
}
|
||
|
||
export interface InterfaceNode {
|
||
type: 'interface';
|
||
name: string;
|
||
methods: MethodSignature[];
|
||
}
|
||
|
||
export interface MethodSignature {
|
||
name: string;
|
||
params: { name: string; type: TypeExpr }[];
|
||
returnType: TypeExpr;
|
||
}
|
||
|
||
export interface EventNode {
|
||
type: 'event';
|
||
name: string;
|
||
fields: { name: string; type: TypeExpr }[];
|
||
}
|
||
|
||
export interface ProvenanceNode {
|
||
type: 'provenance';
|
||
clauses: ProvenanceClause[];
|
||
}
|
||
|
||
export interface ProvenanceClause {
|
||
type: 'regulation' | 'design_decision' | 'parent_spec' | 'external_doc';
|
||
value: string;
|
||
location?: string; // for external_doc
|
||
}
|
||
|
||
export interface ReviewNode {
|
||
type: 'review';
|
||
kind: 'manual' | 'auto' | 'hybrid';
|
||
}
|
||
|
||
export interface DerivesNode {
|
||
type: 'derives';
|
||
from: string;
|
||
via?: string;
|
||
}
|
||
|
||
export interface SatisfiesNode {
|
||
type: 'satisfies';
|
||
requirement: string;
|
||
clause?: string;
|
||
}
|
||
|
||
export interface AuthorNode {
|
||
type: 'author';
|
||
name: string;
|
||
email?: string;
|
||
}
|
||
|
||
export interface SourceNode {
|
||
type: 'source';
|
||
kind: 'conversation' | 'meeting' | 'document' | 'regulation' |
|
||
'architecture_review' | 'threat_model' | 'compliance_audit';
|
||
ref?: string;
|
||
}
|
||
|
||
export interface BOMNode {
|
||
type: 'bom';
|
||
compiler?: { name: string; version?: string };
|
||
solver?: { name: string; version?: string };
|
||
runtime?: { name: string; version?: string };
|
||
license?: string;
|
||
hash?: string;
|
||
}
|
||
|
||
// State machine extension (v0.3)
|
||
export interface StateNode {
|
||
type: 'state';
|
||
variables: StateVar[];
|
||
}
|
||
|
||
export interface StateVar {
|
||
name: string;
|
||
typeExpr: TypeExpr;
|
||
defaultInit?: string; // default initializer expression as raw string
|
||
}
|
||
|
||
export interface InitNode {
|
||
type: 'init';
|
||
assignments: { name: string; expr: string }[];
|
||
}
|
||
|
||
export interface ActionNode {
|
||
type: 'action';
|
||
name: string;
|
||
params: { name: string; type: TypeExpr }[];
|
||
statements: ActionStatement[];
|
||
}
|
||
|
||
export type ActionStatement =
|
||
| { type: 'assign'; target: string; expr: string }
|
||
| { type: 'let'; name: string; expr: string }
|
||
| { type: 'require'; expr: string }
|
||
| { type: 'precondition'; expr: string }
|
||
| { type: 'postcondition'; expr: string }
|
||
| { type: 'emit'; event: string; fields: { name: string; value: string }[] }
|
||
| { type: 'return'; expr: string }
|
||
| { type: 'ifblock'; raw: string };
|
||
|
||
export type MemberNode =
|
||
| ImportNode
|
||
| InputNode
|
||
| OutputNode
|
||
| ConstraintNode
|
||
| VerifyNode
|
||
| InterfaceNode
|
||
| EventNode
|
||
| ProvenanceNode
|
||
| ReviewNode
|
||
| DerivesNode
|
||
| SatisfiesNode
|
||
| AuthorNode
|
||
| SourceNode
|
||
| BOMNode
|
||
| StateNode
|
||
| InitNode
|
||
| ActionNode;
|
||
|
||
export interface TypeExpr {
|
||
type: 'primitive' | 'record' | 'list' | 'set' | 'map' | 'ident';
|
||
name?: string;
|
||
fields?: { name: string; type: TypeExpr }[];
|
||
elementType?: TypeExpr;
|
||
keyType?: TypeExpr; // for Map<K, V>
|
||
valueType?: TypeExpr; // for Map<K, V>
|
||
}
|
||
|
||
export interface AST {
|
||
specks: SpeckNode[];
|
||
}
|
||
|
||
/**
|
||
* Parse a .speck file and return the AST
|
||
*/
|
||
export function parseSpeckFile(filePath: string): AST {
|
||
const content = fs.readFileSync(filePath, 'utf-8');
|
||
return parseSpeckContent(content, filePath);
|
||
}
|
||
|
||
/**
|
||
* Parse SpeckDL content and return the AST
|
||
*/
|
||
export function parseSpeckContent(content: string, filePath?: string): AST {
|
||
const specks: SpeckNode[] = [];
|
||
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: string[], startIndex: number): SpeckNode | null {
|
||
const headerMatch = lines[startIndex].match(/^speck\s+([\w-]+)\s*{/);
|
||
if (!headerMatch) return null;
|
||
|
||
const name = headerMatch[1];
|
||
const members: MemberNode[] = [];
|
||
|
||
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 ', 'input:', 'output:'];
|
||
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]:, verify: always(implies(\n ...\n)))
|
||
if (line.startsWith('constraint ') || line.startsWith('verify ') || 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: string[], startIndex: number, startBraceCount: number): number {
|
||
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: string): boolean {
|
||
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: string[], startIndex: number): MemberNode | null {
|
||
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);
|
||
}
|
||
if (firstLine.startsWith('input:') || firstLine.startsWith('output:')) {
|
||
return parseInputOutputBlock(lines, startIndex, startBraceCount);
|
||
}
|
||
|
||
return null;
|
||
}
|
||
|
||
/**
|
||
* Parse a multi-line `input: { ... }` or `output: { ... }` block.
|
||
*
|
||
* The first line opens with `input: {` or `output: {` and the matching `}`
|
||
* may be many lines later (with field declarations on intermediate lines).
|
||
* We collect all lines up to the matching `}` (brace-counted) and join the
|
||
* inner content into a single record string that `parseTypeExpr` already
|
||
* knows how to handle.
|
||
*/
|
||
function parseInputOutputBlock(
|
||
lines: string[],
|
||
startIndex: number,
|
||
startBraceCount: number,
|
||
): MemberNode | null {
|
||
const header = lines[startIndex].trim();
|
||
const isInput = header.startsWith('input:');
|
||
const kind: 'input' | 'output' = isInput ? 'input' : 'output';
|
||
|
||
// Collect inner content lines, brace-counting across the block.
|
||
// startBraceCount is the brace count on the header line (1 for `input: {`).
|
||
// We need to find the line where braceCount returns to 0 (i.e. the closing `}`).
|
||
const innerLines: string[] = [];
|
||
let braceCount = 0;
|
||
let i = startIndex;
|
||
// First pass: extract inner content from header line (everything after the first `{`).
|
||
const headerLine = lines[startIndex].trim();
|
||
const headerNoComment = headerLine.replace(/\/\/.*$/, '').trim();
|
||
const openIdx = headerNoComment.indexOf('{');
|
||
if (openIdx >= 0) {
|
||
const after = headerNoComment.substring(openIdx + 1).trim();
|
||
if (after) innerLines.push(after);
|
||
}
|
||
braceCount = 1; // we're inside one `{` from the header
|
||
i = startIndex + 1;
|
||
while (i < lines.length && braceCount > 0) {
|
||
const raw = lines[i];
|
||
const stripped = raw.trim();
|
||
// Strip line comments (//...) — they cannot be inside a type expression.
|
||
const noComment = stripped.replace(/\/\/.*$/, '').trim();
|
||
for (const ch of noComment) {
|
||
if (ch === '{') braceCount++;
|
||
else if (ch === '}') braceCount--;
|
||
}
|
||
if (braceCount > 0 && noComment) {
|
||
// Inside the block — keep content (skip the closing `}` line itself).
|
||
innerLines.push(noComment);
|
||
}
|
||
i++;
|
||
}
|
||
|
||
// Join inner content with newlines; `parseTypeExpr`'s record branch
|
||
// splits on commas and matches `name: type` pairs.
|
||
const recordExpr = '{ ' + innerLines.join(' ') + ' }';
|
||
const typeExpr = parseTypeExpr(recordExpr);
|
||
return { type: kind, typeExpr };
|
||
}
|
||
|
||
function parseMember(line: string): MemberNode | null {
|
||
// 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() as 'manual' | 'auto' | 'hybrid';
|
||
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: string): StateNode {
|
||
const variables: StateVar[] = [];
|
||
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: string): InitNode {
|
||
const assignments: { name: string; expr: string }[] = [];
|
||
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: string): ActionNode | null {
|
||
const match = line.match(/^action\s+(\w+)\s*(?:\(([^)]*)\))?\s*\{/);
|
||
if (!match) return null;
|
||
|
||
const name = match[1];
|
||
const paramsStr = match[2] || '';
|
||
const params: { name: string; type: TypeExpr }[] = [];
|
||
|
||
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: string): ImportNode {
|
||
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: string): TypeExpr {
|
||
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: { name: string; type: TypeExpr }[] = [];
|
||
|
||
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: string): InterfaceNode {
|
||
// 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: string): EventNode {
|
||
// 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: string[], line: string): ProvenanceNode {
|
||
// This is a simplified parser - in a real implementation, we'd parse the full block
|
||
return {
|
||
type: 'provenance',
|
||
clauses: [],
|
||
};
|
||
}
|
||
|
||
function parseDerives(line: string): DerivesNode {
|
||
// 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: string): SatisfiesNode {
|
||
// 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: string): AuthorNode {
|
||
// 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: string): SourceNode {
|
||
// 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 as any,
|
||
ref: ref || undefined,
|
||
};
|
||
}
|
||
|
||
function parseStateBlockMultiline(lines: string[], startIndex: number, startBraceCount: number): StateNode {
|
||
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: string[], startIndex: number, startBraceCount: number): InitNode {
|
||
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: string[], startIndex: number, startBraceCount: number): ActionNode | null {
|
||
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: (string | null)[] = [];
|
||
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: ActionStatement[] = [];
|
||
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: { name: string; value: string }[] = [];
|
||
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: string[] = [];
|
||
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: string[], startIndex: number, startBraceCount: number): EventNode {
|
||
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: { name: string; type: TypeExpr }[] = [];
|
||
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: string[], startIndex: number, startBraceCount: number): InterfaceNode {
|
||
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: MethodSignature[] = [];
|
||
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: { name: string; type: TypeExpr }[] = [];
|
||
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: string[], startIndex: number): MemberNode | null {
|
||
const line = lines[startIndex].trim();
|
||
|
||
if (line.startsWith('verify ')) {
|
||
return parseVerifyAnyForm(lines, startIndex);
|
||
}
|
||
|
||
// Multi-line `verify:` form: verify: always(implies(\n ...\n))
|
||
// The body opens parens that span multiple lines; collect continuation
|
||
// lines until parens balance to zero, then return the joined string as
|
||
// the temporalExpr. speckl#54.
|
||
if (line.startsWith('verify:')) {
|
||
return parseVerifyColonBlock(lines, startIndex);
|
||
}
|
||
|
||
if (line.startsWith('constraint ')) {
|
||
return parseConstraintAnyForm(lines, startIndex);
|
||
}
|
||
|
||
return null;
|
||
}
|
||
|
||
/**
|
||
* Parse the `verify: <expr>` form (speckl#54) where the body can span
|
||
* multiple lines:
|
||
*
|
||
* verify: always(implies(
|
||
* cond1,
|
||
* cond2
|
||
* ))
|
||
*
|
||
* The whole expression (the part after `verify:`) is collected by
|
||
* appending subsequent non-empty, non-keyword-starting lines until
|
||
* parens/brackets/braces balance to zero. The joined string is stored
|
||
* in `temporalExpr` so the downstream LTL translator (typescript-state-machine
|
||
* verifyN()) sees a well-formed formula.
|
||
*
|
||
* The `name` is derived from the LTL operator's argument when it matches
|
||
* `always(Name)` / `eventually(Name)`. When the body is a richer expression
|
||
* (e.g. `always(implies(...))`) we fall back to `unnamed` — the generator
|
||
* still emits a working verifyN() that uses the full expression.
|
||
*/
|
||
function parseVerifyColonBlock(lines: string[], startIndex: number): VerifyNode | null {
|
||
const firstLine = lines[startIndex].trim();
|
||
// Strip the `verify:` prefix.
|
||
const head = firstLine.substring(firstLine.indexOf(':') + 1).trim();
|
||
if (!head) return null;
|
||
|
||
// If the head is already balanced on its own (single-line verify: expr),
|
||
// just return it directly — no continuation needed.
|
||
if (isExpressionComplete(head)) {
|
||
const nameMatch = head.match(/^(?:always|Always|eventually|Eventually)\s*\(\s*(\w+)\s*\)$/);
|
||
return {
|
||
type: 'verify',
|
||
name: nameMatch ? nameMatch[1] : 'unnamed',
|
||
temporalExpr: head,
|
||
};
|
||
}
|
||
|
||
// Multi-line: collect continuation lines until parens balance. The same
|
||
// break-condition list used in the parseSpeck skip-loop applies (don't
|
||
// swallow the next member's keyword). We additionally stop at any
|
||
// standalone `}` so a verify inside a brace-block still terminates.
|
||
const parts: string[] = [head];
|
||
let parens = 0, brackets = 0, braces = 0;
|
||
for (const ch of head) {
|
||
if (ch === '(') parens++;
|
||
else if (ch === ')') parens--;
|
||
else if (ch === '[') brackets++;
|
||
else if (ch === ']') brackets--;
|
||
else if (ch === '{') braces++;
|
||
else if (ch === '}') braces--;
|
||
}
|
||
|
||
let lastConsumed = startIndex;
|
||
for (let j = startIndex + 1; j < lines.length; j++) {
|
||
const raw = lines[j];
|
||
const nl = raw.trim();
|
||
if (!nl) {
|
||
// Empty line still updates counters (none) and advances lastConsumed
|
||
lastConsumed = j;
|
||
continue;
|
||
}
|
||
if (nl.startsWith('//') || nl.startsWith('/*')) {
|
||
// Skip standalone comments but treat them as part of the block
|
||
// (the LTL translator doesn't care about comments in temporalExpr).
|
||
lastConsumed = j;
|
||
continue;
|
||
}
|
||
// Stop at a new top-level member keyword — that's the next member.
|
||
if (
|
||
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 === '}' ||
|
||
nl.startsWith('next:') || nl.startsWith('invariant ')
|
||
) {
|
||
break;
|
||
}
|
||
// Update depth counters.
|
||
for (const ch of raw) {
|
||
if (ch === '(') parens++;
|
||
else if (ch === ')') parens--;
|
||
else if (ch === '[') brackets++;
|
||
else if (ch === ']') brackets--;
|
||
else if (ch === '{') braces++;
|
||
else if (ch === '}') braces--;
|
||
}
|
||
parts.push(nl);
|
||
lastConsumed = j;
|
||
if (parens === 0 && brackets === 0 && braces === 0) {
|
||
break;
|
||
}
|
||
}
|
||
|
||
const joined = parts.join(' ').replace(/\s+/g, ' ').trim();
|
||
const nameMatch = joined.match(/^(?:always|Always|eventually|Eventually)\s*\(\s*(\w+)\s*\)$/);
|
||
return {
|
||
type: 'verify',
|
||
name: nameMatch ? nameMatch[1] : 'unnamed',
|
||
temporalExpr: joined,
|
||
};
|
||
}
|
||
|
||
function parseConstraintAnyForm(lines: string[], startIndex: number): ConstraintNode | null {
|
||
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: string[] = [];
|
||
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: string[], startIndex: number): VerifyNode | null {
|
||
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: string[], startIndex: number, startBraceCount: number): VerifyNode | null {
|
||
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: number | undefined;
|
||
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: string): VerifyNode | null {
|
||
// 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: string[], startIndex: number, startBraceCount: number): ConstraintNode | null {
|
||
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: string): string[] {
|
||
const result: string[] = [];
|
||
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;
|
||
}
|