src/Pure/library.ML
changeset 5904 e077a0e66563
parent 5893 c755dfd02509
child 5942 9a7bf515fde1
     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;