added infix op also: 'a * ('a -> 'b) -> 'b;
authorwenzelm
Thu May 19 16:12:37 1994 +0200 (1994-05-19)
changeset 380daca5b594fb3
parent 379 c1e3c8508fd2
child 381 8af09380c517
added infix op also: 'a * ('a -> 'b) -> 'b;
added set, reset, toggle: bool ref -> bool;
added find_first, exists2, forall2, commas_quote, merge_rev_lists;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu May 19 14:06:37 1994 +0200
     1.2 +++ b/src/Pure/library.ML	Thu May 19 16:12:37 1994 +0200
     1.3 @@ -17,6 +17,10 @@
     1.4  fun I x = x;
     1.5  fun K x y = x;
     1.6  
     1.7 +(*reverse apply*)
     1.8 +infix also;
     1.9 +fun (x also f) = f x;
    1.10 +
    1.11  (*combine two functions forming the union of their domains*)
    1.12  infix orelf;
    1.13  fun f orelf g = fn x => f x handle Match => g x;
    1.14 @@ -118,6 +122,13 @@
    1.15    in boolf end;
    1.16  
    1.17  
    1.18 +(* flags *)
    1.19 +
    1.20 +fun set flag = (flag := true; true);
    1.21 +fun reset flag = (flag := false; false);
    1.22 +fun toggle flag = (flag := not (! flag); ! flag);
    1.23 +
    1.24 +
    1.25  
    1.26  (** lists **)
    1.27  
    1.28 @@ -240,8 +251,25 @@
    1.29        | Some y => y :: mapfilter f xs);
    1.30  
    1.31  
    1.32 +fun find_first _ [] = None
    1.33 +  | find_first pred (x :: xs) =
    1.34 +      if pred x then Some x else find_first pred xs;
    1.35 +
    1.36 +
    1.37  (* lists of pairs *)
    1.38  
    1.39 +fun map2 _ ([], []) = []
    1.40 +  | map2 f (x :: xs, y :: ys) = (f (x, y) :: map2 f (xs, ys))
    1.41 +  | map2 _ _ = raise LIST "map2";
    1.42 +
    1.43 +fun exists2 _ ([], []) = false
    1.44 +  | exists2 pred (x :: xs, y :: ys) = pred (x, y) orelse exists2 pred (xs, ys)
    1.45 +  | exists2 _ _ = raise LIST "exists2";
    1.46 +
    1.47 +fun forall2 _ ([], []) = true
    1.48 +  | forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys)
    1.49 +  | forall2 _ _ = raise LIST "forall2";
    1.50 +
    1.51  (*combine two lists forming a list of pairs:
    1.52    [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
    1.53  infix ~~;
    1.54 @@ -249,10 +277,6 @@
    1.55    | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
    1.56    | _ ~~ _ = raise LIST "~~";
    1.57  
    1.58 -(*combine two lists*)
    1.59 -fun map2 _ ([], []) = []
    1.60 -  | map2 f (x :: xs, y :: ys) = (f (x, y) :: map2 f (xs, ys))
    1.61 -  | map2 _ _ = raise LIST "map2";
    1.62  
    1.63  (*inverse of ~~; the old 'split':
    1.64    [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
    1.65 @@ -386,6 +410,7 @@
    1.66  fun space_implode a bs = implode (separate a bs);
    1.67  
    1.68  val commas = space_implode ", ";
    1.69 +val commas_quote = commas o map quote;
    1.70  
    1.71  (*concatenate messages, one per line, into a string*)
    1.72  val cat_lines = space_implode "\n";
    1.73 @@ -566,6 +591,11 @@
    1.74  val extend_list = generic_extend (op =) I I;
    1.75  val merge_lists = generic_merge (op =) I I;
    1.76  
    1.77 +fun merge_rev_lists xs [] = xs
    1.78 +  | merge_rev_lists [] ys = ys
    1.79 +  | merge_rev_lists xs (y :: ys) =
    1.80 +      (if y mem xs then I else cons y) (merge_rev_lists xs ys);
    1.81 +
    1.82  
    1.83  
    1.84  (** balanced trees **)
    1.85 @@ -612,7 +642,7 @@
    1.86  (*print error message and abort to top level*)
    1.87  exception ERROR;
    1.88  fun error msg = (writeln msg; raise ERROR);
    1.89 -fun sys_error msg = (writeln "*** System Error ***"; error msg);
    1.90 +fun sys_error msg = (writeln "*** SYSTEM ERROR ***"; error msg);
    1.91  
    1.92  fun assert p msg = if p then () else error msg;
    1.93  fun deny p msg = if p then error msg else ();