Seq.ml 1.95 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
(******************************************************************************)
(*                                                                            *)
(*                                   Menhir                                   *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*              Yann Régis-Gianas, PPS, Université Paris Diderot              *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU General Public License version 2, as described in the    *)
(*  file LICENSE.                                                             *)
(*                                                                            *)
(******************************************************************************)

14 15 16
(* Sequences with constant time concatenation and linear-time conversion
   to an ordinary list. *)

POTTIER Francois's avatar
POTTIER Francois committed
17 18 19
(* We maintain the invariant that the left-hand side of [SConcat] is never
   an empty sequence. This allows a slight improvement in [first]. *)

20 21 22 23 24 25 26 27 28 29 30 31
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
32 33 34 35 36 37
  match xs with
  | SZero ->
      ys
  | SOne _
  | SConcat _ ->
      SConcat (xs, ys)
38 39 40 41 42 43 44 45 46 47 48 49

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
50 51 52 53 54 55 56

let rec concat xss =
  match xss with
  | [] ->
      empty
  | xs :: xss ->
      append xs (concat xss)
POTTIER Francois's avatar
POTTIER Francois committed
57 58 59 60 61 62 63 64 65 66 67 68

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