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