src/Pure/General/seq.ML
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/General/seq.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/General/seq.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -56,17 +56,17 @@
     1.4  (*the abstraction for making a sequence*)
     1.5  val make = Seq;
     1.6  
     1.7 -(*return next sequence element as None or Some (x, xq)*)
     1.8 +(*return next sequence element as NONE or SOME (x, xq)*)
     1.9  fun pull (Seq f) = f ();
    1.10  
    1.11  
    1.12  (*the empty sequence*)
    1.13 -val empty = Seq (fn () => None);
    1.14 +val empty = Seq (fn () => NONE);
    1.15  
    1.16  (*prefix an element to the sequence -- use cons (x, xq) only if
    1.17    evaluation of xq need not be delayed, otherwise use
    1.18 -  make (fn () => Some (x, xq))*)
    1.19 -fun cons x_xq = make (fn () => Some x_xq);
    1.20 +  make (fn () => SOME (x, xq))*)
    1.21 +fun cons x_xq = make (fn () => SOME x_xq);
    1.22  
    1.23  fun single x = cons (x, empty);
    1.24  
    1.25 @@ -77,8 +77,8 @@
    1.26  (*partial function as procedure*)
    1.27  fun try f x =
    1.28    (case Library.try f x of
    1.29 -    Some y => single y
    1.30 -  | None => empty);
    1.31 +    SOME y => single y
    1.32 +  | NONE => empty);
    1.33  
    1.34  
    1.35  (*the list of the first n elements, paired with rest of sequence;
    1.36 @@ -87,14 +87,14 @@
    1.37    if n <= 0 then ([], xq)
    1.38    else
    1.39      (case pull xq of
    1.40 -      None => ([], xq)
    1.41 -    | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
    1.42 +      NONE => ([], xq)
    1.43 +    | SOME (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
    1.44  
    1.45  (*conversion from sequence to list*)
    1.46  fun list_of xq =
    1.47    (case pull xq of
    1.48 -    None => []
    1.49 -  | Some (x, xq') => x :: list_of xq');
    1.50 +    NONE => []
    1.51 +  | SOME (x, xq') => x :: list_of xq');
    1.52  
    1.53  (*conversion from list to sequence*)
    1.54  fun of_list xs = foldr cons (xs, empty);
    1.55 @@ -104,8 +104,8 @@
    1.56  fun map f xq =
    1.57    make (fn () =>
    1.58      (case pull xq of
    1.59 -      None => None
    1.60 -    | Some (x, xq') => Some (f x, map f xq')));
    1.61 +      NONE => NONE
    1.62 +    | SOME (x, xq') => SOME (f x, map f xq')));
    1.63  
    1.64  (*map over a sequence xq, append the sequence yq*)
    1.65  fun mapp f xq yq =
    1.66 @@ -113,8 +113,8 @@
    1.67      fun copy s =
    1.68        make (fn () =>
    1.69          (case pull s of
    1.70 -          None => pull yq
    1.71 -        | Some (x, s') => Some (f x, copy s')))
    1.72 +          NONE => pull yq
    1.73 +        | SOME (x, s') => SOME (f x, copy s')))
    1.74    in copy xq end;
    1.75  
    1.76  (*sequence append:  put the elements of xq in front of those of yq*)
    1.77 @@ -123,8 +123,8 @@
    1.78      fun copy s =
    1.79        make (fn () =>
    1.80          (case pull s of
    1.81 -          None => pull yq
    1.82 -        | Some (x, s') => Some (x, copy s')))
    1.83 +          NONE => pull yq
    1.84 +        | SOME (x, s') => SOME (x, copy s')))
    1.85    in copy xq end;
    1.86  
    1.87  (*filter sequence by predicate*)
    1.88 @@ -133,23 +133,23 @@
    1.89      fun copy s =
    1.90        make (fn () =>
    1.91          (case pull s of
    1.92 -          None => None
    1.93 -        | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));
    1.94 +          NONE => NONE
    1.95 +        | SOME (x, s') => if pred x then SOME (x, copy s') else pull (copy s')));
    1.96    in copy xq end;
    1.97  
    1.98  (*flatten a sequence of sequences to a single sequence*)
    1.99  fun flat xqq =
   1.100    make (fn () =>
   1.101      (case pull xqq of
   1.102 -      None => None
   1.103 -    | Some (xq, xqq') => pull (append (xq, flat xqq'))));
   1.104 +      NONE => NONE
   1.105 +    | SOME (xq, xqq') => pull (append (xq, flat xqq'))));
   1.106  
   1.107  (*interleave elements of xq with those of yq -- fairer than append*)
   1.108  fun interleave (xq, yq) =
   1.109    make (fn () =>
   1.110      (case pull xq of
   1.111 -      None => pull yq
   1.112 -    | Some (x, xq') => Some (x, interleave (yq, xq'))));
   1.113 +      NONE => pull yq
   1.114 +    | SOME (x, xq') => SOME (x, interleave (yq, xq'))));
   1.115  
   1.116  
   1.117  (*functional to print a sequence, up to "count" elements;
   1.118 @@ -160,8 +160,8 @@
   1.119        if k > count then ()
   1.120        else
   1.121          (case pull xq of
   1.122 -          None => ()
   1.123 -        | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
   1.124 +          NONE => ()
   1.125 +        | SOME (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
   1.126    in pr (1, seq) end;
   1.127  
   1.128  (*accumulating a function over a sequence; this is lazy*)
   1.129 @@ -170,8 +170,8 @@
   1.130      fun its s =
   1.131        make (fn () =>
   1.132          (case pull s of
   1.133 -          None => pull yq
   1.134 -        | Some (a, s') => pull (f (a, its s'))))
   1.135 +          NONE => pull yq
   1.136 +        | SOME (a, s') => pull (f (a, its s'))))
   1.137    in its xq end;
   1.138  
   1.139  (*turn a list of sequences into a sequence of lists*)
   1.140 @@ -179,12 +179,12 @@
   1.141    | commute (xq :: xqs) =
   1.142        make (fn () =>
   1.143          (case pull xq of
   1.144 -          None => None
   1.145 -        | Some (x, xq') =>
   1.146 +          NONE => NONE
   1.147 +        | SOME (x, xq') =>
   1.148              (case pull (commute xqs) of
   1.149 -              None => None
   1.150 -            | Some (xs, xsq) =>
   1.151 -                Some (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs))))));
   1.152 +              NONE => NONE
   1.153 +            | SOME (xs, xsq) =>
   1.154 +                SOME (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs))))));
   1.155  
   1.156  
   1.157  
   1.158 @@ -197,7 +197,7 @@
   1.159  
   1.160  fun op ORELSE (f, g) x =
   1.161    (case pull (f x) of
   1.162 -    None => g x
   1.163 +    NONE => g x
   1.164    | some => make (fn () => some));
   1.165  
   1.166  fun op APPEND (f, g) x =
   1.167 @@ -212,13 +212,13 @@
   1.168    let
   1.169      fun rep qs x =
   1.170        (case pull (f x) of
   1.171 -        None => Some (x, make (fn () => repq qs))
   1.172 -      | Some (x', q) => rep (q :: qs) x')
   1.173 -    and repq [] = None
   1.174 +        NONE => SOME (x, make (fn () => repq qs))
   1.175 +      | SOME (x', q) => rep (q :: qs) x')
   1.176 +    and repq [] = NONE
   1.177        | repq (q :: qs) =
   1.178            (case pull q of
   1.179 -            None => repq qs
   1.180 -          | Some (x, q) => rep (q :: qs) x);
   1.181 +            NONE => repq qs
   1.182 +          | SOME (x, q) => rep (q :: qs) x);
   1.183    in fn x => make (fn () => rep [] x) end;
   1.184  
   1.185  fun REPEAT1 f = THEN (f, REPEAT f);
   1.186 @@ -229,7 +229,7 @@
   1.187  
   1.188  fun DETERM f x =
   1.189    (case pull (f x) of
   1.190 -    None => empty
   1.191 -  | Some (x', _) => cons (x', empty));
   1.192 +    NONE => empty
   1.193 +  | SOME (x', _) => cons (x', empty));
   1.194  
   1.195  end;