@@ -18,6 +18,10 @@ module Agda.Interaction.Imports
18 18
, scopeCheckImport
19 19
, parseSource
20 20
, typeCheckMain
21 +
, getNonMainInterface
22 +
, getNonMainModuleInfo
23 +
, getInterface
24 +
, importPrimitiveModules
21 25
, raiseNonFatalErrors
22 26 23 27
-- Currently only used by test/api/Issue1168.hs:
@@ -478,30 +482,9 @@ typeCheckMain mode src = do
478 482 479 483
-- For the main interface, we also remember the pragmas from the file
480 484
setOptionsFromSourcePragmas True src
481 -
loadPrims <- optLoadPrimitives <$> pragmaOptions
482 - 483 -
when loadPrims $ do
484 -
reportSLn "import.main" 10 "Importing the primitive modules."
485 -
libdirPrim <- useTC stPrimitiveLibDir
486 -
reportSLn "import.main" 20 $ "Library primitive dir = " ++ show libdirPrim
487 -
-- Turn off import-chasing messages.
488 -
-- We have to modify the persistent verbosity setting, since
489 -
-- getInterface resets the current verbosity settings to the persistent ones.
490 - 491 -
bracket_ (getsTC Lens.getPersistentVerbosity) Lens.putPersistentVerbosity $ do
492 -
Lens.modifyPersistentVerbosity
493 -
(Strict.Just . Trie.insert [] 0 . Strict.fromMaybe Trie.empty)
494 -
-- set root verbosity to 0
495 - 496 -
-- We don't want to generate highlighting information for Agda.Primitive.
497 -
withHighlightingLevel None $
498 -
forM_ (map (filePath libdirPrim </>) $ Set.toList primitiveModules) \ f -> do
499 -
sf <- srcFromPath (mkAbsolute f)
500 -
primSource <- parseSource sf
501 -
checkModuleName' (srcModuleName primSource) (srcOrigin primSource)
502 -
void $ getNonMainInterface (srcModuleName primSource) (Just primSource)
503 - 504 -
reportSLn "import.main" 10 $ "Done importing the primitive modules."
485 + 486 +
-- Import the Agda.Primitive modules
487 +
importPrimitiveModules
505 488 506 489
-- Now do the type checking via getInterface.
507 490
checkModuleName' (srcModuleName src) (srcOrigin src)
@@ -514,12 +497,38 @@ typeCheckMain mode src = do
514 497
)
515 498 516 499
return $ CheckResult' mi src
517 -
where
518 -
checkModuleName' m f =
519 -
-- Andreas, 2016-07-11, issue 2092
520 -
-- The error range should be set to the file with the wrong module name
521 -
-- not the importing one (which would be the default).
522 -
setCurrentRange m $ checkModuleName m f Nothing
500 + 501 +
-- Andreas, 2016-07-11, issue 2092
502 +
-- The error range should be set to the file with the wrong module name
503 +
-- not the importing one (which would be the default).
504 +
checkModuleName' :: TopLevelModuleName' Range -> SourceFile -> TCM ()
505 +
checkModuleName' m f =
506 +
setCurrentRange m $ checkModuleName m f Nothing
507 + 508 +
-- | Import the primitive modules (unless --no-load-primitives).
509 +
importPrimitiveModules :: TCM ()
510 +
importPrimitiveModules = whenM (optLoadPrimitives <$> pragmaOptions) $ do
511 +
reportSLn "import.main" 10 "Importing the primitive modules."
512 +
libdirPrim <- useTC stPrimitiveLibDir
513 +
reportSLn "import.main" 20 $ "Library primitive dir = " ++ show libdirPrim
514 +
-- Turn off import-chasing messages.
515 +
-- We have to modify the persistent verbosity setting, since
516 +
-- getInterface resets the current verbosity settings to the persistent ones.
517 + 518 +
bracket_ (getsTC Lens.getPersistentVerbosity) Lens.putPersistentVerbosity $ do
519 +
Lens.modifyPersistentVerbosity
520 +
(Strict.Just . Trie.insert [] 0 . Strict.fromMaybe Trie.empty)
521 +
-- set root verbosity to 0
522 + 523 +
-- We don't want to generate highlighting information for Agda.Primitive.
524 +
withHighlightingLevel None $
525 +
forM_ (map (filePath libdirPrim </>) $ Set.toList primitiveModules) \ f -> do
526 +
sf <- srcFromPath (mkAbsolute f)
527 +
primSource <- parseSource sf
528 +
checkModuleName' (srcModuleName primSource) (srcOrigin primSource)
529 +
void $ getNonMainInterface (srcModuleName primSource) (Just primSource)
530 + 531 +
reportSLn "import.main" 10 $ "Done importing the primitive modules."
523 532 524 533
-- | Tries to return the interface associated to the given (imported) module.
525 534
-- The time stamp of the relevant interface file is also returned.
@@ -535,13 +544,21 @@ getNonMainInterface
535 544
-- ^ Optional: the source code and some information about the source code.
536 545
-> TCM Interface
537 546
getNonMainInterface x msrc = do
538 -
-- Preserve/restore the current pragma options, which will be mutated when loading
539 -
-- and checking the interface.
540 -
mi <- bracket_ (useTC stPragmaOptions) (stPragmaOptions `setTCLens`) $
541 -
getInterface x NotMainInterface msrc
547 +
mi <- getNonMainModuleInfo x msrc
542 548
tcWarningsToError $ Set.toAscList $ miWarnings mi
543 549
return (miInterface mi)
544 550 551 +
getNonMainModuleInfo
552 +
:: TopLevelModuleName
553 +
-> Maybe Source
554 +
-- ^ Optional: the source code and some information about the source code.
555 +
-> TCM ModuleInfo
556 +
getNonMainModuleInfo x msrc =
557 +
-- Preserve/restore the current pragma options, which will be mutated when loading
558 +
-- and checking the interface.
559 +
bracket_ (useTC stPragmaOptions) (stPragmaOptions `setTCLens`) $
560 +
getInterface x NotMainInterface msrc
561 + 545 562
-- | A more precise variant of 'getNonMainInterface'. If warnings are
546 563
-- encountered then they are returned instead of being turned into
547 564
-- errors.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4