added commute: 'a seq list -> 'a list seq;
authorwenzelm
Thu Jul 08 18:29:30 1999 +0200 (1999-07-08)
changeset 692783759063fbbd
parent 6926 7ffc131909e5
child 6928 9b4cd97b459d
added commute: 'a seq list -> 'a list seq;
src/Pure/General/seq.ML
     1.1 --- a/src/Pure/General/seq.ML	Thu Jul 08 18:29:07 1999 +0200
     1.2 +++ b/src/Pure/General/seq.ML	Thu Jul 08 18:29:30 1999 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4    val interleave: 'a seq * 'a seq -> 'a seq
     1.5    val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
     1.6    val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
     1.7 +  val commute: 'a seq list -> 'a list seq
     1.8    val succeed: 'a -> 'a seq
     1.9    val fail: 'a -> 'b seq
    1.10    val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
    1.11 @@ -163,6 +164,18 @@
    1.12          | Some (a, s') => pull (f (a, its s'))))
    1.13    in its xq end;
    1.14  
    1.15 +(*turn a list of sequences into a sequence of lists*)
    1.16 +fun commute [] = single []
    1.17 +  | commute (xq :: xqs) =
    1.18 +      make (fn () =>
    1.19 +        (case pull xq of
    1.20 +          None => None
    1.21 +        | Some (x, xq') =>
    1.22 +            (case pull (commute xqs) of
    1.23 +              None => None
    1.24 +            | Some (xs, xsq) =>
    1.25 +                Some (x :: xs, append (map (Library.cons x) xsq, commute (xq' :: xqs))))));
    1.26 +
    1.27  
    1.28  
    1.29  (** sequence functions **)      (*some code duplicated from Pure/tctical.ML*)