added cons, rcons, last_elem, sort_strings, take_suffix;
authorwenzelm
Fri Oct 08 12:35:53 1993 +0100 (1993-10-08)
changeset 4197aae241094b
parent 40 3f9f8395519e
child 42 d981488bda7b
added cons, rcons, last_elem, sort_strings, take_suffix;
improved tack_on;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Fri Oct 08 12:33:17 1993 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Oct 08 12:35:53 1993 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      library
     1.5 +(*  Title:      Pure/library.ML
     1.6      ID:         $Id$
     1.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1992  University of Cambridge
     1.9 @@ -51,6 +51,13 @@
    1.10    | tl (_::l) = l;
    1.11  
    1.12  
    1.13 +(*curried cons and reverse cons*)
    1.14 +
    1.15 +fun cons x xs = x :: xs;
    1.16 +
    1.17 +fun rcons xs x = x :: xs;
    1.18 +
    1.19 +
    1.20  (*curried functions for pairing and reversed pairing*)
    1.21  fun pair x y = (x,y);
    1.22  fun rpair x y = (y,x);
    1.23 @@ -132,6 +139,12 @@
    1.24    | x::l => x;
    1.25  
    1.26  
    1.27 +(*Last element of a list*)
    1.28 +fun last_elem [] = raise LIST "last_elem"
    1.29 +  | last_elem [x] = x
    1.30 +  | last_elem (_ :: xs) = last_elem xs;
    1.31 +
    1.32 +
    1.33  (*make the list [from, from+1, ..., to]*)
    1.34  infix upto;
    1.35  fun from upto to =
    1.36 @@ -470,6 +483,10 @@
    1.37          | sort1 (x::xs) = insert (x, sort1 xs)
    1.38    in  sort1  end;
    1.39  
    1.40 +(*sort strings*)
    1.41 +val sort_strings = sort (op <= : string * string -> bool);
    1.42 +
    1.43 +
    1.44  (*Transitive Closure. Not Warshall's algorithm*)
    1.45  fun transitive_closure [] = []
    1.46    | transitive_closure ((x,ys)::ps) =
    1.47 @@ -558,6 +575,15 @@
    1.48  	    if  pred x  then  take(x::rxs, xs)  else  (rev rxs, x::xs)
    1.49    in  take([],xs)  end;
    1.50  
    1.51 +(* [x1,...,xi,...,xn]  --->  ([x1,...,xi], [x(i+1),..., xn])
    1.52 +   where xi is the last element that does not satisfy the predicate*)
    1.53 +fun take_suffix _ [] = ([], [])
    1.54 +  | take_suffix pred (x :: xs) =
    1.55 +      (case take_suffix pred xs of
    1.56 +        ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx)
    1.57 +      | (prfx, sffx) => (x :: prfx, sffx));
    1.58 +
    1.59 +
    1.60  infix prefix;
    1.61  fun [] prefix _ = true
    1.62    | (x::xs) prefix (y::ys) = (x=y) andalso (xs prefix ys)
    1.63 @@ -570,6 +596,7 @@
    1.64  (*space_implode "..." (explode "hello");  gives  "h...e...l...l...o" *)
    1.65  fun space_implode a bs = implode (separate a bs); 
    1.66  
    1.67 +(*simple quoting (does not escape special chars) *)
    1.68  fun quote s = "\"" ^ s ^ "\"";
    1.69  
    1.70  (*Concatenate messages, one per line, into a string*)
    1.71 @@ -597,8 +624,8 @@
    1.72    if path does not end with one a slash is appended *)
    1.73  fun tack_on "" name = name
    1.74    | tack_on path name =
    1.75 -      if (hd (rev (explode path))) = "/" then path ^ name
    1.76 -                                         else path ^ "/" ^ name;
    1.77 +      if last_elem (explode path) = "/" then path ^ name
    1.78 +      else path ^ "/" ^ name;
    1.79  
    1.80  (*Remove the extension of a filename, i.e. the part after the last '.' *)
    1.81  fun remove_ext name =