feat: Add a few more Std.Collections.Seq functions (#4867)

### Description
These are functions I got used to having around in [THIS "standard
library"](https://github.com/aws/aws-cryptographic-material-providers-library-dafny/tree/main/StandardLibrary)
and didn't spot they weren't in OUR standard library until now. :)

Also removed `Std.Strings.Concat` (already covered more generically with
`Std.Collections.Seq.Flatten`) and moved `Std.Strings.Join` to
`Std.Collections.Seq`: these were only referenced by tests and their
existence contradicted the documentation on the purpose of the `Strings`
library.

Also commented out the remaining print statements in JSONTests.dfy to
keep the testing output cleaner.

### How has this been tested?
DafnyStandardLibraries tests.

Source/DafnyStandardLibraries/Makefile

@@ -8,7 +8,8 @@ DOO_FILE_TARGET=binaries/DafnyStandardLibraries.doo
 all: check-binary test check-format check-examples
 
 verify:
-	$(DAFNY) verify src/DafnyStdLibs/dfyconfig.toml
+	$(DAFNY) verify src/Std/dfyconfig.toml
+	make -C src/Std/TargetSpecific verify-all
 
 build-binary:
 	$(DAFNY) build -t:lib src/Std/dfyconfig.toml --output:${DOO_FILE_SOURCE}

Source/DafnyStandardLibraries/examples/CollectionsExamples.dfy

@@ -41,6 +41,8 @@ module CollectionsExamples {
       expect IndexOf(s, 1) == 0;
       AssertAndExpect(IndexOfOption(s, 5) == Some(4));
       AssertAndExpect(IndexOfOption(s, 42) == None);
+      expect IndexByOption(s, x => x % 2 == 0) == Some(2);
+      AssertAndExpect(IndexByOption(s, x => 100 < x) == None);
     }
 
     method {:test} TestSequenceLastIndexOf() {
@@ -78,6 +80,18 @@ module CollectionsExamples {
     method {:test} TestFlatten() {
       AssertAndExpect(Flatten([[1, 1, 2], [3, 5], [], [8, 13, 21]]) == s);
       AssertAndExpect(FlattenReverse([[1, 1, 2], [3, 5], [], [8, 13, 21]]) == s);
+      AssertAndExpect(Flatten([]) == "");
+      AssertAndExpect(Flatten(["aaa", "bbb", "ccc"]) == "aaabbbccc");
+    }
+
+    method {:test} TestJoin() {
+      AssertAndExpect(Join([], ",") == "");
+      AssertAndExpect(Join(["0", "1", "2"], ",") == "0,1,2");
+    }
+
+    method {:test} TestSplit() {
+      expect Split("0,1,2", ',') == ["0", "1", "2"];
+      expect Split("0 1  2", ' ') == ["0", "1", "", "2"];
     }
 
     method {:test} TestMapFilter() {

Source/DafnyStandardLibraries/examples/JSON/JSONTests.dfy

@@ -15,9 +15,9 @@ abstract module AbstractWrapper {
     var js  :- expect Deserialize(bs);
     // print indent, "=> ", js, "\n";
     var bs'  :- expect Serialize(js);
-    print indent, "=> ", FromUTF8Checked(bs'), "\n";
+    // print indent, "=> ", FromUTF8Checked(bs'), "\n";
     var sbs' :- expect SpecSerialize(js);
-    print indent, "=> ", FromUTF8Checked(sbs'), "\n";
+    // print indent, "=> ", FromUTF8Checked(sbs'), "\n";
     var js'  :- expect Deserialize(bs');
     Check(bs, js, bs', sbs', js');
   }
@@ -32,9 +32,9 @@ abstract module AbstractWrapper {
       var input := vectors[i];
       var idx := Strings.OfInt(i);
       var indent := seq(|idx| + 1, _ => ' ');
-      print "[", idx, "]: ", input, "\n";
+      // print "[", idx, "]: ", input, "\n";
       TestString(input, indent);
-      print "\n";
+      // print "\n";
     }
   }
 }

Source/DafnyStandardLibraries/examples/StringsExamples.dfy

@@ -53,14 +53,4 @@ module StringsExamples {
     expect OfChar('c') == "c";
     expect OfChar('f') == "f";
   }
-
-  method {:test} TestJoin() {
-    expect Join(",", []) == "";
-    expect Join(",", ["0", "1", "2"]) == "0,1,2";
-  }
-
-  method {:test} TestConcat() {
-    expect Concat([]) == "";
-    expect Concat(["aaa", "bbb", "ccc"]) == "aaabbbccc";
-  }
 }

Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy

@@ -282,12 +282,22 @@ module Std.Collections.Seq {
     ensures if o.Some? then o.value < |xs| && xs[o.value] == v &&
                             forall j {:trigger xs[j]} :: 0 <= j < o.value ==> xs[j] != v
             else v !in xs
+  {
+    IndexByOption(xs, x => x == v)
+  }
+
+  /* Returns Some(i), if an element satisfying p occurs at least once in a sequence, and i is
+    the index of the first such occurrence. Otherwise the return is None. */
+  function {:opaque} IndexByOption<T(==)>(xs: seq<T>, p: T -> bool): (o: Option<nat>)
+    ensures if o.Some? then o.value < |xs| && p(xs[o.value]) &&
+                            forall j {:trigger xs[j]} :: 0 <= j < o.value ==> !p(xs[j])
+            else forall x <- xs ::!p(x)
   {
     if |xs| == 0 then None()
     else
-    if xs[0] == v then Some(0)
+    if p(xs[0]) then Some(0)
     else
-      var o' := IndexOfOption(xs[1..], v);
+      var o' := IndexByOption(xs[1..], p);
       if o'.Some? then Some(o'.value + 1) else None()
   }
 
@@ -307,9 +317,19 @@ module Std.Collections.Seq {
     ensures if o.Some? then o.value < |xs| && xs[o.value] == v &&
                             forall j {:trigger xs[j]} :: o.value < j < |xs| ==> xs[j] != v
             else v !in xs
+  {
+    LastIndexByOption(xs, x => x == v)
+  }
+
+  /* Returns Some(i), if an element satisfying p occurs at least once in a sequence, and i is
+     the index of the last such occurrence. Otherwise the return is None. */
+  function {:opaque} LastIndexByOption<T(==)>(xs: seq<T>, p: T -> bool): (o: Option<nat>)
+    ensures if o.Some? then o.value < |xs| && p(xs[o.value]) &&
+                            forall j {:trigger xs[j]} :: o.value < j < |xs| ==> !p(xs[j])
+            else forall x <- xs ::!p(x)
   {
     if |xs| == 0 then None()
-    else if xs[|xs|-1] == v then Some(|xs| - 1) else LastIndexOfOption(xs[..|xs|-1], v)
+    else if p(xs[|xs|-1]) then Some(|xs| - 1) else LastIndexByOption(xs[..|xs|-1], p)
   }
 
   /* Returns a sequence without the element at a given position. */
@@ -604,6 +624,90 @@ module Std.Collections.Seq {
     }
   }
 
+  /* Join a sequence of sequences using a separator sequence.
+     Particularly useful for strings (since string is just an alias for seq<char>) */
+  function Join<T>(seqs: seq<seq<T>>, separator: seq<T>) : seq<T> {
+    if |seqs| == 0 then []
+    else if |seqs| == 1 then seqs[0]
+    else seqs[0] + separator + Join(seqs[1..], separator)
+  }
+
+  lemma LemmaJoinWithEmptySeparator(seqs: seq<string>)
+    ensures Flatten(seqs) == Join(seqs, [])
+  {}
+
+  function {:tailrecursion} Split<T(==)>(s: seq<T>, delim: T): (res: seq<seq<T>>)
+    ensures delim !in s ==> res == [s]
+    ensures s == [] ==> res == [[]]
+    ensures 0 < |res|
+    ensures forall i :: 0 <= i < |res| ==> delim !in res[i]
+    ensures Join(res, [delim]) == s
+    decreases |s|
+  {
+    var i := IndexOfOption(s, delim);
+    if i.Some? then [s[..i.value]] + Split(s[(i.value + 1)..], delim) else [s]
+  }
+
+  /* Split on first occurrence of delim, which must exist */
+  function {:tailrecursion} SplitOnce<T(==)>(s: seq<T>, delim: T): (res : (seq<T>,seq<T>))
+    requires delim in s
+    ensures res.0 + [delim] + res.1 == s
+    ensures !(delim in res.0)
+  {
+    var i := IndexOfOption(s, delim);
+    assert i.Some?;
+    (s[..i.value], s[(i.value + 1)..])
+  }
+
+  // split on first occurrence of delim, return None if delim not present
+  function {:tailrecursion} SplitOnceOption<T(==)>(s: seq<T>, delim: T): (res : Option<(seq<T>,seq<T>)>)
+    ensures res.Some? ==> res.value.0 + [delim] + res.value.1 == s
+    ensures res.None? ==> !(delim in s)
+    ensures res.Some? ==> !(delim in res.value.0)
+  {
+    var i :- IndexOfOption(s, delim);
+    Some((s[..i], s[(i + 1)..]))
+  }
+
+  lemma WillSplitOnDelim<T>(s: seq<T>, delim: T, prefix: seq<T>)
+    requires |prefix| < |s|
+    requires forall i :: 0 <= i < |prefix| ==> prefix[i] == s[i]
+    requires delim !in prefix && s[|prefix|] == delim
+    ensures Split(s, delim) == [prefix] + Split(s[|prefix| + 1..], delim)
+  {
+    calc {
+      Split(s, delim);
+    ==
+      var i := IndexOfOption(s, delim);
+      if i.Some? then [s[..i.value]] + Split(s[i.value + 1..], delim) else [s];
+    ==  { IndexOfOptionLocatesElem(s, delim, |prefix|); assert IndexOfOption(s, delim).Some?; }
+      [s[..|prefix|]] + Split(s[|prefix| + 1..], delim);
+    ==  { assert s[..|prefix|] == prefix; }
+      [prefix] + Split(s[|prefix| + 1..], delim);
+    }
+  }
+
+  lemma WillNotSplitWithOutDelim<T>(s: seq<T>, delim: T)
+    requires delim !in s
+    ensures Split(s, delim) == [s]
+  {
+    calc {
+      Split(s, delim);
+    ==
+      var i := IndexOfOption(s, delim);
+      if i.Some? then [s[..i.value]] + Split(s[i.value+1..], delim) else [s];
+    ==  { IndexOfOptionLocatesElem(s, delim, |s|); }
+      [s];
+    }
+  }
+
+  lemma IndexOfOptionLocatesElem<T>(s: seq<T>, c: T, elemIndex: nat)
+    requires 0 <= elemIndex <= |s|
+    requires forall i :: 0 <= i < elemIndex ==> s[i] != c
+    requires elemIndex == |s| || s[elemIndex] == c
+    ensures IndexOfOption(s, c) == if elemIndex == |s| then None else Some(elemIndex)
+    decreases elemIndex
+  {}
 
   /**********************************************************
    *

Source/DafnyStandardLibraries/src/Std/Strings.dfy

@@ -255,25 +255,4 @@ module {:disableNonlinearArithmetic} Std.Strings {
   function OfChar(c: char) : string {
     [c]
   }
-
-  /**
-  Join a sequence of strings using a separator string
-   */
-  function Join(sep: string, strs: seq<string>) : string {
-    if |strs| == 0 then ""
-    else if |strs| == 1 then strs[0]
-    else strs[0] + sep + Join(sep, strs[1..])
-  }
-
-  /**
-  Concatenate a sequence of strings
-   */
-  function Concat(strs: seq<string>) : string {
-    if |strs| == 0 then ""
-    else strs[0] + Concat(strs[1..])
-  }
-
-  lemma Concat_Join(strs: seq<string>)
-    ensures Concat(strs) == Join("", strs)
-  {}
 }