Merge pull request #1097 from andylokandy/multiline

Implement multi-line string

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

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

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 '\\' = ("\\\\" ++)

src/Core/Core.idr

@@ -147,6 +147,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
@@ -313,6 +314,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" ++
@@ -390,6 +392,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

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, [])

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,21 +414,71 @@ 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 (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
 
       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} ->

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))
 

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

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)
 

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

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)