Seq.ml 1 KB
Newer Older
1 2 3
(* Sequences with constant time concatenation and linear-time conversion
   to an ordinary list. *)

POTTIER Francois's avatar
POTTIER Francois committed
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]. *)

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's avatar
POTTIER Francois committed
19 20 21 22 23 24
  match xs with
  | SZero ->
      ys
  | SOne _
  | SConcat _ ->
      SConcat (xs, ys)
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's avatar
POTTIER Francois committed
37 38 39 40 41 42 43

let rec concat xss =
  match xss with
  | [] ->
      empty
  | xs :: xss ->
      append xs (concat xss)
POTTIER Francois's avatar
POTTIER Francois committed
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