src/Pure/library.ML
changeset 14106 bbf708a7e27f
parent 13794 332eb2e69a65
child 14472 cba7c0a3ffb3
equal deleted inserted replaced
14105:85d1a908f024 14106:bbf708a7e27f
   239   val sort: ('a * 'a -> order) -> 'a list -> 'a list
   239   val sort: ('a * 'a -> order) -> 'a list -> 'a list
   240   val sort_strings: string list -> string list
   240   val sort_strings: string list -> string list
   241   val sort_wrt: ('a -> string) -> 'a list -> 'a list
   241   val sort_wrt: ('a -> string) -> 'a list -> 'a list
   242   val unique_strings: string list -> string list
   242   val unique_strings: string list -> string list
   243 
   243 
       
   244   (*random numbers*)
       
   245   exception RANDOM
       
   246   val random: unit -> real
       
   247   val random_range: int -> int -> int
       
   248   val one_of: 'a list -> 'a
       
   249   val frequency: (int * 'a) list -> 'a
       
   250 
   244   (*I/O and diagnostics*)
   251   (*I/O and diagnostics*)
   245   val cd: string -> unit
   252   val cd: string -> unit
   246   val pwd: unit -> string
   253   val pwd: unit -> string
   247   val writeln_fn: (string -> unit) ref
   254   val writeln_fn: (string -> unit) ref
   248   val priority_fn: (string -> unit) ref
   255   val priority_fn: (string -> unit) ref
  1133   | unique_strings (x :: y :: ys) =
  1140   | unique_strings (x :: y :: ys) =
  1134       if x = y then unique_strings (y :: ys)
  1141       if x = y then unique_strings (y :: ys)
  1135       else x :: unique_strings (y :: ys);
  1142       else x :: unique_strings (y :: ys);
  1136 
  1143 
  1137 
  1144 
       
  1145 (** random numbers **)
       
  1146 
       
  1147 exception RANDOM;
       
  1148 
       
  1149 fun rmod x y = x - y * real (Real.floor (x / y));
       
  1150 
       
  1151 local
       
  1152   val a = 16807.0;
       
  1153   val m = 2147483647.0;
       
  1154   val random_seed = ref 1.0;
       
  1155 in
       
  1156 
       
  1157 fun random () =
       
  1158   let val r = rmod (a * !random_seed) m
       
  1159   in (random_seed := r; r) end;
       
  1160 
       
  1161 end;
       
  1162 
       
  1163 fun random_range l h =
       
  1164   if h < l orelse l < 0 then raise RANDOM
       
  1165   else l + Real.floor (rmod (random ()) (real (h - l + 1)));
       
  1166 
       
  1167 fun one_of xs = nth_elem (random_range 0 (length xs - 1), xs);
       
  1168 
       
  1169 fun frequency xs =
       
  1170   let
       
  1171     val sum = foldl op + (0, map fst xs);
       
  1172     fun pick n ((k, x) :: xs) =
       
  1173       if n <= k then x else pick (n - k) xs
       
  1174   in pick (random_range 1 sum) xs end;
       
  1175 
       
  1176 
  1138 (** input / output and diagnostics **)
  1177 (** input / output and diagnostics **)
  1139 
  1178 
  1140 val cd = OS.FileSys.chDir;
  1179 val cd = OS.FileSys.chDir;
  1141 val pwd = OS.FileSys.getDir;
  1180 val pwd = OS.FileSys.getDir;
  1142 
  1181