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