src/Pure/seq.ML
author nipkow
Fri Nov 28 07:35:10 1997 +0100 (1997-11-28)
changeset 4318 9b672ea2dfe7
parent 4279 835ea07170a6
child 4992 c63a93b8577c
permissions -rw-r--r--
Fixed the definition of `termord': is now antisymmetric.
wenzelm@4270
     1
(*  Title:      Pure/seq.ML
wenzelm@4270
     2
    ID:         $Id$
wenzelm@4270
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@4270
     4
wenzelm@4270
     5
Unbounded sequences implemented by closures.  RECOMPUTES if sequence
wenzelm@4270
     6
is re-inspected.  Memoing, using polymorphic refs, was found to be
wenzelm@4270
     7
slower!  (More GCs)
wenzelm@4270
     8
*)
wenzelm@4270
     9
wenzelm@4270
    10
signature SEQ =
wenzelm@4270
    11
sig
wenzelm@4270
    12
  type 'a seq
wenzelm@4270
    13
  val make: (unit -> ('a * 'a seq) option) -> 'a seq
wenzelm@4270
    14
  val pull: 'a seq -> ('a * 'a seq) option
wenzelm@4270
    15
  val empty: 'a seq
wenzelm@4270
    16
  val cons: 'a * 'a seq -> 'a seq
wenzelm@4270
    17
  val single: 'a -> 'a seq
wenzelm@4270
    18
  val hd: 'a seq -> 'a
wenzelm@4270
    19
  val tl: 'a seq -> 'a seq
wenzelm@4270
    20
  val chop: int * 'a seq -> 'a list * 'a seq
wenzelm@4270
    21
  val list_of: 'a seq -> 'a list
wenzelm@4270
    22
  val of_list: 'a list -> 'a seq
wenzelm@4270
    23
  val map: ('a -> 'b) -> 'a seq -> 'b seq
wenzelm@4270
    24
  val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
wenzelm@4270
    25
  val append: 'a seq * 'a seq -> 'a seq
wenzelm@4270
    26
  val filter: ('a -> bool) -> 'a seq -> 'a seq
wenzelm@4270
    27
  val flat: 'a seq seq -> 'a seq
wenzelm@4270
    28
  val interleave: 'a seq * 'a seq -> 'a seq
wenzelm@4270
    29
  val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
wenzelm@4270
    30
  val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
wenzelm@4270
    31
end;
wenzelm@4270
    32
wenzelm@4270
    33
structure Seq: SEQ =
wenzelm@4270
    34
struct
wenzelm@4270
    35
wenzelm@4270
    36
wenzelm@4270
    37
datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
wenzelm@4270
    38
wenzelm@4270
    39
(*the abstraction for making a sequence*)
wenzelm@4270
    40
val make = Seq;
wenzelm@4270
    41
wenzelm@4270
    42
(*return next sequence element as None or Some (x, xq)*)
wenzelm@4270
    43
fun pull (Seq f) = f ();
wenzelm@4270
    44
wenzelm@4270
    45
wenzelm@4270
    46
(*the empty sequence*)
wenzelm@4279
    47
val empty = Seq (fn () => None);
wenzelm@4270
    48
wenzelm@4270
    49
(*prefix an element to the sequence -- use cons (x, xq) only if
wenzelm@4270
    50
  evaluation of xq need not be delayed, otherwise use
wenzelm@4270
    51
  make (fn () => Some (x, xq))*)
wenzelm@4270
    52
fun cons x_xq = make (fn () => Some x_xq);
wenzelm@4270
    53
wenzelm@4270
    54
fun single x = cons (x, empty);
wenzelm@4270
    55
wenzelm@4270
    56
(*head and tail -- beware of calling the sequence function twice!!*)
wenzelm@4270
    57
fun hd xq = #1 (the (pull xq))
wenzelm@4270
    58
and tl xq = #2 (the (pull xq));
wenzelm@4270
    59
wenzelm@4270
    60
wenzelm@4270
    61
(*the list of the first n elements, paired with rest of sequence;
wenzelm@4270
    62
  if length of list is less than n, then sequence had less than n elements*)
wenzelm@4270
    63
fun chop (n, xq) =
wenzelm@4270
    64
  if n <= 0 then ([], xq)
wenzelm@4270
    65
  else
wenzelm@4270
    66
    (case pull xq of
wenzelm@4270
    67
      None => ([], xq)
wenzelm@4270
    68
    | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
wenzelm@4270
    69
wenzelm@4270
    70
(*conversion from sequence to list*)
wenzelm@4270
    71
fun list_of xq =
wenzelm@4270
    72
  (case pull xq of
wenzelm@4270
    73
    None => []
wenzelm@4270
    74
  | Some (x, xq') => x :: list_of xq');
wenzelm@4270
    75
wenzelm@4270
    76
(*conversion from list to sequence*)
wenzelm@4270
    77
fun of_list xs = foldr cons (xs, empty);
wenzelm@4270
    78
wenzelm@4270
    79
wenzelm@4270
    80
(*map the function f over the sequence, making a new sequence*)
wenzelm@4270
    81
fun map f xq =
wenzelm@4270
    82
  make (fn () =>
wenzelm@4270
    83
    (case pull xq of
wenzelm@4270
    84
      None => None
wenzelm@4270
    85
    | Some (x, xq') => Some (f x, map f xq')));
wenzelm@4270
    86
wenzelm@4270
    87
(*map over a sequence xq, append the sequence yq*)
wenzelm@4270
    88
fun mapp f xq yq =
wenzelm@4270
    89
  let
wenzelm@4270
    90
    fun copy s =
wenzelm@4270
    91
      make (fn () =>
wenzelm@4270
    92
        (case pull s of
wenzelm@4270
    93
          None => pull yq
wenzelm@4270
    94
        | Some (x, s') => Some (f x, copy s')))
wenzelm@4270
    95
  in copy xq end;
wenzelm@4270
    96
wenzelm@4270
    97
(*sequence append:  put the elements of xq in front of those of yq*)
wenzelm@4270
    98
fun append (xq, yq) =
wenzelm@4270
    99
  let
wenzelm@4270
   100
    fun copy s =
wenzelm@4270
   101
      make (fn () =>
wenzelm@4270
   102
        (case pull s of
wenzelm@4270
   103
          None => pull yq
wenzelm@4270
   104
        | Some (x, s') => Some (x, copy s')))
wenzelm@4270
   105
  in copy xq end;
wenzelm@4270
   106
wenzelm@4270
   107
(*filter sequence by predicate*)
wenzelm@4270
   108
fun filter pred xq =
wenzelm@4270
   109
  let
wenzelm@4270
   110
    fun copy s =
wenzelm@4270
   111
      make (fn () =>
wenzelm@4270
   112
        (case pull s of
wenzelm@4270
   113
          None => None
wenzelm@4270
   114
        | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));
wenzelm@4270
   115
  in copy xq end;
wenzelm@4270
   116
wenzelm@4270
   117
(*flatten a sequence of sequences to a single sequence*)
wenzelm@4270
   118
fun flat xqq =
wenzelm@4270
   119
  make (fn () =>
wenzelm@4270
   120
    (case pull xqq of
wenzelm@4270
   121
      None => None
wenzelm@4270
   122
    | Some (xq, xqq') => pull (append (xq, flat xqq'))));
wenzelm@4270
   123
wenzelm@4270
   124
(*interleave elements of xq with those of yq -- fairer than append*)
wenzelm@4270
   125
fun interleave (xq, yq) =
wenzelm@4270
   126
  make (fn () =>
wenzelm@4270
   127
    (case pull xq of
wenzelm@4270
   128
      None => pull yq
wenzelm@4270
   129
    | Some (x, xq') => Some (x, interleave (yq, xq'))));
wenzelm@4270
   130
wenzelm@4270
   131
wenzelm@4270
   132
(*functional to print a sequence, up to "count" elements;
wenzelm@4270
   133
  the function prelem should print the element number and also the element*)
wenzelm@4270
   134
fun print prelem count seq =
wenzelm@4270
   135
  let
wenzelm@4270
   136
    fun pr (k, xq) =
wenzelm@4270
   137
      if k > count then ()
wenzelm@4270
   138
      else
wenzelm@4270
   139
        (case pull xq of
wenzelm@4270
   140
          None => ()
wenzelm@4270
   141
        | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
wenzelm@4270
   142
  in pr (1, seq) end;
wenzelm@4270
   143
wenzelm@4270
   144
(*accumulating a function over a sequence; this is lazy*)
wenzelm@4270
   145
fun it_right f (xq, yq) =
wenzelm@4270
   146
  let
wenzelm@4270
   147
    fun its s =
wenzelm@4270
   148
      make (fn () =>
wenzelm@4270
   149
        (case pull s of
wenzelm@4270
   150
          None => pull yq
wenzelm@4270
   151
        | Some (a, s') => pull (f (a, its s'))))
wenzelm@4270
   152
  in its xq end;
wenzelm@4270
   153
wenzelm@4270
   154
wenzelm@4270
   155
end;