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