1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7signature LIST_EXTRAS = 8sig 9 (* 10 `map_find_first f xs` applies `f` to each element of `xs`, returning the 11 first result that is `SOME _`, or `NONE` otherwise. For example: 12 13 `map_find_first (try hd) [[], [1], [2]] = SOME 1` 14 15 `map_find_first (try hd) [[], [], []] = NONE` 16 *) 17 val map_find_first: ('a -> 'b option) -> 'a list -> 'b option; 18 19 (* 20 `find_index test xs` returns the index of the first element of `xs` that 21 passes `test`, or `NONE` if no such element exists. For example: 22 23 `find_index (curry op = "c") ["a", "b", "c"] = SOME 2` 24 25 `find_index (curry op = "d") ["a", "b", "c"] = NONE` 26 27 This is similar to `Library.get_index`, except we don't try and return the 28 found element. 29 *) 30 val find_index: ('a -> bool) -> 'a list -> int option; 31 32 (* 33 `unfold f init` repeatedly calls `f` to construct elements 34 of a list, until it returns NONE. For example: 35 36 `unfold 37 (fn idx => if idx < 10 then SOME ("hello", idx + 1) else NONE) 38 7 39 = ["hello", "hello", "hello"]` 40 41 `unfold (fn x => SOME (1, x)) anything` never returns. 42 43 `unfold (K NONE) anything = []` 44 *) 45 val unfold: ('acc -> ('item * 'acc) option) -> 'acc -> 'item list; 46 47 (* `range from to` produces the list of integers between 48 `from` (inclusive) and `to` (exclusive). For example: 49 50 `range 3 5 = [3, 4]` 51 `range ~1 2 = [~1, 0, 1]` 52 *) 53 val range: int -> int -> int list; 54end 55 56structure ListExtras: LIST_EXTRAS = 57struct 58 59fun map_find_first (f: 'a -> 'b option) (xs: 'a list): 'b option = 60 case xs of 61 [] => NONE 62 | x :: xs' => 63 (case f x of 64 SOME x' => SOME x' 65 | NONE => map_find_first f xs') 66 67fun find_index test = 68 Library.get_index (fn x => if test x then SOME () else NONE) #> Option.map fst 69 70fun unfold (f: 'acc -> ('item * 'acc) option) (acc: 'acc) = 71 case f acc of 72 NONE => [] 73 | SOME (item, new_acc) => item :: unfold f new_acc; 74 75fun range from to = 76 unfold (fn i => if i < to then SOME (i, i + 1) else NONE) from; 77 78end 79