src/Pure/library.ML
changeset 41 97aae241094b
parent 24 f3d4ff75d9f2
child 160 80ccb6c354ba
equal deleted inserted replaced
40:3f9f8395519e 41:97aae241094b
     1 (*  Title:      library
     1 (*  Title:      Pure/library.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Basic library: booleans, lists, pairs, input/output, etc.
     6 Basic library: booleans, lists, pairs, input/output, etc.
    47 fun hd   []   = raise LIST "hd"
    47 fun hd   []   = raise LIST "hd"
    48   | hd (a::_) = a;
    48   | hd (a::_) = a;
    49 
    49 
    50 fun tl   []   = raise LIST "tl"
    50 fun tl   []   = raise LIST "tl"
    51   | tl (_::l) = l;
    51   | tl (_::l) = l;
       
    52 
       
    53 
       
    54 (*curried cons and reverse cons*)
       
    55 
       
    56 fun cons x xs = x :: xs;
       
    57 
       
    58 fun rcons xs x = x :: xs;
    52 
    59 
    53 
    60 
    54 (*curried functions for pairing and reversed pairing*)
    61 (*curried functions for pairing and reversed pairing*)
    55 fun pair x y = (x,y);
    62 fun pair x y = (x,y);
    56 fun rpair x y = (y,x);
    63 fun rpair x y = (y,x);
   128 (*Return nth element of l, where 0 designates the first element;
   135 (*Return nth element of l, where 0 designates the first element;
   129   raise EXCEPTION if list too short.*)
   136   raise EXCEPTION if list too short.*)
   130 fun nth_elem NL = case (drop NL) of
   137 fun nth_elem NL = case (drop NL) of
   131     []   => raise LIST "nth_elem" 
   138     []   => raise LIST "nth_elem" 
   132   | x::l => x;
   139   | x::l => x;
       
   140 
       
   141 
       
   142 (*Last element of a list*)
       
   143 fun last_elem [] = raise LIST "last_elem"
       
   144   | last_elem [x] = x
       
   145   | last_elem (_ :: xs) = last_elem xs;
   133 
   146 
   134 
   147 
   135 (*make the list [from, from+1, ..., to]*)
   148 (*make the list [from, from+1, ..., to]*)
   136 infix upto;
   149 infix upto;
   137 fun from upto to =
   150 fun from upto to =
   467         | insert (x, y::ys) = 
   480         | insert (x, y::ys) = 
   468               if less(y,x) then y :: insert (x,ys) else x::y::ys;
   481               if less(y,x) then y :: insert (x,ys) else x::y::ys;
   469       fun sort1 [] = []
   482       fun sort1 [] = []
   470         | sort1 (x::xs) = insert (x, sort1 xs)
   483         | sort1 (x::xs) = insert (x, sort1 xs)
   471   in  sort1  end;
   484   in  sort1  end;
       
   485 
       
   486 (*sort strings*)
       
   487 val sort_strings = sort (op <= : string * string -> bool);
       
   488 
   472 
   489 
   473 (*Transitive Closure. Not Warshall's algorithm*)
   490 (*Transitive Closure. Not Warshall's algorithm*)
   474 fun transitive_closure [] = []
   491 fun transitive_closure [] = []
   475   | transitive_closure ((x,ys)::ps) =
   492   | transitive_closure ((x,ys)::ps) =
   476       let val qs = transitive_closure ps
   493       let val qs = transitive_closure ps
   556   let fun take (rxs, []) = (rev rxs, [])
   573   let fun take (rxs, []) = (rev rxs, [])
   557 	| take (rxs, x::xs) =
   574 	| take (rxs, x::xs) =
   558 	    if  pred x  then  take(x::rxs, xs)  else  (rev rxs, x::xs)
   575 	    if  pred x  then  take(x::rxs, xs)  else  (rev rxs, x::xs)
   559   in  take([],xs)  end;
   576   in  take([],xs)  end;
   560 
   577 
       
   578 (* [x1,...,xi,...,xn]  --->  ([x1,...,xi], [x(i+1),..., xn])
       
   579    where xi is the last element that does not satisfy the predicate*)
       
   580 fun take_suffix _ [] = ([], [])
       
   581   | take_suffix pred (x :: xs) =
       
   582       (case take_suffix pred xs of
       
   583         ([], sffx) => if pred x then ([], x :: sffx) else ([x], sffx)
       
   584       | (prfx, sffx) => (x :: prfx, sffx));
       
   585 
       
   586 
   561 infix prefix;
   587 infix prefix;
   562 fun [] prefix _ = true
   588 fun [] prefix _ = true
   563   | (x::xs) prefix (y::ys) = (x=y) andalso (xs prefix ys)
   589   | (x::xs) prefix (y::ys) = (x=y) andalso (xs prefix ys)
   564   | _ prefix _ = false;
   590   | _ prefix _ = false;
   565 
   591 
   568   | separate _ xs = xs;
   594   | separate _ xs = xs;
   569 
   595 
   570 (*space_implode "..." (explode "hello");  gives  "h...e...l...l...o" *)
   596 (*space_implode "..." (explode "hello");  gives  "h...e...l...l...o" *)
   571 fun space_implode a bs = implode (separate a bs); 
   597 fun space_implode a bs = implode (separate a bs); 
   572 
   598 
       
   599 (*simple quoting (does not escape special chars) *)
   573 fun quote s = "\"" ^ s ^ "\"";
   600 fun quote s = "\"" ^ s ^ "\"";
   574 
   601 
   575 (*Concatenate messages, one per line, into a string*)
   602 (*Concatenate messages, one per line, into a string*)
   576 val cat_lines = implode o (map (apr(op^,"\n")));
   603 val cat_lines = implode o (map (apr(op^,"\n")));
   577 
   604 
   595 
   622 
   596 (*Merge splitted filename (path and file);
   623 (*Merge splitted filename (path and file);
   597   if path does not end with one a slash is appended *)
   624   if path does not end with one a slash is appended *)
   598 fun tack_on "" name = name
   625 fun tack_on "" name = name
   599   | tack_on path name =
   626   | tack_on path name =
   600       if (hd (rev (explode path))) = "/" then path ^ name
   627       if last_elem (explode path) = "/" then path ^ name
   601                                          else path ^ "/" ^ name;
   628       else path ^ "/" ^ name;
   602 
   629 
   603 (*Remove the extension of a filename, i.e. the part after the last '.' *)
   630 (*Remove the extension of a filename, i.e. the part after the last '.' *)
   604 fun remove_ext name =
   631 fun remove_ext name =
   605   let val (file,_) = take_prefix (apr(op<>,".")) (rev (explode name))
   632   let val (file,_) = take_prefix (apr(op<>,".")) (rev (explode name))
   606   in implode (rev file) end;
   633   in implode (rev file) end;