git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/src/Idris/ModeCommon.hs
187 lines 8.8 kB history raw
1{-|
2Module : Idris.ModeCommon
3Description : Common utilities used by all modes.
4License : BSD3
5Maintainer : The Idris Community.
6-}
8{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
9{-# OPTIONS_GHC -fwarn-unused-binds #-}
10{-# OPTIONS_GHC -fwarn-unused-imports #-}
12module Idris.ModeCommon (banner, defaultPort, loadInputs, warranty) where
14import Idris.AbsSyntax
15import Idris.Chaser
16import Idris.Core.TT
17import Idris.Delaborate
18import Idris.Erasure
19import Idris.Error
20import Idris.IBC
21import Idris.Imports
22import Idris.Info
23import Idris.Options
24import Idris.Output
25import Idris.Parser hiding (indent)
26import IRTS.Exports
28import Prelude hiding (id, (.), (<$>))
30import Control.Category
31import Control.DeepSeq
32import Control.Monad
33import Network.Socket (PortNumber)
35defaultPort :: PortNumber
36defaultPort = 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 logParser 3 $ show "loadInputs loadCode" ++ show loadCode
54 -- For each ifile list, check it and build ibcs in the same clean IState
55 -- so that they don't interfere with each other when checking
57 importlists <- getImports [] inputs
59 logParser 1 (show (map (\(i,m) -> (i, map import_path m)) importlists))
61 let ninputs = zip [1..] inputs
62 ifiles <- mapWhileOK (\(num, input) ->
63 do putIState ist
64 logParser 3 $ show "loadInputs (num, input)" ++ show (num, input)
65 modTree <- buildTree
66 (map snd (take (num-1) ninputs))
67 importlists
68 input
69 let ifiles = getModuleFiles modTree
70 logParser 1 ("MODULE TREE : " ++ show modTree)
71 logParser 1 ("RELOAD: " ++ show ifiles)
72 when (not (all ibc ifiles) || loadCode) $
73 tryLoad False IBC_Building (filter (not . ibc) ifiles)
74 -- return the files that need rechecking
75 return (input, ifiles))
76 ninputs
77 inew <- getIState
78 let tidata = idris_tyinfodata inew
79 -- If it worked, load the whole thing from all the ibcs together
80 case errSpan inew of
81 Nothing ->
82 do putIState $!! ist { idris_tyinfodata = tidata }
83 logParser 3 $ "loadInputs ifiles" ++ show ifiles
85 let fileToIFileType :: FilePath -> Idris IFileType
86 fileToIFileType file = do
87 ibcsd <- valIBCSubDir ist
88 ids <- rankedImportDirs file
89 findImport ids ibcsd file
91 ibcfiles <- mapM fileToIFileType inputs
92 logParser 3 $ show "loadInputs ibcfiles" ++ show ibcfiles
94 tryLoad True (IBC_REPL True) ibcfiles
95 _ -> return ()
96 exports <- findExports
98 case opt getOutput opts of
99 [] -> performUsageAnalysis (getExpNames exports) -- interactive
100 _ -> return [] -- batch, will be checked by the compiler
102 return (map fst ifiles))
103 (\e -> do i <- getIState
104 case e of
105 At f e' -> do setErrSpan f
106 iWarn f $ pprintErr i e'
107 ProgramLineComment -> return () -- fail elsewhere
108 _ -> do setErrSpan emptyFC -- FIXME! Propagate it
109 -- Issue #1576 on the issue tracker.
110 -- https://github.com/idris-lang/Idris-dev/issues/1576
111 iWarn emptyFC $ pprintErr i e
112 return [])
113 where -- load all files, stop if any fail
114 tryLoad :: Bool -> IBCPhase -> [IFileType] -> Idris ()
115 tryLoad keepstate phase [] = warnTotality >> return ()
116 tryLoad keepstate phase (f : fs)
117 = do ist <- getIState
118 logParser 3 $ "tryLoad (keepstate, phase, f : fs)" ++
119 show (keepstate, phase, f : fs)
120 let maxline
121 = case toline of
122 Nothing -> Nothing
123 Just l -> case f of
124 IDR fn -> if any (fmatch fn) inputs
125 then Just l
126 else Nothing
127 LIDR fn -> if any (fmatch fn) inputs
128 then Just l
129 else Nothing
130 _ -> Nothing
131 loadFromIFile True phase f maxline
132 inew <- getIState
133 -- FIXME: Save these in IBC to avoid this hack! Need to
134 -- preserve it all from source inputs
135 --
136 -- Issue #1577 on the issue tracker.
137 -- https://github.com/idris-lang/Idris-dev/issues/1577
138 let tidata = idris_tyinfodata inew
139 let patdefs = idris_patdefs inew
140 ok <- noErrors
141 if ok then
142 -- The $!! here prevents a space leak on reloading.
143 -- This isn't a solution - but it's a temporary stopgap.
144 -- See issue #2386
145 do when (not keepstate) $ putIState $!! ist
146 ist <- getIState
147 putIState $!! ist { idris_tyinfodata = tidata,
148 idris_patdefs = patdefs }
149 tryLoad keepstate phase fs
150 else warnTotality
152 ibc (IBC _ _) = True
153 ibc _ = False
155 fmatch ('.':'/':xs) ys = fmatch xs ys
156 fmatch xs ('.':'/':ys) = fmatch xs ys
157 fmatch xs ys = xs == ys
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"