git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/ModeCommon.hs
188 lines 9.0 kB history raw
1{-|
2Module : Idris.ModeCommon
3Description : Common utilities used by all modes.
4License : BSD3
5Maintainer : The Idris Community.
6-}
7module Idris.ModeCommon where
9import Idris.AbsSyntax
10import Idris.Chaser
11import Idris.Core.TT
12import Idris.Delaborate
13import Idris.Erasure
14import Idris.Error
15import Idris.IBC
16import Idris.Imports
17import Idris.Info
18import Idris.Options
19import Idris.Output
20import Idris.Parser hiding (indent)
21import IRTS.Exports
23import Prelude hiding (id, (.), (<$>))
25import Control.Category
26import Control.DeepSeq
27import Control.Monad
28import Control.Monad.Trans.State.Strict (get)
29import Data.List hiding (group)
30import Data.Maybe
31import Network.Socket (PortNumber)
32import System.Directory
34defaultPort :: PortNumber
35defaultPort = fromIntegral 4294
38loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
39loadInputs inputs toline -- furthest line to read in input source files
40 = idrisCatch
41 (do ist <- getIState
42 -- if we're in --check and not outputting anything, don't bother
43 -- loading, as it gets really slow if there's lots of modules in
44 -- a package (instead, reload all at the end to check for
45 -- consistency only)
46 opts <- getCmdLine
48 let loadCode = case opt getOutput opts of
49 [] -> not (NoREPL `elem` opts)
50 _ -> True
52 -- For each ifile list, check it and build ibcs in the same clean IState
53 -- so that they don't interfere with each other when checking
55 importlists <- getImports [] inputs
57 logParser 1 (show (map (\(i,m) -> (i, map import_path m)) importlists))
59 let ninputs = zip [1..] inputs
60 ifiles <- mapWhileOK (\(num, input) ->
61 do putIState ist
62 modTree <- buildTree
63 (map snd (take (num-1) ninputs))
64 importlists
65 input
66 let ifiles = getModuleFiles modTree
67 logParser 1 ("MODULE TREE : " ++ show modTree)
68 logParser 1 ("RELOAD: " ++ show ifiles)
69 when (not (all ibc ifiles) || loadCode) $
70 tryLoad False IBC_Building (filter (not . ibc) ifiles)
71 -- return the files that need rechecking
72 return (input, ifiles))
73 ninputs
74 inew <- getIState
75 let tidata = idris_tyinfodata inew
76 -- If it worked, load the whole thing from all the ibcs together
77 case errSpan inew of
78 Nothing ->
79 do putIState $!! ist { idris_tyinfodata = tidata }
80 ibcfiles <- mapM findNewIBC (nub (concatMap snd ifiles))
81-- logLvl 0 $ "Loading from " ++ show ibcfiles
82 tryLoad True (IBC_REPL True) (mapMaybe id ibcfiles)
83 _ -> return ()
84 exports <- findExports
86 case opt getOutput opts of
87 [] -> performUsageAnalysis (getExpNames exports) -- interactive
88 _ -> return [] -- batch, will be checked by the compiler
90 return (map fst ifiles))
91 (\e -> do i <- getIState
92 case e of
93 At f e' -> do setErrSpan f
94 iWarn f $ pprintErr i e'
95 ProgramLineComment -> return () -- fail elsewhere
96 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
97 -- Issue #1576 on the issue tracker.
98 -- https://github.com/idris-lang/Idris-dev/issues/1576
99 iWarn emptyFC $ pprintErr i e
100 return [])
101 where -- load all files, stop if any fail
102 tryLoad :: Bool -> IBCPhase -> [IFileType] -> Idris ()
103 tryLoad keepstate phase [] = warnTotality >> return ()
104 tryLoad keepstate phase (f : fs)
105 = do ist <- getIState
106 let maxline
107 = case toline of
108 Nothing -> Nothing
109 Just l -> case f of
110 IDR fn -> if any (fmatch fn) inputs
111 then Just l
112 else Nothing
113 LIDR fn -> if any (fmatch fn) inputs
114 then Just l
115 else Nothing
116 _ -> Nothing
117 loadFromIFile True phase f maxline
118 inew <- getIState
119 -- FIXME: Save these in IBC to avoid this hack! Need to
120 -- preserve it all from source inputs
121 --
122 -- Issue #1577 on the issue tracker.
123 -- https://github.com/idris-lang/Idris-dev/issues/1577
124 let tidata = idris_tyinfodata inew
125 let patdefs = idris_patdefs inew
126 ok <- noErrors
127 if ok then
128 -- The $!! here prevents a space leak on reloading.
129 -- This isn't a solution - but it's a temporary stopgap.
130 -- See issue #2386
131 do when (not keepstate) $ putIState $!! ist
132 ist <- getIState
133 putIState $!! ist { idris_tyinfodata = tidata,
134 idris_patdefs = patdefs }
135 tryLoad keepstate phase fs
136 else warnTotality
138 ibc (IBC _ _) = True
139 ibc _ = False
141 fmatch ('.':'/':xs) ys = fmatch xs ys
142 fmatch xs ('.':'/':ys) = fmatch xs ys
143 fmatch xs ys = xs == ys
145 findNewIBC :: IFileType -> Idris (Maybe IFileType)
146 findNewIBC i@(IBC _ _) = return (Just i)
147 findNewIBC s@(IDR f) = do ist <- get
148 ibcsd <- valIBCSubDir ist
149 let ibc = ibcPathNoFallback ibcsd f
150 ok <- runIO $ doesFileExist ibc
151 if ok then return (Just (IBC ibc s))
152 else return Nothing
153 findNewIBC s@(LIDR f) = do ist <- get
154 ibcsd <- valIBCSubDir ist
155 let ibc = ibcPathNoFallback ibcsd f
156 ok <- runIO $ doesFileExist ibc
157 if ok then return (Just (IBC ibc s))
158 else return Nothing
160 -- Like mapM, but give up when there's an error
161 mapWhileOK f [] = return []
162 mapWhileOK f (x : xs) = do x' <- f x
163 ok <- noErrors
164 if ok then do xs' <- mapWhileOK f xs
165 return (x' : xs')
166 else return [x']
168banner = " ____ __ _ \n" ++
169 " / _/___/ /____(_)____ \n" ++
170 " / // __ / ___/ / ___/ Version " ++ getIdrisVersion ++ "\n" ++
171 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
172 " /___/\\__,_/_/ /_/____/ Type :? for help \n" ++
173 "\n" ++
174 "Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++
175 "For details type :warranty."
177warranty = "\n" ++
178 "\t THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY \n" ++
179 "\t EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE \n" ++
180 "\t IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR \n" ++
181 "\t PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE \n" ++
182 "\t LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR \n" ++
183 "\t CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF \n" ++
184 "\t SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR \n" ++
185 "\t BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, \n" ++
186 "\t WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE \n" ++
187 "\t OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN\n" ++
188 "\t IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.\n"