1(* ===================================================================== *) 2(* FILE : Portable.sml *) 3(* DESCRIPTION : Structure for SML System dependent functions. *) 4(* AUTHOR : Ken Larsen, University of Cambridge (or DTU) *) 5(* based on code by *) 6(* Elsa L. Gunter, AT&T Bell Laboratories *) 7(* DATE : 19 September, 1997 *) 8(* ===================================================================== *) 9 10(* Copyright 1993 by AT&T Bell Laboratories *) 11(* Copyright 1997 by University of Cambridge *) 12 13(* Share and Enjoy *) 14 15structure Portable :> Portable = 16struct 17 18structure Process = OS.Process 19structure FileSys = OS.FileSys 20 21exception Div = General.Div 22exception Mod = General.Div 23 24fun assert_exn P x e = if P x then x else raise e 25fun with_exn f x e = f x handle Interrupt => raise Interrupt | _ => raise e 26 27val int_to_string = Int.toString 28 29(*---------------------------------------------------------------------------* 30 * Combinators * 31 *---------------------------------------------------------------------------*) 32 33fun curry f x y = f (x, y) 34fun uncurry f (x, y) = f x y 35infix 3 ## 36fun (f ## g) (x, y) = (f x, g y) 37fun apfst f (x, y) = (f x, y) 38fun apsnd f (x, y) = (x, f y) 39infix |> ||> |>> ||-> 40fun x |> f = f x 41fun (x,y) |>> f = (f x, y) 42fun (x,y) ||> f = (x, f y) 43fun (x,y) ||-> f = f x y 44infixr $ ? 45fun f $ x = f x 46fun (b ? f) x = if b then f x else x 47fun C f x y = f y x 48fun I x = x 49fun K x y = x 50fun S f g x = f x (g x) 51fun W f x = f x x 52 53(*---------------------------------------------------------------------------* 54 * Curried versions of infixes. * 55 *---------------------------------------------------------------------------*) 56 57fun append l1 l2 = l1 @ l2 58fun equal x y = x = y 59val strcat = curry (op ^) 60fun cons a L = a :: L 61fun pair x y = (x, y) 62 63fun rpair x y = (y, x) 64fun swap (x, y) = (y, x) 65fun fst (x, _) = x 66fun snd (_, y) = y 67 68fun triple x y z = (x, y, z) 69fun quadruple x1 x2 x3 x4 = (x1, x2, x3, x4) 70 71(*---------------------------------------------------------------------------* 72 * Success and failure. Interrupt has a special status in Standard ML. * 73 *---------------------------------------------------------------------------*) 74 75fun can f x = (f x; true) handle Interrupt => raise Interrupt | _ => false 76 77fun total f x = SOME (f x) handle Interrupt => raise Interrupt | _ => NONE 78 79fun partial e f x = case f x of SOME y => y | NONE => raise e 80 81fun these (SOME x) = x 82 | these NONE = [] 83 84(* ---------------------------------------------------------------------- 85 Lists 86 ---------------------------------------------------------------------- *) 87 88fun list_of_singleton a = [a] 89fun single a = [a] 90fun the_single [x] = x 91 | the_single _ = raise List.Empty; 92fun singleton f x = the_single (f [x]) 93 94fun list_of_pair (a, b) = [a, b] 95fun list_of_triple (a, b, c) = [a, b, c] 96fun list_of_quadruple (a, b, c, d) = [a, b, c, d] 97 98fun the_list NONE = [] 99 | the_list (SOME x) = [x] 100fun the_default d NONE = d 101 | the_default _ (SOME x) = x 102 103val all = List.all 104val exists = List.exists 105 106fun first_opt f = 107 let 108 fun fo n [] = NONE 109 | fo n (a :: rst) = 110 let 111 val vo = f n a handle Interrupt => raise Interrupt | _ => NONE 112 in 113 if isSome vo then vo else fo (n + 1) rst 114 end 115 in 116 fo 0 117 end 118 119fun itlist f L base_value = List.foldr (uncurry f) base_value L 120val foldr' = itlist 121 122fun rev_itlist f L base_value = List.foldl (uncurry f) base_value L 123val foldl' = rev_itlist 124 125fun foldl_map _ (acc, []) = (acc, []) 126 | foldl_map f (acc, x :: xs) = 127 let 128 val (acc', y) = f (acc, x) 129 val (acc'', ys) = foldl_map f (acc', xs) 130 in 131 (acc'', y :: ys) 132 end 133 134fun foldl2' _ [] [] z = z 135 | foldl2' f (x::xs) (y::ys) z = foldl2' f xs ys (f x y z) 136 | foldl2' _ _ _ _ = raise ListPair.UnequalLengths 137fun foldr2' _ [] [] z = z 138 | foldr2' f (x::xs) (y::ys) z = f x y (foldr2' f xs ys z) 139 | foldr2' _ _ _ _ = raise ListPair.UnequalLengths 140 141(* separate s [x1, x2, ..., xn] ===> [x1, s, x2, s, ..., s, xn] *) 142 143fun separate s (x :: (xs as _ :: _)) = x :: s :: separate s xs 144 | separate _ xs = xs 145 146val filter = List.filter 147fun filter_out P = filter (not o P) 148 149val partition = List.partition 150 151fun pull_prefix ps l = 152 case ps of 153 [] => l 154 | p :: rest => 155 let 156 val (s, l0) = List.partition p l 157 in 158 s @ pull_prefix rest l0 159 end 160 161val unzip = ListPair.unzip 162val split = unzip 163 164fun mapfilter f list = 165 itlist (fn i => fn L => (f i :: L) 166 handle Interrupt => raise Interrupt 167 | otherwise => L) 168 list [] 169 170val flatten = List.concat 171 172fun trypluck' f list = 173 let 174 fun recurse acc l = 175 case l of 176 [] => (NONE, list) 177 | h :: t => (case f h of 178 NONE => recurse (h :: acc) t 179 | SOME v => (SOME v, List.revAppend (acc, t))) 180 in 181 recurse [] list 182 end 183 184fun funpow n f x = 185 let 186 fun iter (0, res) = res 187 | iter (n, res) = iter (n - 1, f res) 188 in 189 if n < 0 then x else iter (n, x) 190 end 191 192fun repeat f = 193 let 194 exception LAST of 'a 195 fun loop x = 196 let 197 val y = (f x handle Interrupt => raise Interrupt 198 | otherwise => raise (LAST x)) 199 in 200 loop y 201 end 202 in 203 fn x => loop x handle (LAST y) => y 204 end 205 206fun enumerate i [] = [] 207 | enumerate i (h :: t) = (i, h) :: enumerate (i + 1) t 208 209fun upto b t = 210 let 211 fun up i A = if i > t then A else up (i + 1) (i :: A) 212 in 213 List.rev (up b []) 214 end 215 216fun appi f = 217 let 218 fun recurse n lst = 219 case lst of 220 [] => () 221 | h :: t => (f n h; recurse (n + 1) t) 222 in 223 recurse 0 224 end 225 226fun mapi f lst = 227 let 228 fun recurse n acc lst = 229 case lst of 230 [] => acc 231 | h :: t => recurse (n + 1) (f n h :: acc) t 232 in 233 List.rev (recurse 0 [] lst) 234 end 235 236fun assoc1 item = 237 let 238 fun assc ((e as (key, _)) :: rst) = 239 if item = key then SOME e else assc rst 240 | assc [] = NONE 241 in 242 assc 243 end 244 245fun assoc2 item = 246 let 247 fun assc ((e as (_, key)) :: rst) = 248 if item = key then SOME e else assc rst 249 | assc [] = NONE 250 in 251 assc 252 end 253 254type 'a cmp = 'a * 'a -> order 255 256fun flip_order LESS = GREATER 257 | flip_order EQUAL = EQUAL 258 | flip_order GREATER = LESS 259 260fun flip_cmp cmp = flip_order o cmp 261 262fun bool_compare (true, true) = EQUAL 263 | bool_compare (true, false) = GREATER 264 | bool_compare (false, true) = LESS 265 | bool_compare (false, false) = EQUAL 266 267fun option_compare cmp optp = 268 case optp of 269 (NONE, NONE) => EQUAL 270 | (NONE, SOME _) => LESS 271 | (SOME _, NONE) => GREATER 272 | (SOME x, SOME y) => cmp(x,y) 273 274fun list_compare cfn = 275 let 276 fun comp ([], []) = EQUAL 277 | comp ([], _) = LESS 278 | comp (_, []) = GREATER 279 | comp (h1 :: t1, h2 :: t2) = 280 case cfn (h1, h2) of EQUAL => comp (t1, t2) | x => x 281 in 282 comp 283 end 284 285fun pair_compare (acmp, bcmp) ((a1, b1), (a2, b2)) = 286 case acmp (a1, a2) of 287 EQUAL => bcmp (b1, b2) 288 | x => x 289 290fun measure_cmp f (x, y) = Int.compare (f x, f y) 291fun inv_img_cmp f c (x, y) = c (f x, f y) 292 293(* streamlined combination of inv_img_cmp and pair_compare *) 294fun lex_cmp (c1, c2) (f1, f2) (x1, x2) = 295 case c1 (f1 x1, f1 x2) of 296 EQUAL => c2 (f2 x1, f2 x2) 297 | x => x 298 299(*---------------------------------------------------------------------------* 300 * For loops * 301 *---------------------------------------------------------------------------*) 302 303fun for base top f = 304 let fun For i = if i > top then [] else f i :: For (i + 1) in For base end 305 306fun for_se base top f = 307 let fun For i = if i > top then () else (f i; For (i + 1)) in For base end 308 309(*---------------------------------------------------------------------------* 310 * A naive merge sort. * 311 *---------------------------------------------------------------------------*) 312 313fun sort P = 314 let 315 fun merge [] a = a 316 | merge a [] = a 317 | merge (A as (a :: t1)) (B as (b :: t2)) = 318 if P a b then a :: merge t1 B 319 else b :: merge A t2 320 fun srt [] = [] 321 | srt [a] = a 322 | srt (h1 :: h2 :: t) = srt (merge h1 h2 :: t) 323 in 324 srt o (map (fn x => [x])) 325 end 326 327val int_sort = sort (curry (op <= : int * int -> bool)) 328 329(* linear time version of topsort (in Lib) 330 only works when nodes are integers 0 up to some n 331 deps = vector of adjacency lists *) 332 333fun vector_topsort deps = 334 let 335 open Array 336 val n = Vector.length deps 337 val a = tabulate (n, SOME o (curry Vector.sub deps)) 338 fun visit (n, ls) = 339 case sub (a, n) of 340 NONE => ls 341 | SOME dl => let 342 val _ = update (a, n, NONE) 343 val ls = List.foldl visit ls dl 344 in 345 n :: ls 346 end 347 fun v (0, ls) = ls 348 | v (n, ls) = v (n - 1, visit (n - 1, ls)) 349 in 350 v (n, []) 351 end 352 353(*---------------------------------------------------------------------------* 354 * Substitutions. * 355 *---------------------------------------------------------------------------*) 356 357type ('a, 'b) subst = {redex: 'a, residue: 'b} list 358 359fun subst_assoc test = 360 let 361 fun assc [] = NONE 362 | assc ({redex, residue} :: rst) = 363 if test redex then SOME residue else assc rst 364 in 365 assc 366 end 367 368infix 5 |-> 369fun (r1 |-> r2) = {redex = r1, residue = r2} 370 371(*---------------------------------------------------------------------------* 372 * Sets as lists * 373 *---------------------------------------------------------------------------*) 374 375fun mem i = List.exists (equal i) 376 377fun insert i L = if mem i L then L else i :: L 378 379fun mk_set [] = [] 380 | mk_set (a :: rst) = insert a (mk_set rst) 381 382fun union [] S = S 383 | union S [] = S 384 | union (a :: rst) S2 = union rst (insert a S2) 385 386(* Union of a family of sets *) 387 388fun U set_o_sets = itlist union set_o_sets [] 389 390(* All the elements in the first set that are not also in the second set. *) 391 392fun set_diff a b = filter (not o C mem b) a 393val subtract = set_diff 394 395fun intersect [] _ = [] 396 | intersect _ [] = [] 397 | intersect S1 S2 = mk_set (filter (C mem S2) S1) 398 399fun null_intersection _ [] = true 400 | null_intersection [] _ = true 401 | null_intersection (a :: rst) S = 402 not (mem a S) andalso null_intersection rst S 403 404fun set_eq S1 S2 = set_diff S1 S2 = [] andalso set_diff S2 S1 = [] 405 406(*---------------------------------------------------------------------------* 407 * Opaque type set operations * 408 *---------------------------------------------------------------------------*) 409 410(* functions for lifting equality functions over standard type operators *) 411type 'a eqf = 'a -> 'a -> bool 412fun pair_eq eq1 eq2 (x1,y1) (x2,y2) = eq1 x1 x2 andalso eq2 y1 y2 413fun option_eq eq NONE NONE = true 414 | option_eq eq (SOME x) (SOME y) = eq x y 415 | option_eq _ _ _ = false 416fun list_eq eq l1 l2 = ListPair.allEq (fn (x,y) => eq x y) (l1, l2) 417fun redres_eq eq1 eq2 {residue=res1,redex=red1} {residue=res2,redex=red2} = 418 eq1 red1 red2 andalso eq2 res1 res2 419 420fun op_assoc1 eq_func k alist = 421 case alist of 422 [] => NONE 423 | (k',v) :: rest => if eq_func k k' then SOME v 424 else op_assoc1 eq_func k rest 425 426fun op_mem eq_func i = List.exists (eq_func i) 427 428fun op_insert eq_func = 429 let 430 val mem = op_mem eq_func 431 in 432 fn i => fn L => if (mem i L) then L else i :: L 433 end 434 435fun op_mk_set eqf = 436 let 437 val insert = op_insert eqf 438 fun mkset [] = [] 439 | mkset (a :: rst) = insert a (mkset rst) 440 in 441 mkset 442 end 443 444fun op_union eq_func = 445 let 446 val mem = op_mem eq_func 447 val insert = op_insert eq_func 448 fun un [] [] = [] 449 | un a [] = a 450 | un [] a = a 451 | un (a :: b) c = un b (insert a c) 452 in 453 un 454 end 455 456(* Union of a family of sets *) 457 458fun op_U eq_func set_o_sets = itlist (op_union eq_func) set_o_sets [] 459 460fun op_intersect eq_func a b = 461 let 462 val mem = op_mem eq_func 463 val in_b = C mem b 464 val mk_set = op_mk_set eq_func 465 in 466 mk_set (filter in_b a) 467 end 468 469(* All the elements in the first set that are not also in the second set. *) 470 471fun op_set_diff eq_func S1 S2 = 472 let 473 val memb = op_mem eq_func 474 in 475 filter (fn x => not (memb x S2)) S1 476 end 477 478fun op_remove eq x list = 479 if op_mem eq x list then 480 filter (fn y => not (eq x y)) list 481 else list 482 483fun op_update eq x xs = cons x (op_remove eq x xs) 484 485(*--------------------------------------------------------------------------- 486 quote puts double quotes around a string. mlquote does this as well, 487 but also quotes all of the characters in the string so that the 488 resulting string could be printed out in a way that would make it a 489 valid ML lexeme (e.g., newlines turn into \n) 490 ---------------------------------------------------------------------------*) 491 492fun mlquote s = String.concat ["\"", String.toString s, "\""] 493 494fun quote s = String.concat ["\"", s, "\""] 495 496val is_substring = String.isSubstring 497 498fun prime s = s ^ "'" 499 500val commafy = separate ", " 501 502fun enclose ld rd s = ld ^ s ^ rd 503 504val str_all = CharVector.all 505 506(*---------------------------------------------------------------------------* 507 * A hash function used for various tasks in the system. It works fairly * 508 * well for our applications, but is not industrial strength. The size * 509 * argument should be a prime. The function then takes a string and * 510 * a pair (i,A) and returns a number < size. "i" is the index in the * 511 * string to start hashing from, and A is an accumulator. In simple * 512 * cases i=0 and A=0. * 513 *---------------------------------------------------------------------------*) 514 515local 516 open Char String 517in 518 fun hash size = 519 fn s => 520 let 521 fun hsh (i, A) = 522 hsh (i + 1, (A * 4 + ord (sub (s, i))) mod size) 523 handle Subscript => A 524 in 525 hsh 526 end 527end 528 529(*--------------------------------------------------------------------------- 530 Refs 531 ---------------------------------------------------------------------------*) 532 533fun inc r = (r := !r + 1) 534fun dec r = (r := !r - 1) 535 536(*--------------------------------------------------------------------------- 537 SML/NJ v.93 style string operations 538 ---------------------------------------------------------------------------*) 539 540fun ordof (string, place) = Char.ord (String.sub (string, place)) 541val implode = String.concat 542val explode = map Char.toString o String.explode 543 544fun words2 sep string = 545 snd (itlist (fn ch => fn (chs, tokl) => 546 if ch = sep 547 then if null chs 548 then ([], tokl) 549 else ([], implode chs :: tokl) 550 else (ch :: chs, tokl)) 551 (sep :: explode string) ([], [])) 552 553fun replace_string {from, to} = 554 let 555 val next = Substring.position from 556 val drop = Substring.triml (String.size from) 557 val to = Substring.full to 558 fun f acc s = 559 let 560 val (prefix,s) = next s 561 val acc = prefix::acc 562 in 563 if Substring.isEmpty s then 564 Substring.concat(List.rev acc) 565 else 566 f (to::acc) (drop s) 567 end 568 in 569 f [] o Substring.full 570 end 571 572(*--------------------------------------------------------------------------- 573 System 574 ---------------------------------------------------------------------------*) 575 576val getEnv = Process.getEnv 577val cd = FileSys.chDir 578val pwd = FileSys.getDir 579fun system s = if Process.isSuccess (Process.system s) then 0 else 1 580val getArgs = CommandLine.arguments 581val argv = getArgs 582fun exit() = Process.exit Process.success 583 584(*--------------------------------------------------------------------------- 585 IO 586 ---------------------------------------------------------------------------*) 587 588exception Io of string; 589type instream = TextIO.instream 590type outstream = TextIO.outstream 591val std_out = TextIO.stdOut 592val stdin = TextIO.stdIn 593fun open_in file = TextIO.openIn file 594 handle IO.Io{cause=SysErr(s,_),...} => raise (Io s) 595 (* handle OS.SysErr (s,_) => raise Io s; *) 596fun open_out file = TextIO.openOut file 597 handle IO.Io{cause=SysErr(s,_),...} => raise (Io s) 598 (* handle OS.SysErr (s,_) => raise Io s; *) 599val output = TextIO.output 600fun outputc strm s = output(strm,s) 601val close_in = TextIO.closeIn 602val close_out = TextIO.closeOut 603val flush_out = TextIO.flushOut 604fun input_line is = case TextIO.inputLine is of NONE => "" | SOME s => s 605val end_of_stream = TextIO.endOfStream 606 607(*---------------------------------------------------------------------------*) 608(* Yet another variant of the sum type, used for the failure monad *) 609(*---------------------------------------------------------------------------*) 610 611datatype ('a, 'b) verdict = PASS of 'a | FAIL of 'b 612 613fun verdict f c x = PASS (f x) handle e => FAIL (c x, e) 614 615fun ?>(PASS x, f) = f x 616 | ?>(FAIL y, f) = FAIL y 617 618(*--------------------------------------------------------------------------- 619 Time 620 ---------------------------------------------------------------------------*) 621 622type time = Time.time 623 624local 625 open Time 626in 627 val timestamp: unit -> time = now 628 val time_to_string: time -> string = toString 629 fun dest_time t = 630 let 631 val r = toReal t 632 val sec = Arbnum.floor (toReal t) 633 val sec_million = Arbnum.* (sec, Arbnum.fromInt 1000000) 634 val r_million = r * 1000000.0 635 val usec = Arbnum.- (Arbnum.floor r_million, sec_million) 636 in 637 {sec = sec, usec = usec} 638 end 639 fun mk_time {sec, usec} = 640 fromReal (Real.+ (Arbnum.toReal sec, Arbnum.toReal usec / 1000000.0)) 641 fun time_eq (t1:time) t2 = (t1 = t2) 642 fun time_lt (t1:time) t2 = Time.<(t1,t2) 643 fun time_max (t1,t2) = if time_lt t1 t2 then t2 else t1 644 fun time_maxl l = 645 case l of 646 [] => Time.zeroTime 647 | h::t => List.foldl time_max h t 648 fun realtime f x = 649 let 650 val timer = Timer.startRealTimer() 651 val result = verdict f (fn x => x) x 652 val t = Timer.checkRealTimer timer 653 in 654 print ("clock time: " ^ Time.toString t ^ "s\n"); 655 case result of 656 PASS y => y 657 | FAIL (_, e) => raise e 658 end 659end 660 661(*---------------------------------------------------------------------------* 662 * Invoking a function with a flag temporarily assigned to the given value. * 663 *---------------------------------------------------------------------------*) 664 665fun with_flag (flag, b) f x = 666 let 667 val fval = !flag 668 val () = flag := b 669 val res = f x handle e => (flag := fval; raise e) 670 in 671 flag := fval; res 672 end 673 674(*---------------------------------------------------------------------------* 675 * An abstract type of imperative streams. * 676 *---------------------------------------------------------------------------*) 677 678abstype ('a, 'b) istream = STRM of {mutator: 'a -> 'a, 679 project: 'a -> 'b, 680 state: 'a ref, 681 init: 'a} 682with 683 fun mk_istream f i g = 684 STRM {mutator = f, project = g, state = ref i, init = i} 685 fun next (strm as STRM{mutator, state, ...}) = 686 (state := mutator (!state); strm) 687 fun state (STRM {project, state, ...}) = project (!state) 688 fun reset (strm as STRM {state, init, ...}) = (state := init; strm) 689end 690 691(*--------------------------------------------------------------------------- 692 A type that can be used for sharing, and some functions for lifting 693 to various type operators (just lists and pairs currently). 694 ---------------------------------------------------------------------------*) 695 696datatype 'a delta = SAME | DIFF of 'a 697 698fun delta_apply f x = case f x of SAME => x | DIFF y => y 699 700fun delta_map f = 701 let 702 fun map [] = SAME 703 | map (h :: t) = 704 case (f h, map t) of 705 (SAME, SAME) => SAME 706 | (SAME, DIFF t') => DIFF (h :: t') 707 | (DIFF h', SAME) => DIFF (h' :: t) 708 | (DIFF h', DIFF t') => DIFF (h' :: t') 709 in 710 map 711 end 712 713fun delta_pair f g (x, y) = 714 case (f x, g y) of 715 (SAME, SAME) => SAME 716 | (SAME, DIFF y') => DIFF (x, y') 717 | (DIFF x', SAME) => DIFF (x', y) 718 | (DIFF x', DIFF y') => DIFF (x', y') 719 720(*--------------------------------------------------------------------------- 721 A function that strips leading (nested) comments and whitespace 722 from a string. 723 ---------------------------------------------------------------------------*) 724 725fun deinitcomment0 ss n = 726 case Substring.getc ss of 727 NONE => ss 728 | SOME (c, ss') => 729 if Char.isSpace c 730 then deinitcomment0 ss' n 731 else if c = #"(" 732 then case Substring.getc ss' of 733 NONE => ss 734 | SOME (c, ss'') => 735 if c = #"*" 736 then deinitcomment0 ss'' (n + 1) 737 else if n = 0 738 then ss 739 else deinitcomment0 ss'' n 740 else if n > 0 andalso c = #"*" 741 then case Substring.getc ss' of 742 NONE => ss 743 | SOME (c, ss'') => 744 if c = #")" 745 then deinitcomment0 ss'' (n - 1) 746 else deinitcomment0 ss'' n 747 else if n = 0 748 then ss 749 else deinitcomment0 ss' n 750 751fun deinitcommentss ss = deinitcomment0 ss 0 752fun deinitcomment s = Substring.string (deinitcomment0 (Substring.full s) 0) 753 754(*--------------------------------------------------------------------------- 755 Pretty Printing 756 ---------------------------------------------------------------------------*) 757 758(*--------------------------------------------------------------------------- 759 * Simple and heavily used. 760 * pfun = item printing function 761 * dfun = delimiter printing function 762 * bfun = break printer function 763 *---------------------------------------------------------------------------*) 764 765fun with_ppstream ppstrm = 766 let 767 open OldPP 768 in 769 {add_string = add_string ppstrm, 770 add_break = add_break ppstrm, 771 begin_block = begin_block ppstrm, 772 end_block = fn () => end_block ppstrm, 773 add_newline = fn () => add_newline ppstrm, 774 clear_ppstream = fn () => clear_ppstream ppstrm, 775 flush_ppstream = fn () => flush_ppstream ppstrm} 776 end 777 778(*--------------------------------------------------------------------------- 779 MoscowML returns lists of QUOTE'd strings when a quote is spread 780 over more than one line. "norm_quote" concatenates all adjacent 781 QUOTE elements in this list. 782 ---------------------------------------------------------------------------*) 783 784type 'a quotation = 'a HOLPP.quotation 785open HOLPP 786 787fun pprint f x = prettyPrint(TextIO.print, 72) (f x) 788 789fun norm_quote [] = [] 790 | norm_quote [x] = [x] 791 | norm_quote (QUOTE s1 :: QUOTE s2 :: rst) = 792 norm_quote (QUOTE (s1 ^ s2) :: rst) 793 | norm_quote (h :: rst) = h :: norm_quote rst 794 795local 796 fun strip_comments (d, a) s = 797 if Substring.size s = 0 798 then a 799 else let 800 val (l, r) = Substring.splitl (fn c => c <> #"(" andalso c <> #"*") s 801 val a' = if 0 < d then a else a @ [l] 802 in 803 if Substring.isPrefix "(*#loc " r 804 then strip_comments (d + 1, a @ [Substring.trimr 1 l]) 805 (Substring.triml 7 r) 806 else if Substring.isPrefix "(*" r 807 then strip_comments (d + 1, a') (Substring.triml 2 r) 808 else if Substring.isPrefix "*)" r 809 then strip_comments (d - 1, a') (Substring.triml 2 r) 810 else if Substring.size r = 0 811 then a' 812 else let 813 val (r1, r2) = Substring.splitAt (r, 1) 814 in 815 strip_comments (d, if 0 < d then a' else a' @ [r1]) r2 816 end 817 end 818 val finish = Substring.concat o strip_comments (0, []) o Substring.full o 819 String.concat o List.rev 820in 821 fun quote_to_string (f : 'a -> string) = 822 let 823 fun quote_to_strings a = 824 fn [] => finish a 825 | QUOTE s :: r => quote_to_strings (s :: a) r 826 | ANTIQUOTE s :: r => quote_to_strings (f s :: a) r 827 in 828 quote_to_strings [] 829 end 830 val quote_to_string_list = 831 String.tokens (fn c => c = #"\n") o quote_to_string (fn x => x) 832end 833 834(* suck in implementation specific stuff *) 835 836open MLSYSPortable 837structure HOLSusp = MLSYSPortable.HOLSusp 838 839(* rebinding the exception seems to be necessary in Moscow ML 2.01 *) 840 841exception Interrupt = MLSYSPortable.Interrupt 842 843end (* Portable *) 844