From 634a3c7bec7717a47b12ef6ba4102e77dcf6d201 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Sat, 11 Jul 2026 15:06:22 -0400 Subject: [PATCH] more ops, and update docs --- SPEC.md | 5 ++++- tools/src/dafny-emit.ts | 29 ++++++++++++++++++++++++++++- tools/src/resolve.ts | 4 ++-- 3 files changed, 34 insertions(+), 4 deletions(-) diff --git a/SPEC.md b/SPEC.md index 20542dd..ed72f7d 100644 --- a/SPEC.md +++ b/SPEC.md @@ -167,7 +167,7 @@ When imported types can't be resolved by ts-morph (e.g., in monorepos with bundl //@ declare-type Rect { x: number, y: number, width: number, height: number } ``` -Each `declare-type` generates a Dafny `datatype` (or Lean `structure`) with the given fields. Field types use TS syntax (`number`, `string`, `boolean`, `T[]`, etc.) and are mapped through the standard type rules (§6.1). +Each `declare-type` generates a Dafny `datatype` (or Lean `structure`) with the given fields. Fields separate on `,` or `;` (TS object types accept either). Field types use TS syntax (`number`, `string`, `boolean`, `T[]`, etc.) and are mapped through the standard type rules (§6.1). Place `declare-type` annotations before the first function that uses the type. They can appear as leading comments on any statement. `declare-type` takes precedence over any type/interface of the same name in the source file, and is never filtered out by brownfield mode. @@ -478,18 +478,21 @@ The same coercion applies to non-bool conditions in `if`/`while`/`?:` positions: | `arr.find((x) => e)` | `arr.find? (fun x => e)` | — | | `arr.findIndex((x) => e)` | — | `SeqFindIndex(arr, (x) => e)` (preamble: `-1 ⇔ no match`, `≥0 ⇔ first match with no earlier match`) | | `arr.findLast((x) => e)` | — | `SeqFindLast(arr, (x) => e)` (preamble) | +| `arr.findLastIndex((x) => e)` | — | `SeqFindLastIndex(arr, (x) => e)` (preamble: `-1 ⇔ no match`, `≥0 ⇔ last match with no later match`) | | `arr.flat()` | — | `SeqFlatten(arr)` (preamble) | | `arr.join(sep)` | `(String.intercalate sep arr.toList)` | `SeqJoin(arr, sep)` (preamble) | | `arr.shift()` | — | `arr[0]` + `arr := arr[1..]` | | `arr.pop()` | — | `(if \|arr\|>0 then Some(arr[\|arr\|-1]) else None)` + `arr := (if \|arr\|>0 then arr[..\|arr\|-1] else arr)` | | `arr.unshift(e)` | `(#[e] ++ arr)` (mutating → reassignment) | `([e] + arr)` (mutating → reassignment) | | `arr.sort(cmp)` | — | `SeqSortBy(arr, cmp)` (preamble axiom: permutation + length-preserving + sorted; mutating; `requires` cmp a total preorder) | +| `arr.sort()` (no comparator) | — | `SeqSort(arr)` (preamble axiom: permutation + length-preserving only — JS default order is type-dependent) | | `arr.slice(start)` | `arr.extract start arr.size` | `arr[start..]` | | `arr.slice(start, end)` | `arr.extract start end` | `arr[start..end]` | | `expr!` (non-null) | unwrap Option | unwrap Option / direct map access | | `expr \|\| default` (on optional) | match Some/None | `match { Some(v) => v, None => default }` | | `expr \|\| undefined` (on optional) | identity | identity (no-op) | | `expr \|\| default` (on string) | if non-empty | `if \|expr\| > 0 then expr else default` | +| `expr \|\| default` (on number) | if nonzero | `if expr != 0 then expr else default` | | `expr \|\| default` (on array) | `expr` (arrays are always truthy) | `expr` (arrays are always truthy) | | `expr?.method(args)` | — | `if key in map { ... }` | | `expr as T` | stripped | stripped | diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index fcc4190..8522268 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -262,7 +262,10 @@ function emitExpr(e: Expr): string { if (e.method === "push") return `(${obj} + [${args.join(", ")}])`; if (e.method === "unshift") return `([${args.join(", ")}] + ${obj})`; if (e.method === "concat") return `(${obj} + [${args.join(", ")}])`; - if (e.method === "sort") { needPreamble("SeqSortBy"); return `SeqSortBy(${obj}, ${args[0]})`; } + if (e.method === "sort") { + if (args.length === 0) { needPreamble("SeqSort"); return `SeqSort(${obj})`; } + needPreamble("SeqSortBy"); return `SeqSortBy(${obj}, ${args[0]})`; + } // No-arg slice is a full copy; Dafny seq is an immutable value type, so // the copy is just the seq itself (the idiom for "copy then mutate"). if (e.method === "slice" && args.length === 0) return obj; @@ -291,6 +294,10 @@ function emitExpr(e: Expr): string { needPreamble("SeqFindIndex"); return `SeqFindIndex(${obj}, ${args[0]})`; } + if (e.method === "findLastIndex") { + needPreamble("SeqFindLastIndex"); + return `SeqFindLastIndex(${obj}, ${args[0]})`; + } if (e.method === "flat" && args.length === 0) { needPreamble("SeqFlatten"); return `SeqFlatten(${obj})`; @@ -954,6 +961,19 @@ function SeqIndexOfFrom(s: seq, x: T, from: nat): int else SeqIndexOfFrom(s, x, from + 1) }`; +const SEQ_FIND_LAST_INDEX = `function SeqFindLastIndex(s: seq, p: T -> bool): int + ensures -1 <= SeqFindLastIndex(s, p) < |s| + ensures SeqFindLastIndex(s, p) >= 0 ==> p(s[SeqFindLastIndex(s, p)]) + ensures SeqFindLastIndex(s, p) >= 0 ==> + (forall j: int :: SeqFindLastIndex(s, p) < j < |s| ==> !p(s[j])) + ensures SeqFindLastIndex(s, p) == -1 ==> (forall i: nat :: i < |s| ==> !p(s[i])) + decreases |s| +{ + if |s| == 0 then -1 + else if p(s[|s|-1]) then |s| - 1 + else SeqFindLastIndex(s[..|s|-1], p) +}`; + const SEQ_FIND_LAST = `function SeqFindLast(s: seq, p: T -> bool): Option ensures SeqFindLast(s, p).Some? ==> p(SeqFindLast(s, p).value) ensures SeqFindLast(s, p).Some? ==> SeqFindLast(s, p).value in s @@ -1034,6 +1054,11 @@ const STRING_SPLIT = `function {:axiom} StringSplit(s: string, d: string): seq a.k - b.k` is total + transitive by linear arithmetic). +// Bare `.sort()`: permutation only, no sortedness (JS default order is type-dependent). +const SEQ_SORT = `function {:axiom} SeqSort(s: seq): seq + ensures multiset(SeqSort(s)) == multiset(s) + ensures |SeqSort(s)| == |s|`; + const SEQ_SORT_BY = `function {:axiom} SeqSortBy(s: seq, cmp: (T, T) -> int): seq requires forall a: T, b: T :: cmp(a, b) <= 0 || cmp(b, a) <= 0 requires forall a: T, b: T, c: T :: cmp(a, b) <= 0 && cmp(b, c) <= 0 ==> cmp(a, c) <= 0 @@ -1216,6 +1241,7 @@ const PREAMBLE_CODE: [string, string][] = [ ["FloorReal", FLOOR_REAL], ["SeqIndexOf", SEQ_INDEX_OF], ["SeqFindIndex", SEQ_FIND_INDEX], + ["SeqFindLastIndex", SEQ_FIND_LAST_INDEX], ["SeqFilterSome", SEQ_FILTER_SOME], ["SeqFindLast", SEQ_FIND_LAST], ["SeqFlatten", SEQ_FLATTEN], @@ -1223,6 +1249,7 @@ const PREAMBLE_CODE: [string, string][] = [ ["SafeSlice", SAFE_SLICE], ["StringIndexOf", STRING_INDEX_OF], ["StringSplit", STRING_SPLIT], + ["SeqSort", SEQ_SORT], ["SeqSortBy", SEQ_SORT_BY], ["StringTrim", STRING_TRIM], ["StringToLower", STRING_TO_LOWER], diff --git a/tools/src/resolve.ts b/tools/src/resolve.ts index ddb1206..5209a93 100644 --- a/tools/src/resolve.ts +++ b/tools/src/resolve.ts @@ -496,7 +496,7 @@ function inferLambdaParamTypes(fn: TExpr, rawArgs: RawExpr[], ctx?: Ctx): RawExp } } if (fn.kind === "field" && fn.obj.ty.kind === "array" && - ["map", "filter", "every", "some", "find", "findLast", "findIndex"].includes(fn.field) && + ["map", "filter", "every", "some", "find", "findLast", "findIndex", "findLastIndex"].includes(fn.field) && rawArgs.length >= 1 && rawArgs[0].kind === "lambda" && rawArgs[0].params.length >= 1 && !rawArgs[0].params[0].tsType) { const elemTy = fn.obj.ty.elem; @@ -598,7 +598,7 @@ function inferMethodReturnTy(fn: TExpr, args: TExpr[], ctx: Ctx): Ty { if (fn.field === "filter") return objTy; if (fn.field === "every" || fn.field === "some") return { kind: "bool" }; if (fn.field === "find" || fn.field === "findLast") return { kind: "optional", inner: objTy.elem }; - if (fn.field === "findIndex") return { kind: "int" }; + if (fn.field === "findIndex" || fn.field === "findLastIndex") return { kind: "int" }; if (fn.field === "flat" && objTy.elem.kind === "array") return { kind: "array", elem: objTy.elem.elem }; if (fn.field === "slice") return objTy; if (fn.field === "join" && objTy.elem.kind === "string") return { kind: "string" };