{-| Module : Idris.ModeCommon Description : Common utilities used by all modes. License : BSD3 Maintainer : The Idris Community. -} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} {-# OPTIONS_GHC -fwarn-unused-binds #-} {-# OPTIONS_GHC -fwarn-unused-imports #-} module Idris.ModeCommon (banner, defaultPort, loadInputs, warranty) where import Idris.AbsSyntax import Idris.Chaser import Idris.Core.TT import Idris.Delaborate import Idris.Erasure import Idris.Error import Idris.IBC import Idris.Imports import Idris.Info import Idris.Options import Idris.Output import Idris.Parser hiding (indent) import IRTS.Exports import Prelude hiding (id, (.), (<$>)) import Control.Category import Control.DeepSeq import Control.Monad import Network.Socket (PortNumber) defaultPort :: PortNumber defaultPort = fromIntegral 4294 loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath] loadInputs inputs toline -- furthest line to read in input source files = idrisCatch (do ist <- getIState -- if we're in --check and not outputting anything, don't bother -- loading, as it gets really slow if there's lots of modules in -- a package (instead, reload all at the end to check for -- consistency only) opts <- getCmdLine let loadCode = case opt getOutput opts of [] -> not (NoREPL `elem` opts) _ -> True logParser 3 $ show "loadInputs loadCode" ++ show loadCode -- For each ifile list, check it and build ibcs in the same clean IState -- so that they don't interfere with each other when checking importlists <- getImports [] inputs logParser 1 (show (map (\(i,m) -> (i, map import_path m)) importlists)) let ninputs = zip [1..] inputs ifiles <- mapWhileOK (\(num, input) -> do putIState ist logParser 3 $ show "loadInputs (num, input)" ++ show (num, input) modTree <- buildTree (map snd (take (num-1) ninputs)) importlists input let ifiles = getModuleFiles modTree logParser 2 ("MODULE TREE : " ++ show modTree) logParser 2 ("RELOAD: " ++ show ifiles) when (not (all ibc ifiles) || loadCode) $ tryLoad False IBC_Building (filter (not . ibc) ifiles) -- return the files that need rechecking return (input, ifiles)) ninputs inew <- getIState let tidata = idris_tyinfodata inew -- If it worked, load the whole thing from all the ibcs together case errSpan inew of Nothing -> do putIState $!! ist { idris_tyinfodata = tidata } logParser 3 $ "loadInputs ifiles" ++ show ifiles let fileToIFileType :: FilePath -> Idris IFileType fileToIFileType file = do ibcsd <- valIBCSubDir ist ids <- rankedImportDirs file findImport ids ibcsd file ibcfiles <- mapM fileToIFileType inputs logParser 3 $ show "loadInputs ibcfiles" ++ show ibcfiles tryLoad True (IBC_REPL True) ibcfiles _ -> return () exports <- findExports case opt getOutput opts of [] -> performUsageAnalysis (getExpNames exports) -- interactive _ -> return [] -- batch, will be checked by the compiler return (map fst ifiles)) (\e -> do i <- getIState case e of At f e' -> do setErrSpan f iWarn f $ pprintErr i e' ProgramLineComment -> return () -- fail elsewhere _ -> do setErrSpan emptyFC -- FIXME! Propagate it -- Issue #1576 on the issue tracker. -- https://github.com/idris-lang/Idris-dev/issues/1576 iWarn emptyFC $ pprintErr i e return []) where -- load all files, stop if any fail tryLoad :: Bool -> IBCPhase -> [IFileType] -> Idris () tryLoad keepstate phase [] = warnTotality >> return () tryLoad keepstate phase (f : fs) = do ist <- getIState logParser 3 $ "tryLoad (keepstate, phase, f : fs)" ++ show (keepstate, phase, f : fs) let maxline = case toline of Nothing -> Nothing Just l -> case f of IDR fn -> if any (fmatch fn) inputs then Just l else Nothing LIDR fn -> if any (fmatch fn) inputs then Just l else Nothing _ -> Nothing loadFromIFile True phase f maxline inew <- getIState -- FIXME: Save these in IBC to avoid this hack! Need to -- preserve it all from source inputs -- -- Issue #1577 on the issue tracker. -- https://github.com/idris-lang/Idris-dev/issues/1577 let tidata = idris_tyinfodata inew let patdefs = idris_patdefs inew ok <- noErrors if ok then -- The $!! here prevents a space leak on reloading. -- This isn't a solution - but it's a temporary stopgap. -- See issue #2386 do when (not keepstate) $ putIState $!! ist ist <- getIState putIState $!! ist { idris_tyinfodata = tidata, idris_patdefs = patdefs } tryLoad keepstate phase fs else warnTotality ibc (IBC _ _) = True ibc _ = False fmatch ('.':'/':xs) ys = fmatch xs ys fmatch xs ('.':'/':ys) = fmatch xs ys fmatch xs ys = xs == ys -- Like mapM, but give up when there's an error mapWhileOK f [] = return [] mapWhileOK f (x : xs) = do x' <- f x ok <- noErrors if ok then do xs' <- mapWhileOK f xs return (x' : xs') else return [x'] banner = " ____ __ _ \n" ++ " / _/___/ /____(_)____ \n" ++ " / // __ / ___/ / ___/ Version " ++ getIdrisVersion ++ "\n" ++ " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++ " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++ "\n" ++ "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++ "For details type :warranty." warranty = "\n" ++ "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" ++ "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" ++ "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" ++ "\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" ++ "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" ++ "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" ++ "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" ++ "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++ "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" ++ "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++ "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"