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