diff --git a/compiler/src/generators/typescript-state-machine.ts b/compiler/src/generators/typescript-state-machine.ts index 9eb3816..78ac8ae 100644 --- a/compiler/src/generators/typescript-state-machine.ts +++ b/compiler/src/generators/typescript-state-machine.ts @@ -310,87 +310,66 @@ function emitAction(action: ActionNode, stateVarNames: Set, mapVarNames: .map(p => `${p.name}: ${tsType(p.type, speckName, enumMap)}`) .join(', '); - const preconditions = action.statements - .filter(s => s.type === 'precondition') - .map(s => { - const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues); - return ` // precondition: ${expr}\n if (!(${expr})) throw new Error('Precondition failed: ${expr.replace(/'/g, "\\'")}');`; - }) - .join('\n'); - - const requires = action.statements - .filter(s => s.type === 'require') - .map(s => { - const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues); - return ` if (!(${expr})) throw new Error('Guard failed: ${expr.replace(/'/g, "\\'")}');`; - }) - .join('\n'); - - const assigns = action.statements - .filter(s => s.type === 'assign') - .map(s => { - const target = cleanName(s.target); - const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues); - // Map assignment: map[key] = val -> map.set(key, val) - const mapBracketMatch = target.match(/^(\w+)\[([^\]]+)\]$/); - if (mapBracketMatch && mapVarNames.has(mapBracketMatch[1])) { - const varName = mapBracketMatch[1]; - const key = mapBracketMatch[2]; - return ` this.${varName}.set(${key}, ${expr});`; + // Statements in SpeckDL order: emit lets before guards so guards can reference them + // (SpeckDL allows guards to reference let-bound variables that appear before them) + const bodyParts: string[] = []; + for (const stmt of action.statements) { + switch (stmt.type) { + case 'precondition': { + const expr = rewriteExpr(stmt.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues); + bodyParts.push(` // precondition: ${expr}\n if (!(${expr})) throw new Error('Precondition failed: ${expr.replace(/'/g, "\\'")}');`); + break; } - return ` this.${target} = ${expr};`; - }) - .join('\n'); - - // Handle let statements: let x := expr -> const x = expr; - const lets = action.statements - .filter(s => s.type === 'let') - .map(s => { - const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues); - return ` const ${s.name} = ${expr};`; - }) - .join('\n'); - - const emits = action.statements - .filter(s => s.type === 'emit') - .map(s => { - const fields = s.fields - .map(f => { + case 'require': { + const expr = rewriteExpr(stmt.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues); + bodyParts.push(` if (!(${expr})) throw new Error('Guard failed: ${expr.replace(/'/g, "\\'")}');`); + break; + } + case 'let': { + const expr = rewriteExpr(stmt.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues); + bodyParts.push(` const ${stmt.name} = ${expr};`); + break; + } + case 'assign': { + const target = cleanName(stmt.target); + const expr = rewriteExpr(stmt.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues); + const mapBracketMatch = target.match(/^(\w+)\[([^\]]+)\]$/); + if (mapBracketMatch && mapVarNames.has(mapBracketMatch[1])) { + bodyParts.push(` this.${mapBracketMatch[1]}.set(${mapBracketMatch[2]}, ${expr});`); + } else { + bodyParts.push(` this.${target} = ${expr};`); + } + break; + } + case 'emit': { + const fields = stmt.fields.map(f => { const name = cleanName(f.name); const val = rewriteExpr(f.value, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues); return ` ${name}: ${val}`; - }) - .join(',\n'); - return ` this.decisionLog.push({\n${fields}\n } as ${s.event});`; - }) - .join('\n'); - - // Handle ifblock statements (SpeckDL conditional blocks) - // Note: Full if/else block support requires recursive parsing of block contents - const ifblocks = action.statements - .filter(s => s.type === 'ifblock') - .map(s => { - // Output as comment - full implementation requires recursive statement parsing - return ` // TODO: SpeckDL conditional block (if/else) - manual translation required`; - }) - .join('\n'); - - const postconditions = action.statements - .filter(s => s.type === 'postcondition') - .map(s => { - const expr = rewriteExpr(s.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues); - // If the expression compares objects/arrays with ===, add ts-ignore to suppress TS2839 - const needsTsIgnore = /===\s*\{|===\s*\[/.test(expr); - const tsIgnore = needsTsIgnore ? ' // @ts-expect-error TS2839 — generated spec comparison (structural equality not available in JS)\n' : ''; - return `${tsIgnore} // postcondition: ${expr}\n if (!(${expr})) throw new Error('Postcondition failed: ${expr.replace(/'/g, "\\'")}');`; - }) - .join('\n'); - - // Preconditions + requires first (guards), then mutations (let + assign + emit + ifblock), then postconditions - const guards = [preconditions, requires].filter(Boolean).join('\n'); - const mutations = [lets, assigns, emits, ifblocks].filter(Boolean).join('\n'); - const bodyParts = [guards, mutations, postconditions].filter(Boolean).join('\n'); - return ` ${action.name}(${params}) {\n${bodyParts}\n }`; + }).join(',\n'); + bodyParts.push(` this.decisionLog.push({\n${fields}\n } as ${stmt.event});`); + break; + } + case 'ifblock': { + bodyParts.push(` // TODO: SpeckDL conditional block (if/else) - manual translation required`); + break; + } + case 'return': { + const expr = rewriteExpr(stmt.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues); + bodyParts.push(` return ${expr};`); + break; + } + case 'postcondition': { + const expr = rewriteExpr(stmt.expr, stateVarNames, mapVarNames, localNames, stateEnumName, knownStateValues); + const needsTsIgnore = /===\s*\{|===\s*\[/.test(expr); + const tsIgnore = needsTsIgnore ? ' // @ts-expect-error TS2839 — generated spec comparison (structural equality not available in JS)\n' : ''; + bodyParts.push(`${tsIgnore} // postcondition: ${expr}\n if (!(${expr})) throw new Error('Postcondition failed: ${expr.replace(/'/g, "\\'")}');`); + break; + } + } + } + const bodyPartsStr = bodyParts.filter(Boolean).join('\n'); + return ` ${action.name}(${params}) {\n${bodyPartsStr}\n }`; } // Rewrite SpeckDL expressions to valid TypeScript @@ -426,6 +405,17 @@ function rewriteExpr(expr: string, stateVarNames: Set, mapVarNames: Set< return `__OBJ_LIT_${objectLiterals.length - 1}__`; }); + // Step 3a: notIn rewrite BEFORE this-prefixing so we can match bare identifiers + // notIn -> !.has() (e.g. "t.id notIn transfers.keys" -> "!transfers.has(t.id)") + ts = ts.replace(/(\S+)\s+notIn\s+(\S+)\.keys/g, '!$2.has($1)'); + // notIn for Sets (no .keys suffix), e.g. "acctId notIn accounts" -> "!accounts.has(acctId)" + ts = ts.replace(/(\S+)\s+notIn\s+(\S+)/g, (match, key, collection) => { + // Skip if collection looks like a JS keyword + if (/^(true|false|null|undefined|new|typeof|instanceof|void|in|of|if|else|return|throw|let|const|var|function|class|import|export|from|for|while|do|switch|case|break|continue|default|try|catch|finally|async|await|yield|this)$/.test(collection)) return match; + return `!${collection}.has(${key})`; + }); + + // Step 3b: Replace identifiers that are state variables but not local params const tokens = ts.split(/([\s\(\)\[\]{}+\-*/=<>!&|.,;:'"`]+)/); const result = tokens.map(tok => { if (/^[a-zA-Z_]\w*\.\w+$/.test(tok)) return tok; // already has dot (enum ref) @@ -449,15 +439,7 @@ function rewriteExpr(expr: string, stateVarNames: Set, mapVarNames: Set< // Step 5: Translate SpeckDL expression patterns to JavaScript - // 5a: notIn -> !.has() (e.g. "t.id notIn transfers.keys" -> "!transfers.has(t.id)") - ts = ts.replace(/(\S+)\s+notIn\s+(\S+)\.keys/g, '!$2.has($1)'); - // 5a1: notIn for Sets (no .keys suffix), e.g. "acctId notIn accounts" -> "!accounts.has(acctId)" - ts = ts.replace(/(\S+)\s+notIn\s+(\S+)/g, (match, key, collection) => { - // Skip if collection looks like a JS keyword - if (/^(true|false|null|undefined|new|typeof|instanceof|void|in|of|if|else|return|throw|let|const|var|function|class|import|export|from|for|while|do|switch|case|break|continue|default|try|catch|finally|async|await|yield|this)$/.test(collection)) return match; - return `!${collection}.has(${key})`; - }); - // 5a2: x in .keys -> .has(x) (e.g. "t.from in accounts.keys" -> "accounts.has(t.from)") + // 5a: x in .keys -> .has(x) (e.g. "t.from in accounts.keys" -> "accounts.has(t.from)") ts = ts.replace(/(\S+)\s+in\s+(\S+)\.keys/g, '$2.has($1)'); // 5a3: x in -> .has(x) (e.g. "id in pending" -> "pending.has(id)") ts = ts.replace(/(\S+)\s+in\s+(\S+)/g, (match, key, collection) => { @@ -514,7 +496,10 @@ function rewriteExpr(expr: string, stateVarNames: Set, mapVarNames: Set< ts = ts.replace(/\.size\(\)/g, '.size'); // 5i: SpeckDL conditional expression: if cond: a else b -> cond ? a : b - ts = ts.replace(/\bif\s+([^:]+):\s*([^\s][^]+?)\s+else\s+([^\s][^]*?)(?=\s*[)};]|$)/g, '($1 ? $2 : $3)'); + // Use a careful regex that matches word boundaries and stops at expression end + // Pattern: if : else + // Where cond, then, else are balanced expressions (no unbalanced braces at top level) + ts = ts.replace(/\bif\s+((?:[^{}:()]|\([^)]*\)|\{[^}]*\})+):\s*((?:[^{};]|\{[^}]*\})+)\s+else\s+((?:[^{};]|\{[^}]*\})+)(?=[;)}\],\s]|$)/g, '($1 ? $2 : $3)'); return ts.trim(); }