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/Compiler/ES/ES.idr b/src/Compiler/ES/ES.idr index cf100c072e..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 diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index a5ea8e0609..e29a3c4f19 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/Core.idr b/src/Core/Core.idr index 16ce5e2109..d651f87ea9 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -144,6 +144,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 @@ -310,6 +311,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" ++ @@ -387,6 +389,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/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index 0c213c08c5..44c75fca22 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, []) diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index cb0503fa48..ae032c4177 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -9,7 +9,9 @@ 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 import Idris.DocString @@ -30,7 +32,11 @@ 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 +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 @@ -78,7 +84,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) @@ -273,7 +279,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 (PString fc strs) = addFromString fc !(expandString side ps fc 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 strs) desugarB side ps (PDoBlock fc ns block) = expandDo side ps fc ns block desugarB side ps (PBang fc term) @@ -405,7 +414,7 @@ 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 @@ -413,6 +422,13 @@ mutual 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 ((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 (StrInterp _ _) = True @@ -420,6 +436,49 @@ mutual concatStr : RawImp -> RawImp -> RawImp concatStr a b = IApp (getFC a) (IApp (getFC b) (IVar (getFC b) (UN "++")) a) b + 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 + 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 _ (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 "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 "Closing delimiter of multiline strings cannot be preceded by non-whitespace characters" + + dropLastNL : List PStr -> List PStr + dropLastNL pstrs with (snocList pstrs) + dropLastNL [] | Empty = [] + dropLastNL (initLines `snoc` (StrLiteral fc str)) | Snoc (StrLiteral _ _) initLines _ + = initLines `snoc` (StrLiteral fc (fst $ break isNL str)) + dropLastNL pstrs | _ = pstrs + + 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 "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 "Line is less indented than the closing delimiter" + else pure $ (StrLiteral fc (fastPack rest))::xs + 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} -> {auto u : Ref UST UState} -> diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index 4d01e32f6e..974b53feba 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -423,7 +423,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/Error.idr b/src/Idris/Error.idr index 3d6f4e20f1..995dd5ed5c 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 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/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 f127baf614..879ce76cbf 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -394,8 +394,8 @@ mutual <|> binder fname indents <|> rewrite_ fname indents <|> record_ fname indents - <|> do b <- bounds (interpStr pdef fname indents) - pure (PString (boundToFC fname b) b.val) + <|> 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 ")") @@ -778,23 +778,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 (List PStr) - interpStr q fname idents = do - strBegin - commit - xs <- many $ bounds $ interpBlock <||> strLit - strEnd - pure $ toPString <$> xs + singlelineStr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm + singlelineStr q fname idents + = 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 + 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)) -> Either String PStr + toPStr x = case x.val of + 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 - toPString : (WithBounds $ Either PTerm String) -> PStr - toPString x + 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 = acc `snoc` line + toLines (x::xs) line acc = case x.val of - Right s => StrLiteral (boundToFC fname x) s - Left tm => StrInterp (boundToFC fname x) tm + Left tm => toLines xs (line `snoc` (StrInterp (boundToFC fname x) tm)) acc + Right (str:::[]) => toLines xs (line `snoc` (StrLiteral (boundToFC fname x) str)) acc + 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))) visOption : Rule Visibility visOption @@ -1187,7 +1213,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..230210a51a 100644 --- a/src/Idris/Pretty.idr +++ b/src/Idris/Pretty.idr @@ -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 <$> 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 6a72d4099a..b95a0b93f1 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 (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 @@ -496,9 +498,10 @@ mutual showDo (DoRewrite _ rule) = "rewrite " ++ show rule - showString : PStr -> String - showString (StrLiteral _ str) = show str - showString (StrInterp _ tm) = show tm + export + Show PStr where + show (StrLiteral _ str) = show str + show (StrInterp _ tm) = show tm showUpdate : PFieldUpdate -> String showUpdate (PSetField p v) = showSep "." p ++ " = " ++ show v @@ -587,7 +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 " ++ " $ showString <$> 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 @@ -915,6 +919,9 @@ mapPTermM f = goPTerm where goPTerm (PString fc xs) = PString fc <$> goPStrings xs >>= f + goPTerm (PMultiline fc x ys) = + PMultiline fc x <$> goPStringLines ys + >>= f goPTerm (PDoBlock fc ns xs) = PDoBlock fc ns <$> goPDos xs >>= f @@ -975,9 +982,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 @@ -1103,9 +1110,13 @@ 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) = (::) <$> 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..f54b8edb08 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. @@ -11,9 +13,24 @@ 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 +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..946fcdb7ac 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" @@ -174,6 +176,13 @@ stringBegin = many (is '#') <+> (is '"') stringEnd : Nat -> String stringEnd hashtag = "\"" ++ replicate hashtag '#' +multilineBegin : Lexer +multilineBegin = many (is '#') <+> (exact "\"\"\"") <+> + manyUntil newline space <+> 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 @@ -271,15 +280,20 @@ 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 multilineEnd hashtag else stringEnd hashtag) in - match (someUntil (exact interpStart) (escapeLexer <|> stringLexer)) (\x => StringLit hashtag x) - <|> compose (exact interpStart) (const InterpBegin) (const ()) (\_ => rawTokens) (const $ is '}') (const InterpEnd) + match (someUntil (exact interpStart) (escapeLexer <|> charLexer)) (\x => StringLit hashtag x) + <|> compose (exact interpStart) + (const InterpBegin) + (const ()) + (\_ => rawTokens) + (const $ is '}') + (const InterpEnd) rawTokens : Tokenizer Token rawTokens = @@ -288,14 +302,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 multilineBegin + (const $ StringBegin True) + countHashtag + (stringTokens True) + (exact . multilineEnd) + (const StringEnd) + <|> compose stringBegin + (const $ StringBegin False) + countHashtag + (stringTokens False) + (\hashtag => exact (stringEnd hashtag) <+> reject (is '"')) + (const StringEnd) <|> match charLit (\x => CharLit (stripQuotes x)) <|> match dotIdent (\x => DotIdent (assert_total $ strTail x)) <|> match namespacedIdent parseNamespace @@ -312,7 +342,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 4bba932ee1..c61571428e 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 @@ -82,11 +83,28 @@ strLit StringLit n s => escape n s _ => Nothing) +||| String literal split by line wrap (not striped) before escaping the string. +export +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) + export strBegin : Rule () strBegin = terminal "Expected string begin" (\x => case x.val of - StringBegin => Just () + 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/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 8b3ad7159e..eadddbf2cd 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -124,7 +124,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..c5c12bd599 100644 --- a/tests/idris2/basic053/StringLiteral.idr +++ b/tests/idris2/basic053/StringLiteral.idr @@ -1,52 +1,68 @@ module StringLiteral -withWrap : String -withWrap = "foo -bar" +rawStr : String +rawStr = #""""""# -withNoWrap : String -withNoWrap = "foo \ -bar" +interp1 : String +interp1 = "Just 1 + Just 2 = \{ + show $ do a <- Just 1 + b <- Just 2 + Just (a + b) +}" -withIndent : String -withIndent = "foo - bar" +interp2 : String +interp2 = "hello\{ " " ++ ##"world\##{#"."#}"## }" -withEscape : String -withEscape = #""foo"\#n - \bar"# +multi1 : String +multi1 = """ + [project] + name: "project" + version: "0.1.0" + [deps] + "semver" = 0.2 + """ -withEscapeNoWrap : String -withEscapeNoWrap = #""foo" \# - \bar"# +multi2 : String +multi2 = #""" + a\# + b\n + \#{"c"} + """# -interp : String -interp = "\{withNoWrap}" +multi3 : String +multi3 = """ + \{"sticking"} \{"together"}\{ + ""}\{#""" +! -interp2 : String -interp2 = "hello\{ " " ++ ##"world\##{#"."#}"## }" +"""#} + """ -interp3 : String -interp3 = "Just 1 + Just 2 = \{ - show $ do a <- Just 1 - b <- Just 2 - Just (a + b) -}" +multi4 : String +multi4 = """ + 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 interp +test = do + putStrLn rawStr + putStrLn interp1 putStrLn interp2 - putStrLn interp3 let idris = "Idris" putStrLn "Hello \{idris ++ show 2}!" - putStrLn ##" + putStrLn multi1 + putStrLn multi2 + putStrLn multi3 + putStrLn multi4 + putStrLn """ + """ + putStrLn ##""" +a +"""## + putStrLn ##""" name: #"foo" version: "bar" -bzs: \#\'a\n\t\\'"## +bzs: \#\'a\n\t\\' +""" +"""## diff --git a/tests/idris2/basic053/expected b/tests/idris2/basic053/expected index 86887f9958..0ed41e4974 100644 --- a/tests/idris2/basic053/expected +++ b/tests/idris2/basic053/expected @@ -1,17 +1,24 @@ -foo -bar -foo bar -foo - bar -"foo" - - \bar -"foo" \bar -foo bar -hello world. +"""" Just 1 + Just 2 = Just 3 +hello world. Hello Idris2! +[project] +name: "project" +version: "0.1.0" +[deps] +"semver" = 0.2 +a b\n + c +sticking together! + +A very very + +very very very + +very long string. +a 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/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/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/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..d081e68e9e 100644 --- a/tests/idris2/perror007/expected +++ b/tests/idris2/perror007/expected @@ -1,24 +1,99 @@ -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: Bracket is not properly closed. + +StrError4.idr:2:7--2:8 + 1 | foo : String + 2 | foo = """""" + ^ + +1/1: Building StrError5 (StrError5.idr) +Error: While processing multi-line string. Line is less indented than the closing delimiter. + +StrError5.idr:3:1--4:5 + 3 | a + 4 | """ + +1/1: Building StrError6 (StrError6.idr) +Error: Bracket is not properly closed. + +StrError6.idr:2:7--2:8 + 1 | foo : String + 2 | foo = """a + ^ + +1/1: Building StrError7 (StrError7.idr) +Error: Bracket is not properly closed. + +StrError7.idr:2:7--2:8 + 1 | foo : String + 2 | foo = """a""" + ^ + +1/1: Building StrError8 (StrError8.idr) +Error: Bracket is not properly closed. + +StrError8.idr:2:7--2:8 + 1 | foo : String + 2 | foo = """\{"hello"} + ^ + +1/1: Building StrError9 (StrError9.idr) +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 + 2 | foo = """ + 3 | \{"hello"}""" + ^^^^^^^^^^ + +1/1: Building StrError10 (StrError10.idr) +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 + 2 | foo = """ + 3 | a""" + ^ + +1/1: Building StrError11 (StrError11.idr) +Error: Multi-line string is expected to begin with """. + +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. + +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 e9d6937ab5..c35e9dc600 100755 --- a/tests/idris2/perror007/run +++ b/tests/idris2/perror007/run @@ -1,5 +1,14 @@ -$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 +$1 --no-color --console-width 0 --check StrError11.idr || true +$1 --no-color --console-width 0 --check StrError12.idr || true rm -rf build