From 22a769e6b54d0964125d7eb7033ad8c06f88e6a8 Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Sat, 20 Feb 2021 17:59:06 +0800 Subject: [PATCH] Implement multiline string --- libs/base/Data/String.idr | 2 + src/Core/Core.idr | 3 + src/Idris/Desugar.idr | 59 ++++++++++++++-- src/Idris/Error.idr | 1 + src/Idris/IDEMode/Parser.idr | 7 +- src/Idris/Parser.idr | 37 +++++----- src/Idris/Pretty.idr | 3 +- src/Idris/Syntax.idr | 27 +++++--- src/Libraries/Data/List/Extra.idr | 17 +++++ src/Parser/Lexer/Source.idr | 37 +++++++--- src/Parser/Rule/Source.idr | 16 ++++- src/TTImp/Parser.idr | 2 +- tests/idris2/basic053/StringLiteral.idr | 46 +++++++++++-- tests/idris2/basic053/expected | 26 +++++-- .../perror007/{PError.idr => StrError1.idr} | 0 tests/idris2/perror007/StrError10.idr | 3 + .../perror007/{PError2.idr => StrError2.idr} | 0 .../perror007/{PError3.idr => StrError3.idr} | 0 tests/idris2/perror007/StrError4.idr | 2 + tests/idris2/perror007/StrError5.idr | 4 ++ tests/idris2/perror007/StrError6.idr | 3 + tests/idris2/perror007/StrError7.idr | 2 + tests/idris2/perror007/StrError8.idr | 3 + tests/idris2/perror007/StrError9.idr | 3 + tests/idris2/perror007/expected | 67 +++++++++++++++++-- tests/idris2/perror007/run | 13 +++- 26 files changed, 323 insertions(+), 60 deletions(-) rename tests/idris2/perror007/{PError.idr => StrError1.idr} (100%) create mode 100644 tests/idris2/perror007/StrError10.idr rename tests/idris2/perror007/{PError2.idr => StrError2.idr} (100%) rename tests/idris2/perror007/{PError3.idr => StrError3.idr} (100%) create mode 100644 tests/idris2/perror007/StrError4.idr create mode 100644 tests/idris2/perror007/StrError5.idr create mode 100644 tests/idris2/perror007/StrError6.idr create mode 100644 tests/idris2/perror007/StrError7.idr create mode 100644 tests/idris2/perror007/StrError8.idr create mode 100644 tests/idris2/perror007/StrError9.idr diff --git a/libs/base/Data/String.idr b/libs/base/Data/String.idr index afe9bb366..1f45c5f68 100644 --- a/libs/base/Data/String.idr +++ b/libs/base/Data/String.idr @@ -90,6 +90,7 @@ unwords = pack . unwords' . map unpack ||| ```idris example ||| lines' (unpack "\rA BC\nD\r\nE\n") ||| ``` +export lines' : List Char -> List (List Char) lines' [] = [] lines' s = case break isNL s of @@ -111,6 +112,7 @@ lines s = map pack (lines' (unpack s)) ||| ```idris example ||| unlines' [['l','i','n','e'], ['l','i','n','e','2'], ['l','n','3'], ['D']] ||| ``` +export unlines' : List (List Char) -> List Char unlines' [] = [] unlines' (l::ls) = l ++ '\n' :: unlines' ls diff --git a/src/Core/Core.idr b/src/Core/Core.idr index ab6c9ead5..a14a1370a 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -142,6 +142,7 @@ data Error : Type where InternalError : String -> Error UserError : String -> Error NoForeignCC : FC -> Error + BadMultiline : FC -> String -> Error InType : FC -> Name -> Error -> Error InCon : FC -> Name -> Error -> Error @@ -308,6 +309,7 @@ Show Error where show (UserError str) = "Error: " ++ str show (NoForeignCC fc) = show fc ++ ":The given specifier was not accepted by any available backend." + show (BadMultiline fc str) = "Invalid multiline string: " ++ str show (InType fc n err) = show fc ++ ":When elaborating type of " ++ show n ++ ":\n" ++ @@ -385,6 +387,7 @@ getErrorLoc ForceNeeded = Nothing getErrorLoc (InternalError _) = Nothing getErrorLoc (UserError _) = Nothing getErrorLoc (NoForeignCC loc) = Just loc +getErrorLoc (BadMultiline loc _) = Just loc getErrorLoc (InType _ _ err) = getErrorLoc err getErrorLoc (InCon _ _ err) = getErrorLoc err getErrorLoc (InLHS _ _ err) = getErrorLoc err diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index fcc95cd92..d5fed169b 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -10,6 +10,7 @@ import Core.TT import Core.Unify import Libraries.Data.StringMap +import Libraries.Data.String.Extra import Libraries.Data.ANameMap import Idris.DocString @@ -30,6 +31,9 @@ import Libraries.Utils.String import Control.Monad.State import Data.List +import Data.List.Views +import Data.List1 +import Data.Strings -- Convert high level Idris declarations (PDecl from Idris.Syntax) into -- TTImp, recording any high level syntax info on the way (e.g. infix @@ -77,7 +81,7 @@ toTokList (POp fc opn l r) let op = nameRoot opn case lookup op (infixes syn) of Nothing => - if any isOpChar (unpack op) + if any isOpChar (fastUnpack op) then throw (GenericMsg fc $ "Unknown operator '" ++ op ++ "'") else do rtoks <- toTokList r pure (Expr l :: Op fc opn backtickPrec :: rtoks) @@ -272,6 +276,8 @@ mutual = pure $ IMustUnify fc UserDotted !(desugarB side ps x) desugarB side ps (PImplicit fc) = pure $ Implicit fc True desugarB side ps (PInfer fc) = pure $ Implicit fc False + desugarB side ps (PMultiline fc indent strs) + = addFromString fc !(expandString side ps fc !(trimMultiline fc indent strs)) desugarB side ps (PString fc strs) = addFromString fc !(expandString side ps fc strs) desugarB side ps (PDoBlock fc ns block) = expandDo side ps fc ns block @@ -404,21 +410,66 @@ mutual {auto m : Ref MD Metadata} -> {auto u : Ref UST UState} -> Side -> List Name -> FC -> List PStr -> Core RawImp - expandString side ps fc xs = pure $ case !(traverse toRawImp (filter notEmpty xs)) of + expandString side ps fc xs = pure $ case !(traverse toRawImp (filter notEmpty $ mergeStrLit xs)) of [] => IPrimVal fc (Str "") xs@(_::_) => foldr1 concatStr xs where toRawImp : PStr -> Core RawImp - toRawImp (StrLiteral fc str) = pure $ IPrimVal fc (Str str) + toRawImp (StrLiteral fc _ str) = pure $ IPrimVal fc (Str str) toRawImp (StrInterp fc tm) = desugarB side ps tm + -- merge neighbouring StrLiteral + mergeStrLit : List PStr -> List PStr + mergeStrLit [] = [] + mergeStrLit [x] = [x] + mergeStrLit ((StrLiteral fc isLB str1)::(StrLiteral _ _ str2)::xs) + = (StrLiteral fc isLB (str1 ++ str2)) :: xs + mergeStrLit (x::xs) = x :: mergeStrLit xs + notEmpty : PStr -> Bool - notEmpty (StrLiteral _ str) = str /= "" + notEmpty (StrLiteral _ _ str) = str /= "" notEmpty (StrInterp _ _) = True concatStr : RawImp -> RawImp -> RawImp concatStr a b = IApp (getFC a) (IApp (getFC b) (IVar (getFC b) (UN "++")) a) b + trimMultiline : FC -> Nat -> List PStr -> Core (List PStr) + trimMultiline fc indent xs = do + xs <- trimFirst fc xs + xs <- trimLast fc xs + xs <- traverse (trimLeft indent) xs + pure xs + where + trimFirst : FC -> List PStr -> Core (List PStr) + trimFirst fc [] = throw $ BadMultiline fc "Expected line wrap" + trimFirst _ ((StrInterp fc _)::_) = throw $ BadMultiline fc "Unexpected interpolation in the first line" + trimFirst _ ((StrLiteral fc isLB str)::pstrs) + = if any (not . isSpace) (fastUnpack str) + then throw $ BadMultiline fc "Unexpected character in the first line" + else pure pstrs + + trimLast : FC -> List PStr -> Core (List PStr) + trimLast fc pstrs with (snocList pstrs) + trimLast fc [] | Empty = throw $ BadMultiline fc "Expected line wrap" + trimLast _ (initPStr `snoc` (StrInterp fc _)) | Snoc (StrInterp _ _) initPStr _ + = throw $ BadMultiline fc "Unexpected interpolation in the last line" + trimLast _ (initPStr `snoc` (StrLiteral fc _ str)) | Snoc (StrLiteral _ _ _) initPStr rec + = if any (not . isSpace) (fastUnpack str) + then throw $ BadMultiline fc "Unexpected character in the last line" + else case rec of + Snoc (StrLiteral fc isLB str) initPStr' _ => + -- remove the last line wrap + pure $ initPStr' `snoc` (StrLiteral fc isLB (dropLast 1 str)) + _ => pure initPStr + + trimLeft : Nat -> PStr -> Core PStr + trimLeft indent (StrLiteral fc True line) + = let (trimed, rest) = splitAt indent (fastUnpack line) in + if any (not . isSpace) trimed + then throw $ BadMultiline fc "Indentation not enough" + else pure $ StrLiteral fc True (fastPack rest) + trimLeft indent x = pure x + expandDo : {auto s : Ref Syn SyntaxInfo} -> {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 3d6f4e20f..71d10e502 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -426,6 +426,7 @@ perror (NoForeignCC fc) = do , reflow "Some backends have additional specifier rules, refer to their documentation." ] <+> line <+> !(ploc fc) pure res +perror (BadMultiline fc str) = pure $ errorDesc (reflow "While processing multiline string" <+> dot <++> pretty str <+> dot) <+> line <+> !(ploc fc) perror (InType fc n err) = pure $ hsep [ errorDesc (reflow "While processing type of" <++> code (pretty !(prettyName n))) <+> dot diff --git a/src/Idris/IDEMode/Parser.idr b/src/Idris/IDEMode/Parser.idr index 00da8fd5e..3fe89e858 100644 --- a/src/Idris/IDEMode/Parser.idr +++ b/src/Idris/IDEMode/Parser.idr @@ -34,7 +34,12 @@ ideTokens : Tokenizer Token ideTokens = match (choice $ exact <$> symbols) Symbol <|> match digits (\x => IntegerLit (cast x)) - <|> compose (is '"') (const StringBegin) (const ()) (const stringTokens) (const $ is '"') (const StringEnd) + <|> compose (is '"') + (const $ StringBegin False) + (const ()) + (const stringTokens) + (const $ is '"') + (const StringEnd) <|> match identAllowDashes Ident <|> match space (const Comment) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 8d7a1404e..b5ecfc7a1 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -392,8 +392,7 @@ mutual <|> binder fname indents <|> rewrite_ fname indents <|> record_ fname indents - <|> do b <- bounds (interpStr pdef fname indents) - pure (PString (boundToFC fname b) b.val) + <|> interpStr pdef fname indents <|> do b <- bounds (symbol ".(" *> commit *> expr pdef fname indents <* symbol ")") pure (PDotted (boundToFC fname b) b.val) <|> do b <- bounds (symbol "`(" *> expr pdef fname indents <* symbol ")") @@ -777,22 +776,30 @@ mutual expr = typeExpr export - interpStr : ParseOpts -> FileName -> IndentInfo -> Rule (List PStr) - interpStr q fname idents = do - strBegin - commit - xs <- many $ bounds $ interpBlock <||> strLit - strEnd - pure $ toPString <$> xs + interpStr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm + interpStr q fname idents + = do b <- bounds $ do multi <- strBegin + commit + xs <- many $ bounds $ interpBlock <||> strLitLines + endloc <- location + strEnd + pure (multi, endloc, concatMap toPStr xs) + the (SourceEmptyRule PTerm) $ + case b.val of + (False, _, xs) => pure $ PString (boundToFC fname b) xs + (True, (_, col), xs) => pure $ PMultiline (boundToFC fname b) (fromInteger $ cast col) xs where interpBlock : Rule PTerm interpBlock = interpBegin *> (mustWork $ expr q fname idents) <* interpEnd - toPString : (WithBounds $ Either PTerm String) -> PStr - toPString x - = case x.val of - Right s => StrLiteral (boundToFC fname x) s - Left tm => StrInterp (boundToFC fname x) tm + toPStr : (WithBounds $ Either PTerm (List1 String)) -> List PStr + toPStr x = case x.val of + -- The lines after '\n' is considered line begin (to be trimed in multiline). + -- Note that the first item of the result of splitting by '\n' is not line begin. + -- FIXME: calculate the precise FC so as to improve error report for invalid indentation. + Right (str ::: strs) => (StrLiteral (boundToFC fname x) False str) :: + (StrLiteral (boundToFC fname x) True <$> strs) + Left tm => [StrInterp (boundToFC fname x) tm] visOption : Rule Visibility visOption @@ -1185,7 +1192,7 @@ visOpt fname pure (Right opt) getVisibility : Maybe Visibility -> List (Either Visibility PFnOpt) -> - SourceEmptyRule Visibility + SourceEmptyRule Visibility getVisibility Nothing [] = pure Private getVisibility (Just vis) [] = pure vis getVisibility Nothing (Left x :: xs) = getVisibility (Just x) xs diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index 8ab0e95ed..dc5a94108 100644 --- a/src/Idris/Pretty.idr +++ b/src/Idris/Pretty.idr @@ -122,7 +122,7 @@ mutual prettyTerm lhs <++> impossible_ prettyString : PStr -> Doc IdrisAnn - prettyString (StrLiteral _ str) = pretty str + prettyString (StrLiteral _ _ str) = pretty str prettyString (StrInterp _ tm) = prettyTerm tm prettyDo : PDo -> Doc IdrisAnn @@ -282,6 +282,7 @@ mutual go d (PEq fc l r) = parenthesise (d > appPrec) $ go startPrec l <++> equals <++> go startPrec r go d (PBracketed _ tm) = parens (go startPrec tm) go d (PString _ xs) = parenthesise (d > appPrec) $ hsep $ punctuate "++" (prettyString <$> xs) + go d (PMultiline _ indent xs) = "multiline" <++> (parenthesise (d > appPrec) $ hsep $ punctuate "++" (prettyString <$> xs)) go d (PDoBlock _ ns ds) = parenthesise (d > appPrec) $ group $ align $ hang 2 $ do_ <++> (vsep $ punctuate semi (prettyDo <$> ds)) go d (PBang _ tm) = "!" <+> go d tm go d (PIdiom _ tm) = enclose (pretty "[|") (pretty "|]") (go startPrec tm) diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 6a72d4099..da5c52ca0 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -82,6 +82,7 @@ mutual -- Syntactic sugar PString : FC -> List PStr -> PTerm + PMultiline : FC -> (indent : Nat) -> List PStr -> PTerm PDoBlock : FC -> Maybe Namespace -> List PDo -> PTerm PBang : FC -> PTerm -> PTerm PIdiom : FC -> PTerm -> PTerm @@ -143,6 +144,7 @@ mutual getPTermLoc (PEq fc _ _) = fc getPTermLoc (PBracketed fc _) = fc getPTermLoc (PString fc _) = fc + getPTermLoc (PMultiline fc _ _) = fc getPTermLoc (PDoBlock fc _ _) = fc getPTermLoc (PBang fc _) = fc getPTermLoc (PIdiom fc _) = fc @@ -177,7 +179,9 @@ mutual public export data PStr : Type where - StrLiteral : FC -> String -> PStr + ||| String literals that are split after visual line wrap (not the escaped '\n'). + ||| @isLineBegin indicates whether the previous item is ended by a line wrap. + StrLiteral : FC -> (isLineBegin : Bool) -> String -> PStr StrInterp : FC -> PTerm -> PStr export @@ -496,9 +500,10 @@ mutual showDo (DoRewrite _ rule) = "rewrite " ++ show rule - showString : PStr -> String - showString (StrLiteral _ str) = show str - showString (StrInterp _ tm) = show tm + export + showPStr : PStr -> String + showPStr (StrLiteral _ _ str) = show str + showPStr (StrInterp _ tm) = show tm showUpdate : PFieldUpdate -> String showUpdate (PSetField p v) = showSep "." p ++ " = " ++ show v @@ -587,7 +592,8 @@ mutual showPrec d (PSectionR _ x op) = "(" ++ showPrec d x ++ " " ++ showPrec d op ++ ")" showPrec d (PEq fc l r) = showPrec d l ++ " = " ++ showPrec d r showPrec d (PBracketed _ tm) = "(" ++ showPrec d tm ++ ")" - showPrec d (PString _ xs) = join " ++ " $ showString <$> xs + showPrec d (PString _ xs) = join " ++ " $ showPStr <$> xs + showPrec d (PMultiline _ indent xs) = "multiline (" ++ (join " ++ " $ showPStr <$> xs) ++ ")" showPrec d (PDoBlock _ ns ds) = "do " ++ showSep " ; " (map showDo ds) showPrec d (PBang _ tm) = "!" ++ showPrec d tm @@ -915,6 +921,9 @@ mapPTermM f = goPTerm where goPTerm (PString fc xs) = PString fc <$> goPStrings xs >>= f + goPTerm (PMultiline fc x ys) = + PMultiline fc x <$> goPStrings ys + >>= f goPTerm (PDoBlock fc ns xs) = PDoBlock fc ns <$> goPDos xs >>= f @@ -975,9 +984,9 @@ mapPTermM f = goPTerm where goPFieldUpdate (PSetField p t) = PSetField p <$> goPTerm t goPFieldUpdate (PSetFieldApp p t) = PSetFieldApp p <$> goPTerm t - goPString : PStr -> Core PStr - goPString (StrInterp fc t) = StrInterp fc <$> goPTerm t - goPString x = pure x + goPStr : PStr -> Core PStr + goPStr (StrInterp fc t) = StrInterp fc <$> goPTerm t + goPStr x = pure x goPDo : PDo -> Core PDo goPDo (DoExp fc t) = DoExp fc <$> goPTerm t @@ -1105,7 +1114,7 @@ mapPTermM f = goPTerm where goPStrings : List PStr -> Core (List PStr) goPStrings [] = pure [] - goPStrings (str :: strs) = (::) <$> goPString str <*> goPStrings strs + goPStrings (str :: strs) = (::) <$> goPStr str <*> goPStrings strs goPDos : List PDo -> Core (List PDo) goPDos [] = pure [] diff --git a/src/Libraries/Data/List/Extra.idr b/src/Libraries/Data/List/Extra.idr index fbdf7ac42..49ed7fc85 100644 --- a/src/Libraries/Data/List/Extra.idr +++ b/src/Libraries/Data/List/Extra.idr @@ -1,5 +1,7 @@ module Libraries.Data.List.Extra +import Data.List1 + %default total ||| Fetches the element at a given position. @@ -17,3 +19,18 @@ firstBy p (x :: xs) = case p x of Nothing => firstBy p xs Just win => pure win + +export +breakAfter : (a -> Bool) -> List a -> (List a, List a) +breakAfter p [] = ([], []) +breakAfter p (x::xs) + = if p x + then ([x], xs) + else let (ys, zs) = breakAfter p xs in (x::ys, zs) + +export +splitAfter : (a -> Bool) -> List a -> List1 (List a) +splitAfter p xs + = case breakAfter p xs of + (chunk, []) => singleton chunk + (chunk, rest@(_::_)) => cons chunk (splitAfter p (assert_smaller xs rest)) diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 4261928fb..79be280e6 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -27,7 +27,7 @@ data Token | DoubleLit Double | IntegerLit Integer -- String - | StringBegin + | StringBegin Bool -- Whether is multiline string | StringEnd | InterpBegin | InterpEnd @@ -55,7 +55,8 @@ Show Token where show (DoubleLit x) = "double " ++ show x show (IntegerLit x) = "literal " ++ show x -- String - show StringBegin = "string begin" + show (StringBegin True) = "string begin" + show (StringBegin False) = "multiline string begin" show StringEnd = "string end" show InterpBegin = "string interp begin" show InterpEnd = "string interp end" @@ -83,7 +84,8 @@ Pretty Token where pretty (DoubleLit x) = pretty "double" <++> pretty x pretty (IntegerLit x) = pretty "literal" <++> pretty x -- String - pretty StringBegin = reflow "string begin" + pretty (StringBegin True) = reflow "string begin" + pretty (StringBegin False) = reflow "multiline string begin" pretty StringEnd = reflow "string end" pretty InterpBegin = reflow "string interp begin" pretty InterpEnd = reflow "string interp end" @@ -271,14 +273,14 @@ fromOctLit str -- ^-- can't happen if the literal lexed correctly mutual - stringTokens : Nat -> Tokenizer Token - stringTokens hashtag + stringTokens : Bool -> Nat -> Tokenizer Token + stringTokens multi hashtag = let escapeChars = "\\" ++ replicate hashtag '#' interpStart = escapeChars ++ "{" escapeLexer = escape (exact escapeChars) any - stringLexer = non $ exact (stringEnd hashtag) + charLexer = non $ exact (if multi then "\"\"\"" else stringEnd hashtag) in - match (someUntil (exact interpStart) (escapeLexer <|> stringLexer)) (\x => StringLit hashtag x) + match (someUntil (exact interpStart) (escapeLexer <|> charLexer)) (\x => StringLit hashtag x) <|> compose (exact interpStart) (const InterpBegin) (const ()) (\_ => rawTokens) (const $ is '}') (const InterpEnd) rawTokens : Tokenizer Token @@ -288,14 +290,30 @@ mutual <|> match docComment (DocComment . drop 3) <|> match cgDirective mkDirective <|> match holeIdent (\x => HoleIdent (assert_total (strTail x))) - <|> compose (choice $ exact <$> groupSymbols) Symbol id (\_ => rawTokens) (exact . groupClose) Symbol + <|> compose (choice $ exact <$> groupSymbols) + Symbol + id + (\_ => rawTokens) + (exact . groupClose) + Symbol <|> match (choice $ exact <$> symbols) Symbol <|> match doubleLit (\x => DoubleLit (cast x)) <|> match binLit (\x => IntegerLit (fromBinLit x)) <|> match hexLit (\x => IntegerLit (fromHexLit x)) <|> match octLit (\x => IntegerLit (fromOctLit x)) <|> match digits (\x => IntegerLit (cast x)) - <|> compose stringBegin (const StringBegin) countHashtag stringTokens (exact . stringEnd) (const StringEnd) + <|> compose (exact "\"\"\"") + (const $ StringBegin True) + (const ()) + (const $ stringTokens True 0) + (const $ exact "\"\"\"") + (const StringEnd) + <|> compose stringBegin + (const $ StringBegin False) + countHashtag + (stringTokens False) + (exact . stringEnd) + (const StringEnd) <|> match charLit (\x => CharLit (stripQuotes x)) <|> match dotIdent (\x => DotIdent (assert_total $ strTail x)) <|> match namespacedIdent parseNamespace @@ -312,7 +330,6 @@ mutual parseNamespace ns = case mkNamespacedIdent ns of (Nothing, ident) => parseIdent ident (Just ns, n) => DotSepIdent ns n - countHashtag : String -> Nat countHashtag = count (== '#') . unpack diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr index 0cd906590..5926726cc 100644 --- a/src/Parser/Rule/Source.idr +++ b/src/Parser/Rule/Source.idr @@ -7,6 +7,7 @@ import public Parser.Support import Core.TT import Data.List1 import Data.Strings +import Libraries.Data.List.Extra %default total @@ -84,11 +85,22 @@ strLit StringLit n s => escape n s _ => Nothing) +||| String literal split by line wrap (not striped) before escaping the string. export -strBegin : Rule () +strLitLines : Rule (List1 String) +strLitLines + = terminal "Expected string literal" + (\x => case x.val of + StringLit n s => traverse (escape n . fastPack) + (splitAfter isNL (fastUnpack s)) + _ => Nothing) + +||| String literal begin quote. The bool indicates whether the it is multiline string. +export +strBegin : Rule Bool strBegin = terminal "Expected string begin" (\x => case x.val of - StringBegin => Just () + StringBegin multi => Just multi _ => Nothing) export diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 9eaaa3e9e..4413a506e 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -123,7 +123,7 @@ visOpt pure (Right opt) getVisibility : Maybe Visibility -> List (Either Visibility FnOpt) -> - SourceEmptyRule Visibility + SourceEmptyRule Visibility getVisibility Nothing [] = pure Private getVisibility (Just vis) [] = pure vis getVisibility Nothing (Left x :: xs) = getVisibility (Just x) xs diff --git a/tests/idris2/basic053/StringLiteral.idr b/tests/idris2/basic053/StringLiteral.idr index 230775676..2e4007e3a 100644 --- a/tests/idris2/basic053/StringLiteral.idr +++ b/tests/idris2/basic053/StringLiteral.idr @@ -33,6 +33,38 @@ interp3 = "Just 1 + Just 2 = \{ Just (a + b) }" +multi1 : String +multi1 = """ + [project] + name: "project" + version: "0.1.0" + [deps] + "semver" = 0.2 + """ + +multi2 : String +multi2 = """ + a + b\n + c + """ + +multi3 : String +multi3 = """ + \{"sticking"} \{"together"}\{ + ""}\{""" +! + +"""} + """ + +multi4 : String +multi4 = """ + A very very very very very \n + very very very\n\n very very \n + very long string. + """ + test : IO () test = do @@ -41,12 +73,18 @@ test = putStrLn withIndent putStrLn withEscape putStrLn withEscapeNoWrap + putStrLn ##" +name: #"foo" +version: "bar" +bzs: \#\'a\n\t\\'"## putStrLn interp putStrLn interp2 putStrLn interp3 let idris = "Idris" putStrLn "Hello \{idris ++ show 2}!" - putStrLn ##" -name: #"foo" -version: "bar" -bzs: \#\'a\n\t\\'"## + putStrLn multi1 + putStrLn multi2 + putStrLn multi3 + putStrLn multi4 + putStrLn """ + """ diff --git a/tests/idris2/basic053/expected b/tests/idris2/basic053/expected index 86887f995..80ddc6ac4 100644 --- a/tests/idris2/basic053/expected +++ b/tests/idris2/basic053/expected @@ -7,11 +7,29 @@ foo \bar "foo" \bar -foo bar -hello world. -Just 1 + Just 2 = Just 3 -Hello Idris2! name: #"foo" version: "bar" bzs: \#\'a\n\t\\' +foo bar +hello world. +Just 1 + Just 2 = Just 3 +Hello Idris2! +[project] +name: "project" +version: "0.1.0" +[deps] +"semver" = 0.2 +a + b + + c +sticking together! +A very very very very very + +very very very + + very very + +very long string. + diff --git a/tests/idris2/perror007/PError.idr b/tests/idris2/perror007/StrError1.idr similarity index 100% rename from tests/idris2/perror007/PError.idr rename to tests/idris2/perror007/StrError1.idr diff --git a/tests/idris2/perror007/StrError10.idr b/tests/idris2/perror007/StrError10.idr new file mode 100644 index 000000000..2088eda66 --- /dev/null +++ b/tests/idris2/perror007/StrError10.idr @@ -0,0 +1,3 @@ +foo : String +foo = """ +a""" diff --git a/tests/idris2/perror007/PError2.idr b/tests/idris2/perror007/StrError2.idr similarity index 100% rename from tests/idris2/perror007/PError2.idr rename to tests/idris2/perror007/StrError2.idr diff --git a/tests/idris2/perror007/PError3.idr b/tests/idris2/perror007/StrError3.idr similarity index 100% rename from tests/idris2/perror007/PError3.idr rename to tests/idris2/perror007/StrError3.idr diff --git a/tests/idris2/perror007/StrError4.idr b/tests/idris2/perror007/StrError4.idr new file mode 100644 index 000000000..1a2c743c8 --- /dev/null +++ b/tests/idris2/perror007/StrError4.idr @@ -0,0 +1,2 @@ +foo : String +foo = """""" diff --git a/tests/idris2/perror007/StrError5.idr b/tests/idris2/perror007/StrError5.idr new file mode 100644 index 000000000..578c456f0 --- /dev/null +++ b/tests/idris2/perror007/StrError5.idr @@ -0,0 +1,4 @@ +foo : String +foo = """ + a + """ diff --git a/tests/idris2/perror007/StrError6.idr b/tests/idris2/perror007/StrError6.idr new file mode 100644 index 000000000..22038516a --- /dev/null +++ b/tests/idris2/perror007/StrError6.idr @@ -0,0 +1,3 @@ +foo : String +foo = """a +""" diff --git a/tests/idris2/perror007/StrError7.idr b/tests/idris2/perror007/StrError7.idr new file mode 100644 index 000000000..a38fab5cd --- /dev/null +++ b/tests/idris2/perror007/StrError7.idr @@ -0,0 +1,2 @@ +foo : String +foo = """a""" diff --git a/tests/idris2/perror007/StrError8.idr b/tests/idris2/perror007/StrError8.idr new file mode 100644 index 000000000..c5ed2edc4 --- /dev/null +++ b/tests/idris2/perror007/StrError8.idr @@ -0,0 +1,3 @@ +foo : String +foo = """\{"hello"} +""" diff --git a/tests/idris2/perror007/StrError9.idr b/tests/idris2/perror007/StrError9.idr new file mode 100644 index 000000000..da8649d62 --- /dev/null +++ b/tests/idris2/perror007/StrError9.idr @@ -0,0 +1,3 @@ +foo : String +foo = """ +\{"hello"}""" diff --git a/tests/idris2/perror007/expected b/tests/idris2/perror007/expected index d6f9f9960..658b54869 100644 --- a/tests/idris2/perror007/expected +++ b/tests/idris2/perror007/expected @@ -1,24 +1,79 @@ -1/1: Building PError (PError.idr) +1/1: Building StrError1 (StrError1.idr) Error: Expected 'case', 'if', 'do', application or operator expression. -PError.idr:2:24--2:25 +StrError1.idr:2:24--2:25 1 | foo : String 2 | foo = "empty interp: \{}" ^ -1/1: Building PError2 (PError2.idr) +1/1: Building StrError2 (StrError2.idr) Error: Expected 'case', 'if', 'do', application or operator expression. -PError2.idr:2:19--2:20 +StrError2.idr:2:19--2:20 1 | foo : String 2 | foo = "nested: \{ " \{ 1 + } " }" ^ -1/1: Building PError3 (PError3.idr) +1/1: Building StrError3 (StrError3.idr) Error: Expected 'case', 'if', 'do', application or operator expression. -PError3.idr:2:7--2:8 +StrError3.idr:2:7--2:8 1 | foo : String 2 | foo = "incomplete: \{ a <+> }" ^ +1/1: Building StrError4 (StrError4.idr) +Error: While processing multiline string. Expected line wrap. + +StrError4.idr:2:7--2:13 + 1 | foo : String + 2 | foo = """""" + ^^^^^^ + +1/1: Building StrError5 (StrError5.idr) +Error: While processing multiline string. Indentation not enough. + +StrError5.idr:2:10--4:5 + 2 | foo = """ + 3 | a + 4 | """ + +1/1: Building StrError6 (StrError6.idr) +Error: While processing multiline string. Unexpected character in the first line. + +StrError6.idr:2:10--3:1 + 2 | foo = """a + 3 | """ + +1/1: Building StrError7 (StrError7.idr) +Error: While processing multiline string. Unexpected character in the first line. + +StrError7.idr:2:10--2:11 + 1 | foo : String + 2 | foo = """a""" + ^ + +1/1: Building StrError8 (StrError8.idr) +Error: While processing multiline string. Unexpected interpolation in the first line. + +StrError8.idr:2:10--2:20 + 1 | foo : String + 2 | foo = """\{"hello"} + ^^^^^^^^^^ + +1/1: Building StrError9 (StrError9.idr) +Error: While processing multiline string. Unexpected interpolation in the last line. + +StrError9.idr:3:1--3:11 + 1 | foo : String + 2 | foo = """ + 3 | \{"hello"}""" + ^^^^^^^^^^ + +1/1: Building StrError10 (StrError10.idr) +Error: While processing multiline string. Unexpected character in the last line. + +StrError10.idr:2:10--3:2 + 2 | foo = """ + 3 | a""" + diff --git a/tests/idris2/perror007/run b/tests/idris2/perror007/run index e9d6937ab..fab9a8811 100755 --- a/tests/idris2/perror007/run +++ b/tests/idris2/perror007/run @@ -1,5 +1,12 @@ -$1 --no-color --console-width 0 --check PError.idr || true -$1 --no-color --console-width 0 --check PError2.idr || true -$1 --no-color --console-width 0 --check PError3.idr || true +$1 --no-color --console-width 0 --check StrError1.idr || true +$1 --no-color --console-width 0 --check StrError2.idr || true +$1 --no-color --console-width 0 --check StrError3.idr || true +$1 --no-color --console-width 0 --check StrError4.idr || true +$1 --no-color --console-width 0 --check StrError5.idr || true +$1 --no-color --console-width 0 --check StrError6.idr || true +$1 --no-color --console-width 0 --check StrError7.idr || true +$1 --no-color --console-width 0 --check StrError8.idr || true +$1 --no-color --console-width 0 --check StrError9.idr || true +$1 --no-color --console-width 0 --check StrError10.idr || true rm -rf build