src/Pure/library.ML
changeset 21395 f34ac19659ae
parent 21335 6b9d4a19a3a8
child 21479 63e7eb863ae6
     1.1 --- a/src/Pure/library.ML	Thu Nov 16 01:07:23 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Nov 16 01:07:25 2006 +0100
     1.3 @@ -5,15 +5,16 @@
     1.4  
     1.5  Basic library: functions, options, pairs, booleans, lists, integers,
     1.6  strings, lists as sets, balanced trees, orders, current directory, misc.
     1.7 +
     1.8 +See also General/basics.ML for the most fundamental concepts.
     1.9  *)
    1.10  
    1.11 -infix 1 |> |-> ||> ||>> |>> #> #-> ##> ##>> #>> |>>> ;
    1.12 -infix 2 ?;
    1.13 -infix 3 o oo ooo oooo;
    1.14 -
    1.15 -infix 4 ~~ upto downto;
    1.16 +infix 1 |>>>
    1.17 +infix 2 ?
    1.18 +infix 3 o oo ooo oooo
    1.19 +infix 4 ~~ upto downto
    1.20  infix orf andf \ \\ mem mem_int mem_string union union_int
    1.21 -  union_string inter inter_int inter_string subset subset_int subset_string;
    1.22 +  union_string inter inter_int inter_string subset subset_int subset_string
    1.23  
    1.24  signature BASIC_LIBRARY =
    1.25  sig
    1.26 @@ -22,37 +23,14 @@
    1.27    val K: 'a -> 'b -> 'a
    1.28    val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
    1.29    val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
    1.30 -  val |> : 'a * ('a -> 'b) -> 'b
    1.31 -  val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b
    1.32 -  val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
    1.33 -  val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
    1.34 -  val |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c
    1.35 -  val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
    1.36 -  val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd
    1.37 -  val ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd
    1.38 -  val ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd
    1.39 -  val #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b
    1.40    val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
    1.41    val ? : ('a -> bool) * ('a -> 'a) -> 'a -> 'a
    1.42 -  val ` : ('b -> 'a) -> 'b -> 'a * 'b
    1.43 -  val tap: ('b -> 'a) -> 'b -> 'b
    1.44    val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    1.45    val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    1.46    val oooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'f -> 'a) -> 'c -> 'd -> 'e -> 'f -> 'b
    1.47    val funpow: int -> ('a -> 'a) -> 'a -> 'a
    1.48  
    1.49 -  (*options*)
    1.50 -  val the: 'a option -> 'a
    1.51 -  val these: 'a list option -> 'a list
    1.52 -  val the_default: 'a -> 'a option -> 'a
    1.53 -  val the_list: 'a option -> 'a list
    1.54 -  val is_some: 'a option -> bool
    1.55 -  val is_none: 'a option -> bool
    1.56 -  val perhaps: ('a -> 'a option) -> 'a -> 'a
    1.57 -
    1.58    (*exceptions*)
    1.59 -  val try: ('a -> 'b) -> 'a -> 'b option
    1.60 -  val can: ('a -> 'b) -> 'a -> bool
    1.61    exception EXCEPTION of exn * string
    1.62    val do_transform_failure: bool ref
    1.63    val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
    1.64 @@ -102,22 +80,17 @@
    1.65  
    1.66    (*lists*)
    1.67    exception UnequalLengths
    1.68 -  val cons: 'a -> 'a list -> 'a list
    1.69    val single: 'a -> 'a list
    1.70    val the_single: 'a list -> 'a
    1.71    val singleton: ('a list -> 'b list) -> 'a -> 'b
    1.72 -  val append: 'a list -> 'a list -> 'a list
    1.73    val apply: ('a -> 'a) list -> 'a -> 'a
    1.74 -  val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.75 -  val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    1.76 -  val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
    1.77    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    1.78    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    1.79    val flat: 'a list list -> 'a list
    1.80 -  val maps: ('a -> 'b list) -> 'a list -> 'b list
    1.81    val unflat: 'a list list -> 'b list -> 'b list list
    1.82    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
    1.83    val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
    1.84 +  val maps: ('a -> 'b list) -> 'a list -> 'b list
    1.85    val chop: int -> 'a list -> 'a list * 'a list
    1.86    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    1.87    val nth: 'a list -> int -> 'a
    1.88 @@ -290,36 +263,19 @@
    1.89  structure Library: LIBRARY =
    1.90  struct
    1.91  
    1.92 -
    1.93 -(** functions **)
    1.94 +(* functions *)
    1.95  
    1.96  fun I x = x;
    1.97  fun K x = fn _ => x;
    1.98  fun curry f x y = f (x, y);
    1.99  fun uncurry f (x, y) = f x y;
   1.100  
   1.101 -(*reverse application and structured results*)
   1.102 -fun x |> f = f x;
   1.103 -fun (x, y) |-> f = f x y;
   1.104 -fun (x, y) |>> f = (f x, y);
   1.105 -fun (x, y) ||> f = (x, f y);
   1.106 +(*application and structured results -- old version*)
   1.107  fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
   1.108 -fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
   1.109 -
   1.110 -(*reverse composition and structured results*)
   1.111 -fun f #> g = g o f;
   1.112 -fun f #-> g = uncurry g o f;
   1.113 -fun (f ##> g) x = let val (y, z) = f x in (y, g z) end;
   1.114 -fun (f ##>> g) x = let val (y, z) = f x; val (w, u) = g z in ((y, w), u) end;
   1.115 -fun (f #>> g) x = let val (y, z) = f x in (g y, z) end;
   1.116  
   1.117  (*conditional application*)
   1.118  fun b ? f = fn x => if b x then f x else x;
   1.119  
   1.120 -(*view results*)
   1.121 -fun `f = fn x => (f x, x);
   1.122 -fun tap f = fn x => (f x; x);
   1.123 -
   1.124  (*composition with multiple args*)
   1.125  fun (f oo g) x y = f (g x y);
   1.126  fun (f ooo g) x y z = f (g x y z);
   1.127 @@ -332,28 +288,6 @@
   1.128    in rep (n, x) end;
   1.129  
   1.130  
   1.131 -(** options **)
   1.132 -
   1.133 -val the = Option.valOf;
   1.134 -
   1.135 -fun these (SOME x) = x
   1.136 -  | these _ = [];
   1.137 -
   1.138 -fun the_default x (SOME y) = y
   1.139 -  | the_default x _ = x;
   1.140 -
   1.141 -fun the_list (SOME x) = [x]
   1.142 -  | the_list _ = []
   1.143 -
   1.144 -fun is_some (SOME _) = true
   1.145 -  | is_some NONE = false;
   1.146 -
   1.147 -fun is_none (SOME _) = false
   1.148 -  | is_none NONE = true;
   1.149 -
   1.150 -fun perhaps f x = the_default x (f x);
   1.151 -
   1.152 -
   1.153  (* exceptions *)
   1.154  
   1.155  val do_transform_failure = ref true;
   1.156 @@ -365,13 +299,6 @@
   1.157  
   1.158  exception EXCEPTION of exn * string;
   1.159  
   1.160 -
   1.161 -fun try f x = SOME (f x)
   1.162 -  handle Interrupt => raise Interrupt | _ => NONE;
   1.163 -
   1.164 -fun can f x = is_some (try f x);
   1.165 -
   1.166 -
   1.167  datatype 'a result =
   1.168    Result of 'a |
   1.169    Exn of exn;
   1.170 @@ -409,7 +336,7 @@
   1.171    in ass list end;
   1.172  
   1.173  
   1.174 -(** pairs **)
   1.175 +(* pairs *)
   1.176  
   1.177  fun pair x y = (x, y);
   1.178  fun rpair x y = (y, x);
   1.179 @@ -431,20 +358,16 @@
   1.180  fun string_of_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
   1.181  
   1.182  
   1.183 -(** booleans **)
   1.184 +(* booleans *)
   1.185  
   1.186 -(* equality *)
   1.187 -
   1.188 +(*polymorphic equality*)
   1.189  fun equal x y = x = y;
   1.190  fun not_equal x y = x <> y;
   1.191  
   1.192 -(* operators for combining predicates *)
   1.193 -
   1.194 +(*combining predicates*)
   1.195  fun p orf q = fn x => p x orelse q x;
   1.196  fun p andf q = fn x => p x andalso q x;
   1.197  
   1.198 -(* predicates on lists *)
   1.199 -
   1.200  (*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
   1.201  fun exists (pred: 'a -> bool) : 'a list -> bool =
   1.202    let fun boolf [] = false
   1.203 @@ -481,12 +404,11 @@
   1.204  fun conditional b f = if b then f () else ();
   1.205  
   1.206  
   1.207 +
   1.208  (** lists **)
   1.209  
   1.210  exception UnequalLengths;
   1.211  
   1.212 -fun cons x xs = x :: xs;
   1.213 -
   1.214  fun single x = [x];
   1.215  
   1.216  fun the_single [x] = x
   1.217 @@ -494,35 +416,11 @@
   1.218  
   1.219  fun singleton f x = the_single (f [x]);
   1.220  
   1.221 -fun append xs ys = xs @ ys;
   1.222 -
   1.223  fun apply [] x = x
   1.224    | apply (f :: fs) x = apply fs (f x);
   1.225  
   1.226  
   1.227 -(* fold *)
   1.228 -
   1.229 -fun fold f =
   1.230 -  let
   1.231 -    fun fold_aux [] y = y
   1.232 -      | fold_aux (x :: xs) y = fold_aux xs (f x y);
   1.233 -  in fold_aux end;
   1.234 -
   1.235 -fun fold_rev f =
   1.236 -  let
   1.237 -    fun fold_aux [] y = y
   1.238 -      | fold_aux (x :: xs) y = f x (fold_aux xs y);
   1.239 -  in fold_aux end;
   1.240 -
   1.241 -fun fold_map f =
   1.242 -  let
   1.243 -    fun fold_aux [] y = ([], y)
   1.244 -      | fold_aux (x :: xs) y =
   1.245 -          let
   1.246 -            val (x', y') = f x y;
   1.247 -            val (xs', y'') = fold_aux xs y';
   1.248 -          in (x' :: xs', y'') end;
   1.249 -  in fold_aux end;
   1.250 +(* fold -- old versions *)
   1.251  
   1.252  (*the following versions of fold are designed to fit nicely with infixes*)
   1.253  
   1.254 @@ -570,9 +468,7 @@
   1.255  fun maps f [] = []
   1.256    | maps f (x :: xs) = f x @ maps f xs;
   1.257  
   1.258 -fun chop 0 xs = ([], xs)
   1.259 -  | chop _ [] = ([], [])
   1.260 -  | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
   1.261 +fun chop n xs = unfold_rev n dest xs;
   1.262  
   1.263  (*take the first n elements from a list*)
   1.264  fun take (n, []) = []