Boot.hs

{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Syntax.TopLevelModuleName.Boot where

import Agda.Utils.List1 (List1)
import Agda.Utils.BiMap (HasTag, Tag, tag)

import Control.DeepSeq (NFData, rnf)
import Data.Function (on)
import Data.Hashable (Hashable, hashWithSalt)
import Data.Text (Text)
import Data.Word (Word64)
import GHC.Generics (Generic)

newtype ModuleNameHash = ModuleNameHash { moduleNameHash :: Word64 }
  deriving (Eq, Ord, Hashable)

instance NFData ModuleNameHash where
  rnf _ = ()

instance HasTag ModuleNameHash where
  type Tag ModuleNameHash = ModuleNameHash
  tag = Just

noModuleNameHash :: ModuleNameHash
noModuleNameHash = ModuleNameHash 0

-- | The record selector is not included in the resulting strings.

instance Show ModuleNameHash where
  showsPrec p (ModuleNameHash h) = showParen (p > 0) $
    showString "ModuleNameHash " . shows h

type TopLevelModuleNameParts = List1 Text

data TopLevelModuleName' range = TopLevelModuleName
  { moduleNameRange :: range
  , moduleNameId    :: {-# UNPACK #-} !ModuleNameHash
  , moduleNameParts :: TopLevelModuleNameParts
  , moduleNameInferred :: !Bool
      -- ^ Was this module name constructed from a file name
      --   rather than declared in the file?
  }
  deriving (Show, Generic)

instance HasTag (TopLevelModuleName' range) where
  type Tag (TopLevelModuleName' range) = ModuleNameHash
  tag = Just . moduleNameId

instance Eq (TopLevelModuleName' range) where
  (==) = (==) `on` moduleNameId

instance Ord (TopLevelModuleName' range) where
  compare = compare `on` moduleNameId

instance Hashable (TopLevelModuleName' range) where
  hashWithSalt salt = hashWithSalt salt . moduleNameId

-- | The 'range' is not forced.

instance NFData (TopLevelModuleName' range) where
  rnf (TopLevelModuleName _ x y _) = rnf (x, y)