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