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