1.1 --- a/src/Pure/library.ML Tue Nov 17 14:05:47 1998 +0100
1.2 +++ b/src/Pure/library.ML Tue Nov 17 14:06:32 1998 +0100
1.3 @@ -75,6 +75,7 @@
1.4 val cons: 'a -> 'a list -> 'a list
1.5 val single: 'a -> 'a list
1.6 val append: 'a list -> 'a list -> 'a list
1.7 + val apply: ('a -> 'a) list -> 'a -> 'a
1.8 val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
1.9 val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
1.10 val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
1.11 @@ -225,6 +226,7 @@
1.12 val handle_error: ('a -> 'b) -> 'a -> 'b error
1.13 exception ERROR_MESSAGE of string
1.14 val transform_error: ('a -> 'b) -> 'a -> 'b
1.15 + val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
1.16
1.17 (*timing*)
1.18 val cond_timeit: bool -> (unit -> 'a) -> 'a
1.19 @@ -397,6 +399,9 @@
1.20
1.21 fun append xs ys = xs @ ys;
1.22
1.23 +fun apply [] x = x
1.24 + | apply (f :: fs) x = apply fs (f x);
1.25 +
1.26
1.27 (* fold *)
1.28
1.29 @@ -1111,6 +1116,12 @@
1.30 | Error msg => raise ERROR_MESSAGE msg);
1.31
1.32
1.33 +(* transform any exception, including ERROR *)
1.34 +
1.35 +fun transform_failure exn f x =
1.36 + transform_error f x handle e => raise exn e;
1.37 +
1.38 +
1.39
1.40 (** timing **)
1.41
1.42 @@ -1121,7 +1132,7 @@
1.43 let val start = startTiming()
1.44 val result = f ()
1.45 in
1.46 - writeln (endTiming start); result
1.47 + writeln (endTiming start); result
1.48 end
1.49 else f ();
1.50
1.51 @@ -1184,7 +1195,7 @@
1.52 | transitive_closure ((x, ys)::ps) =
1.53 let val qs = transitive_closure ps
1.54 val zs = foldl (fn (zs, y) => assocs qs y union_string zs) (ys, ys)
1.55 - fun step(u, us) = (u, if x mem_string us then zs union_string us
1.56 + fun step(u, us) = (u, if x mem_string us then zs union_string us
1.57 else us)
1.58 in (x, zs) :: map step qs end;
1.59
1.60 @@ -1195,15 +1206,15 @@
1.61 local
1.62 (*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
1.63 fun char i = if i<26 then chr (ord "A" + i)
1.64 - else if i<52 then chr (ord "a" + i - 26)
1.65 - else if i<62 then chr (ord"0" + i - 52)
1.66 - else if i=62 then "_"
1.67 - else (*i=63*) "'";
1.68 + else if i<52 then chr (ord "a" + i - 26)
1.69 + else if i<62 then chr (ord"0" + i - 52)
1.70 + else if i=62 then "_"
1.71 + else (*i=63*) "'";
1.72
1.73 val charVec = Vector.tabulate (64, char);
1.74
1.75 -fun newid n =
1.76 - let
1.77 +fun newid n =
1.78 + let
1.79 in implode (map (fn i => Vector.sub(charVec,i)) (radixpand (64,n))) end;
1.80
1.81 val seedr = ref 0;
1.82 @@ -1219,7 +1230,7 @@
1.83 local
1.84 (*Identifies those character codes legal in identifiers.
1.85 chould use Basis Library character functions if Poly/ML provided characters*)
1.86 -fun idCode k = (ord "a" <= k andalso k < ord "z") orelse
1.87 +fun idCode k = (ord "a" <= k andalso k < ord "z") orelse
1.88 (ord "A" <= k andalso k < ord "Z") orelse
1.89 (ord "0" <= k andalso k < ord "9");
1.90
1.91 @@ -1233,9 +1244,9 @@
1.92 "_" and "'" are not changed.
1.93 For making variants of identifiers.*)
1.94
1.95 -fun bump_int_list(c::cs) =
1.96 - if c="9" then "0" :: bump_int_list cs
1.97 - else
1.98 +fun bump_int_list(c::cs) =
1.99 + if c="9" then "0" :: bump_int_list cs
1.100 + else
1.101 if "0" <= c andalso c < "9" then chr(ord(c)+1) :: cs
1.102 else "1" :: c :: cs
1.103 | bump_int_list([]) = error("bump_int_list: not an identifier");
1.104 @@ -1245,13 +1256,13 @@
1.105 | bump_list("z"::cs, _) = "a" :: bump_list(cs, "a")
1.106 | bump_list("Z"::cs, _) = "A" :: bump_list(cs, "A")
1.107 | bump_list("9"::cs, _) = "0" :: bump_int_list cs
1.108 - | bump_list(c::cs, _) =
1.109 + | bump_list(c::cs, _) =
1.110 let val k = ord(c)
1.111 - in if Vector.sub(idCodeVec,k) then chr(k+1) :: cs
1.112 - else
1.113 - if c="'" orelse c="_" then c :: bump_list(cs, "")
1.114 - else error("bump_list: not legal in identifier: " ^
1.115 - implode(rev(c::cs)))
1.116 + in if Vector.sub(idCodeVec,k) then chr(k+1) :: cs
1.117 + else
1.118 + if c="'" orelse c="_" then c :: bump_list(cs, "")
1.119 + else error("bump_list: not legal in identifier: " ^
1.120 + implode(rev(c::cs)))
1.121 end;
1.122
1.123 end;