    {-# 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
    moduleNameHash :: Word64 }
      deriving (ModuleNameHash -> ModuleNameHash -> Bool
    (ModuleNameHash -> ModuleNameHash -> Bool)
    -> (ModuleNameHash -> ModuleNameHash -> Bool) -> Eq ModuleNameHash
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ModuleNameHash -> ModuleNameHash -> Bool
    == :: ModuleNameHash -> ModuleNameHash -> Bool
    $c/= :: ModuleNameHash -> ModuleNameHash -> Bool
    /= :: ModuleNameHash -> ModuleNameHash -> Bool
    Eq, Eq ModuleNameHash
    Eq ModuleNameHash =>
    (ModuleNameHash -> ModuleNameHash -> Ordering)
    -> (ModuleNameHash -> ModuleNameHash -> Bool)
    -> (ModuleNameHash -> ModuleNameHash -> Bool)
    -> (ModuleNameHash -> ModuleNameHash -> Bool)
    -> (ModuleNameHash -> ModuleNameHash -> Bool)
    -> (ModuleNameHash -> ModuleNameHash -> ModuleNameHash)
    -> (ModuleNameHash -> ModuleNameHash -> ModuleNameHash)
    -> Ord ModuleNameHash
    ModuleNameHash -> ModuleNameHash -> Bool
    ModuleNameHash -> ModuleNameHash -> Ordering
    ModuleNameHash -> ModuleNameHash -> ModuleNameHash
    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 :: ModuleNameHash -> ModuleNameHash -> Ordering
    compare :: ModuleNameHash -> ModuleNameHash -> Ordering
    $c< :: ModuleNameHash -> ModuleNameHash -> Bool
    < :: ModuleNameHash -> ModuleNameHash -> Bool
    $c<= :: ModuleNameHash -> ModuleNameHash -> Bool
    <= :: ModuleNameHash -> ModuleNameHash -> Bool
    $c> :: ModuleNameHash -> ModuleNameHash -> Bool
    > :: ModuleNameHash -> ModuleNameHash -> Bool
    $c>= :: ModuleNameHash -> ModuleNameHash -> Bool
    >= :: ModuleNameHash -> ModuleNameHash -> Bool
    $cmax :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash
    max :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash
    $cmin :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash
    min :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash
    Ord, Eq ModuleNameHash
    Eq ModuleNameHash =>
    (Int -> ModuleNameHash -> Int)
    -> (ModuleNameHash -> Int) -> Hashable ModuleNameHash
    Int -> ModuleNameHash -> Int
    ModuleNameHash -> Int
    forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
    $chashWithSalt :: Int -> ModuleNameHash -> Int
    hashWithSalt :: Int -> ModuleNameHash -> Int
    $chash :: ModuleNameHash -> Int
    hash :: ModuleNameHash -> Int
    Hashable)

    instance NFData ModuleNameHash where
      rnf :: ModuleNameHash -> ()
    rnf ModuleNameHash
    _ = ()

    instance HasTag ModuleNameHash where
      type Tag ModuleNameHash = ModuleNameHash
      tag :: ModuleNameHash -> Maybe (Tag ModuleNameHash)
    tag = ModuleNameHash -> Maybe (Tag ModuleNameHash)
    ModuleNameHash -> Maybe ModuleNameHash
    forall a. a -> Maybe a
    Just

    noModuleNameHash :: ModuleNameHash
    noModuleNameHash :: ModuleNameHash
    noModuleNameHash = Word64 -> ModuleNameHash
    ModuleNameHash Word64
    0

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

    instance Show ModuleNameHash where
      showsPrec :: Int -> ModuleNameHash -> ShowS
    showsPrec Int
    p (ModuleNameHash Word64
    h) = Bool -> ShowS -> ShowS
    showParen (Int
    p Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0) (ShowS -> ShowS) -> ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $
        String -> ShowS
    showString String
    "ModuleNameHash " ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word64 -> ShowS
    forall a. Show a => a -> ShowS
    shows Word64
    h

    type TopLevelModuleNameParts = List1 Text

    data TopLevelModuleName' range = TopLevelModuleName
      { forall range. TopLevelModuleName' range -> range
    moduleNameRange :: range
      , forall range. TopLevelModuleName' range -> ModuleNameHash
    moduleNameId    :: {-# UNPACK #-} !ModuleNameHash
      , forall range. TopLevelModuleName' range -> TopLevelModuleNameParts
    moduleNameParts :: TopLevelModuleNameParts
      , forall range. TopLevelModuleName' range -> Bool
    moduleNameInferred :: !Bool
          -- ^ Was this module name constructed from a file name
          --   rather than declared in the file?
      }
      deriving (Int -> TopLevelModuleName' range -> ShowS
    [TopLevelModuleName' range] -> ShowS
    TopLevelModuleName' range -> String
    (Int -> TopLevelModuleName' range -> ShowS)
    -> (TopLevelModuleName' range -> String)
    -> ([TopLevelModuleName' range] -> ShowS)
    -> Show (TopLevelModuleName' range)
    forall range.
    Show range =>
    Int -> TopLevelModuleName' range -> ShowS
    forall range. Show range => [TopLevelModuleName' range] -> ShowS
    forall range. Show range => TopLevelModuleName' range -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall range.
    Show range =>
    Int -> TopLevelModuleName' range -> ShowS
    showsPrec :: Int -> TopLevelModuleName' range -> ShowS
    $cshow :: forall range. Show range => TopLevelModuleName' range -> String
    show :: TopLevelModuleName' range -> String
    $cshowList :: forall range. Show range => [TopLevelModuleName' range] -> ShowS
    showList :: [TopLevelModuleName' range] -> ShowS
    Show, (forall x.
     TopLevelModuleName' range -> Rep (TopLevelModuleName' range) x)
    -> (forall x.
        Rep (TopLevelModuleName' range) x -> TopLevelModuleName' range)
    -> Generic (TopLevelModuleName' range)
    forall x.
    Rep (TopLevelModuleName' range) x -> TopLevelModuleName' range
    forall x.
    TopLevelModuleName' range -> Rep (TopLevelModuleName' range) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall range x.
    Rep (TopLevelModuleName' range) x -> TopLevelModuleName' range
    forall range x.
    TopLevelModuleName' range -> Rep (TopLevelModuleName' range) x
    $cfrom :: forall range x.
    TopLevelModuleName' range -> Rep (TopLevelModuleName' range) x
    from :: forall x.
    TopLevelModuleName' range -> Rep (TopLevelModuleName' range) x
    $cto :: forall range x.
    Rep (TopLevelModuleName' range) x -> TopLevelModuleName' range
    to :: forall x.
    Rep (TopLevelModuleName' range) x -> TopLevelModuleName' range
    Generic)

    instance HasTag (TopLevelModuleName' range) where
      type Tag (TopLevelModuleName' range) = ModuleNameHash
      tag :: TopLevelModuleName' range
    -> Maybe (Tag (TopLevelModuleName' range))
    tag = ModuleNameHash -> Maybe ModuleNameHash
    forall a. a -> Maybe a
    Just (ModuleNameHash -> Maybe ModuleNameHash)
    -> (TopLevelModuleName' range -> ModuleNameHash)
    -> TopLevelModuleName' range
    -> Maybe ModuleNameHash
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TopLevelModuleName' range -> ModuleNameHash
    forall range. TopLevelModuleName' range -> ModuleNameHash
    moduleNameId

    instance Eq (TopLevelModuleName' range) where
      == :: TopLevelModuleName' range -> TopLevelModuleName' range -> Bool
    (==) = ModuleNameHash -> ModuleNameHash -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (ModuleNameHash -> ModuleNameHash -> Bool)
    -> (TopLevelModuleName' range -> ModuleNameHash)
    -> TopLevelModuleName' range
    -> TopLevelModuleName' range
    -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` TopLevelModuleName' range -> ModuleNameHash
    forall range. TopLevelModuleName' range -> ModuleNameHash
    moduleNameId

    instance Ord (TopLevelModuleName' range) where
      compare :: TopLevelModuleName' range -> TopLevelModuleName' range -> Ordering
    compare = ModuleNameHash -> ModuleNameHash -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (ModuleNameHash -> ModuleNameHash -> Ordering)
    -> (TopLevelModuleName' range -> ModuleNameHash)
    -> TopLevelModuleName' range
    -> TopLevelModuleName' range
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` TopLevelModuleName' range -> ModuleNameHash
    forall range. TopLevelModuleName' range -> ModuleNameHash
    moduleNameId

    instance Hashable (TopLevelModuleName' range) where
      hashWithSalt :: Int -> TopLevelModuleName' range -> Int
    hashWithSalt Int
    salt = Int -> ModuleNameHash -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    salt (ModuleNameHash -> Int)
    -> (TopLevelModuleName' range -> ModuleNameHash)
    -> TopLevelModuleName' range
    -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TopLevelModuleName' range -> ModuleNameHash
    forall range. TopLevelModuleName' range -> ModuleNameHash
    moduleNameId

    -- | The 'range' is not forced.

    instance NFData (TopLevelModuleName' range) where
      rnf :: TopLevelModuleName' range -> ()
    rnf (TopLevelModuleName range
    _ ModuleNameHash
    x TopLevelModuleNameParts
    y Bool
    _) = (ModuleNameHash, TopLevelModuleNameParts) -> ()
    forall a. NFData a => a -> ()
    rnf (ModuleNameHash
    x, TopLevelModuleNameParts
    y)