23
22
import Data.Monoid (mempty, mappend)
24
23
import Data.Map (Map)
25
24
import Data.Set (Set)
26
26
import System.Directory (doesFileExist, getModificationTime, removeFile)
27
27
import System.FilePath ((</>))
29
import qualified Text.PrettyPrint.Boxes as Boxes
29
31
import Paths_Agda (getDataFileName)
31
33
import qualified Agda.Syntax.Abstract as A
40
42
import Agda.TypeChecking.Errors
41
43
import Agda.TypeChecking.Reduce
42
44
import Agda.TypeChecking.Monad
45
import Agda.TypeChecking.Monad.Base.KillRange -- killRange for Signature
43
46
import Agda.TypeChecking.Serialise
47
import Agda.TypeChecking.Telescope
44
48
import Agda.TypeChecking.Primitive
45
49
import Agda.TypeChecking.Monad.Benchmark (billTop, reimburseTop)
46
50
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
55
58
import Agda.Interaction.Highlighting.Generate
56
59
import Agda.Interaction.Highlighting.Vim
61
import Agda.Utils.Except ( MonadError(catchError, throwError) )
58
62
import Agda.Utils.FileName
63
import Agda.Utils.Lens
59
64
import Agda.Utils.Monad
65
import Agda.Utils.Null (unlessNullM)
60
66
import Agda.Utils.IO.Binary
61
67
import Agda.Utils.Pretty
62
import Agda.Utils.Fresh
63
68
import Agda.Utils.Time
64
69
import Agda.Utils.Hash
65
70
import qualified Agda.Utils.Trie as Trie
67
#include "../undefined.h"
72
#include "undefined.h"
68
73
import Agda.Utils.Impossible
75
-- | Are we loading the interface for the user-loaded file
78
= MainInterface -- ^ Interface for main file.
79
| NotMainInterface -- ^ Interface for imported file.
70
82
-- | Merge an interface into the current proof state.
71
83
mergeInterface :: Interface -> TCM ()
72
84
mergeInterface i = do
73
let sig = iSignature i
74
builtin = Map.toList $ iBuiltin i
75
prim = [ x | (_,Prim x) <- builtin ]
76
bi = Map.fromList [ (x,Builtin t) | (x,Builtin t) <- builtin ]
85
let sig = iSignature i
86
builtin = Map.toList $ iBuiltin i
87
prim = [ x | (_,Prim x) <- builtin ]
88
bi = Map.fromList [ (x,Builtin t) | (x,Builtin t) <- builtin ]
77
89
bs <- gets stBuiltinThings
78
90
reportSLn "import.iface.merge" 10 $ "Merging interface"
79
91
reportSLn "import.iface.merge" 20 $
92
104
reportSLn "import.iface.merge" 20 $
93
105
" Rebinding primitives " ++ show prim
94
106
prim <- Map.fromList <$> mapM rebind prim
95
modify $ \st -> st { stImportedBuiltins = stImportedBuiltins st `Map.union` prim
107
stImportedBuiltins %= (`Map.union` prim)
99
PrimImpl _ pf <- lookupPrimitiveFunction x
100
return (x, Prim $ pf { primFunName = q })
110
PrimImpl _ pf <- lookupPrimitiveFunction x
111
return (x, Prim $ pf { primFunName = q })
102
113
addImportedThings ::
103
114
Signature -> BuiltinThings PrimFun -> Set String -> A.PatternSynDefns -> TCM ()
104
addImportedThings isig ibuiltin hsImports patsyns =
106
{ stImports = unionSignatures [stImports st, isig]
107
, stImportedBuiltins = Map.union (stImportedBuiltins st) ibuiltin
108
, stHaskellImports = Set.union (stHaskellImports st) hsImports
109
, stPatternSynImports = Map.union (stPatternSynImports st) patsyns
115
addImportedThings isig ibuiltin hsImports patsyns = do
116
stImports %= \imp -> unionSignatures [imp, isig]
117
stImportedBuiltins %= \imp -> Map.union imp ibuiltin
118
stHaskellImports %= \imp -> Set.union imp hsImports
119
stPatternSynImports %= \imp -> Map.union imp patsyns
120
addSignatureInstances isig
112
122
-- | Scope checks the given module. A proper version of the module
113
123
-- name (with correct definition sites) is returned.
145
155
-- A module with warnings should never be allowed to be
146
156
-- imported from another module.
147
Just mi | not (miWarnings mi) -> do
157
Just mi | not (miWarnings mi) -> do
148
158
reportSLn "import.visit" 10 $ " Already visited " ++ render (pretty x)
149
159
return (miInterface mi, NoWarnings)
151
161
reportSLn "import.visit" 5 $ " Getting interface for " ++ render (pretty x)
152
162
r@(i, wt) <- getIface
153
163
reportSLn "import.visit" 5 $ " Now we've looked at " ++ render (pretty x)
186
196
moduleName $ mkAbsolute $
187
197
libpath </> "prim" </> "Agda" </> "Primitive.agda"
188
198
reportSLn "import.main" 10 $ "Done importing the primitive modules."
193
typeCheck :: AbsolutePath -> TCM (Interface, MaybeWarnings)
200
-- Now do the type checking via getInterface.
195
201
m <- moduleName f
202
getInterface' m MainInterface
204
-- | Tries to return the interface associated to the given (imported) module.
205
-- The time stamp of the relevant interface file is also returned.
206
-- Calls itself recursively for the imports of the given module.
207
-- May type check the module.
208
-- An error is raised if a warning is encountered.
210
-- Do not use this for the main file, use 'typeCheckMain' instead.
199
212
getInterface :: ModuleName -> TCM Interface
200
213
getInterface = getInterface_ . toTopLevelModuleName
215
-- | See 'getInterface'.
202
217
getInterface_ :: C.TopLevelModuleName -> TCM Interface
203
218
getInterface_ x = do
204
(i, wt) <- getInterface' x False
219
(i, wt) <- getInterface' x NotMainInterface
206
SomeWarnings w -> typeError $ warningsToError w
221
SomeWarnings w -> warningsToError w
207
222
NoWarnings -> return i
209
224
-- | A more precise variant of 'getInterface'. If warnings are
210
225
-- encountered then they are returned instead of being turned into
213
getInterface' :: C.TopLevelModuleName
214
-> Bool -- ^ If type checking is necessary, should all
215
-- state changes inflicted by 'createInterface'
217
-> TCM (Interface, MaybeWarnings)
218
getInterface' x includeStateChanges =
219
withIncreasedModuleNestingLevel $
229
:: C.TopLevelModuleName
231
-- ^ If type checking is necessary,
232
-- should all state changes inflicted by 'createInterface' be preserved?
233
-> TCM (Interface, MaybeWarnings)
234
getInterface' x isMain = do
235
withIncreasedModuleNestingLevel $ do
220
236
-- Preserve the pragma options unless includeStateChanges is True.
221
bracket_ (stPragmaOptions <$> get)
237
bracket_ (use stPragmaOptions)
222
238
(unless includeStateChanges . setPragmaOptions) $ do
223
239
-- Forget the pragma options (locally).
224
setCommandLineOptions . stPersistentOptions . stPersistent =<< get
240
setCommandLineOptions . stPersistentOptions . stPersistentState =<< get
226
242
alreadyVisited x $ addImportCycleCheck x $ do
227
243
file <- findFile x -- requires source to exist
251
261
" " ++ render (pretty x) ++ " is " ++
252
262
(if uptodate then "" else "not ") ++ "up-to-date."
264
-- Andreas, 2014-10-20 AIM XX:
265
-- Always retype-check the main file to get the iInsideScope
266
-- which is no longer serialized.
254
267
(stateChangesIncluded, (i, wt)) <-
255
if uptodate then skip file else typeCheckThe file
268
if uptodate && isMain == NotMainInterface then skip file else typeCheckThe file
257
270
-- Ensure that the given module name matches the one in the file.
258
271
let topLevelName = toTopLevelModuleName $ iModuleName i
370
385
ms <- getImportPath
371
nesting <- envModuleNestingLevel <$> ask
372
mf <- stModuleToSource <$> get
386
nesting <- asks envModuleNestingLevel
387
range <- asks envRange
389
mf <- use stModuleToSource
373
390
vs <- getVisitedModules
374
391
ds <- getDecodedModules
375
opts <- stPersistentOptions . stPersistent <$> get
392
opts <- stPersistentOptions . stPersistentState <$> get
376
393
isig <- getImportedSignature
377
ibuiltin <- gets stImportedBuiltins
394
ibuiltin <- use stImportedBuiltins
378
395
ipatsyns <- getPatternSynImports
379
396
ho <- getInteractionOutputCallback
380
397
-- Every interface is treated in isolation. Note: Changes
387
404
withImportPath ms $
388
405
local (\e -> e { envModuleNestingLevel = nesting
406
-- Andreas, 2014-08-18:
407
-- Preserve the range of import statement
408
-- for reporting termination errors in
390
413
setDecodedModules ds
391
414
setCommandLineOptions opts
392
415
setInteractionOutputCallback ho
393
modify $ \s -> s { stModuleToSource = mf
416
stModuleToSource .= mf
395
417
setVisitedModules vs
396
418
addImportedThings isig ibuiltin Set.empty ipatsyns
398
420
r <- withMsgs $ createInterface file x
399
mf <- stModuleToSource <$> get
421
mf <- use stModuleToSource
400
422
ds <- getDecodedModules
402
modify $ \s -> s { stModuleToSource = mf }
424
stModuleToSource .= mf
403
425
setDecodedModules ds
405
427
(i, NoWarnings) -> storeDecodedModule i
467
489
writeInterface :: FilePath -> Interface -> TCM ()
468
490
writeInterface file i = do
469
491
reportSLn "import.iface.write" 5 $ "Writing interface file " ++ file ++ "."
492
-- Andreas, Makoto, 2014-10-18 AIM XX:
493
-- iInsideScope is bloating the interface files, so we do not serialize it?
495
i { iInsideScope = emptyScopeInfo
470
497
encodeFile file i
471
498
reportSLn "import.iface.write" 5 $ "Wrote interface file."
472
499
reportSLn "import.iface.write" 50 $ " hash = " ++ show (iFullHash i) ++ ""
490
517
-> TCM (Interface, MaybeWarnings)
491
518
createInterface file mname =
492
519
local (\e -> e { envCurrentPath = file }) $ do
493
modFile <- stModuleToSource <$> get
520
modFile <- use stModuleToSource
494
521
fileTokenInfo <- billTop Bench.Highlighting $ generateTokenInfo file
495
modify $ \st -> st { stTokens = fileTokenInfo }
522
stTokens .= fileTokenInfo
497
524
reportSLn "import.iface.create" 5 $
498
525
"Creating interface for " ++ render (pretty mname) ++ "."
549
576
billTop Bench.Highlighting $ do
551
578
-- Move any remaining token highlighting to stSyntaxInfo.
552
ifTopLevelAndHighlightingLevelIs NonInteractive $
553
printHighlightingInfo . stTokens =<< get
555
st { stTokens = mempty
556
, stSyntaxInfo = stSyntaxInfo st `mappend` stTokens st
580
ifTopLevelAndHighlightingLevelIs NonInteractive $ printHighlightingInfo toks
582
stSyntaxInfo %= \inf -> inf `mappend` toks
559
584
whenM (optGenerateVimFile <$> commandLineOptions) $
560
585
-- Generate Vim file.
565
590
reportSLn "scope.top" 50 $ "SCOPE " ++ show (insideScope topLevel)
567
592
-- Serialization.
568
syntaxInfo <- stSyntaxInfo <$> get
593
syntaxInfo <- use stSyntaxInfo
569
594
i <- billTop Bench.Serialization $ do
570
595
buildInterface file topLevel syntaxInfo previousHsImports options
572
597
-- TODO: It would be nice if unsolved things were highlighted
573
598
-- after every mutual block.
575
termErrs <- Fold.toList <$> stTermErrs <$> get
576
600
unsolvedMetas <- List.nub <$> (mapM getMetaRange =<< getOpenMetas)
577
601
unsolvedConstraints <- getAllConstraints
578
602
interactionPoints <- getInteractionPoints
580
604
ifTopLevelAndHighlightingLevelIs NonInteractive $
581
605
printUnsolvedInfo
583
r <- if and [ null termErrs, null unsolvedMetas, null unsolvedConstraints, null interactionPoints ]
607
r <- if and [ null unsolvedMetas, null unsolvedConstraints, null interactionPoints ]
584
608
then billTop Bench.Serialization $ do
585
609
-- The file was successfully type-checked (and no warnings were
586
610
-- encountered), so the interface should be written out.
587
611
let ifile = filePath $ toIFile file
588
612
writeInterface ifile i
589
613
return (i, NoWarnings)
591
return (i, SomeWarnings $ Warnings termErrs unsolvedMetas unsolvedConstraints)
615
return (i, SomeWarnings $ Warnings unsolvedMetas unsolvedConstraints)
593
617
-- Profiling: Print statistics.
618
printStatistics 30 (Just mname) =<< getStatistics
620
-- Get the statistics of the current module
621
-- and add it to the accumulated statistics.
622
localStatistics <- getStatistics
623
lensAccumStatistics %= Map.unionWith (+) localStatistics
594
624
verboseS "profile" 1 $ do
595
stats <- Map.toList <$> getStatistics
598
_ -> reportS "profile" 1 $ unlines $
599
[ "Ticks for " ++ show (pretty mname) ] ++
600
[ " " ++ s ++ " = " ++ show n
601
| (s, n) <- sortBy (compare `on` snd) stats ]
625
reportSLn "import.iface" 5 $ "Accumulated statistics."
623
647
let scope = scope' { scopeCurrent = m }
624
648
-- Andreas, 2014-05-03: killRange did not result in significant reduction
625
649
-- of .agdai file size, and lost a few seconds performance on library-test.
626
-- sig <- killRange <$> getSignature
628
builtin <- gets stLocalBuiltins
650
-- Andreas, Makoto, 2014-10-18 AIM XX: repeating the experiment
651
-- with discarding also the nameBindingSite in QName:
652
-- Saves 10% on serialization time (and file size)!
653
sig <- killRange <$> getSignature
654
builtin <- use stLocalBuiltins
630
656
mhs <- mapM (\ m -> (m,) <$> moduleHash m) $ Set.toList ms
631
657
hsImps <- getHaskellImports
632
658
patsyns <- getPatternSyns
633
659
h <- liftIO $ hashFile file
634
let builtin' = Map.mapWithKey (\ x b -> (x,) . primFunName <$> b) builtin
660
let builtin' = Map.mapWithKey (\ x b -> (x,) . primFunName <$> b) builtin
635
661
reportSLn "import.iface" 7 " instantiating all meta variables"
636
662
i <- instantiateFull $ Interface
637
663
{ iSourceHash = h
675
701
newExist <- doesFileExist new
676
702
oldExist <- doesFileExist old
677
703
if not (newExist && oldExist)
680
newT <- getModificationTime new
681
oldT <- getModificationTime old
682
return $ newT >= oldT
706
newT <- getModificationTime new
707
oldT <- getModificationTime old
708
return $ newT >= oldT
added
removed
src/full/Agda/Interaction/Imports.hs
