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