Preserve statement order, fix notIn with object literals, Paxos now 0 errors
- Replaced grouped statement emission with per-statement switch preserving order
- Moved notIn rewrite BEFORE object literal restoration to protect { } blocks
- Fixed if/else ternary expression regex for complex cases
- Paxos: 6 errors → 0 errors
- Total: 168 → 124 errors across 7 specs
This commit is contained in:
Scott Scoble
parent
71de0c1d35
commit
a1efbadbd1
1 changed files with 72 additions and 87 deletions
|
|
@ -310,87 +310,66 @@ function emitAction(action: ActionNode, stateVarNames: Set<string>, 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<string>, mapVarNames: Set<
|
|||
return `__OBJ_LIT_${objectLiterals.length - 1}__`;
|
||||
});
|
||||
|
||||
// Step 3a: notIn rewrite BEFORE this-prefixing so we can match bare identifiers
|
||||
// notIn -> !<map>.has(<key>) (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<string>, mapVarNames: Set<
|
|||
|
||||
// Step 5: Translate SpeckDL expression patterns to JavaScript
|
||||
|
||||
// 5a: notIn -> !<map>.has(<key>) (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 <map>.keys -> <map>.has(x) (e.g. "t.from in accounts.keys" -> "accounts.has(t.from)")
|
||||
// 5a: x in <map>.keys -> <map>.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 <set> -> <set>.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<string>, 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 <cond>: <then> else <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();
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue