git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4200 from msmorgan/verbatim-string-trailing-quotes
72c233dAhmad Salim Al-Sibahi
CHANGELOG.md+3
compare with master
unifiedsplit
@@ -23,6 +23,9 @@
23 uninhabited (MkDPair n prf) = absurd prf
23 uninhabited (MkDPair n prf) = absurd prf
24 ```
24 ```
25 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}`.
25 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\""`.
26
29
27## Library Updates
30## Library Updates
28
31
src/Idris/Parser/Expr.hs+3−2
@@ -1461,7 +1461,7 @@ constant = P.choice [ do fc <- reservedFC name; return (ty, fc)
1461
1461
1462@
1462@
1463VerbatimString_t ::=
1463VerbatimString_t ::=
1464− '\"\"\"' ~'\"\"\"' '\"\"\"'
1464+ '\"\"\"' ~'\"\"\"' '\"'* '\"\"\"'
1465;
1465;
1466@
1466@
1467 -}
1467 -}
@@ -1469,8 +1469,9 @@ verbatimStringLiteral :: IdrisParser (String, FC)
1469verbatimStringLiteral = token $ do (FC f start _) <- getFC
1469verbatimStringLiteral = token $ do (FC f start _) <- getFC
1470 P.try $ string "\"\"\""
1470 P.try $ string "\"\"\""
1471 str <- P.manyTill P.anyChar $ P.try (string "\"\"\"")
1471 str <- P.manyTill P.anyChar $ P.try (string "\"\"\"")
1472+ moreQuotes <- P.many $ P.char '"'
1472 (FC _ _ end) <- getFC
1473 (FC _ _ end) <- getFC
1473− return (str, FC f start end)
1474+ return (str ++ moreQuotes, FC f start end)
1474
1475
1475{- | Parses a static modifier
1476{- | Parses a static modifier
1476
1477
test/primitives003/expected+4
@@ -5,6 +5,10 @@ False
5True
5True
6False
6False
7True
7True
8+True
9+True
10+True
11+True
8False
12False
9True
13True
10False
14False
test/primitives003/test038.idr+14−10
@@ -1,4 +1,4 @@
1−module Main
1+module Main
2
2
3import Data.Vect
3import Data.Vect
4import Data.Fin
4import Data.Fin
@@ -17,18 +17,22 @@ main = do
17 putStrLn . show $ test "hello" "world"
17 putStrLn . show $ test "hello" "world"
18 putStrLn . show $ test (the Char '\0') (the Char '\0')
18 putStrLn . show $ test (the Char '\0') (the Char '\0')
19 putStrLn . show $ test (the Char '\1') (the Char '\2')
19 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 """""""""" "\"\"\"\""
20-- Non-primitives
24-- Non-primitives
21 -- Vect
25 -- Vect
22− putStrLn . show $
26+ putStrLn . show $
23 test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,3])
27 test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,3])
24− putStrLn . show $
28+ putStrLn . show $
25 test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,4])
29 test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,4])
26 -- List
30 -- List
27− putStrLn . show $
31+ putStrLn . show $
28 test (the (List Int) [1,2,3]) (the (List Int) [1,2,3])
32 test (the (List Int) [1,2,3]) (the (List Int) [1,2,3])
29− putStrLn . show $
33+ putStrLn . show $
30 test (the (List Int) [1,2,3]) (the (List Int) [1,2])
34 test (the (List Int) [1,2,3]) (the (List Int) [1,2])
31− putStrLn . show $
35+ putStrLn . show $
32 test (the (List Int) [1,2,3]) (the (List Int) [1,2,4])
36 test (the (List Int) [1,2,3]) (the (List Int) [1,2,4])
33 -- Tuple
37 -- Tuple
34 putStrLn . show $
38 putStrLn . show $
@@ -45,16 +49,16 @@ main = do
45 putStrLn . show $ test (Just "hello") (Just "world")
49 putStrLn . show $ test (Just "hello") (Just "world")
46 putStrLn . show $ test (Just "hello") Nothing
50 putStrLn . show $ test (Just "hello") Nothing
47 -- Either
51 -- Either
48− putStrLn . show $ test (the (Either String Bool) (Left "hello"))
52+ putStrLn . show $ test (the (Either String Bool) (Left "hello"))
49 (the (Either String Bool) (Left "hello"))
53 (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"))
51 (the (Either String Bool) (Left "world"))
55 (the (Either String Bool) (Left "world"))
52 putStrLn . show $ test (Left "hello") (Right "world")
56 putStrLn . show $ test (Left "hello") (Right "world")
53 putStrLn . show $ test (Left "hello") (Right False)
57 putStrLn . show $ test (Left "hello") (Right False)
54 -- Fin
58 -- 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))))
56 (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
60 (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))))
58 (the (Fin (S (S (S (Z))))) (FS (FZ)))
62 (the (Fin (S (S (S (Z))))) (FS (FZ)))
59 -- Nat
63 -- Nat
60 putStrLn . show $ test (S (S (S Z))) (S (S (S Z)))
64 putStrLn . show $ test (S (S (S Z))) (S (S (S Z)))