moved seq.ML to General/seq.ML;
authorwenzelm
Wed Jun 10 11:52:59 1998 +0200 (1998-06-10)
changeset 501432e6cab5e7d4
parent 5013 5b0c97631aff
child 5015 44fd9e09c637
moved seq.ML to General/seq.ML;
src/Pure/General/seq.ML
src/Pure/seq.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/seq.ML	Wed Jun 10 11:52:59 1998 +0200
     1.3 @@ -0,0 +1,204 @@
     1.4 +(*  Title:      Pure/seq.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +
     1.8 +Unbounded sequences implemented by closures.  RECOMPUTES if sequence
     1.9 +is re-inspected.  Memoing, using polymorphic refs, was found to be
    1.10 +slower!  (More GCs)
    1.11 +*)
    1.12 +
    1.13 +signature SEQ =
    1.14 +sig
    1.15 +  type 'a seq
    1.16 +  val make: (unit -> ('a * 'a seq) option) -> 'a seq
    1.17 +  val pull: 'a seq -> ('a * 'a seq) option
    1.18 +  val empty: 'a seq
    1.19 +  val cons: 'a * 'a seq -> 'a seq
    1.20 +  val single: 'a -> 'a seq
    1.21 +  val hd: 'a seq -> 'a
    1.22 +  val tl: 'a seq -> 'a seq
    1.23 +  val chop: int * 'a seq -> 'a list * 'a seq
    1.24 +  val list_of: 'a seq -> 'a list
    1.25 +  val of_list: 'a list -> 'a seq
    1.26 +  val map: ('a -> 'b) -> 'a seq -> 'b seq
    1.27 +  val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
    1.28 +  val append: 'a seq * 'a seq -> 'a seq
    1.29 +  val filter: ('a -> bool) -> 'a seq -> 'a seq
    1.30 +  val flat: 'a seq seq -> 'a seq
    1.31 +  val interleave: 'a seq * 'a seq -> 'a seq
    1.32 +  val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
    1.33 +  val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    1.34 +  val succeed: 'a -> 'a seq
    1.35 +  val fail: 'a -> 'b seq
    1.36 +  val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
    1.37 +  val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
    1.38 +  val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
    1.39 +  val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
    1.40 +  val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
    1.41 +  val TRY: ('a -> 'a seq) -> 'a -> 'a seq
    1.42 +  val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
    1.43 +end;
    1.44 +
    1.45 +structure Seq: SEQ =
    1.46 +struct
    1.47 +
    1.48 +
    1.49 +(** lazy sequences **)
    1.50 +
    1.51 +datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
    1.52 +
    1.53 +(*the abstraction for making a sequence*)
    1.54 +val make = Seq;
    1.55 +
    1.56 +(*return next sequence element as None or Some (x, xq)*)
    1.57 +fun pull (Seq f) = f ();
    1.58 +
    1.59 +
    1.60 +(*the empty sequence*)
    1.61 +val empty = Seq (fn () => None);
    1.62 +
    1.63 +(*prefix an element to the sequence -- use cons (x, xq) only if
    1.64 +  evaluation of xq need not be delayed, otherwise use
    1.65 +  make (fn () => Some (x, xq))*)
    1.66 +fun cons x_xq = make (fn () => Some x_xq);
    1.67 +
    1.68 +fun single x = cons (x, empty);
    1.69 +
    1.70 +(*head and tail -- beware of calling the sequence function twice!!*)
    1.71 +fun hd xq = #1 (the (pull xq))
    1.72 +and tl xq = #2 (the (pull xq));
    1.73 +
    1.74 +
    1.75 +(*the list of the first n elements, paired with rest of sequence;
    1.76 +  if length of list is less than n, then sequence had less than n elements*)
    1.77 +fun chop (n, xq) =
    1.78 +  if n <= 0 then ([], xq)
    1.79 +  else
    1.80 +    (case pull xq of
    1.81 +      None => ([], xq)
    1.82 +    | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
    1.83 +
    1.84 +(*conversion from sequence to list*)
    1.85 +fun list_of xq =
    1.86 +  (case pull xq of
    1.87 +    None => []
    1.88 +  | Some (x, xq') => x :: list_of xq');
    1.89 +
    1.90 +(*conversion from list to sequence*)
    1.91 +fun of_list xs = foldr cons (xs, empty);
    1.92 +
    1.93 +
    1.94 +(*map the function f over the sequence, making a new sequence*)
    1.95 +fun map f xq =
    1.96 +  make (fn () =>
    1.97 +    (case pull xq of
    1.98 +      None => None
    1.99 +    | Some (x, xq') => Some (f x, map f xq')));
   1.100 +
   1.101 +(*map over a sequence xq, append the sequence yq*)
   1.102 +fun mapp f xq yq =
   1.103 +  let
   1.104 +    fun copy s =
   1.105 +      make (fn () =>
   1.106 +        (case pull s of
   1.107 +          None => pull yq
   1.108 +        | Some (x, s') => Some (f x, copy s')))
   1.109 +  in copy xq end;
   1.110 +
   1.111 +(*sequence append:  put the elements of xq in front of those of yq*)
   1.112 +fun append (xq, yq) =
   1.113 +  let
   1.114 +    fun copy s =
   1.115 +      make (fn () =>
   1.116 +        (case pull s of
   1.117 +          None => pull yq
   1.118 +        | Some (x, s') => Some (x, copy s')))
   1.119 +  in copy xq end;
   1.120 +
   1.121 +(*filter sequence by predicate*)
   1.122 +fun filter pred xq =
   1.123 +  let
   1.124 +    fun copy s =
   1.125 +      make (fn () =>
   1.126 +        (case pull s of
   1.127 +          None => None
   1.128 +        | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));
   1.129 +  in copy xq end;
   1.130 +
   1.131 +(*flatten a sequence of sequences to a single sequence*)
   1.132 +fun flat xqq =
   1.133 +  make (fn () =>
   1.134 +    (case pull xqq of
   1.135 +      None => None
   1.136 +    | Some (xq, xqq') => pull (append (xq, flat xqq'))));
   1.137 +
   1.138 +(*interleave elements of xq with those of yq -- fairer than append*)
   1.139 +fun interleave (xq, yq) =
   1.140 +  make (fn () =>
   1.141 +    (case pull xq of
   1.142 +      None => pull yq
   1.143 +    | Some (x, xq') => Some (x, interleave (yq, xq'))));
   1.144 +
   1.145 +
   1.146 +(*functional to print a sequence, up to "count" elements;
   1.147 +  the function prelem should print the element number and also the element*)
   1.148 +fun print prelem count seq =
   1.149 +  let
   1.150 +    fun pr (k, xq) =
   1.151 +      if k > count then ()
   1.152 +      else
   1.153 +        (case pull xq of
   1.154 +          None => ()
   1.155 +        | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
   1.156 +  in pr (1, seq) end;
   1.157 +
   1.158 +(*accumulating a function over a sequence; this is lazy*)
   1.159 +fun it_right f (xq, yq) =
   1.160 +  let
   1.161 +    fun its s =
   1.162 +      make (fn () =>
   1.163 +        (case pull s of
   1.164 +          None => pull yq
   1.165 +        | Some (a, s') => pull (f (a, its s'))))
   1.166 +  in its xq end;
   1.167 +
   1.168 +
   1.169 +
   1.170 +(** sequence functions **)      (*some code duplicated from Pure/tctical.ML*)
   1.171 +
   1.172 +fun succeed x = single x;
   1.173 +fun fail _ = empty;
   1.174 +
   1.175 +
   1.176 +fun THEN (f, g) x = flat (map g (f x));
   1.177 +
   1.178 +fun ORELSE (f, g) x =
   1.179 +  (case pull (f x) of
   1.180 +    None => g x
   1.181 +  | some => make (fn () => some));
   1.182 +
   1.183 +fun APPEND (f, g) x =
   1.184 +  append (f x, make (fn () => pull (g x)));
   1.185 +
   1.186 +
   1.187 +fun EVERY fs = foldr THEN (fs, succeed);
   1.188 +fun FIRST fs = foldr ORELSE (fs, fail);
   1.189 +
   1.190 +
   1.191 +fun TRY f = ORELSE (f, succeed);
   1.192 +
   1.193 +fun REPEAT f =
   1.194 +  let
   1.195 +    fun rep qs x =
   1.196 +      (case pull (f x) of
   1.197 +        None => Some (x, make (fn () => repq qs))
   1.198 +      | Some (x', q) => rep (q :: qs) x')
   1.199 +    and repq [] = None
   1.200 +      | repq (q :: qs) =
   1.201 +          (case pull q of
   1.202 +            None => repq qs
   1.203 +          | Some (x, q) => rep (q :: qs) x);
   1.204 +  in fn x => make (fn () => rep [] x) end;
   1.205 +
   1.206 +
   1.207 +end;
     2.1 --- a/src/Pure/seq.ML	Wed Jun 10 11:52:34 1998 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,204 +0,0 @@
     2.4 -(*  Title:      Pure/seq.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -
     2.8 -Unbounded sequences implemented by closures.  RECOMPUTES if sequence
     2.9 -is re-inspected.  Memoing, using polymorphic refs, was found to be
    2.10 -slower!  (More GCs)
    2.11 -*)
    2.12 -
    2.13 -signature SEQ =
    2.14 -sig
    2.15 -  type 'a seq
    2.16 -  val make: (unit -> ('a * 'a seq) option) -> 'a seq
    2.17 -  val pull: 'a seq -> ('a * 'a seq) option
    2.18 -  val empty: 'a seq
    2.19 -  val cons: 'a * 'a seq -> 'a seq
    2.20 -  val single: 'a -> 'a seq
    2.21 -  val hd: 'a seq -> 'a
    2.22 -  val tl: 'a seq -> 'a seq
    2.23 -  val chop: int * 'a seq -> 'a list * 'a seq
    2.24 -  val list_of: 'a seq -> 'a list
    2.25 -  val of_list: 'a list -> 'a seq
    2.26 -  val map: ('a -> 'b) -> 'a seq -> 'b seq
    2.27 -  val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
    2.28 -  val append: 'a seq * 'a seq -> 'a seq
    2.29 -  val filter: ('a -> bool) -> 'a seq -> 'a seq
    2.30 -  val flat: 'a seq seq -> 'a seq
    2.31 -  val interleave: 'a seq * 'a seq -> 'a seq
    2.32 -  val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
    2.33 -  val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    2.34 -  val succeed: 'a -> 'a seq
    2.35 -  val fail: 'a -> 'b seq
    2.36 -  val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
    2.37 -  val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
    2.38 -  val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
    2.39 -  val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
    2.40 -  val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
    2.41 -  val TRY: ('a -> 'a seq) -> 'a -> 'a seq
    2.42 -  val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
    2.43 -end;
    2.44 -
    2.45 -structure Seq: SEQ =
    2.46 -struct
    2.47 -
    2.48 -
    2.49 -(** lazy sequences **)
    2.50 -
    2.51 -datatype 'a seq = Seq of unit -> ('a * 'a seq) option;
    2.52 -
    2.53 -(*the abstraction for making a sequence*)
    2.54 -val make = Seq;
    2.55 -
    2.56 -(*return next sequence element as None or Some (x, xq)*)
    2.57 -fun pull (Seq f) = f ();
    2.58 -
    2.59 -
    2.60 -(*the empty sequence*)
    2.61 -val empty = Seq (fn () => None);
    2.62 -
    2.63 -(*prefix an element to the sequence -- use cons (x, xq) only if
    2.64 -  evaluation of xq need not be delayed, otherwise use
    2.65 -  make (fn () => Some (x, xq))*)
    2.66 -fun cons x_xq = make (fn () => Some x_xq);
    2.67 -
    2.68 -fun single x = cons (x, empty);
    2.69 -
    2.70 -(*head and tail -- beware of calling the sequence function twice!!*)
    2.71 -fun hd xq = #1 (the (pull xq))
    2.72 -and tl xq = #2 (the (pull xq));
    2.73 -
    2.74 -
    2.75 -(*the list of the first n elements, paired with rest of sequence;
    2.76 -  if length of list is less than n, then sequence had less than n elements*)
    2.77 -fun chop (n, xq) =
    2.78 -  if n <= 0 then ([], xq)
    2.79 -  else
    2.80 -    (case pull xq of
    2.81 -      None => ([], xq)
    2.82 -    | Some (x, xq') => apfst (Library.cons x) (chop (n - 1, xq')));
    2.83 -
    2.84 -(*conversion from sequence to list*)
    2.85 -fun list_of xq =
    2.86 -  (case pull xq of
    2.87 -    None => []
    2.88 -  | Some (x, xq') => x :: list_of xq');
    2.89 -
    2.90 -(*conversion from list to sequence*)
    2.91 -fun of_list xs = foldr cons (xs, empty);
    2.92 -
    2.93 -
    2.94 -(*map the function f over the sequence, making a new sequence*)
    2.95 -fun map f xq =
    2.96 -  make (fn () =>
    2.97 -    (case pull xq of
    2.98 -      None => None
    2.99 -    | Some (x, xq') => Some (f x, map f xq')));
   2.100 -
   2.101 -(*map over a sequence xq, append the sequence yq*)
   2.102 -fun mapp f xq yq =
   2.103 -  let
   2.104 -    fun copy s =
   2.105 -      make (fn () =>
   2.106 -        (case pull s of
   2.107 -          None => pull yq
   2.108 -        | Some (x, s') => Some (f x, copy s')))
   2.109 -  in copy xq end;
   2.110 -
   2.111 -(*sequence append:  put the elements of xq in front of those of yq*)
   2.112 -fun append (xq, yq) =
   2.113 -  let
   2.114 -    fun copy s =
   2.115 -      make (fn () =>
   2.116 -        (case pull s of
   2.117 -          None => pull yq
   2.118 -        | Some (x, s') => Some (x, copy s')))
   2.119 -  in copy xq end;
   2.120 -
   2.121 -(*filter sequence by predicate*)
   2.122 -fun filter pred xq =
   2.123 -  let
   2.124 -    fun copy s =
   2.125 -      make (fn () =>
   2.126 -        (case pull s of
   2.127 -          None => None
   2.128 -        | Some (x, s') => if pred x then Some (x, copy s') else pull (copy s')));
   2.129 -  in copy xq end;
   2.130 -
   2.131 -(*flatten a sequence of sequences to a single sequence*)
   2.132 -fun flat xqq =
   2.133 -  make (fn () =>
   2.134 -    (case pull xqq of
   2.135 -      None => None
   2.136 -    | Some (xq, xqq') => pull (append (xq, flat xqq'))));
   2.137 -
   2.138 -(*interleave elements of xq with those of yq -- fairer than append*)
   2.139 -fun interleave (xq, yq) =
   2.140 -  make (fn () =>
   2.141 -    (case pull xq of
   2.142 -      None => pull yq
   2.143 -    | Some (x, xq') => Some (x, interleave (yq, xq'))));
   2.144 -
   2.145 -
   2.146 -(*functional to print a sequence, up to "count" elements;
   2.147 -  the function prelem should print the element number and also the element*)
   2.148 -fun print prelem count seq =
   2.149 -  let
   2.150 -    fun pr (k, xq) =
   2.151 -      if k > count then ()
   2.152 -      else
   2.153 -        (case pull xq of
   2.154 -          None => ()
   2.155 -        | Some (x, xq') => (prelem k x; writeln ""; pr (k + 1, xq')))
   2.156 -  in pr (1, seq) end;
   2.157 -
   2.158 -(*accumulating a function over a sequence; this is lazy*)
   2.159 -fun it_right f (xq, yq) =
   2.160 -  let
   2.161 -    fun its s =
   2.162 -      make (fn () =>
   2.163 -        (case pull s of
   2.164 -          None => pull yq
   2.165 -        | Some (a, s') => pull (f (a, its s'))))
   2.166 -  in its xq end;
   2.167 -
   2.168 -
   2.169 -
   2.170 -(** sequence functions **)      (*some code duplicated from Pure/tctical.ML*)
   2.171 -
   2.172 -fun succeed x = single x;
   2.173 -fun fail _ = empty;
   2.174 -
   2.175 -
   2.176 -fun THEN (f, g) x = flat (map g (f x));
   2.177 -
   2.178 -fun ORELSE (f, g) x =
   2.179 -  (case pull (f x) of
   2.180 -    None => g x
   2.181 -  | some => make (fn () => some));
   2.182 -
   2.183 -fun APPEND (f, g) x =
   2.184 -  append (f x, make (fn () => pull (g x)));
   2.185 -
   2.186 -
   2.187 -fun EVERY fs = foldr THEN (fs, succeed);
   2.188 -fun FIRST fs = foldr ORELSE (fs, fail);
   2.189 -
   2.190 -
   2.191 -fun TRY f = ORELSE (f, succeed);
   2.192 -
   2.193 -fun REPEAT f =
   2.194 -  let
   2.195 -    fun rep qs x =
   2.196 -      (case pull (f x) of
   2.197 -        None => Some (x, make (fn () => repq qs))
   2.198 -      | Some (x', q) => rep (q :: qs) x')
   2.199 -    and repq [] = None
   2.200 -      | repq (q :: qs) =
   2.201 -          (case pull q of
   2.202 -            None => repq qs
   2.203 -          | Some (x, q) => rep (q :: qs) x);
   2.204 -  in fn x => make (fn () => rep [] x) end;
   2.205 -
   2.206 -
   2.207 -end;