1(* ===================================================================== *) 2(* FILE : Lib.sml *) 3(* DESCRIPTION : library of useful SML functions. *) 4(* *) 5(* AUTHOR : (c) Konrad Slind, University of Calgary *) 6(* DATE : August 26, 1991 *) 7(* Modified : September 22, 1997, Ken Larsen *) 8(* ===================================================================== *) 9 10structure Lib :> Lib = 11struct 12 13open Feedback; 14 15val ERR = mk_HOL_ERR "Lib" 16 17open Portable; 18datatype frag = datatype HOLPP.frag 19 20(*---------------------------------------------------------------------------* 21 * A version of try that coerces non-HOL_ERR exceptions to be HOL_ERRs. * 22 * To be used with tacticals and the like that get driven by HOL_ERR * 23 * exceptions. * 24 *---------------------------------------------------------------------------*) 25 26local 27 val default_exn = ERR "trye" "original exn. not a HOL_ERR" 28in 29 fun trye f x = 30 f x handle e as HOL_ERR _ => raise e 31 | Interrupt => raise Interrupt 32 | _ => raise default_exn 33end 34 35(*---------------------------------------------------------------------------* 36 * For interactive use: "Raise" prints out the exception. * 37 *---------------------------------------------------------------------------*) 38 39fun try f x = f x handle e => Feedback.Raise e 40 41fun assert P x = assert_exn P x (ERR "assert" "predicate not true") 42 43(*---------------------------------------------------------------------------* 44 * Common list operations * 45 *---------------------------------------------------------------------------*) 46 47(* turning lists into tuples *) 48 49fun singleton_of_list [x] = x 50 | singleton_of_list _ = raise ERR "singleton_of_list" "not a list of length 1" 51 52fun pair_of_list [x, y] = (x, y) 53 | pair_of_list _ = raise ERR "pair_of_list" "not a list of length 2" 54 55fun triple_of_list [x, y, z] = (x, y, z) 56 | triple_of_list _ = raise ERR "triple_of_list" "not a list of length 3" 57 58fun quadruple_of_list [x1, x2, x3, x4] = (x1, x2, x3, x4) 59 | quadruple_of_list _ = raise ERR "quadruple_of_list" "not a list of length 4" 60 61fun tryfind f = 62 let 63 fun F [] = raise ERR "tryfind" "all applications failed" 64 | F (h :: t) = f h handle Interrupt => raise Interrupt | _ => F t 65 in 66 F 67 end 68 69(* Counting starts from 1 *) 70 71fun el n l = 72 if n < 1 73 then raise ERR "el" "index too small" 74 else let 75 fun elem (_, []) = raise ERR "el" "index too large" 76 | elem (1, h :: _) = h 77 | elem (n, _ :: rst) = elem (n - 1, rst) 78 in 79 elem (n, l) 80 end 81 82fun index P l = 83 let 84 fun idx (i, []) = raise ERR "index" "no such element" 85 | idx (i, y :: l) = if P y then i else idx (i + 1, l) 86 in 87 idx (0, l) 88 end 89 90fun map2 f L1 L2 = 91 let 92 fun mp2 [] [] L = rev L 93 | mp2 (a1 :: rst1) (a2 :: rst2) L = mp2 rst1 rst2 (f a1 a2 :: L) 94 | mp2 _ _ _ = raise ERR "map2" "different length lists" 95 in 96 mp2 L1 L2 [] 97 end 98 99fun all2 P = 100 let 101 fun every2 [] [] = true 102 | every2 (a1 :: rst1) (a2 :: rst2) = P a1 a2 andalso every2 rst1 rst2 103 | every2 _ _ = raise ERR "all2" "different length lists" 104 in 105 every2 106 end 107 108fun first P = 109 let 110 fun oneth (a :: rst) = if P a then a else oneth rst 111 | oneth [] = raise ERR "first" "unsatisfied predicate" 112 in 113 oneth 114 end 115 116fun split_after n alist = 117 if n >= 0 118 then let 119 fun spa 0 (L, R) = (rev L, R) 120 | spa n (L, a :: rst) = spa (n - 1) (a :: L, rst) 121 | spa _ _ = raise ERR "split_after" "index too big" 122 in 123 spa n ([], alist) 124 end 125 else raise ERR "split_after" "negative index" 126 127fun itlist2 f L1 L2 base_value = 128 let 129 fun itl ([], []) = base_value 130 | itl (a :: rst1, b :: rst2) = f a b (itl (rst1, rst2)) 131 | itl _ = raise ERR "itlist2" "lists of different length" 132 in 133 itl (L1, L2) 134 end 135 136fun rev_itlist2 f L1 L2 = 137 let 138 fun rev_it2 ([], []) base = base 139 | rev_it2 (a :: rst1, b :: rst2) base = rev_it2 (rst1, rst2) (f a b base) 140 | rev_it2 _ _ = raise ERR"rev_itlist2" "lists of different length" 141 in 142 rev_it2 (L1, L2) 143 end 144 145fun end_itlist f = 146 let 147 fun endit [] = raise ERR "end_itlist" "list too short" 148 | endit [x] = x 149 | endit (h :: t) = f h (endit t) 150 in 151 endit 152 end 153 154fun get_first f l = 155 case l of 156 [] => NONE 157 | h :: t => (case f h of NONE => get_first f t | some => some) 158 159fun zip [] [] = [] 160 | zip (a :: b) (c :: d) = (a, c) :: zip b d 161 | zip _ _ = raise ERR "zip" "different length lists" 162 163fun combine (l1, l2) = zip l1 l2 164 165fun front_last l = 166 let 167 fun fl _ [] = raise ERR "front_last" "empty list" 168 | fl acc [x] = (List.rev acc, x) 169 | fl acc (h :: t) = fl (h :: acc) t 170 in 171 fl [] l 172 end 173 174fun butlast l = 175 fst (front_last l) handle HOL_ERR _ => raise ERR "butlast" "empty list" 176 177fun last [] = raise ERR "last" "empty list" 178 | last [x] = x 179 | last (_ :: t) = last t 180 181fun pluck P = 182 let 183 fun pl _ [] = raise ERR "pluck" "predicate not satisfied" 184 | pl A (h :: t) = 185 if P h then (h, List.revAppend (A, t)) else pl (h :: A) t 186 in 187 pl [] 188 end 189 190fun trypluck f = 191 let 192 fun try acc [] = raise ERR "trypluck" "no successful fn. application" 193 | try acc (h :: t) = 194 case total f h of 195 NONE => try (h :: acc) t 196 | SOME v => (v, List.revAppend (acc, t)) 197 in 198 try [] 199 end 200 201(* apnth : ('a -> 'a) -> int -> 'a list -> 'a list 202 apply a function to the nth member of a list *) 203fun apnth f 0 (y :: ys) = f y :: ys 204 | apnth f n (y :: ys) = y :: apnth f (n-1) ys 205 | apnth f n [] = raise ERR "apnth" "list too short (or -ve index)" 206 207fun mapshape [] _ _ = [] 208 | mapshape (n :: nums) (f :: funcs) all_args = 209 let 210 val (fargs, rst) = split_after n all_args 211 in 212 f fargs :: mapshape nums funcs rst 213 end 214 | mapshape _ _ _ = raise ERR "mapshape" "irregular lists" 215 216(*---------------------------------------------------------------------------* 217 * Assoc lists. * 218 *---------------------------------------------------------------------------*) 219 220fun assoc item = 221 let 222 fun assc ((key, ob) :: rst) = if item = key then ob else assc rst 223 | assc [] = raise ERR "assoc" "not found" 224 in 225 assc 226 end 227 228fun rev_assoc item = 229 let 230 fun assc ((ob, key) :: rst) = if item = key then ob else assc rst 231 | assc [] = raise ERR "assoc" "not found" 232 in 233 assc 234 end 235 236fun op_assoc eq_func k l = 237 case l of 238 [] => raise ERR "op_assoc" "not found" 239 | (key,ob) :: rst => if eq_func k key then ob else op_assoc eq_func k rst 240 241(*---------------------------------------------------------------------------*) 242(* Topologically sort a list wrt partial order R. *) 243(*---------------------------------------------------------------------------*) 244 245fun topsort R = 246 let 247 fun pred_of y x = R x y 248 fun a1 l1 l2 = l1 @ l2 249 fun a2 l1 l2 = foldl (op ::) l2 l1 250 fun deps [] _ acc = acc 251 | deps (h :: t) front (nodeps, rst) = 252 let 253 val pred_of_h = pred_of h 254 val hdep = exists pred_of_h t orelse exists pred_of_h front 255 val acc = if hdep then (nodeps, h :: rst) else (h :: nodeps, rst) 256 in 257 deps t (h :: front) acc 258 end 259 fun loop _ [] = [] 260 | loop (a1, a2) l = 261 case (deps l [] ([], [])) of 262 ([], _) => raise ERR "topsort" "cyclic dependency" 263 | (nodeps, rst) => a1 nodeps (loop (a2, a1) rst) 264 in 265 loop (a2, a1) 266 end 267 268(* for the following two implementations, 269 each node appears before all its dependencies 270 in the returned list *) 271 272(* O(n*log(n)) time version 273 deps = map from nodes to adjacency lists *) 274 275fun dict_topsort deps = 276 let 277 open Redblackmap 278 val deps = transform (fn ls => ref (SOME ls)) deps 279 fun visit (n, ls) = 280 let 281 val r = find (deps, n) 282 in 283 case !r of 284 NONE => ls 285 | SOME dl => let 286 val _ = r := NONE 287 val ls = List.foldl visit ls dl 288 in 289 n :: ls 290 end 291 end 292 fun v (n, _, ls) = visit (n, ls) 293 in 294 foldl v [] deps 295 end 296 297(*---------------------------------------------------------------------------* 298 * Strings. * 299 *---------------------------------------------------------------------------*) 300 301val string_to_int = 302 partial (ERR "string_to_int" "not convertable") Int.fromString 303 304val saying = ref true 305 306fun say s = if !saying then !Feedback.MESG_outstream s else () 307 308fun unprime s = 309 let 310 val n = size s - 1 311 in 312 if 0 <= n andalso String.sub (s, n) = #"'" 313 then String.substring (s, 0, n) 314 else raise ERR "unprime" "string doesn't end with a prime" 315 end 316 317fun unprefix pfx s = 318 if String.isPrefix pfx s 319 then String.extract (s, size pfx, NONE) 320 else raise ERR "unprefix" "1st argument is not a prefix of 2nd argument" 321 322fun ppstring pf x = HOLPP.pp_to_string (!Globals.linewidth) pf x 323 324fun delete_trailing_wspace s = 325 let 326 val toks = String.fields (equal #"\n") s 327 fun do1 i s = 328 if i < 0 then "" 329 else if Char.isSpace (String.sub(s,i)) then do1 (i - 1) s 330 else String.extract(s,0,SOME(i + 1)) 331 fun remove_rptd_nls i cnt s = 332 if i < 0 then if cnt > 0 then "\n" else "" 333 else if String.sub(s,i) = #"\n" then 334 remove_rptd_nls (i - 1) (cnt + 1) s 335 else String.extract(s,0,SOME(i + 1 + (if cnt > 0 then 1 else 0))) 336 val s1 = String.concatWith "\n" (map (fn s => do1 (size s - 1) s) toks) 337 in 338 remove_rptd_nls (size s1 - 1) 0 s1 339 end 340 341(*---------------------------------------------------------------------------* 342 * Timing * 343 *---------------------------------------------------------------------------*) 344 345local 346 val second = Time.fromReal 1.0 347 val minute = Time.fromReal 60.0 348 val year0 = Date.year (Date.fromTimeUniv Time.zeroTime) 349 fun to_str i u = if i = 0 then "" else Int.toString i ^ u 350in 351 fun time_to_string t = 352 if Time.< (t, second) 353 then Time.fmt 5 t ^ "s" 354 else if Time.< (t, minute) 355 then Time.fmt 1 t ^ "s" 356 else let 357 val d = Date.fromTimeUniv t 358 val years = Date.year d - year0 359 val days = Date.yearDay d 360 val hours = Date.hour d 361 val minutes = Date.minute d 362 in 363 if years + days + hours = 0 andalso minutes < 10 then 364 to_str minutes "m" ^ Date.fmt "%Ss" d 365 else to_str years "y" ^ to_str days "d" ^ to_str hours "h" ^ 366 Date.fmt "%Mm%Ss" d 367 end 368end 369 370fun start_time () = Timer.startCPUTimer () 371 372fun end_time timer = 373 let 374 val {sys, usr} = Timer.checkCPUTimer timer 375 val gc = Timer.checkGCTime timer 376 in 377 say ("runtime: " ^ time_to_string usr ^ ",\ 378 \ gctime: " ^ time_to_string gc ^ ", \ 379 \ systime: " ^ time_to_string sys ^ ".\n") 380 end 381 382fun time f x = 383 let 384 val timer = start_time () 385 val y = f x handle e => (end_time timer; raise e) 386 in 387 end_time timer; y 388 end 389 390fun start_real_time () = Timer.startRealTimer () 391 392fun end_real_time timer = 393 say ("realtime: " ^ Time.toString (Timer.checkRealTimer timer) ^ "s\n") 394 395fun real_time f x = 396 let 397 val timer = start_real_time () 398 val y = f x handle e => (end_real_time timer; raise e) 399 in 400 end_real_time timer; y 401 end 402 403(* set helpers/abbreviations *) 404type 'a set = 'a HOLset.set 405fun op Un p = HOLset.union p 406fun op Isct p = HOLset.intersection p 407fun op -- p = HOLset.difference p 408fun op IN (e,s) = HOLset.member(s,e) 409 410end (* Lib *) 411