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