[ #6145, #6146 ] Removed SourceToModule.

Furthermore canonicalizeAbsolutePath is no longer used in the serialiser.
agda · Oct 12, 2022 · c2cb1e7 · c2cb1e7
1 parent fcf3028
commit c2cb1e7
Show file tree

Hide file tree

Showing 4 changed files with 15 additions and 77 deletions.
diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs
@@ -883,25 +883,6 @@ instance FreshName () where
 
 type ModuleToSource = Map TopLevelModuleName AbsolutePath
 
--- | Maps source file names to the corresponding top-level module
--- names.
-
-type SourceToModule = Map AbsolutePath TopLevelModuleName
-
--- | Creates a 'SourceToModule' map based on 'stModuleToSource'.
---
---   O(n log n).
---
---   For a single reverse lookup in 'stModuleToSource',
---   rather use 'lookupModuleFromSourse'.
-
-sourceToModule :: TCM SourceToModule
-sourceToModule =
-  Map.fromListWith __IMPOSSIBLE__
-     .  List.map (\(m, f) -> (f, m))
-     .  Map.toList
-    <$> useTC stModuleToSource
-
 ---------------------------------------------------------------------------
 -- ** Associating concrete names to an abstract name
 ---------------------------------------------------------------------------

diff --git a/src/full/Agda/TypeChecking/Serialise.hs b/src/full/Agda/TypeChecking/Serialise.hs
@@ -69,7 +69,6 @@ import Agda.TypeChecking.Serialise.Instances () --instance only
 
 import Agda.TypeChecking.Monad
 
-import Agda.Utils.FileName (canonicalizeAbsolutePath)
 import Agda.Utils.Hash
 import qualified Agda.Utils.HashTable as H
 import Agda.Utils.IORef
@@ -83,7 +82,7 @@ import Agda.Utils.Impossible
 -- 32-bit machines). Word64 does not have these problems.
 
 currentInterfaceVersion :: Word64
-currentInterfaceVersion = 20221011 * 10 + 0
+currentInterfaceVersion = 20221011 * 10 + 1
 
 -- | The result of 'encode' and 'encodeInterface'.
 
@@ -101,17 +100,14 @@ data Encoded = Encoded
 encode :: EmbPrj a => a -> TCM Encoded
 encode a = do
     collectStats <- hasProfileOption Profile.Serialize
-    fileMod <- sourceToModule
     newD@(Dict nD ltD stD bD iD dD _tD
       _nameD
       _qnameD
       nC ltC stC bC iC dC tC
       nameC
       qnameC
-      stats _ _) <- liftIO $ emptyDict collectStats
-    root <- liftIO $ (`runReaderT` newD) $ do
-       icodeFileMod fileMod  -- Only fills absPathD from fileMod
-       icode a
+      stats _) <- liftIO $ emptyDict collectStats
+    root <- liftIO $ (`runReaderT` newD) $ icode a
     nL  <- benchSort $ l nD
     stL <- benchSort $ l stD
     ltL <- benchSort $ l ltD
@@ -318,20 +314,3 @@ decodeHashes s
 
 decodeFile :: FilePath -> TCM (Maybe Interface)
 decodeFile f = decodeInterface =<< liftIO (L.readFile f)
-
--- | Store a 'SourceToModule' (map from 'AbsolutePath' to 'TopLevelModuleName')
---   as map from 'AbsolutePath' to 'Int32', in order to directly get the identifiers
---   from absolute pathes rather than going through top level module names.
-icodeFileMod
-  :: SourceToModule
-     -- ^ Maps file names to the corresponding module names.
-     --   Must contain a mapping for every file name that is later encountered.
-  -> S ()
-icodeFileMod fileMod = do
-  hmap <- asks absPathD
-  forM_ (Map.toList fileMod) $ \ (absolutePath, topLevelModuleName) -> do
-    -- Andreas, 2020-08-11, issue #4828.
-    -- Expand symlinks before storing in the dictonary.
-    absolutePath <- liftIO $ canonicalizeAbsolutePath absolutePath
-    i <- icod_ topLevelModuleName
-    liftIO $ H.insert hmap absolutePath i
diff --git a/src/full/Agda/TypeChecking/Serialise/Base.hs b/src/full/Agda/TypeChecking/Serialise/Base.hs
@@ -109,7 +109,6 @@ data Dict = Dict
   , collectStats :: Bool
     -- ^ If @True@ collect in @stats@ the quantities of
     --   calls to @icode@ for each @Typeable a@.
-  , absPathD     :: !(HashTable AbsolutePath Int32) -- ^ Not written to interface file.
   }
 
 -- | Creates an empty dictionary.
@@ -138,7 +137,6 @@ emptyDict collectStats = Dict
   <*> newIORef farEmpty
   <*> H.empty
   <*> pure collectStats
-  <*> H.empty
 
 -- | Universal type, wraps everything.
 data U = forall a . Typeable a => U !a

diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Common.hs
@@ -195,36 +195,6 @@ instance EmbPrj Language where
     [1, a] -> valuN Cubical a
     _      -> malformed
 
-instance EmbPrj AbsolutePath where
-  icod_ file = do
-    d <- asks absPathD
-    -- Andreas, 2020-08-11, issue #4828
-    -- AbsolutePath is no longer canonical (can contain symlinks).
-    -- The dictonary contains canonical pathes, though.
-    file <- liftIO $ canonicalizeAbsolutePath file
-    liftIO $ flip fromMaybeM (H.lookup d file) $ do
-      -- The path @file@ should be cached in the dictionary @d@.
-      -- This seems not to be the case, thus, crash here.
-      -- But leave some hints for the posterity why things could go so wrong.
-      -- reportSLn "impossible" 10 -- does not work here
-      putStrLn $ unlines $
-        [ "Panic while serializing absolute path: " ++ show file
-        , "The path could not be found in the dictionary:"
-        ]
-      print =<< H.toList d
-      __IMPOSSIBLE__
-
-  value m = do
-    m :: TopLevelModuleName
-            <- value m
-    mf      <- gets modFile
-    incs    <- gets includes
-    (r, mf) <- liftIO $ findFile'' incs m mf
-    modify $ \s -> s { modFile = mf }
-    case r of
-      Left err -> throwError $ findErrorToTypeError m err
-      Right f  -> return (srcFilePath f)
-
 instance EmbPrj a => EmbPrj (Position' a) where
   icod_ (P.Pn file pos line col) = icodeN' P.Pn file pos line col
 
@@ -316,9 +286,19 @@ instance EmbPrj a => EmbPrj (P.Interval' a) where
   value = valueN P.Interval
 
 instance EmbPrj RangeFile where
-  icod_ (RangeFile a b) = icode (a, b)
+  icod_ (RangeFile _ Nothing)  = __IMPOSSIBLE__
+  icod_ (RangeFile _ (Just a)) = icode a
 
-  value r = uncurry RangeFile <$> value r
+  value r = do
+    m :: TopLevelModuleName
+            <- value r
+    mf      <- gets modFile
+    incs    <- gets includes
+    (r, mf) <- liftIO $ findFile'' incs m mf
+    modify $ \s -> s { modFile = mf }
+    case r of
+      Left err -> throwError $ findErrorToTypeError m err
+      Right f  -> return $ RangeFile (srcFilePath f) (Just m)
 
 -- | Ranges are always deserialised as 'noRange'.