src/Pure/library.ML

-(*  Title:      library
+(*  Title:      Pure/library.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
 
 Basic library: booleans, lists, pairs, input/output, etc.

 fun hd   []   = raise LIST "hd"
   | hd (a::_) = a;
 
 fun tl   []   = raise LIST "tl"
   | 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);

 (*Return nth element of l, where 0 designates the first element;
   raise EXCEPTION if list too short.*)
 fun nth_elem NL = case (drop NL) of
     []   => raise LIST "nth_elem" 
   | 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 =

         | insert (x, y::ys) = 
               if less(y,x) then y :: insert (x,ys) else x::y::ys;
       fun sort1 [] = []
         | 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) =
       let val qs = transitive_closure ps

   let fun take (rxs, []) = (rev rxs, [])
 	| take (rxs, x::xs) =
 	    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)
   | _ prefix _ = false;
 

   | separate _ xs = xs;
 
 (*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*)
 val cat_lines = implode o (map (apr(op^,"\n")));
 

 
 (*Merge splitted filename (path and file);
   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 =
   let val (file,_) = take_prefix (apr(op<>,".")) (rev (explode name))
   in implode (rev file) end;