src/Pure/library.ML
changeset 23220 9e04da929160
parent 23202 98736a2fec98
child 23251 471b576aad25
     1.1 --- a/src/Pure/library.ML	Sun Jun 03 23:16:47 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Sun Jun 03 23:16:48 2007 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    (*functions*)
     1.5    val I: 'a -> 'a
     1.6    val K: 'a -> 'b -> 'a
     1.7 +  val flip: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
     1.8    val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
     1.9    val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
    1.10    val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
    1.11 @@ -129,7 +130,6 @@
    1.12    val dec: int ref -> int
    1.13    val upto: int * int -> int list
    1.14    val downto: int * int -> int list
    1.15 -  val downto0: int list * int -> bool
    1.16    val radixpand: int * int -> int list
    1.17    val radixstring: int * string * int -> string
    1.18    val string_of_int: int -> string
    1.19 @@ -159,7 +159,6 @@
    1.20    val suffix: string -> string -> string
    1.21    val unprefix: string -> string -> string
    1.22    val unsuffix: string -> string -> string
    1.23 -  val plural: 'a -> 'a -> 'b list -> 'a
    1.24    val replicate_string: int -> string -> string
    1.25    val translate_string: (string -> string) -> string -> string
    1.26  
    1.27 @@ -193,14 +192,9 @@
    1.28    val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
    1.29    val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
    1.30  
    1.31 -  (* lists as multisets *)
    1.32 +  (*lists as multisets*)
    1.33    val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
    1.34 -  val gen_submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.35 -
    1.36 -  (*lists as tables -- see also Pure/General/alist.ML*)
    1.37 -  val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
    1.38 -  val merge_lists: ''a list -> ''a list -> ''a list
    1.39 -  val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
    1.40 +  val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.41  
    1.42    (*balanced trees*)
    1.43    exception Balance
    1.44 @@ -256,7 +250,6 @@
    1.45    val take: int * 'a list -> 'a list
    1.46    val drop: int * 'a list -> 'a list
    1.47    val last_elem: 'a list -> 'a
    1.48 -  val seq: ('a -> unit) -> 'a list -> unit
    1.49  end;
    1.50  
    1.51  structure Library: LIBRARY =
    1.52 @@ -266,6 +259,7 @@
    1.53  
    1.54  fun I x = x;
    1.55  fun K x = fn _ => x;
    1.56 +fun flip f x y = f y x;
    1.57  fun curry f x y = f (x, y);
    1.58  fun uncurry f (x, y) = f x y;
    1.59  
    1.60 @@ -346,7 +340,6 @@
    1.61  
    1.62  fun swap (x, y) = (y, x);
    1.63  
    1.64 -(*apply function to components*)
    1.65  fun apfst f (x, y) = (f x, y);
    1.66  fun apsnd f (x, y) = (x, f y);
    1.67  fun pairself f (x, y) = (f x, f y);
    1.68 @@ -457,7 +450,9 @@
    1.69  fun maps f [] = []
    1.70    | maps f (x :: xs) = f x @ maps f xs;
    1.71  
    1.72 -fun chop n xs = unfold_rev n dest xs;
    1.73 +fun chop 0 xs = ([], xs)
    1.74 +  | chop _ [] = ([], [])
    1.75 +  | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
    1.76  
    1.77  (*take the first n elements from a list*)
    1.78  fun take (n, []) = []
    1.79 @@ -541,10 +536,6 @@
    1.80  fun fold_burrow f xss s =
    1.81    apfst (unflat xss) (f (flat xss) s);
    1.82  
    1.83 -(*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
    1.84 -  (proc x1; ...; proc xn) for side effects*)
    1.85 -val seq = List.app;
    1.86 -
    1.87  (*separate s [x1, x2, ..., xn]  ===>  [x1, s, x2, s, ..., s, xn]*)
    1.88  fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs
    1.89    | separate _ xs = xs;
    1.90 @@ -586,12 +577,9 @@
    1.91    | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
    1.92    | map2 _ _ _ = raise UnequalLengths;
    1.93  
    1.94 -fun fold2 f =
    1.95 -  let
    1.96 -    fun fold_aux [] [] z = z
    1.97 -      | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z)
    1.98 -      | fold_aux _ _ _ = raise UnequalLengths;
    1.99 -  in fold_aux end;
   1.100 +fun fold2 f [] [] z = z
   1.101 +  | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
   1.102 +  | fold2 f _ _ _ = raise UnequalLengths;
   1.103  
   1.104  fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
   1.105    | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
   1.106 @@ -625,10 +613,10 @@
   1.107  
   1.108  fun chop_prefix eq ([], ys) = ([], ([], ys))
   1.109    | chop_prefix eq (xs, []) = ([], (xs, []))
   1.110 -  | chop_prefix eq (xs as x::xs', ys as y::ys') =
   1.111 +  | chop_prefix eq (xs as x :: xs', ys as y :: ys') =
   1.112        if eq (x, y) then
   1.113          let val (ps', xys'') = chop_prefix eq (xs', ys')
   1.114 -        in (x::ps', xys'') end
   1.115 +        in (x :: ps', xys'') end
   1.116        else ([], (xs, ys));
   1.117  
   1.118  (* [x1, ..., xi, ..., xn]  --->  ([x1, ..., xi], [x(i+1), ..., xn])
   1.119 @@ -647,6 +635,8 @@
   1.120  fun suffixes1 xs = map rev (prefixes1 (rev xs));
   1.121  fun suffixes xs = [] :: suffixes1 xs;
   1.122  
   1.123 +
   1.124 +
   1.125  (** integers **)
   1.126  
   1.127  fun gcd (x, y) =
   1.128 @@ -670,10 +660,6 @@
   1.129  fun (i downto j) =
   1.130    if i < j then [] else i :: (i - 1 downto j);
   1.131  
   1.132 -(*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
   1.133 -fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1)
   1.134 -  | downto0 ([], n) = n = ~1;
   1.135 -
   1.136  
   1.137  (* convert integers to strings *)
   1.138  
   1.139 @@ -699,8 +685,8 @@
   1.140  fun signed_string_of_int i =
   1.141    if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i;
   1.142  
   1.143 -fun string_of_indexname (a,0) = a
   1.144 -  | string_of_indexname (a,i) = a ^ "_" ^ Int.toString i;
   1.145 +fun string_of_indexname (a, 0) = a
   1.146 +  | string_of_indexname (a, i) = a ^ "_" ^ string_of_int i;
   1.147  
   1.148  
   1.149  (* read integers *)
   1.150 @@ -797,10 +783,6 @@
   1.151    if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
   1.152    else raise Fail "unsuffix";
   1.153  
   1.154 -(* Ex: "The variable" ^ plural " is" "s are" vs *)
   1.155 -fun plural sg pl [x] = sg
   1.156 -  | plural sg pl _ = pl
   1.157 -
   1.158  fun replicate_string 0 _ = ""
   1.159    | replicate_string 1 a = a
   1.160    | replicate_string k a =
   1.161 @@ -808,6 +790,7 @@
   1.162        else replicate_string (k div 2) (a ^ a) ^ a;
   1.163  
   1.164  
   1.165 +
   1.166  (** lists as sets -- see also Pure/General/ord_list.ML **)
   1.167  
   1.168  (*canonical member, insert, remove*)
   1.169 @@ -935,24 +918,15 @@
   1.170    in dups end;
   1.171  
   1.172  
   1.173 +
   1.174  (** lists as multisets **)
   1.175  
   1.176  fun remove1 _ _ [] = raise Empty
   1.177 -  | remove1 eq y (x::xs) = if eq(y,x) then xs else x :: remove1 eq y xs;
   1.178 -
   1.179 -fun gen_submultiset _  ([],    _)  = true
   1.180 -  | gen_submultiset eq (x::xs, ys) =
   1.181 -      member eq ys x  andalso  gen_submultiset eq (xs, remove1 eq x ys);
   1.182 -
   1.183 +  | remove1 eq y (x::xs) = if eq (y, x) then xs else x :: remove1 eq y xs;
   1.184  
   1.185 -(** association lists -- legacy operations **)
   1.186 +fun submultiset _ ([], _)  = true
   1.187 +  | submultiset eq (x :: xs, ys) = member eq ys x andalso submultiset eq (xs, remove1 eq x ys);
   1.188  
   1.189 -fun gen_merge_lists _ xs [] = xs
   1.190 -  | gen_merge_lists _ [] ys = ys
   1.191 -  | gen_merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
   1.192 -
   1.193 -fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
   1.194 -fun merge_alists xs = gen_merge_lists (eq_fst (op =)) xs;
   1.195  
   1.196  
   1.197  (** balanced trees **)
   1.198 @@ -1093,6 +1067,7 @@
   1.199    in pick (random_range 1 sum) xs end;
   1.200  
   1.201  
   1.202 +
   1.203  (** current directory **)
   1.204  
   1.205  val cd = OS.FileSys.chDir;