git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4200 from msmorgan/verbatim-string-trailing-quotes

Support trailing quotes in verbatim string literals

commit72c233d22c2816f15fd2af2f5854b1c9b317e69e authorAhmad Salim Al-Sibahi <asal@itu.dk> dateFri 17 Nov 2017, 19:12 (9 years ago) parent21ab1965fd758c
4 files changed+24−12
compare with master
unifiedsplit
CHANGELOG.md+3 src/Idris/Parser/Expr.hs+3−2 test/primitives003/expected+4 test/primitives003/test038.idr+14−10
CHANGELOG.md+3
@@ -23,6 +23,9 @@
2323 uninhabited (MkDPair n prf) = absurd prf
2424 ```
2525 It is possible to use `using implementation uninhabltb` to add the implementation to the automated resolution, but if it fails to find the instance due to non-injectivity, one must pass it explicitly to target function, i.e. `absurd @{uninhabltb}`.
26++ Verbatim strings now support trailing quote characters. All quote characters
27+ until the final three are considered part of the string. Now a string such as
28+ `""""hello""""` will parse, and is equivalent to `"\"hello\""`.
2629
2730## Library Updates
2831
src/Idris/Parser/Expr.hs+3−2
@@ -1461,7 +1461,7 @@ constant = P.choice [ do fc <- reservedFC name; return (ty, fc)
14611461
14621462@
14631463VerbatimString_t ::=
1464− '\"\"\"' ~'\"\"\"' '\"\"\"'
1464+ '\"\"\"' ~'\"\"\"' '\"'* '\"\"\"'
14651465;
14661466@
14671467 -}
@@ -1469,8 +1469,9 @@ verbatimStringLiteral :: IdrisParser (String, FC)
14691469verbatimStringLiteral = token $ do (FC f start _) <- getFC
14701470 P.try $ string "\"\"\""
14711471 str <- P.manyTill P.anyChar $ P.try (string "\"\"\"")
1472+ moreQuotes <- P.many $ P.char '"'
14721473 (FC _ _ end) <- getFC
1473− return (str, FC f start end)
1474+ return (str ++ moreQuotes, FC f start end)
14741475
14751476{- | Parses a static modifier
14761477
test/primitives003/expected+4
@@ -5,6 +5,10 @@ False
55True
66False
77True
8+True
9+True
10+True
11+True
812False
913True
1014False
test/primitives003/test038.idr+14−10
@@ -1,4 +1,4 @@
1−module Main
1+module Main
22
33import Data.Vect
44import Data.Fin
@@ -17,18 +17,22 @@ main = do
1717 putStrLn . show $ test "hello" "world"
1818 putStrLn . show $ test (the Char '\0') (the Char '\0')
1919 putStrLn . show $ test (the Char '\1') (the Char '\2')
20+ putStrLn . show $ test """""" ""
21+ putStrLn . show $ test """"hello"""" "\"hello\""
22+ putStrLn . show $ test """""hello""""" "\"\"hello\"\""
23+ putStrLn . show $ test """""""""" "\"\"\"\""
2024-- Non-primitives
2125 -- Vect
22− putStrLn . show $
26+ putStrLn . show $
2327 test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,3])
24− putStrLn . show $
28+ putStrLn . show $
2529 test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,4])
2630 -- List
27− putStrLn . show $
31+ putStrLn . show $
2832 test (the (List Int) [1,2,3]) (the (List Int) [1,2,3])
29− putStrLn . show $
33+ putStrLn . show $
3034 test (the (List Int) [1,2,3]) (the (List Int) [1,2])
31− putStrLn . show $
35+ putStrLn . show $
3236 test (the (List Int) [1,2,3]) (the (List Int) [1,2,4])
3337 -- Tuple
3438 putStrLn . show $
@@ -45,16 +49,16 @@ main = do
4549 putStrLn . show $ test (Just "hello") (Just "world")
4650 putStrLn . show $ test (Just "hello") Nothing
4751 -- Either
48− putStrLn . show $ test (the (Either String Bool) (Left "hello"))
52+ putStrLn . show $ test (the (Either String Bool) (Left "hello"))
4953 (the (Either String Bool) (Left "hello"))
50− putStrLn . show $ test (the (Either String Bool) (Left "hello"))
54+ putStrLn . show $ test (the (Either String Bool) (Left "hello"))
5155 (the (Either String Bool) (Left "world"))
5256 putStrLn . show $ test (Left "hello") (Right "world")
5357 putStrLn . show $ test (Left "hello") (Right False)
5458 -- Fin
55− putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
59+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
5660 (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
57− putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
61+ putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
5862 (the (Fin (S (S (S (Z))))) (FS (FZ)))
5963 -- Nat
6064 putStrLn . show $ test (S (S (S Z))) (S (S (S Z)))