-- | 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