src/Pure/library.ML
changeset 5904 e077a0e66563
parent 5893 c755dfd02509
child 5942 9a7bf515fde1
equal deleted inserted replaced
5903:5d9beee36fbe 5904:e077a0e66563
    73   val hd: 'a list -> 'a
    73   val hd: 'a list -> 'a
    74   val tl: 'a list -> 'a list
    74   val tl: 'a list -> 'a list
    75   val cons: 'a -> 'a list -> 'a list
    75   val cons: 'a -> 'a list -> 'a list
    76   val single: 'a -> 'a list
    76   val single: 'a -> 'a list
    77   val append: 'a list -> 'a list -> 'a list
    77   val append: 'a list -> 'a list -> 'a list
       
    78   val apply: ('a -> 'a) list -> 'a -> 'a
    78   val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
    79   val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
    79   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
    80   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
    80   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    81   val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
    81   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    82   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
    82   val length: 'a list -> int
    83   val length: 'a list -> int
   223   val get_error: 'a error -> string option
   224   val get_error: 'a error -> string option
   224   val get_ok: 'a error -> 'a option
   225   val get_ok: 'a error -> 'a option
   225   val handle_error: ('a -> 'b) -> 'a -> 'b error
   226   val handle_error: ('a -> 'b) -> 'a -> 'b error
   226   exception ERROR_MESSAGE of string
   227   exception ERROR_MESSAGE of string
   227   val transform_error: ('a -> 'b) -> 'a -> 'b
   228   val transform_error: ('a -> 'b) -> 'a -> 'b
       
   229   val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
   228 
   230 
   229   (*timing*)
   231   (*timing*)
   230   val cond_timeit: bool -> (unit -> 'a) -> 'a
   232   val cond_timeit: bool -> (unit -> 'a) -> 'a
   231   val timeit: (unit -> 'a) -> 'a
   233   val timeit: (unit -> 'a) -> 'a
   232   val timeap: ('a -> 'b) -> 'a -> 'b
   234   val timeap: ('a -> 'b) -> 'a -> 'b
   394 
   396 
   395 fun cons x xs = x :: xs;
   397 fun cons x xs = x :: xs;
   396 fun single x = [x];
   398 fun single x = [x];
   397 
   399 
   398 fun append xs ys = xs @ ys;
   400 fun append xs ys = xs @ ys;
       
   401 
       
   402 fun apply [] x = x
       
   403   | apply (f :: fs) x = apply fs (f x);
   399 
   404 
   400 
   405 
   401 (* fold *)
   406 (* fold *)
   402 
   407 
   403 (*the following versions of fold are designed to fit nicely with infixes*)
   408 (*the following versions of fold are designed to fit nicely with infixes*)
  1109   (case handle_error f x of
  1114   (case handle_error f x of
  1110     OK y => y
  1115     OK y => y
  1111   | Error msg => raise ERROR_MESSAGE msg);
  1116   | Error msg => raise ERROR_MESSAGE msg);
  1112 
  1117 
  1113 
  1118 
       
  1119 (* transform any exception, including ERROR *)
       
  1120 
       
  1121 fun transform_failure exn f x =
       
  1122   transform_error f x handle e => raise exn e;
       
  1123 
       
  1124 
  1114 
  1125 
  1115 (** timing **)
  1126 (** timing **)
  1116 
  1127 
  1117 (*a conditional timing function: applies f to () and, if the flag is true,
  1128 (*a conditional timing function: applies f to () and, if the flag is true,
  1118   prints its runtime*)
  1129   prints its runtime*)
  1119 fun cond_timeit flag f =
  1130 fun cond_timeit flag f =
  1120   if flag then
  1131   if flag then
  1121     let val start = startTiming()
  1132     let val start = startTiming()
  1122         val result = f ()
  1133         val result = f ()
  1123     in
  1134     in
  1124 	writeln (endTiming start);  result
  1135         writeln (endTiming start);  result
  1125     end
  1136     end
  1126   else f ();
  1137   else f ();
  1127 
  1138 
  1128 (*unconditional timing function*)
  1139 (*unconditional timing function*)
  1129 fun timeit x = cond_timeit true x;
  1140 fun timeit x = cond_timeit true x;
  1182 
  1193 
  1183 fun transitive_closure [] = []
  1194 fun transitive_closure [] = []
  1184   | transitive_closure ((x, ys)::ps) =
  1195   | transitive_closure ((x, ys)::ps) =
  1185       let val qs = transitive_closure ps
  1196       let val qs = transitive_closure ps
  1186           val zs = foldl (fn (zs, y) => assocs qs y union_string zs) (ys, ys)
  1197           val zs = foldl (fn (zs, y) => assocs qs y union_string zs) (ys, ys)
  1187           fun step(u, us) = (u, if x mem_string us then zs union_string us 
  1198           fun step(u, us) = (u, if x mem_string us then zs union_string us
  1188                                 else us)
  1199                                 else us)
  1189       in (x, zs) :: map step qs end;
  1200       in (x, zs) :: map step qs end;
  1190 
  1201 
  1191 
  1202 
  1192 (* generating identifiers *)
  1203 (* generating identifiers *)
  1193 
  1204 
  1194 (** Freshly generated identifiers; supplied prefix MUST start with a letter **)
  1205 (** Freshly generated identifiers; supplied prefix MUST start with a letter **)
  1195 local
  1206 local
  1196 (*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
  1207 (*Maps 0-63 to A-Z, a-z, 0-9 or _ or ' for generating random identifiers*)
  1197 fun char i =      if i<26 then chr (ord "A" + i)
  1208 fun char i =      if i<26 then chr (ord "A" + i)
  1198 	     else if i<52 then chr (ord "a" + i - 26)
  1209              else if i<52 then chr (ord "a" + i - 26)
  1199 	     else if i<62 then chr (ord"0" + i - 52)
  1210              else if i<62 then chr (ord"0" + i - 52)
  1200 	     else if i=62 then "_"
  1211              else if i=62 then "_"
  1201 	     else  (*i=63*)    "'";
  1212              else  (*i=63*)    "'";
  1202 
  1213 
  1203 val charVec = Vector.tabulate (64, char);
  1214 val charVec = Vector.tabulate (64, char);
  1204 
  1215 
  1205 fun newid n = 
  1216 fun newid n =
  1206   let 
  1217   let
  1207   in  implode (map (fn i => Vector.sub(charVec,i)) (radixpand (64,n)))  end;
  1218   in  implode (map (fn i => Vector.sub(charVec,i)) (radixpand (64,n)))  end;
  1208 
  1219 
  1209 val seedr = ref 0;
  1220 val seedr = ref 0;
  1210 
  1221 
  1211 in
  1222 in
  1217 
  1228 
  1218 
  1229 
  1219 local
  1230 local
  1220 (*Identifies those character codes legal in identifiers.
  1231 (*Identifies those character codes legal in identifiers.
  1221   chould use Basis Library character functions if Poly/ML provided characters*)
  1232   chould use Basis Library character functions if Poly/ML provided characters*)
  1222 fun idCode k = (ord "a" <= k andalso k < ord "z") orelse 
  1233 fun idCode k = (ord "a" <= k andalso k < ord "z") orelse
  1223                (ord "A" <= k andalso k < ord "Z") orelse
  1234                (ord "A" <= k andalso k < ord "Z") orelse
  1224                (ord "0" <= k andalso k < ord "9");
  1235                (ord "0" <= k andalso k < ord "9");
  1225 
  1236 
  1226 val idCodeVec = Vector.tabulate (256, idCode);
  1237 val idCodeVec = Vector.tabulate (256, idCode);
  1227 
  1238 
  1231   If head is "z", bumps chars in tail.
  1242   If head is "z", bumps chars in tail.
  1232   Digits are incremented as if they were integers.
  1243   Digits are incremented as if they were integers.
  1233   "_" and "'" are not changed.
  1244   "_" and "'" are not changed.
  1234   For making variants of identifiers.*)
  1245   For making variants of identifiers.*)
  1235 
  1246 
  1236 fun bump_int_list(c::cs) = 
  1247 fun bump_int_list(c::cs) =
  1237 	if c="9" then "0" :: bump_int_list cs 
  1248         if c="9" then "0" :: bump_int_list cs
  1238 	else
  1249         else
  1239         if "0" <= c andalso c < "9" then chr(ord(c)+1) :: cs
  1250         if "0" <= c andalso c < "9" then chr(ord(c)+1) :: cs
  1240         else "1" :: c :: cs
  1251         else "1" :: c :: cs
  1241   | bump_int_list([]) = error("bump_int_list: not an identifier");
  1252   | bump_int_list([]) = error("bump_int_list: not an identifier");
  1242 
  1253 
  1243 fun bump_list([], d) = [d]
  1254 fun bump_list([], d) = [d]
  1244   | bump_list(["'"], d) = [d, "'"]
  1255   | bump_list(["'"], d) = [d, "'"]
  1245   | bump_list("z"::cs, _) = "a" :: bump_list(cs, "a")
  1256   | bump_list("z"::cs, _) = "a" :: bump_list(cs, "a")
  1246   | bump_list("Z"::cs, _) = "A" :: bump_list(cs, "A")
  1257   | bump_list("Z"::cs, _) = "A" :: bump_list(cs, "A")
  1247   | bump_list("9"::cs, _) = "0" :: bump_int_list cs
  1258   | bump_list("9"::cs, _) = "0" :: bump_int_list cs
  1248   | bump_list(c::cs, _) = 
  1259   | bump_list(c::cs, _) =
  1249         let val k = ord(c)
  1260         let val k = ord(c)
  1250         in if Vector.sub(idCodeVec,k) then chr(k+1) :: cs 
  1261         in if Vector.sub(idCodeVec,k) then chr(k+1) :: cs
  1251 	   else
  1262            else
  1252            if c="'" orelse c="_" then c :: bump_list(cs, "") 
  1263            if c="'" orelse c="_" then c :: bump_list(cs, "")
  1253 	   else error("bump_list: not legal in identifier: " ^
  1264            else error("bump_list: not legal in identifier: " ^
  1254 		      implode(rev(c::cs)))
  1265                       implode(rev(c::cs)))
  1255         end;
  1266         end;
  1256 
  1267 
  1257 end;
  1268 end;
  1258 
  1269 
  1259 fun bump_string s : string = implode (rev (bump_list(rev(explode s), "")));
  1270 fun bump_string s : string = implode (rev (bump_list(rev(explode s), "")));