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