src/Pure/General/seq.ML
author wenzelm
Thu Oct 11 19:22:15 2001 +0200 (2001-10-11 ago)
changeset 11721 0d60622b668f
parent 8806 a202293db3f6
child 12851 e87496286934
permissions -rw-r--r--
added try;
wenzelm@6118
     1
(*  Title:      Pure/General/seq.ML
wenzelm@5014
     2
    ID:         $Id$
wenzelm@5014
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@8806
     4
    Author:   	Markus Wenzel, TU Munich
wenzelm@8806
     5
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@5014
     6
wenzelm@5014
     7
Unbounded sequences implemented by closures.  RECOMPUTES if sequence
wenzelm@5014
     8
is re-inspected.  Memoing, using polymorphic refs, was found to be
wenzelm@5014
     9
slower!  (More GCs)
wenzelm@5014
    10
*)
wenzelm@5014
    11
wenzelm@5014
    12
signature SEQ =
wenzelm@5014
    13
sig
wenzelm@5014
    14
  type 'a seq
wenzelm@5014
    15
  val make: (unit -> ('a * 'a seq) option) -> 'a seq
wenzelm@5014
    16
  val pull: 'a seq -> ('a * 'a seq) option
wenzelm@5014
    17
  val empty: 'a seq
wenzelm@5014
    18
  val cons: 'a * 'a seq -> 'a seq
wenzelm@5014
    19
  val single: 'a -> 'a seq
wenzelm@11721
    20
  val try: ('a -> 'b) -> 'a -> 'b seq
wenzelm@5014
    21
  val hd: 'a seq -> 'a
wenzelm@5014
    22
  val tl: 'a seq -> 'a seq
wenzelm@5014
    23
  val chop: int * 'a seq -> 'a list * 'a seq
wenzelm@5014
    24
  val list_of: 'a seq -> 'a list
wenzelm@5014
    25
  val of_list: 'a list -> 'a seq
wenzelm@5014
    26
  val map: ('a -> 'b) -> 'a seq -> 'b seq
wenzelm@5014
    27
  val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
wenzelm@5014
    28
  val append: 'a seq * 'a seq -> 'a seq
