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