
   0 | module Language.LSP.VirtualDocument
   1 | 
   2 | -- The VirtualDocument is the version of the document that the LSP server maintains
   3 | -- based on the incoming DidChange events. It should mirror the actively edited but
   4 | -- unsaved content of the opened documents.
   5 | 
   6 | import Data.Nat
   7 | import Data.List
   8 | import Data.String
   9 | import Data.OneOf
  10 | import Language.LSP.Message.Location
  11 | import Language.LSP.Message.TextDocument
  12 | import Decidable.Equality
  13 | import Data.DPair
  14 | import Control.Function
  15 | import Syntax.PreorderReasoning
  16 | import Data.Void
  17 | 
  18 | %default total
  19 | 
  20 | 
  21 | -- As the edits come in incremental change, the virtual document must be
  22 | -- updated accordingly. The string needs to be split in a particular way,
  23 | -- as detailed below:
  24 | --
  25 | -- Cut the string in half.
  26 | --
  27 | -- The `rangeSplit` cuts the string into three parts based on a Range.
  28 | --
  29 | -- In a Range based edit, the client sends a text that must replace the part
  30 | -- within the Range found in the edit request. The Range consists of a start
  31 | -- and an end position. Positions consist of a line and a character index.
  32 | --
  33 | -- Although the Position is encoded with line and char index, the file is
  34 | -- represented as a String, in which a natural number indexes characters.
  35 | -- The Position must be mapped to the string index-based encoding, which
  36 | -- can be done via a string traversal. When a newline character is found,
  37 | -- the line index is decreased. When the line index reaches zero, the character
  38 | -- index is decreased. When the character index reaches zero, the string index of
  39 | -- the Position is found. See below:
  40 | --
  41 | -- ...      m         n         p
  42 | -- ...4567890123456789012345678901234567890....  (positions in string)
  43 | --          ^              ^
  44 | --        start           end                    (range in format (line:character))
  45 | --
  46 | -- As the text edit replaces a string in the Range, the prefix of the string
  47 | -- must be kept. This means (0..start-1) both indexes included, then the new
  48 | -- string must be inserted, and after the string from the end position must
  49 | -- be included (end..length-1), both indexes included.
  50 | --
  51 | -- Although the situation is complex, the position encoding is based on line
  52 | -- and character index, which must be decreased appropriately; the new line
  53 | -- encoding of \r\n vs \n makes it trickier. However, this module only handles \n case.
  54 | --
  55 | -- Another complication is that the positions could refer to non-existing parts
  56 | -- of the content. Such as, the Position could point after the end of
  57 | -- the line end of the file.
  58 | --
  59 | -- The [before the first character of the line] range is encoded as the start position
  60 | -- pointing after the line's last character and at the new line's first character
  61 | -- such as (l,c+1) and (l+1,0).
  62 | --
  63 | -- Characters that point after the last character are considered invalid Range,
  64 | -- and it must be interpreted as the last character of the line.
  65 | 
  66 | 
  67 | Pos : Type
  68 | Pos = (Nat, Nat)
  69 | 
  70 | ||| Line length as defined in LSP, newline character is not counted in.
  71 | |||
  72 | ||| See more:
  73 | ||| https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#position
  74 | lineLength : String -> Nat
  75 | lineLength ""  = 0
  76 | lineLength str = assert_total $
  77 |   let l = strLength str in
  78 |   if isNL (strIndex str (l - 1))
  79 |     then minus (cast l) 1
  80 |     else cast l
  81 | 
  82 | -- Take the string up to the position, character addressed by the position is included.
  83 | takePos : Pos -> String -> String
  84 | takePos (l,c) str =
  85 |   let ls : List String = lines str in
  86 |   let ln : Nat         = length ls in
  87 |   case l < ln of
  88 |     False => fastUnlines ls
  89 |     True  =>
  90 |       let (pre, post) = splitAt l ls in
  91 |       case post of
  92 |         [] => fastUnlines pre
  93 |         (pl :: _) =>
  94 |           let ll : Nat := lineLength pl in
  95 |           let cx : Nat := if c > ll then ll else c in
  96 |           fastUnlines $ pre ++ [strSubstr 0 (cast cx) pl]
  97 | 
  98 | -- Drop the string up to the position, character addressed by the position is excluded.
  99 | dropPos : Pos -> String -> String
 100 | dropPos (l,c) str =
 101 |   let ls : List String = lines str in
 102 |   let ln : Nat         = length ls in
 103 |   case l < ln of
 104 |     False => "\n" -- Assumes always a newline at the end.
 105 |     True =>
 106 |       let (pre, post) = splitAt l ls in
 107 |       case post of
 108 |         [] => "\n"
 109 |         (pl :: prest) =>
 110 |           let ll : Nat := lineLength pl in
 111 |           let cx : Nat := if c > ll then ll else c in
 112 |           fastUnlines $ (strSubstr (cast cx) (cast (minus (cast (strLength pl)) cx)) pl :: prest)
 113 | 
 114 | -- Newline character is always assumed from takePos and dropPos, and they must be
 115 | -- removed to re-establish consistency. The SubString operations should be quick.
 116 | dropLastNL : String -> String
 117 | dropLastNL str = assert_total $ case strLength str of
 118 |   0 => str
 119 |   n => strSubstr 0 (n - 1) str
 120 | 
 121 | -- Computes the pre and post part for the given range. Drops the part which is addressed by the range.
 122 | rangeSplit : Pos -> Pos -> String -> (String, String)
 123 | rangeSplit s e str = (dropLastNL $ takePos s str, dropLastNL $ dropPos e str)
 124 | 
 125 | ||| Updates the content string with the new string replacing the part between the start and end positions.
 126 | |||
 127 | ||| This function is an approximation as the implementation is based on unlines and lines,
 128 | ||| and the lines function adds newline characters. The edge-case around newlines
 129 | ||| at the end of files is simplified to assume that the virtual content always
 130 | ||| has the empty line as the last line.
 131 | update : Pos -> Pos -> String -> String -> String
 132 | update s e new content =
 133 |   let (pre, post) = rangeSplit s e content in
 134 |   fastConcat [pre, new, post, "\n"]
 135 | 
 136 | -- * Identifier
 137 | 
 138 | -- Oversimplified version of the identifier.
 139 | isIdentifierChar : Char -> Bool
 140 | isIdentifierChar c = or [isAlphaNum c, c == '.', c == '_', c == '\'']
 141 | 
 142 | -- * Word at position
 143 | 
 144 | -- Determines the identifier at the index.
 145 | --
 146 | -- The implementation tart out scanning for the start position
 147 | -- of the identifier and then looks for the end position.
 148 | identifierAtIndex : String -> Nat -> String
 149 | identifierAtIndex ""  i = ""
 150 | identifierAtIndex str i = identifierPre (minus i 1) i
 151 |   where
 152 |     l : Nat
 153 |     l = cast (strLength str)
 154 | 
 155 |     identifierPost : Nat -> Nat -> String
 156 |     identifierPost n Z = assert_total $ case isIdentifierChar (strIndex str (cast Z)) of
 157 |       True => identifierPost n (S Z)
 158 |       False => "" -- n < m -- assumed and this means an empty result
 159 |     identifierPost n (S m) = assert_total $ case (S m) == l of
 160 |       True  => strSubstr (cast n) (cast (minus (S m) n)) str
 161 |       False => case isIdentifierChar (strIndex str (cast (S m))) of
 162 |         True  => identifierPost n (S (S m))
 163 |         False => strSubstr (cast n) (cast (minus (S m) n)) str
 164 | 
 165 |     identifierPre : Nat -> Nat -> String
 166 |     identifierPre Z m = assert_total $ case isIdentifierChar (strIndex str (cast Z)) of
 167 |       True  => identifierPost Z m
 168 |       False => identifierPost (S Z) m
 169 |     identifierPre (S n) m = assert_total $ case isIdentifierChar (strIndex str (cast (S n))) of
 170 |       True  => identifierPre n m
 171 |       False => identifierPost (S (S n)) m
 172 | 
 173 | -- Identifier at position.
 174 | --
 175 | -- Picks the line and char, if exists, otherwise reports empty string.
 176 | identifierAtPos : Pos -> String -> String
 177 | identifierAtPos (l,c) str =
 178 |   let ls : List String := lines str in
 179 |   let ln : Nat         := length ls in
 180 |   case l > ln of
 181 |     True  => ""
 182 |     False => case drop l ls of
 183 |       []        => ""
 184 |       (line::_) =>
 185 |         let ll : Nat := lineLength line in
 186 |         let cx : Nat := if c > ll then ll else c in
 187 |         identifierAtIndex line cx
 188 | 
 189 | ||| Determines an identifier like string at a given position.
 190 | |||
 191 | ||| The empty String will be reported if the position points to a non-existent
 192 | ||| part of the String. This function is needed when generating the suggestion list.
 193 | export
 194 | identifierAtPosition : Position -> String -> String
 195 | identifierAtPosition (MkPosition line character) str = identifierAtPos (cast line, cast character) str
 196 | 
 197 | -- * LSP API
 198 | 
 199 | validRange : (startline, startchar, endline, endchar : Nat) -> Bool
 200 | validRange startline startchar endline endchar =
 201 |   case compare startline endline of
 202 |     LT => True
 203 |     EQ => case compare startchar endchar of
 204 |       LT => True
 205 |       EQ => True
 206 |       GT => False
 207 |     GT => False
 208 | 
 209 | changeRange : Range -> String -> String -> Either String String
 210 | changeRange (MkRange (MkPosition sl sc) (MkPosition el ec)) content str =
 211 |   case validRange (cast sl) (cast sc) (cast el) (cast ec) of
 212 |     False => Left "Invalid range: \{show (sl,sc,el,ec)}"
 213 |     True  => Right $ update (cast sl, cast sc) (cast el, cast ec) str content
 214 | 
 215 | contentChangeEvent : TextDocumentContentChangeEvent -> String
 216 | contentChangeEvent (MkTextDocumentContentChangeEvent text) = text
 217 | 
 218 | contentChangeEventWithRange : TextDocumentContentChangeEventWithRange -> String -> Either String String
 219 | contentChangeEventWithRange
 220 |       (MkTextDocumentContentChangeEventWithRange range rangeLength text)
 221 |       content
 222 |   = changeRange range content text
 223 | 
 224 | contentChangeOneOf : OneOf [TextDocumentContentChangeEvent, TextDocumentContentChangeEventWithRange] -> String -> Either String String
 225 | contentChangeOneOf (Here c)         _ = Right $ contentChangeEvent c
 226 | contentChangeOneOf (There (Here r)) c = contentChangeEventWithRange r c
 227 | 
 228 | export
 229 | changeVirtualContent
 230 |   :  List (OneOf [TextDocumentContentChangeEvent, TextDocumentContentChangeEventWithRange])
 231 |   -> String -> Either String String
 232 | changeVirtualContent changes content = foldlM (flip contentChangeOneOf) content changes
 233 | 
 234 | ---------------------------
 235 | -- Poor man's testing :) --
 236 | ---------------------------
 237 | 
 238 | wordPosTestCase : Pos -> String -> String -> IO ()
 239 | wordPosTestCase p str expected = do
 240 |   let res = identifierAtPos p str
 241 |   if expected == res
 242 |     then do
 243 |       putStrLn "OK: identifierAtPos \{show p} \{show str} \{show expected}"
 244 |     else do
 245 |       putStrLn "Failed: identifierAtPos \{show p} \{show str} \{show expected}"
 246 |       putStrLn "Expected: \{show expected}"
 247 |       putStrLn "Got: \{show res}"
 248 | 
 249 | updateTestCase : Pos -> Pos -> String -> String -> String -> IO ()
 250 | updateTestCase s e new str expected = do
 251 |   let res = update s e new str
 252 |   if expected == res
 253 |     then do
 254 |       putStrLn "OK: update \{show s} \{show e} \{show new} \{show str}"
 255 |     else do
 256 |       putStrLn "Failed: update \{show s} \{show e} \{show new} \{show str}"
 257 |       putStrLn "Expected: \{show expected}"
 258 |       putStrLn "Got: \{show res}"
 259 | 
 260 | tests : IO ()
 261 | tests = do
 262 | 
 263 |   -- Update tests
 264 | 
 265 |   do -- Empty string
 266 |     let str = ""
 267 |     updateTestCase (0,0) (0,0) ""     str "\n"
 268 |     updateTestCase (0,0) (0,0) "a\nb" str "a\nb\n"
 269 |     updateTestCase (0,0) (0,1) "a"    str "a\n"
 270 |     updateTestCase (1,0) (1,0) "a"    str "a\n"
 271 |     updateTestCase (1,1) (1,1) "a"    str "a\n"
 272 |     updateTestCase (1,1) (1,2) "a"    str "a\n"
 273 |     updateTestCase (1,1) (2,2) "a"    str "a\n"
 274 | 
 275 |   do -- New line sting
 276 |     let str = " "
 277 |     updateTestCase (0,0) (0,0) ""     str " \n"
 278 |     updateTestCase (0,0) (0,0) "a\nb" str "a\nb \n"
 279 |     updateTestCase (0,0) (0,1) "a"    str "a\n"
 280 |     updateTestCase (1,0) (1,0) "a"    str " a\n"
 281 |     updateTestCase (1,1) (1,1) "a"    str " a\n"
 282 |     updateTestCase (2,1) (2,1) ""     str " \n"
 283 |     updateTestCase (2,1) (2,1) "a"    str " a\n"
 284 | 
 285 |   do -- New line sting
 286 |     let str = "\n"
 287 |     updateTestCase (0,0) (0,0) ""     str "\n"
 288 |     updateTestCase (0,0) (0,0) "a\nb" str "a\nb\n"
 289 |     updateTestCase (0,0) (0,1) "a"    str "a\n"
 290 |     updateTestCase (1,0) (1,0) "a"    str "a\n"
 291 |     updateTestCase (1,1) (1,1) "a"    str "a\n"
 292 |     updateTestCase (2,1) (2,1) ""     str "\n"
 293 |     updateTestCase (2,1) (2,1) "a"    str "a\n"
 294 | 
 295 |   do -- One line, no newline
 296 |     --         0         1   1
 297 |     --         012345678901234
 298 |     let str = "This is a line."
 299 |     updateTestCase (0,0) (0,0)   ""    str "This is a line.\n"
 300 |     updateTestCase (0,5) (0,5)   ""    str "This is a line.\n"
 301 |     updateTestCase (0,0) (0,0)   "a"   str "aThis is a line.\n"
 302 |     updateTestCase (0,5) (0,5)   "a"   str "This ais a line.\n"
 303 |     updateTestCase (0,5) (0,8)   "xx"  str "This xxa line.\n"
 304 |     updateTestCase (0,5) (0,15)  "aaa" str "This aaa\n"
 305 |     updateTestCase (0,3) (0,4)   ""    str "Thi is a line.\n"
 306 |     updateTestCase (0,11) (0,20) ""    str "This is a l\n"
 307 | 
 308 |   do -- One line, newline
 309 |     --         0         1       1
 310 |     --         0123456789012345678
 311 |     let str = "This is a newline.\n"
 312 |     updateTestCase (0,0) (0,0)  ""    str str
 313 |     updateTestCase (0,5) (0,5)  ""    str str
 314 |     updateTestCase (0,0) (0,0)  "a"   str "aThis is a newline.\n"
 315 |     updateTestCase (0,5) (0,5)  "a"   str "This ais a newline.\n"
 316 |     updateTestCase (0,5) (0,8)  "aa"  str "This aaa newline.\n"
 317 |     updateTestCase (0,5) (0,18) "aaa" str "This aaa\n"
 318 |     updateTestCase (0,18) (0,18) "a"  str "This is a newline.a\n"
 319 |     updateTestCase (0,11) (0,20) ""   str "This is a n\n"
 320 | 
 321 |   do -- Multiple lines, no newline at the last line.
 322 |           --   0         1         2  2 0         1         2   2 0         1         2 2
 323 |           --   012345678901234567890123 0123456789012345678901234 01234567890123456789012
 324 |     let str = "This is the first line.\nThis is the second line.\nThis is the third line."
 325 |     updateTestCase (1,0) (1,0)   ""   str (str ++ "\n")
 326 |     updateTestCase (1,0) (1,0)   "a"  str "This is the first line.\naThis is the second line.\nThis is the third line.\n"
 327 |     -- https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#range
 328 |     -- If you want to specify a range that contains a line including the line ending character(s)
 329 |     -- then use an end position denoting the start of the next line.
 330 |     updateTestCase (1,24) (2,0)  "a"  str "This is the first line.\nThis is the second line.aThis is the third line.\n"
 331 |     updateTestCase (1,19) (2,0)  "a"  str "This is the first line.\nThis is the second aThis is the third line.\n"
 332 |     updateTestCase (1,0)  (2,0)  ""   str "This is the first line.\nThis is the third line.\n"
 333 |     updateTestCase (1,0)  (2,0)  "a"  str "This is the first line.\naThis is the third line.\n"
 334 |     updateTestCase (1,8)  (2,8)  ""   str "This is the first line.\nThis is the third line.\n"
 335 |     updateTestCase (1,8)  (2,8)  "a " str "This is the first line.\nThis is a the third line.\n"
 336 |     updateTestCase (1,8)  (2,9)  "x"  str "This is the first line.\nThis is xhe third line.\n"
 337 |     updateTestCase (1,23) (2,22) ""   str "This is the first line.\nThis is the second line.\n"
 338 |     updateTestCase (1,23) (2,22) "a"  str "This is the first line.\nThis is the second linea.\n"
 339 |     updateTestCase (1,23) (2,23) "a"  str "This is the first line.\nThis is the second linea\n"
 340 |     updateTestCase (0,23) (1,24) ""   str "This is the first line.\nThis is the third line.\n"
 341 |     updateTestCase (1,0)  (1,40) ""   str "This is the first line.\n\nThis is the third line.\n"
 342 |     updateTestCase (1,0)  (1,24) ""   str "This is the first line.\n\nThis is the third line.\n"
 343 |     updateTestCase (1,10) (1,40) ""   str "This is the first line.\nThis is th\nThis is the third line.\n"
 344 |     updateTestCase (1,0)  (4,40) ""   str "This is the first line.\n\n"
 345 |     updateTestCase (1,10) (4,40) ""   str "This is the first line.\nThis is th\n"
 346 | 
 347 |   do -- Multiple lines, newline at the last line.
 348 |           --   0         1         2    0         1         2   2 0         1         2  2
 349 |           --   012345678901234567890123 0123456789012345678901234 012345678901234567890123
 350 |     let str = "This is the first line.\nThis is the second line.\nThis is the third line.\n"
 351 |     updateTestCase (1,0) (1,0)   ""   str str
 352 |     updateTestCase (1,0) (1,0)   "a"  str "This is the first line.\naThis is the second line.\nThis is the third line.\n"
 353 |     -- https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#range
 354 |     -- If you want to specify a range that contains a line including the line ending character(s)
 355 |     -- then use an end position denoting the start of the next line.
 356 |     updateTestCase (1,24) (2,0)  "a"  str "This is the first line.\nThis is the second line.aThis is the third line.\n"
 357 |     updateTestCase (1,19) (2,0)  "a"  str "This is the first line.\nThis is the second aThis is the third line.\n"
 358 |     updateTestCase (1,0)  (2,0)  ""   str "This is the first line.\nThis is the third line.\n"
 359 |     updateTestCase (1,0)  (2,0)  "a"  str "This is the first line.\naThis is the third line.\n"
 360 |     updateTestCase (1,8)  (2,8)  ""   str "This is the first line.\nThis is the third line.\n"
 361 |     updateTestCase (1,8)  (2,8)  "a " str "This is the first line.\nThis is a the third line.\n"
 362 |     updateTestCase (1,8)  (2,9)  "x"  str "This is the first line.\nThis is xhe third line.\n"
 363 |     updateTestCase (1,23) (2,22) ""   str "This is the first line.\nThis is the second line.\n"
 364 |     updateTestCase (1,23) (2,22) "a"  str "This is the first line.\nThis is the second linea.\n"
 365 |     updateTestCase (1,23) (2,23) "a"  str "This is the first line.\nThis is the second linea\n"
 366 |     updateTestCase (0,23) (1,24) ""   str "This is the first line.\nThis is the third line.\n"
 367 |     updateTestCase (1,0)  (1,40) ""   str "This is the first line.\n\nThis is the third line.\n"
 368 |     updateTestCase (1,0)  (1,24) ""   str "This is the first line.\n\nThis is the third line.\n"
 369 |     updateTestCase (1,10) (1,40) ""   str "This is the first line.\nThis is th\nThis is the third line.\n"
 370 |     updateTestCase (1,0)  (4,40) ""   str "This is the first line.\n\n"
 371 |     updateTestCase (1,10) (4,40) ""   str "This is the first line.\nThis is th\n"
 372 | 
 373 |   -- Word at position tests.
 374 | 
 375 |   do -- Empty string
 376 |     wordPosTestCase (0,0)  "" ""
 377 |     wordPosTestCase (0,10) "" ""
 378 |     wordPosTestCase (1,0)  "" ""
 379 |     wordPosTestCase (1,10) "" ""
 380 | 
 381 |   do -- New line
 382 |     wordPosTestCase (0,0)  "\n" ""
 383 |     wordPosTestCase (0,10) "\n" ""
 384 |     wordPosTestCase (1,0)  "\n" ""
 385 |     wordPosTestCase (1,10) "\n" ""
 386 |     wordPosTestCase (2,0)  "\n" ""
 387 |     wordPosTestCase (2,10) "\n" ""
 388 | 
 389 |   do -- Space character
 390 |     wordPosTestCase (0,0)  " " ""
 391 |     wordPosTestCase (0,10) " " ""
 392 |     wordPosTestCase (1,0)  " " ""
 393 |     wordPosTestCase (1,10) " " ""
 394 | 
 395 |   do -- One line without newline
 396 |     --         0         1   1
 397 |     --         012345678901234
 398 |     let str = "This is a line."
 399 |     wordPosTestCase (0,0)  str "This"
 400 |     wordPosTestCase (0,2)  str "This"
 401 |     wordPosTestCase (0,4)  str "This"
 402 |     wordPosTestCase (0,5)  str "is"
 403 |     wordPosTestCase (0,6)  str "is"
 404 |     wordPosTestCase (0,7)  str "is"
 405 |     wordPosTestCase (0,8)  str "a"
 406 |     wordPosTestCase (0,9)  str "a"
 407 |     wordPosTestCase (0,10) str "line."
 408 |     wordPosTestCase (0,12) str "line."
 409 |     wordPosTestCase (0,14) str "line."
 410 |     wordPosTestCase (0,20) str "line."
 411 |     wordPosTestCase (1,0)  str ""
 412 | 
 413 |   do -- One line with newline
 414 |     --         0         1    1
 415 |     --         0123456789012345
 416 |     let str = "This is a line.\n"
 417 |     wordPosTestCase (0,0)  str "This"
 418 |     wordPosTestCase (0,2)  str "This"
 419 |     wordPosTestCase (0,4)  str "This"
 420 |     wordPosTestCase (0,5)  str "is"
 421 |     wordPosTestCase (0,6)  str "is"
 422 |     wordPosTestCase (0,7)  str "is"
 423 |     wordPosTestCase (0,8)  str "a"
 424 |     wordPosTestCase (0,9)  str "a"
 425 |     wordPosTestCase (0,10) str "line."
 426 |     wordPosTestCase (0,12) str "line."
 427 |     wordPosTestCase (0,14) str "line."
 428 |     wordPosTestCase (0,20) str "line."
 429 |     wordPosTestCase (1,0)  str ""
 430 | 
 431 |   do -- Three lines without newline
 432 |           --   0         1         2    0         1         2   2 0         1         2 2
 433 |           --   012345678901234567890123 0123456789012345678901234 01234567890123456789012
 434 |     let str = "This is the first line.\nThis is the second line.\nThis is the third line."
 435 |     wordPosTestCase (0,0)  str "This"
 436 |     wordPosTestCase (0,2)  str "This"
 437 |     wordPosTestCase (0,4)  str "This"
 438 |     wordPosTestCase (0,5)  str "is"
 439 |     wordPosTestCase (0,6)  str "is"
 440 |     wordPosTestCase (0,7)  str "is"
 441 |     wordPosTestCase (0,8)  str "the"
 442 |     wordPosTestCase (0,12) str "first"
 443 |     wordPosTestCase (0,21) str "line."
 444 |     wordPosTestCase (0,30) str "line."
 445 |     wordPosTestCase (1,0)  str "This"
 446 |     wordPosTestCase (1,14) str "second"
 447 |     wordPosTestCase (1,21) str "line."
 448 |     wordPosTestCase (1,30) str "line."
 449 |     wordPosTestCase (2,0)  str "This"
 450 |     wordPosTestCase (2,14) str "third"
 451 |     wordPosTestCase (2,21) str "line."
 452 |     wordPosTestCase (2,30) str "line."
 453 |     wordPosTestCase (3,0)  str ""
 454 |     wordPosTestCase (3,30) str ""
 455 | 
 456 |   do -- Three lines with newline
 457 |           --   0         1         2    0         1         2   2 0         1         2  2
 458 |           --   012345678901234567890123 0123456789012345678901234 012345678901234567890123
 459 |     let str = "This is the first line.\nThis is the second line.\nThis is the third line.\n"
 460 |     wordPosTestCase (0,0)  str "This"
 461 |     wordPosTestCase (0,2)  str "This"
 462 |     wordPosTestCase (0,4)  str "This"
 463 |     wordPosTestCase (0,5)  str "is"
 464 |     wordPosTestCase (0,6)  str "is"
 465 |     wordPosTestCase (0,7)  str "is"
 466 |     wordPosTestCase (0,8)  str "the"
 467 |     wordPosTestCase (0,12) str "first"
 468 |     wordPosTestCase (0,21) str "line."
 469 |     wordPosTestCase (0,30) str "line."
 470 |     wordPosTestCase (1,0)  str "This"
 471 |     wordPosTestCase (1,14) str "second"
 472 |     wordPosTestCase (1,21) str "line."
 473 |     wordPosTestCase (1,30) str "line."
 474 |     wordPosTestCase (2,0)  str "This"
 475 |     wordPosTestCase (2,14) str "third"
 476 |     wordPosTestCase (2,21) str "line."
 477 |     wordPosTestCase (2,30) str "line."
 478 |     wordPosTestCase (3,0)  str ""
 479 |     wordPosTestCase (3,30) str ""
 480 |