added foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list;
authorwenzelm
Mon May 25 21:10:45 1998 +0200 (1998-05-25)
changeset 4956a7538e43896e
parent 4955 a9fa93e1a86e
child 4957 30c49821e61f
added foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list;
added seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit;
tuned 'beginning';
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon May 25 12:55:01 1998 +0200
     1.2 +++ b/src/Pure/library.ML	Mon May 25 21:10:45 1998 +0200
     1.3 @@ -73,6 +73,7 @@
     1.4    val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
     1.5    val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
     1.6    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
     1.7 +  val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
     1.8    val length: 'a list -> int
     1.9    val take: int * 'a list -> 'a list
    1.10    val drop: int * 'a list -> 'a list
    1.11 @@ -96,6 +97,7 @@
    1.12    val map2: ('a * 'b -> 'c) -> 'a list * 'b list -> 'c list
    1.13    val exists2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.14    val forall2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.15 +  val seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit
    1.16    val ~~ : 'a list * 'b list -> ('a * 'b) list
    1.17    val split_list: ('a * 'b) list -> 'a list * 'b list
    1.18    val prefix: ''a list * ''a list -> bool
    1.19 @@ -412,6 +414,13 @@
    1.20          | itr (x::l) = f(x, itr l)
    1.21    in  itr l  end;
    1.22  
    1.23 +fun foldl_map _ (x, []) = (x, [])
    1.24 +  | foldl_map f (x, y :: ys) =
    1.25 +      let
    1.26 +        val (x', y') = f (x, y);
    1.27 +        val (x'', ys') = foldl_map f (x', ys);
    1.28 +      in (x'', y' :: ys') end;
    1.29 +
    1.30  
    1.31  (* basic list functions *)
    1.32  
    1.33 @@ -540,6 +549,10 @@
    1.34    | forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys)
    1.35    | forall2 _ _ = raise LIST "forall2";
    1.36  
    1.37 +fun seq2 _ ([], []) = ()
    1.38 +  | seq2 f (x :: xs, y :: ys) = (f (x, y); seq2 f (xs, ys))
    1.39 +  | seq2 _ _ = raise LIST "seq2";
    1.40 +
    1.41  (*combine two lists forming a list of pairs:
    1.42    [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
    1.43  fun [] ~~ [] = []
    1.44 @@ -625,7 +638,8 @@
    1.45  (** strings **)
    1.46  
    1.47  (*beginning of text*)
    1.48 -fun beginning cs = implode (take (10, cs)) ^ " ...";
    1.49 +fun beginning cs =
    1.50 +  implode (map (fn c => if ord c < ord " " then " " else c) (take (10, cs))) ^ " ...";
    1.51  
    1.52  (*enclose in brackets*)
    1.53  fun enclose lpar rpar str = lpar ^ str ^ rpar;