wenzelm@5014
    29
  val filter: ('a -> bool) -> 'a seq -> 'a seq
wenzelm@5014
    30
  val flat: 'a seq seq -> 'a seq
wenzelm@5014
    31
  val interleave: 'a seq * 'a seq -> 'a seq
wenzelm@5014
    32
  val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
wenzelm@5014
    33
  val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
wenzelm@6927
    34
  val commute: 'a seq list -> 'a list seq
wenzelm@5014
    35
  val succeed: 'a -> 'a seq
wenzelm@5014
    36
  val fail: 'a -> 'b seq
wenzelm@5014
    37
  val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
wenzelm@5014
    38
  val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
wenzelm@5014
    39
  val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
wenzelm@5014
    40
  val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
wenzelm@5014
    41
  val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
wenzelm@5014
    42
  val TRY: ('a -> 'a seq) -> 'a -> 'a seq
wenzelm@5014
    43
  val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
wenzelm@5558
    44
  val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
wenzelm@8535
    45
  val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
wenzelm@5014
    46
end;
wenzelm@5014
    47
wenzelm@5014
    48
structure Seq: SEQ =
wenzelm@5014
    49
struct
wenzelm@5014
    50
wenzelm@5014
    51
wenzelm@5014
    52
(** lazy sequences **)
wenzelm@5014
    53
wenzelm@5014
    54
datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
wenzelm@5014
    55
wenzelm@5014
    56
(*the abstraction for making a sequence*)
wenzelm@5014
    57
val make = Seq;
wenzelm@5014
    58
wenzelm@5014
    59
(*return next sequence element as None or Some (x, xq)*)
wenzelm@5014
    60
fun pull (Seq f) = f ();
wenzelm@5014
    61
wenzelm@5014
    62
wenzelm@5014
    63
(*the empty sequence*)
wenzelm@5014
    64
val empty = Seq (fn () => None);
wenzelm@5014
    65
wenzelm@5014
    66
(*prefix an element to the sequence -- use cons (x, xq) only if
wenzelm@5014
    67
  evaluation of xq need not be delayed, otherwise use
wenzelm@5014
    68
  make (fn () => Some (x, xq))*)
wenzelm@5014
    69
fun cons x_xq = make (fn () => Some x_xq);
wenzelm@5014
    70
wenzelm@5014
    71
fun single x = cons (x, empty);
wenzelm@5014
    72
wenzelm@5014
    73
(*head and tail -- beware of calling the sequence function twice!!*)
wenzelm@5014
    74
fun hd xq = #1 (the (pull xq))
wenzelm@5014
    75
and tl xq = #2 (the (pull xq));
wenzelm@5014
    76
wenzelm@11721
    77
(*partial function as procedure*)
wenzelm@11721
    78
fun try f x =
wenzelm@11721
    79
  (case Library.try f x of
wenzelm@11721
    80
    Some y => single y
wenzelm@11721
    81
  | None => empty);
wenzelm@11721
    82
wenzelm@5014
    83
wenzelm@5014
    84
(*the list of the first n elements, paired with rest of sequence;
wenzelm@5014
    85
  if length of list is less than n, then sequence had less than n elements*)
wenzelm@5014
    86
fun chop (n, xq) =
wenzelm@5014
    87
  if n <= 0 then ([], xq)
wenzelm@5014
    88
  else
wenzelm@5014
    89
    (case pull xq of
wenzelm@5014
    90
      None => ([], xq)
wenzelm@5014
    91
    | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
wenzelm@5014
    92
wenzelm@5014
    93
(*conversion from sequence to list*)
wenzelm@5014
    94
fun list_of xq =
wenzelm@5014
    95
  (case pull xq of
wenzelm@5014
    96
    None => []
wenzelm@5014
    97
  | Some (x, xq') => x :: list_of xq');
wenzelm@5014
    98
wenzelm@5014
    99
(*conversion from list to sequence*)
wenzelm@5014
   100
fun of_list xs = foldr cons (xs, empty);
wenzelm@5014
   101
wenzelm@5014
   102
wenzelm@5014
   103
(*map the function f over the sequence, making a new sequence*)
wenzelm@5014
   104
fun map f xq =
wenzelm@5014
   105
  make (fn () =>
wenzelm@5014
   106
    (case pull xq of
wenzelm@5014
   107
      None => None
wenzelm@5014
   108
    | Some (x, xq') => Some (f x, map f xq')));
wenzelm@5014
   109
wenzelm@5014
   110
(*map over a sequence xq, append the sequence yq*)
wenzelm@5014
   111
fun mapp f xq yq =
wenzelm@5014
   112
  let
wenzelm@5014
   113
    fun copy s =
wenzelm@5014
   114
      make (fn () =>
wenzelm@5014
   115
        (case pull s of
wenzelm@5014
   116
          None => pull yq
wenzelm@5014
   117
        | Some (x, s') => Some (f x, copy s')))
wenzelm@5014
   118
  in copy xq end;
wenzelm@5014
   119
wenzelm@5014
   120
(*sequence append:  put the elements of xq in front of those of yq*)
wenzelm@5014
   121
fun append (xq, yq) =
wenzelm@5014
   122
  let
wenzelm@5014
   123
    fun copy s =
wenzelm@5014
   124
      make (fn () =>
wenzelm@5014
   125
        (case pull s of
wenzelm@5014
   126
          None => pull yq
wenzelm@5014
   127
        | Some (x, s') => Some (x, copy s')))
wenzelm@5014
   128
  in copy xq end;
wenzelm@5014
   129
wenzelm@5014
   130
(*filter sequence by predicate*)
wenzelm@5014
   131
fun filter pred xq =
wenzelm@5014
   132
  let
wenzelm@5014
   133
    fun copy s =
wenzelm@5014
   134
      make (fn () =>
wenzelm@5014
   135
        (case pull s of
wenzelm@5014
   136
          None => None
wenzelm@5014
   137
        | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));
wenzelm@5014
   138
  in copy xq end;
wenzelm@5014
   139
wenzelm@5014
   140
(*flatten a sequence of sequences to a single sequence*)
wenzelm@5014
   141
fun flat xqq =
wenzelm@5014
   142
  make (fn () =>
wenzelm@5014
   143
    (case pull xqq of
wenzelm@5014
   144
      None => None
wenzelm@5014
   145
    | Some (xq, xqq') => pull (append (xq, flat xqq'))));
wenzelm@5014
   146
wenzelm@5014
   147
(*interleave elements of xq with those of yq -- fairer than append*)
wenzelm@5014
   148
fun interleave (xq, yq) =
wenzelm@5014
   149
  make (fn () =>
wenzelm@5014
   150
    (case pull xq of
wenzelm@5014
   151
      None => pull yq
wenzelm@5014
   152
    | Some (x, xq') => Some (x, interleave (yq, xq'))));
wenzelm@5014
   153
wenzelm@5014
   154
wenzelm@5014
   155
(*functional to print a sequence, up to "count" elements;
wenzelm@5014
   156
  the function prelem should print the element number and also the element*)
wenzelm@5014
   157
fun print prelem count seq =
wenzelm@5014
   158
  let
wenzelm@5014
   159
    fun pr (k, xq) =
wenzelm@5014
   160
      if k > count then ()
wenzelm@5014
   161
      else
wenzelm@5014
   162
        (case pull xq of
wenzelm@5014
   163
          None => ()
wenzelm@5014
   164
        | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
wenzelm@5014
   165
  in pr (1, seq) end;
wenzelm@5014
   166
wenzelm@5014
   167
(*accumulating a function over a sequence; this is lazy*)
wenzelm@5014
   168
fun it_right f (xq, yq) =
wenzelm@5014
   169
  let
wenzelm@5014
   170
    fun its s =
wenzelm@5014
   171
      make (fn () =>
wenzelm@5014
   172
        (case pull s of
wenzelm@5014
   173
          None => pull yq
wenzelm@5014
   174
        | Some (a, s') => pull (f (a, its s'))))
wenzelm@5014
   175
  in its xq end;
wenzelm@5014
   176
wenzelm@6927
   177
(*turn a list of sequences into a sequence of lists*)
wenzelm@6927
   178
fun commute [] = single []
wenzelm@6927
   179
  | commute (xq :: xqs) =
wenzelm@6927
   180
      make (fn () =>
wenzelm@6927
   181
        (case pull xq of
wenzelm@6927
   182
          None => None
wenzelm@6927
   183
        | Some (x, xq') =>
wenzelm@6927
   184
            (case pull (commute xqs) of
wenzelm@6927
   185
              None => None
wenzelm@6927
   186
            | Some (xs, xsq) =>
wenzelm@6927
   187
                Some (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs))))));
