|
| 1 | +import /List |
| 2 | +import open /Test |
| 3 | + |
| 4 | +type Width = Int |
| 5 | +type Dangling = Int |
| 6 | + |
| 7 | +{## |
| 8 | + Shift list aka `SList' |
| 9 | + |
| 10 | + Structure stores width as a list of floating elements. |
| 11 | + Floating aka floating elements will align globally with other floating |
| 12 | + elements. |
| 13 | + |
| 14 | + `SFix' represents singular unmoveable object. |
| 15 | + |
| 16 | + Each `SShift' stores an information about floating elements that |
| 17 | + are willing to globally align with others. |
| 18 | + |
| 19 | + The `SLast' node is a label that indicates a line where <> will attach |
| 20 | + foramatted text. In every Size object there is exactly one SLast node. |
| 21 | + ##} |
| 22 | +data rec SList = |
| 23 | + | SFix of Width |
| 24 | + | SShift of Width, Dangling, SList |
| 25 | + | SLast of Width, SList |
| 26 | + |
| 27 | +method rec format {?prec : Int, ?fmt : Unit} (self : SList) = |
| 28 | + match self with |
| 29 | + | SFix fix => "SF \{fix}" |
| 30 | + | SShift sep dangl tl => "SS \{sep} \{dangl} (\{tl})" |
| 31 | + | SLast last tl => "SL \{last} (\{tl})" |
| 32 | + end |
| 33 | + |
| 34 | +method rec equal (s1 : SList) (s2 : SList) = |
| 35 | + match (s1, s2) with |
| 36 | + | SFix v1, SFix v2 => v1 == v2 |
| 37 | + | SShift i1 j1 s1, SShift i2 j2 s2 => i1 == i2 && j1 == j2 && s1 == s2 |
| 38 | + | SLast i1 s1, SLast i2 s2 => i1 == i2 && s1 == s2 |
| 39 | + | _ => False |
| 40 | + end |
| 41 | + |
| 42 | +{## |
| 43 | + Structure stores a size of a given thunk of formatted text. |
| 44 | + |
| 45 | + Height is given explicitly, width is stored as a `shift list'. |
| 46 | + ##} |
| 47 | +data Size = |
| 48 | + { width : SList |
| 49 | + , height : Int |
| 50 | + } |
| 51 | + |
| 52 | +method format (self : Size) = |
| 53 | + "Size {width = \{self.width}, height = \{self.height}}" |
| 54 | + |
| 55 | +method equal (w1 : Size) (w2 : Size) = |
| 56 | + w1.width == w2.width && w1.height == w2.height |
| 57 | + |
| 58 | +{## Constructs Size object for a singular string ##} |
| 59 | +let text (s : String) = Size {width=SLast s.length (SFix s.length), height=0} |
| 60 | + |
| 61 | +{## Empty width ##} |
| 62 | +let empty = text "" |
| 63 | + |
| 64 | +{## Inserts newline ##} |
| 65 | +method flush (Size {width, height}) = |
| 66 | + let rec dropL w = match w with |
| 67 | + | SShift i j tl => SShift i j (dropL tl) |
| 68 | + | SLast _ tl => tl |
| 69 | + | SFix i => impossible () |
| 70 | + end in |
| 71 | + Size {width = SLast 0 (dropL width), height = height + 1} |
| 72 | + |
| 73 | +{## |
| 74 | + Calculates size after <> operation as such: |
| 75 | + |
| 76 | + _____________ _____________ |
| 77 | + | | >shift> | | >shift> |.....| |
| 78 | + | __| | __| |
| 79 | + |________| |________| <> _____________ |
| 80 | + | | >....> |
| 81 | + | __| |
| 82 | + |________| |
| 83 | + ##} |
| 84 | +method combine (w1 : Size) (w2 : Size) = |
| 85 | + let height = w1.height + w2.height in |
| 86 | + |
| 87 | + # Moves a shift list by a fixed amount |
| 88 | + let rec moveBy w xs = match xs with |
| 89 | + | SLast i tl => SLast (i + w) (moveBy w tl) |
| 90 | + | SFix i => SFix (i + w) |
| 91 | + | SShift i j tl => SShift (i + w) (j + w) tl |
| 92 | + end in |
| 93 | + |
| 94 | + # Handles paraller join of two given shift list |
| 95 | + # By assumpion w1 does NOT contain SLast label |
| 96 | + let rec combineWs (w1 : SList) (w2 : SList) = |
| 97 | + match (w1, w2) with |
| 98 | + ## regular elements |
| 99 | + |
| 100 | + # take maximum over elements |
| 101 | + | SFix i, SFix i' => SFix (max i i') |
| 102 | + | SShift i j w1, SShift i' j' w2 => |
| 103 | + SShift (max i i') (max j j') (combineWs w1 w2) |
| 104 | + |
| 105 | + # add SFix as a dangling width |
| 106 | + | SFix i, SShift i' j' w2 => SShift i' (max i j') w2 |
| 107 | + | SShift i j w1, SFix i' => SShift i (max j i') w1 |
| 108 | + |
| 109 | + ## right last - copy last and continue as usual |
| 110 | + | w1, SLast last w2 => SLast last (combineWs w1 w2) |
| 111 | + |
| 112 | + # left last and anything else |
| 113 | + | _ => impossible () |
| 114 | + end in |
| 115 | + |
| 116 | + # The starting point of algorithm |
| 117 | + # The <> catenation happens at `SLast' node of w1, thus |
| 118 | + # width is copied up until `SLast' and then combineWs |
| 119 | + # operation is permormed. The SLast label will be |
| 120 | + # propagated from w2 |
| 121 | + let rec copyTillL (w1 : SList) (w2 : SList) = |
| 122 | + match w1 with |
| 123 | + | SFix _ => impossible () |
| 124 | + | SShift i j tl => SShift i j (copyTillL tl w2) |
| 125 | + | SLast w tl => combineWs tl (moveBy w w2) |
| 126 | + end in |
| 127 | + |
| 128 | + Size {width = copyTillL w1.width w2.width, height} |
| 129 | + |
| 130 | +{## Fixes shifts in place and propagates fixed width information ##} |
| 131 | +method reset (w : Size) = |
| 132 | + let rec iter (xs : SList) = match xs with |
| 133 | + | SFix fix => (fix, None) |
| 134 | + | SLast last tl => (fst (iter tl), Some last) |
| 135 | + | SShift step dangling tl => |
| 136 | + let tl = iter tl in |
| 137 | + let tot = max dangling (step + tl.fst) in |
| 138 | + (tot, tl.snd.map (fn x => (step + x))) |
| 139 | + end in |
| 140 | + match iter w.width with |
| 141 | + | (fix, Some last) => |
| 142 | + Size { width = SLast fix (SFix last), height = w.height } |
| 143 | + | _ => impossible () |
| 144 | + end |
| 145 | + |
| 146 | +{## Adds an empty shift. ##} |
| 147 | +method shift (Size {width, height}) = |
| 148 | + Size {width = SShift 0 0 width, height} |
| 149 | + |
| 150 | +{## |
| 151 | + Calculates true vertiacal catenation. |
| 152 | + |
| 153 | + To simplify calculation, vcat can performed only if dangling width |
| 154 | + of every SShift node of w1 is 0. To preserve monoid like behaviour |
| 155 | + of this operation, same restriction have been put on w2. |
| 156 | +##} |
| 157 | +let seqE {~onError} (w1 : Size) (w2 : Size) = |
| 158 | + let rec checkAssumpions (sh : SList) = match sh with |
| 159 | + | SLast _ tl => checkAssumpions tl |
| 160 | + | SFix _ => () |
| 161 | + | SShift _ dangle tl => |
| 162 | + if dangle != 0 then |
| 163 | + ~onError () |
| 164 | + else |
| 165 | + checkAssumpions tl |
| 166 | + end in |
| 167 | + let _ = checkAssumpions w1.width |
| 168 | + let _ = checkAssumpions w2.width |
| 169 | + |
| 170 | + let rec join s = match s with |
| 171 | + | SLast x tl => join tl |
| 172 | + | SShift i j tl => SShift i j (join tl) |
| 173 | + | SFix i => match w2.width with |
| 174 | + | SLast l (SFix i') => SLast (l + i) (SFix (i' + i)) |
| 175 | + | SLast l (SShift i' j' tl) => SLast (l + i) (SShift (i' + i) 0 tl) |
| 176 | + | SShift i' j' tl => SShift (i' + i) 0 tl |
| 177 | + | _ => impossible () |
| 178 | + end |
| 179 | + end in |
| 180 | + Size {height = max w1.height w2.height, width = join w1.width} |
| 181 | + |
| 182 | +method seq {~__line__, ~__file__} w1 w2 = |
| 183 | + let ~onError () = runtimeError "Cannot perform vcat" in |
| 184 | + seqE w1 w2 |
| 185 | + |
| 186 | +let (<>) (s : Size) = s.combine |
| 187 | +let ($$) (s : Size) = s.flush.combine |
| 188 | +let (<+>) (s : Size) = s.seq |
| 189 | + |
| 190 | +let _ = testSuite "PrettyPrinter/Size" (fn () => |
| 191 | + testCase "Empty has 0 width" (fn () => |
| 192 | + assertEq empty.width (SLast 0 (SFix 0))); |
| 193 | + |
| 194 | + testCase "Empty has 0 height" (fn () => |
| 195 | + assertEq empty.height 0); |
| 196 | + |
| 197 | + testCase "Text has fix width" (fn () => |
| 198 | + ["", "abc", "jak-to-jest-byc-skyba?"].iter (fn str => |
| 199 | + assertEq (text str).width (SLast str.length (SFix str.length)))); |
| 200 | + |
| 201 | + testCase "Text has 0 height" (fn () => |
| 202 | + ["", "abc", "jak-to-jest-byc-skyba?"].iter (fn str => |
| 203 | + assertEq (text str).height 0)); |
| 204 | + |
| 205 | + testCase "Empty text <> identity" (fn () => |
| 206 | + let t = text "abc" in |
| 207 | + assertEq t (t <> empty); |
| 208 | + assertEq t (empty <> t)); |
| 209 | + |
| 210 | + testCase "Simple text <>" (fn () => |
| 211 | + let t = text "abc" <> text "def" in |
| 212 | + assertEq t.width (SLast 6 (SFix 6)); |
| 213 | + assertEq t.height 0); |
| 214 | + |
| 215 | + testCase "Semigroup <>" (fn () => |
| 216 | + let t1 = text "defghijk" |
| 217 | + let t2 = text "abc" |
| 218 | + let t3 = text "asdasd" in |
| 219 | + assertEq ((t1 <> t2) <> t3) (t1 <> (t2 <> t3))); |
| 220 | + |
| 221 | + testCase "Simple flush" (fn () => |
| 222 | + let t = text "abc" >. flush in |
| 223 | + assertEq t.height 1; |
| 224 | + assertEq t.width (SLast 0 (SFix 3))); |
| 225 | + |
| 226 | + testCase "Simple $$ 1" (fn () => |
| 227 | + let t = text "abc" $$ text "defghijk" in |
| 228 | + assertEq t.height 1; |
| 229 | + assertEq t.width (SLast 8 (SFix 8))); |
| 230 | + |
| 231 | + testCase "Simple $$ 2" (fn () => |
| 232 | + let t = text "defghijk" $$ text "abc" in |
| 233 | + assertEq t.height 1; |
| 234 | + assertEq t.width (SLast 3 (SFix 8))); |
| 235 | + |
| 236 | + testCase "Semigroup $$" (fn () => |
| 237 | + let t1 = text "defghijk" |
| 238 | + let t2 = text "abc" |
| 239 | + let t3 = text "asdasd" in |
| 240 | + assertEq ((t1 $$ t2) $$ t3) (t1 $$ (t2 $$ t3))); |
| 241 | + |
| 242 | + testCase "Semigroup <> with $$" (fn () => |
| 243 | + let t1 = text "aaaaaaaaaa" $$ text "aa" |
| 244 | + let t2 = text "bbb" $$ text "bbbbbb" |
| 245 | + let t3 = text "ccccccc" $$ text "cc" in |
| 246 | + assertEq ((t1 <> t2) <> t3) (t1 <> (t2 <> t3))); |
| 247 | + |
| 248 | + testCase "Simple shift" (fn () => |
| 249 | + let t1 = text "abc" >.shift in |
| 250 | + assertEq t1.height 0; |
| 251 | + assertEq t1.width (SShift 0 0 (SLast 3 (SFix 3)))); |
| 252 | + |
| 253 | + testCase "Reset identity over text" (fn () => |
| 254 | + let t1 = text "abc" in |
| 255 | + assertEq t1 t1.reset); |
| 256 | + |
| 257 | + testCase "Shift add width" (fn () => |
| 258 | + let t = text "abc" in |
| 259 | + assertEqF (t <> t.shift).width (SShift 3 3 (SLast 3 (SFix 3)))); |
| 260 | + |
| 261 | + testCase "Shift/reset" (fn () => |
| 262 | + let t = text "abc" in |
| 263 | + assertEqF (t <> t.shift).reset.width (SLast 6 (SFix 6))); |
| 264 | + |
| 265 | + testCase "Shift aligns paraller structures" (fn () => |
| 266 | + let t1 = text "aaaaa" <> (text "bb" >.shift) <> (text "ccccc" >.shift) |
| 267 | + let t2 = text "aa" <> (text "bbbbb" >.shift) <> (text "cc" >. shift) in |
| 268 | + assertEqF (t1 $$ t2).width (SShift 5 5 (SShift 5 5 (SLast 2 (SFix 5))))); |
| 269 | + ()) |
0 commit comments