39
40
import Agda.TypeChecking.Primitive
40
41
import Agda.TypeChecker
43
import Agda.Interaction.FindFile
42
44
import Agda.Interaction.Options
43
45
import Agda.Interaction.Highlighting.Precise (HighlightingInfo)
44
46
import Agda.Interaction.Highlighting.Generate
45
import Agda.Interaction.Highlighting.Emacs
46
47
import Agda.Interaction.Highlighting.Vim
47
48
import qualified Agda.Interaction.Highlighting.Range as R
49
50
import Agda.Utils.FileName
50
51
import Agda.Utils.Monad
52
import Agda.Utils.IO.Binary
53
import Agda.Utils.Pretty
53
55
import Agda.Utils.Impossible
54
56
#include "../undefined.h"
57
toIFile :: FilePath -> FilePath
58
toIFile = setExtension ".agdai"
58
-- | Which directory should form the base of relative include paths?
62
-- ^ The root directory of the \"project\" containing the current
65
-- ^ The current working directory.
67
-- | A variant of 'moduleName'' which raises an error if the file name
68
-- does not match the module name.
70
-- The file name is interpreted relative to the current working
71
-- directory (unless it is absolute).
73
moduleName :: FilePath -> TCM C.TopLevelModuleName
75
file <- liftIO (absolute file)
77
checkModuleName m file
80
-- | Computes the module name of the top-level module in the given
83
moduleName' :: AbsolutePath -> TCM C.TopLevelModuleName
84
moduleName' file = liftIO $ do
85
C.topLevelModuleName <$> parseFile' moduleParser file
60
87
-- | Merge an interface into the current proof state.
61
88
mergeInterface :: Interface -> TCM ()
88
111
PrimImpl _ pf <- lookupPrimitiveFunction x
89
112
return (x, Prim pf)
91
addImportedThings :: Signature -> BuiltinThings PrimFun -> TCM ()
92
addImportedThings isig ibuiltin =
115
Signature -> BuiltinThings PrimFun -> Set String -> TCM ()
116
addImportedThings isig ibuiltin hsImports =
93
117
modify $ \st -> st
94
118
{ stImports = unionSignatures [stImports st, isig]
95
119
, stImportedBuiltins = Map.union (stImportedBuiltins st) ibuiltin
120
, stHaskellImports = Set.union (stHaskellImports st) hsImports
98
data FileType = SourceFile | InterfaceFile
100
findFile :: FileType -> ModuleName -> TCM FilePath
102
let x = mnameToConcrete m
103
dirs <- getIncludeDirs
104
let files = [ dir ++ [slash] ++ file
106
, file <- map (C.moduleNameToFileName x) exts
108
files' <- liftIO $ filterM doesFileExist files
109
files' <- liftIO $ nubFiles files'
111
[] -> typeError $ FileNotFound m files
112
file:_ -> return file
115
SourceFile -> [".agda", ".lagda"]
116
InterfaceFile -> [".agdai"]
118
123
-- | Scope checks the given module. A proper version of the module
119
124
-- name (with correct definition sites) is returned.
121
126
scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope)
122
127
scopeCheckImport x = do
123
128
reportSLn "import.scope" 5 $ "Scope checking " ++ show x
124
visited <- Map.keys <$> getVisitedModules
125
reportSLn "import.scope" 10 $ " visited: " ++ show visited
126
(i,t) <- getInterface x
129
verboseS "import.scope" 10 $ do
130
visited <- Map.keys <$> getVisitedModules
131
liftIO $ LocIO.putStrLn $
132
" visited: " ++ intercalate ", " (map (render . pretty) visited)
133
i <- fst <$> getInterface x
128
135
return (iModuleName i `withRangesOfQ` mnameToConcrete x, iScope i)
130
alreadyVisited :: ModuleName -> TCM (Interface, ClockTime) -> TCM (Interface, ClockTime)
137
-- | If the module has already been visited (without warnings), then
138
-- its interface is returned directly. Otherwise the computation is
139
-- used to find the interface and the computed interface is stored for
140
-- potential later use.
142
alreadyVisited :: C.TopLevelModuleName ->
143
TCM (Interface, Either Warnings ClockTime) ->
144
TCM (Interface, Either Warnings ClockTime)
131
145
alreadyVisited x getIface = do
132
146
mm <- getVisitedModule x
135
reportSLn "import.visit" 10 $ " Already visited " ++ show x
138
reportSLn "import.visit" 5 $ " Getting interface for " ++ show x
140
reportSLn "import.visit" 5 $ " Now we've looked at " ++ show x
148
-- A module with warnings should never be allowed to be
149
-- imported from another module.
150
Just mi | not (miWarnings mi) -> do
151
reportSLn "import.visit" 10 $ " Already visited " ++ render (pretty x)
152
return (miInterface mi, Right $ miTimeStamp mi)
154
reportSLn "import.visit" 5 $ " Getting interface for " ++ render (pretty x)
155
r@(i, wt) <- getIface
156
reportSLn "import.visit" 5 $ " Now we've looked at " ++ render (pretty x)
159
t <- liftIO getClockTime
160
visitModule $ ModuleInfo
166
visitModule $ ModuleInfo
175
-- Invariant: The fields are never empty at the same time.
177
data Warnings = Warnings
178
{ terminationProblems :: [([QName], [R.Range])]
179
-- ^ Termination checking problems are not reported if
180
-- 'optTerminationCheck' is 'False'.
181
, unsolvedMetaVariables :: [Range]
182
-- ^ Meta-variable problems are reported as type errors unless
183
-- 'optAllowUnsolved' is 'True'.
184
, unsolvedConstraints :: Constraints
185
-- ^ Same as 'unsolvedMetaVariables'.
188
-- | Turns warnings into an error. Even if several errors are possible
189
-- only one is raised.
191
warningsToError :: Warnings -> TypeError
192
warningsToError (Warnings [] [] []) = __IMPOSSIBLE__
193
warningsToError (Warnings _ w@(_:_) _) = UnsolvedMetas w
194
warningsToError (Warnings _ _ w@(_:_)) = UnsolvedConstraints w
195
warningsToError (Warnings w@(_:_) _ _) = TerminationCheckFailed w
197
-- | Type checks the given module (if necessary).
199
-- The function also makes relative directories absolute, based on the
200
-- 'RelativeTo' argument. If this argument is 'ProjectRoot', then the
201
-- \"current file\" is taken to be the one given as the first
204
typeCheck :: FilePath
205
-- ^ The file name is interpreted relative to the current
206
-- working directory (unless it is absolute).
208
-> Maybe [AbsolutePath]
209
-- ^ If this argument is given, and it does not coincide
210
-- with the new value of the include directories (after
211
-- making them absolute), the state is reset (but the
212
-- command-line options are preserved).
213
-> TCM (Interface, Maybe Warnings)
214
typeCheck f relativeTo oldIncs = do
215
f <- liftIO (absolute f)
218
makeIncludeDirsAbsolute =<< case relativeTo of
219
CurrentDir -> liftIO (absolute =<< getCurrentDirectory)
220
ProjectRoot -> return $ C.projectRoot f m
222
-- If the include directories have changed the state is reset.
223
incs <- getIncludeDirs
225
Just incs' | incs' /= incs -> resetState
230
(i, wt) <- getInterface' m True
231
return (i, case wt of
235
-- | Tries to return the interface associated to the given module. The
236
-- time stamp of the relevant interface file is also returned. May
237
-- type check the module. An error is raised if a warning is
144
240
getInterface :: ModuleName -> TCM (Interface, ClockTime)
145
getInterface x = alreadyVisited x $ addImportCycleCheck x $ do
146
file <- findFile SourceFile x -- requires source to exist
242
(i, wt) <- getInterface' (toTopLevelModuleName x) False
244
Left w -> typeError $ warningsToError w
245
Right t -> return (i, t)
247
-- | A more precise variant of 'getInterface'. If warnings are
248
-- encountered then they are returned instead of being turned into
251
getInterface' :: C.TopLevelModuleName
252
-> Bool -- ^ If type checking is necessary, should all
253
-- state changes inflicted by 'createInterface'
255
-> TCM (Interface, Either Warnings ClockTime)
256
getInterface' x includeStateChanges =
257
-- Preserve the pragma options unless includeStateChanges is True.
258
bracket (stPragmaOptions <$> get)
259
(unless includeStateChanges .
260
setCommandLineOptions PragmaOptions) $ \_ -> do
261
-- Forget the pragma options (locally).
262
setCommandLineOptions PersistentOptions . stPersistentOptions =<< get
264
alreadyVisited x $ addImportCycleCheck x $ do
265
file <- findFile x -- requires source to exist
148
267
reportSLn "import.iface" 10 $ " Check for cycle"
149
268
checkForImportCycle
151
270
uptodate <- ifM ignoreInterfaces
153
(liftIO $ toIFile file `isNewerThan` file)
155
reportSLn "import.iface" 5 $ " " ++ show x ++ " is " ++ (if uptodate then "" else "not ") ++ "up-to-date."
272
(liftIO $ filePath (toIFile file)
276
reportSLn "import.iface" 5 $
277
" " ++ render (pretty x) ++ " is " ++
278
(if uptodate then "" else "not ") ++ "up-to-date."
280
(stateChangesIncluded, (i, wt)) <-
281
if uptodate then skip x file else typeCheck file
283
-- Ensure that the given module name matches the one in the file.
284
let topLevelName = toTopLevelModuleName $ iModuleName i
285
unless (topLevelName == x) $ do
286
checkModuleName topLevelName file
287
typeError $ OverlappingProjects file topLevelName x
161
289
visited <- isVisited x
162
290
reportSLn "import.iface" 5 $ if visited then " We've been here. Don't merge."
163
else " New module. Let's check it out."
164
unless visited $ mergeInterface i
166
storeDecodedModule x i t
291
else " New module. Let's check it out."
292
unless (visited || stateChangesIncluded) $ mergeInterface i
294
modify (\s -> s { stCurrentModule = Just $ iModuleName i })
296
-- Interfaces are only stored if no warnings were encountered.
299
Right t -> storeDecodedModule i t
171
305
-- Examine the mtime of the interface file. If it is newer than the
172
306
-- stored version (in stDecodedModules), or if there is no stored version,
173
307
-- read and decode it. Otherwise use the stored version.
174
let ifile = toIFile file
175
t <- liftIO $ getModificationTime ifile
176
mm <- getDecodedModule x
308
let ifile = filePath $ toIFile file
309
t <- liftIO $ getModificationTime ifile
310
mm <- getDecodedModule x
311
(cached, mi) <- case mm of
180
314
then do dropDecodedModule x
181
315
reportSLn "import.iface" 5 $ " file is newer, re-reading " ++ ifile
182
liftIO $ readInterface ifile
316
(,) False <$> readInterface ifile
183
317
else do reportSLn "import.iface" 5 $ " using stored version of " ++ ifile
318
return (True, Just mi)
186
320
do reportSLn "import.iface" 5 $ " no stored version, reading " ++ ifile
187
liftIO $ readInterface ifile
321
(,) False <$> readInterface ifile
189
323
-- Check that it's the right version
204
337
-- liftIO close -- Close the interface file. See above.
207
reportSLn "" 1 $ "Skipping " ++ show x ++ " (" ++ ifile ++ ")."
341
"Skipping " ++ render (pretty x) ++
342
" (" ++ (if cached then "cached" else ifile) ++ ")."
343
return (False, (i, Right t))
210
345
typeCheck file = do
211
-- Do the type checking
213
vs <- getVisitedModules
214
ds <- getDecodedModules
215
opts <- commandLineOptions
217
isig <- getImportedSignature
218
ibuiltin <- gets stImportedBuiltins
219
r <- liftIO $ runTCM $ -- Every interface should be
220
-- treated in isolation.
221
createInterface opts trace ms vs ds
222
isig ibuiltin (Just x) file False
225
Left err -> throwError err
226
Right (_, Warnings termErrs@(_:_) []) -> do
227
typeError $ TerminationCheckFailed termErrs
228
Right (_, Warnings _ _) -> __IMPOSSIBLE__
229
Right (_, Success vs ds i isig ibuiltin) -> do
230
-- writeInterface (used by createInterface) may
232
let ifile = toIFile file
233
t <- liftIO $ ifM (doesFileExist ifile)
234
(getModificationTime ifile)
238
-- We need to add things imported when checking
239
-- the imported modules.
240
addImportedThings isig ibuiltin
243
readInterface :: FilePath -> IO (Maybe Interface)
346
-- Do the type checking.
347
reportSLn "" 1 $ "Checking " ++ render (pretty x) ++ " (" ++ filePath file ++ ")."
348
if includeStateChanges then do
349
r <- createInterface file x
351
-- Merge the signature with the signature for imported
354
addImportedThings sig Map.empty Set.empty
355
setSignature emptySignature
360
mf <- stModuleToSource <$> get
361
vs <- getVisitedModules
362
ds <- getDecodedModules
363
opts <- stPersistentOptions <$> get
365
isig <- getImportedSignature
366
ibuiltin <- gets stImportedBuiltins
367
-- Every interface is treated in isolation.
368
r <- liftIO $ runTCM $
369
withImportPath ms $ do
372
setCommandLineOptions PersistentOptions opts
373
modify $ \s -> s { stModuleToSource = mf }
375
addImportedThings isig ibuiltin Set.empty
377
r <- createInterface file x
379
mf <- stModuleToSource <$> get
380
vs <- getVisitedModules
381
ds <- getDecodedModules
382
isig <- getImportedSignature
383
ibuiltin <- gets stImportedBuiltins
384
hsImports <- getHaskellImports
386
modify $ \s -> s { stModuleToSource = mf }
390
addImportedThings isig ibuiltin hsImports)
393
Left err -> throwError err
394
Right (result, update) -> do
396
return (False, result)
398
readInterface :: FilePath -> TCM (Maybe Interface)
244
399
readInterface file = do
245
400
-- Decode the interface file
246
(s, close) <- readBinaryFile' file
249
-- Force the entire string, to allow the file to be closed.
251
() <- when (n == n) $ return ()
256
-- Force the interface to make sure the interface version is looked at
257
i `seq` return $ Just i
401
(s, close) <- liftIO $ readBinaryFile' file
402
do i <- liftIO . E.evaluate =<< decode s
404
-- Close the file. Note
405
-- ⑴ that evaluate ensures that i is evaluated to WHNF (before
406
-- the next IO operation is executed), and
407
-- ⑵ that decode returns Nothing if an error is encountered,
408
-- so it is safe to close the file here.
258
412
-- Catch exceptions and close
259
`catch` \e -> close >> handler e
413
`catchError` \e -> liftIO close >> handler e
260
414
-- Catch exceptions
263
handler e = case e of
264
ErrorCall _ -> return Nothing
266
UTF8.putStrLn $ "IO exception: " ++ show e
267
return Nothing -- work-around for file locking bug
270
writeInterface :: FilePath -> Interface -> IO ()
417
handler e = case errError e of
418
IOException _ e -> do
419
liftIO $ LocIO.putStrLn $ "IO exception: " ++ show e
420
return Nothing -- Work-around for file locking bug.
421
-- TODO: What does this refer to? Please
425
-- | Writes the given interface to the given file. Returns the file's
426
-- new modification time stamp, or 'Nothing' if the write failed.
428
writeInterface :: FilePath -> Interface -> TCM ClockTime
271
429
writeInterface file i = do
272
430
encodeFile file i
274
UTF8.putStrLn $ "failed to write interface " ++ file ++ " : " ++ show e
279
data CreateInterfaceResult
280
= Success { cirVisited :: VisitedModules
281
, cirDecoded :: DecodedModules
282
, cirInterface :: Interface
283
, cirSignature :: Signature
284
, cirBuiltin :: BuiltinThings PrimFun
286
-- ^ Everything completed successfully, and an interface file was
288
| Warnings { terminationProblems :: [([QName], [R.Range])]
289
, unsolvedMetaVariables :: [Range]
291
-- ^ Type checking was successful, except for some termination
292
-- checking problems or unsolved meta-variables.
294
-- Meta-variable problems are reported as type errors unless we
295
-- are type checking a top-level module and the flag to allow
296
-- unsolved meta-variables has been selected.
431
liftIO $ getModificationTime file
432
`catchError` \e -> do
434
"Failed to write interface " ++ file ++ "."
436
whenM (doesFileExist file) $ removeFile file
439
-- | Tries to type check a module and write out its interface. The
440
-- function only writes out an interface file if it does not encounter
299
443
-- If appropriate this function writes out syntax highlighting
303
:: CommandLineOptions
309
-> BuiltinThings PrimFun
310
-> Maybe ModuleName -- ^ Expected module name.
311
-> FilePath -- ^ The file to type check.
312
-- Must be an absolute path.
313
-> Bool -- ^ Should the working directory be
314
-- changed to the root directory of
315
-- the \"project\" containing the
317
-> TCM (TopLevelInfo, CreateInterfaceResult)
318
createInterface opts trace path visited decoded
319
isig ibuiltin mname file changeDir
320
| not (isAbsolute file) = __IMPOSSIBLE__
321
| otherwise = withImportPath path $ do
322
setDecodedModules decoded
324
setCommandLineOptions opts
325
setVisitedModules visited
327
reportSLn "" 1 $ "Checking " ++ (case mname of
329
Just m -> show m ++ " (" ++ file ++ ")") ++ "."
330
reportSLn "import.iface.create" 5 $ "Creating interface for " ++ show mname
331
reportSLn "import.iface.create" 10 $ " visited: " ++ show (Map.keys visited)
333
addImportedThings isig ibuiltin
447
:: AbsolutePath -- ^ The file to type check.
448
-> C.TopLevelModuleName -- ^ The expected module name.
449
-> TCM (Interface, Either Warnings ClockTime)
450
createInterface file mname = do
451
reportSLn "import.iface.create" 5 $
452
"Creating interface for " ++ render (pretty mname) ++ "."
453
verboseS "import.iface.create" 10 $ do
454
visited <- Map.keys <$> getVisitedModules
455
liftIO $ LocIO.putStrLn $
456
" visited: " ++ intercalate ", " (map (render . pretty) visited)
458
previousHsImports <- getHaskellImports
335
460
(pragmas, top) <- liftIO $ parseFile' moduleParser file
337
liftIO $ setWorkingDirectory file top
338
462
pragmas <- concat <$> concreteToAbstract_ pragmas
339
463
-- identity for top-level pragmas at the moment
340
-- Note that pragmas can affect scope checking.
341
464
setOptionsFromPragmas pragmas
342
465
topLevel <- concreteToAbstract_ (TopLevel top)
344
467
termErrs <- catchError (do
345
checkModuleName mname file topLevel
347
468
-- Type checking.
348
469
checkDecls (topLevelDecls topLevel)
362
481
-- If there is an error syntax highlighting info can still be
363
-- generated. Since there is no Vim highlighting for errors no
364
-- Vim highlighting is generated, though.
365
whenM (optGenerateEmacsFile <$> commandLineOptions) $ do
367
generateSyntaxInfo file TypeCheckingNotDone topLevel []
483
case rStart $ getRange e of
484
Just (Pn { srcFile = Just f }) | f == file -> do
485
syntaxInfo <- generateSyntaxInfo file (Just e) topLevel []
486
modFile <- stModuleToSource <$> get
487
-- The highlighting info is included with the error.
488
case errHighlighting e of
489
Just _ -> __IMPOSSIBLE__
491
throwError $ e { errHighlighting =
492
Just (syntaxInfo, modFile) }
371
496
-- Generate syntax highlighting info.
372
syntaxInfo <- generateSyntaxInfo file TypeCheckingDone
376
whenM (optGenerateEmacsFile <$> commandLineOptions) $
377
writeEmacsFile syntaxInfo
497
syntaxInfo <- generateSyntaxInfo file Nothing topLevel termErrs
379
499
-- Generate Vim file.
380
500
whenM (optGenerateVimFile <$> commandLineOptions) $
381
withScope_ (insideScope topLevel) $ generateVimFile file
501
withScope_ (insideScope topLevel) $ generateVimFile $ filePath file
383
-- Check if there are unsolved meta-variables.
503
-- Check if there are unsolved meta-variables...
384
504
unsolvedMetas <- List.nub <$> (mapM getMetaRange =<< getOpenMetas)
385
case unsolvedMetas of
388
unsolvedOK <- optAllowUnsolved <$> commandLineOptions
389
unless (unsolvedOK && path == []) $ do
390
typeError $ UnsolvedMetas unsolvedMetas
505
unless (null unsolvedMetas) $ do
506
unsolvedOK <- optAllowUnsolved <$> commandLineOptions
508
typeError $ UnsolvedMetas unsolvedMetas
510
-- ...or unsolved constraints
511
unsolvedConstraints <- getConstraints
512
unless (null unsolvedConstraints) $ do
513
unsolvedOK <- optAllowUnsolved <$> commandLineOptions
515
typeError $ UnsolvedConstraints unsolvedConstraints
392
517
setScope $ outsideScope topLevel
394
519
reportSLn "scope.top" 50 $ "SCOPE " ++ show (insideScope topLevel)
396
-- True if the file was successfully and completely
398
let ok = null termErrs && null unsolvedMetas
521
i <- buildInterface topLevel syntaxInfo previousHsImports
400
(,) topLevel <$> if ok then do
401
i <- buildInterface (topLevelModuleName topLevel) syntaxInfo
402
isig <- getImportedSignature
403
vs <- getVisitedModules
404
ds <- getDecodedModules
405
ibuiltin <- gets stImportedBuiltins
406
liftIO $ writeInterface (toIFile file) i
407
modify (\s -> s { stCurrentModule =
408
Just (topLevelModuleName topLevel, i) })
409
return (Success vs ds i isig ibuiltin)
523
if and [ null termErrs, null unsolvedMetas, null unsolvedConstraints ]
525
-- The file was successfully type-checked (and no warnings were
526
-- encountered), so the interface should be written out.
527
t <- writeInterface (filePath $ toIFile file) i
411
return (Warnings termErrs unsolvedMetas)
530
return (i, Left $ Warnings termErrs unsolvedMetas unsolvedConstraints)
413
532
-- | Builds an interface for the current module, which should already
414
533
-- have been successfully type checked.
416
buildInterface :: ModuleName
417
-- ^ The name of the current module.
535
buildInterface :: TopLevelInfo
536
-- ^ 'TopLevelInfo' for the current module.
418
537
-> HighlightingInfo
419
538
-- ^ Syntax highlighting info for the module.
540
-- ^ Haskell modules imported in imported modules
421
buildInterface m syntaxInfo = do
543
buildInterface topLevel syntaxInfo previousHsImports = do
422
544
reportSLn "import.iface" 5 "Building interface..."
423
545
scope' <- getScope
424
546
let scope = scope' { scopeCurrent = m }
432
554
{ iImportedModules = Set.toList ms
433
555
, iModuleName = m
434
556
, iScope = publicModules scope
557
, iInsideScope = insideScope topLevel
435
558
, iSignature = sig
436
559
, iBuiltin = builtin'
437
, iHaskellImports = hsImps
560
, iHaskellImports = Set.difference hsImps
438
562
, iHighlighting = syntaxInfo
440
564
reportSLn "import.iface" 7 " interface complete"
445
setWorkingDirectory :: FilePath -> [C.Declaration] -> IO ()
446
setWorkingDirectory _ [] = __IMPOSSIBLE__
447
setWorkingDirectory file xs = case last xs of
448
C.Module _ n _ _ -> do
449
-- canonicalizePath seems to return absolute paths.
450
absolute <- canonicalizePath file
451
let (path, _, _) = splitFilePath absolute
452
setCurrentDirectory (dropDirectory (countDots n) path)
455
countDots (C.QName _) = 0
456
countDots (C.Qual _ n) = 1 + countDots n
458
matchFileName :: ModuleName -> FilePath -> Bool
459
matchFileName mname file = expected `isSuffixOf` given || literate `isSuffixOf` given
461
given = splitPath file
462
expected = splitPath $ C.moduleNameToFileName (mnameToConcrete mname) ".agda"
463
literate = splitPath $ C.moduleNameToFileName (mnameToConcrete mname) ".lagda"
467
:: Maybe ModuleName -- ^ The module should have this name (might be
469
-> FilePath -- ^ The module is defined in this file, whose
470
-- file name is known to be consistent with the
471
-- previous argument.
472
-> TopLevelInfo -- ^ The module.
474
checkModuleName mname file topLevel = case mname of
475
Nothing -> unless (matchFileName actualName file) err
476
Just expectedName -> unless (actualName == expectedName) err
478
actualName = topLevelModuleName topLevel
479
err = typeError $ ModuleNameDoesntMatchFileName actualName
566
where m = topLevelModuleName topLevel
481
568
-- | True if the first file is newer than the second file. If a file doesn't
482
569
-- exist it is considered to be infinitely old.
added
removed
src/full/Agda/Interaction/Imports.hs
