lib: add ML utilties 'bucket' file.

The SML standard library is pretty bare-bones compared to that of other
functional languages, so in a large enough SML project you end up with a
bunch of reimplementations of basic combinators scattered all over the
place. We'd be able to collect them if we had somewhere to collect them,
so here it is.

lib/ROOT

@@ -52,6 +52,7 @@ session Lib (lib) = Word_Lib +
     HaskellLemmaBucket
     "ml-helpers/TermPatternAntiquote"
     "ml-helpers/TacticAntiquotation"
+    "ml-helpers/MLUtils"
     "subgoal_focus/Subgoal_Methods"
     Insulin
     ExtraCorres

lib/ml-helpers/List.ML

@@ -0,0 +1,39 @@
+(*
+ * Copyright 2019, Data61
+ * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+ * ABN 41 687 119 230.
+
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+
+ * @TAG(DATA61_BSD)
+ *)
+
+signature LIST =
+sig
+  include LIST
+
+  (*
+    `map_find_first f xs` applies `f` to each element of `xs`, returning
+    the first result that is `SOME _`, or `NONE` otherwise. For example:
+
+    `map_find_first (try hd) [[], [1], [2]] = SOME 1`
+
+    `map_find_first (try hd) [[], [], []] = NONE`
+  *)
+  val map_find_first: ('a -> 'b option) -> 'a list -> 'b option;
+end
+
+structure List: LIST =
+struct
+open List
+
+fun map_find_first (f: 'a -> 'b option) (xs: 'a list): 'b option =
+    case xs of
+      [] => NONE
+    | x :: xs' =>
+          (case f x of
+            SOME x' => SOME x'
+          | NONE => map_find_first f xs')
+end

lib/ml-helpers/MLUtils.thy

@@ -0,0 +1,39 @@
+(*
+ * Copyright 2019, Data61
+ * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+ * ABN 41 687 119 230.
+
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+
+ * @TAG(DATA61_BSD)
+ *)
+
+\<comment>\<open>
+  MLUtils is a collection of 'basic' ML utilities (kind of like @{file
+  "~~/src/Pure/library.ML"}, but maintained by Trustworthy Systems). If you
+  find yourself implementing:
+      - A simple data-structure-shuffling task,
+      - Something that shows up in the standard library of other functional
+        languages, or
+      - Something that's "missing" from the general pattern of an Isabelle ML
+        library,
+  consider adding it here.
+
+  When appropriate, you should consider *extending* an existing signature,
+  rather than creating a new one: `String.whatever` is more meaningful than
+  `TSStringLib.whatever`, and it doesn't damage the bindings to the "original"
+  signature in any way. Look at `String.ML` in this directory for an example.
+
+  Some structures (like `Method`) can't be overridden this way. In these cases
+  name the new structure with a `Utils` suffix.
+\<close>
+
+theory MLUtils
+imports Main
+begin
+ML_file "String.ML"
+ML_file "List.ML"
+ML_file "Method.ML"
+end

lib/ml-helpers/Method.ML

@@ -0,0 +1,28 @@
+(*
+ * Copyright 2019, Data61
+ * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+ * ABN 41 687 119 230.
+
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+
+ * @TAG(DATA61_BSD)
+ *)
+
+signature METHOD_UTILS =
+sig
+  include METHOD
+
+  (* `then_all_new m1 m2` is equivalent to `(m1; m2)`. *)
+  val then_all_new:
+      (Proof.context -> method) * (Proof.context -> method) -> Proof.context -> method;
+end
+
+structure MethodUtils: METHOD_UTILS =
+struct
+open Method
+
+fun then_all_new (m1, m2) =
+    Combinator (no_combinator_info, Then_All_New, [Basic m1, Basic m2]) |> evaluate
+end

lib/ml-helpers/String.ML

@@ -0,0 +1,62 @@
+(*
+ * @TAG(OTHER_BSD)
+ *)
+(*
+ * Copyright 2019, Data61
+ * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+ * ABN 41 687 119 230.
+
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+
+ * @TAG(DATA61_BSD)
+ *)
+(*
+ * Includes code under BSD license, copyright 2001 John Hurd.
+ *)
+
+signature STRING =
+sig
+  include STRING
+
+  (*
+    `split sep s` returns the list of substrings of `s` that are
+    separated by `sep`. For example:
+
+    `split ":" "hello:world" = ["hello", "world"]`
+    `split "foo" "barbaz" = ["barbaz"]`
+  *)
+  val split: string -> string -> string list
+end
+
+structure String: STRING =
+struct
+open String
+
+\<comment>\<open>
+  Copied from @{file "~~/src/Tools/Metis/src/Useful.sml"}.
+\<close>
+local
+  fun match [] l = SOME l
+    | match _ [] = NONE
+    | match (x :: xs) (y :: ys) = if x = y then match xs ys else NONE;
+
+  fun stringify acc [] = acc
+    | stringify acc (h :: t) = stringify (String.implode h :: acc) t;
+in
+  fun split (sep: string) (s: string) =
+      let
+        val pat = String.explode sep
+
+        fun div1 prev recent [] = stringify [] (List.rev recent :: prev)
+          | div1 prev recent (l as h :: t) =
+            case match pat l of
+              NONE => div1 prev (h :: recent) t
+            | SOME rest => div1 (List.rev recent :: prev) [] rest
+      in
+        div1 [] [] (String.explode s)
+      end;
+end;
+
+end;