From 675ef98ef99ee95847d21e45ce2aa61410098e8d Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Sat, 11 Jul 2026 14:27:25 -0400 Subject: [PATCH 1/2] accept ; as well for interfaces --- tools/src/extract.ts | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/tools/src/extract.ts b/tools/src/extract.ts index 303e04c..7419eba 100644 --- a/tools/src/extract.ts +++ b/tools/src/extract.ts @@ -1880,7 +1880,8 @@ export function extractModule(sourceFile: SourceFile): RawModule { const name = recordMatch[1]; // `` → bare `T`: a Dafny type param, like the def path. const typeParams = recordMatch[2]?.split(",").map(s => s.trim().split(/\s+extends\s+/)[0].trim()).filter(Boolean); - const fields = recordMatch[3].split(",").map(f => f.trim()).filter(Boolean).map(f => { + // Split on `,` OR `;` — TS object types allow both. + const fields = recordMatch[3].split(/[,;]/).map(f => f.trim()).filter(Boolean).map(f => { const [fname, ftype] = f.split(":").map(s => s.trim()); const synth = _synthFromTsTypeString(ftype); return { name: fname, tsType: synth ?? ftype }; From 65bf7a7727f2df06476d775c82acae3115beeab3 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Sat, 11 Jul 2026 14:27:40 -0400 Subject: [PATCH 2/2] missing case for truthy int --- tools/src/transform.ts | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/tools/src/transform.ts b/tools/src/transform.ts index 415a9a5..801ed2f 100644 --- a/tools/src/transform.ts +++ b/tools/src/transform.ts @@ -602,6 +602,13 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr { else: { kind: "var", name: "undefined" }, }; } + // || on a number → `if x != 0 then x else default` (0 the only falsy int). + if (e.op === "||" && (e.left.ty.kind === "int" || e.left.ty.kind === "nat")) { + const left = lowerExpr(e.left, binds); + const right = lowerExpr(e.right, binds); + const truthy = valueTruthyCond(left, e.left.ty)!; + return { kind: "if", cond: truthy, then: left, else: right }; + } // String concatenation: `+` with a string operand. Stringify int/nat // operands (Dafny NatToString, Lean toString) and join with arrayConcat // (rendered `+` in Dafny, `++` in Lean).