@@ -55,7 +55,7 @@ import Data.Maybe
5555import Data.Ord
5656import qualified Data.Set as S
5757import qualified Data.Text as T
58−import qualified System.Directory as Dir (makeAbsolute)
58+import qualified System.Directory as Dir (makeAbsolute, getModificationTime, doesFileExist)
5959import System.FilePath
6060import Text.Megaparsec ((<?>))
6161import qualified Text.Megaparsec as P
@@ -1640,162 +1640,196 @@ loadSource' lidr r maxline
16401640{-| Load Idris source code-}
16411641loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
16421642loadSource lidr f toline
1643− = do logParser 1 ("Reading " ++ f)
1644− iReport 2 ("Reading " ++ f)
1645− i <- getIState
1646− let def_total = default_total i
1647− file_in <- runIO $ readSource f
1648− file <- if lidr then tclift $ unlit f file_in else return file_in
1649− (mdocs, mname, imports_in, pos) <- parseImports f file
1650− ai <- getAutoImports
1651− let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1652− ids <- rankedImportDirs f
1653− ibcsd <- valIBCSubDir i
1654− mapM_ (\(re, f, ns, nfc) ->
1655− do fp <- findImport ids ibcsd f
1656− case fp of
1657− LIDR fn -> ifail $ "No ibc for " ++ f
1658− IDR fn -> ifail $ "No ibc for " ++ f
1659− IBC fn src ->
1660− do loadIBC True IBC_Building fn
1661− let srcFn = case src of
1662− IDR fn -> Just fn
1663− LIDR fn -> Just fn
1664− _ -> Nothing
1665− srcFnAbs <- case srcFn of
1666− Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1667− Nothing -> return Nothing
1668− sendHighlighting $ S.fromList [(FC' nfc, AnnNamespace ns srcFnAbs)])
1669− [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1670− reportParserWarnings
1671− sendParserHighlighting
1672−
1673− -- process and check module aliases
1674− let modAliases = M.fromList
1675− [ (prep alias, prep realName)
1676− | ImportInfo { import_reexport = reexport
1677− , import_path = realName
1678− , import_rename = Just (alias, _)
1679− , import_location = fc } <- imports
1680− ]
1681− prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1682− aliasNames = [ (alias, fc)
1683− | ImportInfo { import_rename = Just (alias, fc)
1684− } <- imports
1685− ]
1686− histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1687− case map head . filter ((/= 1) . length) $ histogram of
1688− [] -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)
1689− (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1690−
1691− i <- getIState
1692− putIState (i { default_access = Private, module_aliases = modAliases })
1693− clearIBC -- start a new .ibc file
1694− -- record package info in .ibc
1695− imps <- allImportDirs
1696− mapM_ addIBC (map IBCImportDir imps)
1697− mapM_ (addIBC . IBCImport)
1698− [ (reexport, realName)
1643+ = do logParser 1 ("Reading " ++ f)
1644+ iReport 2 ("Reading " ++ f)
1645+ i <- getIState
1646+ let def_total = default_total i
1647+ file_in <- runIO $ readSource f
1648+ file <- if lidr then tclift $ unlit f file_in else return file_in
1649+ (mdocs, mname, imports_in, pos) <- parseImports f file
1650+ ai <- getAutoImports
1651+ let imports = map (\n -> ImportInfo True n Nothing [] NoFC NoFC) ai ++ imports_in
1652+ ids <- rankedImportDirs f
1653+ ibcsd <- valIBCSubDir i
1654+ let ibc = ibcPathNoFallback ibcsd f
1655+ impHashes <- idrisCatch (getImportHashes ibc)
1656+ (\err -> return [])
1657+ newHashes <- mapM (\ (_, f, _, _) ->
1658+ do fp <- findImport ids ibcsd f
1659+ case fp of
1660+ IBC fn src ->
1661+ idrisCatch (do hash <- getIBCHash fn
1662+ return (Just (fn, hash)))
1663+ (\err -> return Nothing)
1664+ _ -> return Nothing)
1665+ [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1666+
1667+ fmod <- liftIO $ Dir.getModificationTime f
1668+ ibcexists <- liftIO $ Dir.doesFileExist ibc
1669+ ibcmod <- if ibcexists
1670+ then liftIO $ Dir.getModificationTime ibc
1671+ else return fmod
1672+
1673+ logParser 10 $ ibc ++ " " ++ show ibcmod
1674+ logParser 10 $ f ++ " " ++ show fmod
1675+ logParser 10 $ show impHashes ++ "\n" ++ show newHashes
1676+
1677+ -- If the ibc is newer than the source, and the old import
1678+ -- hashes are the same as the ones we've just read,
1679+ -- quit and just load the IBC
1680+
1681+ let needLoad = (ibcmod <= fmod) ||
1682+ (sort impHashes /= sort (mapMaybe id newHashes))
1683+
1684+ if not needLoad
1685+ then iReport 1 $ "Loading " ++ f
1686+ else do
1687+ mapM_ (\ (re, f, ns, nfc) ->
1688+ do fp <- findImport ids ibcsd f
1689+ case fp of
1690+ LIDR fn -> ifail $ "No ibc for " ++ f
1691+ IDR fn -> ifail $ "No ibc for " ++ f
1692+ IBC fn src ->
1693+ do loadIBC True IBC_Building fn
1694+ let srcFn = case src of
1695+ IDR fn -> Just fn
1696+ LIDR fn -> Just fn
1697+ _ -> Nothing
1698+ srcFnAbs <- case srcFn of
1699+ Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)
1700+ Nothing -> return Nothing
1701+ sendHighlighting $ S.fromList [(FC' nfc, AnnNamespace ns srcFnAbs)])
1702+ [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
1703+ reportParserWarnings
1704+ sendParserHighlighting
1705+
1706+ -- process and check module aliases
1707+ let modAliases = M.fromList
1708+ [ (prep alias, prep realName)
16991709 | ImportInfo { import_reexport = reexport
17001710 , import_path = realName
1701− } <- imports
1711+ , import_rename = Just (alias, _)
1712+ , import_location = fc } <- imports
17021713 ]
1703− let syntax = defaultSyntax{ syn_namespace = reverse mname,
1704− maxline = toline }
1705− ist <- getIState
1706− -- Save the span from parsing the module header, because
1707− -- an empty program parse might obliterate it.
1708− let oldSpan = idris_parsedSpan ist
1709− ds' <- parseProg syntax f file pos
1710−
1711− case (ds', oldSpan) of
1712− ([], Just fc) ->
1713− -- If no program elements were parsed, we dind't
1714− -- get a loaded region in the IBC file. That
1715− -- means we need to add it back.
1716− do ist <- getIState
1717− putIState ist { idris_parsedSpan = oldSpan
1718− , ibc_write = IBCParsedRegion fc :
1719− ibc_write ist
1720− }
1721− _ -> return ()
1722− sendParserHighlighting
1723−
1724− -- Parsing done, now process declarations
1725−
1726− let ds = namespaces mname ds'
1727− logParser 3 (show $ showDecls verbosePPOption ds)
1728− i <- getIState
1729− logLvl 10 (show (toAlist (idris_implicits i)))
1730− logLvl 3 (show (idris_infixes i))
1731− -- Now add all the declarations to the context
1732− iReport 1 $ "Type checking " ++ f
1733− -- we totality check after every Mutual block, so if
1734− -- anything is a single definition, wrap it in a
1735− -- mutual block on its own
1736− elabDecls (toplevelWith f) (map toMutual ds)
1737− i <- getIState
1738− -- simplify every definition do give the totality checker
1739− -- a better chance
1740− mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1741− ctxt' <-
1742− do ctxt <- getContext
1743− tclift $ simplifyCasedef n [] [] (getErasureInfo i) ctxt
1744− setContext ctxt')
1745− (map snd (idris_totcheck i))
1746− -- build size change graph from simplified definitions
1747− iReport 3 $ "Totality checking " ++ f
1748− logLvl 1 $ "Totality checking " ++ f
1749− i <- getIState
1750− mapM_ buildSCG (idris_totcheck i)
1751− mapM_ checkDeclTotality (idris_totcheck i)
1752− mapM_ verifyTotality (idris_totcheck i)
1753−
1754− -- Redo totality check for deferred names
1755− let deftots = idris_defertotcheck i
1756− logLvl 2 $ "Totality checking " ++ show deftots
1757− mapM_ (\x -> do tot <- getTotality x
1758− case tot of
1759− Total _ ->
1760− do let opts = case lookupCtxtExact x (idris_flags i) of
1761− Just os -> os
1762− Nothing -> []
1763− when (AssertTotal `notElem` opts) $
1764− setTotality x Unchecked
1765− _ -> return ()) (map snd deftots)
1766− mapM_ buildSCG deftots
1767− mapM_ checkDeclTotality deftots
1768−
1769− logLvl 1 ("Finished " ++ f)
1770− ibcsd <- valIBCSubDir i
1771− logLvl 1 $ "Universe checking " ++ f
1772− iReport 3 $ "Universe checking " ++ f
1773− iucheck
1774− let ibc = ibcPathNoFallback ibcsd f
1775− i <- getIState
1776− addHides (hide_list i)
1777−
1778− -- Save module documentation if applicable
1779− i <- getIState
1780− case mdocs of
1781− Nothing -> return ()
1782− Just docs -> addModDoc syntax mname docs
1783−
1784−
1785− -- Finally, write an ibc and highlights if checking was successful
1786− ok <- noErrors
1787− when ok $
1788− do idrisCatch (do writeIBC f ibc; clearIBC)
1789− (\c -> return ()) -- failure is harmless
1790− hl <- getDumpHighlighting
1791− when hl $
1792− idrisCatch (writeHighlights f)
1793− (const $ return ()) -- failure is harmless
1794− clearHighlights
1795− i <- getIState
1796− putIState (i { default_total = def_total,
1797− hide_list = emptyContext })
1798− return ()
1714+ prep = map T.pack . reverse . Spl.splitOn [pathSeparator]
1715+ aliasNames = [ (alias, fc)
1716+ | ImportInfo { import_rename = Just (alias, fc)
1717+ } <- imports
1718+ ]
1719+ histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames
1720+ case map head . filter ((/= 1) . length) $ histogram of
1721+ [] -> logParser 3 $ "Module aliases: " ++ show (M.toList modAliases)
1722+ (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n
1723+
1724+ i <- getIState
1725+ putIState (i { default_access = Private, module_aliases = modAliases })
1726+ clearIBC -- start a new .ibc file
1727+ mapM_ addIBC (map (\ (f, h) -> IBCImportHash f h)
1728+ (mapMaybe id newHashes))
1729+ -- record package info in .ibc
1730+ imps <- allImportDirs
1731+ mapM_ addIBC (map IBCImportDir imps)
1732+ mapM_ (addIBC . IBCImport)
1733+ [ (reexport, realName)
1734+ | ImportInfo { import_reexport = reexport
1735+ , import_path = realName
1736+ } <- imports
1737+ ]
1738+ let syntax = defaultSyntax{ syn_namespace = reverse mname,
1739+ maxline = toline }
1740+ ist <- getIState
1741+ -- Save the span from parsing the module header, because
1742+ -- an empty program parse might obliterate it.
1743+ let oldSpan = idris_parsedSpan ist
1744+ ds' <- parseProg syntax f file pos
1745+
1746+ case (ds', oldSpan) of
1747+ ([], Just fc) ->
1748+ -- If no program elements were parsed, we dind't
1749+ -- get a loaded region in the IBC file. That
1750+ -- means we need to add it back.
1751+ do ist <- getIState
1752+ putIState ist { idris_parsedSpan = oldSpan
1753+ , ibc_write = IBCParsedRegion fc :
1754+ ibc_write ist
1755+ }
1756+ _ -> return ()
1757+ sendParserHighlighting
1758+
1759+ -- Parsing done, now process declarations
1760+
1761+ let ds = namespaces mname ds'
1762+ logParser 3 (show $ showDecls verbosePPOption ds)
1763+ i <- getIState
1764+ logLvl 10 (show (toAlist (idris_implicits i)))
1765+ logLvl 3 (show (idris_infixes i))
1766+ -- Now add all the declarations to the context
1767+ iReport 1 $ "Type checking " ++ f
1768+ -- we totality check after every Mutual block, so if
1769+ -- anything is a single definition, wrap it in a
1770+ -- mutual block on its own
1771+ elabDecls (toplevelWith f) (map toMutual ds)
1772+ i <- getIState
1773+ -- simplify every definition do give the totality checker
1774+ -- a better chance
1775+ mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1776+ ctxt' <-
1777+ do ctxt <- getContext
1778+ tclift $ simplifyCasedef n [] [] (getErasureInfo i) ctxt
1779+ setContext ctxt')
1780+ (map snd (idris_totcheck i))
1781+ -- build size change graph from simplified definitions
1782+ iReport 3 $ "Totality checking " ++ f
1783+ logLvl 1 $ "Totality checking " ++ f
1784+ i <- getIState
1785+ mapM_ buildSCG (idris_totcheck i)
1786+ mapM_ checkDeclTotality (idris_totcheck i)
1787+ mapM_ verifyTotality (idris_totcheck i)
1788+
1789+ -- Redo totality check for deferred names
1790+ let deftots = idris_defertotcheck i
1791+ logLvl 2 $ "Totality checking " ++ show deftots
1792+ mapM_ (\x -> do tot <- getTotality x
1793+ case tot of
1794+ Total _ ->
1795+ do let opts = case lookupCtxtExact x (idris_flags i) of
1796+ Just os -> os
1797+ Nothing -> []
1798+ when (AssertTotal `notElem` opts) $
1799+ setTotality x Unchecked
1800+ _ -> return ()) (map snd deftots)
1801+ mapM_ buildSCG deftots
1802+ mapM_ checkDeclTotality deftots
1803+
1804+ logLvl 1 ("Finished " ++ f)
1805+ ibcsd <- valIBCSubDir i
1806+ logLvl 1 $ "Universe checking " ++ f
1807+ iReport 3 $ "Universe checking " ++ f
1808+ iucheck
1809+ i <- getIState
1810+ addHides (hide_list i)
1811+
1812+ -- Save module documentation if applicable
1813+ i <- getIState
1814+ case mdocs of
1815+ Nothing -> return ()
1816+ Just docs -> addModDoc syntax mname docs
1817+
1818+
1819+ -- Finally, write an ibc and highlights if checking was successful
1820+ ok <- noErrors
1821+ when ok $
1822+ do idrisCatch (do writeIBC f ibc; clearIBC)
1823+ (\c -> return ()) -- failure is harmless
1824+ hl <- getDumpHighlighting
1825+ when hl $
1826+ idrisCatch (writeHighlights f)
1827+ (const $ return ()) -- failure is harmless
1828+ clearHighlights
1829+ i <- getIState
1830+ putIState (i { default_total = def_total,
1831+ hide_list = emptyContext })
1832+ return ()
17991833 where
18001834 namespaces :: [String] -> [PDecl] -> [PDecl]
18011835 namespaces [] ds = ds