better safe slice function

examples/safeSlice.dfy

@@ -0,0 +1,48 @@
+// Generated by lsc from safeSlice.ts
+
+function NormalizeSliceIndex(n: nat, i: int): int
+  ensures 0 <= NormalizeSliceIndex(n, i) <= n as int
+{
+  if i < 0 then
+    if n as int + i < 0 then 0 else n as int + i
+  else if i > n as int then n as int
+  else i
+}
+
+function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
+  ensures |SafeSlice(s, lo, hi)| <= |s|
+{
+  var lo' := NormalizeSliceIndex(|s|, lo);
+  var hi' := NormalizeSliceIndex(|s|, hi);
+  if hi' < lo' then [] else s[lo'..hi']
+}
+
+function sliceNegativeStart(): seq<int>
+{
+  SafeSlice([1, 2], -1, 2)
+}
+
+lemma sliceNegativeStart_ensures()
+  ensures (sliceNegativeStart() == [2])
+{
+}
+
+function sliceNegativeEnd(): seq<int>
+{
+  SafeSlice([1, 2], 0, -1)
+}
+
+lemma sliceNegativeEnd_ensures()
+  ensures (sliceNegativeEnd() == [1])
+{
+}
+
+function sliceNegativeBounds(): seq<int>
+{
+  SafeSlice([1, 2, 3, 4], -3, -1)
+}
+
+lemma sliceNegativeBounds_ensures()
+  ensures (sliceNegativeBounds() == [2, 3])
+{
+}

examples/safeSlice.dfy.gen

@@ -0,0 +1,48 @@
+// Generated by lsc from safeSlice.ts
+
+function NormalizeSliceIndex(n: nat, i: int): int
+  ensures 0 <= NormalizeSliceIndex(n, i) <= n as int
+{
+  if i < 0 then
+    if n as int + i < 0 then 0 else n as int + i
+  else if i > n as int then n as int
+  else i
+}
+
+function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
+  ensures |SafeSlice(s, lo, hi)| <= |s|
+{
+  var lo' := NormalizeSliceIndex(|s|, lo);
+  var hi' := NormalizeSliceIndex(|s|, hi);
+  if hi' < lo' then [] else s[lo'..hi']
+}
+
+function sliceNegativeStart(): seq<int>
+{
+  SafeSlice([1, 2], -1, 2)
+}
+
+lemma sliceNegativeStart_ensures()
+  ensures (sliceNegativeStart() == [2])
+{
+}
+
+function sliceNegativeEnd(): seq<int>
+{
+  SafeSlice([1, 2], 0, -1)
+}
+
+lemma sliceNegativeEnd_ensures()
+  ensures (sliceNegativeEnd() == [1])
+{
+}
+
+function sliceNegativeBounds(): seq<int>
+{
+  SafeSlice([1, 2, 3, 4], -3, -1)
+}
+
+lemma sliceNegativeBounds_ensures()
+  ensures (sliceNegativeBounds() == [2, 3])
+{
+}

examples/safeSlice.ts

@@ -0,0 +1,21 @@
+// examples/safeSlice.ts
+
+//@ backend dafny
+//@ safe-slice
+
+
+
+function sliceNegativeStart(): number[] {
+  //@ ensures \result === [2]
+  return [1, 2].slice(-1, 2);
+}
+
+function sliceNegativeEnd(): number[] {
+  //@ ensures \result === [1]
+  return [1, 2].slice(0, -1);
+}
+
+function sliceNegativeBounds(): number[] {
+  //@ ensures \result === [2, 3]
+  return [1, 2, 3, 4].slice(-3, -1);
+}

tools/src/dafny-emit.ts

@@ -1003,12 +1003,21 @@ const SEQ_JOIN = `function SeqJoin(s: seq<string>, sep: string): string
   else s[0] + sep + SeqJoin(s[1..], sep)
 }`;
 
-const SAFE_SLICE = `function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
+const SAFE_SLICE = `function NormalizeSliceIndex(n: nat, i: int): int
+  ensures 0 <= NormalizeSliceIndex(n, i) <= n as int
+{
+  if i < 0 then
+    if n as int + i < 0 then 0 else n as int + i
+  else if i > n as int then n as int
+  else i
+}
+
+function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
   ensures |SafeSlice(s, lo, hi)| <= |s|
 {
-  var lo' := if lo < 0 then 0 else if lo > |s| as int then |s| else lo;
-  var hi' := if hi > |s| as int then |s| else if hi < lo' then lo' else hi;
-  s[lo'..hi']
+  var lo' := NormalizeSliceIndex(|s|, lo);
+  var hi' := NormalizeSliceIndex(|s|, hi);
+  if hi' < lo' then [] else s[lo'..hi']
 }`;
 
 const STRING_INDEX_OF = `function StringIndexOf(s: string, sub: string): int