src/Pure/library.ML
 changeset 41 97aae241094b parent 24 f3d4ff75d9f2 child 160 80ccb6c354ba
```     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 =
```