1(* ========================================================================= *) 2(* PRETTY-PRINTING *) 3(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure Print :> Print = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* Constants. *) 13(* ------------------------------------------------------------------------- *) 14 15val initialLineLength = 75; 16 17(* ------------------------------------------------------------------------- *) 18(* Helper functions. *) 19(* ------------------------------------------------------------------------- *) 20 21fun revAppend xs s = 22 case xs of 23 [] => s () 24 | x :: xs => revAppend xs (K (Stream.Cons (x,s))); 25 26fun revConcat strm = 27 case strm of 28 Stream.Nil => Stream.Nil 29 | Stream.Cons (h,t) => revAppend h (fn () => revConcat (t ())); 30 31local 32 fun calcSpaces n = nChars #" " n; 33 34 val cacheSize = 2 * initialLineLength; 35 36 val cachedSpaces = Vector.tabulate (cacheSize,calcSpaces); 37in 38 fun nSpaces n = 39 if n < cacheSize then Vector.sub (cachedSpaces,n) 40 else calcSpaces n; 41end; 42 43(* ------------------------------------------------------------------------- *) 44(* Escaping strings. *) 45(* ------------------------------------------------------------------------- *) 46 47fun escapeString {escape} = 48 let 49 val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape 50 51 fun escapeChar c = 52 case c of 53 #"\\" => "\\\\" 54 | #"\n" => "\\n" 55 | #"\t" => "\\t" 56 | _ => 57 case List.find (equal c o fst) escapeMap of 58 SOME (_,s) => s 59 | NONE => str c 60 in 61 String.translate escapeChar 62 end; 63 64(* ------------------------------------------------------------------------- *) 65(* Pretty-printing blocks. *) 66(* ------------------------------------------------------------------------- *) 67 68datatype style = Consistent | Inconsistent; 69 70datatype block = 71 Block of 72 {style : style, 73 indent : int}; 74 75fun toStringStyle style = 76 case style of 77 Consistent => "Consistent" 78 | Inconsistent => "Inconsistent"; 79 80fun isConsistentStyle style = 81 case style of 82 Consistent => true 83 | Inconsistent => false; 84 85fun isInconsistentStyle style = 86 case style of 87 Inconsistent => true 88 | Consistent => false; 89 90fun mkBlock style indent = 91 Block 92 {style = style, 93 indent = indent}; 94 95val mkConsistentBlock = mkBlock Consistent; 96 97val mkInconsistentBlock = mkBlock Inconsistent; 98 99fun styleBlock (Block {style = x, ...}) = x; 100 101fun indentBlock (Block {indent = x, ...}) = x; 102 103fun isConsistentBlock block = isConsistentStyle (styleBlock block); 104 105fun isInconsistentBlock block = isInconsistentStyle (styleBlock block); 106 107(* ------------------------------------------------------------------------- *) 108(* Words are unbreakable strings annotated with their effective size. *) 109(* ------------------------------------------------------------------------- *) 110 111datatype word = Word of {word : string, size : int}; 112 113fun mkWord s = Word {word = s, size = String.size s}; 114 115val emptyWord = mkWord ""; 116 117fun charWord c = mkWord (str c); 118 119fun spacesWord i = Word {word = nSpaces i, size = i}; 120 121fun sizeWord (Word {size = x, ...}) = x; 122 123fun renderWord (Word {word = x, ...}) = x; 124 125(* ------------------------------------------------------------------------- *) 126(* Possible line breaks. *) 127(* ------------------------------------------------------------------------- *) 128 129datatype break = Break of {size : int, extraIndent : int}; 130 131fun mkBreak n = Break {size = n, extraIndent = 0}; 132 133fun sizeBreak (Break {size = x, ...}) = x; 134 135fun extraIndentBreak (Break {extraIndent = x, ...}) = x; 136 137fun renderBreak b = nSpaces (sizeBreak b); 138 139fun updateSizeBreak size break = 140 let 141 val Break {size = _, extraIndent} = break 142 in 143 Break 144 {size = size, 145 extraIndent = extraIndent} 146 end; 147 148fun appendBreak break1 break2 = 149 let 150(*BasicDebug 151 val () = warn "merging consecutive pretty-printing breaks" 152*) 153 val Break {size = size1, extraIndent = extraIndent1} = break1 154 and Break {size = size2, extraIndent = extraIndent2} = break2 155 156 val size = size1 + size2 157 and extraIndent = Int.max (extraIndent1,extraIndent2) 158 in 159 Break 160 {size = size, 161 extraIndent = extraIndent} 162 end; 163 164(* ------------------------------------------------------------------------- *) 165(* A type of pretty-printers. *) 166(* ------------------------------------------------------------------------- *) 167 168datatype step = 169 BeginBlock of block 170 | EndBlock 171 | AddWord of word 172 | AddBreak of break 173 | AddNewline; 174 175type ppstream = step Stream.stream; 176 177type 'a pp = 'a -> ppstream; 178 179fun toStringStep step = 180 case step of 181 BeginBlock _ => "BeginBlock" 182 | EndBlock => "EndBlock" 183 | AddWord _ => "Word" 184 | AddBreak _ => "Break" 185 | AddNewline => "Newline"; 186 187val skip : ppstream = Stream.Nil; 188 189fun sequence pp1 pp2 : ppstream = Stream.append pp1 (K pp2); 190 191local 192 fun dup pp n () = if n = 1 then pp else Stream.append pp (dup pp (n - 1)); 193in 194 fun duplicate n pp : ppstream = 195 let 196(*BasicDebug 197 val () = if 0 <= n then () else raise Bug "Print.duplicate" 198*) 199 in 200 if n = 0 then skip else dup pp n () 201 end; 202end; 203 204val program : ppstream list -> ppstream = Stream.concatList; 205 206val stream : ppstream Stream.stream -> ppstream = Stream.concat; 207 208(* ------------------------------------------------------------------------- *) 209(* Pretty-printing blocks. *) 210(* ------------------------------------------------------------------------- *) 211 212local 213 fun beginBlock b = Stream.singleton (BeginBlock b); 214 215 val endBlock = Stream.singleton EndBlock; 216in 217 fun block b pp = program [beginBlock b, pp, endBlock]; 218end; 219 220fun consistentBlock i pps = block (mkConsistentBlock i) (program pps); 221 222fun inconsistentBlock i pps = block (mkInconsistentBlock i) (program pps); 223 224(* ------------------------------------------------------------------------- *) 225(* Words are unbreakable strings annotated with their effective size. *) 226(* ------------------------------------------------------------------------- *) 227 228fun ppWord w = Stream.singleton (AddWord w); 229 230val space = ppWord (mkWord " "); 231 232fun spaces i = ppWord (spacesWord i); 233 234(* ------------------------------------------------------------------------- *) 235(* Possible line breaks. *) 236(* ------------------------------------------------------------------------- *) 237 238fun ppBreak b = Stream.singleton (AddBreak b); 239 240fun breaks i = ppBreak (mkBreak i); 241 242val break = breaks 1; 243 244(* ------------------------------------------------------------------------- *) 245(* Forced line breaks. *) 246(* ------------------------------------------------------------------------- *) 247 248val newline = Stream.singleton AddNewline; 249 250fun newlines i = duplicate i newline; 251 252(* ------------------------------------------------------------------------- *) 253(* Pretty-printer combinators. *) 254(* ------------------------------------------------------------------------- *) 255 256fun ppMap f ppB a : ppstream = ppB (f a); 257 258fun ppBracket' l r ppA a = 259 let 260 val n = sizeWord l 261 in 262 inconsistentBlock n 263 [ppWord l, 264 ppA a, 265 ppWord r] 266 end; 267 268fun ppOp' w = sequence (ppWord w) break; 269 270fun ppOp2' ab ppA ppB (a,b) = 271 inconsistentBlock 0 272 [ppA a, 273 ppOp' ab, 274 ppB b]; 275 276fun ppOp3' ab bc ppA ppB ppC (a,b,c) = 277 inconsistentBlock 0 278 [ppA a, 279 ppOp' ab, 280 ppB b, 281 ppOp' bc, 282 ppC c]; 283 284fun ppOpList' s ppA = 285 let 286 fun ppOpA a = sequence (ppOp' s) (ppA a) 287 in 288 fn [] => skip 289 | h :: t => inconsistentBlock 0 (ppA h :: List.map ppOpA t) 290 end; 291 292fun ppOpStream' s ppA = 293 let 294 fun ppOpA a = sequence (ppOp' s) (ppA a) 295 in 296 fn Stream.Nil => skip 297 | Stream.Cons (h,t) => 298 inconsistentBlock 0 299 [ppA h, 300 Stream.concat (Stream.map ppOpA (t ()))] 301 end; 302 303fun ppBracket l r = ppBracket' (mkWord l) (mkWord r); 304 305fun ppOp s = ppOp' (mkWord s); 306 307fun ppOp2 ab = ppOp2' (mkWord ab); 308 309fun ppOp3 ab bc = ppOp3' (mkWord ab) (mkWord bc); 310 311fun ppOpList s = ppOpList' (mkWord s); 312 313fun ppOpStream s = ppOpStream' (mkWord s); 314 315(* ------------------------------------------------------------------------- *) 316(* Pretty-printers for common types. *) 317(* ------------------------------------------------------------------------- *) 318 319fun ppChar c = ppWord (charWord c); 320 321fun ppString s = ppWord (mkWord s); 322 323fun ppEscapeString escape = ppMap (escapeString escape) ppString; 324 325local 326 val pp = ppString "()"; 327in 328 fun ppUnit () = pp; 329end; 330 331local 332 val ppTrue = ppString "true" 333 and ppFalse = ppString "false"; 334in 335 fun ppBool b = if b then ppTrue else ppFalse; 336end; 337 338val ppInt = ppMap Int.toString ppString; 339 340local 341 val ppNeg = ppString "~" 342 and ppSep = ppString "," 343 and ppZero = ppString "0" 344 and ppZeroZero = ppString "00"; 345 346 fun ppIntBlock i = 347 if i < 10 then sequence ppZeroZero (ppInt i) 348 else if i < 100 then sequence ppZero (ppInt i) 349 else ppInt i; 350 351 fun ppIntBlocks i = 352 if i < 1000 then ppInt i 353 else sequence (ppIntBlocks (i div 1000)) 354 (sequence ppSep (ppIntBlock (i mod 1000))); 355in 356 fun ppPrettyInt i = 357 if i < 0 then sequence ppNeg (ppIntBlocks (~i)) 358 else ppIntBlocks i; 359end; 360 361val ppReal = ppMap Real.toString ppString; 362 363val ppPercent = ppMap percentToString ppString; 364 365local 366 val ppLess = ppString "Less" 367 and ppEqual = ppString "Equal" 368 and ppGreater = ppString "Greater"; 369in 370 fun ppOrder ord = 371 case ord of 372 LESS => ppLess 373 | EQUAL => ppEqual 374 | GREATER => ppGreater; 375end; 376 377local 378 val left = mkWord "[" 379 and right = mkWord "]" 380 and sep = mkWord ","; 381in 382 fun ppList ppX xs = ppBracket' left right (ppOpList' sep ppX) xs; 383 384 fun ppStream ppX xs = ppBracket' left right (ppOpStream' sep ppX) xs; 385end; 386 387local 388 val ppNone = ppString "-"; 389in 390 fun ppOption ppX xo = 391 case xo of 392 SOME x => ppX x 393 | NONE => ppNone; 394end; 395 396local 397 val left = mkWord "(" 398 and right = mkWord ")" 399 and sep = mkWord ","; 400in 401 fun ppPair ppA ppB = 402 ppBracket' left right (ppOp2' sep ppA ppB); 403 404 fun ppTriple ppA ppB ppC = 405 ppBracket' left right (ppOp3' sep sep ppA ppB ppC); 406end; 407 408fun ppException e = ppString (exnMessage e); 409 410(* ------------------------------------------------------------------------- *) 411(* A type of pretty-printers. *) 412(* ------------------------------------------------------------------------- *) 413 414local 415 val ppStepType = ppMap toStringStep ppString; 416 417 val ppStyle = ppMap toStringStyle ppString; 418 419 val ppBlockInfo = 420 let 421 val sep = mkWord " " 422 in 423 fn Block {style = s, indent = i} => 424 program [ppStyle s, ppWord sep, ppInt i] 425 end; 426 427 val ppWordInfo = 428 let 429 val left = mkWord "\"" 430 and right = mkWord "\"" 431 and escape = {escape = [#"\""]} 432 433 val pp = ppBracket' left right (ppEscapeString escape) 434 in 435 fn Word {word = s, size = n} => 436 if size s = n then pp s else ppPair pp ppInt (s,n) 437 end; 438 439 val ppBreakInfo = 440 let 441 val sep = mkWord "+" 442 in 443 fn Break {size = n, extraIndent = k} => 444 if k = 0 then ppInt n else program [ppInt n, ppWord sep, ppInt k] 445 end; 446 447 fun ppStep step = 448 inconsistentBlock 2 449 (ppStepType step :: 450 (case step of 451 BeginBlock b => 452 [break, 453 ppBlockInfo b] 454 | EndBlock => [] 455 | AddWord w => 456 [break, 457 ppWordInfo w] 458 | AddBreak b => 459 [break, 460 ppBreakInfo b] 461 | AddNewline => [])); 462in 463 val ppPpstream = ppStream ppStep; 464end; 465 466(* ------------------------------------------------------------------------- *) 467(* Pretty-printing infix operators. *) 468(* ------------------------------------------------------------------------- *) 469 470type token = string; 471 472datatype assoc = 473 LeftAssoc 474 | NonAssoc 475 | RightAssoc; 476 477datatype infixes = 478 Infixes of 479 {token : token, 480 precedence : int, 481 assoc : assoc} list; 482 483local 484 fun comparePrecedence (io1,io2) = 485 let 486 val {token = _, precedence = p1, assoc = _} = io1 487 and {token = _, precedence = p2, assoc = _} = io2 488 in 489 Int.compare (p2,p1) 490 end; 491 492 fun equalAssoc a a' = 493 case a of 494 LeftAssoc => (case a' of LeftAssoc => true | _ => false) 495 | NonAssoc => (case a' of NonAssoc => true | _ => false) 496 | RightAssoc => (case a' of RightAssoc => true | _ => false); 497 498 fun new t a acc = {tokens = StringSet.singleton t, assoc = a} :: acc; 499 500 fun add t a' acc = 501 case acc of 502 [] => raise Bug "Print.layerInfixes: null" 503 | {tokens = ts, assoc = a} :: acc => 504 if equalAssoc a a' then {tokens = StringSet.add ts t, assoc = a} :: acc 505 else raise Bug "Print.layerInfixes: mixed assocs"; 506 507 fun layer ({token = t, precedence = p, assoc = a}, (acc,p')) = 508 let 509 val acc = if p = p' then add t a acc else new t a acc 510 in 511 (acc,p) 512 end; 513in 514 fun layerInfixes (Infixes ios) = 515 case sort comparePrecedence ios of 516 [] => [] 517 | {token = t, precedence = p, assoc = a} :: ios => 518 let 519 val acc = new t a [] 520 521 val (acc,_) = List.foldl layer (acc,p) ios 522 in 523 acc 524 end; 525end; 526 527local 528 fun add ({tokens = ts, assoc = _}, tokens) = StringSet.union ts tokens; 529in 530 fun tokensLayeredInfixes l = List.foldl add StringSet.empty l; 531end; 532 533fun tokensInfixes ios = tokensLayeredInfixes (layerInfixes ios); 534 535fun destInfixOp dest tokens tm = 536 case dest tm of 537 NONE => NONE 538 | s as SOME (t,a,b) => if StringSet.member t tokens then s else NONE; 539 540fun ppLayeredInfixes dest ppTok {tokens,assoc} ppLower ppSub = 541 let 542 fun isLayer t = StringSet.member t tokens 543 544 fun ppTerm aligned (tm,r) = 545 case dest tm of 546 NONE => ppSub (tm,r) 547 | SOME (t,a,b) => 548 if aligned andalso isLayer t then ppLayer (tm,t,a,b,r) 549 else ppLower (tm,t,a,b,r) 550 551 and ppLeft tm_r = 552 let 553 val aligned = case assoc of LeftAssoc => true | _ => false 554 in 555 ppTerm aligned tm_r 556 end 557 558 and ppLayer (tm,t,a,b,r) = 559 program 560 [ppLeft (a,true), 561 ppTok (tm,t), 562 ppRight (b,r)] 563 564 and ppRight tm_r = 565 let 566 val aligned = case assoc of RightAssoc => true | _ => false 567 in 568 ppTerm aligned tm_r 569 end 570 in 571 fn tm_t_a_b_r as (_,t,_,_,_) => 572 if isLayer t then inconsistentBlock 0 [ppLayer tm_t_a_b_r] 573 else ppLower tm_t_a_b_r 574 end; 575 576local 577 val leftBrack = mkWord "(" 578 and rightBrack = mkWord ")"; 579in 580 fun ppInfixes ops = 581 let 582 val layers = layerInfixes ops 583 584 val toks = tokensLayeredInfixes layers 585 in 586 fn dest => fn ppTok => fn ppSub => 587 let 588 fun destOp tm = destInfixOp dest toks tm 589 590 fun ppInfix tm_t_a_b_r = ppLayers layers tm_t_a_b_r 591 592 and ppLayers ls (tm,t,a,b,r) = 593 case ls of 594 [] => 595 ppBracket' leftBrack rightBrack ppInfix (tm,t,a,b,false) 596 | l :: ls => 597 let 598 val ppLower = ppLayers ls 599 in 600 ppLayeredInfixes destOp ppTok l ppLower ppSub (tm,t,a,b,r) 601 end 602 in 603 fn (tm,r) => 604 case destOp tm of 605 SOME (t,a,b) => ppInfix (tm,t,a,b,r) 606 | NONE => ppSub (tm,r) 607 end 608 end; 609end; 610 611(* ------------------------------------------------------------------------- *) 612(* A type of output lines. *) 613(* ------------------------------------------------------------------------- *) 614 615type line = {indent : int, line : string}; 616 617val emptyLine = 618 let 619 val indent = 0 620 and line = "" 621 in 622 {indent = indent, 623 line = line} 624 end; 625 626fun addEmptyLine lines = emptyLine :: lines; 627 628fun addLine lines indent line = {indent = indent, line = line} :: lines; 629 630(* ------------------------------------------------------------------------- *) 631(* Pretty-printer rendering. *) 632(* ------------------------------------------------------------------------- *) 633 634datatype chunk = 635 WordChunk of word 636 | BreakChunk of break 637 | FrameChunk of frame 638 639and frame = 640 Frame of 641 {block : block, 642 broken : bool, 643 indent : int, 644 size : int, 645 chunks : chunk list}; 646 647datatype state = 648 State of 649 {lineIndent : int, 650 lineSize : int, 651 stack : frame list}; 652 653fun blockFrame (Frame {block = x, ...}) = x; 654 655fun brokenFrame (Frame {broken = x, ...}) = x; 656 657fun indentFrame (Frame {indent = x, ...}) = x; 658 659fun sizeFrame (Frame {size = x, ...}) = x; 660 661fun chunksFrame (Frame {chunks = x, ...}) = x; 662 663fun styleFrame frame = styleBlock (blockFrame frame); 664 665fun isConsistentFrame frame = isConsistentBlock (blockFrame frame); 666 667fun breakingFrame frame = isConsistentFrame frame andalso brokenFrame frame; 668 669fun sizeChunk chunk = 670 case chunk of 671 WordChunk w => sizeWord w 672 | BreakChunk b => sizeBreak b 673 | FrameChunk f => sizeFrame f; 674 675local 676 fun add (c,acc) = sizeChunk c + acc; 677in 678 fun sizeChunks cs = List.foldl add 0 cs; 679end; 680 681local 682 fun flattenChunks acc chunks = 683 case chunks of 684 [] => acc 685 | chunk :: chunks => flattenChunk acc chunk chunks 686 687 and flattenChunk acc chunk chunks = 688 case chunk of 689 WordChunk w => flattenChunks (renderWord w :: acc) chunks 690 | BreakChunk b => flattenChunks (renderBreak b :: acc) chunks 691 | FrameChunk f => flattenFrame acc f chunks 692 693 and flattenFrame acc frame chunks = 694 flattenChunks acc (chunksFrame frame @ chunks); 695in 696 fun renderChunks chunks = String.concat (flattenChunks [] chunks); 697end; 698 699fun addChunksLine lines indent chunks = 700 addLine lines indent (renderChunks chunks); 701 702local 703 fun add baseIndent ((extraIndent,chunks),lines) = 704 addChunksLine lines (baseIndent + extraIndent) chunks; 705in 706 fun addIndentChunksLines lines baseIndent indent_chunks = 707 List.foldl (add baseIndent) lines indent_chunks; 708end; 709 710fun isEmptyFrame frame = 711 let 712 val chunks = chunksFrame frame 713 714 val empty = List.null chunks 715 716(*BasicDebug 717 val () = 718 if not empty orelse sizeFrame frame = 0 then () 719 else raise Bug "Print.isEmptyFrame: bad size" 720*) 721 in 722 empty 723 end; 724 725local 726 fun breakInconsistent blockIndent = 727 let 728 fun break chunks = 729 case chunks of 730 [] => NONE 731 | chunk :: chunks => 732 case chunk of 733 BreakChunk b => 734 let 735 val pre = chunks 736 and indent = blockIndent + extraIndentBreak b 737 and post = [] 738 in 739 SOME (pre,indent,post) 740 end 741 | _ => 742 case break chunks of 743 SOME (pre,indent,post) => 744 let 745 val post = chunk :: post 746 in 747 SOME (pre,indent,post) 748 end 749 | NONE => NONE 750 in 751 break 752 end; 753 754 fun breakConsistent blockIndent = 755 let 756 fun break indent_chunks chunks = 757 case breakInconsistent blockIndent chunks of 758 NONE => (chunks,indent_chunks) 759 | SOME (pre,indent,post) => 760 break ((indent,post) :: indent_chunks) pre 761 in 762 break [] 763 end; 764in 765 fun breakFrame frame = 766 let 767 val Frame 768 {block, 769 broken = _, 770 indent = _, 771 size = _, 772 chunks} = frame 773 774 val blockIndent = indentBlock block 775 in 776 case breakInconsistent blockIndent chunks of 777 NONE => NONE 778 | SOME (pre,indent,post) => 779 let 780 val broken = true 781 and size = sizeChunks post 782 783 val frame = 784 Frame 785 {block = block, 786 broken = broken, 787 indent = indent, 788 size = size, 789 chunks = post} 790 in 791 case styleBlock block of 792 Inconsistent => 793 let 794 val indent_chunks = [] 795 in 796 SOME (pre,indent_chunks,frame) 797 end 798 | Consistent => 799 let 800 val (pre,indent_chunks) = breakConsistent blockIndent pre 801 in 802 SOME (pre,indent_chunks,frame) 803 end 804 end 805 end; 806end; 807 808fun removeChunksFrame frame = 809 let 810 val Frame 811 {block, 812 broken, 813 indent, 814 size = _, 815 chunks} = frame 816 in 817 if broken andalso List.null chunks then NONE 818 else 819 let 820 val frame = 821 Frame 822 {block = block, 823 broken = true, 824 indent = indent, 825 size = 0, 826 chunks = []} 827 in 828 SOME (chunks,frame) 829 end 830 end; 831 832val removeChunksFrames = 833 let 834 fun remove frames = 835 case frames of 836 [] => 837 let 838 val chunks = [] 839 and frames = NONE 840 and indent = 0 841 in 842 (chunks,frames,indent) 843 end 844 | top :: rest => 845 let 846 val (chunks,rest',indent) = remove rest 847 848 val indent = indent + indentFrame top 849 850 val (chunks,top') = 851 case removeChunksFrame top of 852 NONE => (chunks,NONE) 853 | SOME (topChunks,top) => (topChunks @ chunks, SOME top) 854 855 val frames' = 856 case (top',rest') of 857 (NONE,NONE) => NONE 858 | (SOME top, NONE) => SOME (top :: rest) 859 | (NONE, SOME rest) => SOME (top :: rest) 860 | (SOME top, SOME rest) => SOME (top :: rest) 861 in 862 (chunks,frames',indent) 863 end 864 in 865 fn frames => 866 let 867 val (chunks,frames',indent) = remove frames 868 869 val frames = Option.getOpt (frames',frames) 870 in 871 (chunks,frames,indent) 872 end 873 end; 874 875local 876 fun breakUp lines lineIndent frames = 877 case frames of 878 [] => NONE 879 | frame :: frames => 880 case breakUp lines lineIndent frames of 881 SOME (lines_indent,lineSize,frames) => 882 let 883 val lineSize = lineSize + sizeFrame frame 884 and frames = frame :: frames 885 in 886 SOME (lines_indent,lineSize,frames) 887 end 888 | NONE => 889 case breakFrame frame of 890 NONE => NONE 891 | SOME (frameChunks,indent_chunks,frame) => 892 let 893 val (chunks,frames,indent) = removeChunksFrames frames 894 895 val chunks = frameChunks @ chunks 896 897 val lines = addChunksLine lines lineIndent chunks 898 899 val lines = addIndentChunksLines lines indent indent_chunks 900 901 val lineIndent = indent + indentFrame frame 902 903 val lineSize = sizeFrame frame 904 905 val frames = frame :: frames 906 in 907 SOME ((lines,lineIndent),lineSize,frames) 908 end; 909 910 fun breakInsideChunk chunk = 911 case chunk of 912 WordChunk _ => NONE 913 | BreakChunk _ => raise Bug "Print.breakInsideChunk" 914 | FrameChunk frame => 915 case breakFrame frame of 916 SOME (pathChunks,indent_chunks,frame) => 917 let 918 val pathIndent = 0 919 and breakIndent = indentFrame frame 920 in 921 SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) 922 end 923 | NONE => breakInsideFrame frame 924 925 and breakInsideChunks chunks = 926 case chunks of 927 [] => NONE 928 | chunk :: chunks => 929 case breakInsideChunk chunk of 930 SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) => 931 let 932 val pathChunks = pathChunks @ chunks 933 and chunks = [FrameChunk frame] 934 in 935 SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) 936 end 937 | NONE => 938 case breakInsideChunks chunks of 939 SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) => 940 let 941 val chunks = chunk :: chunks 942 in 943 SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) 944 end 945 | NONE => NONE 946 947 and breakInsideFrame frame = 948 let 949 val Frame 950 {block, 951 broken = _, 952 indent, 953 size = _, 954 chunks} = frame 955 in 956 case breakInsideChunks chunks of 957 SOME (pathChunks,pathIndent,indent_chunks,breakIndent,chunks) => 958 let 959 val pathIndent = pathIndent + indent 960 and broken = true 961 and size = sizeChunks chunks 962 963 val frame = 964 Frame 965 {block = block, 966 broken = broken, 967 indent = indent, 968 size = size, 969 chunks = chunks} 970 in 971 SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) 972 end 973 | NONE => NONE 974 end; 975 976 fun breakInside lines lineIndent frames = 977 case frames of 978 [] => NONE 979 | frame :: frames => 980 case breakInsideFrame frame of 981 SOME (pathChunks,pathIndent,indent_chunks,breakIndent,frame) => 982 let 983 val (chunks,frames,indent) = removeChunksFrames frames 984 985 val chunks = pathChunks @ chunks 986 and indent = indent + pathIndent 987 988 val lines = addChunksLine lines lineIndent chunks 989 990 val lines = addIndentChunksLines lines indent indent_chunks 991 992 val lineIndent = indent + breakIndent 993 994 val lineSize = sizeFrame frame 995 996 val frames = frame :: frames 997 in 998 SOME ((lines,lineIndent),lineSize,frames) 999 end 1000 | NONE => 1001 case breakInside lines lineIndent frames of 1002 SOME (lines_indent,lineSize,frames) => 1003 let 1004 val lineSize = lineSize + sizeFrame frame 1005 and frames = frame :: frames 1006 in 1007 SOME (lines_indent,lineSize,frames) 1008 end 1009 | NONE => NONE; 1010in 1011 fun breakFrames lines lineIndent frames = 1012 case breakUp lines lineIndent frames of 1013 SOME ((lines,lineIndent),lineSize,frames) => 1014 SOME (lines,lineIndent,lineSize,frames) 1015 | NONE => 1016 case breakInside lines lineIndent frames of 1017 SOME ((lines,lineIndent),lineSize,frames) => 1018 SOME (lines,lineIndent,lineSize,frames) 1019 | NONE => NONE; 1020end; 1021 1022(*BasicDebug 1023fun checkChunk chunk = 1024 case chunk of 1025 WordChunk t => (false, sizeWord t) 1026 | BreakChunk b => (false, sizeBreak b) 1027 | FrameChunk b => checkFrame b 1028 1029and checkChunks chunks = 1030 case chunks of 1031 [] => (false,0) 1032 | chunk :: chunks => 1033 let 1034 val (bk,sz) = checkChunk chunk 1035 1036 val (bk',sz') = checkChunks chunks 1037 in 1038 (bk orelse bk', sz + sz') 1039 end 1040 1041and checkFrame frame = 1042 let 1043 val Frame 1044 {block = _, 1045 broken, 1046 indent = _, 1047 size, 1048 chunks} = frame 1049 1050 val (bk,sz) = checkChunks chunks 1051 1052 val () = 1053 if size = sz then () 1054 else raise Bug "Print.checkFrame: wrong size" 1055 1056 val () = 1057 if broken orelse not bk then () 1058 else raise Bug "Print.checkFrame: deep broken frame" 1059 in 1060 (broken,size) 1061 end; 1062 1063fun checkFrames frames = 1064 case frames of 1065 [] => (true,0) 1066 | frame :: frames => 1067 let 1068 val (bk,sz) = checkFrame frame 1069 1070 val (bk',sz') = checkFrames frames 1071 1072 val () = 1073 if bk' orelse not bk then () 1074 else raise Bug "Print.checkFrame: broken stack frame" 1075 in 1076 (bk, sz + sz') 1077 end; 1078*) 1079 1080(*BasicDebug 1081fun checkState state = 1082 (let 1083 val State {lineIndent,lineSize,stack} = state 1084 1085 val () = 1086 if not (List.null stack) then () 1087 else raise Error "no stack" 1088 1089 val (_,sz) = checkFrames stack 1090 1091 val () = 1092 if lineSize = sz then () 1093 else raise Error "wrong lineSize" 1094 in 1095 () 1096 end 1097 handle Error err => raise Bug err) 1098 handle Bug bug => raise Bug ("Print.checkState: " ^ bug); 1099*) 1100 1101fun isEmptyState state = 1102 let 1103 val State {lineSize,stack,...} = state 1104 in 1105 lineSize = 0 andalso List.all isEmptyFrame stack 1106 end; 1107 1108fun isFinalState state = 1109 let 1110 val State {stack,...} = state 1111 in 1112 case stack of 1113 [] => raise Bug "Print.isFinalState: empty stack" 1114 | [frame] => isEmptyFrame frame 1115 | _ :: _ :: _ => false 1116 end; 1117 1118local 1119 val initialBlock = 1120 let 1121 val indent = 0 1122 and style = Inconsistent 1123 in 1124 Block 1125 {indent = indent, 1126 style = style} 1127 end; 1128 1129 val initialFrame = 1130 let 1131 val block = initialBlock 1132 and broken = false 1133 and indent = 0 1134 and size = 0 1135 and chunks = [] 1136 in 1137 Frame 1138 {block = block, 1139 broken = broken, 1140 indent = indent, 1141 size = size, 1142 chunks = chunks} 1143 end; 1144in 1145 val initialState = 1146 let 1147 val lineIndent = 0 1148 and lineSize = 0 1149 and stack = [initialFrame] 1150 in 1151 State 1152 {lineIndent = lineIndent, 1153 lineSize = lineSize, 1154 stack = stack} 1155 end; 1156end; 1157 1158fun normalizeState lineLength lines state = 1159 let 1160 val State {lineIndent,lineSize,stack} = state 1161 1162 val within = 1163 case lineLength of 1164 NONE => true 1165 | SOME len => lineIndent + lineSize <= len 1166 in 1167 if within then (lines,state) 1168 else 1169 case breakFrames lines lineIndent stack of 1170 NONE => (lines,state) 1171 | SOME (lines,lineIndent,lineSize,stack) => 1172 let 1173(*BasicDebug 1174 val () = checkState state 1175*) 1176 val state = 1177 State 1178 {lineIndent = lineIndent, 1179 lineSize = lineSize, 1180 stack = stack} 1181 in 1182 normalizeState lineLength lines state 1183 end 1184 end 1185(*BasicDebug 1186 handle Bug bug => raise Bug ("Print.normalizeState:\n" ^ bug) 1187*) 1188 1189local 1190 fun executeBeginBlock block lines state = 1191 let 1192 val State {lineIndent,lineSize,stack} = state 1193 1194 val broken = false 1195 and indent = indentBlock block 1196 and size = 0 1197 and chunks = [] 1198 1199 val frame = 1200 Frame 1201 {block = block, 1202 broken = broken, 1203 indent = indent, 1204 size = size, 1205 chunks = chunks} 1206 1207 val stack = frame :: stack 1208 1209 val state = 1210 State 1211 {lineIndent = lineIndent, 1212 lineSize = lineSize, 1213 stack = stack} 1214 in 1215 (lines,state) 1216 end; 1217 1218 fun executeEndBlock lines state = 1219 let 1220 val State {lineIndent,lineSize,stack} = state 1221 1222 val (lineSize,stack) = 1223 case stack of 1224 [] => raise Bug "Print.executeEndBlock: empty stack" 1225 | topFrame :: stack => 1226 let 1227 val Frame 1228 {block = topBlock, 1229 broken = topBroken, 1230 indent = topIndent, 1231 size = topSize, 1232 chunks = topChunks} = topFrame 1233 1234 val (lineSize,topSize,topChunks,topFrame) = 1235 case topChunks of 1236 BreakChunk break :: chunks => 1237 let 1238(*BasicDebug 1239 val () = 1240 let 1241 val mesg = 1242 "ignoring a break at the end of a " ^ 1243 "pretty-printing block" 1244 in 1245 warn mesg 1246 end 1247*) 1248 val n = sizeBreak break 1249 1250 val lineSize = lineSize - n 1251 and topSize = topSize - n 1252 and topChunks = chunks 1253 1254 val topFrame = 1255 Frame 1256 {block = topBlock, 1257 broken = topBroken, 1258 indent = topIndent, 1259 size = topSize, 1260 chunks = topChunks} 1261 in 1262 (lineSize,topSize,topChunks,topFrame) 1263 end 1264 | _ => (lineSize,topSize,topChunks,topFrame) 1265 in 1266 if List.null topChunks then (lineSize,stack) 1267 else 1268 case stack of 1269 [] => raise Error "Print.execute: too many end blocks" 1270 | frame :: stack => 1271 let 1272 val Frame 1273 {block, 1274 broken, 1275 indent, 1276 size, 1277 chunks} = frame 1278 1279 val size = size + topSize 1280 1281 val chunk = FrameChunk topFrame 1282 1283 val chunks = chunk :: chunks 1284 1285 val frame = 1286 Frame 1287 {block = block, 1288 broken = broken, 1289 indent = indent, 1290 size = size, 1291 chunks = chunks} 1292 1293 val stack = frame :: stack 1294 in 1295 (lineSize,stack) 1296 end 1297 end 1298 1299 val state = 1300 State 1301 {lineIndent = lineIndent, 1302 lineSize = lineSize, 1303 stack = stack} 1304 in 1305 (lines,state) 1306 end; 1307 1308 fun executeAddWord lineLength word lines state = 1309 let 1310 val State {lineIndent,lineSize,stack} = state 1311 1312 val n = sizeWord word 1313 1314 val lineSize = lineSize + n 1315 1316 val stack = 1317 case stack of 1318 [] => raise Bug "Print.executeAddWord: empty stack" 1319 | frame :: stack => 1320 let 1321 val Frame 1322 {block, 1323 broken, 1324 indent, 1325 size, 1326 chunks} = frame 1327 1328 val size = size + n 1329 1330 val chunk = WordChunk word 1331 1332 val chunks = chunk :: chunks 1333 1334 val frame = 1335 Frame 1336 {block = block, 1337 broken = broken, 1338 indent = indent, 1339 size = size, 1340 chunks = chunks} 1341 1342 val stack = frame :: stack 1343 in 1344 stack 1345 end 1346 1347 val state = 1348 State 1349 {lineIndent = lineIndent, 1350 lineSize = lineSize, 1351 stack = stack} 1352 in 1353 normalizeState lineLength lines state 1354 end; 1355 1356 fun executeAddBreak lineLength break lines state = 1357 let 1358 val State {lineIndent,lineSize,stack} = state 1359 1360 val (topFrame,restFrames) = 1361 case stack of 1362 [] => raise Bug "Print.executeAddBreak: empty stack" 1363 | topFrame :: restFrames => (topFrame,restFrames) 1364 1365 val Frame 1366 {block = topBlock, 1367 broken = topBroken, 1368 indent = topIndent, 1369 size = topSize, 1370 chunks = topChunks} = topFrame 1371 in 1372 case topChunks of 1373 [] => (lines,state) 1374 | topChunk :: restTopChunks => 1375 let 1376 val (topChunks,n) = 1377 case topChunk of 1378 BreakChunk break' => 1379 let 1380 val break = appendBreak break' break 1381 1382 val chunk = BreakChunk break 1383 1384 val topChunks = chunk :: restTopChunks 1385 and n = sizeBreak break - sizeBreak break' 1386 in 1387 (topChunks,n) 1388 end 1389 | _ => 1390 let 1391 val chunk = BreakChunk break 1392 1393 val topChunks = chunk :: topChunks 1394 and n = sizeBreak break 1395 in 1396 (topChunks,n) 1397 end 1398 1399 val lineSize = lineSize + n 1400 1401 val topSize = topSize + n 1402 1403 val topFrame = 1404 Frame 1405 {block = topBlock, 1406 broken = topBroken, 1407 indent = topIndent, 1408 size = topSize, 1409 chunks = topChunks} 1410 1411 val stack = topFrame :: restFrames 1412 1413 val state = 1414 State 1415 {lineIndent = lineIndent, 1416 lineSize = lineSize, 1417 stack = stack} 1418 1419 val lineLength = 1420 if breakingFrame topFrame then SOME ~1 else lineLength 1421 in 1422 normalizeState lineLength lines state 1423 end 1424 end; 1425 1426 fun executeBigBreak lines state = 1427 let 1428 val lineLength = SOME ~1 1429 and break = mkBreak 0 1430 in 1431 executeAddBreak lineLength break lines state 1432 end; 1433 1434 fun executeAddNewline lineLength lines state = 1435 if isEmptyState state then (addEmptyLine lines, state) 1436 else executeBigBreak lines state; 1437 1438 fun executeEof lineLength lines state = 1439 if isFinalState state then (lines,state) 1440 else 1441 let 1442 val (lines,state) = executeBigBreak lines state 1443 1444(*BasicDebug 1445 val () = 1446 if isFinalState state then () 1447 else raise Bug "Print.executeEof: not a final state" 1448*) 1449 in 1450 (lines,state) 1451 end; 1452in 1453 fun render {lineLength} = 1454 let 1455 fun execute step state = 1456 let 1457 val lines = [] 1458 in 1459 case step of 1460 BeginBlock block => executeBeginBlock block lines state 1461 | EndBlock => executeEndBlock lines state 1462 | AddWord word => executeAddWord lineLength word lines state 1463 | AddBreak break => executeAddBreak lineLength break lines state 1464 | AddNewline => executeAddNewline lineLength lines state 1465 end 1466 1467(*BasicDebug 1468 val execute = fn step => fn state => 1469 let 1470 val (lines,state) = execute step state 1471 1472 val () = checkState state 1473 in 1474 (lines,state) 1475 end 1476 handle Bug bug => 1477 raise Bug ("Print.execute: after " ^ toStringStep step ^ 1478 " command:\n" ^ bug) 1479*) 1480 1481 fun final state = 1482 let 1483 val lines = [] 1484 1485 val (lines,state) = executeEof lineLength lines state 1486 1487(*BasicDebug 1488 val () = checkState state 1489*) 1490 in 1491 if List.null lines then Stream.Nil else Stream.singleton lines 1492 end 1493(*BasicDebug 1494 handle Bug bug => raise Bug ("Print.final: " ^ bug) 1495*) 1496 in 1497 fn pps => 1498 let 1499 val lines = Stream.maps execute final initialState pps 1500 in 1501 revConcat lines 1502 end 1503 end; 1504end; 1505 1506local 1507 fun inc {indent,line} acc = line :: nSpaces indent :: acc; 1508 1509 fun incn (indent_line,acc) = inc indent_line ("\n" :: acc); 1510in 1511 fun toStringWithLineLength len ppA a = 1512 case render len (ppA a) of 1513 Stream.Nil => "" 1514 | Stream.Cons (h,t) => 1515 let 1516 val lines = Stream.foldl incn (inc h []) (t ()) 1517 in 1518 String.concat (List.rev lines) 1519 end; 1520end; 1521 1522local 1523 fun renderLine {indent,line} = nSpaces indent ^ line ^ "\n"; 1524in 1525 fun toStreamWithLineLength len ppA a = 1526 Stream.map renderLine (render len (ppA a)); 1527end; 1528 1529fun toLine ppA a = toStringWithLineLength {lineLength = NONE} ppA a; 1530 1531(* ------------------------------------------------------------------------- *) 1532(* Pretty-printer rendering with a global line length. *) 1533(* ------------------------------------------------------------------------- *) 1534 1535val lineLength = ref initialLineLength; 1536 1537fun toString ppA a = 1538 let 1539 val len = {lineLength = SOME (!lineLength)} 1540 in 1541 toStringWithLineLength len ppA a 1542 end; 1543 1544fun toStream ppA a = 1545 let 1546 val len = {lineLength = SOME (!lineLength)} 1547 in 1548 toStreamWithLineLength len ppA a 1549 end; 1550 1551local 1552 val sep = mkWord " ="; 1553in 1554 fun trace ppX nameX x = 1555 Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n"); 1556end; 1557 1558end 1559