src/Pure/library.ML
 changeset 380 daca5b594fb3 parent 265 443dc2c37583 child 410 c8171ee32744
```--- a/src/Pure/library.ML	Thu May 19 14:06:37 1994 +0200
+++ b/src/Pure/library.ML	Thu May 19 16:12:37 1994 +0200
@@ -17,6 +17,10 @@
fun I x = x;
fun K x y = x;

+(*reverse apply*)
+infix also;
+fun (x also f) = f x;
+
(*combine two functions forming the union of their domains*)
infix orelf;
fun f orelf g = fn x => f x handle Match => g x;
@@ -118,6 +122,13 @@
in boolf end;

+(* flags *)
+
+fun set flag = (flag := true; true);
+fun reset flag = (flag := false; false);
+fun toggle flag = (flag := not (! flag); ! flag);
+
+

(** lists **)

@@ -240,8 +251,25 @@
| Some y => y :: mapfilter f xs);

+fun find_first _ [] = None
+  | find_first pred (x :: xs) =
+      if pred x then Some x else find_first pred xs;
+
+
(* lists of pairs *)

+fun map2 _ ([], []) = []
+  | map2 f (x :: xs, y :: ys) = (f (x, y) :: map2 f (xs, ys))
+  | map2 _ _ = raise LIST "map2";
+
+fun exists2 _ ([], []) = false
+  | exists2 pred (x :: xs, y :: ys) = pred (x, y) orelse exists2 pred (xs, ys)
+  | exists2 _ _ = raise LIST "exists2";
+
+fun forall2 _ ([], []) = true
+  | forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys)
+  | forall2 _ _ = raise LIST "forall2";
+
(*combine two lists forming a list of pairs:
[x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
infix ~~;
@@ -249,10 +277,6 @@
| (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
| _ ~~ _ = raise LIST "~~";

-(*combine two lists*)
-fun map2 _ ([], []) = []
-  | map2 f (x :: xs, y :: ys) = (f (x, y) :: map2 f (xs, ys))
-  | map2 _ _ = raise LIST "map2";

(*inverse of ~~; the old 'split':
[(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
@@ -386,6 +410,7 @@
fun space_implode a bs = implode (separate a bs);

val commas = space_implode ", ";
+val commas_quote = commas o map quote;

(*concatenate messages, one per line, into a string*)
val cat_lines = space_implode "\n";
@@ -566,6 +591,11 @@
val extend_list = generic_extend (op =) I I;
val merge_lists = generic_merge (op =) I I;

+fun merge_rev_lists xs [] = xs
+  | merge_rev_lists [] ys = ys
+  | merge_rev_lists xs (y :: ys) =
+      (if y mem xs then I else cons y) (merge_rev_lists xs ys);
+

(** balanced trees **)
@@ -612,7 +642,7 @@
(*print error message and abort to top level*)
exception ERROR;
fun error msg = (writeln msg; raise ERROR);
-fun sys_error msg = (writeln "*** System Error ***"; error msg);
+fun sys_error msg = (writeln "*** SYSTEM ERROR ***"; error msg);

fun assert p msg = if p then () else error msg;
fun deny p msg = if p then error msg else ();```