wenzelm@6927
   188
wenzelm@5014
   189
wenzelm@5014
   190
wenzelm@5014
   191
(** sequence functions **)      (*some code duplicated from Pure/tctical.ML*)
wenzelm@5014
   192
wenzelm@5014
   193
fun succeed x = single x;
wenzelm@5014
   194
fun fail _ = empty;
wenzelm@5014
   195
wenzelm@5014
   196
wenzelm@5864
   197
fun op THEN (f, g) x = flat (map g (f x));
wenzelm@5014
   198
wenzelm@5864
   199
fun op ORELSE (f, g) x =
wenzelm@5014
   200
  (case pull (f x) of
wenzelm@5014
   201
    None => g x
wenzelm@5014
   202
  | some => make (fn () => some));
wenzelm@5014
   203
wenzelm@5864
   204
fun op APPEND (f, g) x =
wenzelm@5014
   205
  append (f x, make (fn () => pull (g x)));
wenzelm@5014
   206
wenzelm@5014
   207
wenzelm@5014
   208
fun EVERY fs = foldr THEN (fs, succeed);
wenzelm@5014
   209
fun FIRST fs = foldr ORELSE (fs, fail);
wenzelm@5014
   210
wenzelm@5014
   211
wenzelm@5014
   212
fun TRY f = ORELSE (f, succeed);
wenzelm@5014
   213
wenzelm@5014
   214
fun REPEAT f =
wenzelm@5014
   215
  let
wenzelm@5014
   216
    fun rep qs x =
wenzelm@5014
   217
      (case pull (f x) of
wenzelm@5014
   218
        None => Some (x, make (fn () => repq qs))
wenzelm@5014
   219
      | Some (x', q) => rep (q :: qs) x')
wenzelm@5014
   220
    and repq [] = None
wenzelm@5014
   221
      | repq (q :: qs) =
wenzelm@5014
   222
          (case pull q of
wenzelm@5014
   223
            None => repq qs
wenzelm@5014
   224
          | Some (x, q) => rep (q :: qs) x);
wenzelm@5014
   225
  in fn x => make (fn () => rep [] x) end;
wenzelm@5014
   226
wenzelm@5558
   227
fun REPEAT1 f = THEN (f, REPEAT f);
wenzelm@5558
   228
wenzelm@5014
   229
wenzelm@8535
   230
fun INTERVAL f i j x =
wenzelm@8535
   231
  if i > j then single x
wenzelm@8535
   232
  else op THEN (f j, INTERVAL f i (j - 1)) x;
wenzelm@8535
   233
wenzelm@8535
   234
wenzelm@5014
   235
end;