moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
authorwenzelm
Sat Oct 08 22:39:40 2005 +0200 (2005-10-08)
changeset 17802f3b1ca16cebd
parent 17801 30cbd2685e73
child 17803 e235a57651a1
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
src/HOL/Import/lazy_scan.ML
src/HOL/Import/lazy_seq.ML
src/HOL/Import/susp.ML
src/Pure/General/ROOT.ML
src/Pure/General/lazy_scan.ML
src/Pure/General/lazy_seq.ML
src/Pure/General/susp.ML
src/Pure/IsaMakefile
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Import/lazy_scan.ML	Sat Oct 08 22:39:40 2005 +0200
     1.3 @@ -0,0 +1,206 @@
     1.4 +(*  Title:      HOL/Import/lazy_scan.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Sebastian Skalberg, TU Muenchen
     1.7 +
     1.8 +Scanner combinators for lazy sequences.
     1.9 +*)
    1.10 +
    1.11 +signature LAZY_SCAN =
    1.12 +sig
    1.13 +
    1.14 +    exception SyntaxError
    1.15 +
    1.16 +    type ('a,'b) scanner = 'a LazySeq.seq -> 'b * 'a LazySeq.seq
    1.17 +
    1.18 +    val :--      : ('a,'b) scanner * ('b -> ('a,'c) scanner)
    1.19 +		   -> ('a,'b*'c) scanner
    1.20 +    val --       : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b*'c) scanner
    1.21 +    val >>       : ('a,'b) scanner * ('b -> 'c) -> ('a,'c) scanner
    1.22 +    val --|      : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b) scanner
    1.23 +    val |--      : ('a,'b) scanner * ('a,'c) scanner -> ('a,'c) scanner
    1.24 +    val ^^       : ('a,string) scanner * ('a,string) scanner
    1.25 +		   -> ('a,string) scanner
    1.26 +    val ||       : ('a,'b) scanner * ('a,'b) scanner -> ('a,'b) scanner
    1.27 +    val one      : ('a -> bool) -> ('a,'a) scanner
    1.28 +    val succeed  : 'b -> ('a,'b) scanner
    1.29 +    val any      : ('a -> bool) -> ('a,'a list) scanner
    1.30 +    val any1     : ('a -> bool) -> ('a,'a list) scanner
    1.31 +    val optional : ('a,'b) scanner -> 'b -> ('a,'b) scanner
    1.32 +    val option   : ('a,'b) scanner -> ('a,'b option) scanner
    1.33 +    val repeat   : ('a,'b) scanner -> ('a,'b list) scanner
    1.34 +    val repeat1  : ('a,'b) scanner -> ('a,'b list) scanner
    1.35 +    val ahead    : ('a,'b) scanner -> ('a,'b) scanner
    1.36 +    val unless   : ('a LazySeq.seq -> bool) -> ('a,'b) scanner -> ('a,'b) scanner
    1.37 +    val $$       : ''a -> (''a,''a) scanner
    1.38 +    val !!       : ('a LazySeq.seq -> string) -> ('a,'b) scanner -> ('a,'b) scanner
    1.39 +    val scan_full: ('a,'b) scanner -> 'a LazySeq.seq -> 'b LazySeq.seq
    1.40 +
    1.41 +end
    1.42 +
    1.43 +structure LazyScan :> LAZY_SCAN =
    1.44 +struct
    1.45 +
    1.46 +infix 7 |-- --|
    1.47 +infix 5 :-- -- ^^
    1.48 +infix 3 >>
    1.49 +infix 0 ||
    1.50 +
    1.51 +exception SyntaxError
    1.52 +exception Fail of string
    1.53 +
    1.54 +type ('a,'b) scanner = 'a LazySeq.seq -> 'b * 'a LazySeq.seq
    1.55 +
    1.56 +fun (sc1 :-- sc2) toks =
    1.57 +    let
    1.58 +	val (x,toks2) = sc1 toks
    1.59 +	val (y,toks3) = sc2 x toks2
    1.60 +    in
    1.61 +	((x,y),toks3)
    1.62 +    end
    1.63 +
    1.64 +fun (sc1 -- sc2) toks =
    1.65 +    let
    1.66 +	val (x,toks2) = sc1 toks
    1.67 +	val (y,toks3) = sc2 toks2
    1.68 +    in
    1.69 +	((x,y),toks3)
    1.70 +    end
    1.71 +
    1.72 +fun (sc >> f) toks =
    1.73 +    let
    1.74 +	val (x,toks2) = sc toks
    1.75 +    in
    1.76 +	(f x,toks2)
    1.77 +    end
    1.78 +
    1.79 +fun (sc1 --| sc2) toks =
    1.80 +    let
    1.81 +	val (x,toks2) = sc1 toks
    1.82 +	val (_,toks3) = sc2 toks2
    1.83 +    in
    1.84 +	(x,toks3)
    1.85 +    end
    1.86 +
    1.87 +fun (sc1 |-- sc2) toks =
    1.88 +    let
    1.89 +	val (_,toks2) = sc1 toks
    1.90 +    in
    1.91 +	sc2 toks2
    1.92 +    end
    1.93 +
    1.94 +fun (sc1 ^^ sc2) toks =
    1.95 +    let
    1.96 +	val (x,toks2) = sc1 toks
    1.97 +	val (y,toks3) = sc2 toks2
    1.98 +    in
    1.99 +	(x^y,toks3)
   1.100 +    end
   1.101 +
   1.102 +fun (sc1 || sc2) toks =
   1.103 +    (sc1 toks)
   1.104 +    handle SyntaxError => sc2 toks
   1.105 +
   1.106 +fun one p toks =
   1.107 +    case LazySeq.getItem toks of
   1.108 +	NONE => raise SyntaxError
   1.109 +      | SOME(t,toks) => if p t
   1.110 +			then (t,toks)
   1.111 +			else raise SyntaxError
   1.112 +
   1.113 +fun succeed e toks = (e,toks)
   1.114 +
   1.115 +fun any p toks =
   1.116 +    case LazySeq.getItem toks of
   1.117 +	NONE =>  ([],toks)
   1.118 +      | SOME(x,toks2) => if p x
   1.119 +			 then
   1.120 +			     let
   1.121 +				 val (xs,toks3) = any p toks2
   1.122 +			     in
   1.123 +				 (x::xs,toks3)
   1.124 +			     end
   1.125 +			 else ([],toks)
   1.126 +
   1.127 +fun any1 p toks =
   1.128 +    let
   1.129 +	val (x,toks2) = one p toks
   1.130 +	val (xs,toks3) = any p toks2
   1.131 +    in
   1.132 +	(x::xs,toks3)
   1.133 +    end
   1.134 +
   1.135 +fun optional sc def =  sc || succeed def
   1.136 +fun option sc = (sc >> SOME) || succeed NONE
   1.137 +
   1.138 +(*
   1.139 +fun repeat sc =
   1.140 +    let
   1.141 +	fun R toks =
   1.142 +	    let
   1.143 +		val (x,toks2) = sc toks
   1.144 +		val (xs,toks3) = R toks2
   1.145 +	    in
   1.146 +		(x::xs,toks3)
   1.147 +	    end
   1.148 +	    handle SyntaxError => ([],toks)
   1.149 +    in
   1.150 +	R
   1.151 +    end
   1.152 +*)
   1.153 +
   1.154 +(* A tail-recursive version of repeat.  It is (ever so) slightly slower
   1.155 + * than the above, non-tail-recursive version (due to the garbage generation
   1.156 + * associated with the reversal of the list).  However,  this version will be
   1.157 + * able to process input where the former version must give up (due to stack
   1.158 + * overflow).  The slowdown seems to be around the one percent mark.
   1.159 + *)
   1.160 +fun repeat sc =
   1.161 +    let
   1.162 +	fun R xs toks =
   1.163 +	    case SOME (sc toks) handle SyntaxError => NONE of
   1.164 +		SOME (x,toks2) => R (x::xs) toks2
   1.165 +	      | NONE => (List.rev xs,toks)
   1.166 +    in
   1.167 +	R []
   1.168 +    end
   1.169 +
   1.170 +fun repeat1 sc toks =
   1.171 +    let
   1.172 +	val (x,toks2) = sc toks
   1.173 +	val (xs,toks3) = repeat sc toks2
   1.174 +    in
   1.175 +	(x::xs,toks3)
   1.176 +    end
   1.177 +
   1.178 +fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks)
   1.179 +
   1.180 +fun unless test sc toks =
   1.181 +    let
   1.182 +	val test_failed = (test toks;false) handle SyntaxError => true
   1.183 +    in
   1.184 +	if test_failed
   1.185 +	then sc toks
   1.186 +	else raise SyntaxError
   1.187 +    end
   1.188 +
   1.189 +fun $$ arg = one (fn x => x = arg)
   1.190 +
   1.191 +fun !! f sc toks = (sc toks
   1.192 +		    handle SyntaxError => raise Fail (f toks))
   1.193 +
   1.194 +fun scan_full sc toks =
   1.195 +    let
   1.196 +	fun F toks =
   1.197 +	    if LazySeq.null toks
   1.198 +	    then NONE
   1.199 +	    else
   1.200 +		let
   1.201 +		    val (x,toks') = sc toks
   1.202 +		in
   1.203 +		    SOME(x,LazySeq.make (fn () => F toks'))
   1.204 +		end
   1.205 +    in
   1.206 +	LazySeq.make (fn () => F toks)
   1.207 +    end
   1.208 +
   1.209 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Import/lazy_seq.ML	Sat Oct 08 22:39:40 2005 +0200
     2.3 @@ -0,0 +1,543 @@
     2.4 +(*  Title:      HOL/Import/lazy_seq.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Sebastian Skalberg, TU Muenchen
     2.7 +
     2.8 +Alternative version of lazy sequences.
     2.9 +*)
    2.10 +
    2.11 +signature LAZY_SEQ =
    2.12 +sig
    2.13 +
    2.14 +    type 'a seq
    2.15 +
    2.16 +    (* From LIST *)
    2.17 +
    2.18 +    val null : 'a seq -> bool
    2.19 +    val length : 'a seq -> int
    2.20 +    val @ : 'a seq * 'a seq -> 'a seq
    2.21 +    val hd : 'a seq -> 'a
    2.22 +    val tl : 'a seq -> 'a seq
    2.23 +    val last : 'a seq -> 'a
    2.24 +    val getItem : 'a seq -> ('a * 'a seq) option
    2.25 +    val nth : 'a seq * int -> 'a
    2.26 +    val take : 'a seq * int -> 'a seq
    2.27 +    val drop : 'a seq * int -> 'a seq
    2.28 +    val rev : 'a seq -> 'a seq
    2.29 +    val concat : 'a seq seq -> 'a seq
    2.30 +    val revAppend : 'a seq * 'a seq -> 'a seq
    2.31 +    val app : ('a -> unit) -> 'a seq -> unit
    2.32 +    val map : ('a -> 'b) -> 'a seq -> 'b seq
    2.33 +    val mapPartial : ('a -> 'b option) -> 'a seq -> 'b seq
    2.34 +    val find : ('a -> bool) -> 'a seq -> 'a option
    2.35 +    val filter : ('a -> bool) -> 'a seq -> 'a seq
    2.36 +    val partition : ('a -> bool)
    2.37 +                      -> 'a seq -> 'a seq * 'a seq
    2.38 +    val foldl : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
    2.39 +    val foldr : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
    2.40 +    val exists : ('a -> bool) -> 'a seq -> bool
    2.41 +    val all : ('a -> bool) -> 'a seq -> bool
    2.42 +    val tabulate : int * (int -> 'a) -> 'a seq
    2.43 +    val collate : ('a * 'a -> order)
    2.44 +                    -> 'a seq * 'a seq -> order 
    2.45 +
    2.46 +    (* Miscellaneous *)
    2.47 +
    2.48 +    val cycle      : ((unit ->'a seq) -> 'a seq) -> 'a seq
    2.49 +    val iterates   : ('a -> 'a) -> 'a -> 'a seq
    2.50 +    val of_function: (unit -> 'a option) -> 'a seq
    2.51 +    val of_string  : string -> char seq
    2.52 +    val of_instream: TextIO.instream -> char seq
    2.53 +
    2.54 +    (* From SEQ *)
    2.55 +
    2.56 +    val make: (unit -> ('a * 'a seq) option) -> 'a seq
    2.57 +    val empty: 'a -> 'a seq
    2.58 +    val cons: 'a * 'a seq -> 'a seq
    2.59 +    val single: 'a -> 'a seq
    2.60 +    val try: ('a -> 'b) -> 'a -> 'b seq
    2.61 +    val chop: int * 'a seq -> 'a list * 'a seq
    2.62 +    val list_of: 'a seq -> 'a list
    2.63 +    val of_list: 'a list -> 'a seq
    2.64 +    val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
    2.65 +    val interleave: 'a seq * 'a seq -> 'a seq
    2.66 +    val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
    2.67 +    val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    2.68 +    val commute: 'a seq list -> 'a list seq
    2.69 +    val succeed: 'a -> 'a seq
    2.70 +    val fail: 'a -> 'b seq
    2.71 +    val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
    2.72 +    val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
    2.73 +    val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
    2.74 +    val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
    2.75 +    val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
    2.76 +    val TRY: ('a -> 'a seq) -> 'a -> 'a seq
    2.77 +    val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
    2.78 +    val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
    2.79 +    val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
    2.80 +    val DETERM: ('a -> 'b seq) -> 'a -> 'b seq
    2.81 +
    2.82 +end
    2.83 +
    2.84 +structure LazySeq :> LAZY_SEQ =
    2.85 +struct
    2.86 +
    2.87 +open Susp
    2.88 +
    2.89 +datatype 'a seq = Seq of ('a * 'a seq) option susp
    2.90 +
    2.91 +exception Empty
    2.92 +
    2.93 +fun getItem (Seq s) = force s
    2.94 +fun make f = Seq (delay f)
    2.95 +
    2.96 +fun null s = isSome (getItem s)
    2.97 +
    2.98 +local
    2.99 +    fun F n NONE = n
   2.100 +      | F n (SOME(_,s)) = F (n+1) (getItem s)
   2.101 +in
   2.102 +fun length s = F 0 (getItem s)
   2.103 +end
   2.104 +
   2.105 +fun s1 @ s2 =
   2.106 +    let
   2.107 +	fun F NONE = getItem s2
   2.108 +	  | F (SOME(x,s1')) = SOME(x,F' s1')
   2.109 +	and F' s = make (fn () => F (getItem s))
   2.110 +    in
   2.111 +	F' s1
   2.112 +    end
   2.113 +
   2.114 +local
   2.115 +    fun F NONE = raise Empty
   2.116 +      | F (SOME arg) = arg
   2.117 +in
   2.118 +fun hd s = #1 (F (getItem s))
   2.119 +fun tl s = #2 (F (getItem s))
   2.120 +end
   2.121 +
   2.122 +local
   2.123 +    fun F x NONE = x
   2.124 +      | F _ (SOME(x,s)) = F x (getItem s)
   2.125 +    fun G NONE = raise Empty
   2.126 +      | G (SOME(x,s)) = F x (getItem s)
   2.127 +in
   2.128 +fun last s = G (getItem s)
   2.129 +end
   2.130 +
   2.131 +local
   2.132 +    fun F NONE _ = raise Subscript
   2.133 +      | F (SOME(x,_)) 0 = x
   2.134 +      | F (SOME(_,s)) n = F (getItem s) (n-1)
   2.135 +in
   2.136 +fun nth(s,n) =
   2.137 +    if n < 0
   2.138 +    then raise Subscript
   2.139 +    else F (getItem s) n
   2.140 +end
   2.141 +
   2.142 +local
   2.143 +    fun F NONE _ = raise Subscript
   2.144 +      | F (SOME(x,s)) n = SOME(x,F' s (n-1))
   2.145 +    and F' s 0 = Seq (value NONE)
   2.146 +      | F' s n = make (fn () => F (getItem s) n)
   2.147 +in
   2.148 +fun take (s,n) =
   2.149 +    if n < 0
   2.150 +    then raise Subscript
   2.151 +    else F' s n
   2.152 +end
   2.153 +
   2.154 +local
   2.155 +    fun F s 0 = s
   2.156 +      | F NONE _ = raise Subscript
   2.157 +      | F (SOME(_,s)) n = F (getItem s) (n-1)
   2.158 +in
   2.159 +fun drop (s,0) = s
   2.160 +  | drop (s,n) = 
   2.161 +    if n < 0
   2.162 +    then raise Subscript
   2.163 +    else make (fn () => F (getItem s) n)
   2.164 +end
   2.165 +
   2.166 +local
   2.167 +    fun F s NONE = s
   2.168 +      | F s (SOME(x,s')) = F (SOME(x, Seq (value s))) (getItem s')
   2.169 +in
   2.170 +fun rev s = make (fn () => F NONE (getItem s))
   2.171 +end
   2.172 +
   2.173 +local
   2.174 +    fun F s NONE = getItem s
   2.175 +      | F s (SOME(x,s')) = F (Seq (value (SOME(x,s)))) (getItem s')
   2.176 +in
   2.177 +fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
   2.178 +end
   2.179 +
   2.180 +local
   2.181 +    fun F NONE = NONE
   2.182 +      | F (SOME(s1,s2)) =
   2.183 +	let
   2.184 +	    fun G NONE = F (getItem s2)
   2.185 +	      | G (SOME(x,s)) = SOME(x,make (fn () => G (getItem s)))
   2.186 +	in
   2.187 +	    G (getItem s1)
   2.188 +	end
   2.189 +in
   2.190 +fun concat s = make (fn () => F (getItem s))
   2.191 +end
   2.192 +
   2.193 +fun app f =
   2.194 +    let
   2.195 +	fun F NONE = ()
   2.196 +	  | F (SOME(x,s)) =
   2.197 +	    (f x;
   2.198 +	     F (getItem s))
   2.199 +    in
   2.200 +	F o getItem
   2.201 +    end
   2.202 +
   2.203 +fun map f =
   2.204 +    let
   2.205 +	fun F NONE = NONE
   2.206 +	  | F (SOME(x,s)) = SOME(f x,F' s)
   2.207 +	and F' s = make (fn() => F (getItem s))
   2.208 +    in
   2.209 +	F'
   2.210 +    end
   2.211 +
   2.212 +fun mapPartial f =
   2.213 +    let
   2.214 +	fun F NONE = NONE
   2.215 +	  | F (SOME(x,s)) =
   2.216 +	    (case f x of
   2.217 +		 SOME y => SOME(y,F' s)
   2.218 +	       | NONE => F (getItem s))
   2.219 +	and F' s = make (fn()=> F (getItem s))
   2.220 +    in
   2.221 +	F'
   2.222 +    end
   2.223 +
   2.224 +fun find P =
   2.225 +    let
   2.226 +	fun F NONE = NONE
   2.227 +	  | F (SOME(x,s)) =
   2.228 +	    if P x
   2.229 +	    then SOME x
   2.230 +	    else F (getItem s)
   2.231 +    in
   2.232 +	F o getItem
   2.233 +    end
   2.234 +
   2.235 +(*fun filter p = mapPartial (fn x => if p x then SOME x else NONE)*)
   2.236 +
   2.237 +fun filter P =
   2.238 +    let
   2.239 +	fun F NONE = NONE
   2.240 +	  | F (SOME(x,s)) =
   2.241 +	    if P x
   2.242 +	    then SOME(x,F' s)
   2.243 +	    else F (getItem s)
   2.244 +	and F' s = make (fn () => F (getItem s))
   2.245 +    in
   2.246 +	F'
   2.247 +    end
   2.248 +
   2.249 +fun partition f s =
   2.250 +    let
   2.251 +	val s' = map (fn x => (x,f x)) s
   2.252 +    in
   2.253 +	(mapPartial (fn (x,true) => SOME x | _ => NONE) s',
   2.254 +	 mapPartial (fn (x,false) => SOME x | _ => NONE) s')
   2.255 +    end
   2.256 +
   2.257 +fun exists P =
   2.258 +    let
   2.259 +	fun F NONE = false
   2.260 +	  | F (SOME(x,s)) = P x orelse F (getItem s)
   2.261 +    in
   2.262 +	F o getItem
   2.263 +    end
   2.264 +
   2.265 +fun all P =
   2.266 +    let
   2.267 +	fun F NONE = true
   2.268 +	  | F (SOME(x,s)) = P x andalso F (getItem s)
   2.269 +    in
   2.270 +	F o getItem
   2.271 +    end
   2.272 +
   2.273 +(*fun tabulate f = map f (iterates (fn x => x + 1) 0)*)
   2.274 +
   2.275 +fun tabulate (n,f) =
   2.276 +    let
   2.277 +	fun F n = make (fn () => SOME(f n,F (n+1)))
   2.278 +    in
   2.279 +	F n
   2.280 +    end
   2.281 +
   2.282 +fun collate c (s1,s2) =
   2.283 +    let
   2.284 +	fun F NONE _ = LESS
   2.285 +	  | F _ NONE = GREATER
   2.286 +	  | F (SOME(x,s1)) (SOME(y,s2)) =
   2.287 +	    (case c (x,y) of
   2.288 +		 LESS => LESS
   2.289 +	       | GREATER => GREATER
   2.290 +	       | EQUAL => F' s1 s2)
   2.291 +	and F' s1 s2 = F (getItem s1) (getItem s2)
   2.292 +    in
   2.293 +	F' s1 s2
   2.294 +    end
   2.295 +
   2.296 +fun empty  _ = Seq (value NONE)
   2.297 +fun single x = Seq(value (SOME(x,Seq (value NONE))))
   2.298 +fun cons a = Seq(value (SOME a))
   2.299 +
   2.300 +fun cycle seqfn =
   2.301 +    let
   2.302 +	val knot = ref (Seq (value NONE))
   2.303 +    in
   2.304 +	knot := seqfn (fn () => !knot);
   2.305 +	!knot
   2.306 +    end
   2.307 +
   2.308 +fun iterates f =
   2.309 +    let
   2.310 +	fun F x = make (fn() => SOME(x,F (f x)))
   2.311 +    in
   2.312 +	F
   2.313 +    end
   2.314 +
   2.315 +fun interleave (s1,s2) =
   2.316 +    let
   2.317 +	fun F NONE = getItem s2
   2.318 +	  | F (SOME(x,s1')) = SOME(x,interleave(s2,s1'))
   2.319 +    in
   2.320 +	make (fn()=> F (getItem s1))
   2.321 +    end
   2.322 +
   2.323 +(* val force_all = app ignore *)
   2.324 +
   2.325 +local
   2.326 +    fun F NONE = ()
   2.327 +      | F (SOME(x,s)) = F (getItem s)
   2.328 +in
   2.329 +fun force_all s = F (getItem s)
   2.330 +end
   2.331 +
   2.332 +fun of_function f =
   2.333 +    let
   2.334 +	fun F () = case f () of
   2.335 +		       SOME x => SOME(x,make F)
   2.336 +		     | NONE => NONE
   2.337 +    in
   2.338 +	make F
   2.339 +    end
   2.340 +
   2.341 +local
   2.342 +    fun F [] = NONE
   2.343 +      | F (x::xs) = SOME(x,F' xs)
   2.344 +    and F' xs = make (fn () => F xs)
   2.345 +in
   2.346 +fun of_list xs = F' xs
   2.347 +end
   2.348 +
   2.349 +val of_string = of_list o String.explode
   2.350 +
   2.351 +fun of_instream is =
   2.352 +    let
   2.353 +	val buffer : char list ref = ref []
   2.354 +	fun get_input () =
   2.355 +	    case !buffer of
   2.356 +		(c::cs) => (buffer:=cs;
   2.357 +			    SOME c)
   2.358 +	      |	[] => (case String.explode (TextIO.input is) of
   2.359 +			   [] => NONE
   2.360 +			 | (c::cs) => (buffer := cs;
   2.361 +				       SOME c))
   2.362 +    in
   2.363 +	of_function get_input
   2.364 +    end
   2.365 +
   2.366 +local
   2.367 +    fun F k NONE = k []
   2.368 +      | F k (SOME(x,s)) = F (fn xs => k (x::xs)) (getItem s)
   2.369 +in
   2.370 +fun list_of s = F (fn x => x) (getItem s)
   2.371 +end
   2.372 +
   2.373 +(* Adapted from seq.ML *)
   2.374 +
   2.375 +val succeed = single
   2.376 +fun fail _ = Seq (value NONE)
   2.377 +
   2.378 +(* fun op THEN (f, g) x = flat (map g (f x)) *)
   2.379 +
   2.380 +fun op THEN (f, g) =
   2.381 +    let
   2.382 +	fun F NONE = NONE
   2.383 +	  | F (SOME(x,xs)) =
   2.384 +	    let
   2.385 +		fun G NONE = F (getItem xs)
   2.386 +		  | G (SOME(y,ys)) = SOME(y,make (fn () => G (getItem ys)))
   2.387 +	    in
   2.388 +		G (getItem (g x))
   2.389 +	    end
   2.390 +    in
   2.391 +	fn x => make (fn () => F (getItem (f x)))
   2.392 +    end
   2.393 +
   2.394 +fun op ORELSE (f, g) x =
   2.395 +    make (fn () =>
   2.396 +	     case getItem (f x) of
   2.397 +		 NONE => getItem (g x)
   2.398 +	       | some => some)
   2.399 +
   2.400 +fun op APPEND (f, g) x =
   2.401 +    let
   2.402 +	fun copy s =
   2.403 +	    case getItem s of
   2.404 +		NONE => getItem (g x)
   2.405 +	      | SOME(x,xs) => SOME(x,make (fn () => copy xs))
   2.406 +    in
   2.407 +	make (fn () => copy (f x))
   2.408 +    end
   2.409 +
   2.410 +fun EVERY fs = foldr (op THEN) succeed fs
   2.411 +fun FIRST fs = foldr (op ORELSE) fail fs
   2.412 +
   2.413 +fun TRY f x =
   2.414 +    make (fn () =>
   2.415 +	     case getItem (f x) of
   2.416 +		 NONE => SOME(x,Seq (value NONE))
   2.417 +	       | some => some)
   2.418 +
   2.419 +fun REPEAT f =
   2.420 +    let
   2.421 +	fun rep qs x =
   2.422 +	    case getItem (f x) of
   2.423 +		NONE => SOME(x, make (fn () => repq qs))
   2.424 +	      | SOME (x', q) => rep (q :: qs) x'
   2.425 +	and repq [] = NONE
   2.426 +	  | repq (q :: qs) =
   2.427 +            case getItem q of
   2.428 +		NONE => repq qs
   2.429 +              | SOME (x, q) => rep (q :: qs) x
   2.430 +    in
   2.431 +     fn x => make (fn () => rep [] x)
   2.432 +    end
   2.433 +
   2.434 +fun REPEAT1 f = op THEN (f, REPEAT f);
   2.435 +
   2.436 +fun INTERVAL f i =
   2.437 +    let
   2.438 +	fun F j =
   2.439 +	    if i > j
   2.440 +	    then single
   2.441 +	    else op THEN (f j, F (j - 1))
   2.442 +    in F end
   2.443 +
   2.444 +fun DETERM f x =
   2.445 +    make (fn () =>
   2.446 +	     case getItem (f x) of
   2.447 +		 NONE => NONE
   2.448 +	       | SOME (x', _) => SOME(x',Seq (value NONE)))
   2.449 +
   2.450 +(*partial function as procedure*)
   2.451 +fun try f x =
   2.452 +    make (fn () =>
   2.453 +	     case Library.try f x of
   2.454 +		 SOME y => SOME(y,Seq (value NONE))
   2.455 +	       | NONE => NONE)
   2.456 +
   2.457 +(*functional to print a sequence, up to "count" elements;
   2.458 +  the function prelem should print the element number and also the element*)
   2.459 +fun print prelem count seq =
   2.460 +    let
   2.461 +	fun pr k xq =
   2.462 +	    if k > count
   2.463 +	    then ()
   2.464 +	    else
   2.465 +		case getItem xq of
   2.466 +		    NONE => ()
   2.467 +		  | SOME (x, xq') =>
   2.468 +		    (prelem k x;
   2.469 +		     writeln "";
   2.470 +		     pr (k + 1) xq')
   2.471 +    in
   2.472 +	pr 1 seq
   2.473 +    end
   2.474 +
   2.475 +(*accumulating a function over a sequence; this is lazy*)
   2.476 +fun it_right f (xq, yq) =
   2.477 +    let
   2.478 +	fun its s =
   2.479 +	    make (fn () =>
   2.480 +		     case getItem s of
   2.481 +			 NONE => getItem yq
   2.482 +		       | SOME (a, s') => getItem(f (a, its s')))
   2.483 +    in
   2.484 +	its xq
   2.485 +    end
   2.486 +
   2.487 +(*map over a sequence s1, append the sequence s2*)
   2.488 +fun mapp f s1 s2 =
   2.489 +    let
   2.490 +	fun F NONE = getItem s2
   2.491 +	  | F (SOME(x,s1')) = SOME(f x,F' s1')
   2.492 +	and F' s = make (fn () => F (getItem s))
   2.493 +    in
   2.494 +	F' s1
   2.495 +    end
   2.496 +
   2.497 +(*turn a list of sequences into a sequence of lists*)
   2.498 +local
   2.499 +    fun F [] = SOME([],Seq (value NONE))
   2.500 +      | F (xq :: xqs) =
   2.501 +        case getItem xq of
   2.502 +            NONE => NONE
   2.503 +          | SOME (x, xq') =>
   2.504 +            (case F xqs of
   2.505 +		 NONE => NONE
   2.506 +	       | SOME (xs, xsq) =>
   2.507 +		 let
   2.508 +		     fun G s =
   2.509 +			 make (fn () =>
   2.510 +				  case getItem s of
   2.511 +				      NONE => F (xq' :: xqs)
   2.512 +				    | SOME(ys,ysq) => SOME(x::ys,G ysq))
   2.513 +		 in
   2.514 +		     SOME (x :: xs, G xsq)
   2.515 +		 end)
   2.516 +in
   2.517 +fun commute xqs = make (fn () => F xqs)
   2.518 +end
   2.519 +
   2.520 +(*the list of the first n elements, paired with rest of sequence;
   2.521 +  if length of list is less than n, then sequence had less than n elements*)
   2.522 +fun chop (n, xq) =
   2.523 +    if n <= 0
   2.524 +    then ([], xq)
   2.525 +    else
   2.526 +	case getItem xq of
   2.527 +	    NONE => ([], xq)
   2.528 +	  | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))
   2.529 +
   2.530 +fun foldl f e s =
   2.531 +    let
   2.532 +	fun F k NONE = k e
   2.533 +	  | F k (SOME(x,s)) = F (fn y => k (f(x,y))) (getItem s)
   2.534 +    in
   2.535 +	F (fn x => x) (getItem s)
   2.536 +    end
   2.537 +
   2.538 +fun foldr f e s =
   2.539 +    let
   2.540 +	fun F e NONE = e
   2.541 +	  | F e (SOME(x,s)) = F (f(x,e)) (getItem s)
   2.542 +    in
   2.543 +	F e (getItem s)
   2.544 +    end
   2.545 +
   2.546 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Import/susp.ML	Sat Oct 08 22:39:40 2005 +0200
     3.3 @@ -0,0 +1,41 @@
     3.4 +(*  Title:      HOL/Import/susp.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Sebastian Skalberg, TU Muenchen
     3.7 +
     3.8 +Delayed evaluation.
     3.9 +*)
    3.10 +
    3.11 +signature SUSP =
    3.12 +sig
    3.13 +
    3.14 +type 'a susp
    3.15 +
    3.16 +val force : 'a susp -> 'a
    3.17 +val delay : (unit -> 'a) -> 'a susp
    3.18 +val value : 'a -> 'a susp
    3.19 +
    3.20 +end
    3.21 +
    3.22 +structure Susp :> SUSP =
    3.23 +struct
    3.24 +
    3.25 +datatype 'a suspVal
    3.26 +  = Value of 'a
    3.27 +  | Delay of unit -> 'a
    3.28 +
    3.29 +type 'a susp = 'a suspVal ref
    3.30 +
    3.31 +fun force (ref (Value v)) = v
    3.32 +  | force (r as ref (Delay f)) =
    3.33 +    let
    3.34 +	val v = f ()
    3.35 +    in
    3.36 +	r := Value v;
    3.37 +	v
    3.38 +    end
    3.39 +
    3.40 +fun delay f = ref (Delay f)
    3.41 +
    3.42 +fun value v = ref (Value v)
    3.43 +
    3.44 +end
     4.1 --- a/src/Pure/General/ROOT.ML	Sat Oct 08 22:39:39 2005 +0200
     4.2 +++ b/src/Pure/General/ROOT.ML	Sat Oct 08 22:39:40 2005 +0200
     4.3 @@ -16,9 +16,6 @@
     4.4  use "symbol.ML";
     4.5  use "name_space.ML";
     4.6  use "seq.ML";
     4.7 -use "susp.ML";
     4.8 -use "lazy_seq.ML";
     4.9 -use "lazy_scan.ML";
    4.10  use "position.ML";
    4.11  use "path.ML";
    4.12  use "url.ML";
     5.1 --- a/src/Pure/General/lazy_scan.ML	Sat Oct 08 22:39:39 2005 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,206 +0,0 @@
     5.4 -(*  Title:      Pure/General/lazy_scan.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Sebastian Skalberg, TU Muenchen
     5.7 -
     5.8 -Scanner combinators for lazy sequences.
     5.9 -*)
    5.10 -
    5.11 -signature LAZY_SCAN =
    5.12 -sig
    5.13 -
    5.14 -    exception SyntaxError
    5.15 -
    5.16 -    type ('a,'b) scanner = 'a LazySeq.seq -> 'b * 'a LazySeq.seq
    5.17 -
    5.18 -    val :--      : ('a,'b) scanner * ('b -> ('a,'c) scanner)
    5.19 -		   -> ('a,'b*'c) scanner
    5.20 -    val --       : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b*'c) scanner
    5.21 -    val >>       : ('a,'b) scanner * ('b -> 'c) -> ('a,'c) scanner
    5.22 -    val --|      : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b) scanner
    5.23 -    val |--      : ('a,'b) scanner * ('a,'c) scanner -> ('a,'c) scanner
    5.24 -    val ^^       : ('a,string) scanner * ('a,string) scanner
    5.25 -		   -> ('a,string) scanner
    5.26 -    val ||       : ('a,'b) scanner * ('a,'b) scanner -> ('a,'b) scanner
    5.27 -    val one      : ('a -> bool) -> ('a,'a) scanner
    5.28 -    val succeed  : 'b -> ('a,'b) scanner
    5.29 -    val any      : ('a -> bool) -> ('a,'a list) scanner
    5.30 -    val any1     : ('a -> bool) -> ('a,'a list) scanner
    5.31 -    val optional : ('a,'b) scanner -> 'b -> ('a,'b) scanner
    5.32 -    val option   : ('a,'b) scanner -> ('a,'b option) scanner
    5.33 -    val repeat   : ('a,'b) scanner -> ('a,'b list) scanner
    5.34 -    val repeat1  : ('a,'b) scanner -> ('a,'b list) scanner
    5.35 -    val ahead    : ('a,'b) scanner -> ('a,'b) scanner
    5.36 -    val unless   : ('a LazySeq.seq -> bool) -> ('a,'b) scanner -> ('a,'b) scanner
    5.37 -    val $$       : ''a -> (''a,''a) scanner
    5.38 -    val !!       : ('a LazySeq.seq -> string) -> ('a,'b) scanner -> ('a,'b) scanner
    5.39 -    val scan_full: ('a,'b) scanner -> 'a LazySeq.seq -> 'b LazySeq.seq
    5.40 -
    5.41 -end
    5.42 -
    5.43 -structure LazyScan :> LAZY_SCAN =
    5.44 -struct
    5.45 -
    5.46 -infix 7 |-- --|
    5.47 -infix 5 :-- -- ^^
    5.48 -infix 3 >>
    5.49 -infix 0 ||
    5.50 -
    5.51 -exception SyntaxError
    5.52 -exception Fail of string
    5.53 -
    5.54 -type ('a,'b) scanner = 'a LazySeq.seq -> 'b * 'a LazySeq.seq
    5.55 -
    5.56 -fun (sc1 :-- sc2) toks =
    5.57 -    let
    5.58 -	val (x,toks2) = sc1 toks
    5.59 -	val (y,toks3) = sc2 x toks2
    5.60 -    in
    5.61 -	((x,y),toks3)
    5.62 -    end
    5.63 -
    5.64 -fun (sc1 -- sc2) toks =
    5.65 -    let
    5.66 -	val (x,toks2) = sc1 toks
    5.67 -	val (y,toks3) = sc2 toks2
    5.68 -    in
    5.69 -	((x,y),toks3)
    5.70 -    end
    5.71 -
    5.72 -fun (sc >> f) toks =
    5.73 -    let
    5.74 -	val (x,toks2) = sc toks
    5.75 -    in
    5.76 -	(f x,toks2)
    5.77 -    end
    5.78 -
    5.79 -fun (sc1 --| sc2) toks =
    5.80 -    let
    5.81 -	val (x,toks2) = sc1 toks
    5.82 -	val (_,toks3) = sc2 toks2
    5.83 -    in
    5.84 -	(x,toks3)
    5.85 -    end
    5.86 -
    5.87 -fun (sc1 |-- sc2) toks =
    5.88 -    let
    5.89 -	val (_,toks2) = sc1 toks
    5.90 -    in
    5.91 -	sc2 toks2
    5.92 -    end
    5.93 -
    5.94 -fun (sc1 ^^ sc2) toks =
    5.95 -    let
    5.96 -	val (x,toks2) = sc1 toks
    5.97 -	val (y,toks3) = sc2 toks2
    5.98 -    in
    5.99 -	(x^y,toks3)
   5.100 -    end
   5.101 -
   5.102 -fun (sc1 || sc2) toks =
   5.103 -    (sc1 toks)
   5.104 -    handle SyntaxError => sc2 toks
   5.105 -
   5.106 -fun one p toks =
   5.107 -    case LazySeq.getItem toks of
   5.108 -	NONE => raise SyntaxError
   5.109 -      | SOME(t,toks) => if p t
   5.110 -			then (t,toks)
   5.111 -			else raise SyntaxError
   5.112 -
   5.113 -fun succeed e toks = (e,toks)
   5.114 -
   5.115 -fun any p toks =
   5.116 -    case LazySeq.getItem toks of
   5.117 -	NONE =>  ([],toks)
   5.118 -      | SOME(x,toks2) => if p x
   5.119 -			 then
   5.120 -			     let
   5.121 -				 val (xs,toks3) = any p toks2
   5.122 -			     in
   5.123 -				 (x::xs,toks3)
   5.124 -			     end
   5.125 -			 else ([],toks)
   5.126 -
   5.127 -fun any1 p toks =
   5.128 -    let
   5.129 -	val (x,toks2) = one p toks
   5.130 -	val (xs,toks3) = any p toks2
   5.131 -    in
   5.132 -	(x::xs,toks3)
   5.133 -    end
   5.134 -
   5.135 -fun optional sc def =  sc || succeed def
   5.136 -fun option sc = (sc >> SOME) || succeed NONE
   5.137 -
   5.138 -(*
   5.139 -fun repeat sc =
   5.140 -    let
   5.141 -	fun R toks =
   5.142 -	    let
   5.143 -		val (x,toks2) = sc toks
   5.144 -		val (xs,toks3) = R toks2
   5.145 -	    in
   5.146 -		(x::xs,toks3)
   5.147 -	    end
   5.148 -	    handle SyntaxError => ([],toks)
   5.149 -    in
   5.150 -	R
   5.151 -    end
   5.152 -*)
   5.153 -
   5.154 -(* A tail-recursive version of repeat.  It is (ever so) slightly slower
   5.155 - * than the above, non-tail-recursive version (due to the garbage generation
   5.156 - * associated with the reversal of the list).  However,  this version will be
   5.157 - * able to process input where the former version must give up (due to stack
   5.158 - * overflow).  The slowdown seems to be around the one percent mark.
   5.159 - *)
   5.160 -fun repeat sc =
   5.161 -    let
   5.162 -	fun R xs toks =
   5.163 -	    case SOME (sc toks) handle SyntaxError => NONE of
   5.164 -		SOME (x,toks2) => R (x::xs) toks2
   5.165 -	      | NONE => (List.rev xs,toks)
   5.166 -    in
   5.167 -	R []
   5.168 -    end
   5.169 -
   5.170 -fun repeat1 sc toks =
   5.171 -    let
   5.172 -	val (x,toks2) = sc toks
   5.173 -	val (xs,toks3) = repeat sc toks2
   5.174 -    in
   5.175 -	(x::xs,toks3)
   5.176 -    end
   5.177 -
   5.178 -fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks)
   5.179 -
   5.180 -fun unless test sc toks =
   5.181 -    let
   5.182 -	val test_failed = (test toks;false) handle SyntaxError => true
   5.183 -    in
   5.184 -	if test_failed
   5.185 -	then sc toks
   5.186 -	else raise SyntaxError
   5.187 -    end
   5.188 -
   5.189 -fun $$ arg = one (fn x => x = arg)
   5.190 -
   5.191 -fun !! f sc toks = (sc toks
   5.192 -		    handle SyntaxError => raise Fail (f toks))
   5.193 -
   5.194 -fun scan_full sc toks =
   5.195 -    let
   5.196 -	fun F toks =
   5.197 -	    if LazySeq.null toks
   5.198 -	    then NONE
   5.199 -	    else
   5.200 -		let
   5.201 -		    val (x,toks') = sc toks
   5.202 -		in
   5.203 -		    SOME(x,LazySeq.make (fn () => F toks'))
   5.204 -		end
   5.205 -    in
   5.206 -	LazySeq.make (fn () => F toks)
   5.207 -    end
   5.208 -
   5.209 -end
     6.1 --- a/src/Pure/General/lazy_seq.ML	Sat Oct 08 22:39:39 2005 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,543 +0,0 @@
     6.4 -(*  Title:      Pure/General/lazy_seq.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Sebastian Skalberg, TU Muenchen
     6.7 -
     6.8 -Alternative version of lazy sequences.
     6.9 -*)
    6.10 -
    6.11 -signature LAZY_SEQ =
    6.12 -sig
    6.13 -
    6.14 -    type 'a seq
    6.15 -
    6.16 -    (* From LIST *)
    6.17 -
    6.18 -    val null : 'a seq -> bool
    6.19 -    val length : 'a seq -> int
    6.20 -    val @ : 'a seq * 'a seq -> 'a seq
    6.21 -    val hd : 'a seq -> 'a
    6.22 -    val tl : 'a seq -> 'a seq
    6.23 -    val last : 'a seq -> 'a
    6.24 -    val getItem : 'a seq -> ('a * 'a seq) option
    6.25 -    val nth : 'a seq * int -> 'a
    6.26 -    val take : 'a seq * int -> 'a seq
    6.27 -    val drop : 'a seq * int -> 'a seq
    6.28 -    val rev : 'a seq -> 'a seq
    6.29 -    val concat : 'a seq seq -> 'a seq
    6.30 -    val revAppend : 'a seq * 'a seq -> 'a seq
    6.31 -    val app : ('a -> unit) -> 'a seq -> unit
    6.32 -    val map : ('a -> 'b) -> 'a seq -> 'b seq
    6.33 -    val mapPartial : ('a -> 'b option) -> 'a seq -> 'b seq
    6.34 -    val find : ('a -> bool) -> 'a seq -> 'a option
    6.35 -    val filter : ('a -> bool) -> 'a seq -> 'a seq
    6.36 -    val partition : ('a -> bool)
    6.37 -                      -> 'a seq -> 'a seq * 'a seq
    6.38 -    val foldl : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
    6.39 -    val foldr : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
    6.40 -    val exists : ('a -> bool) -> 'a seq -> bool
    6.41 -    val all : ('a -> bool) -> 'a seq -> bool
    6.42 -    val tabulate : int * (int -> 'a) -> 'a seq
    6.43 -    val collate : ('a * 'a -> order)
    6.44 -                    -> 'a seq * 'a seq -> order 
    6.45 -
    6.46 -    (* Miscellaneous *)
    6.47 -
    6.48 -    val cycle      : ((unit ->'a seq) -> 'a seq) -> 'a seq
    6.49 -    val iterates   : ('a -> 'a) -> 'a -> 'a seq
    6.50 -    val of_function: (unit -> 'a option) -> 'a seq
    6.51 -    val of_string  : string -> char seq
    6.52 -    val of_instream: TextIO.instream -> char seq
    6.53 -
    6.54 -    (* From SEQ *)
    6.55 -
    6.56 -    val make: (unit -> ('a * 'a seq) option) -> 'a seq
    6.57 -    val empty: 'a -> 'a seq
    6.58 -    val cons: 'a * 'a seq -> 'a seq
    6.59 -    val single: 'a -> 'a seq
    6.60 -    val try: ('a -> 'b) -> 'a -> 'b seq
    6.61 -    val chop: int * 'a seq -> 'a list * 'a seq
    6.62 -    val list_of: 'a seq -> 'a list
    6.63 -    val of_list: 'a list -> 'a seq
    6.64 -    val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
    6.65 -    val interleave: 'a seq * 'a seq -> 'a seq
    6.66 -    val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
    6.67 -    val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    6.68 -    val commute: 'a seq list -> 'a list seq
    6.69 -    val succeed: 'a -> 'a seq
    6.70 -    val fail: 'a -> 'b seq
    6.71 -    val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
    6.72 -    val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
    6.73 -    val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
    6.74 -    val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
    6.75 -    val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
    6.76 -    val TRY: ('a -> 'a seq) -> 'a -> 'a seq
    6.77 -    val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
    6.78 -    val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
    6.79 -    val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
    6.80 -    val DETERM: ('a -> 'b seq) -> 'a -> 'b seq
    6.81 -
    6.82 -end
    6.83 -
    6.84 -structure LazySeq :> LAZY_SEQ =
    6.85 -struct
    6.86 -
    6.87 -open Susp
    6.88 -
    6.89 -datatype 'a seq = Seq of ('a * 'a seq) option susp
    6.90 -
    6.91 -exception Empty
    6.92 -
    6.93 -fun getItem (Seq s) = force s
    6.94 -fun make f = Seq (delay f)
    6.95 -
    6.96 -fun null s = isSome (getItem s)
    6.97 -
    6.98 -local
    6.99 -    fun F n NONE = n
   6.100 -      | F n (SOME(_,s)) = F (n+1) (getItem s)
   6.101 -in
   6.102 -fun length s = F 0 (getItem s)
   6.103 -end
   6.104 -
   6.105 -fun s1 @ s2 =
   6.106 -    let
   6.107 -	fun F NONE = getItem s2
   6.108 -	  | F (SOME(x,s1')) = SOME(x,F' s1')
   6.109 -	and F' s = make (fn () => F (getItem s))
   6.110 -    in
   6.111 -	F' s1
   6.112 -    end
   6.113 -
   6.114 -local
   6.115 -    fun F NONE = raise Empty
   6.116 -      | F (SOME arg) = arg
   6.117 -in
   6.118 -fun hd s = #1 (F (getItem s))
   6.119 -fun tl s = #2 (F (getItem s))
   6.120 -end
   6.121 -
   6.122 -local
   6.123 -    fun F x NONE = x
   6.124 -      | F _ (SOME(x,s)) = F x (getItem s)
   6.125 -    fun G NONE = raise Empty
   6.126 -      | G (SOME(x,s)) = F x (getItem s)
   6.127 -in
   6.128 -fun last s = G (getItem s)
   6.129 -end
   6.130 -
   6.131 -local
   6.132 -    fun F NONE _ = raise Subscript
   6.133 -      | F (SOME(x,_)) 0 = x
   6.134 -      | F (SOME(_,s)) n = F (getItem s) (n-1)
   6.135 -in
   6.136 -fun nth(s,n) =
   6.137 -    if n < 0
   6.138 -    then raise Subscript
   6.139 -    else F (getItem s) n
   6.140 -end
   6.141 -
   6.142 -local
   6.143 -    fun F NONE _ = raise Subscript
   6.144 -      | F (SOME(x,s)) n = SOME(x,F' s (n-1))
   6.145 -    and F' s 0 = Seq (value NONE)
   6.146 -      | F' s n = make (fn () => F (getItem s) n)
   6.147 -in
   6.148 -fun take (s,n) =
   6.149 -    if n < 0
   6.150 -    then raise Subscript
   6.151 -    else F' s n
   6.152 -end
   6.153 -
   6.154 -local
   6.155 -    fun F s 0 = s
   6.156 -      | F NONE _ = raise Subscript
   6.157 -      | F (SOME(_,s)) n = F (getItem s) (n-1)
   6.158 -in
   6.159 -fun drop (s,0) = s
   6.160 -  | drop (s,n) = 
   6.161 -    if n < 0
   6.162 -    then raise Subscript
   6.163 -    else make (fn () => F (getItem s) n)
   6.164 -end
   6.165 -
   6.166 -local
   6.167 -    fun F s NONE = s
   6.168 -      | F s (SOME(x,s')) = F (SOME(x, Seq (value s))) (getItem s')
   6.169 -in
   6.170 -fun rev s = make (fn () => F NONE (getItem s))
   6.171 -end
   6.172 -
   6.173 -local
   6.174 -    fun F s NONE = getItem s
   6.175 -      | F s (SOME(x,s')) = F (Seq (value (SOME(x,s)))) (getItem s')
   6.176 -in
   6.177 -fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
   6.178 -end
   6.179 -
   6.180 -local
   6.181 -    fun F NONE = NONE
   6.182 -      | F (SOME(s1,s2)) =
   6.183 -	let
   6.184 -	    fun G NONE = F (getItem s2)
   6.185 -	      | G (SOME(x,s)) = SOME(x,make (fn () => G (getItem s)))
   6.186 -	in
   6.187 -	    G (getItem s1)
   6.188 -	end
   6.189 -in
   6.190 -fun concat s = make (fn () => F (getItem s))
   6.191 -end
   6.192 -
   6.193 -fun app f =
   6.194 -    let
   6.195 -	fun F NONE = ()
   6.196 -	  | F (SOME(x,s)) =
   6.197 -	    (f x;
   6.198 -	     F (getItem s))
   6.199 -    in
   6.200 -	F o getItem
   6.201 -    end
   6.202 -
   6.203 -fun map f =
   6.204 -    let
   6.205 -	fun F NONE = NONE
   6.206 -	  | F (SOME(x,s)) = SOME(f x,F' s)
   6.207 -	and F' s = make (fn() => F (getItem s))
   6.208 -    in
   6.209 -	F'
   6.210 -    end
   6.211 -
   6.212 -fun mapPartial f =
   6.213 -    let
   6.214 -	fun F NONE = NONE
   6.215 -	  | F (SOME(x,s)) =
   6.216 -	    (case f x of
   6.217 -		 SOME y => SOME(y,F' s)
   6.218 -	       | NONE => F (getItem s))
   6.219 -	and F' s = make (fn()=> F (getItem s))
   6.220 -    in
   6.221 -	F'
   6.222 -    end
   6.223 -
   6.224 -fun find P =
   6.225 -    let
   6.226 -	fun F NONE = NONE
   6.227 -	  | F (SOME(x,s)) =
   6.228 -	    if P x
   6.229 -	    then SOME x
   6.230 -	    else F (getItem s)
   6.231 -    in
   6.232 -	F o getItem
   6.233 -    end
   6.234 -
   6.235 -(*fun filter p = mapPartial (fn x => if p x then SOME x else NONE)*)
   6.236 -
   6.237 -fun filter P =
   6.238 -    let
   6.239 -	fun F NONE = NONE
   6.240 -	  | F (SOME(x,s)) =
   6.241 -	    if P x
   6.242 -	    then SOME(x,F' s)
   6.243 -	    else F (getItem s)
   6.244 -	and F' s = make (fn () => F (getItem s))
   6.245 -    in
   6.246 -	F'
   6.247 -    end
   6.248 -
   6.249 -fun partition f s =
   6.250 -    let
   6.251 -	val s' = map (fn x => (x,f x)) s
   6.252 -    in
   6.253 -	(mapPartial (fn (x,true) => SOME x | _ => NONE) s',
   6.254 -	 mapPartial (fn (x,false) => SOME x | _ => NONE) s')
   6.255 -    end
   6.256 -
   6.257 -fun exists P =
   6.258 -    let
   6.259 -	fun F NONE = false
   6.260 -	  | F (SOME(x,s)) = P x orelse F (getItem s)
   6.261 -    in
   6.262 -	F o getItem
   6.263 -    end
   6.264 -
   6.265 -fun all P =
   6.266 -    let
   6.267 -	fun F NONE = true
   6.268 -	  | F (SOME(x,s)) = P x andalso F (getItem s)
   6.269 -    in
   6.270 -	F o getItem
   6.271 -    end
   6.272 -
   6.273 -(*fun tabulate f = map f (iterates (fn x => x + 1) 0)*)
   6.274 -
   6.275 -fun tabulate (n,f) =
   6.276 -    let
   6.277 -	fun F n = make (fn () => SOME(f n,F (n+1)))
   6.278 -    in
   6.279 -	F n
   6.280 -    end
   6.281 -
   6.282 -fun collate c (s1,s2) =
   6.283 -    let
   6.284 -	fun F NONE _ = LESS
   6.285 -	  | F _ NONE = GREATER
   6.286 -	  | F (SOME(x,s1)) (SOME(y,s2)) =
   6.287 -	    (case c (x,y) of
   6.288 -		 LESS => LESS
   6.289 -	       | GREATER => GREATER
   6.290 -	       | EQUAL => F' s1 s2)
   6.291 -	and F' s1 s2 = F (getItem s1) (getItem s2)
   6.292 -    in
   6.293 -	F' s1 s2
   6.294 -    end
   6.295 -
   6.296 -fun empty  _ = Seq (value NONE)
   6.297 -fun single x = Seq(value (SOME(x,Seq (value NONE))))
   6.298 -fun cons a = Seq(value (SOME a))
   6.299 -
   6.300 -fun cycle seqfn =
   6.301 -    let
   6.302 -	val knot = ref (Seq (value NONE))
   6.303 -    in
   6.304 -	knot := seqfn (fn () => !knot);
   6.305 -	!knot
   6.306 -    end
   6.307 -
   6.308 -fun iterates f =
   6.309 -    let
   6.310 -	fun F x = make (fn() => SOME(x,F (f x)))
   6.311 -    in
   6.312 -	F
   6.313 -    end
   6.314 -
   6.315 -fun interleave (s1,s2) =
   6.316 -    let
   6.317 -	fun F NONE = getItem s2
   6.318 -	  | F (SOME(x,s1')) = SOME(x,interleave(s2,s1'))
   6.319 -    in
   6.320 -	make (fn()=> F (getItem s1))
   6.321 -    end
   6.322 -
   6.323 -(* val force_all = app ignore *)
   6.324 -
   6.325 -local
   6.326 -    fun F NONE = ()
   6.327 -      | F (SOME(x,s)) = F (getItem s)
   6.328 -in
   6.329 -fun force_all s = F (getItem s)
   6.330 -end
   6.331 -
   6.332 -fun of_function f =
   6.333 -    let
   6.334 -	fun F () = case f () of
   6.335 -		       SOME x => SOME(x,make F)
   6.336 -		     | NONE => NONE
   6.337 -    in
   6.338 -	make F
   6.339 -    end
   6.340 -
   6.341 -local
   6.342 -    fun F [] = NONE
   6.343 -      | F (x::xs) = SOME(x,F' xs)
   6.344 -    and F' xs = make (fn () => F xs)
   6.345 -in
   6.346 -fun of_list xs = F' xs
   6.347 -end
   6.348 -
   6.349 -val of_string = of_list o String.explode
   6.350 -
   6.351 -fun of_instream is =
   6.352 -    let
   6.353 -	val buffer : char list ref = ref []
   6.354 -	fun get_input () =
   6.355 -	    case !buffer of
   6.356 -		(c::cs) => (buffer:=cs;
   6.357 -			    SOME c)
   6.358 -	      |	[] => (case String.explode (TextIO.input is) of
   6.359 -			   [] => NONE
   6.360 -			 | (c::cs) => (buffer := cs;
   6.361 -				       SOME c))
   6.362 -    in
   6.363 -	of_function get_input
   6.364 -    end
   6.365 -
   6.366 -local
   6.367 -    fun F k NONE = k []
   6.368 -      | F k (SOME(x,s)) = F (fn xs => k (x::xs)) (getItem s)
   6.369 -in
   6.370 -fun list_of s = F (fn x => x) (getItem s)
   6.371 -end
   6.372 -
   6.373 -(* Adapted from seq.ML *)
   6.374 -
   6.375 -val succeed = single
   6.376 -fun fail _ = Seq (value NONE)
   6.377 -
   6.378 -(* fun op THEN (f, g) x = flat (map g (f x)) *)
   6.379 -
   6.380 -fun op THEN (f, g) =
   6.381 -    let
   6.382 -	fun F NONE = NONE
   6.383 -	  | F (SOME(x,xs)) =
   6.384 -	    let
   6.385 -		fun G NONE = F (getItem xs)
   6.386 -		  | G (SOME(y,ys)) = SOME(y,make (fn () => G (getItem ys)))
   6.387 -	    in
   6.388 -		G (getItem (g x))
   6.389 -	    end
   6.390 -    in
   6.391 -	fn x => make (fn () => F (getItem (f x)))
   6.392 -    end
   6.393 -
   6.394 -fun op ORELSE (f, g) x =
   6.395 -    make (fn () =>
   6.396 -	     case getItem (f x) of
   6.397 -		 NONE => getItem (g x)
   6.398 -	       | some => some)
   6.399 -
   6.400 -fun op APPEND (f, g) x =
   6.401 -    let
   6.402 -	fun copy s =
   6.403 -	    case getItem s of
   6.404 -		NONE => getItem (g x)
   6.405 -	      | SOME(x,xs) => SOME(x,make (fn () => copy xs))
   6.406 -    in
   6.407 -	make (fn () => copy (f x))
   6.408 -    end
   6.409 -
   6.410 -fun EVERY fs = foldr THEN succeed fs
   6.411 -fun FIRST fs = foldr ORELSE fail fs
   6.412 -
   6.413 -fun TRY f x =
   6.414 -    make (fn () =>
   6.415 -	     case getItem (f x) of
   6.416 -		 NONE => SOME(x,Seq (value NONE))
   6.417 -	       | some => some)
   6.418 -
   6.419 -fun REPEAT f =
   6.420 -    let
   6.421 -	fun rep qs x =
   6.422 -	    case getItem (f x) of
   6.423 -		NONE => SOME(x, make (fn () => repq qs))
   6.424 -	      | SOME (x', q) => rep (q :: qs) x'
   6.425 -	and repq [] = NONE
   6.426 -	  | repq (q :: qs) =
   6.427 -            case getItem q of
   6.428 -		NONE => repq qs
   6.429 -              | SOME (x, q) => rep (q :: qs) x
   6.430 -    in
   6.431 -     fn x => make (fn () => rep [] x)
   6.432 -    end
   6.433 -
   6.434 -fun REPEAT1 f = THEN (f, REPEAT f);
   6.435 -
   6.436 -fun INTERVAL f i =
   6.437 -    let
   6.438 -	fun F j =
   6.439 -	    if i > j
   6.440 -	    then single
   6.441 -	    else op THEN (f j, F (j - 1))
   6.442 -    in F end
   6.443 -
   6.444 -fun DETERM f x =
   6.445 -    make (fn () =>
   6.446 -	     case getItem (f x) of
   6.447 -		 NONE => NONE
   6.448 -	       | SOME (x', _) => SOME(x',Seq (value NONE)))
   6.449 -
   6.450 -(*partial function as procedure*)
   6.451 -fun try f x =
   6.452 -    make (fn () =>
   6.453 -	     case Library.try f x of
   6.454 -		 SOME y => SOME(y,Seq (value NONE))
   6.455 -	       | NONE => NONE)
   6.456 -
   6.457 -(*functional to print a sequence, up to "count" elements;
   6.458 -  the function prelem should print the element number and also the element*)
   6.459 -fun print prelem count seq =
   6.460 -    let
   6.461 -	fun pr k xq =
   6.462 -	    if k > count
   6.463 -	    then ()
   6.464 -	    else
   6.465 -		case getItem xq of
   6.466 -		    NONE => ()
   6.467 -		  | SOME (x, xq') =>
   6.468 -		    (prelem k x;
   6.469 -		     writeln "";
   6.470 -		     pr (k + 1) xq')
   6.471 -    in
   6.472 -	pr 1 seq
   6.473 -    end
   6.474 -
   6.475 -(*accumulating a function over a sequence; this is lazy*)
   6.476 -fun it_right f (xq, yq) =
   6.477 -    let
   6.478 -	fun its s =
   6.479 -	    make (fn () =>
   6.480 -		     case getItem s of
   6.481 -			 NONE => getItem yq
   6.482 -		       | SOME (a, s') => getItem(f (a, its s')))
   6.483 -    in
   6.484 -	its xq
   6.485 -    end
   6.486 -
   6.487 -(*map over a sequence s1, append the sequence s2*)
   6.488 -fun mapp f s1 s2 =
   6.489 -    let
   6.490 -	fun F NONE = getItem s2
   6.491 -	  | F (SOME(x,s1')) = SOME(f x,F' s1')
   6.492 -	and F' s = make (fn () => F (getItem s))
   6.493 -    in
   6.494 -	F' s1
   6.495 -    end
   6.496 -
   6.497 -(*turn a list of sequences into a sequence of lists*)
   6.498 -local
   6.499 -    fun F [] = SOME([],Seq (value NONE))
   6.500 -      | F (xq :: xqs) =
   6.501 -        case getItem xq of
   6.502 -            NONE => NONE
   6.503 -          | SOME (x, xq') =>
   6.504 -            (case F xqs of
   6.505 -		 NONE => NONE
   6.506 -	       | SOME (xs, xsq) =>
   6.507 -		 let
   6.508 -		     fun G s =
   6.509 -			 make (fn () =>
   6.510 -				  case getItem s of
   6.511 -				      NONE => F (xq' :: xqs)
   6.512 -				    | SOME(ys,ysq) => SOME(x::ys,G ysq))
   6.513 -		 in
   6.514 -		     SOME (x :: xs, G xsq)
   6.515 -		 end)
   6.516 -in
   6.517 -fun commute xqs = make (fn () => F xqs)
   6.518 -end
   6.519 -
   6.520 -(*the list of the first n elements, paired with rest of sequence;
   6.521 -  if length of list is less than n, then sequence had less than n elements*)
   6.522 -fun chop (n, xq) =
   6.523 -    if n <= 0
   6.524 -    then ([], xq)
   6.525 -    else
   6.526 -	case getItem xq of
   6.527 -	    NONE => ([], xq)
   6.528 -	  | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq'))
   6.529 -
   6.530 -fun foldl f e s =
   6.531 -    let
   6.532 -	fun F k NONE = k e
   6.533 -	  | F k (SOME(x,s)) = F (fn y => k (f(x,y))) (getItem s)
   6.534 -    in
   6.535 -	F (fn x => x) (getItem s)
   6.536 -    end
   6.537 -
   6.538 -fun foldr f e s =
   6.539 -    let
   6.540 -	fun F e NONE = e
   6.541 -	  | F e (SOME(x,s)) = F (f(x,e)) (getItem s)
   6.542 -    in
   6.543 -	F e (getItem s)
   6.544 -    end
   6.545 -
   6.546 -end
     7.1 --- a/src/Pure/General/susp.ML	Sat Oct 08 22:39:39 2005 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,41 +0,0 @@
     7.4 -(*  Title:      Pure/General/susp.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Sebastian Skalberg, TU Muenchen
     7.7 -
     7.8 -Delayed evaluation.
     7.9 -*)
    7.10 -
    7.11 -signature SUSP =
    7.12 -sig
    7.13 -
    7.14 -type 'a susp
    7.15 -
    7.16 -val force : 'a susp -> 'a
    7.17 -val delay : (unit -> 'a) -> 'a susp
    7.18 -val value : 'a -> 'a susp
    7.19 -
    7.20 -end
    7.21 -
    7.22 -structure Susp :> SUSP =
    7.23 -struct
    7.24 -
    7.25 -datatype 'a suspVal
    7.26 -  = Value of 'a
    7.27 -  | Delay of unit -> 'a
    7.28 -
    7.29 -type 'a susp = 'a suspVal ref
    7.30 -
    7.31 -fun force (ref (Value v)) = v
    7.32 -  | force (r as ref (Delay f)) =
    7.33 -    let
    7.34 -	val v = f ()
    7.35 -    in
    7.36 -	r := Value v;
    7.37 -	v
    7.38 -    end
    7.39 -
    7.40 -fun delay f = ref (Delay f)
    7.41 -
    7.42 -fun value v = ref (Value v)
    7.43 -
    7.44 -end
     8.1 --- a/src/Pure/IsaMakefile	Sat Oct 08 22:39:39 2005 +0200
     8.2 +++ b/src/Pure/IsaMakefile	Sat Oct 08 22:39:40 2005 +0200
     8.3 @@ -21,15 +21,15 @@
     8.4  
     8.5  ## Pure
     8.6  
     8.7 -Pure: $(OUT)/Pure
     8.8 +Pure: $(OUT)/Pure$(ML_SUFFIX)
     8.9  
    8.10 -$(OUT)/Pure: CPure.thy General/ROOT.ML General/alist.ML                 \
    8.11 +$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML     \
    8.12    General/buffer.ML                                                     \
    8.13    General/file.ML General/graph.ML General/heap.ML General/history.ML   \
    8.14 -  General/lazy_scan.ML General/lazy_seq.ML General/name_space.ML        \
    8.15 +  General/name_space.ML        \
    8.16    General/ord_list.ML General/output.ML General/path.ML                 \
    8.17    General/position.ML General/pretty.ML General/scan.ML General/seq.ML  \
    8.18 -  General/source.ML General/stack.ML General/susp.ML General/symbol.ML  \
    8.19 +  General/source.ML General/stack.ML General/symbol.ML  \
    8.20    General/table.ML General/url.ML General/xml.ML IsaPlanner/focus_term_lib.ML \
    8.21    IsaPlanner/isa_fterm.ML IsaPlanner/isand.ML IsaPlanner/isaplib.ML     \
    8.22    IsaPlanner/rw_inst.ML IsaPlanner/rw_tools.ML IsaPlanner/term_lib.ML   \
    8.23 @@ -44,7 +44,7 @@
    8.24    Isar/proof_history.ML Isar/rule_cases.ML Isar/session.ML              \
    8.25    Isar/skip_proof.ML Isar/term_style.ML Isar/thy_header.ML              \
    8.26    Isar/toplevel.ML ML-Systems/cpu-timer-basis.ML                        \
    8.27 -  ML-Systems/cpu-timer-gc.ML                                            \
    8.28 +  ML-Systems/cpu-timer-gc.ML ML-Systems/poplogml.ML                     \
    8.29    ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML                  \
    8.30    ML-Systems/polyml-posix.ML ML-Systems/smlnj-basis-compat.ML           \
    8.31    ML-Systems/smlnj-compiler.ML ML-Systems/smlnj-ptreql.ML               \
    8.32 @@ -82,4 +82,4 @@
    8.33  ## clean
    8.34  
    8.35  clean:
    8.36 -	@rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz
    8.37 +	@rm -f $(OUT)/Pure$(ML_SUFFIX) $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz