{-# LANGUAGE CPP #-}
module Agda.Interaction.Imports where
import Prelude hiding (null)
import Control.Arrow
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Maybe
import qualified Control.Exception as E
import qualified Data.Map as Map
import qualified Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Maybe
import Data.Monoid (mempty, mappend)
import Data.Map (Map)
import qualified Data.HashMap.Strict as HMap
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as T
import System.Directory (doesFileExist, getModificationTime, removeFile)
import System.FilePath ((</>))
import Agda.Benchmarking
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Syntax.Parser
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Rewriting.Confluence ( checkConfluenceOfRules )
import Agda.TypeChecking.MetaVars ( openMetasToPostulates )
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Serialise
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Pretty as P
import Agda.TypeChecking.DeadCode
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TheTypeChecker
import Agda.Interaction.BasicOps (getGoals, showGoals)
import Agda.Interaction.FindFile
import Agda.Interaction.Highlighting.Generate
import Agda.Interaction.Highlighting.Precise ( compress )
import Agda.Interaction.Highlighting.Vim
import Agda.Interaction.Options
import qualified Agda.Interaction.Options.Lenses as Lens
import Agda.Interaction.Response
(RemoveTokenBasedHighlighting(KeepHighlighting))
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.IO.Binary
import Agda.Utils.Pretty hiding (Mode)
import Agda.Utils.Hash
import qualified Agda.Utils.Trie as Trie
import Agda.Utils.Impossible
data SourceInfo = SourceInfo
{ SourceInfo -> Text
siSource :: Text
, SourceInfo -> FileType
siFileType :: FileType
, SourceInfo -> Module
siModule :: C.Module
, SourceInfo -> TopLevelModuleName
siModuleName :: C.TopLevelModuleName
}
sourceInfo :: SourceFile -> TCM SourceInfo
sourceInfo :: SourceFile -> TCM SourceInfo
sourceInfo (SourceFile f :: AbsolutePath
f) = Account Phase -> TCM SourceInfo -> TCM SourceInfo
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Parsing] (TCM SourceInfo -> TCM SourceInfo)
-> TCM SourceInfo -> TCM SourceInfo
forall a b. (a -> b) -> a -> b
$ do
Text
source <- PM Text -> TCM Text
forall a. PM a -> TCM a
runPM (PM Text -> TCM Text) -> PM Text -> TCM Text
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> PM Text
readFilePM AbsolutePath
f
(parsedMod :: Module
parsedMod, fileType :: FileType
fileType) <- PM (Module, FileType) -> TCM (Module, FileType)
forall a. PM a -> TCM a
runPM (PM (Module, FileType) -> TCM (Module, FileType))
-> PM (Module, FileType) -> TCM (Module, FileType)
forall a b. (a -> b) -> a -> b
$
Parser Module -> AbsolutePath -> String -> PM (Module, FileType)
forall a.
Show a =>
Parser a -> AbsolutePath -> String -> PM (a, FileType)
parseFile Parser Module
moduleParser AbsolutePath
f (String -> PM (Module, FileType))
-> String -> PM (Module, FileType)
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
source
TopLevelModuleName
moduleName <- AbsolutePath -> Module -> TCM TopLevelModuleName
moduleName AbsolutePath
f Module
parsedMod
SourceInfo -> TCM SourceInfo
forall (m :: * -> *) a. Monad m => a -> m a
return SourceInfo :: Text -> FileType -> Module -> TopLevelModuleName -> SourceInfo
SourceInfo
{ siSource :: Text
siSource = Text
source
, siFileType :: FileType
siFileType = FileType
fileType
, siModule :: Module
siModule = Module
parsedMod
, siModuleName :: TopLevelModuleName
siModuleName = TopLevelModuleName
moduleName
}
data Mode
= ScopeCheck
| TypeCheck
deriving (Mode -> Mode -> Bool
(Mode -> Mode -> Bool) -> (Mode -> Mode -> Bool) -> Eq Mode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Mode -> Mode -> Bool
$c/= :: Mode -> Mode -> Bool
== :: Mode -> Mode -> Bool
$c== :: Mode -> Mode -> Bool
Eq, Int -> Mode -> ShowS
[Mode] -> ShowS
Mode -> String
(Int -> Mode -> ShowS)
-> (Mode -> String) -> ([Mode] -> ShowS) -> Show Mode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Mode] -> ShowS
$cshowList :: [Mode] -> ShowS
show :: Mode -> String
$cshow :: Mode -> String
showsPrec :: Int -> Mode -> ShowS
$cshowsPrec :: Int -> Mode -> ShowS
Show)
data MainInterface
= MainInterface Mode
| NotMainInterface
deriving (MainInterface -> MainInterface -> Bool
(MainInterface -> MainInterface -> Bool)
-> (MainInterface -> MainInterface -> Bool) -> Eq MainInterface
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MainInterface -> MainInterface -> Bool
$c/= :: MainInterface -> MainInterface -> Bool
== :: MainInterface -> MainInterface -> Bool
$c== :: MainInterface -> MainInterface -> Bool
Eq, Int -> MainInterface -> ShowS
[MainInterface] -> ShowS
MainInterface -> String
(Int -> MainInterface -> ShowS)
-> (MainInterface -> String)
-> ([MainInterface] -> ShowS)
-> Show MainInterface
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MainInterface] -> ShowS
$cshowList :: [MainInterface] -> ShowS
show :: MainInterface -> String
$cshow :: MainInterface -> String
showsPrec :: Int -> MainInterface -> ShowS
$cshowsPrec :: Int -> MainInterface -> ShowS
Show)
includeStateChanges :: MainInterface -> Bool
includeStateChanges :: MainInterface -> Bool
includeStateChanges (MainInterface _) = Bool
True
includeStateChanges NotMainInterface = Bool
False
mergeInterface :: Interface -> TCM ()
mergeInterface :: Interface -> TCM ()
mergeInterface i :: Interface
i = do
let sig :: Signature
sig = Interface -> Signature
iSignature Interface
i
builtin :: [(String, Builtin (String, QName))]
builtin = Map String (Builtin (String, QName))
-> [(String, Builtin (String, QName))]
forall k a. Map k a -> [(k, a)]
Map.toList (Map String (Builtin (String, QName))
-> [(String, Builtin (String, QName))])
-> Map String (Builtin (String, QName))
-> [(String, Builtin (String, QName))]
forall a b. (a -> b) -> a -> b
$ Interface -> Map String (Builtin (String, QName))
iBuiltin Interface
i
prim :: [(String, QName)]
prim = [ (String, QName)
x | (_,Prim x :: (String, QName)
x) <- [(String, Builtin (String, QName))]
builtin ]
bi :: Map String (Builtin pf)
bi = [(String, Builtin pf)] -> Map String (Builtin pf)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (String
x,Term -> Builtin pf
forall pf. Term -> Builtin pf
Builtin Term
t) | (x :: String
x,Builtin t :: Term
t) <- [(String, Builtin (String, QName))]
builtin ]
warns :: [TCWarning]
warns = Interface -> [TCWarning]
iWarnings Interface
i
BuiltinThings PrimFun
bs <- (TCState -> BuiltinThings PrimFun)
-> TCMT IO (BuiltinThings PrimFun)
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> BuiltinThings PrimFun
stBuiltinThings
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.merge" 10 "Merging interface"
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.merge" 20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
" Current builtins " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show (BuiltinThings PrimFun -> [String]
forall k a. Map k a -> [k]
Map.keys BuiltinThings PrimFun
bs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
" New builtins " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show (Map String (Builtin Any) -> [String]
forall k a. Map k a -> [k]
Map.keys Map String (Builtin Any)
forall pf. Map String (Builtin pf)
bi)
let check :: String -> m ()
check b :: String
b = case (Builtin PrimFun
b1, Builtin Any
forall pf. Builtin pf
b2) of
(Builtin x :: Term
x, Builtin y :: Term
y)
| Term
x Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
y -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise -> TypeError -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ String -> Term -> Term -> TypeError
DuplicateBuiltinBinding String
b Term
x Term
y
_ -> m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
where
Just b1 :: Builtin PrimFun
b1 = String -> BuiltinThings PrimFun -> Maybe (Builtin PrimFun)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
b BuiltinThings PrimFun
bs
Just b2 :: Builtin pf
b2 = String -> Map String (Builtin pf) -> Maybe (Builtin pf)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
b Map String (Builtin pf)
forall pf. Map String (Builtin pf)
bi
(String -> TCM ()) -> [String] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> TCM ()
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m ()
check (((String, Builtin PrimFun) -> String)
-> [(String, Builtin PrimFun)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Builtin PrimFun) -> String
forall a b. (a, b) -> a
fst ([(String, Builtin PrimFun)] -> [String])
-> [(String, Builtin PrimFun)] -> [String]
forall a b. (a -> b) -> a -> b
$ BuiltinThings PrimFun -> [(String, Builtin PrimFun)]
forall k a. Map k a -> [(k, a)]
Map.toList (BuiltinThings PrimFun -> [(String, Builtin PrimFun)])
-> BuiltinThings PrimFun -> [(String, Builtin PrimFun)]
forall a b. (a -> b) -> a -> b
$ BuiltinThings PrimFun
-> Map String (Builtin Any) -> BuiltinThings PrimFun
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection BuiltinThings PrimFun
bs Map String (Builtin Any)
forall pf. Map String (Builtin pf)
bi)
Signature
-> BuiltinThings PrimFun
-> PatternSynDefns
-> DisplayForms
-> Map QName String
-> Set QName
-> [TCWarning]
-> TCM ()
addImportedThings Signature
sig BuiltinThings PrimFun
forall pf. Map String (Builtin pf)
bi (Interface -> PatternSynDefns
iPatternSyns Interface
i) (Interface -> DisplayForms
iDisplayForms Interface
i) (Interface -> Map QName String
iUserWarnings Interface
i) (Interface -> Set QName
iPartialDefs Interface
i) [TCWarning]
warns
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.merge" 20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
" Rebinding primitives " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, QName)] -> String
forall a. Show a => a -> String
show [(String, QName)]
prim
((String, QName) -> TCM ()) -> [(String, QName)] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String, QName) -> TCM ()
rebind [(String, QName)]
prim
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (PragmaOptions -> Bool
optConfluenceCheck (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.confluence" 20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ " Checking confluence of imported rewrite rules"
[RewriteRule] -> TCM ()
checkConfluenceOfRules ([RewriteRule] -> TCM ()) -> [RewriteRule] -> TCM ()
forall a b. (a -> b) -> a -> b
$ [[RewriteRule]] -> [RewriteRule]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[RewriteRule]] -> [RewriteRule])
-> [[RewriteRule]] -> [RewriteRule]
forall a b. (a -> b) -> a -> b
$ HashMap QName [RewriteRule] -> [[RewriteRule]]
forall k v. HashMap k v -> [v]
HMap.elems (HashMap QName [RewriteRule] -> [[RewriteRule]])
-> HashMap QName [RewriteRule] -> [[RewriteRule]]
forall a b. (a -> b) -> a -> b
$ Signature
sig Signature
-> Lens' (HashMap QName [RewriteRule]) Signature
-> HashMap QName [RewriteRule]
forall o i. o -> Lens' i o -> i
^. Lens' (HashMap QName [RewriteRule]) Signature
sigRewriteRules
where
rebind :: (String, QName) -> TCM ()
rebind (x :: String
x, q :: QName
q) = do
PrimImpl _ pf :: PrimFun
pf <- String -> TCM PrimitiveImpl
lookupPrimitiveFunction String
x
Lens' (BuiltinThings PrimFun) TCState
stImportedBuiltins Lens' (BuiltinThings PrimFun) TCState
-> (BuiltinThings PrimFun -> BuiltinThings PrimFun) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` String
-> Builtin PrimFun
-> BuiltinThings PrimFun
-> BuiltinThings PrimFun
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
x (PrimFun -> Builtin PrimFun
forall pf. pf -> Builtin pf
Prim PrimFun
pf{ primFunName :: QName
primFunName = QName
q })
addImportedThings
:: Signature
-> BuiltinThings PrimFun
-> A.PatternSynDefns
-> DisplayForms
-> Map A.QName String
-> Set QName
-> [TCWarning]
-> TCM ()
addImportedThings :: Signature
-> BuiltinThings PrimFun
-> PatternSynDefns
-> DisplayForms
-> Map QName String
-> Set QName
-> [TCWarning]
-> TCM ()
addImportedThings isig :: Signature
isig ibuiltin :: BuiltinThings PrimFun
ibuiltin patsyns :: PatternSynDefns
patsyns display :: DisplayForms
display userwarn :: Map QName String
userwarn partialdefs :: Set QName
partialdefs warnings :: [TCWarning]
warnings = do
Lens' Signature TCState
stImports Lens' Signature TCState -> (Signature -> Signature) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ imp :: Signature
imp -> [Signature] -> Signature
unionSignatures [Signature
imp, Signature
isig]
Lens' (BuiltinThings PrimFun) TCState
stImportedBuiltins Lens' (BuiltinThings PrimFun) TCState
-> (BuiltinThings PrimFun -> BuiltinThings PrimFun) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ imp :: BuiltinThings PrimFun
imp -> BuiltinThings PrimFun
-> BuiltinThings PrimFun -> BuiltinThings PrimFun
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union BuiltinThings PrimFun
imp BuiltinThings PrimFun
ibuiltin
Lens' (Map QName String) TCState
stImportedUserWarnings Lens' (Map QName String) TCState
-> (Map QName String -> Map QName String) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ imp :: Map QName String
imp -> Map QName String -> Map QName String -> Map QName String
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map QName String
imp Map QName String
userwarn
Lens' (Set QName) TCState
stImportedPartialDefs Lens' (Set QName) TCState -> (Set QName -> Set QName) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ imp :: Set QName
imp -> Set QName -> Set QName -> Set QName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set QName
imp Set QName
partialdefs
Lens' PatternSynDefns TCState
stPatternSynImports Lens' PatternSynDefns TCState
-> (PatternSynDefns -> PatternSynDefns) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ imp :: PatternSynDefns
imp -> PatternSynDefns -> PatternSynDefns -> PatternSynDefns
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union PatternSynDefns
imp PatternSynDefns
patsyns
Lens' DisplayForms TCState
stImportedDisplayForms Lens' DisplayForms TCState
-> (DisplayForms -> DisplayForms) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ imp :: DisplayForms
imp -> ([LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm])
-> DisplayForms -> DisplayForms -> DisplayForms
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HMap.unionWith [LocalDisplayForm] -> [LocalDisplayForm] -> [LocalDisplayForm]
forall a. [a] -> [a] -> [a]
(++) DisplayForms
imp DisplayForms
display
Lens' [TCWarning] TCState
stTCWarnings Lens' [TCWarning] TCState -> ([TCWarning] -> [TCWarning]) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \ imp :: [TCWarning]
imp -> [TCWarning] -> [TCWarning] -> [TCWarning]
forall a. Eq a => [a] -> [a] -> [a]
List.union [TCWarning]
imp [TCWarning]
warnings
Signature -> TCM ()
addImportedInstances Signature
isig
scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)
scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)
scopeCheckImport x :: ModuleName
x = do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.scope" 5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Scope checking " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ModuleName -> String
forall a. Pretty a => a -> String
prettyShow ModuleName
x
String -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS "import.scope" 10 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
[TopLevelModuleName]
visited <- Map TopLevelModuleName ModuleInfo -> [TopLevelModuleName]
forall k a. Map k a -> [k]
Map.keys (Map TopLevelModuleName ModuleInfo -> [TopLevelModuleName])
-> TCMT IO (Map TopLevelModuleName ModuleInfo)
-> TCMT IO [TopLevelModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Map TopLevelModuleName ModuleInfo)
getVisitedModules
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.scope" 10 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
" visited: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate ", " ((TopLevelModuleName -> String) -> [TopLevelModuleName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow [TopLevelModuleName]
visited)
Interface
i <- Account Phase -> TCMT IO Interface -> TCMT IO Interface
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [] (TCMT IO Interface -> TCMT IO Interface)
-> TCMT IO Interface -> TCMT IO Interface
forall a b. (a -> b) -> a -> b
$ ModuleName -> TCMT IO Interface
getInterface ModuleName
x
ModuleName -> TCM ()
addImport ModuleName
x
Maybe String -> (String -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Interface -> Maybe String
iImportWarning Interface
i) ((String -> TCM ()) -> TCM ()) -> (String -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ Warning -> TCM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> TCM ()) -> (String -> Warning) -> String -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Warning
UserWarning
let s :: Map ModuleName Scope
s = Interface -> Map ModuleName Scope
iScope Interface
i
(ModuleName, Map ModuleName Scope)
-> TCM (ModuleName, Map ModuleName Scope)
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface -> ModuleName
iModuleName Interface
i ModuleName -> QName -> ModuleName
`withRangesOfQ` ModuleName -> QName
mnameToConcrete ModuleName
x, Map ModuleName Scope
s)
data MaybeWarnings' a = NoWarnings | SomeWarnings a
deriving (Int -> MaybeWarnings' a -> ShowS
[MaybeWarnings' a] -> ShowS
MaybeWarnings' a -> String
(Int -> MaybeWarnings' a -> ShowS)
-> (MaybeWarnings' a -> String)
-> ([MaybeWarnings' a] -> ShowS)
-> Show (MaybeWarnings' a)
forall a. Show a => Int -> MaybeWarnings' a -> ShowS
forall a. Show a => [MaybeWarnings' a] -> ShowS
forall a. Show a => MaybeWarnings' a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MaybeWarnings' a] -> ShowS
$cshowList :: forall a. Show a => [MaybeWarnings' a] -> ShowS
show :: MaybeWarnings' a -> String
$cshow :: forall a. Show a => MaybeWarnings' a -> String
showsPrec :: Int -> MaybeWarnings' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> MaybeWarnings' a -> ShowS
Show, a -> MaybeWarnings' b -> MaybeWarnings' a
(a -> b) -> MaybeWarnings' a -> MaybeWarnings' b
(forall a b. (a -> b) -> MaybeWarnings' a -> MaybeWarnings' b)
-> (forall a b. a -> MaybeWarnings' b -> MaybeWarnings' a)
-> Functor MaybeWarnings'
forall a b. a -> MaybeWarnings' b -> MaybeWarnings' a
forall a b. (a -> b) -> MaybeWarnings' a -> MaybeWarnings' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> MaybeWarnings' b -> MaybeWarnings' a
$c<$ :: forall a b. a -> MaybeWarnings' b -> MaybeWarnings' a
fmap :: (a -> b) -> MaybeWarnings' a -> MaybeWarnings' b
$cfmap :: forall a b. (a -> b) -> MaybeWarnings' a -> MaybeWarnings' b
Functor, MaybeWarnings' a -> Bool
(a -> m) -> MaybeWarnings' a -> m
(a -> b -> b) -> b -> MaybeWarnings' a -> b
(forall m. Monoid m => MaybeWarnings' m -> m)
-> (forall m a. Monoid m => (a -> m) -> MaybeWarnings' a -> m)
-> (forall m a. Monoid m => (a -> m) -> MaybeWarnings' a -> m)
-> (forall a b. (a -> b -> b) -> b -> MaybeWarnings' a -> b)
-> (forall a b. (a -> b -> b) -> b -> MaybeWarnings' a -> b)
-> (forall b a. (b -> a -> b) -> b -> MaybeWarnings' a -> b)
-> (forall b a. (b -> a -> b) -> b -> MaybeWarnings' a -> b)
-> (forall a. (a -> a -> a) -> MaybeWarnings' a -> a)
-> (forall a. (a -> a -> a) -> MaybeWarnings' a -> a)
-> (forall a. MaybeWarnings' a -> [a])
-> (forall a. MaybeWarnings' a -> Bool)
-> (forall a. MaybeWarnings' a -> Int)
-> (forall a. Eq a => a -> MaybeWarnings' a -> Bool)
-> (forall a. Ord a => MaybeWarnings' a -> a)
-> (forall a. Ord a => MaybeWarnings' a -> a)
-> (forall a. Num a => MaybeWarnings' a -> a)
-> (forall a. Num a => MaybeWarnings' a -> a)
-> Foldable MaybeWarnings'
forall a. Eq a => a -> MaybeWarnings' a -> Bool
forall a. Num a => MaybeWarnings' a -> a
forall a. Ord a => MaybeWarnings' a -> a
forall m. Monoid m => MaybeWarnings' m -> m
forall a. MaybeWarnings' a -> Bool
forall a. MaybeWarnings' a -> Int
forall a. MaybeWarnings' a -> [a]
forall a. (a -> a -> a) -> MaybeWarnings' a -> a
forall m a. Monoid m => (a -> m) -> MaybeWarnings' a -> m
forall b a. (b -> a -> b) -> b -> MaybeWarnings' a -> b
forall a b. (a -> b -> b) -> b -> MaybeWarnings' a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: MaybeWarnings' a -> a
$cproduct :: forall a. Num a => MaybeWarnings' a -> a
sum :: MaybeWarnings' a -> a
$csum :: forall a. Num a => MaybeWarnings' a -> a
minimum :: MaybeWarnings' a -> a
$cminimum :: forall a. Ord a => MaybeWarnings' a -> a
maximum :: MaybeWarnings' a -> a
$cmaximum :: forall a. Ord a => MaybeWarnings' a -> a
elem :: a -> MaybeWarnings' a -> Bool
$celem :: forall a. Eq a => a -> MaybeWarnings' a -> Bool
length :: MaybeWarnings' a -> Int
$clength :: forall a. MaybeWarnings' a -> Int
null :: MaybeWarnings' a -> Bool
$cnull :: forall a. MaybeWarnings' a -> Bool
toList :: MaybeWarnings' a -> [a]
$ctoList :: forall a. MaybeWarnings' a -> [a]
foldl1 :: (a -> a -> a) -> MaybeWarnings' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> MaybeWarnings' a -> a
foldr1 :: (a -> a -> a) -> MaybeWarnings' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> MaybeWarnings' a -> a
foldl' :: (b -> a -> b) -> b -> MaybeWarnings' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> MaybeWarnings' a -> b
foldl :: (b -> a -> b) -> b -> MaybeWarnings' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> MaybeWarnings' a -> b
foldr' :: (a -> b -> b) -> b -> MaybeWarnings' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> MaybeWarnings' a -> b
foldr :: (a -> b -> b) -> b -> MaybeWarnings' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> MaybeWarnings' a -> b
foldMap' :: (a -> m) -> MaybeWarnings' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> MaybeWarnings' a -> m
foldMap :: (a -> m) -> MaybeWarnings' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> MaybeWarnings' a -> m
fold :: MaybeWarnings' m -> m
$cfold :: forall m. Monoid m => MaybeWarnings' m -> m
Foldable, Functor MaybeWarnings'
Foldable MaybeWarnings'
(Functor MaybeWarnings', Foldable MaybeWarnings') =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MaybeWarnings' a -> f (MaybeWarnings' b))
-> (forall (f :: * -> *) a.
Applicative f =>
MaybeWarnings' (f a) -> f (MaybeWarnings' a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MaybeWarnings' a -> m (MaybeWarnings' b))
-> (forall (m :: * -> *) a.
Monad m =>
MaybeWarnings' (m a) -> m (MaybeWarnings' a))
-> Traversable MaybeWarnings'
(a -> f b) -> MaybeWarnings' a -> f (MaybeWarnings' b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
MaybeWarnings' (m a) -> m (MaybeWarnings' a)
forall (f :: * -> *) a.
Applicative f =>
MaybeWarnings' (f a) -> f (MaybeWarnings' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MaybeWarnings' a -> m (MaybeWarnings' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MaybeWarnings' a -> f (MaybeWarnings' b)
sequence :: MaybeWarnings' (m a) -> m (MaybeWarnings' a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
MaybeWarnings' (m a) -> m (MaybeWarnings' a)
mapM :: (a -> m b) -> MaybeWarnings' a -> m (MaybeWarnings' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MaybeWarnings' a -> m (MaybeWarnings' b)
sequenceA :: MaybeWarnings' (f a) -> f (MaybeWarnings' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
MaybeWarnings' (f a) -> f (MaybeWarnings' a)
traverse :: (a -> f b) -> MaybeWarnings' a -> f (MaybeWarnings' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MaybeWarnings' a -> f (MaybeWarnings' b)
$cp2Traversable :: Foldable MaybeWarnings'
$cp1Traversable :: Functor MaybeWarnings'
Traversable)
type MaybeWarnings = MaybeWarnings' [TCWarning]
applyFlagsToMaybeWarnings :: MaybeWarnings -> TCM MaybeWarnings
applyFlagsToMaybeWarnings :: MaybeWarnings -> TCM MaybeWarnings
applyFlagsToMaybeWarnings mw :: MaybeWarnings
mw = do
MaybeWarnings
w' <- ([TCWarning] -> TCMT IO [TCWarning])
-> MaybeWarnings -> TCM MaybeWarnings
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse [TCWarning] -> TCMT IO [TCWarning]
applyFlagsToTCWarnings MaybeWarnings
mw
MaybeWarnings -> TCM MaybeWarnings
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeWarnings -> TCM MaybeWarnings)
-> MaybeWarnings -> TCM MaybeWarnings
forall a b. (a -> b) -> a -> b
$ if MaybeWarnings -> Bool
forall a. Null a => a -> Bool
null MaybeWarnings
w' then MaybeWarnings
forall a. MaybeWarnings' a
NoWarnings else MaybeWarnings
w'
instance Null a => Null (MaybeWarnings' a) where
empty :: MaybeWarnings' a
empty = MaybeWarnings' a
forall a. MaybeWarnings' a
NoWarnings
null :: MaybeWarnings' a -> Bool
null mws :: MaybeWarnings' a
mws = case MaybeWarnings' a
mws of
NoWarnings -> Bool
True
SomeWarnings ws :: a
ws -> a -> Bool
forall a. Null a => a -> Bool
null a
ws
hasWarnings :: MaybeWarnings -> Bool
hasWarnings :: MaybeWarnings -> Bool
hasWarnings = Bool -> Bool
not (Bool -> Bool) -> (MaybeWarnings -> Bool) -> MaybeWarnings -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeWarnings -> Bool
forall a. Null a => a -> Bool
null
alreadyVisited :: C.TopLevelModuleName ->
MainInterface ->
PragmaOptions ->
TCM (Interface, MaybeWarnings) ->
TCM (Interface, MaybeWarnings)
alreadyVisited :: TopLevelModuleName
-> MainInterface
-> PragmaOptions
-> TCM (Interface, MaybeWarnings)
-> TCM (Interface, MaybeWarnings)
alreadyVisited x :: TopLevelModuleName
x isMain :: MainInterface
isMain currentOptions :: PragmaOptions
currentOptions getIface :: TCM (Interface, MaybeWarnings)
getIface = do
Maybe ModuleInfo
mm <- TopLevelModuleName -> TCM (Maybe ModuleInfo)
getVisitedModule TopLevelModuleName
x
case Maybe ModuleInfo
mm of
Just mi :: ModuleInfo
mi | Bool -> Bool
not (ModuleInfo -> Bool
miWarnings ModuleInfo
mi) -> do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.visit" 10 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ " Already visited " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
x
let i :: Interface
i = ModuleInfo -> Interface
miInterface ModuleInfo
mi
Bool
optsCompat <- if ModuleInfo -> Bool
miPrimitive ModuleInfo
mi then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else
TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((TCEnv -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envCheckOptionConsistency)
(PragmaOptions -> PragmaOptions -> ModuleName -> TCMT IO Bool
checkOptionsCompatible PragmaOptions
currentOptions (Interface -> PragmaOptions
iOptionsUsed Interface
i)
(Interface -> ModuleName
iModuleName Interface
i))
(Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
if Bool
optsCompat then (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface
i , MaybeWarnings
forall a. MaybeWarnings' a
NoWarnings) else do
MaybeWarnings
wt <- MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' MainInterface
isMain WhichWarnings
ErrorWarnings
(Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface
i, MaybeWarnings
wt)
_ -> do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.visit" 5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ " Getting interface for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
x
r :: (Interface, MaybeWarnings)
r@(i :: Interface
i, wt :: MaybeWarnings
wt) <- TCM (Interface, MaybeWarnings)
getIface
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.visit" 5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ " Now we've looked at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
x
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MainInterface
isMain MainInterface -> MainInterface -> Bool
forall a. Eq a => a -> a -> Bool
== Mode -> MainInterface
MainInterface Mode
ScopeCheck) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
ModuleInfo -> TCM ()
visitModule ModuleInfo :: Interface -> Bool -> Bool -> ModuleInfo
ModuleInfo
{ miInterface :: Interface
miInterface = Interface
i
, miWarnings :: Bool
miWarnings = MaybeWarnings -> Bool
hasWarnings MaybeWarnings
wt
, miPrimitive :: Bool
miPrimitive = Bool
False
}
(Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface, MaybeWarnings)
r
typeCheckMain
:: SourceFile
-> Mode
-> SourceInfo
-> TCM (Interface, MaybeWarnings)
typeCheckMain :: SourceFile -> Mode -> SourceInfo -> TCM (Interface, MaybeWarnings)
typeCheckMain f :: SourceFile
f mode :: Mode
mode si :: SourceInfo
si = do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.main" 10 "Importing the primitive modules."
String
libdir <- IO String -> TCMT IO String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO String
defaultLibDir
let libdirPrim :: String
libdirPrim = String
libdir String -> ShowS
</> "prim"
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.main" 20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Library dir = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
libdir
TCMT IO PersistentVerbosity
-> (PersistentVerbosity -> TCM ()) -> TCM () -> TCM ()
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ ((TCState -> PersistentVerbosity) -> TCMT IO PersistentVerbosity
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC TCState -> PersistentVerbosity
forall a. LensPersistentVerbosity a => a -> PersistentVerbosity
Lens.getPersistentVerbosity) PersistentVerbosity -> TCM ()
Lens.putPersistentVerbosity (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
(PersistentVerbosity -> PersistentVerbosity) -> TCM ()
Lens.modifyPersistentVerbosity ([String] -> PersistentVerbosity -> PersistentVerbosity
forall k v. Ord k => [k] -> Trie k v -> Trie k v
Trie.delete [])
HighlightingLevel -> TCM () -> TCM ()
forall a. HighlightingLevel -> TCM a -> TCM a
withHighlightingLevel HighlightingLevel
None (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> TCM ()
forall a. TCM a -> TCM a
withoutOptionsChecking (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
Set String -> (String -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (ShowS -> Set String -> Set String
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (String
libdirPrim String -> ShowS
</>) Set String
Lens.primitiveModules) ((String -> TCM ()) -> TCM ()) -> (String -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \f :: String
f -> do
let file :: SourceFile
file = AbsolutePath -> SourceFile
SourceFile (AbsolutePath -> SourceFile) -> AbsolutePath -> SourceFile
forall a b. (a -> b) -> a -> b
$ String -> AbsolutePath
mkAbsolute String
f
SourceInfo
si <- SourceFile -> TCM SourceInfo
sourceInfo SourceFile
file
TopLevelModuleName -> SourceFile -> TCM ()
checkModuleName' (SourceInfo -> TopLevelModuleName
siModuleName SourceInfo
si) SourceFile
file
Interface
_ <- TopLevelModuleName -> Maybe SourceInfo -> TCMT IO Interface
getInterface_ (SourceInfo -> TopLevelModuleName
siModuleName SourceInfo
si) (SourceInfo -> Maybe SourceInfo
forall a. a -> Maybe a
Just SourceInfo
si)
TopLevelModuleName -> (ModuleInfo -> ModuleInfo) -> TCM ()
mapVisitedModule (SourceInfo -> TopLevelModuleName
siModuleName SourceInfo
si) (\ m :: ModuleInfo
m -> ModuleInfo
m { miPrimitive :: Bool
miPrimitive = Bool
True })
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.main" 10 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ "Done importing the primitive modules."
TopLevelModuleName -> SourceFile -> TCM ()
checkModuleName' (SourceInfo -> TopLevelModuleName
siModuleName SourceInfo
si) SourceFile
f
TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
getInterface' (SourceInfo -> TopLevelModuleName
siModuleName SourceInfo
si) (Mode -> MainInterface
MainInterface Mode
mode) (SourceInfo -> Maybe SourceInfo
forall a. a -> Maybe a
Just SourceInfo
si)
where
checkModuleName' :: TopLevelModuleName -> SourceFile -> TCM ()
checkModuleName' m :: TopLevelModuleName
m f :: SourceFile
f =
(if Range -> Bool
forall a. Null a => a -> Bool
null Range
r then TCM () -> TCM ()
forall a. a -> a
id else Call -> TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm) =>
Call -> tcm a -> tcm a
traceCall (Range -> Call
SetRange Range
r)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
TopLevelModuleName
-> SourceFile -> Maybe TopLevelModuleName -> TCM ()
checkModuleName TopLevelModuleName
m SourceFile
f Maybe TopLevelModuleName
forall a. Maybe a
Nothing
where
r :: Range
r = TopLevelModuleName -> Range
forall t. HasRange t => t -> Range
getRange TopLevelModuleName
m
getInterface :: ModuleName -> TCM Interface
getInterface :: ModuleName -> TCMT IO Interface
getInterface m :: ModuleName
m = TopLevelModuleName -> Maybe SourceInfo -> TCMT IO Interface
getInterface_ (ModuleName -> TopLevelModuleName
toTopLevelModuleName ModuleName
m) Maybe SourceInfo
forall a. Maybe a
Nothing
getInterface_
:: C.TopLevelModuleName
-> Maybe SourceInfo
-> TCM Interface
getInterface_ :: TopLevelModuleName -> Maybe SourceInfo -> TCMT IO Interface
getInterface_ x :: TopLevelModuleName
x msi :: Maybe SourceInfo
msi = do
(i :: Interface
i, wt :: MaybeWarnings
wt) <- TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
getInterface' TopLevelModuleName
x MainInterface
NotMainInterface Maybe SourceInfo
msi
case MaybeWarnings
wt of
SomeWarnings w :: [TCWarning]
w -> [TCWarning] -> TCMT IO Interface
forall a. [TCWarning] -> TCM a
tcWarningsToError ((TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Warning -> Bool
notIM (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) [TCWarning]
w)
NoWarnings -> Interface -> TCMT IO Interface
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i
where notIM :: Warning -> Bool
notIM UnsolvedInteractionMetas{} = Bool
False
notIM _ = Bool
True
getInterface'
:: C.TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
getInterface' :: TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
getInterface' x :: TopLevelModuleName
x isMain :: MainInterface
isMain msi :: Maybe SourceInfo
msi =
TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a. TCM a -> TCM a
withIncreasedModuleNestingLevel (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$
TCMT IO PragmaOptions
-> (PragmaOptions -> TCM ())
-> TCM (Interface, MaybeWarnings)
-> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_ (Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PragmaOptions TCState
stPragmaOptions)
(Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MainInterface -> Bool
includeStateChanges MainInterface
isMain) (TCM () -> TCM ())
-> (PragmaOptions -> TCM ()) -> PragmaOptions -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Lens' PragmaOptions TCState
stPragmaOptions Lens' PragmaOptions TCState -> PragmaOptions -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens`)) (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (MainInterface -> Bool
includeStateChanges MainInterface
isMain) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
[[String]]
pragmas <- [Pragma] -> TCM [[String]]
concreteOptionsToOptionPragmas
(Module -> [Pragma]
forall a b. (a, b) -> a
fst (Module -> [Pragma]) -> Module -> [Pragma]
forall a b. (a -> b) -> a -> b
$ Module -> (SourceInfo -> Module) -> Maybe SourceInfo -> Module
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Module
forall a. HasCallStack => a
__IMPOSSIBLE__ SourceInfo -> Module
siModule Maybe SourceInfo
msi)
([String] -> TCM ()) -> [[String]] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [String] -> TCM ()
setOptionsFromPragma [[String]]
pragmas
PragmaOptions
currentOptions <- Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PragmaOptions TCState
stPragmaOptions
CommandLineOptions -> TCM ()
setCommandLineOptions (CommandLineOptions -> TCM ())
-> (TCState -> CommandLineOptions) -> TCState -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PersistentTCState -> CommandLineOptions
stPersistentOptions (PersistentTCState -> CommandLineOptions)
-> (TCState -> PersistentTCState) -> TCState -> CommandLineOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState (TCState -> TCM ()) -> TCMT IO TCState -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
TopLevelModuleName
-> MainInterface
-> PragmaOptions
-> TCM (Interface, MaybeWarnings)
-> TCM (Interface, MaybeWarnings)
alreadyVisited TopLevelModuleName
x MainInterface
isMain PragmaOptions
currentOptions (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a. TopLevelModuleName -> TCM a -> TCM a
addImportCycleCheck TopLevelModuleName
x (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ do
SourceFile
file <- TopLevelModuleName -> TCM SourceFile
findFile TopLevelModuleName
x
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 10 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ " Check for cycle"
TCM ()
checkForImportCycle
Bool
uptodate <- Account Phase -> TCMT IO Bool -> TCMT IO Bool
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Import] (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
Bool
ignore <- (TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
ignoreInterfaces TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`and2M`
(Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCMT IO Bool
Lens.isBuiltinModule (AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file)))
TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
ignoreAllInterfaces
Maybe Interface
cached <- MaybeT TCM Interface -> TCM (Maybe Interface)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT TCM Interface -> TCM (Maybe Interface))
-> MaybeT TCM Interface -> TCM (Maybe Interface)
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> SourceFile -> MaybeT TCM Interface
isCached TopLevelModuleName
x SourceFile
file
Hash
sourceH <- case Maybe SourceInfo
msi of
Nothing -> IO Hash -> TCMT IO Hash
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Hash -> TCMT IO Hash) -> IO Hash -> TCMT IO Hash
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> IO Hash
hashTextFile (SourceFile -> AbsolutePath
srcFilePath SourceFile
file)
Just si :: SourceInfo
si -> Hash -> TCMT IO Hash
forall (m :: * -> *) a. Monad m => a -> m a
return (Hash -> TCMT IO Hash) -> Hash -> TCMT IO Hash
forall a b. (a -> b) -> a -> b
$ Text -> Hash
hashText (SourceInfo -> Text
siSource SourceInfo
si)
Maybe Hash
ifaceH <- case Maybe Interface
cached of
Nothing -> do
AbsolutePath
mifile <- SourceFile -> TCM AbsolutePath
toIFile SourceFile
file
((Hash, Hash) -> Hash) -> Maybe (Hash, Hash) -> Maybe Hash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Hash, Hash) -> Hash
forall a b. (a, b) -> a
fst (Maybe (Hash, Hash) -> Maybe Hash)
-> TCMT IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe Hash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsolutePath -> TCMT IO (Maybe (Hash, Hash))
getInterfaceFileHashes AbsolutePath
mifile
Just i :: Interface
i -> Maybe Hash -> TCMT IO (Maybe Hash)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Hash -> TCMT IO (Maybe Hash))
-> Maybe Hash -> TCMT IO (Maybe Hash)
forall a b. (a -> b) -> a -> b
$ Hash -> Maybe Hash
forall a. a -> Maybe a
Just (Hash -> Maybe Hash) -> Hash -> Maybe Hash
forall a b. (a -> b) -> a -> b
$ Interface -> Hash
iSourceHash Interface
i
let unchanged :: Bool
unchanged = Hash -> Maybe Hash
forall a. a -> Maybe a
Just Hash
sourceH Maybe Hash -> Maybe Hash -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Hash
ifaceH
Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TCMT IO Bool) -> Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Bool
unchanged Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
ignore Bool -> Bool -> Bool
|| Maybe Interface -> Bool
forall a. Maybe a -> Bool
isJust Maybe Interface
cached)
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is " String -> ShowS
forall a. [a] -> [a] -> [a]
++
(if Bool
uptodate then "" else "not ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ "up-to-date."
(stateChangesIncluded :: Bool
stateChangesIncluded, (i :: Interface
i, wt :: MaybeWarnings
wt)) <- do
let maySkip :: Bool
maySkip = Bool
True
if Bool
uptodate Bool -> Bool -> Bool
&& Bool
maySkip
then TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCM (Bool, (Interface, MaybeWarnings))
getStoredInterface TopLevelModuleName
x SourceFile
file MainInterface
isMain Maybe SourceInfo
msi
else TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCM (Bool, (Interface, MaybeWarnings))
typeCheck TopLevelModuleName
x SourceFile
file MainInterface
isMain Maybe SourceInfo
msi
let topLevelName :: TopLevelModuleName
topLevelName = ModuleName -> TopLevelModuleName
toTopLevelModuleName (ModuleName -> TopLevelModuleName)
-> ModuleName -> TopLevelModuleName
forall a b. (a -> b) -> a -> b
$ Interface -> ModuleName
iModuleName Interface
i
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TopLevelModuleName
topLevelName TopLevelModuleName -> TopLevelModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== TopLevelModuleName
x) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ AbsolutePath
-> TopLevelModuleName -> TopLevelModuleName -> TypeError
OverlappingProjects (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) TopLevelModuleName
topLevelName TopLevelModuleName
x
Bool
visited <- TopLevelModuleName -> TCMT IO Bool
isVisited TopLevelModuleName
x
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ if Bool
visited then " We've been here. Don't merge."
else " New module. Let's check it out."
MaybeWarnings
wt' <- TCMT IO Bool
-> TCM MaybeWarnings -> TCM MaybeWarnings -> TCM MaybeWarnings
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envCheckOptionConsistency)
(MaybeWarnings -> TCM MaybeWarnings
forall (m :: * -> *) a. Monad m => a -> m a
return MaybeWarnings
wt) (TCM MaybeWarnings -> TCM MaybeWarnings)
-> TCM MaybeWarnings -> TCM MaybeWarnings
forall a b. (a -> b) -> a -> b
$ do
Bool
optComp <- PragmaOptions -> PragmaOptions -> ModuleName -> TCMT IO Bool
checkOptionsCompatible PragmaOptions
currentOptions (Interface -> PragmaOptions
iOptionsUsed Interface
i) (Interface -> ModuleName
iModuleName Interface
i)
if Bool
optComp then MaybeWarnings -> TCM MaybeWarnings
forall (m :: * -> *) a. Monad m => a -> m a
return MaybeWarnings
wt else MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' MainInterface
isMain WhichWarnings
ErrorWarnings
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
visited Bool -> Bool -> Bool
|| Bool
stateChangesIncluded) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
Interface -> TCM ()
mergeInterface Interface
i
Account Phase -> TCM () -> TCM ()
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Highlighting] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
Interface -> SourceFile -> TCM ()
highlightFromInterface Interface
i SourceFile
file
Lens' (Maybe ModuleName) TCState
stCurrentModule Lens' (Maybe ModuleName) TCState -> Maybe ModuleName -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` ModuleName -> Maybe ModuleName
forall a. a -> Maybe a
Just (Interface -> ModuleName
iModuleName Interface
i)
case (MainInterface
isMain, MaybeWarnings
wt') of
(MainInterface ScopeCheck, _) -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(_, SomeWarnings w :: [TCWarning]
w) -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
_ -> Interface -> TCM ()
storeDecodedModule Interface
i
String -> Int -> [String] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
reportS "warning.import" 10
[ "module: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show (TopLevelModuleName -> [String]
C.moduleNameParts TopLevelModuleName
x)
, "WarningOnImport: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe String -> String
forall a. Show a => a -> String
show (Interface -> Maybe String
iImportWarning Interface
i)
]
(Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a. Monad m => a -> m a
return (Interface
i, MaybeWarnings
wt')
checkOptionsCompatible :: PragmaOptions -> PragmaOptions -> ModuleName -> TCM Bool
checkOptionsCompatible :: PragmaOptions -> PragmaOptions -> ModuleName -> TCMT IO Bool
checkOptionsCompatible current :: PragmaOptions
current imported :: PragmaOptions
imported importedModule :: ModuleName
importedModule = (StateT Bool TCM () -> Bool -> TCMT IO Bool)
-> Bool -> StateT Bool TCM () -> TCMT IO Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT Bool TCM () -> Bool -> TCMT IO Bool
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Bool
True (StateT Bool TCM () -> TCMT IO Bool)
-> StateT Bool TCM () -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> TCM Doc -> StateT Bool TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc "import.iface.options" 5 (TCM Doc -> StateT Bool TCM ()) -> TCM Doc -> StateT Bool TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
P.nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "current options =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> PragmaOptions -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc), IsString (m Doc)) =>
PragmaOptions -> m Doc
showOptions PragmaOptions
current
String -> Int -> TCM Doc -> StateT Bool TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc "import.iface.options" 5 (TCM Doc -> StateT Bool TCM ()) -> TCM Doc -> StateT Bool TCM ()
forall a b. (a -> b) -> a -> b
$ Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
P.nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "imported options =" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> PragmaOptions -> TCM Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc), IsString (m Doc)) =>
PragmaOptions -> m Doc
showOptions PragmaOptions
imported
[(PragmaOptions -> Bool, String)]
-> ((PragmaOptions -> Bool, String) -> StateT Bool TCM ())
-> StateT Bool TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(PragmaOptions -> Bool, String)]
coinfectiveOptions (((PragmaOptions -> Bool, String) -> StateT Bool TCM ())
-> StateT Bool TCM ())
-> ((PragmaOptions -> Bool, String) -> StateT Bool TCM ())
-> StateT Bool TCM ()
forall a b. (a -> b) -> a -> b
$ \ (opt :: PragmaOptions -> Bool
opt, optName :: String
optName) -> do
Bool -> StateT Bool TCM () -> StateT Bool TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PragmaOptions -> Bool
opt PragmaOptions
current Bool -> Bool -> Bool
`implies` PragmaOptions -> Bool
opt PragmaOptions
imported) (StateT Bool TCM () -> StateT Bool TCM ())
-> StateT Bool TCM () -> StateT Bool TCM ()
forall a b. (a -> b) -> a -> b
$ do
Bool -> StateT Bool TCM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Bool
False
Warning -> StateT Bool TCM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (String -> ModuleName -> Warning
CoInfectiveImport String
optName ModuleName
importedModule)
[(PragmaOptions -> Bool, String)]
-> ((PragmaOptions -> Bool, String) -> StateT Bool TCM ())
-> StateT Bool TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(PragmaOptions -> Bool, String)]
infectiveOptions (((PragmaOptions -> Bool, String) -> StateT Bool TCM ())
-> StateT Bool TCM ())
-> ((PragmaOptions -> Bool, String) -> StateT Bool TCM ())
-> StateT Bool TCM ()
forall a b. (a -> b) -> a -> b
$ \ (opt :: PragmaOptions -> Bool
opt, optName :: String
optName) -> do
Bool -> StateT Bool TCM () -> StateT Bool TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PragmaOptions -> Bool
opt PragmaOptions
imported Bool -> Bool -> Bool
`implies` PragmaOptions -> Bool
opt PragmaOptions
current) (StateT Bool TCM () -> StateT Bool TCM ())
-> StateT Bool TCM () -> StateT Bool TCM ()
forall a b. (a -> b) -> a -> b
$ do
Bool -> StateT Bool TCM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Bool
False
Warning -> StateT Bool TCM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (String -> ModuleName -> Warning
InfectiveImport String
optName ModuleName
importedModule)
where
implies :: Bool -> Bool -> Bool
p :: Bool
p implies :: Bool -> Bool -> Bool
`implies` q :: Bool
q = Bool
p Bool -> Bool -> Bool
forall a. Ord a => a -> a -> Bool
<= Bool
q
showOptions :: PragmaOptions -> m Doc
showOptions opts :: PragmaOptions
opts = [m Doc] -> m Doc
forall (m :: * -> *).
(Monad m, Semigroup (m Doc)) =>
[m Doc] -> m Doc
P.prettyList (((PragmaOptions -> Bool, String) -> m Doc)
-> [(PragmaOptions -> Bool, String)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (o :: PragmaOptions -> Bool
o, n :: String
n) -> (String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
P.text String
n m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> ": ") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
P.<+> (Bool -> m Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
P.pretty (Bool -> m Doc) -> Bool -> m Doc
forall a b. (a -> b) -> a -> b
$ PragmaOptions -> Bool
o PragmaOptions
opts))
([(PragmaOptions -> Bool, String)]
coinfectiveOptions [(PragmaOptions -> Bool, String)]
-> [(PragmaOptions -> Bool, String)]
-> [(PragmaOptions -> Bool, String)]
forall a. [a] -> [a] -> [a]
++ [(PragmaOptions -> Bool, String)]
infectiveOptions))
isCached
:: C.TopLevelModuleName
-> SourceFile
-> MaybeT TCM Interface
isCached :: TopLevelModuleName -> SourceFile -> MaybeT TCM Interface
isCached x :: TopLevelModuleName
x file :: SourceFile
file = do
InterfaceFile
ifile <- TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile)
-> TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile
forall a b. (a -> b) -> a -> b
$ SourceFile -> TCMT IO (Maybe InterfaceFile)
findInterfaceFile' SourceFile
file
Interface
mi <- TCM (Maybe Interface) -> MaybeT TCM Interface
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCM (Maybe Interface) -> MaybeT TCM Interface)
-> TCM (Maybe Interface) -> MaybeT TCM Interface
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> TCM (Maybe Interface)
getDecodedModule TopLevelModuleName
x
Hash
h <- TCMT IO (Maybe Hash) -> MaybeT TCM Hash
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe Hash) -> MaybeT TCM Hash)
-> TCMT IO (Maybe Hash) -> MaybeT TCM Hash
forall a b. (a -> b) -> a -> b
$ ((Hash, Hash) -> Hash) -> Maybe (Hash, Hash) -> Maybe Hash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Hash, Hash) -> Hash
forall a b. (a, b) -> b
snd (Maybe (Hash, Hash) -> Maybe Hash)
-> TCMT IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe Hash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InterfaceFile -> TCMT IO (Maybe (Hash, Hash))
getInterfaceFileHashes' InterfaceFile
ifile
Bool -> MaybeT TCM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> MaybeT TCM ()) -> Bool -> MaybeT TCM ()
forall a b. (a -> b) -> a -> b
$ Interface -> Hash
iFullHash Interface
mi Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
== Hash
h
Interface -> MaybeT TCM Interface
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
mi
getStoredInterface
:: C.TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCM (Bool, (Interface, MaybeWarnings))
getStoredInterface :: TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCM (Bool, (Interface, MaybeWarnings))
getStoredInterface x :: TopLevelModuleName
x file :: SourceFile
file isMain :: MainInterface
isMain msi :: Maybe SourceInfo
msi = do
let fp :: String
fp = AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file
let fallback :: TCM (Bool, (Interface, MaybeWarnings))
fallback = TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCM (Bool, (Interface, MaybeWarnings))
typeCheck TopLevelModuleName
x SourceFile
file MainInterface
isMain Maybe SourceInfo
msi
AbsolutePath
ifile <- SourceFile -> TCM AbsolutePath
toIFile SourceFile
file
let ifp :: String
ifp = AbsolutePath -> String
filePath AbsolutePath
ifile
Maybe Hash
h <- ((Hash, Hash) -> Hash) -> Maybe (Hash, Hash) -> Maybe Hash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Hash, Hash) -> Hash
forall a b. (a, b) -> b
snd (Maybe (Hash, Hash) -> Maybe Hash)
-> TCMT IO (Maybe (Hash, Hash)) -> TCMT IO (Maybe Hash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsolutePath -> TCMT IO (Maybe (Hash, Hash))
getInterfaceFileHashes AbsolutePath
ifile
Maybe Interface
mm <- TopLevelModuleName -> TCM (Maybe Interface)
getDecodedModule TopLevelModuleName
x
(cached :: Bool
cached, mi :: Maybe Interface
mi) <- Account Phase
-> TCMT IO (Bool, Maybe Interface)
-> TCMT IO (Bool, Maybe Interface)
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Deserialization] (TCMT IO (Bool, Maybe Interface)
-> TCMT IO (Bool, Maybe Interface))
-> TCMT IO (Bool, Maybe Interface)
-> TCMT IO (Bool, Maybe Interface)
forall a b. (a -> b) -> a -> b
$ case Maybe Interface
mm of
Just mi :: Interface
mi ->
if Hash -> Maybe Hash
forall a. a -> Maybe a
Just (Interface -> Hash
iFullHash Interface
mi) Maybe Hash -> Maybe Hash -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Hash
h
then do
TopLevelModuleName -> TCM ()
dropDecodedModule TopLevelModuleName
x
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 50 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ " cached hash = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Hash -> String
forall a. Show a => a -> String
show (Interface -> Hash
iFullHash Interface
mi)
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 50 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ " stored hash = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Hash -> String
forall a. Show a => a -> String
show Maybe Hash
h
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ " file is newer, re-reading " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ifp
(Bool
False,) (Maybe Interface -> (Bool, Maybe Interface))
-> TCM (Maybe Interface) -> TCMT IO (Bool, Maybe Interface)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsolutePath -> TCM (Maybe Interface)
readInterface AbsolutePath
ifile
else do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ " using stored version of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ifp
(Bool, Maybe Interface) -> TCMT IO (Bool, Maybe Interface)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, Interface -> Maybe Interface
forall a. a -> Maybe a
Just Interface
mi)
Nothing -> do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ " no stored version, reading " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ifp
(Bool
False,) (Maybe Interface -> (Bool, Maybe Interface))
-> TCM (Maybe Interface) -> TCMT IO (Bool, Maybe Interface)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsolutePath -> TCM (Maybe Interface)
readInterface AbsolutePath
ifile
case Maybe Interface
mi of
Nothing -> do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 5 " bad interface, re-type checking"
TCM (Bool, (Interface, MaybeWarnings))
fallback
Just i :: Interface
i -> do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ " imports: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(ModuleName, Hash)] -> String
forall a. Show a => a -> String
show (Interface -> [(ModuleName, Hash)]
iImportedModules Interface
i)
([String] -> TCM ()) -> [[String]] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [String] -> TCM ()
setOptionsFromPragma (Interface -> [[String]]
iPragmaOptions Interface
i)
Bool
optionsChanged <-TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ((Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Bool) -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Bool
envCheckOptionConsistency) TCMT IO Bool -> TCMT IO Bool -> TCMT IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M`
String -> TCMT IO Bool
Lens.isBuiltinModule String
fp)
(Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) (TCMT IO Bool -> TCMT IO Bool) -> TCMT IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ do
PragmaOptions
currentOptions <- Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PragmaOptions TCState
stPragmaOptions
let disagreements :: [String]
disagreements =
[ String
optName | (opt :: PragmaOptions -> RestartCodomain
opt, optName :: String
optName) <- [(PragmaOptions -> RestartCodomain, String)]
restartOptions,
PragmaOptions -> RestartCodomain
opt PragmaOptions
currentOptions RestartCodomain -> RestartCodomain -> Bool
forall a. Eq a => a -> a -> Bool
/= PragmaOptions -> RestartCodomain
opt (Interface -> PragmaOptions
iOptionsUsed Interface
i) ]
if [String] -> Bool
forall a. Null a => a -> Bool
null [String]
disagreements then Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False else do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.options" 4 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ " Changes in the following options in "
, ShowS
forall a. Pretty a => a -> String
prettyShow String
fp
, ", re-typechecking: "
, [String] -> String
forall a. Pretty a => a -> String
prettyShow [String]
disagreements
]
Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
if Bool
optionsChanged then TCM (Bool, (Interface, MaybeWarnings))
fallback else do
[Hash]
hs <- (Interface -> Hash) -> [Interface] -> [Hash]
forall a b. (a -> b) -> [a] -> [b]
map Interface -> Hash
iFullHash ([Interface] -> [Hash]) -> TCMT IO [Interface] -> TCMT IO [Hash]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModuleName -> TCMT IO Interface)
-> [ModuleName] -> TCMT IO [Interface]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ModuleName -> TCMT IO Interface
getInterface (((ModuleName, Hash) -> ModuleName)
-> [(ModuleName, Hash)] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, Hash) -> ModuleName
forall a b. (a, b) -> a
fst ([(ModuleName, Hash)] -> [ModuleName])
-> [(ModuleName, Hash)] -> [ModuleName]
forall a b. (a -> b) -> a -> b
$ Interface -> [(ModuleName, Hash)]
iImportedModules Interface
i)
if [Hash]
hs [Hash] -> [Hash] -> Bool
forall a. Eq a => a -> a -> Bool
/= ((ModuleName, Hash) -> Hash) -> [(ModuleName, Hash)] -> [Hash]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, Hash) -> Hash
forall a b. (a, b) -> b
snd (Interface -> [(ModuleName, Hash)]
iImportedModules Interface
i)
then TCM (Bool, (Interface, MaybeWarnings))
fallback
else do
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
cached (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
String -> TopLevelModuleName -> Maybe String -> TCM ()
chaseMsg "Loading " TopLevelModuleName
x (Maybe String -> TCM ()) -> Maybe String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
ifp
let ws :: [TCWarning]
ws = (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter ((AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Strict.Just (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) Maybe AbsolutePath -> Maybe AbsolutePath -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe AbsolutePath -> Bool)
-> (TCWarning -> Maybe AbsolutePath) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Maybe AbsolutePath
tcWarningOrigin) (Interface -> [TCWarning]
iWarnings Interface
i)
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
ws) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc "warning" 1 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
P.vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCWarning -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
P.prettyTCM (TCWarning -> TCM Doc) -> [TCWarning] -> [TCM Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TCWarning]
ws
(Bool, (Interface, MaybeWarnings))
-> TCM (Bool, (Interface, MaybeWarnings))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, (Interface
i, MaybeWarnings
forall a. MaybeWarnings' a
NoWarnings))
typeCheck
:: C.TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCM (Bool, (Interface, MaybeWarnings))
typeCheck :: TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCM (Bool, (Interface, MaybeWarnings))
typeCheck x :: TopLevelModuleName
x file :: SourceFile
file isMain :: MainInterface
isMain msi :: Maybe SourceInfo
msi = do
let fp :: String
fp = AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath SourceFile
file
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MainInterface -> Bool
includeStateChanges MainInterface
isMain) TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
let checkMsg :: String
checkMsg = case MainInterface
isMain of
MainInterface ScopeCheck -> "Reading "
_ -> "Checking"
withMsgs :: TCMT IO b -> TCMT IO b
withMsgs = TCM () -> (() -> TCM ()) -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b.
Monad m =>
m a -> (a -> m ()) -> m b -> m b
bracket_
(String -> TopLevelModuleName -> Maybe String -> TCM ()
chaseMsg String
checkMsg TopLevelModuleName
x (Maybe String -> TCM ()) -> Maybe String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
fp)
(TCM () -> () -> TCM ()
forall a b. a -> b -> a
const (TCM () -> () -> TCM ()) -> TCM () -> () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do [TCWarning]
ws <- WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
let classified :: WarningsAndNonFatalErrors
classified = [TCWarning] -> WarningsAndNonFatalErrors
classifyWarnings [TCWarning]
ws
let wa' :: [TCWarning]
wa' = (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter ((AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Strict.Just (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) Maybe AbsolutePath -> Maybe AbsolutePath -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe AbsolutePath -> Bool)
-> (TCWarning -> Maybe AbsolutePath) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Maybe AbsolutePath
tcWarningOrigin) (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
classified)
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
wa') (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
String -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc "warning" 1 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
P.vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCWarning -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
P.prettyTCM (TCWarning -> TCM Doc) -> [TCWarning] -> [TCM Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TCWarning]
wa'
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null (WarningsAndNonFatalErrors -> [TCWarning]
nonFatalErrors WarningsAndNonFatalErrors
classified)) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TopLevelModuleName -> Maybe String -> TCM ()
chaseMsg "Finished" TopLevelModuleName
x Maybe String
forall a. Maybe a
Nothing)
case MainInterface
isMain of
MainInterface _ -> do
(Interface, MaybeWarnings)
r <- TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a. TCM a -> TCM a
withMsgs (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ SourceFile
-> TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
createInterface SourceFile
file TopLevelModuleName
x MainInterface
isMain Maybe SourceInfo
msi
(Bool, (Interface, MaybeWarnings))
-> TCM (Bool, (Interface, MaybeWarnings))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, (Interface, MaybeWarnings)
r)
NotMainInterface -> do
[TopLevelModuleName]
ms <- TCMT IO [TopLevelModuleName]
getImportPath
Int
nesting <- (TCEnv -> Int) -> TCMT IO Int
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Int
envModuleNestingLevel
Range
range <- (TCEnv -> Range) -> TCMT IO Range
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Range
envRange
Maybe (Closure Call)
call <- (TCEnv -> Maybe (Closure Call)) -> TCMT IO (Maybe (Closure Call))
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe (Closure Call)
envCall
ModuleToSource
mf <- Lens' ModuleToSource TCState -> TCMT IO ModuleToSource
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' ModuleToSource TCState
stModuleToSource
Map TopLevelModuleName ModuleInfo
vs <- TCMT IO (Map TopLevelModuleName ModuleInfo)
getVisitedModules
DecodedModules
ds <- TCM DecodedModules
getDecodedModules
CommandLineOptions
opts <- PersistentTCState -> CommandLineOptions
stPersistentOptions (PersistentTCState -> CommandLineOptions)
-> (TCState -> PersistentTCState) -> TCState -> CommandLineOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCState -> PersistentTCState
stPersistentState (TCState -> CommandLineOptions)
-> TCMT IO TCState -> TCMT IO CommandLineOptions
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
Signature
isig <- Lens' Signature TCState -> TCMT IO Signature
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' Signature TCState
stImports
BuiltinThings PrimFun
ibuiltin <- Lens' (BuiltinThings PrimFun) TCState
-> TCMT IO (BuiltinThings PrimFun)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (BuiltinThings PrimFun) TCState
stImportedBuiltins
DisplayForms
display <- Lens' DisplayForms TCState -> TCMT IO DisplayForms
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' DisplayForms TCState
stImportsDisplayForms
Map QName String
userwarn <- Lens' (Map QName String) TCState -> TCMT IO (Map QName String)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName String) TCState
stImportedUserWarnings
Set QName
partialdefs <- Lens' (Set QName) TCState -> TCMT IO (Set QName)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Set QName) TCState
stImportedPartialDefs
PatternSynDefns
ipatsyns <- TCMT IO PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSynImports
InteractionOutputCallback
ho <- TCM InteractionOutputCallback
getInteractionOutputCallback
Either TCErr ((Interface, MaybeWarnings), TCM ())
r <- TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
-> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
forall (m :: * -> *) a.
(MonadTCState m, ReadTCState m) =>
m a -> m a
withoutCache (TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
-> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ())))
-> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
-> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
forall a b. (a -> b) -> a -> b
$
TCM ((Interface, MaybeWarnings), TCM ())
-> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
forall a. TCM a -> TCM (Either TCErr a)
freshTCM (TCM ((Interface, MaybeWarnings), TCM ())
-> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ())))
-> TCM ((Interface, MaybeWarnings), TCM ())
-> TCMT IO (Either TCErr ((Interface, MaybeWarnings), TCM ()))
forall a b. (a -> b) -> a -> b
$
[TopLevelModuleName]
-> TCM ((Interface, MaybeWarnings), TCM ())
-> TCM ((Interface, MaybeWarnings), TCM ())
forall a. [TopLevelModuleName] -> TCM a -> TCM a
withImportPath [TopLevelModuleName]
ms (TCM ((Interface, MaybeWarnings), TCM ())
-> TCM ((Interface, MaybeWarnings), TCM ()))
-> TCM ((Interface, MaybeWarnings), TCM ())
-> TCM ((Interface, MaybeWarnings), TCM ())
forall a b. (a -> b) -> a -> b
$
(TCEnv -> TCEnv)
-> TCM ((Interface, MaybeWarnings), TCM ())
-> TCM ((Interface, MaybeWarnings), TCM ())
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\e :: TCEnv
e -> TCEnv
e { envModuleNestingLevel :: Int
envModuleNestingLevel = Int
nesting
, envRange :: Range
envRange = Range
range
, envCall :: Maybe (Closure Call)
envCall = Maybe (Closure Call)
call
}) (TCM ((Interface, MaybeWarnings), TCM ())
-> TCM ((Interface, MaybeWarnings), TCM ()))
-> TCM ((Interface, MaybeWarnings), TCM ())
-> TCM ((Interface, MaybeWarnings), TCM ())
forall a b. (a -> b) -> a -> b
$ do
DecodedModules -> TCM ()
setDecodedModules DecodedModules
ds
CommandLineOptions -> TCM ()
setCommandLineOptions CommandLineOptions
opts
InteractionOutputCallback -> TCM ()
setInteractionOutputCallback InteractionOutputCallback
ho
Lens' ModuleToSource TCState
stModuleToSource Lens' ModuleToSource TCState -> ModuleToSource -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` ModuleToSource
mf
Map TopLevelModuleName ModuleInfo -> TCM ()
setVisitedModules Map TopLevelModuleName ModuleInfo
vs
Signature
-> BuiltinThings PrimFun
-> PatternSynDefns
-> DisplayForms
-> Map QName String
-> Set QName
-> [TCWarning]
-> TCM ()
addImportedThings Signature
isig BuiltinThings PrimFun
ibuiltin PatternSynDefns
ipatsyns DisplayForms
display Map QName String
userwarn Set QName
partialdefs []
(Interface, MaybeWarnings)
r <- TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a. TCM a -> TCM a
withMsgs (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ SourceFile
-> TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
createInterface SourceFile
file TopLevelModuleName
x MainInterface
isMain Maybe SourceInfo
msi
ModuleToSource
mf <- Lens' ModuleToSource TCState -> TCMT IO ModuleToSource
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' ModuleToSource TCState
stModuleToSource
DecodedModules
ds <- TCM DecodedModules
getDecodedModules
((Interface, MaybeWarnings), TCM ())
-> TCM ((Interface, MaybeWarnings), TCM ())
forall (m :: * -> *) a. Monad m => a -> m a
return ((Interface, MaybeWarnings)
r, do
Lens' ModuleToSource TCState
stModuleToSource Lens' ModuleToSource TCState -> ModuleToSource -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` ModuleToSource
mf
DecodedModules -> TCM ()
setDecodedModules DecodedModules
ds
case (Interface, MaybeWarnings)
r of
(i :: Interface
i, NoWarnings) -> Interface -> TCM ()
storeDecodedModule Interface
i
_ -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
)
case Either TCErr ((Interface, MaybeWarnings), TCM ())
r of
Left err :: TCErr
err -> TCErr -> TCM (Bool, (Interface, MaybeWarnings))
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
err
Right (r :: (Interface, MaybeWarnings)
r, update :: TCM ()
update) -> do
TCM ()
update
case (Interface, MaybeWarnings)
r of
(_, NoWarnings) ->
TopLevelModuleName
-> SourceFile
-> MainInterface
-> Maybe SourceInfo
-> TCM (Bool, (Interface, MaybeWarnings))
getStoredInterface TopLevelModuleName
x SourceFile
file MainInterface
isMain Maybe SourceInfo
msi
_ -> (Bool, (Interface, MaybeWarnings))
-> TCM (Bool, (Interface, MaybeWarnings))
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, (Interface, MaybeWarnings)
r)
chaseMsg
:: String
-> C.TopLevelModuleName
-> Maybe String
-> TCM ()
chaseMsg :: String -> TopLevelModuleName -> Maybe String -> TCM ()
chaseMsg kind :: String
kind x :: TopLevelModuleName
x file :: Maybe String
file = do
String
indentation <- (Int -> Char -> String
forall a. Int -> a -> [a]
`replicate` ' ') (Int -> String) -> TCMT IO Int -> TCMT IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Int) -> TCMT IO Int
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Int
envModuleNestingLevel
let maybeFile :: String
maybeFile = Maybe String -> String -> ShowS -> String
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe String
file "." (ShowS -> String) -> ShowS -> String
forall a b. (a -> b) -> a -> b
$ \ f :: String
f -> " (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")."
vLvl :: Int
vLvl | String
kind String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "Checking" = 1
| Bool
otherwise = 2
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.chase" Int
vLvl (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ String
indentation, String
kind, " ", TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
x, String
maybeFile ]
highlightFromInterface
:: Interface
-> SourceFile
-> TCM ()
highlightFromInterface :: Interface -> SourceFile -> TCM ()
highlightFromInterface i :: Interface
i file :: SourceFile
file = do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
"Generating syntax info for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> String
filePath (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) String -> ShowS
forall a. [a] -> [a] -> [a]
++
" (read from interface)."
RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (Interface -> HighlightingInfo
iHighlighting Interface
i)
readInterface :: AbsolutePath -> TCM (Maybe Interface)
readInterface :: AbsolutePath -> TCM (Maybe Interface)
readInterface file :: AbsolutePath
file = MaybeT TCM Interface -> TCM (Maybe Interface)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT TCM Interface -> TCM (Maybe Interface))
-> MaybeT TCM Interface -> TCM (Maybe Interface)
forall a b. (a -> b) -> a -> b
$ do
InterfaceFile
ifile <- TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile)
-> TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile
forall a b. (a -> b) -> a -> b
$ IO (Maybe InterfaceFile) -> TCMT IO (Maybe InterfaceFile)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe InterfaceFile) -> TCMT IO (Maybe InterfaceFile))
-> IO (Maybe InterfaceFile) -> TCMT IO (Maybe InterfaceFile)
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> IO (Maybe InterfaceFile)
mkInterfaceFile AbsolutePath
file
TCM (Maybe Interface) -> MaybeT TCM Interface
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCM (Maybe Interface) -> MaybeT TCM Interface)
-> TCM (Maybe Interface) -> MaybeT TCM Interface
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> TCM (Maybe Interface)
readInterface' InterfaceFile
ifile
readInterface' :: InterfaceFile -> TCM (Maybe Interface)
readInterface' :: InterfaceFile -> TCM (Maybe Interface)
readInterface' file :: InterfaceFile
file = do
let ifp :: String
ifp = AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> AbsolutePath
intFilePath InterfaceFile
file
(s :: ByteString
s, close :: IO ()
close) <- IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ())
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ()))
-> IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ())
forall a b. (a -> b) -> a -> b
$ String -> IO (ByteString, IO ())
readBinaryFile' String
ifp
do Maybe Interface
mi <- IO (Maybe Interface) -> TCM (Maybe Interface)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe Interface) -> TCM (Maybe Interface))
-> (Maybe Interface -> IO (Maybe Interface))
-> Maybe Interface
-> TCM (Maybe Interface)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Interface -> IO (Maybe Interface)
forall a. a -> IO a
E.evaluate (Maybe Interface -> TCM (Maybe Interface))
-> TCM (Maybe Interface) -> TCM (Maybe Interface)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ByteString -> TCM (Maybe Interface)
decodeInterface ByteString
s
IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ()
close
Maybe Interface -> TCM (Maybe Interface)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Interface -> TCM (Maybe Interface))
-> Maybe Interface -> TCM (Maybe Interface)
forall a b. (a -> b) -> a -> b
$ Interface -> Interface
constructIScope (Interface -> Interface) -> Maybe Interface -> Maybe Interface
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Interface
mi
TCM (Maybe Interface)
-> (TCErr -> TCM (Maybe Interface)) -> TCM (Maybe Interface)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \e :: TCErr
e -> IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ()
close TCM () -> TCM (Maybe Interface) -> TCM (Maybe Interface)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TCErr -> TCM (Maybe Interface)
forall (m :: * -> *) a.
(MonadDebug m, MonadError TCErr m) =>
TCErr -> m (Maybe a)
handler TCErr
e
TCM (Maybe Interface)
-> (TCErr -> TCM (Maybe Interface)) -> TCM (Maybe Interface)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` TCErr -> TCM (Maybe Interface)
forall (m :: * -> *) a.
(MonadDebug m, MonadError TCErr m) =>
TCErr -> m (Maybe a)
handler
where
handler :: TCErr -> m (Maybe a)
handler e :: TCErr
e = case TCErr
e of
IOException _ _ e :: IOException
e -> do
String -> Int -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "" 0 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "IO exception: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ IOException -> String
forall a. Show a => a -> String
show IOException
e
Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
_ -> TCErr -> m (Maybe a)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
e
writeInterface :: AbsolutePath -> Interface -> TCM Interface
writeInterface :: AbsolutePath -> Interface -> TCMT IO Interface
writeInterface file :: AbsolutePath
file i :: Interface
i = let fp :: String
fp = AbsolutePath -> String
filePath AbsolutePath
file in do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.write" 5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
"Writing interface file " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fp String -> ShowS
forall a. [a] -> [a] -> [a]
++ "."
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.write" 50 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
"Writing interface file with hash" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Hash -> String
forall a. Show a => a -> String
show (Interface -> Hash
iFullHash Interface
i) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "."
ByteString
i' <- String -> Interface -> TCM ByteString
encodeFile String
fp Interface
i
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.write" 5 "Wrote interface file."
Maybe Interface
i <-
#if __GLASGOW_HASKELL__ >= 804
Account Phase -> TCM (Maybe Interface) -> TCM (Maybe Interface)
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Deserialization] (ByteString -> TCM (Maybe Interface)
forall a. EmbPrj a => ByteString -> TCM (Maybe a)
decode ByteString
i')
#else
return (Just i)
#endif
case Maybe Interface
i of
Just i :: Interface
i -> Interface -> TCMT IO Interface
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i
Nothing -> TCMT IO Interface
forall a. HasCallStack => a
__IMPOSSIBLE__
TCMT IO Interface
-> (TCErr -> TCMT IO Interface) -> TCMT IO Interface
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \e :: TCErr
e -> do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "" 1 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
"Failed to write interface " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fp String -> ShowS
forall a. [a] -> [a] -> [a]
++ "."
IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$
IO Bool -> IO () -> IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (String -> IO Bool
doesFileExist String
fp) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
removeFile String
fp
TCErr -> TCMT IO Interface
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError TCErr
e
removePrivates :: ScopeInfo -> ScopeInfo
removePrivates :: ScopeInfo -> ScopeInfo
removePrivates = Lens' (Map ModuleName Scope) ScopeInfo
-> LensMap (Map ModuleName Scope) ScopeInfo
forall i o. Lens' i o -> LensMap i o
over Lens' (Map ModuleName Scope) ScopeInfo
scopeModules LensMap (Map ModuleName Scope) ScopeInfo
-> LensMap (Map ModuleName Scope) ScopeInfo
forall a b. (a -> b) -> a -> b
$ (Scope -> Scope) -> Map ModuleName Scope -> Map ModuleName Scope
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Scope -> Scope
restrictPrivate
concreteOptionsToOptionPragmas :: [C.Pragma] -> TCM [OptionsPragma]
concreteOptionsToOptionPragmas :: [Pragma] -> TCM [[String]]
concreteOptionsToOptionPragmas p :: [Pragma]
p = do
[Pragma]
pragmas <- [[Pragma]] -> [Pragma]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Pragma]] -> [Pragma]) -> TCMT IO [[Pragma]] -> TCMT IO [Pragma]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pragma] -> TCMT IO [[Pragma]]
forall c a. ToAbstract c a => c -> ScopeM a
concreteToAbstract_ [Pragma]
p
let getOptions :: Pragma -> Maybe [String]
getOptions (A.OptionsPragma opts :: [String]
opts) = [String] -> Maybe [String]
forall a. a -> Maybe a
Just [String]
opts
getOptions _ = Maybe [String]
forall a. Maybe a
Nothing
[[String]] -> TCM [[String]]
forall (m :: * -> *) a. Monad m => a -> m a
return ([[String]] -> TCM [[String]]) -> [[String]] -> TCM [[String]]
forall a b. (a -> b) -> a -> b
$ (Pragma -> Maybe [String]) -> [Pragma] -> [[String]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Pragma -> Maybe [String]
getOptions [Pragma]
pragmas
createInterface
:: SourceFile
-> C.TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
createInterface :: SourceFile
-> TopLevelModuleName
-> MainInterface
-> Maybe SourceInfo
-> TCM (Interface, MaybeWarnings)
createInterface file :: SourceFile
file mname :: TopLevelModuleName
mname isMain :: MainInterface
isMain msi :: Maybe SourceInfo
msi =
Account Phase
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [TopLevelModuleName -> Phase
Bench.TopModule TopLevelModuleName
mname] (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$
(TCEnv -> TCEnv)
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\e :: TCEnv
e -> TCEnv
e { envCurrentPath :: Maybe AbsolutePath
envCurrentPath = AbsolutePath -> Maybe AbsolutePath
forall a. a -> Maybe a
Just (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) }) (TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> TCM (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 5 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
"Creating interface for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow TopLevelModuleName
mname String -> ShowS
forall a. [a] -> [a] -> [a]
++ "."
String -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS "import.iface.create" 10 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
[TopLevelModuleName]
visited <- Map TopLevelModuleName ModuleInfo -> [TopLevelModuleName]
forall k a. Map k a -> [k]
Map.keys (Map TopLevelModuleName ModuleInfo -> [TopLevelModuleName])
-> TCMT IO (Map TopLevelModuleName ModuleInfo)
-> TCMT IO [TopLevelModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Map TopLevelModuleName ModuleInfo)
getVisitedModules
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 10 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$
" visited: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate ", " ((TopLevelModuleName -> String) -> [TopLevelModuleName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow [TopLevelModuleName]
visited)
(source :: Text
source, fileType :: FileType
fileType, (pragmas :: [Pragma]
pragmas, top :: [Declaration]
top)) <- do
SourceInfo
si <- case Maybe SourceInfo
msi of
Nothing -> SourceFile -> TCM SourceInfo
sourceInfo SourceFile
file
Just si :: SourceInfo
si -> SourceInfo -> TCM SourceInfo
forall (m :: * -> *) a. Monad m => a -> m a
return SourceInfo
si
case SourceInfo
si of
SourceInfo {..} -> (Text, FileType, Module) -> TCMT IO (Text, FileType, Module)
forall (m :: * -> *) a. Monad m => a -> m a
return (Text
siSource, FileType
siFileType, Module
siModule)
ModuleToSource
modFile <- Lens' ModuleToSource TCState -> TCMT IO ModuleToSource
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' ModuleToSource TCState
stModuleToSource
HighlightingInfo
fileTokenInfo <- Account Phase
-> TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Highlighting] (TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo)
-> TCMT IO HighlightingInfo -> TCMT IO HighlightingInfo
forall a b. (a -> b) -> a -> b
$
AbsolutePath -> String -> TCMT IO HighlightingInfo
generateTokenInfoFromSource
(SourceFile -> AbsolutePath
srcFilePath SourceFile
file) (Text -> String
T.unpack Text
source)
Lens' HighlightingInfo TCState
stTokens Lens' HighlightingInfo TCState -> HighlightingInfo -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` HighlightingInfo
fileTokenInfo
[[String]]
options <- [Pragma] -> TCM [[String]]
concreteOptionsToOptionPragmas [Pragma]
pragmas
([String] -> TCM ()) -> [[String]] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [String] -> TCM ()
setOptionsFromPragma [[String]]
options
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Starting scope checking."
TopLevelInfo
topLevel <- Account Phase -> TCMT IO TopLevelInfo -> TCMT IO TopLevelInfo
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Scoping] (TCMT IO TopLevelInfo -> TCMT IO TopLevelInfo)
-> TCMT IO TopLevelInfo -> TCMT IO TopLevelInfo
forall a b. (a -> b) -> a -> b
$
TopLevel [Declaration] -> TCMT IO TopLevelInfo
forall c a. ToAbstract c a => c -> ScopeM a
concreteToAbstract_ (AbsolutePath
-> TopLevelModuleName -> [Declaration] -> TopLevel [Declaration]
forall a. AbsolutePath -> TopLevelModuleName -> a -> TopLevel a
TopLevel (SourceFile -> AbsolutePath
srcFilePath SourceFile
file) TopLevelModuleName
mname [Declaration]
top)
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Finished scope checking."
let ds :: [Declaration]
ds = TopLevelInfo -> [Declaration]
topLevelDecls TopLevelInfo
topLevel
scope :: ScopeInfo
scope = TopLevelInfo -> ScopeInfo
topLevelScope TopLevelInfo
topLevel
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Starting highlighting from scope."
Account Phase -> TCM () -> TCM ()
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Highlighting] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting HighlightingInfo
fileTokenInfo
let onlyScope :: Bool
onlyScope = MainInterface
isMain MainInterface -> MainInterface -> Bool
forall a. Eq a => a -> a -> Bool
== Mode -> MainInterface
MainInterface Mode
ScopeCheck
HighlightingLevel -> Bool -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> Bool -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIsOr HighlightingLevel
NonInteractive Bool
onlyScope (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
(Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ d :: Declaration
d -> Declaration -> Level -> Bool -> TCM ()
generateAndPrintSyntaxInfo Declaration
d Level
Partial Bool
onlyScope) [Declaration]
ds
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Finished highlighting from scope."
TCM ()
forall (m :: * -> *).
(HasOptions m, MonadDebug m, MonadTCState m) =>
m ()
activateLoadedFileCache
TCM ()
forall (m :: * -> *). (MonadTCState m, ReadTCState m) => m ()
cachingStarts
PragmaOptions
opts <- Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PragmaOptions TCState
stPragmaOptions
Maybe (TypeCheckAction, PostScopeState)
me <- TCMT IO (Maybe (TypeCheckAction, PostScopeState))
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
m (Maybe (TypeCheckAction, PostScopeState))
readFromCachedLog
case Maybe (TypeCheckAction, PostScopeState)
me of
Just (Pragmas opts' :: PragmaOptions
opts', _) | PragmaOptions
opts PragmaOptions -> PragmaOptions -> Bool
forall a. Eq a => a -> a -> Bool
== PragmaOptions
opts'
-> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
_ -> do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "cache" 10 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ "pragma changed: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show (Maybe (TypeCheckAction, PostScopeState) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (TypeCheckAction, PostScopeState)
me)
TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cleanCachedLog
TypeCheckAction -> TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCState m, ReadTCState m) =>
TypeCheckAction -> m ()
writeToCurrentLog (TypeCheckAction -> TCM ()) -> TypeCheckAction -> TCM ()
forall a b. (a -> b) -> a -> b
$ PragmaOptions -> TypeCheckAction
Pragmas PragmaOptions
opts
case MainInterface
isMain of
MainInterface ScopeCheck -> do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Skipping type checking."
TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cacheCurrentLog
_ -> do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Starting type checking."
Account Phase -> TCM () -> TCM ()
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Typing] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (Declaration -> TCM ()) -> [Declaration] -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Declaration -> TCM ()
checkDeclCached [Declaration]
ds TCM () -> TCM () -> TCM ()
forall a b. TCM a -> TCM b -> TCM a
`finally_` TCM ()
forall (m :: * -> *). (MonadDebug m, MonadTCState m) => m ()
cacheCurrentLog
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Finished type checking."
TCM ()
unfreezeMetas
String -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS "profile.metas" 10 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
MetaId n :: Int
n <- TCMT IO MetaId
forall i (m :: * -> *). MonadFresh i m => m i
fresh
String -> Integer -> TCM ()
forall (m :: * -> *).
MonadStatistics m =>
String -> Integer -> m ()
tickN "metas" (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n)
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Starting highlighting from type info."
Account Phase -> TCM () -> TCM ()
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Highlighting] (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
HighlightingInfo
toks <- Lens' HighlightingInfo TCState -> TCMT IO HighlightingInfo
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' HighlightingInfo TCState
stTokens
HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting HighlightingInfo
toks
Lens' HighlightingInfo TCState
stTokens Lens' HighlightingInfo TCState -> HighlightingInfo -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` HighlightingInfo
forall a. Monoid a => a
mempty
[TCWarning]
warnings <- WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
warnings) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc "import.iface.create" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
"collected warnings: " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> [TCWarning] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
warnings
[TCWarning]
unsolved <- TCMT IO [TCWarning]
getAllUnsolved
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
unsolved) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc "import.iface.create" 20 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$
"collected unsolved: " TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> [TCWarning] -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [TCWarning]
unsolved
let warningInfo :: HighlightingInfo
warningInfo = File -> HighlightingInfo
compress (File -> HighlightingInfo) -> File -> HighlightingInfo
forall a b. (a -> b) -> a -> b
$ (TCWarning -> File) -> [TCWarning] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TCWarning -> File
warningHighlighting ([TCWarning] -> File) -> [TCWarning] -> File
forall a b. (a -> b) -> a -> b
$ [TCWarning]
unsolved [TCWarning] -> [TCWarning] -> [TCWarning]
forall a. [a] -> [a] -> [a]
++ [TCWarning]
warnings
Lens' HighlightingInfo TCState
stSyntaxInfo Lens' HighlightingInfo TCState
-> (HighlightingInfo -> HighlightingInfo) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` \inf :: HighlightingInfo
inf -> (HighlightingInfo
inf HighlightingInfo -> HighlightingInfo -> HighlightingInfo
forall a. Monoid a => a -> a -> a
`mappend` HighlightingInfo
toks) HighlightingInfo -> HighlightingInfo -> HighlightingInfo
forall a. Monoid a => a -> a -> a
`mappend` HighlightingInfo
warningInfo
TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (CommandLineOptions -> Bool
optGenerateVimFile (CommandLineOptions -> Bool)
-> TCMT IO CommandLineOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
ScopeInfo -> TCM () -> TCM ()
forall (m :: * -> *) a. ReadTCState m => ScopeInfo -> m a -> m a
withScope_ ScopeInfo
scope (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TCM ()
generateVimFile (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ SourceFile -> AbsolutePath
srcFilePath (SourceFile -> AbsolutePath) -> SourceFile -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ SourceFile
file
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Finished highlighting from type info."
ScopeInfo -> TCM ()
setScope ScopeInfo
scope
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "scope.top" 50 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ "SCOPE " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ScopeInfo -> String
forall a. Show a => a -> String
show ScopeInfo
scope
[MetaId]
openMetas <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([MetaId] -> Bool
forall a. Null a => a -> Bool
null [MetaId]
openMetas) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.metas" 10 "We have unsolved metas."
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.metas" 10 (String -> TCM ()) -> TCMT IO String -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Goals -> TCMT IO String
showGoals (Goals -> TCMT IO String) -> TCMT IO Goals -> TCMT IO String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Goals
getGoals
HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive TCM ()
printUnsolvedInfo
Bool
allowUnsolved <- PragmaOptions -> Bool
optAllowUnsolved (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MainInterface -> Bool
includeStateChanges MainInterface
isMain) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
allowUnsolved (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Turning unsolved metas (if any) into postulates."
ModuleName -> TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => ModuleName -> m a -> m a
withCurrentModule (ScopeInfo
scope ScopeInfo -> Lens' ModuleName ScopeInfo -> ModuleName
forall o i. o -> Lens' i o -> i
^. Lens' ModuleName ScopeInfo
scopeCurrent) TCM ()
openMetasToPostulates
Lens' Constraints TCState
stAwakeConstraints Lens' Constraints TCState -> Constraints -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` []
Lens' Constraints TCState
stSleepingConstraints Lens' Constraints TCState -> Constraints -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` []
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Starting serialization."
Interface
i <- Account Phase -> TCMT IO Interface -> TCMT IO Interface
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Serialization, Phase
Bench.BuildInterface] (TCMT IO Interface -> TCMT IO Interface)
-> TCMT IO Interface -> TCMT IO Interface
forall a b. (a -> b) -> a -> b
$
Text -> FileType -> TopLevelInfo -> [[String]] -> TCMT IO Interface
buildInterface Text
source FileType
fileType TopLevelInfo
topLevel [[String]]
options
String -> Int -> [String] -> TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
String -> Int -> a -> m ()
reportS "tc.top" 101 ([String] -> TCM ()) -> [String] -> TCM ()
forall a b. (a -> b) -> a -> b
$
"Signature:" String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
[ [String] -> String
unlines
[ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x
, " type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show (Definition -> Type
defType Definition
def)
, " def: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe CompiledClauses -> String
forall a. Show a => a -> String
show Maybe CompiledClauses
cc
]
| (x :: QName
x, def :: Definition
def) <- HashMap QName Definition -> [(QName, Definition)]
forall k v. HashMap k v -> [(k, v)]
HMap.toList (HashMap QName Definition -> [(QName, Definition)])
-> HashMap QName Definition -> [(QName, Definition)]
forall a b. (a -> b) -> a -> b
$ Interface -> Signature
iSignature Interface
i Signature
-> Lens' (HashMap QName Definition) Signature
-> HashMap QName Definition
forall o i. o -> Lens' i o -> i
^. Lens' (HashMap QName Definition) Signature
sigDefinitions,
Function{ funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Maybe CompiledClauses
cc } <- [Definition -> Defn
theDef Definition
def]
]
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Finished serialization."
MaybeWarnings
mallWarnings <- MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' MainInterface
isMain WhichWarnings
ErrorWarnings
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Considering writing to interface file."
Interface
i <- case (MaybeWarnings
mallWarnings, MainInterface
isMain) of
(SomeWarnings allWarnings :: [TCWarning]
allWarnings, _) -> do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "We have warnings, skipping writing interface file."
Interface -> TCMT IO Interface
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i
(_, MainInterface ScopeCheck) -> do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "We are just scope-checking, skipping writing interface file."
Interface -> TCMT IO Interface
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i
_ -> Account Phase -> TCMT IO Interface -> TCMT IO Interface
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
Bench.billTo [Phase
Bench.Serialization] (TCMT IO Interface -> TCMT IO Interface)
-> TCMT IO Interface -> TCMT IO Interface
forall a b. (a -> b) -> a -> b
$ do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Actually calling writeInterface."
AbsolutePath
ifile <- SourceFile -> TCM AbsolutePath
toIFile SourceFile
file
AbsolutePath -> Interface -> TCMT IO Interface
writeInterface AbsolutePath
ifile Interface
i
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface.create" 7 "Finished (or skipped) writing to interface file."
Int -> Maybe TopLevelModuleName -> Statistics -> TCM ()
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, HasOptions m) =>
Int -> Maybe TopLevelModuleName -> Statistics -> m ()
printStatistics 30 (TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just TopLevelModuleName
mname) (Statistics -> TCM ()) -> TCMT IO Statistics -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Statistics
forall (m :: * -> *). ReadTCState m => m Statistics
getStatistics
Statistics
localStatistics <- TCMT IO Statistics
forall (m :: * -> *). ReadTCState m => m Statistics
getStatistics
Lens' Statistics TCState
lensAccumStatistics Lens' Statistics TCState -> (Statistics -> Statistics) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` (Integer -> Integer -> Integer)
-> Statistics -> Statistics -> Statistics
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) Statistics
localStatistics
String -> Int -> TCM () -> TCM ()
forall (m :: * -> *). MonadDebug m => String -> Int -> m () -> m ()
verboseS "profile" 1 (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 5 "Accumulated statistics."
(Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings))
-> (Interface, MaybeWarnings) -> TCM (Interface, MaybeWarnings)
forall a b. (a -> b) -> a -> b
$ (Interface -> Interface)
-> (Interface, MaybeWarnings) -> (Interface, MaybeWarnings)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Interface -> Interface
constructIScope (Interface
i, MaybeWarnings
mallWarnings)
getUniqueMetasRanges :: [MetaId] -> TCM [Range]
getUniqueMetasRanges :: [MetaId] -> TCM [Range]
getUniqueMetasRanges = ([Range] -> [Range]) -> TCM [Range] -> TCM [Range]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Range -> Range) -> [Range] -> [Range]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn Range -> Range
forall a. a -> a
id) (TCM [Range] -> TCM [Range])
-> ([MetaId] -> TCM [Range]) -> [MetaId] -> TCM [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MetaId -> TCMT IO Range) -> [MetaId] -> TCM [Range]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM MetaId -> TCMT IO Range
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange
getUnsolvedMetas :: TCM [Range]
getUnsolvedMetas :: TCM [Range]
getUnsolvedMetas = do
[MetaId]
openMetas <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
[MetaId]
interactionMetas <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
[MetaId] -> TCM [Range]
getUniqueMetasRanges ([MetaId]
openMetas [MetaId] -> [MetaId] -> [MetaId]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [MetaId]
interactionMetas)
getAllUnsolved :: TCM [TCWarning]
getAllUnsolved :: TCMT IO [TCWarning]
getAllUnsolved = do
[Range]
unsolvedInteractions <- [MetaId] -> TCM [Range]
getUniqueMetasRanges ([MetaId] -> TCM [Range]) -> TCMT IO [MetaId] -> TCM [Range]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
Constraints
unsolvedConstraints <- TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints
[Range]
unsolvedMetas <- TCM [Range]
getUnsolvedMetas
let checkNonEmpty :: (a -> a) -> a -> f a
checkNonEmpty c :: a -> a
c rs :: a
rs = a -> a
c a
rs a -> f () -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> f ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a -> Bool
forall a. Null a => a -> Bool
null a
rs)
(Warning -> TCMT IO TCWarning) -> [Warning] -> TCMT IO [TCWarning]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Warning -> TCMT IO TCWarning
forall (m :: * -> *). MonadWarning m => Warning -> m TCWarning
warning_ ([Warning] -> TCMT IO [TCWarning])
-> [Warning] -> TCMT IO [TCWarning]
forall a b. (a -> b) -> a -> b
$ [Maybe Warning] -> [Warning]
forall a. [Maybe a] -> [a]
catMaybes
[ ([Range] -> Warning) -> [Range] -> Maybe Warning
forall (f :: * -> *) a a.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty [Range] -> Warning
UnsolvedInteractionMetas [Range]
unsolvedInteractions
, ([Range] -> Warning) -> [Range] -> Maybe Warning
forall (f :: * -> *) a a.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty [Range] -> Warning
UnsolvedMetaVariables [Range]
unsolvedMetas
, (Constraints -> Warning) -> Constraints -> Maybe Warning
forall (f :: * -> *) a a.
(Alternative f, Null a) =>
(a -> a) -> a -> f a
checkNonEmpty Constraints -> Warning
UnsolvedConstraints Constraints
unsolvedConstraints ]
getAllWarnings :: WhichWarnings -> TCM [TCWarning]
getAllWarnings :: WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings = MainInterface -> WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings' MainInterface
NotMainInterface
getAllWarnings' :: MainInterface -> WhichWarnings -> TCM [TCWarning]
getAllWarnings' :: MainInterface -> WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings' isMain :: MainInterface
isMain ww :: WhichWarnings
ww = do
[TCWarning]
unsolved <- TCMT IO [TCWarning]
getAllUnsolved
[TCWarning]
collectedTCWarnings <- Lens' [TCWarning] TCState -> TCMT IO [TCWarning]
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [TCWarning] TCState
stTCWarnings
let showWarn :: Warning -> Bool
showWarn w :: Warning
w = Warning -> WhichWarnings
classifyWarning Warning
w WhichWarnings -> WhichWarnings -> Bool
forall a. Ord a => a -> a -> Bool
<= WhichWarnings
ww Bool -> Bool -> Bool
&&
Bool -> Bool
not ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
unsolved Bool -> Bool -> Bool
&& Warning -> Bool
onlyShowIfUnsolved Warning
w)
([TCWarning] -> [TCWarning])
-> TCMT IO [TCWarning] -> TCMT IO [TCWarning]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Warning -> Bool
showWarn (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning))
(TCMT IO [TCWarning] -> TCMT IO [TCWarning])
-> TCMT IO [TCWarning] -> TCMT IO [TCWarning]
forall a b. (a -> b) -> a -> b
$ MainInterface -> [TCWarning] -> TCMT IO [TCWarning]
applyFlagsToTCWarnings' MainInterface
isMain ([TCWarning] -> TCMT IO [TCWarning])
-> [TCWarning] -> TCMT IO [TCWarning]
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> [TCWarning]
forall a. [a] -> [a]
reverse
([TCWarning] -> [TCWarning]) -> [TCWarning] -> [TCWarning]
forall a b. (a -> b) -> a -> b
$ [TCWarning]
unsolved [TCWarning] -> [TCWarning] -> [TCWarning]
forall a. [a] -> [a] -> [a]
++ [TCWarning]
collectedTCWarnings
getMaybeWarnings :: WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings :: WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings = MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' MainInterface
NotMainInterface
getMaybeWarnings' :: MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' :: MainInterface -> WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings' isMain :: MainInterface
isMain ww :: WhichWarnings
ww = do
[TCWarning]
allWarnings <- MainInterface -> WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings' MainInterface
isMain WhichWarnings
ww
MaybeWarnings -> TCM MaybeWarnings
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeWarnings -> TCM MaybeWarnings)
-> MaybeWarnings -> TCM MaybeWarnings
forall a b. (a -> b) -> a -> b
$ if [TCWarning] -> Bool
forall a. Null a => a -> Bool
null [TCWarning]
allWarnings
then MaybeWarnings
forall a. MaybeWarnings' a
NoWarnings
else [TCWarning] -> MaybeWarnings
forall a. a -> MaybeWarnings' a
SomeWarnings [TCWarning]
allWarnings
getAllWarningsOfTCErr :: TCErr -> TCM [TCWarning]
getAllWarningsOfTCErr :: TCErr -> TCMT IO [TCWarning]
getAllWarningsOfTCErr err :: TCErr
err = case TCErr
err of
TypeError tcst :: TCState
tcst cls :: Closure TypeError
cls -> case Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
cls of
NonFatalErrors{} -> [TCWarning] -> TCMT IO [TCWarning]
forall (m :: * -> *) a. Monad m => a -> m a
return []
_ -> TCMT IO [TCWarning] -> TCMT IO [TCWarning]
forall a. TCM a -> TCM a
localTCState (TCMT IO [TCWarning] -> TCMT IO [TCWarning])
-> TCMT IO [TCWarning] -> TCMT IO [TCWarning]
forall a b. (a -> b) -> a -> b
$ do
TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcst
[TCWarning]
ws <- WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
[TCWarning] -> TCMT IO [TCWarning]
forall (m :: * -> *) a. Monad m => a -> m a
return ([TCWarning] -> TCMT IO [TCWarning])
-> [TCWarning] -> TCMT IO [TCWarning]
forall a b. (a -> b) -> a -> b
$ (TCWarning -> Bool) -> [TCWarning] -> [TCWarning]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TCWarning -> Bool) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Warning -> Bool
isUnsolvedWarning (Warning -> Bool) -> (TCWarning -> Warning) -> TCWarning -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCWarning -> Warning
tcWarning) [TCWarning]
ws
_ -> [TCWarning] -> TCMT IO [TCWarning]
forall (m :: * -> *) a. Monad m => a -> m a
return []
constructIScope :: Interface -> Interface
constructIScope :: Interface -> Interface
constructIScope i :: Interface
i = Account Phase -> Interface -> Interface
forall a. Account Phase -> a -> a
billToPure [ Phase
Deserialization ] (Interface -> Interface) -> Interface -> Interface
forall a b. (a -> b) -> a -> b
$
Interface
i{ iScope :: Map ModuleName Scope
iScope = ScopeInfo -> Map ModuleName Scope
publicModules (ScopeInfo -> Map ModuleName Scope)
-> ScopeInfo -> Map ModuleName Scope
forall a b. (a -> b) -> a -> b
$ Interface -> ScopeInfo
iInsideScope Interface
i }
buildInterface
:: Text
-> FileType
-> TopLevelInfo
-> [OptionsPragma]
-> TCM Interface
buildInterface :: Text -> FileType -> TopLevelInfo -> [[String]] -> TCMT IO Interface
buildInterface source :: Text
source fileType :: FileType
fileType topLevel :: TopLevelInfo
topLevel pragmas :: [[String]]
pragmas = do
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 5 "Building interface..."
let m :: ModuleName
m = TopLevelInfo -> ModuleName
topLevelModuleName TopLevelInfo
topLevel
ScopeInfo
scope' <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
let scope :: ScopeInfo
scope = Lens' ModuleName ScopeInfo -> LensSet ModuleName ScopeInfo
forall i o. Lens' i o -> LensSet i o
set Lens' ModuleName ScopeInfo
scopeCurrent ModuleName
m ScopeInfo
scope'
BuiltinThings PrimFun
builtin <- Lens' (BuiltinThings PrimFun) TCState
-> TCMT IO (BuiltinThings PrimFun)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (BuiltinThings PrimFun) TCState
stLocalBuiltins
Set ModuleName
ms <- TCM (Set ModuleName)
getImports
[(ModuleName, Hash)]
mhs <- (ModuleName -> TCMT IO (ModuleName, Hash))
-> [ModuleName] -> TCMT IO [(ModuleName, Hash)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ m :: ModuleName
m -> (ModuleName
m,) (Hash -> (ModuleName, Hash))
-> TCMT IO Hash -> TCMT IO (ModuleName, Hash)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO Hash
moduleHash ModuleName
m) ([ModuleName] -> TCMT IO [(ModuleName, Hash)])
-> [ModuleName] -> TCMT IO [(ModuleName, Hash)]
forall a b. (a -> b) -> a -> b
$ Set ModuleName -> [ModuleName]
forall a. Set a -> [a]
Set.toList Set ModuleName
ms
Map String [ForeignCode]
foreignCode <- Lens' (Map String [ForeignCode]) TCState
-> TCMT IO (Map String [ForeignCode])
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map String [ForeignCode]) TCState
stForeignCode
DisplayForms
display <- ([LocalDisplayForm] -> Bool) -> DisplayForms -> DisplayForms
forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
HMap.filter (Bool -> Bool
not (Bool -> Bool)
-> ([LocalDisplayForm] -> Bool) -> [LocalDisplayForm] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [LocalDisplayForm] -> Bool
forall a. Null a => a -> Bool
null) (DisplayForms -> DisplayForms)
-> (DisplayForms -> DisplayForms) -> DisplayForms -> DisplayForms
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([LocalDisplayForm] -> [LocalDisplayForm])
-> DisplayForms -> DisplayForms
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HMap.map ((LocalDisplayForm -> Bool)
-> [LocalDisplayForm] -> [LocalDisplayForm]
forall a. (a -> Bool) -> [a] -> [a]
filter LocalDisplayForm -> Bool
forall a. Open a -> Bool
isClosed) (DisplayForms -> DisplayForms)
-> TCMT IO DisplayForms -> TCMT IO DisplayForms
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' DisplayForms TCState -> TCMT IO DisplayForms
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' DisplayForms TCState
stImportsDisplayForms
(display :: DisplayForms
display, sig :: Signature
sig) <- DisplayForms -> Signature -> TCM (DisplayForms, Signature)
eliminateDeadCode DisplayForms
display (Signature -> TCM (DisplayForms, Signature))
-> TCMT IO Signature -> TCM (DisplayForms, Signature)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Signature
forall (m :: * -> *). ReadTCState m => m Signature
getSignature
Map QName String
userwarns <- Lens' (Map QName String) TCState -> TCMT IO (Map QName String)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName String) TCState
stLocalUserWarnings
Maybe String
importwarn <- Lens' (Maybe String) TCState -> TCMT IO (Maybe String)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Maybe String) TCState
stWarningOnImport
HighlightingInfo
syntaxInfo <- Lens' HighlightingInfo TCState -> TCMT IO HighlightingInfo
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' HighlightingInfo TCState
stSyntaxInfo
PragmaOptions
optionsUsed <- Lens' PragmaOptions TCState -> TCMT IO PragmaOptions
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PragmaOptions TCState
stPragmaOptions
Set QName
partialDefs <- Lens' (Set QName) TCState -> TCMT IO (Set QName)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Set QName) TCState
stLocalPartialDefs
PatternSynDefns
patsyns <- PatternSynDefns -> PatternSynDefns
forall a. KillRange a => KillRangeT a
killRange (PatternSynDefns -> PatternSynDefns)
-> TCMT IO PatternSynDefns -> TCMT IO PatternSynDefns
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PatternSynDefns
forall (m :: * -> *). ReadTCState m => m PatternSynDefns
getPatternSyns
let builtin' :: Map String (Builtin (String, QName))
builtin' = (String -> Builtin PrimFun -> Builtin (String, QName))
-> BuiltinThings PrimFun -> Map String (Builtin (String, QName))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (\ x :: String
x b :: Builtin PrimFun
b -> (String
x,) (QName -> (String, QName))
-> (PrimFun -> QName) -> PrimFun -> (String, QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimFun -> QName
primFunName (PrimFun -> (String, QName))
-> Builtin PrimFun -> Builtin (String, QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Builtin PrimFun
b) BuiltinThings PrimFun
builtin
[TCWarning]
warnings <- WhichWarnings -> TCMT IO [TCWarning]
getAllWarnings WhichWarnings
AllWarnings
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 7 " instantiating all meta variables"
Interface
i <- Interface -> TCMT IO Interface
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Interface :: Hash
-> Text
-> FileType
-> [(ModuleName, Hash)]
-> ModuleName
-> Map ModuleName Scope
-> ScopeInfo
-> Signature
-> DisplayForms
-> Map QName String
-> Maybe String
-> Map String (Builtin (String, QName))
-> Map String [ForeignCode]
-> HighlightingInfo
-> [[String]]
-> PragmaOptions
-> PatternSynDefns
-> [TCWarning]
-> Set QName
-> Interface
Interface
{ iSourceHash :: Hash
iSourceHash = Text -> Hash
hashText Text
source
, iSource :: Text
iSource = Text
source
, iFileType :: FileType
iFileType = FileType
fileType
, iImportedModules :: [(ModuleName, Hash)]
iImportedModules = [(ModuleName, Hash)]
mhs
, iModuleName :: ModuleName
iModuleName = ModuleName
m
, iScope :: Map ModuleName Scope
iScope = Map ModuleName Scope
forall a. Null a => a
empty
, iInsideScope :: ScopeInfo
iInsideScope = TopLevelInfo -> ScopeInfo
topLevelScope TopLevelInfo
topLevel
, iSignature :: Signature
iSignature = Signature
sig
, iDisplayForms :: DisplayForms
iDisplayForms = DisplayForms
display
, iUserWarnings :: Map QName String
iUserWarnings = Map QName String
userwarns
, iImportWarning :: Maybe String
iImportWarning = Maybe String
importwarn
, iBuiltin :: Map String (Builtin (String, QName))
iBuiltin = Map String (Builtin (String, QName))
builtin'
, iForeignCode :: Map String [ForeignCode]
iForeignCode = Map String [ForeignCode]
foreignCode
, iHighlighting :: HighlightingInfo
iHighlighting = HighlightingInfo
syntaxInfo
, iPragmaOptions :: [[String]]
iPragmaOptions = [[String]]
pragmas
, iOptionsUsed :: PragmaOptions
iOptionsUsed = PragmaOptions
optionsUsed
, iPatternSyns :: PatternSynDefns
iPatternSyns = PatternSynDefns
patsyns
, iWarnings :: [TCWarning]
iWarnings = [TCWarning]
warnings
, iPartialDefs :: Set QName
iPartialDefs = Set QName
partialDefs
}
String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn "import.iface" 7 " interface complete"
Interface -> TCMT IO Interface
forall (m :: * -> *) a. Monad m => a -> m a
return Interface
i
getInterfaceFileHashes :: AbsolutePath -> TCM (Maybe (Hash, Hash))
getInterfaceFileHashes :: AbsolutePath -> TCMT IO (Maybe (Hash, Hash))
getInterfaceFileHashes fp :: AbsolutePath
fp = MaybeT TCM (Hash, Hash) -> TCMT IO (Maybe (Hash, Hash))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT TCM (Hash, Hash) -> TCMT IO (Maybe (Hash, Hash)))
-> MaybeT TCM (Hash, Hash) -> TCMT IO (Maybe (Hash, Hash))
forall a b. (a -> b) -> a -> b
$ do
InterfaceFile
mifile <- TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile)
-> TCMT IO (Maybe InterfaceFile) -> MaybeT TCM InterfaceFile
forall a b. (a -> b) -> a -> b
$ IO (Maybe InterfaceFile) -> TCMT IO (Maybe InterfaceFile)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe InterfaceFile) -> TCMT IO (Maybe InterfaceFile))
-> IO (Maybe InterfaceFile) -> TCMT IO (Maybe InterfaceFile)
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> IO (Maybe InterfaceFile)
mkInterfaceFile AbsolutePath
fp
TCMT IO (Maybe (Hash, Hash)) -> MaybeT TCM (Hash, Hash)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TCMT IO (Maybe (Hash, Hash)) -> MaybeT TCM (Hash, Hash))
-> TCMT IO (Maybe (Hash, Hash)) -> MaybeT TCM (Hash, Hash)
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> TCMT IO (Maybe (Hash, Hash))
getInterfaceFileHashes' InterfaceFile
mifile
getInterfaceFileHashes' :: InterfaceFile -> TCM (Maybe (Hash, Hash))
getInterfaceFileHashes' :: InterfaceFile -> TCMT IO (Maybe (Hash, Hash))
getInterfaceFileHashes' fp :: InterfaceFile
fp = do
let ifile :: String
ifile = AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ InterfaceFile -> AbsolutePath
intFilePath InterfaceFile
fp
(s :: ByteString
s, close :: IO ()
close) <- IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ())
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ()))
-> IO (ByteString, IO ()) -> TCMT IO (ByteString, IO ())
forall a b. (a -> b) -> a -> b
$ String -> IO (ByteString, IO ())
readBinaryFile' String
ifile
let hs :: Maybe (Hash, Hash)
hs = ByteString -> Maybe (Hash, Hash)
decodeHashes ByteString
s
IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Hash -> ((Hash, Hash) -> Hash) -> Maybe (Hash, Hash) -> Hash
forall b a. b -> (a -> b) -> Maybe a -> b
maybe 0 ((Hash -> Hash -> Hash) -> (Hash, Hash) -> Hash
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Hash -> Hash -> Hash
forall a. Num a => a -> a -> a
(+)) Maybe (Hash, Hash)
hs Hash -> IO () -> IO ()
forall a b. a -> b -> b
`seq` IO ()
close
Maybe (Hash, Hash) -> TCMT IO (Maybe (Hash, Hash))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Hash, Hash)
hs
moduleHash :: ModuleName -> TCM Hash
moduleHash :: ModuleName -> TCMT IO Hash
moduleHash m :: ModuleName
m = Interface -> Hash
iFullHash (Interface -> Hash) -> TCMT IO Interface -> TCMT IO Hash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCMT IO Interface
getInterface ModuleName
m
isNewerThan :: FilePath -> FilePath -> IO Bool
isNewerThan :: String -> String -> IO Bool
isNewerThan new :: String
new old :: String
old = do
Bool
newExist <- String -> IO Bool
doesFileExist String
new
Bool
oldExist <- String -> IO Bool
doesFileExist String
old
if Bool -> Bool
not (Bool
newExist Bool -> Bool -> Bool
&& Bool
oldExist)
then Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
newExist
else do
UTCTime
newT <- String -> IO UTCTime
getModificationTime String
new
UTCTime
oldT <- String -> IO UTCTime
getModificationTime String
old
Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ UTCTime
newT UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
>= UTCTime
oldT