Implement multi-line string

[andylokandy]

Implements #1029. For example, the idris2 banner can be rewritten with multi-line string:

Before

banner : String
banner = "     ____    __     _         ___                                           \n" ++
         "    /  _/___/ /____(_)____   |__ \\                                          \n" ++
         "    / // __  / ___/ / ___/   __/ /     Version " ++ showVersion True version ++ "\n" ++
         "  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           \n" ++
         " /___/\\__,_/_/  /_/____/   /____/      Type :? for help                     \n" ++
         "\n" ++
         "Welcome to Idris 2.  Enjoy yourself!"

After

banner : String
banner = #"""
          ____    __     _         ___
         /  _/___/ /____(_)____   |__ \
         / // __  / ___/ / ___/   __/ /     Version \#{ showVersion True version }
       _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
      /___/\__,_/_/  /_/____/   /____/      Type :? for help

     Welcome to Idris 2.  Enjoy yourself!
     """#

Known issue (Update: Solved)

In this PR, multiline string is not compatible with the '#' escape introduced by raw string. This is because the syntax chosen for multiline will be ambiguous if '#' is allowed. For example, #""""""# can be interpreted as a raw string equals to "\"\"\"\"" and also can be interpreted as an multiline string (although it is invalid in this example because it's single-line).

[andrevidela]

Note that the known issue is addressed in #1029 by forcing multi line string delimiters to being different lines and forcing the opening delimiter to have a line break after it.

Edit: now that I've looked at the PR quickly it seems the problem is that single line raw strings and multi line raw string overlapping in their functionality might be the real culprit, in other words, single line raw strings should not span multiple lines. Is that it?

[andylokandy]

@andrevidela My example above might be inaccurate. Let's think this one instead:

#"""

   """#

Is this a raw string or a raw multiline string?

[andylokandy]

single line raw strings should not span multiple lines. Is that it?

Exactly. But, if dis-allowing raw strings to span multiline to de-ambiguous, the semantic of the beginning quote will depend on whether the last quote is in the other line.

[andrevidela]

Ah, I understand, I guess we could afford this kind of lookahead because we only need to read until the end of the line, but that would make the lexing even more complex than it already is.

I Suggest we leave this be for now and make a note of the progress on #1029, I'll add this summary:

When we see #""" (or any number of #) we cannot know until we either reach the end of the line, or we see a "# on the same line if it's an opening delimiter for multiline or single line raw strings.

[andylokandy]

What about this: only lex the multiline begin quote if """ is followed by \n

[andrevidela]

Ah yes that's actually much simpler

[mattpolzin]

I imagine some of the "multiline" strings made up of single line strings (even in this PR) can't be moved to the new syntax in the same version as the syntax is introduced, huh?

I noticed there's no entry in the changelog in this PR, and this change is certainly worth calling out!

[andylokandy]

Replying @mattpolzin

I imagine some of the "multiline" strings made up of single line strings (even in this PR) can't be moved to the new syntax in the same version as the syntax is introduced, huh?

yeah, we have to wait until the next minor release.

I noticed there's no entry in the changelog in this PR, and this change is certainly worth calling out!

Because the raw string, multiline string and interpolated string are highly related, I'd like to write the changelog together in an independent pr.

[andrevidela]

Looks good, error messages could be improved but we can open issues for those. Ideally I would like to also have a nicer error message when starting a multine string with non-whitespace characters """hello instead of "bracket not properly closed" but I think it's out of scope for this PR. Good job!

[andrevidela]

Looks good to me! I've opened #1133 and #1132 to track the issues mentioned in the FIXMEs