{-# 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
  }
  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) = (ModuleNameHash, TopLevelModuleNameParts) -> ()
forall a. NFData a => a -> ()
rnf (ModuleNameHash
x, TopLevelModuleNameParts
y)