{-# 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ModuleNameHash -> ModuleNameHash -> Bool
$c/= :: ModuleNameHash -> ModuleNameHash -> Bool
== :: ModuleNameHash -> ModuleNameHash -> Bool
$c== :: ModuleNameHash -> ModuleNameHash -> Bool
Eq, Eq 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
min :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash
$cmin :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash
max :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash
$cmax :: ModuleNameHash -> ModuleNameHash -> ModuleNameHash
>= :: ModuleNameHash -> ModuleNameHash -> Bool
$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
compare :: ModuleNameHash -> ModuleNameHash -> Ordering
$ccompare :: ModuleNameHash -> ModuleNameHash -> Ordering
Ord, Eq ModuleNameHash
Int -> ModuleNameHash -> Int
ModuleNameHash -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: ModuleNameHash -> Int
$chash :: ModuleNameHash -> Int
hashWithSalt :: Int -> ModuleNameHash -> Int
$chashWithSalt :: Int -> 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 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> a
id
noModuleNameHash :: ModuleNameHash
noModuleNameHash :: ModuleNameHash
noModuleNameHash = Word64 -> ModuleNameHash
ModuleNameHash Word64
0
instance Show ModuleNameHash where
showsPrec :: Int -> ModuleNameHash -> ShowS
showsPrec Int
p (ModuleNameHash Word64
h) = Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"ModuleNameHash " forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
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
showList :: [TopLevelModuleName' range] -> ShowS
$cshowList :: forall range. Show range => [TopLevelModuleName' range] -> ShowS
show :: TopLevelModuleName' range -> String
$cshow :: forall range. Show range => TopLevelModuleName' range -> String
showsPrec :: Int -> TopLevelModuleName' range -> ShowS
$cshowsPrec :: forall range.
Show range =>
Int -> TopLevelModuleName' range -> ShowS
Show, 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
$cto :: forall range x.
Rep (TopLevelModuleName' range) x -> TopLevelModuleName' range
$cfrom :: forall range x.
TopLevelModuleName' range -> Rep (TopLevelModuleName' range) x
Generic)
instance HasTag (TopLevelModuleName' range) where
type Tag (TopLevelModuleName' range) = ModuleNameHash
tag :: TopLevelModuleName' range
-> Maybe (Tag (TopLevelModuleName' range))
tag = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall range. TopLevelModuleName' range -> ModuleNameHash
moduleNameId
instance Eq (TopLevelModuleName' range) where
== :: TopLevelModuleName' range -> TopLevelModuleName' range -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall range. TopLevelModuleName' range -> ModuleNameHash
moduleNameId
instance Ord (TopLevelModuleName' range) where
compare :: TopLevelModuleName' range -> TopLevelModuleName' range -> Ordering
compare = forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall range. TopLevelModuleName' range -> ModuleNameHash
moduleNameId
instance Hashable (TopLevelModuleName' range) where
hashWithSalt :: Int -> TopLevelModuleName' range -> Int
hashWithSalt Int
salt = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall range. TopLevelModuleName' range -> ModuleNameHash
moduleNameId
instance NFData (TopLevelModuleName' range) where
rnf :: TopLevelModuleName' range -> ()
rnf (TopLevelModuleName range
_ ModuleNameHash
x TopLevelModuleNameParts
y) = forall a. NFData a => a -> ()
rnf (ModuleNameHash
x, TopLevelModuleNameParts
y)