do not open Susp;
authorwenzelm
Thu Oct 23 13:52:26 2008 +0200 (2008-10-23)
changeset 28670f8bd813b41f9
parent 28669 fdae33134bbf
child 28671 ed6681dd35d8
do not open Susp;
src/HOL/Import/lazy_seq.ML
     1.1 --- a/src/HOL/Import/lazy_seq.ML	Thu Oct 23 13:51:54 2008 +0200
     1.2 +++ b/src/HOL/Import/lazy_seq.ML	Thu Oct 23 13:52:26 2008 +0200
     1.3 @@ -80,15 +80,13 @@
     1.4  structure LazySeq :> LAZY_SEQ =
     1.5  struct
     1.6  
     1.7 -open Susp
     1.8 -
     1.9  datatype 'a seq = Seq of ('a * 'a seq) option Susp.T
    1.10  
    1.11  exception Empty
    1.12  
    1.13 -fun getItem (Seq s) = force s
    1.14 +fun getItem (Seq s) = Susp.force s
    1.15  val pull = getItem
    1.16 -fun make f = Seq (delay f)
    1.17 +fun make f = Seq (Susp.delay f)
    1.18  
    1.19  fun null s = is_none (getItem s)
    1.20  
    1.21 @@ -139,7 +137,7 @@
    1.22  local
    1.23      fun F NONE _ = raise Subscript
    1.24        | F (SOME(x,s)) n = SOME(x,F' s (n-1))
    1.25 -    and F' s 0 = Seq (value NONE)
    1.26 +    and F' s 0 = Seq (Susp.value NONE)
    1.27        | F' s n = make (fn () => F (getItem s) n)
    1.28  in
    1.29  fun take (s,n) =
    1.30 @@ -168,14 +166,14 @@
    1.31  
    1.32  local
    1.33      fun F s NONE = s
    1.34 -      | F s (SOME(x,s')) = F (SOME(x, Seq (value s))) (getItem s')
    1.35 +      | F s (SOME(x,s')) = F (SOME(x, Seq (Susp.value s))) (getItem s')
    1.36  in
    1.37  fun rev s = make (fn () => F NONE (getItem s))
    1.38  end
    1.39  
    1.40  local
    1.41      fun F s NONE = getItem s
    1.42 -      | F s (SOME(x,s')) = F (Seq (value (SOME(x,s)))) (getItem s')
    1.43 +      | F s (SOME(x,s')) = F (Seq (Susp.value (SOME(x,s)))) (getItem s')
    1.44  in
    1.45  fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
    1.46  end
    1.47 @@ -296,13 +294,13 @@
    1.48  	F' s1 s2
    1.49      end
    1.50  
    1.51 -fun empty  _ = Seq (value NONE)
    1.52 -fun single x = Seq(value (SOME(x,Seq (value NONE))))
    1.53 -fun cons a = Seq(value (SOME a))
    1.54 +fun empty  _ = Seq (Susp.value NONE)
    1.55 +fun single x = Seq(Susp.value (SOME(x,Seq (Susp.value NONE))))
    1.56 +fun cons a = Seq(Susp.value (SOME a))
    1.57  
    1.58  fun cycle seqfn =
    1.59      let
    1.60 -	val knot = ref (Seq (value NONE))
    1.61 +	val knot = ref (Seq (Susp.value NONE))
    1.62      in
    1.63  	knot := seqfn (fn () => !knot);
    1.64  	!knot
    1.65 @@ -376,7 +374,7 @@
    1.66  (* Adapted from seq.ML *)
    1.67  
    1.68  val succeed = single
    1.69 -fun fail _ = Seq (value NONE)
    1.70 +fun fail _ = Seq (Susp.value NONE)
    1.71  
    1.72  (* fun op THEN (f, g) x = flat (map g (f x)) *)
    1.73  
    1.74 @@ -416,7 +414,7 @@
    1.75  fun TRY f x =
    1.76      make (fn () =>
    1.77  	     case getItem (f x) of
    1.78 -		 NONE => SOME(x,Seq (value NONE))
    1.79 +		 NONE => SOME(x,Seq (Susp.value NONE))
    1.80  	       | some => some)
    1.81  
    1.82  fun REPEAT f =
    1.83 @@ -448,13 +446,13 @@
    1.84      make (fn () =>
    1.85  	     case getItem (f x) of
    1.86  		 NONE => NONE
    1.87 -	       | SOME (x', _) => SOME(x',Seq (value NONE)))
    1.88 +	       | SOME (x', _) => SOME(x',Seq (Susp.value NONE)))
    1.89  
    1.90  (*partial function as procedure*)
    1.91  fun try f x =
    1.92      make (fn () =>
    1.93  	     case Basics.try f x of
    1.94 -		 SOME y => SOME(y,Seq (value NONE))
    1.95 +		 SOME y => SOME(y,Seq (Susp.value NONE))
    1.96  	       | NONE => NONE)
    1.97  
    1.98  (*functional to print a sequence, up to "count" elements;
    1.99 @@ -499,7 +497,7 @@
   1.100  
   1.101  (*turn a list of sequences into a sequence of lists*)
   1.102  local
   1.103 -    fun F [] = SOME([],Seq (value NONE))
   1.104 +    fun F [] = SOME([],Seq (Susp.value NONE))
   1.105        | F (xq :: xqs) =
   1.106          case getItem xq of
   1.107              NONE => NONE