    -- | Translating between file paths and ids.
    --
    -- This module allows you to build a dictionary from file paths to some unique identifier
    -- and to look up both file paths and identifiers in that dictionary.

    module Agda.Utils.FileId where

    import           Prelude               hiding (null)

    import           Control.DeepSeq       (NFData)
    import           Control.Monad.Except  (ExceptT)
    import           Control.Monad.Reader  (ReaderT)
    import           Control.Monad.State   (StateT)
    import           Control.Monad.Trans   (MonadTrans, lift)

    import           Data.Bifunctor        (second)
    import           Data.EnumMap          (EnumMap)
    import qualified Data.EnumMap          as EnumMap
    import           Data.Map              (Map)
    import qualified Data.Map              as Map
    import           Data.Maybe            (fromMaybe)
    import           Data.Word             (Word32)

    import           GHC.Generics          (Generic)

    import           Agda.Utils.CallStack  (HasCallStack)
    import           Agda.Utils.FileName   (AbsolutePath)
    import           Agda.Utils.Null       (Null(..))

    import Agda.Utils.Impossible (__IMPOSSIBLE__)

    type File = AbsolutePath

    -- | Unique identifier of a file.
    newtype FileId = FileId { FileId -> Word32
    theFileId :: Word32 }
      deriving (FileId -> FileId -> Bool
    (FileId -> FileId -> Bool)
    -> (FileId -> FileId -> Bool) -> Eq FileId
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: FileId -> FileId -> Bool
    == :: FileId -> FileId -> Bool
    $c/= :: FileId -> FileId -> Bool
    /= :: FileId -> FileId -> Bool
    Eq, Eq FileId
    Eq FileId =>
    (FileId -> FileId -> Ordering)
    -> (FileId -> FileId -> Bool)
    -> (FileId -> FileId -> Bool)
    -> (FileId -> FileId -> Bool)
    -> (FileId -> FileId -> Bool)
    -> (FileId -> FileId -> FileId)
    -> (FileId -> FileId -> FileId)
    -> Ord FileId
    FileId -> FileId -> Bool
    FileId -> FileId -> Ordering
    FileId -> FileId -> FileId
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: FileId -> FileId -> Ordering
    compare :: FileId -> FileId -> Ordering
    $c< :: FileId -> FileId -> Bool
    < :: FileId -> FileId -> Bool
    $c<= :: FileId -> FileId -> Bool
    <= :: FileId -> FileId -> Bool
    $c> :: FileId -> FileId -> Bool
    > :: FileId -> FileId -> Bool
    $c>= :: FileId -> FileId -> Bool
    >= :: FileId -> FileId -> Bool
    $cmax :: FileId -> FileId -> FileId
    max :: FileId -> FileId -> FileId
    $cmin :: FileId -> FileId -> FileId
    min :: FileId -> FileId -> FileId
    Ord, Int -> FileId -> ShowS
    [FileId] -> ShowS
    FileId -> String
    (Int -> FileId -> ShowS)
    -> (FileId -> String) -> ([FileId] -> ShowS) -> Show FileId
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> FileId -> ShowS
    showsPrec :: Int -> FileId -> ShowS
    $cshow :: FileId -> String
    show :: FileId -> String
    $cshowList :: [FileId] -> ShowS
    showList :: [FileId] -> ShowS
    Show, (forall x. FileId -> Rep FileId x)
    -> (forall x. Rep FileId x -> FileId) -> Generic FileId
    forall x. Rep FileId x -> FileId
    forall x. FileId -> Rep FileId x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. FileId -> Rep FileId x
    from :: forall x. FileId -> Rep FileId x
    $cto :: forall x. Rep FileId x -> FileId
    to :: forall x. Rep FileId x -> FileId
    Generic, Int -> FileId
    FileId -> Int
    FileId -> [FileId]
    FileId -> FileId
    FileId -> FileId -> [FileId]
    FileId -> FileId -> FileId -> [FileId]
    (FileId -> FileId)
    -> (FileId -> FileId)
    -> (Int -> FileId)
    -> (FileId -> Int)
    -> (FileId -> [FileId])
    -> (FileId -> FileId -> [FileId])
    -> (FileId -> FileId -> [FileId])
    -> (FileId -> FileId -> FileId -> [FileId])
    -> Enum FileId
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: FileId -> FileId
    succ :: FileId -> FileId
    $cpred :: FileId -> FileId
    pred :: FileId -> FileId
    $ctoEnum :: Int -> FileId
    toEnum :: Int -> FileId
    $cfromEnum :: FileId -> Int
    fromEnum :: FileId -> Int
    $cenumFrom :: FileId -> [FileId]
    enumFrom :: FileId -> [FileId]
    $cenumFromThen :: FileId -> FileId -> [FileId]
    enumFromThen :: FileId -> FileId -> [FileId]
    $cenumFromTo :: FileId -> FileId -> [FileId]
    enumFromTo :: FileId -> FileId -> [FileId]
    $cenumFromThenTo :: FileId -> FileId -> FileId -> [FileId]
    enumFromThenTo :: FileId -> FileId -> FileId -> [FileId]
    Enum, Integer -> FileId
    FileId -> FileId
    FileId -> FileId -> FileId
    (FileId -> FileId -> FileId)
    -> (FileId -> FileId -> FileId)
    -> (FileId -> FileId -> FileId)
    -> (FileId -> FileId)
    -> (FileId -> FileId)
    -> (FileId -> FileId)
    -> (Integer -> FileId)
    -> Num FileId
    forall a.
    (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (Integer -> a)
    -> Num a
    $c+ :: FileId -> FileId -> FileId
    + :: FileId -> FileId -> FileId
    $c- :: FileId -> FileId -> FileId
    - :: FileId -> FileId -> FileId
    $c* :: FileId -> FileId -> FileId
    * :: FileId -> FileId -> FileId
    $cnegate :: FileId -> FileId
    negate :: FileId -> FileId
    $cabs :: FileId -> FileId
    abs :: FileId -> FileId
    $csignum :: FileId -> FileId
    signum :: FileId -> FileId
    $cfromInteger :: Integer -> FileId
    fromInteger :: Integer -> FileId
    Num)

    -- * Mapping between files and their unique identifiers.

    type FileToId = Map File FileId
    type IdToFile = EnumMap FileId File

    data FileDict = FileDict
      { FileDict -> FileToId
    fileToId :: FileToId
      , FileDict -> IdToFile
    idToFile :: IdToFile
      } deriving ((forall x. FileDict -> Rep FileDict x)
    -> (forall x. Rep FileDict x -> FileDict) -> Generic FileDict
    forall x. Rep FileDict x -> FileDict
    forall x. FileDict -> Rep FileDict x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. FileDict -> Rep FileDict x
    from :: forall x. FileDict -> Rep FileDict x
    $cto :: forall x. Rep FileDict x -> FileDict
    to :: forall x. Rep FileDict x -> FileDict
    Generic)

    -- | Translate a file to an ID; mapping must exist.
    class GetFileId a where
      getFileId :: HasCallStack => a -> File -> FileId

    -- | Translate a ID to a file; mapping must exist.
    class GetIdFile a where
      getIdFile :: a -> FileId -> File

    -- * Constructing a mapping between files and their unique identifiers.

    data FileDictBuilder = FileDictBuilder
      { FileDictBuilder -> FileId
    nextFileId :: FileId
      , FileDictBuilder -> FileDict
    fileDict   :: FileDict
      } deriving ((forall x. FileDictBuilder -> Rep FileDictBuilder x)
    -> (forall x. Rep FileDictBuilder x -> FileDictBuilder)
    -> Generic FileDictBuilder
    forall x. Rep FileDictBuilder x -> FileDictBuilder
    forall x. FileDictBuilder -> Rep FileDictBuilder x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. FileDictBuilder -> Rep FileDictBuilder x
    from :: forall x. FileDictBuilder -> Rep FileDictBuilder x
    $cto :: forall x. Rep FileDictBuilder x -> FileDictBuilder
    to :: forall x. Rep FileDictBuilder x -> FileDictBuilder
    Generic)

    -- | Register a new file identifier or retrieve an existing one.
    registerFileId :: File -> FileDictBuilder -> (FileId, FileDictBuilder)
    registerFileId :: File -> FileDictBuilder -> (FileId, FileDictBuilder)
    registerFileId File
    f FileDictBuilder
    d = (Maybe FileDictBuilder -> FileDictBuilder)
    -> (FileId, Maybe FileDictBuilder) -> (FileId, FileDictBuilder)
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second (FileDictBuilder -> Maybe FileDictBuilder -> FileDictBuilder
    forall a. a -> Maybe a -> a
    fromMaybe FileDictBuilder
    d) ((FileId, Maybe FileDictBuilder) -> (FileId, FileDictBuilder))
    -> (FileId, Maybe FileDictBuilder) -> (FileId, FileDictBuilder)
    forall a b. (a -> b) -> a -> b
    $ File -> FileDictBuilder -> (FileId, Maybe FileDictBuilder)
    registerFileId'' File
    f FileDictBuilder
    d

    -- | Register a new file identifier ('True') or retrieve an existing one ('False').
    registerFileId' :: File -> FileDictBuilder -> ((FileId, Bool), FileDictBuilder)
    registerFileId' :: File -> FileDictBuilder -> ((FileId, Bool), FileDictBuilder)
    registerFileId' File
    f FileDictBuilder
    d =
      case File -> FileDictBuilder -> (FileId, Maybe FileDictBuilder)
    registerFileId'' File
    f FileDictBuilder
    d of
        (FileId
    i, Maybe FileDictBuilder
    Nothing) -> ((FileId
    i, Bool
    False), FileDictBuilder
    d)
        (FileId
    i, Just FileDictBuilder
    d') -> ((FileId
    i, Bool
    True), FileDictBuilder
    d')

    -- | Register a new file identifier or retrieve an existing one.
    --
    --   If 'Nothing' is returned, the file was already registered.
    registerFileId'' :: File -> FileDictBuilder -> (FileId, Maybe FileDictBuilder)
    registerFileId'' :: File -> FileDictBuilder -> (FileId, Maybe FileDictBuilder)
    registerFileId''  File
    f d :: FileDictBuilder
    d@(FileDictBuilder FileId
    n (FileDict FileToId
    fileToId IdToFile
    idToFile)) =
      case File -> FileToId -> Maybe FileId
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup File
    f FileToId
    fileToId of
        Just FileId
    i  -> (FileId
    i, Maybe FileDictBuilder
    forall a. Maybe a
    Nothing)
        Maybe FileId
    Nothing -> (FileId
    n, FileDictBuilder -> Maybe FileDictBuilder
    forall a. a -> Maybe a
    Just (FileDictBuilder -> Maybe FileDictBuilder)
    -> FileDictBuilder -> Maybe FileDictBuilder
    forall a b. (a -> b) -> a -> b
    $ FileId -> FileDict -> FileDictBuilder
    FileDictBuilder (FileId
    n FileId -> FileId -> FileId
    forall a. Num a => a -> a -> a
    + FileId
    1) (FileToId -> IdToFile -> FileDict
    FileDict FileToId
    fileToId' IdToFile
    idToFile'))
      where
        fileToId' :: FileToId
    fileToId' = File -> FileId -> FileToId -> FileToId
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert File
    f FileId
    n FileToId
    fileToId
        idToFile' :: IdToFile
    idToFile' = FileId -> File -> IdToFile -> IdToFile
    forall k a. Enum k => k -> a -> EnumMap k a -> EnumMap k a
    EnumMap.insert FileId
    n File
    f IdToFile
    idToFile

    -- * Monadic interface

    class Monad m => MonadFileId m where
      fileFromId :: FileId -> m File
      idFromFile :: File -> m FileId

      default fileFromId :: (MonadTrans t, MonadFileId n, m ~ t n) => FileId -> m File
      fileFromId = n File -> m File
    n File -> t n File
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n File -> m File) -> (FileId -> n File) -> FileId -> m File
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FileId -> n File
    forall (m :: * -> *). MonadFileId m => FileId -> m File
    fileFromId

      default idFromFile :: (MonadTrans t, MonadFileId n, m ~ t n) => File -> m FileId
      idFromFile = n FileId -> m FileId
    n FileId -> t n FileId
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (n FileId -> m FileId) -> (File -> n FileId) -> File -> m FileId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . File -> n FileId
    forall (m :: * -> *). MonadFileId m => File -> m FileId
    idFromFile

    instance MonadFileId m => MonadFileId (ExceptT e m)
    instance MonadFileId m => MonadFileId (ReaderT r m)
    instance MonadFileId m => MonadFileId (StateT s m)

    -- Instances for GetFileId

    instance GetFileId FileToId where
      getFileId :: FileToId -> File -> FileId
      getFileId :: FileToId -> File -> FileId
    getFileId FileToId
    m File
    f = FileId -> File -> FileToId -> FileId
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault FileId
    forall a. HasCallStack => a
    __IMPOSSIBLE__ File
    f FileToId
    m

    instance GetFileId FileDict where
      getFileId :: HasCallStack => FileDict -> File -> FileId
    getFileId = FileToId -> File -> FileId
    forall a. (GetFileId a, HasCallStack) => a -> File -> FileId
    getFileId (FileToId -> File -> FileId)
    -> (FileDict -> FileToId) -> FileDict -> File -> FileId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FileDict -> FileToId
    fileToId

    instance GetFileId FileDictBuilder where
      getFileId :: HasCallStack => FileDictBuilder -> File -> FileId
    getFileId = FileDict -> File -> FileId
    forall a. (GetFileId a, HasCallStack) => a -> File -> FileId
    getFileId (FileDict -> File -> FileId)
    -> (FileDictBuilder -> FileDict)
    -> FileDictBuilder
    -> File
    -> FileId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FileDictBuilder -> FileDict
    fileDict

    -- Instances for GetIdFile

    instance GetIdFile IdToFile where
      getIdFile :: IdToFile -> FileId -> File
      getIdFile :: IdToFile -> FileId -> File
    getIdFile IdToFile
    m FileId
    i = File -> FileId -> IdToFile -> File
    forall k a. Enum k => a -> k -> EnumMap k a -> a
    EnumMap.findWithDefault File
    forall a. HasCallStack => a
    __IMPOSSIBLE__ FileId
    i IdToFile
    m

    instance GetIdFile FileDict where
      getIdFile :: FileDict -> FileId -> File
    getIdFile = IdToFile -> FileId -> File
    forall a. GetIdFile a => a -> FileId -> File
    getIdFile (IdToFile -> FileId -> File)
    -> (FileDict -> IdToFile) -> FileDict -> FileId -> File
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FileDict -> IdToFile
    idToFile

    instance GetIdFile FileDictBuilder where
      getIdFile :: FileDictBuilder -> FileId -> File
    getIdFile = FileDict -> FileId -> File
    forall a. GetIdFile a => a -> FileId -> File
    getIdFile (FileDict -> FileId -> File)
    -> (FileDictBuilder -> FileDict)
    -> FileDictBuilder
    -> FileId
    -> File
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FileDictBuilder -> FileDict
    fileDict

    -- Instances for Null

    instance Null FileDict where
      empty :: FileDict
    empty = FileToId -> IdToFile -> FileDict
    FileDict FileToId
    forall a. Null a => a
    empty IdToFile
    forall a. Null a => a
    empty
      null :: FileDict -> Bool
    null (FileDict FileToId
    to IdToFile
    fro) = FileToId -> Bool
    forall a. Null a => a -> Bool
    null FileToId
    to Bool -> Bool -> Bool
    && IdToFile -> Bool
    forall a. Null a => a -> Bool
    null IdToFile
    fro

    instance Null FileDictBuilder where
      empty :: FileDictBuilder
    empty = FileId -> FileDict -> FileDictBuilder
    FileDictBuilder FileId
    1 FileDict
    forall a. Null a => a
    empty
      null :: FileDictBuilder -> Bool
    null (FileDictBuilder FileId
    _ FileDict
    d) = FileDict -> Bool
    forall a. Null a => a -> Bool
    null FileDict
    d

    -- Instances for NFData

    instance NFData FileId
    instance NFData FileDict
    instance NFData FileDictBuilder