src/Pure/General/lazy_seq.ML
author wenzelm
Sat, 18 Jun 2005 22:41:18 +0200
changeset 16465 eb287ce97230
parent 15663 6e6233e8cf5e
permissions -rw-r--r--
added Pure/General/ord_list.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15663
6e6233e8cf5e added header;
wenzelm
parents: 15574
diff changeset
     1
(*  Title:      Pure/General/lazy_seq.ML
6e6233e8cf5e added header;
wenzelm
parents: 15574
diff changeset
     2
    ID:         $Id$
6e6233e8cf5e added header;
wenzelm
parents: 15574
diff changeset
     3
    Author:     Sebastian Skalberg, TU Muenchen
6e6233e8cf5e added header;
wenzelm
parents: 15574
diff changeset
     4
6e6233e8cf5e added header;
wenzelm
parents: 15574
diff changeset
     5
Alternative version of lazy sequences.
6e6233e8cf5e added header;
wenzelm
parents: 15574
diff changeset
     6
*)
6e6233e8cf5e added header;
wenzelm
parents: 15574
diff changeset
     7
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     8
signature LAZY_SEQ =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     9
sig
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    10
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    11
    type 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    12
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    13
    (* From LIST *)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    14
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    15
    val null : 'a seq -> bool
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    16
    val length : 'a seq -> int
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    17
    val @ : 'a seq * 'a seq -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    18
    val hd : 'a seq -> 'a
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    19
    val tl : 'a seq -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    20
    val last : 'a seq -> 'a
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    21
    val getItem : 'a seq -> ('a * 'a seq) option
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    22
    val nth : 'a seq * int -> 'a
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    23
    val take : 'a seq * int -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    24
    val drop : 'a seq * int -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    25
    val rev : 'a seq -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    26
    val concat : 'a seq seq -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    27
    val revAppend : 'a seq * 'a seq -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    28
    val app : ('a -> unit) -> 'a seq -> unit
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    29
    val map : ('a -> 'b) -> 'a seq -> 'b seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    30
    val mapPartial : ('a -> 'b option) -> 'a seq -> 'b seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    31
    val find : ('a -> bool) -> 'a seq -> 'a option
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    32
    val filter : ('a -> bool) -> 'a seq -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    33
    val partition : ('a -> bool)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    34
                      -> 'a seq -> 'a seq * 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    35
    val foldl : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    36
    val foldr : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    37
    val exists : ('a -> bool) -> 'a seq -> bool
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    38
    val all : ('a -> bool) -> 'a seq -> bool
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    39
    val tabulate : int * (int -> 'a) -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    40
    val collate : ('a * 'a -> order)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    41
                    -> 'a seq * 'a seq -> order 
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    42
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    43
    (* Miscellaneous *)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    44
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    45
    val cycle      : ((unit ->'a seq) -> 'a seq) -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    46
    val iterates   : ('a -> 'a) -> 'a -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    47
    val of_function: (unit -> 'a option) -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    48
    val of_string  : string -> char seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    49
    val of_instream: TextIO.instream -> char seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    50
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    51
    (* From SEQ *)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    52
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    53
    val make: (unit -> ('a * 'a seq) option) -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    54
    val empty: 'a -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    55
    val cons: 'a * 'a seq -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    56
    val single: 'a -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    57
    val try: ('a -> 'b) -> 'a -> 'b seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    58
    val chop: int * 'a seq -> 'a list * 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    59
    val list_of: 'a seq -> 'a list
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    60
    val of_list: 'a list -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    61
    val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    62
    val interleave: 'a seq * 'a seq -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    63
    val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    64
    val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    65
    val commute: 'a seq list -> 'a list seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    66
    val succeed: 'a -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    67
    val fail: 'a -> 'b seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    68
    val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    69
    val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    70
    val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    71
    val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    72
    val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    73
    val TRY: ('a -> 'a seq) -> 'a -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    74
    val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    75
    val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    76
    val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    77
    val DETERM: ('a -> 'b seq) -> 'a -> 'b seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    78
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    79
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    80
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    81
structure LazySeq :> LAZY_SEQ =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    82
struct
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    83
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    84
open Susp
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    85
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    86
datatype 'a seq = Seq of ('a * 'a seq) option susp
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    87
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    88
exception Empty
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    89
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    90
fun getItem (Seq s) = force s
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    91
fun make f = Seq (delay f)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    92
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    93
fun null s = isSome (getItem s)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    94
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    95
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
    96
    fun F n NONE = n
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
    97
      | F n (SOME(_,s)) = F (n+1) (getItem s)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    98
in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    99
fun length s = F 0 (getItem s)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   100
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   101
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   102
fun s1 @ s2 =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   103
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   104
	fun F NONE = getItem s2
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   105
	  | F (SOME(x,s1')) = SOME(x,F' s1')
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   106
	and F' s = make (fn () => F (getItem s))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   107
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   108
	F' s1
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   109
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   110
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   111
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   112
    fun F NONE = raise Empty
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   113
      | F (SOME arg) = arg
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   114
in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   115
fun hd s = #1 (F (getItem s))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   116
fun tl s = #2 (F (getItem s))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   117
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   118
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   119
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   120
    fun F x NONE = x
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   121
      | F _ (SOME(x,s)) = F x (getItem s)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   122
    fun G NONE = raise Empty
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   123
      | G (SOME(x,s)) = F x (getItem s)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   124
in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   125
fun last s = G (getItem s)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   126
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   127
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   128
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   129
    fun F NONE _ = raise Subscript
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   130
      | F (SOME(x,_)) 0 = x
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   131
      | F (SOME(_,s)) n = F (getItem s) (n-1)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   132
in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   133
fun nth(s,n) =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   134
    if n < 0
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   135
    then raise Subscript
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   136
    else F (getItem s) n
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   137
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   138
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   139
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   140
    fun F NONE _ = raise Subscript
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   141
      | F (SOME(x,s)) n = SOME(x,F' s (n-1))
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   142
    and F' s 0 = Seq (value NONE)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   143
      | F' s n = make (fn () => F (getItem s) n)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   144
in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   145
fun take (s,n) =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   146
    if n < 0
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   147
    then raise Subscript
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   148
    else F' s n
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   149
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   150
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   151
local
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   152
    fun F s 0 = s
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   153
      | F NONE _ = raise Subscript
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   154
      | F (SOME(_,s)) n = F (getItem s) (n-1)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   155
in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   156
fun drop (s,0) = s
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   157
  | drop (s,n) = 
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   158
    if n < 0
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   159
    then raise Subscript
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   160
    else make (fn () => F (getItem s) n)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   161
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   162
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   163
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   164
    fun F s NONE = s
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   165
      | F s (SOME(x,s')) = F (SOME(x, Seq (value s))) (getItem s')
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   166
in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   167
fun rev s = make (fn () => F NONE (getItem s))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   168
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   169
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   170
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   171
    fun F s NONE = getItem s
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   172
      | F s (SOME(x,s')) = F (Seq (value (SOME(x,s)))) (getItem s')
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   173
in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   174
fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   175
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   176
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   177
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   178
    fun F NONE = NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   179
      | F (SOME(s1,s2)) =
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   180
	let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   181
	    fun G NONE = F (getItem s2)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   182
	      | G (SOME(x,s)) = SOME(x,make (fn () => G (getItem s)))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   183
	in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   184
	    G (getItem s1)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   185
	end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   186
in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   187
fun concat s = make (fn () => F (getItem s))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   188
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   189
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   190
fun app f =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   191
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   192
	fun F NONE = ()
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   193
	  | F (SOME(x,s)) =
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   194
	    (f x;
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   195
	     F (getItem s))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   196
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   197
	F o getItem
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   198
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   199
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   200
fun map f =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   201
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   202
	fun F NONE = NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   203
	  | F (SOME(x,s)) = SOME(f x,F' s)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   204
	and F' s = make (fn() => F (getItem s))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   205
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   206
	F'
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   207
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   208
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   209
fun mapPartial f =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   210
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   211
	fun F NONE = NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   212
	  | F (SOME(x,s)) =
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   213
	    (case f x of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   214
		 SOME y => SOME(y,F' s)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   215
	       | NONE => F (getItem s))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   216
	and F' s = make (fn()=> F (getItem s))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   217
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   218
	F'
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   219
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   220
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   221
fun find P =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   222
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   223
	fun F NONE = NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   224
	  | F (SOME(x,s)) =
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   225
	    if P x
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   226
	    then SOME x
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   227
	    else F (getItem s)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   228
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   229
	F o getItem
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   230
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   231
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   232
(*fun filter p = mapPartial (fn x => if p x then SOME x else NONE)*)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   233
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   234
fun filter P =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   235
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   236
	fun F NONE = NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   237
	  | F (SOME(x,s)) =
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   238
	    if P x
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   239
	    then SOME(x,F' s)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   240
	    else F (getItem s)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   241
	and F' s = make (fn () => F (getItem s))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   242
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   243
	F'
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   244
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   245
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   246
fun partition f s =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   247
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   248
	val s' = map (fn x => (x,f x)) s
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   249
    in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   250
	(mapPartial (fn (x,true) => SOME x | _ => NONE) s',
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   251
	 mapPartial (fn (x,false) => SOME x | _ => NONE) s')
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   252
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   253
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   254
fun exists P =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   255
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   256
	fun F NONE = false
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   257
	  | F (SOME(x,s)) = P x orelse F (getItem s)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   258
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   259
	F o getItem
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   260
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   261
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   262
fun all P =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   263
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   264
	fun F NONE = true
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   265
	  | F (SOME(x,s)) = P x andalso F (getItem s)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   266
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   267
	F o getItem
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   268
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   269
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   270
(*fun tabulate f = map f (iterates (fn x => x + 1) 0)*)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   271
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   272
fun tabulate (n,f) =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   273
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   274
	fun F n = make (fn () => SOME(f n,F (n+1)))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   275
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   276
	F n
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   277
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   279
fun collate c (s1,s2) =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   280
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   281
	fun F NONE _ = LESS
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   282
	  | F _ NONE = GREATER
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   283
	  | F (SOME(x,s1)) (SOME(y,s2)) =
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   284
	    (case c (x,y) of
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   285
		 LESS => LESS
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   286
	       | GREATER => GREATER
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   287
	       | EQUAL => F' s1 s2)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   288
	and F' s1 s2 = F (getItem s1) (getItem s2)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   289
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   290
	F' s1 s2
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   291
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   292
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   293
fun empty  _ = Seq (value NONE)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   294
fun single x = Seq(value (SOME(x,Seq (value NONE))))
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   295
fun cons a = Seq(value (SOME a))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   296
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   297
fun cycle seqfn =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   298
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   299
	val knot = ref (Seq (value NONE))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   300
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   301
	knot := seqfn (fn () => !knot);
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   302
	!knot
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   303
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   304
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   305
fun iterates f =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   306
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   307
	fun F x = make (fn() => SOME(x,F (f x)))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   308
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   309
	F
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   310
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   311
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   312
fun interleave (s1,s2) =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   313
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   314
	fun F NONE = getItem s2
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   315
	  | F (SOME(x,s1')) = SOME(x,interleave(s2,s1'))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   316
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   317
	make (fn()=> F (getItem s1))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   318
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   319
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   320
(* val force_all = app ignore *)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   321
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   322
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   323
    fun F NONE = ()
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   324
      | F (SOME(x,s)) = F (getItem s)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   325
in
15026
60240294bbd5 make SML/NJ happy;
wenzelm
parents: 14278
diff changeset
   326
fun force_all s = F (getItem s)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   327
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   328
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   329
fun of_function f =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   330
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   331
	fun F () = case f () of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   332
		       SOME x => SOME(x,make F)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   333
		     | NONE => NONE
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   334
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   335
	make F
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   336
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   337
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   338
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   339
    fun F [] = NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   340
      | F (x::xs) = SOME(x,F' xs)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   341
    and F' xs = make (fn () => F xs)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   342
in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   343
fun of_list xs = F' xs
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   344
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   345
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   346
val of_string = of_list o String.explode
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   347
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   348
fun of_instream is =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   349
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   350
	val buffer : char list ref = ref []
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   351
	fun get_input () =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   352
	    case !buffer of
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   353
		(c::cs) => (buffer:=cs;
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   354
			    SOME c)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   355
	      |	[] => (case String.explode (TextIO.input is) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   356
			   [] => NONE
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   357
			 | (c::cs) => (buffer := cs;
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   358
				       SOME c))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   359
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   360
	of_function get_input
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   361
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   362
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   363
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   364
    fun F k NONE = k []
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   365
      | F k (SOME(x,s)) = F (fn xs => k (x::xs)) (getItem s)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   366
in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   367
fun list_of s = F (fn x => x) (getItem s)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   368
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   369
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   370
(* Adapted from seq.ML *)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   371
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   372
val succeed = single
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   373
fun fail _ = Seq (value NONE)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   374
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   375
(* fun op THEN (f, g) x = flat (map g (f x)) *)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   376
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   377
fun op THEN (f, g) =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   378
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   379
	fun F NONE = NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   380
	  | F (SOME(x,xs)) =
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   381
	    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   382
		fun G NONE = F (getItem xs)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   383
		  | G (SOME(y,ys)) = SOME(y,make (fn () => G (getItem ys)))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   384
	    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   385
		G (getItem (g x))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   386
	    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   387
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   388
	fn x => make (fn () => F (getItem (f x)))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   389
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   390
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   391
fun op ORELSE (f, g) x =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   392
    make (fn () =>
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   393
	     case getItem (f x) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   394
		 NONE => getItem (g x)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   395
	       | some => some)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   396
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   397
fun op APPEND (f, g) x =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   398
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   399
	fun copy s =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   400
	    case getItem s of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   401
		NONE => getItem (g x)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   402
	      | SOME(x,xs) => SOME(x,make (fn () => copy xs))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   403
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   404
	make (fn () => copy (f x))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   405
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   406
15574
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   407
fun EVERY fs = foldr THEN succeed fs
b1d1b5bfc464 Removed practically all references to Library.foldr.
skalberg
parents: 15570
diff changeset
   408
fun FIRST fs = foldr ORELSE fail fs
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   409
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   410
fun TRY f x =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   411
    make (fn () =>
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   412
	     case getItem (f x) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   413
		 NONE => SOME(x,Seq (value NONE))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   414
	       | some => some)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   415
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   416
fun REPEAT f =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   417
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   418
	fun rep qs x =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   419
	    case getItem (f x) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   420
		NONE => SOME(x, make (fn () => repq qs))
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   421
	      | SOME (x', q) => rep (q :: qs) x'
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   422
	and repq [] = NONE
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   423
	  | repq (q :: qs) =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   424
            case getItem q of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   425
		NONE => repq qs
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   426
              | SOME (x, q) => rep (q :: qs) x
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   427
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   428
     fn x => make (fn () => rep [] x)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   429
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   430
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   431
fun REPEAT1 f = THEN (f, REPEAT f);
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   432
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   433
fun INTERVAL f i =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   434
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   435
	fun F j =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   436
	    if i > j
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   437
	    then single
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   438
	    else op THEN (f j, F (j - 1))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   439
    in F end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   440
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   441
fun DETERM f x =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   442
    make (fn () =>
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   443
	     case getItem (f x) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   444
		 NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   445
	       | SOME (x', _) => SOME(x',Seq (value NONE)))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   446
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   447
(*partial function as procedure*)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   448
fun try f x =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   449
    make (fn () =>
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   450
	     case Library.try f x of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   451
		 SOME y => SOME(y,Seq (value NONE))
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   452
	       | NONE => NONE)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   453
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   454
(*functional to print a sequence, up to "count" elements;
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   455
  the function prelem should print the element number and also the element*)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   456
fun print prelem count seq =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   457
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   458
	fun pr k xq =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   459
	    if k > count
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   460
	    then ()
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   461
	    else
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   462
		case getItem xq of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   463
		    NONE => ()
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   464
		  | SOME (x, xq') =>
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   465
		    (prelem k x;
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   466
		     writeln "";
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   467
		     pr (k + 1) xq')
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   468
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   469
	pr 1 seq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   470
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   471
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   472
(*accumulating a function over a sequence; this is lazy*)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   473
fun it_right f (xq, yq) =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   474
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   475
	fun its s =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   476
	    make (fn () =>
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   477
		     case getItem s of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   478
			 NONE => getItem yq
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   479
		       | SOME (a, s') => getItem(f (a, its s')))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   480
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   481
	its xq
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   482
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   483
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   484
(*map over a sequence s1, append the sequence s2*)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   485
fun mapp f s1 s2 =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   486
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   487
	fun F NONE = getItem s2
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   488
	  | F (SOME(x,s1')) = SOME(f x,F' s1')
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   489
	and F' s = make (fn () => F (getItem s))
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   490
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   491
	F' s1
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   492
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   493
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   494
(*turn a list of sequences into a sequence of lists*)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   495
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   496
    fun F [] = SOME([],Seq (value NONE))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   497
      | F (xq :: xqs) =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   498
        case getItem xq of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   499
            NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   500
          | SOME (x, xq') =>
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   501
            (case F xqs of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   502
		 NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   503
	       | SOME (xs, xsq) =>
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   504
		 let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   505
		     fun G s =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   506
			 make (fn () =>
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   507
				  case getItem s of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   508
				      NONE => F (xq' :: xqs)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   509
				    | SOME(ys,ysq) => SOME(x::ys,G ysq))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   510
		 in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   511
		     SOME (x :: xs, G xsq)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   512
		 end)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   513
in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   514
fun commute xqs = make (fn () => F xqs)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   515
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   516
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   517
(*the list of the first n elements, paired with rest of sequence;
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   518
  if length of list is less than n, then sequence had less than n elements*)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   519
fun chop (n, xq) =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   520
    if n <= 0
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   521
    then ([], xq)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   522
    else
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   523
	case getItem xq of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   524
	    NONE => ([], xq)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   525
	  | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   526
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   527
fun foldl f e s =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   528
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   529
	fun F k NONE = k e
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   530
	  | F k (SOME(x,s)) = F (fn y => k (f(x,y))) (getItem s)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   531
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   532
	F (fn x => x) (getItem s)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   533
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   534
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   535
fun foldr f e s =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   536
    let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   537
	fun F e NONE = e
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15026
diff changeset
   538
	  | F e (SOME(x,s)) = F (f(x,e)) (getItem s)
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   539
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   540
	F e (getItem s)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   541
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   542
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
   543
end