    {-| Instead of checking time-stamps we compute a hash of the module source and
        store it in the interface file. This module contains the functions to do
        that. -}
    module Agda.Utils.Hash where

    import Data.ByteString as B
    import Data.Word
    import qualified Data.Hash as H
    import qualified Data.List as L
    import Data.Digest.Murmur64
    import qualified Data.Text.Encoding as T
    import Data.Text.Lazy (Text)
    import qualified Data.Text.Lazy as T

    import Agda.Utils.FileName
    import Agda.Utils.IO.UTF8 (readTextFile)

    type Hash = Word64

    hashByteString :: ByteString -> Hash
    hashByteString :: ByteString -> Hash
    hashByteString = Hash -> Hash
    H.asWord64 (Hash -> Hash) -> (ByteString -> Hash) -> ByteString -> Hash
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Hash -> Word8 -> Hash) -> Hash -> ByteString -> Hash
    forall a. (a -> Word8 -> a) -> a -> ByteString -> a
    B.foldl' (\Hash
    h Word8
    b -> Hash -> Hash -> Hash
    H.combine Hash
    h (Word8 -> Hash
    H.hashWord8 Word8
    b)) (Word8 -> Hash
    H.hashWord8 Word8
    0)

    hashTextFile :: AbsolutePath -> IO Hash
    hashTextFile :: AbsolutePath -> IO Hash
    hashTextFile AbsolutePath
    file = Text -> Hash
    hashText (Text -> Hash) -> IO Text -> IO Hash
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> IO Text
    readTextFile (AbsolutePath -> String
    filePath AbsolutePath
    file)

    -- | Hashes a piece of 'Text'.

    hashText :: Text -> Hash
    hashText :: Text -> Hash
    hashText = ByteString -> Hash
    hashByteString (ByteString -> Hash) -> (Text -> ByteString) -> Text -> Hash
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> ByteString
    T.encodeUtf8 (Text -> ByteString) -> (Text -> Text) -> Text -> ByteString
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Text
    T.toStrict

    combineHashes :: [Hash] -> Hash
    combineHashes :: [Hash] -> Hash
    combineHashes [Hash]
    hs = Hash -> Hash
    H.asWord64 (Hash -> Hash) -> Hash -> Hash
    forall a b. (a -> b) -> a -> b
    $ (Hash -> Hash -> Hash) -> Hash -> [Hash] -> Hash
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    L.foldl' Hash -> Hash -> Hash
    H.combine (Word8 -> Hash
    H.hashWord8 Word8
    0) ([Hash] -> Hash) -> [Hash] -> Hash
    forall a b. (a -> b) -> a -> b
    $ (Hash -> Hash) -> [Hash] -> [Hash]
    forall a b. (a -> b) -> [a] -> [b]
    L.map Hash -> Hash
    forall a. Hashable a => a -> Hash
    H.hash [Hash]
    hs

    -- | Hashing a module name for unique identifiers.
    hashString :: String -> Word64
    hashString :: String -> Hash
    hashString = Hash64 -> Hash
    asWord64 (Hash64 -> Hash) -> (String -> Hash64) -> String -> Hash
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Hash64
    forall a. Hashable64 a => a -> Hash64
    hash64