From 22a769e6b54d0964125d7eb7033ad8c06f88e6a8 Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Sat, 20 Feb 2021 17:59:06 +0800 Subject: [PATCH 01/11] 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 | 24 ++++++- .../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, 322 insertions(+), 59 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 afe9bb3661..1f45c5f688 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 ab6c9ead56..a14a1370a5 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 fcc95cd926..d5fed169ba 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 3d6f4e20f1..71d10e502d 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 00da8fd5e5..3fe89e858f 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 8d7a1404e4..b5ecfc7a1c 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 8ab0e95ed6..dc5a94108c 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 6a72d4099a..da5c52ca03 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 fbdf7ac42d..49ed7fc85d 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 4261928fbc..79be280e61 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 0cd906590d..5926726cc5 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 9eaaa3e9e7..4413a506e2 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 2307756760..2e4007e3a8 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 86887f9958..80ddc6ac44 100644 --- a/tests/idris2/basic053/expected +++ b/tests/idris2/basic053/expected @@ -7,11 +7,29 @@ foo \bar "foo" \bar + +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. -name: #"foo" -version: "bar" -bzs: \#\'a\n\t\\' 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 0000000000..2088eda66f --- /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 0000000000..1a2c743c8f --- /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 0000000000..578c456f0e --- /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 0000000000..22038516a9 --- /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 0000000000..a38fab5cdb --- /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 0000000000..c5ed2edc45 --- /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 0000000000..da8649d62e --- /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 d6f9f99601..658b54869d 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 e9d6937ab5..fab9a88116 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 From 07eb6fda47149b533d77a1ae6ac41b4bf85f3249 Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Sun, 21 Feb 2021 03:11:01 +0800 Subject: [PATCH 02/11] Allow hashtag escape for multi-line string --- src/Idris/Desugar.idr | 35 +++++++----- src/Idris/Error.idr | 2 +- src/Idris/Parser.idr | 3 +- src/Parser/Lexer/Source.idr | 17 ++++-- tests/idris2/basic053/StringLiteral.idr | 76 +++++++++---------------- tests/idris2/basic053/expected | 32 ++++------- tests/idris2/perror007/StrError11.idr | 3 + tests/idris2/perror007/expected | 38 ++++++++----- tests/idris2/perror007/run | 1 + 9 files changed, 101 insertions(+), 106 deletions(-) create mode 100644 tests/idris2/perror007/StrError11.idr diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index d5fed169ba..406f000f12 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -278,7 +278,8 @@ mutual 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 (PString fc strs) + = addFromString fc !(expandString side ps fc !(checkSingleLine strs)) desugarB side ps (PDoBlock fc ns block) = expandDo side ps fc ns block desugarB side ps (PBang fc term) @@ -433,34 +434,42 @@ mutual concatStr : RawImp -> RawImp -> RawImp concatStr a b = IApp (getFC a) (IApp (getFC b) (IVar (getFC b) (UN "++")) a) b + checkSingleLine : List PStr -> Core (List PStr) + checkSingleLine [] = pure [] + checkSingleLine ((StrLiteral fc True _)::xs) + = throw $ BadMultiline fc "Multi-line string is expected to begin with \"\"\"" + checkSingleLine (x::xs) = pure $ x :: !(checkSingleLine xs) + 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 + xs <- if indent == 0 then pure xs else trimLast fc xs + xs <- traverse (trimLeft indent) (dropLastNL 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) + trimFirst _ ((StrLiteral fc _ str)::pstrs) = if any (not . isSpace) (fastUnpack str) then throw $ BadMultiline fc "Unexpected character in the first line" else pure pstrs + trimFirst _ _ = throw $ InternalError "Expected StrLiteral" - trimLast : FC -> List PStr -> Core (List PStr) + 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 + trimLast _ (initPStr `snoc` (StrLiteral fc _ str)) | Snoc (StrLiteral _ _ _) initPStr _ = 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 + else pure initPStr + + dropLastNL : List PStr -> List PStr + dropLastNL pstrs with (snocList pstrs) + dropLastNL [] | Empty = [] + dropLastNL (initPStr `snoc` (StrLiteral fc isLB str)) | Snoc (StrLiteral _ _ _) initPStr _ + = initPStr `snoc` (StrLiteral fc isLB (fst $ break isNL str)) + dropLastNL pstrs | _ = pstrs trimLeft : Nat -> PStr -> Core PStr trimLeft indent (StrLiteral fc True line) diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 71d10e502d..995dd5ed5c 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -426,7 +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 (BadMultiline fc str) = pure $ errorDesc (reflow "While processing multi-line 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/Parser.idr b/src/Idris/Parser.idr index b5ecfc7a1c..9ae8d63fb0 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -794,8 +794,7 @@ mutual 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. + -- The lines after the first '\n' is considered line begin (to be trimed in multiline). -- 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) diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 79be280e61..988110636d 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -176,6 +176,13 @@ stringBegin = many (is '#') <+> (is '"') stringEnd : Nat -> String stringEnd hashtag = "\"" ++ replicate hashtag '#' +multilineBegin : Lexer +multilineBegin = many (is '#') <+> (exact "\"\"\"") <+> + manyUntil newline space <+> expect newline + +multilineEnd : Nat -> String +multilineEnd hashtag = "\"\"\"" ++ replicate hashtag '#' + -- Do this as an entire token, because the contents will be processed by -- a specific back end cgDirective : Lexer @@ -278,7 +285,7 @@ mutual = let escapeChars = "\\" ++ replicate hashtag '#' interpStart = escapeChars ++ "{" escapeLexer = escape (exact escapeChars) any - charLexer = non $ exact (if multi then "\"\"\"" else stringEnd hashtag) + charLexer = non $ exact (if multi then multilineEnd hashtag else stringEnd hashtag) in match (someUntil (exact interpStart) (escapeLexer <|> charLexer)) (\x => StringLit hashtag x) <|> compose (exact interpStart) (const InterpBegin) (const ()) (\_ => rawTokens) (const $ is '}') (const InterpEnd) @@ -302,11 +309,11 @@ mutual <|> match hexLit (\x => IntegerLit (fromHexLit x)) <|> match octLit (\x => IntegerLit (fromOctLit x)) <|> match digits (\x => IntegerLit (cast x)) - <|> compose (exact "\"\"\"") + <|> compose multilineBegin (const $ StringBegin True) - (const ()) - (const $ stringTokens True 0) - (const $ exact "\"\"\"") + countHashtag + (stringTokens True) + (exact . multilineEnd) (const StringEnd) <|> compose stringBegin (const $ StringBegin False) diff --git a/tests/idris2/basic053/StringLiteral.idr b/tests/idris2/basic053/StringLiteral.idr index 2e4007e3a8..e72540563f 100644 --- a/tests/idris2/basic053/StringLiteral.idr +++ b/tests/idris2/basic053/StringLiteral.idr @@ -1,38 +1,18 @@ module StringLiteral -withWrap : String -withWrap = "foo -bar" +rawStr : String +rawStr = #""""""# -withNoWrap : String -withNoWrap = "foo \ -bar" - -withIndent : String -withIndent = "foo - bar" - -withEscape : String -withEscape = #""foo"\#n - \bar"# - -withEscapeNoWrap : String -withEscapeNoWrap = #""foo" \# - \bar"# - -interp : String -interp = "\{withNoWrap}" - -interp2 : String -interp2 = "hello\{ " " ++ ##"world\##{#"."#}"## }" - -interp3 : String -interp3 = "Just 1 + Just 2 = \{ +interp1 : String +interp1 = "Just 1 + Just 2 = \{ show $ do a <- Just 1 b <- Just 2 Just (a + b) }" +interp2 : String +interp2 = "hello\{ " " ++ ##"world\##{#"."#}"## }" + multi1 : String multi1 = """ [project] @@ -43,43 +23,32 @@ multi1 = """ """ multi2 : String -multi2 = """ +multi2 = #""" a b\n - c - """ + \#{"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. + A very very \n\nvery very very \n + very long string. \ """ test : IO () -test = - do - putStrLn withWrap - putStrLn withNoWrap - putStrLn withIndent - putStrLn withEscape - putStrLn withEscapeNoWrap - putStrLn ##" -name: #"foo" -version: "bar" -bzs: \#\'a\n\t\\'"## - putStrLn interp +test = do + putStrLn rawStr + putStrLn interp1 putStrLn interp2 - putStrLn interp3 let idris = "Idris" putStrLn "Hello \{idris ++ show 2}!" putStrLn multi1 @@ -87,4 +56,13 @@ bzs: \#\'a\n\t\\'"## putStrLn multi3 putStrLn multi4 putStrLn """ - """ + """ + putStrLn ##""" +a +"""## + putStrLn ##""" +name: #"foo" +version: "bar" +bzs: \#\'a\n\t\\' +""" +"""## diff --git a/tests/idris2/basic053/expected b/tests/idris2/basic053/expected index 80ddc6ac44..675fc3b40d 100644 --- a/tests/idris2/basic053/expected +++ b/tests/idris2/basic053/expected @@ -1,19 +1,6 @@ -foo -bar -foo bar -foo - bar -"foo" - - \bar -"foo" \bar - -name: #"foo" -version: "bar" -bzs: \#\'a\n\t\\' -foo bar -hello world. +"""" Just 1 + Just 2 = Just 3 +hello world. Hello Idris2! [project] name: "project" @@ -21,15 +8,18 @@ version: "0.1.0" [deps] "semver" = 0.2 a - b - + b\n c sticking together! -A very very very very very -very very very +A very very - very very +very very very -very long string. +very long string. +a +name: #"foo" +version: "bar" +bzs: \#\'a\n\t\\' +""" diff --git a/tests/idris2/perror007/StrError11.idr b/tests/idris2/perror007/StrError11.idr new file mode 100644 index 0000000000..705dc05b2d --- /dev/null +++ b/tests/idris2/perror007/StrError11.idr @@ -0,0 +1,3 @@ +foo : String +foo = "a + " diff --git a/tests/idris2/perror007/expected b/tests/idris2/perror007/expected index 658b54869d..5b33c95a29 100644 --- a/tests/idris2/perror007/expected +++ b/tests/idris2/perror007/expected @@ -23,15 +23,15 @@ StrError3.idr:2:7--2:8 ^ 1/1: Building StrError4 (StrError4.idr) -Error: While processing multiline string. Expected line wrap. +Error: While processing right hand side of foo. Can't find an implementation for FromString (String -> String -> String). -StrError4.idr:2:7--2:13 +StrError4.idr:2:7--2:9 1 | foo : String 2 | foo = """""" - ^^^^^^ + ^^ 1/1: Building StrError5 (StrError5.idr) -Error: While processing multiline string. Indentation not enough. +Error: While processing multi-line string. Indentation not enough. StrError5.idr:2:10--4:5 2 | foo = """ @@ -39,30 +39,31 @@ StrError5.idr:2:10--4:5 4 | """ 1/1: Building StrError6 (StrError6.idr) -Error: While processing multiline string. Unexpected character in the first line. +Error: While processing right hand side of foo. Can't find an implementation for FromString (String -> String -> String). -StrError6.idr:2:10--3:1 +StrError6.idr:2:7--2:9 + 1 | foo : String 2 | foo = """a - 3 | """ + ^^ 1/1: Building StrError7 (StrError7.idr) -Error: While processing multiline string. Unexpected character in the first line. +Error: While processing right hand side of foo. Can't find an implementation for FromString (String -> String -> String). -StrError7.idr:2:10--2:11 +StrError7.idr:2:7--2:9 1 | foo : String 2 | foo = """a""" - ^ + ^^ 1/1: Building StrError8 (StrError8.idr) -Error: While processing multiline string. Unexpected interpolation in the first line. +Error: While processing right hand side of foo. Can't find an implementation for FromString (String -> String -> String). -StrError8.idr:2:10--2:20 +StrError8.idr:2:7--2:9 1 | foo : String 2 | foo = """\{"hello"} - ^^^^^^^^^^ + ^^ 1/1: Building StrError9 (StrError9.idr) -Error: While processing multiline string. Unexpected interpolation in the last line. +Error: While processing multi-line string. Unexpected interpolation in the last line. StrError9.idr:3:1--3:11 1 | foo : String @@ -71,9 +72,16 @@ StrError9.idr:3:1--3:11 ^^^^^^^^^^ 1/1: Building StrError10 (StrError10.idr) -Error: While processing multiline string. Unexpected character in the last line. +Error: While processing multi-line string. Unexpected character in the last line. StrError10.idr:2:10--3:2 2 | foo = """ 3 | a""" +1/1: Building StrError11 (StrError11.idr) +Error: While processing multi-line string. Multi-line string is expected to begin with """. + +StrError11.idr:2:8--3:5 + 2 | foo = "a + 3 | " + diff --git a/tests/idris2/perror007/run b/tests/idris2/perror007/run index fab9a88116..17de657f27 100755 --- a/tests/idris2/perror007/run +++ b/tests/idris2/perror007/run @@ -8,5 +8,6 @@ $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 +$1 --no-color --console-width 0 --check StrError11.idr || true rm -rf build From 83ab4f0f15538cadb47ecb35862428778a25852c Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Sun, 21 Feb 2021 03:13:13 +0800 Subject: [PATCH 03/11] Fix lint --- tests/idris2/basic053/StringLiteral.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/idris2/basic053/StringLiteral.idr b/tests/idris2/basic053/StringLiteral.idr index e72540563f..21037da887 100644 --- a/tests/idris2/basic053/StringLiteral.idr +++ b/tests/idris2/basic053/StringLiteral.idr @@ -57,10 +57,10 @@ test = do putStrLn multi4 putStrLn """ """ - putStrLn ##""" + putStrLn ##""" a """## - putStrLn ##""" + putStrLn ##""" name: #"foo" version: "bar" bzs: \#\'a\n\t\\' From 2813a68c52aca0bc540bdc24cffbf447c3cfcb6f Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Sun, 21 Feb 2021 03:28:23 +0800 Subject: [PATCH 04/11] Fix self-host --- src/Compiler/ES/ES.idr | 26 +++++++++++++------------- src/Compiler/Scheme/Gambit.idr | 15 ++++++++------- src/Core/LinearCheck.idr | 6 +++--- 3 files changed, 24 insertions(+), 23 deletions(-) diff --git a/src/Compiler/ES/ES.idr b/src/Compiler/ES/ES.idr index 1d6c80e7f4..0b43df3670 100644 --- a/src/Compiler/ES/ES.idr +++ b/src/Compiler/ES/ES.idr @@ -62,19 +62,19 @@ addSupportToPreamble name code = addStringIteratorToPreamble : {auto c : Ref ESs ESSt} -> Core String addStringIteratorToPreamble = do - let defs = " -function __prim_stringIteratorNew(str) { - return 0; -} -function __prim_stringIteratorToString(_, str, it, f) { - return f(str.slice(it)); -} -function __prim_stringIteratorNext(str, it) { - if (it >= str.length) - return {h: 0}; - else - return {h: 1, a1: str.charAt(it), a2: it + 1}; -}" + let defs = + "function __prim_stringIteratorNew(str) {" ++ + " return 0;" ++ + "}" ++ + "function __prim_stringIteratorToString(_, str, it, f) {" ++ + " return f(str.slice(it));" ++ + "}" ++ + "function __prim_stringIteratorNext(str, it) {" ++ + " if (it >= str.length)" ++ + " return {h: 0};" ++ + " else" ++ + " return {h: 1, a1: str.charAt(it), a2: it + 1};" ++ + "}" let name = "stringIterator" let newName = esName name addToPreamble name newName defs diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index 034a340f0f..47d4985d7f 100644 --- a/src/Compiler/Scheme/Gambit.idr +++ b/src/Compiler/Scheme/Gambit.idr @@ -48,13 +48,14 @@ findGSCBackend = Just e => " -cc " ++ e schHeader : String -schHeader = "; @generated\n - (declare (block) - (inlining-limit 450) - (standard-bindings) - (extended-bindings) - (not safe) - (optimize-dead-definitions))\n" +schHeader = + "; @generated\n" ++ + "(declare (block)\n" ++ + "(inlining-limit 450)\n" ++ + "(standard-bindings)\n" ++ + "(extended-bindings)\n" ++ + "(not safe)\n" ++ + "(optimize-dead-definitions))\n" showGambitChar : Char -> String -> String showGambitChar '\\' = ("\\\\" ++) diff --git a/src/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index 8d029ce58a..a82c7a764a 100644 --- a/src/Core/LinearCheck.idr +++ b/src/Core/LinearCheck.idr @@ -667,9 +667,9 @@ mutual = do defs <- get Ctxt empty <- clearDefs defs ty <- quote empty env nty - throw (GenericMsg fc ("Linearity checking failed on metavar - " ++ show n ++ " (" ++ show ty ++ - " not a function type)")) + throw (GenericMsg fc ("Linearity checking failed on metavar " + ++ show n ++ " (" ++ show ty + ++ " not a function type)")) lcheckMeta rig erase env fc n idx [] chk nty = do defs <- get Ctxt pure (Meta fc n idx (reverse chk), glueBack defs env nty, []) From 2358ac0f737a317dc9e4a84574daf0f6b9ed1a41 Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Tue, 23 Feb 2021 02:10:57 +0800 Subject: [PATCH 05/11] Fix StrError12 test --- src/Idris/Desugar.idr | 78 +++++++++++++-------------- src/Idris/Elab/Interface.idr | 2 +- src/Idris/Parser.idr | 60 ++++++++++++++------- src/Idris/Pretty.idr | 4 +- src/Idris/Syntax.idr | 16 +++--- src/Libraries/Data/List/Extra.idr | 8 +-- src/Parser/Lexer/Source.idr | 11 ++-- src/Parser/Rule/Source.idr | 12 +++-- tests/idris2/perror007/StrError12.idr | 4 ++ tests/idris2/perror007/expected | 46 ++++++++++------ tests/idris2/perror007/run | 1 + 11 files changed, 146 insertions(+), 96 deletions(-) create mode 100644 tests/idris2/perror007/StrError12.idr diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 406f000f12..3c79b9df6a 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -9,6 +9,7 @@ import Core.Options import Core.TT import Core.Unify +import Libraries.Data.List.Extra import Libraries.Data.StringMap import Libraries.Data.String.Extra import Libraries.Data.ANameMap @@ -30,6 +31,7 @@ import Libraries.Utils.Shunting import Libraries.Utils.String import Control.Monad.State +import Data.Maybe import Data.List import Data.List.Views import Data.List1 @@ -276,10 +278,10 @@ 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 (PMultiline fc indent lines) + = addFromString fc !(expandString side ps fc !(trimMultiline fc indent lines)) desugarB side ps (PString fc strs) - = addFromString fc !(expandString side ps fc !(checkSingleLine strs)) + = addFromString fc !(expandString side ps fc strs) desugarB side ps (PDoBlock fc ns block) = expandDo side ps fc ns block desugarB side ps (PBang fc term) @@ -416,68 +418,66 @@ mutual 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 ((StrLiteral fc str1)::(StrLiteral _ str2)::xs) + = (StrLiteral fc (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 - checkSingleLine : List PStr -> Core (List PStr) - checkSingleLine [] = pure [] - checkSingleLine ((StrLiteral fc True _)::xs) - = throw $ BadMultiline fc "Multi-line string is expected to begin with \"\"\"" - checkSingleLine (x::xs) = pure $ x :: !(checkSingleLine xs) - - trimMultiline : FC -> Nat -> List PStr -> Core (List PStr) - trimMultiline fc indent xs = do - xs <- trimFirst fc xs - xs <- if indent == 0 then pure xs else trimLast fc xs - xs <- traverse (trimLeft indent) (dropLastNL xs) - pure xs + trimMultiline : FC -> Nat -> List (List PStr) -> Core (List PStr) + trimMultiline fc indent lines + = if indent == 0 + then pure $ dropLastNL $ concat lines + else do + lines <- trimLast fc lines + lines <- traverse (trimLeft indent) lines + pure $ dropLastNL $ concat lines where - trimFirst : FC -> List PStr -> Core (List PStr) - trimFirst _ ((StrLiteral fc _ str)::pstrs) - = if any (not . isSpace) (fastUnpack str) - then throw $ BadMultiline fc "Unexpected character in the first line" - else pure pstrs - trimFirst _ _ = throw $ InternalError "Expected StrLiteral" - - trimLast : FC -> List PStr -> Core (List PStr) - trimLast fc pstrs with (snocList pstrs) + trimLast : FC -> List (List PStr) -> Core (List (List PStr)) + trimLast fc lines with (snocList lines) 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 _ + trimLast _ (initLines `snoc` []) | Snoc [] initLines _ = pure lines + trimLast _ (initLines `snoc` [StrLiteral fc str]) | Snoc [(StrLiteral _ _)] initLines _ = if any (not . isSpace) (fastUnpack str) then throw $ BadMultiline fc "Unexpected character in the last line" - else pure initPStr + else pure initLines + trimLast _ (initLines `snoc` xs) | Snoc xs initLines _ + = let fc = fromMaybe fc $ findBy (\case StrInterp fc _ => Just fc; + StrLiteral _ _ => Nothing) xs in + throw $ BadMultiline fc "Unexpected interpolation in the last line" dropLastNL : List PStr -> List PStr dropLastNL pstrs with (snocList pstrs) dropLastNL [] | Empty = [] - dropLastNL (initPStr `snoc` (StrLiteral fc isLB str)) | Snoc (StrLiteral _ _ _) initPStr _ - = initPStr `snoc` (StrLiteral fc isLB (fst $ break isNL str)) + dropLastNL (initLines `snoc` (StrLiteral fc str)) | Snoc (StrLiteral _ _) initLines _ + = initLines `snoc` (StrLiteral fc (fst $ break isNL str)) dropLastNL pstrs | _ = pstrs - trimLeft : Nat -> PStr -> Core PStr - trimLeft indent (StrLiteral fc True line) - = let (trimed, rest) = splitAt indent (fastUnpack line) in + trimLeft : Nat -> List PStr -> Core (List PStr) + trimLeft indent [] = pure [] + trimLeft indent [(StrLiteral fc str)] + = let (trimed, rest) = splitAt indent (fastUnpack str) 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 + else pure $ [StrLiteral fc (fastPack rest)] + trimLeft indent ((StrLiteral fc str)::xs) + = let (trimed, rest) = splitAt indent (fastUnpack str) in + if any (not . isSpace) trimed || length trimed < indent + then throw $ BadMultiline fc "Indentation not enough" + else pure $ (StrLiteral fc (fastPack rest))::xs + trimLeft indent xs = throw $ BadMultiline fc "Indentation not enough" expandDo : {auto s : Ref Syn SyntaxInfo} -> {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index a2a7792623..0635b31ed9 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -424,7 +424,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body (rig, dty) <- the (Core (RigCount, RawImp)) $ - case firstBy (\ d => d <$ guard (n == d.name)) tydecls of + case findBy (\ d => d <$ guard (n == d.name)) tydecls of Just d => pure (d.count, d.type) Nothing => throw (GenericMsg fc ("No method named " ++ show n ++ " in interface " ++ show iname)) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 9ae8d63fb0..e90e05255a 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -392,7 +392,8 @@ mutual <|> binder fname indents <|> rewrite_ fname indents <|> record_ fname indents - <|> interpStr pdef fname indents + <|> singlelineStr pdef fname indents + <|> multilineStr 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 ")") @@ -775,30 +776,49 @@ mutual expr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm expr = typeExpr + interpBlock : ParseOpts -> FileName -> IndentInfo -> Rule PTerm + interpBlock q fname idents = interpBegin *> (mustWork $ expr q fname idents) <* interpEnd + export - interpStr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm - interpStr q fname idents - = do b <- bounds $ do multi <- strBegin + singlelineStr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm + singlelineStr q fname idents + = do b <- bounds $ do strBegin commit - xs <- many $ bounds $ interpBlock <||> strLitLines - endloc <- location + xs <- many $ bounds $ (interpBlock q fname idents) <||> strLitLines 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 + the (SourceEmptyRule _) $ + case traverse toPStr xs of + Left err => fatalError err + Right pstrs => pure $ pstrs + pure $ PString (boundToFC fname b) b.val where - interpBlock : Rule PTerm - interpBlock = interpBegin *> (mustWork $ expr q fname idents) <* interpEnd - - toPStr : (WithBounds $ Either PTerm (List1 String)) -> List PStr + toPStr : (WithBounds $ Either PTerm (List1 String)) -> Either String PStr toPStr x = case x.val of - -- The lines after the first '\n' is considered line begin (to be trimed in multiline). - -- 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] + Right (str:::[]) => Right $ StrLiteral (boundToFC fname x) str + Right (_:::strs) => Left "Multi-line string is expected to begin with \"\"\"" + Left tm => Right $ StrInterp (boundToFC fname x) tm + + export + multilineStr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm + multilineStr q fname idents + = do b <- bounds $ do multilineBegin + commit + xs <- many $ bounds $ (interpBlock q fname idents) <||> strLitLines + endloc <- location + strEnd + pure (endloc, toLines xs [] []) + pure $ let ((_, col), xs) = b.val in + PMultiline (boundToFC fname b) (fromInteger $ cast col) xs + where + toLines : List (WithBounds $ Either PTerm (List1 String)) -> List PStr -> List (List PStr) -> List (List PStr) + toLines [] line acc = reverse (reverse line::acc) + toLines (x::xs) line acc + = case x.val of + Left tm => toLines xs ((StrInterp (boundToFC fname x) tm)::line) acc + Right (str:::[]) => toLines xs ((StrLiteral (boundToFC fname x) str)::line) acc + Right (str:::strs@(_::_)) => toLines xs [StrLiteral (boundToFC fname x) (last strs)] + ((map (\str => [StrLiteral (boundToFC fname x) str]) (List.drop 1 $ reverse strs)) + ++ (List.reverse ((StrLiteral (boundToFC fname x) str)::line)::acc)) visOption : Rule Visibility visOption diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index dc5a94108c..230210a51a 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,7 +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 (PMultiline _ indent xs) = "multiline" <++> (parenthesise (d > appPrec) $ hsep $ punctuate "++" (prettyString <$> concat 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 da5c52ca03..aaada5a8d3 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -82,7 +82,7 @@ mutual -- Syntactic sugar PString : FC -> List PStr -> PTerm - PMultiline : FC -> (indent : Nat) -> List PStr -> PTerm + PMultiline : FC -> (indent : Nat) -> List (List PStr) -> PTerm PDoBlock : FC -> Maybe Namespace -> List PDo -> PTerm PBang : FC -> PTerm -> PTerm PIdiom : FC -> PTerm -> PTerm @@ -179,9 +179,7 @@ mutual public export data PStr : Type where - ||| 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 + StrLiteral : FC -> String -> PStr StrInterp : FC -> PTerm -> PStr export @@ -502,7 +500,7 @@ mutual export showPStr : PStr -> String - showPStr (StrLiteral _ _ str) = show str + showPStr (StrLiteral _ str) = show str showPStr (StrInterp _ tm) = show tm showUpdate : PFieldUpdate -> String @@ -593,7 +591,7 @@ mutual showPrec d (PEq fc l r) = showPrec d l ++ " = " ++ showPrec d r showPrec d (PBracketed _ tm) = "(" ++ showPrec d tm ++ ")" showPrec d (PString _ xs) = join " ++ " $ showPStr <$> xs - showPrec d (PMultiline _ indent xs) = "multiline (" ++ (join " ++ " $ showPStr <$> xs) ++ ")" + showPrec d (PMultiline _ indent xs) = "multiline (" ++ (join " ++ " $ showPStr <$> concat xs) ++ ")" showPrec d (PDoBlock _ ns ds) = "do " ++ showSep " ; " (map showDo ds) showPrec d (PBang _ tm) = "!" ++ showPrec d tm @@ -922,7 +920,7 @@ mapPTermM f = goPTerm where PString fc <$> goPStrings xs >>= f goPTerm (PMultiline fc x ys) = - PMultiline fc x <$> goPStrings ys + PMultiline fc x <$> goPStringLines ys >>= f goPTerm (PDoBlock fc ns xs) = PDoBlock fc ns <$> goPDos xs @@ -1112,6 +1110,10 @@ mapPTermM f = goPTerm where <*> goPTerm t <*> go4TupledPTerms ts + goPStringLines : List (List PStr) -> Core (List (List PStr)) + goPStringLines [] = pure [] + goPStringLines (line :: lines) = (::) <$> goPStrings line <*> goPStringLines lines + goPStrings : List PStr -> Core (List PStr) goPStrings [] = pure [] goPStrings (str :: strs) = (::) <$> goPStr str <*> goPStrings strs diff --git a/src/Libraries/Data/List/Extra.idr b/src/Libraries/Data/List/Extra.idr index 49ed7fc85d..f54b8edb08 100644 --- a/src/Libraries/Data/List/Extra.idr +++ b/src/Libraries/Data/List/Extra.idr @@ -13,11 +13,11 @@ elemAt (l :: _) Z = Just l elemAt (_ :: ls) (S n) = elemAt ls n export -firstBy : (a -> Maybe b) -> List a -> Maybe b -firstBy p [] = Nothing -firstBy p (x :: xs) +findBy : (a -> Maybe b) -> List a -> Maybe b +findBy p [] = Nothing +findBy p (x :: xs) = case p x of - Nothing => firstBy p xs + Nothing => findBy p xs Just win => pure win export diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 988110636d..946fcdb7ac 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -178,7 +178,7 @@ stringEnd hashtag = "\"" ++ replicate hashtag '#' multilineBegin : Lexer multilineBegin = many (is '#') <+> (exact "\"\"\"") <+> - manyUntil newline space <+> expect newline + manyUntil newline space <+> newline multilineEnd : Nat -> String multilineEnd hashtag = "\"\"\"" ++ replicate hashtag '#' @@ -288,7 +288,12 @@ mutual charLexer = non $ exact (if multi then multilineEnd hashtag else stringEnd hashtag) in match (someUntil (exact interpStart) (escapeLexer <|> charLexer)) (\x => StringLit hashtag x) - <|> compose (exact interpStart) (const InterpBegin) (const ()) (\_ => rawTokens) (const $ is '}') (const InterpEnd) + <|> compose (exact interpStart) + (const InterpBegin) + (const ()) + (\_ => rawTokens) + (const $ is '}') + (const InterpEnd) rawTokens : Tokenizer Token rawTokens = @@ -319,7 +324,7 @@ mutual (const $ StringBegin False) countHashtag (stringTokens False) - (exact . stringEnd) + (\hashtag => exact (stringEnd hashtag) <+> reject (is '"')) (const StringEnd) <|> match charLit (\x => CharLit (stripQuotes x)) <|> match dotIdent (\x => DotIdent (assert_total $ strTail x)) diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr index 5926726cc5..b136b6dacd 100644 --- a/src/Parser/Rule/Source.idr +++ b/src/Parser/Rule/Source.idr @@ -95,12 +95,18 @@ strLitLines (splitAfter isNL (fastUnpack s)) _ => Nothing) -||| String literal begin quote. The bool indicates whether the it is multiline string. export -strBegin : Rule Bool +strBegin : Rule () strBegin = terminal "Expected string begin" (\x => case x.val of - StringBegin multi => Just multi + StringBegin False => Just () + _ => Nothing) + +export +multilineBegin : Rule () +multilineBegin = terminal "Expected multiline string begin" + (\x => case x.val of + StringBegin True => Just () _ => Nothing) export diff --git a/tests/idris2/perror007/StrError12.idr b/tests/idris2/perror007/StrError12.idr new file mode 100644 index 0000000000..4781b8619d --- /dev/null +++ b/tests/idris2/perror007/StrError12.idr @@ -0,0 +1,4 @@ +foo : String +foo = """ + \{show 1} + """ diff --git a/tests/idris2/perror007/expected b/tests/idris2/perror007/expected index 5b33c95a29..d9a087694e 100644 --- a/tests/idris2/perror007/expected +++ b/tests/idris2/perror007/expected @@ -23,44 +23,43 @@ StrError3.idr:2:7--2:8 ^ 1/1: Building StrError4 (StrError4.idr) -Error: While processing right hand side of foo. Can't find an implementation for FromString (String -> String -> String). +Error: Bracket is not properly closed. -StrError4.idr:2:7--2:9 +StrError4.idr:2:7--2:8 1 | foo : String 2 | foo = """""" - ^^ + ^ 1/1: Building StrError5 (StrError5.idr) Error: While processing multi-line string. Indentation not enough. -StrError5.idr:2:10--4:5 - 2 | foo = """ +StrError5.idr:3:1--4:5 3 | a 4 | """ 1/1: Building StrError6 (StrError6.idr) -Error: While processing right hand side of foo. Can't find an implementation for FromString (String -> String -> String). +Error: Bracket is not properly closed. -StrError6.idr:2:7--2:9 +StrError6.idr:2:7--2:8 1 | foo : String 2 | foo = """a - ^^ + ^ 1/1: Building StrError7 (StrError7.idr) -Error: While processing right hand side of foo. Can't find an implementation for FromString (String -> String -> String). +Error: Bracket is not properly closed. -StrError7.idr:2:7--2:9 +StrError7.idr:2:7--2:8 1 | foo : String 2 | foo = """a""" - ^^ + ^ 1/1: Building StrError8 (StrError8.idr) -Error: While processing right hand side of foo. Can't find an implementation for FromString (String -> String -> String). +Error: Bracket is not properly closed. -StrError8.idr:2:7--2:9 +StrError8.idr:2:7--2:8 1 | foo : String 2 | foo = """\{"hello"} - ^^ + ^ 1/1: Building StrError9 (StrError9.idr) Error: While processing multi-line string. Unexpected interpolation in the last line. @@ -74,14 +73,27 @@ StrError9.idr:3:1--3:11 1/1: Building StrError10 (StrError10.idr) Error: While processing multi-line string. Unexpected character in the last line. -StrError10.idr:2:10--3:2 +StrError10.idr:3:1--3:2 + 1 | foo : String 2 | foo = """ 3 | a""" + ^ 1/1: Building StrError11 (StrError11.idr) -Error: While processing multi-line string. Multi-line string is expected to begin with """. +Error: Multi-line string is expected to begin with """. -StrError11.idr:2:8--3:5 +StrError11.idr:4:1--4:2 + 1 | foo : String 2 | foo = "a 3 | " + ^ + +1/1: Building StrError12 (StrError12.idr) +Error: While processing multi-line string. Indentation not enough. + +StrError12.idr:3:1--3:3 + 1 | foo : String + 2 | foo = """ + 3 | \{show 1} + ^^ diff --git a/tests/idris2/perror007/run b/tests/idris2/perror007/run index 17de657f27..c35e9dc600 100755 --- a/tests/idris2/perror007/run +++ b/tests/idris2/perror007/run @@ -9,5 +9,6 @@ $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 $1 --no-color --console-width 0 --check StrError11.idr || true +$1 --no-color --console-width 0 --check StrError12.idr || true rm -rf build From 626cfa8e19ccc4e97d51fb2be880846e66c32dc1 Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Tue, 23 Feb 2021 02:16:31 +0800 Subject: [PATCH 06/11] Add comment --- src/Idris/Parser.idr | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index e90e05255a..f6b1acbd74 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -816,6 +816,7 @@ mutual = case x.val of Left tm => toLines xs ((StrInterp (boundToFC fname x) tm)::line) acc Right (str:::[]) => toLines xs ((StrLiteral (boundToFC fname x) str)::line) acc + -- FIXME: calculate the precise FC so as to improve error report for invalid indentation. Right (str:::strs@(_::_)) => toLines xs [StrLiteral (boundToFC fname x) (last strs)] ((map (\str => [StrLiteral (boundToFC fname x) str]) (List.drop 1 $ reverse strs)) ++ (List.reverse ((StrLiteral (boundToFC fname x) str)::line)::acc)) From 775d7b4bdbb74db68be3756d6861853c16ce3ed9 Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Tue, 23 Feb 2021 13:10:36 +0800 Subject: [PATCH 07/11] Add test for escaping NL --- tests/idris2/basic053/StringLiteral.idr | 2 +- tests/idris2/basic053/expected | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/tests/idris2/basic053/StringLiteral.idr b/tests/idris2/basic053/StringLiteral.idr index 21037da887..c5c12bd599 100644 --- a/tests/idris2/basic053/StringLiteral.idr +++ b/tests/idris2/basic053/StringLiteral.idr @@ -24,7 +24,7 @@ multi1 = """ multi2 : String multi2 = #""" - a + a\# b\n \#{"c"} """# diff --git a/tests/idris2/basic053/expected b/tests/idris2/basic053/expected index 675fc3b40d..0ed41e4974 100644 --- a/tests/idris2/basic053/expected +++ b/tests/idris2/basic053/expected @@ -7,8 +7,7 @@ name: "project" version: "0.1.0" [deps] "semver" = 0.2 -a - b\n +a b\n c sticking together! From 8c23f5944b0de57f0dc57ab06b282f389ef5b8cc Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Thu, 25 Feb 2021 18:43:42 +0800 Subject: [PATCH 08/11] address comment --- src/Idris/Desugar.idr | 11 +++++------ src/Idris/Parser.idr | 12 +++++++----- src/Idris/Syntax.idr | 10 +++++----- tests/idris2/perror007/expected | 8 ++++---- 4 files changed, 21 insertions(+), 20 deletions(-) diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 3c79b9df6a..0c5f0b7e68 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -424,7 +424,6 @@ mutual -- merge neighbouring StrLiteral mergeStrLit : List PStr -> List PStr mergeStrLit [] = [] - mergeStrLit [x] = [x] mergeStrLit ((StrLiteral fc str1)::(StrLiteral _ str2)::xs) = (StrLiteral fc (str1 ++ str2)) :: xs mergeStrLit (x::xs) = x :: mergeStrLit xs @@ -451,12 +450,12 @@ mutual trimLast _ (initLines `snoc` []) | Snoc [] initLines _ = pure lines trimLast _ (initLines `snoc` [StrLiteral fc str]) | Snoc [(StrLiteral _ _)] initLines _ = if any (not . isSpace) (fastUnpack str) - then throw $ BadMultiline fc "Unexpected character in the last line" + then throw $ BadMultiline fc "Closing delimiter of multiline strings cannot be preceded by non-whitespace characters" else pure initLines trimLast _ (initLines `snoc` xs) | Snoc xs initLines _ = let fc = fromMaybe fc $ findBy (\case StrInterp fc _ => Just fc; StrLiteral _ _ => Nothing) xs in - throw $ BadMultiline fc "Unexpected interpolation in the last line" + throw $ BadMultiline fc "Closing delimiter of multiline strings cannot be preceded by non-whitespace characters" dropLastNL : List PStr -> List PStr dropLastNL pstrs with (snocList pstrs) @@ -470,14 +469,14 @@ mutual trimLeft indent [(StrLiteral fc str)] = let (trimed, rest) = splitAt indent (fastUnpack str) in if any (not . isSpace) trimed - then throw $ BadMultiline fc "Indentation not enough" + then throw $ BadMultiline fc "Line is less indented than the closing delimiter" else pure $ [StrLiteral fc (fastPack rest)] trimLeft indent ((StrLiteral fc str)::xs) = let (trimed, rest) = splitAt indent (fastUnpack str) in if any (not . isSpace) trimed || length trimed < indent - then throw $ BadMultiline fc "Indentation not enough" + then throw $ BadMultiline fc "Line is less indented than the closing delimiter" else pure $ (StrLiteral fc (fastPack rest))::xs - trimLeft indent xs = throw $ BadMultiline fc "Indentation not enough" + trimLeft indent xs = throw $ BadMultiline fc "Line is less indented than the closing delimiter" expandDo : {auto s : Ref Syn SyntaxInfo} -> {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index f6b1acbd74..67ca89713d 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -795,6 +795,8 @@ mutual toPStr : (WithBounds $ Either PTerm (List1 String)) -> Either String PStr toPStr x = case x.val of Right (str:::[]) => Right $ StrLiteral (boundToFC fname x) str + -- FIXME: This throws the error at the next line after the line wrap. + -- But it's supposed to point to the string begin quote. Right (_:::strs) => Left "Multi-line string is expected to begin with \"\"\"" Left tm => Right $ StrInterp (boundToFC fname x) tm @@ -811,15 +813,15 @@ mutual PMultiline (boundToFC fname b) (fromInteger $ cast col) xs where toLines : List (WithBounds $ Either PTerm (List1 String)) -> List PStr -> List (List PStr) -> List (List PStr) - toLines [] line acc = reverse (reverse line::acc) + toLines [] line acc = acc `snoc` line toLines (x::xs) line acc = case x.val of - Left tm => toLines xs ((StrInterp (boundToFC fname x) tm)::line) acc - Right (str:::[]) => toLines xs ((StrLiteral (boundToFC fname x) str)::line) acc + Left tm => toLines xs (line `snoc` (StrInterp (boundToFC fname x) tm)) acc + Right (str:::[]) => toLines xs (line `snoc` (StrLiteral (boundToFC fname x) str)) acc -- FIXME: calculate the precise FC so as to improve error report for invalid indentation. Right (str:::strs@(_::_)) => toLines xs [StrLiteral (boundToFC fname x) (last strs)] - ((map (\str => [StrLiteral (boundToFC fname x) str]) (List.drop 1 $ reverse strs)) - ++ (List.reverse ((StrLiteral (boundToFC fname x) str)::line)::acc)) + ((acc `snoc` (line `snoc` (StrLiteral (boundToFC fname x) str))) ++ + ((\str => [StrLiteral (boundToFC fname x) str]) <$> (init strs))) visOption : Rule Visibility visOption diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index aaada5a8d3..b95a0b93f1 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -499,9 +499,9 @@ mutual = "rewrite " ++ show rule export - showPStr : PStr -> String - showPStr (StrLiteral _ str) = show str - showPStr (StrInterp _ tm) = show tm + Show PStr where + show (StrLiteral _ str) = show str + show (StrInterp _ tm) = show tm showUpdate : PFieldUpdate -> String showUpdate (PSetField p v) = showSep "." p ++ " = " ++ show v @@ -590,8 +590,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 " ++ " $ showPStr <$> xs - showPrec d (PMultiline _ indent xs) = "multiline (" ++ (join " ++ " $ showPStr <$> concat xs) ++ ")" + showPrec d (PString _ xs) = join " ++ " $ show <$> xs + showPrec d (PMultiline _ indent xs) = "multiline (" ++ (join " ++ " $ show <$> concat xs) ++ ")" showPrec d (PDoBlock _ ns ds) = "do " ++ showSep " ; " (map showDo ds) showPrec d (PBang _ tm) = "!" ++ showPrec d tm diff --git a/tests/idris2/perror007/expected b/tests/idris2/perror007/expected index d9a087694e..136f9a0c06 100644 --- a/tests/idris2/perror007/expected +++ b/tests/idris2/perror007/expected @@ -31,7 +31,7 @@ StrError4.idr:2:7--2:8 ^ 1/1: Building StrError5 (StrError5.idr) -Error: While processing multi-line string. Indentation not enough. +Error: While processing multi-line string. Line is less indented than the closing delimiter. StrError5.idr:3:1--4:5 3 | a @@ -62,7 +62,7 @@ StrError8.idr:2:7--2:8 ^ 1/1: Building StrError9 (StrError9.idr) -Error: While processing multi-line string. Unexpected interpolation in the last line. +Error: While processing multi-line string. Closing delimiter of multiline strings cannot be preceded by non-whitespace characters. StrError9.idr:3:1--3:11 1 | foo : String @@ -71,7 +71,7 @@ StrError9.idr:3:1--3:11 ^^^^^^^^^^ 1/1: Building StrError10 (StrError10.idr) -Error: While processing multi-line string. Unexpected character in the last line. +Error: While processing multi-line string. Closing delimiter of multiline strings cannot be preceded by non-whitespace characters. StrError10.idr:3:1--3:2 1 | foo : String @@ -89,7 +89,7 @@ StrError11.idr:4:1--4:2 ^ 1/1: Building StrError12 (StrError12.idr) -Error: While processing multi-line string. Indentation not enough. +Error: While processing multi-line string. Line is less indented than the closing delimiter. StrError12.idr:3:1--3:3 1 | foo : String From 01c5011653746d5703583fee735469ad540d669b Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Thu, 25 Feb 2021 20:14:26 +0800 Subject: [PATCH 09/11] improve error report --- src/Idris/Parser.idr | 8 ++++---- tests/idris2/perror007/expected | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 2138114a44..21671f7bd2 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -787,11 +787,11 @@ mutual = do b <- bounds $ do strBegin commit xs <- many $ bounds $ (interpBlock q fname idents) <||> strLitLines + pstrs <- case traverse toPStr xs of + Left err => fatalError err + Right pstrs => pure $ pstrs strEnd - the (SourceEmptyRule _) $ - case traverse toPStr xs of - Left err => fatalError err - Right pstrs => pure $ pstrs + pure pstrs pure $ PString (boundToFC fname b) b.val where toPStr : (WithBounds $ Either PTerm (List1 String)) -> Either String PStr diff --git a/tests/idris2/perror007/expected b/tests/idris2/perror007/expected index 136f9a0c06..d081e68e9e 100644 --- a/tests/idris2/perror007/expected +++ b/tests/idris2/perror007/expected @@ -82,11 +82,11 @@ StrError10.idr:3:1--3:2 1/1: Building StrError11 (StrError11.idr) Error: Multi-line string is expected to begin with """. -StrError11.idr:4:1--4:2 +StrError11.idr:3:5--3:6 1 | foo : String 2 | foo = "a 3 | " - ^ + ^ 1/1: Building StrError12 (StrError12.idr) Error: While processing multi-line string. Line is less indented than the closing delimiter. From 7630aaea5b49206f5c891b408a8cafa851b35a64 Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Thu, 25 Feb 2021 22:12:21 +0800 Subject: [PATCH 10/11] address comment --- src/Compiler/ES/ES.idr | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/src/Compiler/ES/ES.idr b/src/Compiler/ES/ES.idr index aae9042a56..62e4213b2b 100644 --- a/src/Compiler/ES/ES.idr +++ b/src/Compiler/ES/ES.idr @@ -66,19 +66,20 @@ addSupportToPreamble name code = addStringIteratorToPreamble : {auto c : Ref ESs ESSt} -> Core String addStringIteratorToPreamble = do - let defs = - "function __prim_stringIteratorNew(str) {" ++ - " return 0;" ++ - "}" ++ - "function __prim_stringIteratorToString(_, str, it, f) {" ++ - " return f(str.slice(it));" ++ - "}" ++ - "function __prim_stringIteratorNext(str, it) {" ++ - " if (it >= str.length)" ++ - " return {h: 0};" ++ - " else" ++ - " return {h: 1, a1: str.charAt(it), a2: it + 1};" ++ - "}" + let defs = unlines $ + [ "function __prim_stringIteratorNew(str) {" + , " return 0;" + , "}" + , "function __prim_stringIteratorToString(_, str, it, f) {" + , " return f(str.slice(it));" + , "}" + , "function __prim_stringIteratorNext(str, it) {" + , " if (it >= str.length)" + , " return {h: 0};" + , " else" + , " return {h: 1, a1: str.charAt(it), a2: it + 1};" + , "}" + ] let name = "stringIterator" let newName = esName name addToPreamble name newName defs From 75b41bc8b781187aa722200a99dc75abf1a17151 Mon Sep 17 00:00:00 2001 From: Andy Lok Date: Sat, 27 Feb 2021 02:42:42 +0800 Subject: [PATCH 11/11] Remove FIXME Signed-off-by: Andy Lok --- src/Idris/Parser.idr | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 21671f7bd2..879ce76cbf 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -797,8 +797,6 @@ mutual toPStr : (WithBounds $ Either PTerm (List1 String)) -> Either String PStr toPStr x = case x.val of Right (str:::[]) => Right $ StrLiteral (boundToFC fname x) str - -- FIXME: This throws the error at the next line after the line wrap. - -- But it's supposed to point to the string begin quote. Right (_:::strs) => Left "Multi-line string is expected to begin with \"\"\"" Left tm => Right $ StrInterp (boundToFC fname x) tm @@ -820,7 +818,6 @@ mutual = case x.val of Left tm => toLines xs (line `snoc` (StrInterp (boundToFC fname x) tm)) acc Right (str:::[]) => toLines xs (line `snoc` (StrLiteral (boundToFC fname x) str)) acc - -- FIXME: calculate the precise FC so as to improve error report for invalid indentation. Right (str:::strs@(_::_)) => toLines xs [StrLiteral (boundToFC fname x) (last strs)] ((acc `snoc` (line `snoc` (StrLiteral (boundToFC fname x) str))) ++ ((\str => [StrLiteral (boundToFC fname x) str]) <$> (init strs)))