--- a/src/Pure/library.ML Fri Oct 08 12:33:17 1993 +0100
+++ b/src/Pure/library.ML Fri Oct 08 12:35:53 1993 +0100
@@ -1,4 +1,4 @@
-(* Title: library
+(* Title: Pure/library.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
@@ -51,6 +51,13 @@
| tl (_::l) = l;
+(*curried cons and reverse cons*)
+
+fun cons x xs = x :: xs;
+
+fun rcons xs x = x :: xs;
+
+
(*curried functions for pairing and reversed pairing*)
fun pair x y = (x,y);
fun rpair x y = (y,x);
@@ -132,6 +139,12 @@
| x::l => x;
+(*Last element of a list*)
+fun last_elem [] = raise LIST "last_elem"
+ | last_elem [x] = x
+ | last_elem (_ :: xs) = last_elem xs;
+
+
(*make the list [from, from+1, ..., to]*)
infix upto;
fun from upto to =
@@ -470,6 +483,10 @@
| sort1 (x::xs) = insert (x, sort1 xs)
in sort1 end;
+(*sort strings*)
+val sort_strings = sort (op <= : string * string -> bool);
+
+
(*Transitive Closure. Not Warshall's algorithm*)
fun transitive_closure [] = []
| transitive_closure ((x,ys)::ps) =
@@ -558,6 +575,15 @@
if pred x then take(x::rxs, xs) else (rev rxs, x::xs)
in take([],xs) end;
+(* [x1,...,xi,...,xn] ---> ([x1,...,xi], [x(i+1),..., xn])
+ where xi is the last element that does not satisfy the predicate*)
+fun take_suffix _ [] = ([], [])
+ | take_suffix pred (x :: xs) =
+ (case take_suffix pred xs of
+ ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx)
+ | (prfx, sffx) => (x :: prfx, sffx));
+
+
infix prefix;
fun [] prefix _ = true
| (x::xs) prefix (y::ys) = (x=y) andalso (xs prefix ys)
@@ -570,6 +596,7 @@
(*space_implode "..." (explode "hello"); gives "h...e...l...l...o" *)
fun space_implode a bs = implode (separate a bs);
+(*simple quoting (does not escape special chars) *)
fun quote s = "\"" ^ s ^ "\"";
(*Concatenate messages, one per line, into a string*)
@@ -597,8 +624,8 @@
if path does not end with one a slash is appended *)
fun tack_on "" name = name
| tack_on path name =
- if (hd (rev (explode path))) = "/" then path ^ name
- else path ^ "/" ^ name;
+ if last_elem (explode path) = "/" then path ^ name
+ else path ^ "/" ^ name;
(*Remove the extension of a filename, i.e. the part after the last '.' *)
fun remove_ext name =