1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *
6 * Copyright 2001 John Hurd
7 * SPDX-License-Identifier: BSD-3-Clause
8 *)
9
10signature STRING_EXTRAS =
11sig
12  (*
13    `split sep s` returns the list of substrings of `s` that are
14    separated by `sep`. For example:
15
16    `split ":" "hello:world" = ["hello", "world"]`
17    `split "foo" "barbaz" = ["barbaz"]`
18  *)
19  val split: string -> string -> string list
20end
21
22structure StringExtras: STRING_EXTRAS =
23struct
24
25\<comment>\<open>
26  Copied from @{file "~~/src/Tools/Metis/src/Useful.sml"}.
27\<close>
28local
29  fun match [] l = SOME l
30    | match _ [] = NONE
31    | match (x :: xs) (y :: ys) = if x = y then match xs ys else NONE;
32
33  fun stringify acc [] = acc
34    | stringify acc (h :: t) = stringify (String.implode h :: acc) t;
35in
36  fun split (sep: string) (s: string) =
37      let
38        val pat = String.explode sep
39
40        fun div1 prev recent [] = stringify [] (List.rev recent :: prev)
41          | div1 prev recent (l as h :: t) =
42            case match pat l of
43              NONE => div1 prev (h :: recent) t
44            | SOME rest => div1 (List.rev recent :: prev) [] rest
45      in
46        div1 [] [] (String.explode s)
47      end;
48end;
49
50end;
51