Seq.ml 1 KB
 POTTIER Francois committed Jul 03, 2015 1 2 3 ``````(* Sequences with constant time concatenation and linear-time conversion to an ordinary list. *) `````` POTTIER Francois committed Jul 10, 2015 4 5 6 ``````(* We maintain the invariant that the left-hand side of [SConcat] is never an empty sequence. This allows a slight improvement in [first]. *) `````` POTTIER Francois committed Jul 03, 2015 7 8 9 10 11 12 13 14 15 16 17 18 ``````type 'a seq = | SZero | SOne of 'a | SConcat of 'a seq * 'a seq let empty = SZero let singleton x = SOne x let append xs ys = `````` POTTIER Francois committed Jul 10, 2015 19 20 21 22 23 24 `````` match xs with | SZero -> ys | SOne _ | SConcat _ -> SConcat (xs, ys) `````` POTTIER Francois committed Jul 03, 2015 25 26 27 28 29 30 31 32 33 34 35 36 `````` let rec elements xs accu = match xs with | SZero -> accu | SOne x -> x :: accu | SConcat (xs1, xs2) -> elements xs1 (elements xs2 accu) let elements xs = elements xs [] `````` POTTIER Francois committed Jul 03, 2015 37 38 39 40 41 42 43 `````` let rec concat xss = match xss with | [] -> empty | xs :: xss -> append xs (concat xss) `````` POTTIER Francois committed Jul 10, 2015 44 45 46 47 48 49 50 51 52 53 54 55 `````` let rec first xs = match xs with | SZero -> (* We disallow applying [first] to an empty sequence. *) assert false | SOne x -> x | SConcat (xs1, _) -> (* Our invariant guarantees [xs1] is nonempty. *) first xs1 ``````