{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeFamilies #-} -- for type equality ~

{-| Names in the concrete syntax are just strings (or lists of strings for
    qualified names).
-}
module Agda.Syntax.Concrete.Name where

import Control.DeepSeq

import Data.ByteString.Char8 (ByteString)
import Data.Function
import qualified Data.Foldable as Fold
import qualified Data.List as List
import Data.Data (Data)

import GHC.Generics (Generic)

import System.FilePath

import Agda.Syntax.Common
import Agda.Syntax.Position

import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.Pretty
import Agda.Utils.Size
import Agda.Utils.Suffix

import Agda.Utils.Impossible

{-| A name is a non-empty list of alternating 'Id's and 'Hole's. A normal name
    is represented by a singleton list, and operators are represented by a list
    with 'Hole's where the arguments should go. For instance: @[Hole,Id "+",Hole]@
    is infix addition.

    Equality and ordering on @Name@s are defined to ignore range so same names
    in different locations are equal.
-}
data Name
  = Name -- ^ A (mixfix) identifier.
    { Name -> Range
nameRange     :: Range
    , Name -> NameInScope
nameInScope   :: NameInScope
    , Name -> [NamePart]
nameNameParts :: [NamePart]
    }
  | NoName -- ^ @_@.
    { nameRange     :: Range
    , Name -> NameId
nameId        :: NameId
    }
  deriving Typeable Name
DataType
Constr
Typeable Name
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Name -> c Name)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Name)
-> (Name -> Constr)
-> (Name -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Name))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name))
-> ((forall b. Data b => b -> b) -> Name -> Name)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r)
-> (forall u. (forall d. Data d => d -> u) -> Name -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Name -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Name -> m Name)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Name -> m Name)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Name -> m Name)
-> Data Name
Name -> DataType
Name -> Constr
(forall b. Data b => b -> b) -> Name -> Name
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name -> c Name
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Name
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Name -> u
forall u. (forall d. Data d => d -> u) -> Name -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Name -> m Name
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Name -> m Name
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Name
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name -> c Name
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Name)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)
$cNoName :: Constr
$cName :: Constr
$tName :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Name -> m Name
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Name -> m Name
gmapMp :: (forall d. Data d => d -> m d) -> Name -> m Name
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Name -> m Name
gmapM :: (forall d. Data d => d -> m d) -> Name -> m Name
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Name -> m Name
gmapQi :: Int -> (forall d. Data d => d -> u) -> Name -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Name -> u
gmapQ :: (forall d. Data d => d -> u) -> Name -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Name -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Name -> r
gmapT :: (forall b. Data b => b -> b) -> Name -> Name
$cgmapT :: (forall b. Data b => b -> b) -> Name -> Name
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Name)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Name)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Name)
dataTypeOf :: Name -> DataType
$cdataTypeOf :: Name -> DataType
toConstr :: Name -> Constr
$ctoConstr :: Name -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Name
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Name
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name -> c Name
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Name -> c Name
$cp1Data :: Typeable Name
Data

-- | An open mixfix identifier is either prefix, infix, or suffix.
--   That is to say: at least one of its extremities is a @Hole@

isOpenMixfix :: Name -> Bool
isOpenMixfix :: Name -> Bool
isOpenMixfix Name
n = case Name
n of
  Name Range
_ NameInScope
_ (NamePart
x : xs :: [NamePart]
xs@(NamePart
_:[NamePart]
_)) -> NamePart
x NamePart -> NamePart -> Bool
forall a. Eq a => a -> a -> Bool
== NamePart
Hole Bool -> Bool -> Bool
|| [NamePart] -> NamePart
forall a. [a] -> a
last [NamePart]
xs NamePart -> NamePart -> Bool
forall a. Eq a => a -> a -> Bool
== NamePart
Hole
  Name
_                       -> Bool
False

instance Underscore Name where
  underscore :: Name
underscore = Range -> NameId -> Name
NoName Range
forall a. Range' a
noRange NameId
forall a. HasCallStack => a
__IMPOSSIBLE__
  isUnderscore :: Name -> Bool
isUnderscore NoName{} = Bool
True
  isUnderscore (Name {nameNameParts :: Name -> [NamePart]
nameNameParts = [Id RawName
x]}) = RawName -> Bool
forall a. Underscore a => a -> Bool
isUnderscore RawName
x
  isUnderscore Name
_ = Bool
False

-- | Mixfix identifiers are composed of words and holes,
--   e.g. @_+_@ or @if_then_else_@ or @[_/_]@.
data NamePart
  = Hole       -- ^ @_@ part.
  | Id RawName  -- ^ Identifier part.
  deriving (Typeable NamePart
DataType
Constr
Typeable NamePart
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> NamePart -> c NamePart)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c NamePart)
-> (NamePart -> Constr)
-> (NamePart -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c NamePart))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NamePart))
-> ((forall b. Data b => b -> b) -> NamePart -> NamePart)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NamePart -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NamePart -> r)
-> (forall u. (forall d. Data d => d -> u) -> NamePart -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> NamePart -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> NamePart -> m NamePart)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NamePart -> m NamePart)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NamePart -> m NamePart)
-> Data NamePart
NamePart -> DataType
NamePart -> Constr
(forall b. Data b => b -> b) -> NamePart -> NamePart
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NamePart -> c NamePart
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NamePart
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> NamePart -> u
forall u. (forall d. Data d => d -> u) -> NamePart -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NamePart -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NamePart -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NamePart -> m NamePart
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NamePart -> m NamePart
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NamePart
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NamePart -> c NamePart
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NamePart)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NamePart)
$cId :: Constr
$cHole :: Constr
$tNamePart :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> NamePart -> m NamePart
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NamePart -> m NamePart
gmapMp :: (forall d. Data d => d -> m d) -> NamePart -> m NamePart
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NamePart -> m NamePart
gmapM :: (forall d. Data d => d -> m d) -> NamePart -> m NamePart
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NamePart -> m NamePart
gmapQi :: Int -> (forall d. Data d => d -> u) -> NamePart -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> NamePart -> u
gmapQ :: (forall d. Data d => d -> u) -> NamePart -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> NamePart -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NamePart -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NamePart -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NamePart -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NamePart -> r
gmapT :: (forall b. Data b => b -> b) -> NamePart -> NamePart
$cgmapT :: (forall b. Data b => b -> b) -> NamePart -> NamePart
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NamePart)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NamePart)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c NamePart)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NamePart)
dataTypeOf :: NamePart -> DataType
$cdataTypeOf :: NamePart -> DataType
toConstr :: NamePart -> Constr
$ctoConstr :: NamePart -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NamePart
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NamePart
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NamePart -> c NamePart
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NamePart -> c NamePart
$cp1Data :: Typeable NamePart
Data, (forall x. NamePart -> Rep NamePart x)
-> (forall x. Rep NamePart x -> NamePart) -> Generic NamePart
forall x. Rep NamePart x -> NamePart
forall x. NamePart -> Rep NamePart x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NamePart x -> NamePart
$cfrom :: forall x. NamePart -> Rep NamePart x
Generic)

-- | Define equality on @Name@ to ignore range so same names in different
--   locations are equal.
--
--   Is there a reason not to do this? -Jeff
--
--   No. But there are tons of reasons to do it. For instance, when using
--   names as keys in maps you really don't want to have to get the range
--   right to be able to do a lookup. -Ulf

instance Eq Name where
    Name Range
_ NameInScope
_ [NamePart]
xs    == :: Name -> Name -> Bool
== Name Range
_ NameInScope
_ [NamePart]
ys    = [NamePart]
xs [NamePart] -> [NamePart] -> Bool
forall a. Eq a => a -> a -> Bool
== [NamePart]
ys
    NoName Range
_ NameId
i     == NoName Range
_ NameId
j     = NameId
i NameId -> NameId -> Bool
forall a. Eq a => a -> a -> Bool
== NameId
j
    Name
_              == Name
_              = Bool
False

instance Ord Name where
    compare :: Name -> Name -> Ordering
compare (Name Range
_ NameInScope
_ [NamePart]
xs)  (Name Range
_ NameInScope
_ [NamePart]
ys)      = [NamePart] -> [NamePart] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare [NamePart]
xs [NamePart]
ys
    compare (NoName Range
_ NameId
i)   (NoName Range
_ NameId
j)       = NameId -> NameId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare NameId
i NameId
j
    compare (NoName {})    (Name {})          = Ordering
LT
    compare (Name {})      (NoName {})        = Ordering
GT

instance Eq NamePart where
  NamePart
Hole  == :: NamePart -> NamePart -> Bool
== NamePart
Hole  = Bool
True
  Id RawName
s1 == Id RawName
s2 = RawName
s1 RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
== RawName
s2
  NamePart
_     == NamePart
_     = Bool
False

instance Ord NamePart where
  compare :: NamePart -> NamePart -> Ordering
compare NamePart
Hole    NamePart
Hole    = Ordering
EQ
  compare NamePart
Hole    (Id {}) = Ordering
LT
  compare (Id {}) NamePart
Hole    = Ordering
GT
  compare (Id RawName
s1) (Id RawName
s2) = RawName -> RawName -> Ordering
forall a. Ord a => a -> a -> Ordering
compare RawName
s1 RawName
s2

-- | @QName@ is a list of namespaces and the name of the constant.
--   For the moment assumes namespaces are just @Name@s and not
--     explicitly applied modules.
--   Also assumes namespaces are generative by just using derived
--     equality. We will have to define an equality instance to
--     non-generative namespaces (as well as having some sort of
--     lookup table for namespace names).
data QName
  = Qual  Name QName -- ^ @A.rest@.
  | QName Name       -- ^ @x@.
  deriving (Typeable QName
DataType
Constr
Typeable QName
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> QName -> c QName)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c QName)
-> (QName -> Constr)
-> (QName -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c QName))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName))
-> ((forall b. Data b => b -> b) -> QName -> QName)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r)
-> (forall u. (forall d. Data d => d -> u) -> QName -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> QName -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> QName -> m QName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QName -> m QName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> QName -> m QName)
-> Data QName
QName -> DataType
QName -> Constr
(forall b. Data b => b -> b) -> QName -> QName
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QName -> c QName
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QName
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> QName -> u
forall u. (forall d. Data d => d -> u) -> QName -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QName -> m QName
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QName -> m QName
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QName
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QName -> c QName
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QName)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName)
$cQName :: Constr
$cQual :: Constr
$tQName :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> QName -> m QName
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QName -> m QName
gmapMp :: (forall d. Data d => d -> m d) -> QName -> m QName
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QName -> m QName
gmapM :: (forall d. Data d => d -> m d) -> QName -> m QName
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QName -> m QName
gmapQi :: Int -> (forall d. Data d => d -> u) -> QName -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QName -> u
gmapQ :: (forall d. Data d => d -> u) -> QName -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> QName -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> QName -> r
gmapT :: (forall b. Data b => b -> b) -> QName -> QName
$cgmapT :: (forall b. Data b => b -> b) -> QName -> QName
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c QName)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c QName)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c QName)
dataTypeOf :: QName -> DataType
$cdataTypeOf :: QName -> DataType
toConstr :: QName -> Constr
$ctoConstr :: QName -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QName
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c QName
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QName -> c QName
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QName -> c QName
$cp1Data :: Typeable QName
Data, QName -> QName -> Bool
(QName -> QName -> Bool) -> (QName -> QName -> Bool) -> Eq QName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QName -> QName -> Bool
$c/= :: QName -> QName -> Bool
== :: QName -> QName -> Bool
$c== :: QName -> QName -> Bool
Eq, Eq QName
Eq QName
-> (QName -> QName -> Ordering)
-> (QName -> QName -> Bool)
-> (QName -> QName -> Bool)
-> (QName -> QName -> Bool)
-> (QName -> QName -> Bool)
-> (QName -> QName -> QName)
-> (QName -> QName -> QName)
-> Ord QName
QName -> QName -> Bool
QName -> QName -> Ordering
QName -> QName -> QName
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 :: QName -> QName -> QName
$cmin :: QName -> QName -> QName
max :: QName -> QName -> QName
$cmax :: QName -> QName -> QName
>= :: QName -> QName -> Bool
$c>= :: QName -> QName -> Bool
> :: QName -> QName -> Bool
$c> :: QName -> QName -> Bool
<= :: QName -> QName -> Bool
$c<= :: QName -> QName -> Bool
< :: QName -> QName -> Bool
$c< :: QName -> QName -> Bool
compare :: QName -> QName -> Ordering
$ccompare :: QName -> QName -> Ordering
$cp1Ord :: Eq QName
Ord)

instance Underscore QName where
  underscore :: QName
underscore = Name -> QName
QName Name
forall a. Underscore a => a
underscore
  isUnderscore :: QName -> Bool
isUnderscore (QName Name
x) = Name -> Bool
forall a. Underscore a => a -> Bool
isUnderscore Name
x
  isUnderscore Qual{}    = Bool
False

-- | Top-level module names.  Used in connection with the file system.
--
--   Invariant: The list must not be empty.

data TopLevelModuleName = TopLevelModuleName
  { TopLevelModuleName -> Range
moduleNameRange :: Range
  , TopLevelModuleName -> [RawName]
moduleNameParts :: [String]
  }
  deriving (Int -> TopLevelModuleName -> ShowS
[TopLevelModuleName] -> ShowS
TopLevelModuleName -> RawName
(Int -> TopLevelModuleName -> ShowS)
-> (TopLevelModuleName -> RawName)
-> ([TopLevelModuleName] -> ShowS)
-> Show TopLevelModuleName
forall a.
(Int -> a -> ShowS) -> (a -> RawName) -> ([a] -> ShowS) -> Show a
showList :: [TopLevelModuleName] -> ShowS
$cshowList :: [TopLevelModuleName] -> ShowS
show :: TopLevelModuleName -> RawName
$cshow :: TopLevelModuleName -> RawName
showsPrec :: Int -> TopLevelModuleName -> ShowS
$cshowsPrec :: Int -> TopLevelModuleName -> ShowS
Show, Typeable TopLevelModuleName
DataType
Constr
Typeable TopLevelModuleName
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> TopLevelModuleName
    -> c TopLevelModuleName)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TopLevelModuleName)
-> (TopLevelModuleName -> Constr)
-> (TopLevelModuleName -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TopLevelModuleName))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c TopLevelModuleName))
-> ((forall b. Data b => b -> b)
    -> TopLevelModuleName -> TopLevelModuleName)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> TopLevelModuleName -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> TopLevelModuleName -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> TopLevelModuleName -> m TopLevelModuleName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> TopLevelModuleName -> m TopLevelModuleName)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> TopLevelModuleName -> m TopLevelModuleName)
-> Data TopLevelModuleName
TopLevelModuleName -> DataType
TopLevelModuleName -> Constr
(forall b. Data b => b -> b)
-> TopLevelModuleName -> TopLevelModuleName
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TopLevelModuleName
-> c TopLevelModuleName
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TopLevelModuleName
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> TopLevelModuleName -> u
forall u. (forall d. Data d => d -> u) -> TopLevelModuleName -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> TopLevelModuleName -> m TopLevelModuleName
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> TopLevelModuleName -> m TopLevelModuleName
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TopLevelModuleName
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TopLevelModuleName
-> c TopLevelModuleName
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TopLevelModuleName)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TopLevelModuleName)
$cTopLevelModuleName :: Constr
$tTopLevelModuleName :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> TopLevelModuleName -> m TopLevelModuleName
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> TopLevelModuleName -> m TopLevelModuleName
gmapMp :: (forall d. Data d => d -> m d)
-> TopLevelModuleName -> m TopLevelModuleName
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> TopLevelModuleName -> m TopLevelModuleName
gmapM :: (forall d. Data d => d -> m d)
-> TopLevelModuleName -> m TopLevelModuleName
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> TopLevelModuleName -> m TopLevelModuleName
gmapQi :: Int -> (forall d. Data d => d -> u) -> TopLevelModuleName -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> TopLevelModuleName -> u
gmapQ :: (forall d. Data d => d -> u) -> TopLevelModuleName -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TopLevelModuleName -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TopLevelModuleName -> r
gmapT :: (forall b. Data b => b -> b)
-> TopLevelModuleName -> TopLevelModuleName
$cgmapT :: (forall b. Data b => b -> b)
-> TopLevelModuleName -> TopLevelModuleName
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TopLevelModuleName)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c TopLevelModuleName)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TopLevelModuleName)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TopLevelModuleName)
dataTypeOf :: TopLevelModuleName -> DataType
$cdataTypeOf :: TopLevelModuleName -> DataType
toConstr :: TopLevelModuleName -> Constr
$ctoConstr :: TopLevelModuleName -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TopLevelModuleName
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TopLevelModuleName
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TopLevelModuleName
-> c TopLevelModuleName
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> TopLevelModuleName
-> c TopLevelModuleName
$cp1Data :: Typeable TopLevelModuleName
Data)

instance Eq    TopLevelModuleName where == :: TopLevelModuleName -> TopLevelModuleName -> Bool
(==)    = [RawName] -> [RawName] -> Bool
forall a. Eq a => a -> a -> Bool
(==)    ([RawName] -> [RawName] -> Bool)
-> (TopLevelModuleName -> [RawName])
-> TopLevelModuleName
-> TopLevelModuleName
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` TopLevelModuleName -> [RawName]
moduleNameParts
instance Ord   TopLevelModuleName where compare :: TopLevelModuleName -> TopLevelModuleName -> Ordering
compare = [RawName] -> [RawName] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([RawName] -> [RawName] -> Ordering)
-> (TopLevelModuleName -> [RawName])
-> TopLevelModuleName
-> TopLevelModuleName
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` TopLevelModuleName -> [RawName]
moduleNameParts
instance Sized TopLevelModuleName where size :: TopLevelModuleName -> Int
size    = [RawName] -> Int
forall a. Sized a => a -> Int
size     ([RawName] -> Int)
-> (TopLevelModuleName -> [RawName]) -> TopLevelModuleName -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.   TopLevelModuleName -> [RawName]
moduleNameParts

------------------------------------------------------------------------
-- * Operations on 'Name' and 'NamePart'
------------------------------------------------------------------------

nameToRawName :: Name -> RawName
nameToRawName :: Name -> RawName
nameToRawName = Name -> RawName
forall a. Pretty a => a -> RawName
prettyShow

nameParts :: Name -> [NamePart]
nameParts :: Name -> [NamePart]
nameParts (Name Range
_ NameInScope
_ [NamePart]
ps)    = [NamePart]
ps
nameParts (NoName Range
_ NameId
_)     = [RawName -> NamePart
Id RawName
"_"] -- To not return an empty list

nameStringParts :: Name -> [RawName]
nameStringParts :: Name -> [RawName]
nameStringParts Name
n = [ RawName
s | Id RawName
s <- Name -> [NamePart]
nameParts Name
n ]

-- | Parse a string to parts of a concrete name.
--
--   Note: @stringNameParts "_" == [Id "_"] == nameParts NoName{}@

stringNameParts :: String -> [NamePart]
stringNameParts :: RawName -> [NamePart]
stringNameParts RawName
"_" = [RawName -> NamePart
Id RawName
"_"]   -- NoName
stringNameParts RawName
s = RawName -> [NamePart]
loop RawName
s where
  loop :: RawName -> [NamePart]
loop RawName
""                              = []
  loop (Char
'_':RawName
s)                         = NamePart
Hole NamePart -> [NamePart] -> [NamePart]
forall a. a -> [a] -> [a]
: RawName -> [NamePart]
loop RawName
s
  loop RawName
s | (RawName
x, RawName
s') <- (Char -> Bool) -> RawName -> (RawName, RawName)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_') RawName
s = RawName -> NamePart
Id (ShowS
stringToRawName RawName
x) NamePart -> [NamePart] -> [NamePart]
forall a. a -> [a] -> [a]
: RawName -> [NamePart]
loop RawName
s'

-- | Number of holes in a 'Name' (i.e., arity of a mixfix-operator).
class NumHoles a where
  numHoles :: a -> Int

instance NumHoles [NamePart] where
  numHoles :: [NamePart] -> Int
numHoles = [NamePart] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([NamePart] -> Int)
-> ([NamePart] -> [NamePart]) -> [NamePart] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamePart -> Bool) -> [NamePart] -> [NamePart]
forall a. (a -> Bool) -> [a] -> [a]
filter (NamePart -> NamePart -> Bool
forall a. Eq a => a -> a -> Bool
== NamePart
Hole)

instance NumHoles Name where
  numHoles :: Name -> Int
numHoles NoName{}         = Int
0
  numHoles (Name { nameNameParts :: Name -> [NamePart]
nameNameParts = [NamePart]
parts }) = [NamePart] -> Int
forall a. NumHoles a => a -> Int
numHoles [NamePart]
parts

instance NumHoles QName where
  numHoles :: QName -> Int
numHoles (QName Name
x)  = Name -> Int
forall a. NumHoles a => a -> Int
numHoles Name
x
  numHoles (Qual Name
_ QName
x) = QName -> Int
forall a. NumHoles a => a -> Int
numHoles QName
x

-- | Is the name an operator?

isOperator :: Name -> Bool
isOperator :: Name -> Bool
isOperator (NoName {})     = Bool
False
isOperator (Name Range
_ NameInScope
_ [NamePart]
ps)   = [NamePart] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamePart]
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1

isHole :: NamePart -> Bool
isHole :: NamePart -> Bool
isHole NamePart
Hole = Bool
True
isHole NamePart
_    = Bool
False

isPrefix, isPostfix, isInfix, isNonfix :: Name -> Bool
isPrefix :: Name -> Bool
isPrefix  Name
x = Bool -> Bool
not (NamePart -> Bool
isHole ([NamePart] -> NamePart
forall a. [a] -> a
head [NamePart]
xs)) Bool -> Bool -> Bool
&&      NamePart -> Bool
isHole ([NamePart] -> NamePart
forall a. [a] -> a
last [NamePart]
xs)  where xs :: [NamePart]
xs = Name -> [NamePart]
nameParts Name
x
isPostfix :: Name -> Bool
isPostfix Name
x =      NamePart -> Bool
isHole ([NamePart] -> NamePart
forall a. [a] -> a
head [NamePart]
xs)  Bool -> Bool -> Bool
&& Bool -> Bool
not (NamePart -> Bool
isHole ([NamePart] -> NamePart
forall a. [a] -> a
last [NamePart]
xs)) where xs :: [NamePart]
xs = Name -> [NamePart]
nameParts Name
x
isInfix :: Name -> Bool
isInfix   Name
x =      NamePart -> Bool
isHole ([NamePart] -> NamePart
forall a. [a] -> a
head [NamePart]
xs)  Bool -> Bool -> Bool
&&      NamePart -> Bool
isHole ([NamePart] -> NamePart
forall a. [a] -> a
last [NamePart]
xs)  where xs :: [NamePart]
xs = Name -> [NamePart]
nameParts Name
x
isNonfix :: Name -> Bool
isNonfix  Name
x = Bool -> Bool
not (NamePart -> Bool
isHole ([NamePart] -> NamePart
forall a. [a] -> a
head [NamePart]
xs)) Bool -> Bool -> Bool
&& Bool -> Bool
not (NamePart -> Bool
isHole ([NamePart] -> NamePart
forall a. [a] -> a
last [NamePart]
xs)) where xs :: [NamePart]
xs = Name -> [NamePart]
nameParts Name
x


------------------------------------------------------------------------
-- * Keeping track of which names are (not) in scope
------------------------------------------------------------------------

data NameInScope = InScope | NotInScope
  deriving (NameInScope -> NameInScope -> Bool
(NameInScope -> NameInScope -> Bool)
-> (NameInScope -> NameInScope -> Bool) -> Eq NameInScope
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NameInScope -> NameInScope -> Bool
$c/= :: NameInScope -> NameInScope -> Bool
== :: NameInScope -> NameInScope -> Bool
$c== :: NameInScope -> NameInScope -> Bool
Eq, Int -> NameInScope -> ShowS
[NameInScope] -> ShowS
NameInScope -> RawName
(Int -> NameInScope -> ShowS)
-> (NameInScope -> RawName)
-> ([NameInScope] -> ShowS)
-> Show NameInScope
forall a.
(Int -> a -> ShowS) -> (a -> RawName) -> ([a] -> ShowS) -> Show a
showList :: [NameInScope] -> ShowS
$cshowList :: [NameInScope] -> ShowS
show :: NameInScope -> RawName
$cshow :: NameInScope -> RawName
showsPrec :: Int -> NameInScope -> ShowS
$cshowsPrec :: Int -> NameInScope -> ShowS
Show, Typeable NameInScope
DataType
Constr
Typeable NameInScope
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> NameInScope -> c NameInScope)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c NameInScope)
-> (NameInScope -> Constr)
-> (NameInScope -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c NameInScope))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c NameInScope))
-> ((forall b. Data b => b -> b) -> NameInScope -> NameInScope)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NameInScope -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NameInScope -> r)
-> (forall u. (forall d. Data d => d -> u) -> NameInScope -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> NameInScope -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> NameInScope -> m NameInScope)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NameInScope -> m NameInScope)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NameInScope -> m NameInScope)
-> Data NameInScope
NameInScope -> DataType
NameInScope -> Constr
(forall b. Data b => b -> b) -> NameInScope -> NameInScope
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NameInScope -> c NameInScope
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NameInScope
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> NameInScope -> u
forall u. (forall d. Data d => d -> u) -> NameInScope -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NameInScope -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NameInScope -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NameInScope -> m NameInScope
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NameInScope -> m NameInScope
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NameInScope
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NameInScope -> c NameInScope
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NameInScope)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NameInScope)
$cNotInScope :: Constr
$cInScope :: Constr
$tNameInScope :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> NameInScope -> m NameInScope
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NameInScope -> m NameInScope
gmapMp :: (forall d. Data d => d -> m d) -> NameInScope -> m NameInScope
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NameInScope -> m NameInScope
gmapM :: (forall d. Data d => d -> m d) -> NameInScope -> m NameInScope
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NameInScope -> m NameInScope
gmapQi :: Int -> (forall d. Data d => d -> u) -> NameInScope -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> NameInScope -> u
gmapQ :: (forall d. Data d => d -> u) -> NameInScope -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> NameInScope -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NameInScope -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NameInScope -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NameInScope -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NameInScope -> r
gmapT :: (forall b. Data b => b -> b) -> NameInScope -> NameInScope
$cgmapT :: (forall b. Data b => b -> b) -> NameInScope -> NameInScope
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NameInScope)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NameInScope)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c NameInScope)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NameInScope)
dataTypeOf :: NameInScope -> DataType
$cdataTypeOf :: NameInScope -> DataType
toConstr :: NameInScope -> Constr
$ctoConstr :: NameInScope -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NameInScope
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NameInScope
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NameInScope -> c NameInScope
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NameInScope -> c NameInScope
$cp1Data :: Typeable NameInScope
Data)

class LensInScope a where
  lensInScope :: Lens' NameInScope a

  isInScope :: a -> NameInScope
  isInScope a
x = a
x a -> Lens' NameInScope a -> NameInScope
forall o i. o -> Lens' i o -> i
^. forall a. LensInScope a => Lens' NameInScope a
Lens' NameInScope a
lensInScope

  mapInScope :: (NameInScope -> NameInScope) -> a -> a
  mapInScope = Lens' NameInScope a -> (NameInScope -> NameInScope) -> a -> a
forall i o. Lens' i o -> LensMap i o
over forall a. LensInScope a => Lens' NameInScope a
Lens' NameInScope a
lensInScope

  setInScope :: a -> a
  setInScope = (NameInScope -> NameInScope) -> a -> a
forall a. LensInScope a => (NameInScope -> NameInScope) -> a -> a
mapInScope ((NameInScope -> NameInScope) -> a -> a)
-> (NameInScope -> NameInScope) -> a -> a
forall a b. (a -> b) -> a -> b
$ NameInScope -> NameInScope -> NameInScope
forall a b. a -> b -> a
const NameInScope
InScope

  setNotInScope :: a -> a
  setNotInScope = (NameInScope -> NameInScope) -> a -> a
forall a. LensInScope a => (NameInScope -> NameInScope) -> a -> a
mapInScope ((NameInScope -> NameInScope) -> a -> a)
-> (NameInScope -> NameInScope) -> a -> a
forall a b. (a -> b) -> a -> b
$ NameInScope -> NameInScope -> NameInScope
forall a b. a -> b -> a
const NameInScope
NotInScope

instance LensInScope NameInScope where
  lensInScope :: (NameInScope -> f NameInScope) -> NameInScope -> f NameInScope
lensInScope = (NameInScope -> f NameInScope) -> NameInScope -> f NameInScope
forall a. a -> a
id

instance LensInScope Name where
  lensInScope :: (NameInScope -> f NameInScope) -> Name -> f Name
lensInScope NameInScope -> f NameInScope
f = \case
    n :: Name
n@Name{ nameInScope :: Name -> NameInScope
nameInScope = NameInScope
nis } -> (\NameInScope
nis' -> Name
n { nameInScope :: NameInScope
nameInScope = NameInScope
nis' }) (NameInScope -> Name) -> f NameInScope -> f Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameInScope -> f NameInScope
f NameInScope
nis
    n :: Name
n@NoName{} -> Name -> NameInScope -> Name
forall a b. a -> b -> a
const Name
n (NameInScope -> Name) -> f NameInScope -> f Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameInScope -> f NameInScope
f NameInScope
InScope

instance LensInScope QName where
  lensInScope :: (NameInScope -> f NameInScope) -> QName -> f QName
lensInScope NameInScope -> f NameInScope
f = \case
    Qual Name
x QName
xs -> (Name -> QName -> QName
`Qual` QName
xs) (Name -> QName) -> f Name -> f QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NameInScope -> f NameInScope) -> Name -> f Name
forall a. LensInScope a => Lens' NameInScope a
lensInScope NameInScope -> f NameInScope
f Name
x
    QName Name
x   -> Name -> QName
QName (Name -> QName) -> f Name -> f QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NameInScope -> f NameInScope) -> Name -> f Name
forall a. LensInScope a => Lens' NameInScope a
lensInScope NameInScope -> f NameInScope
f Name
x

------------------------------------------------------------------------
-- * Generating fresh names
------------------------------------------------------------------------

nextStr :: String -> String
nextStr :: ShowS
nextStr RawName
s = case RawName -> (RawName, Suffix)
suffixView RawName
s of
  (RawName
s0, Suffix
suf) -> RawName -> Suffix -> RawName
addSuffix RawName
s0 (Suffix -> Suffix
nextSuffix Suffix
suf)

-- | Get the next version of the concrete name. For instance,
--   @nextName "x" = "x₁"@.  The name must not be a 'NoName'.
nextName :: Name -> Name
nextName :: Name -> Name
nextName NoName{} = Name
forall a. HasCallStack => a
__IMPOSSIBLE__
nextName x :: Name
x@Name{ nameNameParts :: Name -> [NamePart]
nameNameParts = [NamePart]
ps } = Name
x { nameInScope :: NameInScope
nameInScope = NameInScope
NotInScope, nameNameParts :: [NamePart]
nameNameParts = [NamePart] -> [NamePart]
nextSuf [NamePart]
ps }
  where
    nextSuf :: [NamePart] -> [NamePart]
nextSuf [Id RawName
s]       = [RawName -> NamePart
Id (RawName -> NamePart) -> RawName -> NamePart
forall a b. (a -> b) -> a -> b
$ ShowS
nextStr RawName
s]
    nextSuf [Id RawName
s, NamePart
Hole] = [RawName -> NamePart
Id (RawName -> NamePart) -> RawName -> NamePart
forall a b. (a -> b) -> a -> b
$ ShowS
nextStr RawName
s, NamePart
Hole]
    nextSuf (NamePart
p : [NamePart]
ps)     = NamePart
p NamePart -> [NamePart] -> [NamePart]
forall a. a -> [a] -> [a]
: [NamePart] -> [NamePart]
nextSuf [NamePart]
ps
    nextSuf []           = [NamePart]
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Get the first version of the concrete name that does not satisfy
--   the given predicate.
firstNonTakenName :: (Name -> Bool) -> Name -> Name
firstNonTakenName :: (Name -> Bool) -> Name -> Name
firstNonTakenName Name -> Bool
taken Name
x =
  if Name -> Bool
taken Name
x
  then (Name -> Bool) -> Name -> Name
firstNonTakenName Name -> Bool
taken (Name -> Name
nextName Name
x)
  else Name
x

-- | Get a raw version of the name with all suffixes removed. For
--   instance, @nameRoot "x₁₂₃" = "x"@. The name must not be a
--   'NoName'.
nameRoot :: Name -> RawName
nameRoot :: Name -> RawName
nameRoot NoName{} = RawName
forall a. HasCallStack => a
__IMPOSSIBLE__
nameRoot x :: Name
x@Name{ nameNameParts :: Name -> [NamePart]
nameNameParts = [NamePart]
ps } =
    Name -> RawName
nameToRawName (Name -> RawName) -> Name -> RawName
forall a b. (a -> b) -> a -> b
$ Name
x{ nameNameParts :: [NamePart]
nameNameParts = [NamePart] -> [NamePart]
root [NamePart]
ps }
  where
    root :: [NamePart] -> [NamePart]
root [Id RawName
s] = [RawName -> NamePart
Id (RawName -> NamePart) -> RawName -> NamePart
forall a b. (a -> b) -> a -> b
$ ShowS
strRoot RawName
s]
    root [Id RawName
s, NamePart
Hole] = [RawName -> NamePart
Id (RawName -> NamePart) -> RawName -> NamePart
forall a b. (a -> b) -> a -> b
$ ShowS
strRoot RawName
s , NamePart
Hole]
    root (NamePart
p : [NamePart]
ps) = NamePart
p NamePart -> [NamePart] -> [NamePart]
forall a. a -> [a] -> [a]
: [NamePart] -> [NamePart]
root [NamePart]
ps
    root [] = [NamePart]
forall a. HasCallStack => a
__IMPOSSIBLE__
    strRoot :: ShowS
strRoot = (RawName, Suffix) -> RawName
forall a b. (a, b) -> a
fst ((RawName, Suffix) -> RawName)
-> (RawName -> (RawName, Suffix)) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawName -> (RawName, Suffix)
suffixView

sameRoot :: Name -> Name -> Bool
sameRoot :: Name -> Name -> Bool
sameRoot = RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
(==) (RawName -> RawName -> Bool)
-> (Name -> RawName) -> Name -> Name -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> RawName
nameRoot

------------------------------------------------------------------------
-- * Operations on qualified names
------------------------------------------------------------------------

-- | @qualify A.B x == A.B.x@
qualify :: QName -> Name -> QName
qualify :: QName -> Name -> QName
qualify (QName Name
m) Name
x     = Name -> QName -> QName
Qual Name
m (Name -> QName
QName Name
x)
qualify (Qual Name
m QName
m') Name
x   = Name -> QName -> QName
Qual Name
m (QName -> QName) -> QName -> QName
forall a b. (a -> b) -> a -> b
$ QName -> Name -> QName
qualify QName
m' Name
x

-- | @unqualify A.B.x == x@
--
-- The range is preserved.
unqualify :: QName -> Name
unqualify :: QName -> Name
unqualify QName
q = QName -> Name
unqualify' QName
q Name -> QName -> Name
forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` QName
q
  where
  unqualify' :: QName -> Name
unqualify' (QName Name
x)  = Name
x
  unqualify' (Qual Name
_ QName
x) = QName -> Name
unqualify' QName
x

-- | @qnameParts A.B.x = [A, B, x]@
qnameParts :: QName -> [Name]
qnameParts :: QName -> [Name]
qnameParts (Qual Name
x QName
q) = Name
x Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: QName -> [Name]
qnameParts QName
q
qnameParts (QName Name
x)  = [Name
x]

-- | Is the name (un)qualified?

isQualified :: QName -> Bool
isQualified :: QName -> Bool
isQualified Qual{}  = Bool
True
isQualified QName{} = Bool
False

isUnqualified :: QName -> Maybe Name
isUnqualified :: QName -> Maybe Name
isUnqualified Qual{}    = Maybe Name
forall a. Maybe a
Nothing
isUnqualified (QName Name
n) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n

------------------------------------------------------------------------
-- * Operations on 'TopLevelModuleName'
------------------------------------------------------------------------

-- | Turns a qualified name into a 'TopLevelModuleName'. The qualified
-- name is assumed to represent a top-level module name.

toTopLevelModuleName :: QName -> TopLevelModuleName
toTopLevelModuleName :: QName -> TopLevelModuleName
toTopLevelModuleName QName
q = Range -> [RawName] -> TopLevelModuleName
TopLevelModuleName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
q) ([RawName] -> TopLevelModuleName)
-> [RawName] -> TopLevelModuleName
forall a b. (a -> b) -> a -> b
$ (Name -> RawName) -> [Name] -> [RawName]
forall a b. (a -> b) -> [a] -> [b]
map Name -> RawName
forall a. Pretty a => a -> RawName
prettyShow ([Name] -> [RawName]) -> [Name] -> [RawName]
forall a b. (a -> b) -> a -> b
$ QName -> [Name]
qnameParts QName
q

-- UNUSED
-- -- | Turns a top level module into a qualified name with 'noRange'.

-- fromTopLevelModuleName :: TopLevelModuleName -> QName
-- fromTopLevelModuleName (TopLevelModuleName _ [])     = __IMPOSSIBLE__
-- fromTopLevelModuleName (TopLevelModuleName _ (x:xs)) = loop x xs
--   where
--   loop x []       = QName (mk x)
--   loop x (y : ys) = Qual  (mk x) $ loop y ys
--   mk :: String -> Name
--   mk x = Name noRange [Id x]

-- | Turns a top-level module name into a file name with the given
-- suffix.

moduleNameToFileName :: TopLevelModuleName -> String -> FilePath
moduleNameToFileName :: TopLevelModuleName -> ShowS
moduleNameToFileName (TopLevelModuleName Range
_ []) RawName
ext = RawName
forall a. HasCallStack => a
__IMPOSSIBLE__
moduleNameToFileName (TopLevelModuleName Range
_ [RawName]
ms) RawName
ext =
  [RawName] -> RawName
joinPath ([RawName] -> [RawName]
forall a. [a] -> [a]
init [RawName]
ms) RawName -> ShowS
</> [RawName] -> RawName
forall a. [a] -> a
last [RawName]
ms RawName -> ShowS
<.> RawName
ext

-- | Finds the current project's \"root\" directory, given a project
-- file and the corresponding top-level module name.
--
-- Example: If the module \"A.B.C\" is located in the file
-- \"/foo/A/B/C.agda\", then the root is \"/foo/\".
--
-- Precondition: The module name must be well-formed.

projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot AbsolutePath
file (TopLevelModuleName Range
_ [RawName]
m) =
  RawName -> AbsolutePath
mkAbsolute (RawName -> AbsolutePath) -> RawName -> AbsolutePath
forall a b. (a -> b) -> a -> b
$
  (ShowS -> ShowS -> ShowS) -> ShowS -> [ShowS] -> ShowS
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ShowS
forall a. a -> a
id (Int -> ShowS -> [ShowS]
forall a. Int -> a -> [a]
replicate ([RawName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RawName]
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ShowS
takeDirectory) ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
  ShowS
takeDirectory ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
  AbsolutePath -> RawName
filePath AbsolutePath
file

------------------------------------------------------------------------
-- * No name stuff
------------------------------------------------------------------------

-- | @noName_ = 'noName' 'noRange'@
noName_ :: Name
noName_ :: Name
noName_ = Range -> Name
noName Range
forall a. Range' a
noRange

noName :: Range -> Name
noName :: Range -> Name
noName Range
r = Range -> NameId -> Name
NoName Range
r (Word64 -> Word64 -> NameId
NameId Word64
0 Word64
0)

-- | Check whether a name is the empty name "_".
class IsNoName a where
  isNoName :: a -> Bool

  default isNoName :: (Foldable t, IsNoName b, t b ~ a) => a -> Bool
  isNoName = (b -> Bool) -> t b -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Fold.all b -> Bool
forall a. IsNoName a => a -> Bool
isNoName

instance IsNoName String where
  isNoName :: RawName -> Bool
isNoName = RawName -> Bool
forall a. Underscore a => a -> Bool
isUnderscore

instance IsNoName ByteString where
  isNoName :: ByteString -> Bool
isNoName = ByteString -> Bool
forall a. Underscore a => a -> Bool
isUnderscore

instance IsNoName Name where
  isNoName :: Name -> Bool
isNoName (NoName Range
_ NameId
_)      = Bool
True
  isNoName (Name Range
_ NameInScope
_ [NamePart
Hole]) = Bool
True   -- TODO: Track down where these come from
  isNoName (Name Range
_ NameInScope
_ [])     = Bool
True
  isNoName (Name Range
_ NameInScope
_ [Id RawName
x]) = RawName -> Bool
forall a. IsNoName a => a -> Bool
isNoName RawName
x
  isNoName Name
_                 = Bool
False

instance IsNoName QName where
  isNoName :: QName -> Bool
isNoName (QName Name
x) = Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x
  isNoName Qual{}    = Bool
False        -- M.A._ does not qualify as empty name

instance IsNoName a => IsNoName (Ranged a) where
instance IsNoName a => IsNoName (WithOrigin a) where

-- no instance for TopLevelModuleName

------------------------------------------------------------------------
-- * Showing names
------------------------------------------------------------------------

-- deriving instance Show Name
-- deriving instance Show NamePart
-- deriving instance Show QName

-- TODO: 'Show' should output Haskell-parseable representations.
-- The following instances are deprecated, and Pretty should be used
-- instead.  Later, simply derive Show for these types:

instance Show Name where
  show :: Name -> RawName
show = Name -> RawName
forall a. Pretty a => a -> RawName
prettyShow

instance Show NamePart where
  show :: NamePart -> RawName
show = NamePart -> RawName
forall a. Pretty a => a -> RawName
prettyShow

instance Show QName where
  show :: QName -> RawName
show = QName -> RawName
forall a. Pretty a => a -> RawName
prettyShow

------------------------------------------------------------------------
-- * Printing names
------------------------------------------------------------------------

instance Pretty Name where
  pretty :: Name -> Doc
pretty (Name Range
_ NameInScope
_ [NamePart]
xs)    = [Doc] -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (NamePart -> Doc) -> [NamePart] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamePart -> Doc
forall a. Pretty a => a -> Doc
pretty [NamePart]
xs
  pretty (NoName Range
_ NameId
_)     = Doc
"_"

instance Pretty NamePart where
  pretty :: NamePart -> Doc
pretty NamePart
Hole   = Doc
"_"
  pretty (Id RawName
s) = RawName -> Doc
text (RawName -> Doc) -> RawName -> Doc
forall a b. (a -> b) -> a -> b
$ ShowS
rawNameToString RawName
s

instance Pretty QName where
  pretty :: QName -> Doc
pretty (Qual Name
m QName
x)
    | Name -> Bool
forall a. Underscore a => a -> Bool
isUnderscore Name
m = QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x -- don't print anonymous modules
    | Bool
otherwise      = Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
m Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"." Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
  pretty (QName Name
x)  = Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x

instance Pretty TopLevelModuleName where
  pretty :: TopLevelModuleName -> Doc
pretty (TopLevelModuleName Range
_ [RawName]
ms) = RawName -> Doc
text (RawName -> Doc) -> RawName -> Doc
forall a b. (a -> b) -> a -> b
$ RawName -> [RawName] -> RawName
forall a. [a] -> [[a]] -> [a]
List.intercalate RawName
"." [RawName]
ms

------------------------------------------------------------------------
-- * Range instances
------------------------------------------------------------------------

instance HasRange Name where
    getRange :: Name -> Range
getRange (Name Range
r NameInScope
_ [NamePart]
ps)    = Range
r
    getRange (NoName Range
r NameId
_)     = Range
r

instance HasRange QName where
    getRange :: QName -> Range
getRange (QName  Name
x) = Name -> Range
forall t. HasRange t => t -> Range
getRange Name
x
    getRange (Qual Name
n QName
x) = Name -> QName -> Range
forall u t. (HasRange u, HasRange t) => u -> t -> Range
fuseRange Name
n QName
x

instance HasRange TopLevelModuleName where
  getRange :: TopLevelModuleName -> Range
getRange = TopLevelModuleName -> Range
moduleNameRange

instance SetRange Name where
  setRange :: Range -> Name -> Name
setRange Range
r (Name Range
_ NameInScope
nis [NamePart]
ps) = Range -> NameInScope -> [NamePart] -> Name
Name Range
r NameInScope
nis [NamePart]
ps
  setRange Range
r (NoName Range
_ NameId
i)  = Range -> NameId -> Name
NoName Range
r NameId
i

instance SetRange QName where
  setRange :: Range -> QName -> QName
setRange Range
r (QName Name
x)  = Name -> QName
QName (Range -> Name -> Name
forall t. SetRange t => Range -> t -> t
setRange Range
r Name
x)
  setRange Range
r (Qual Name
n QName
x) = Name -> QName -> QName
Qual (Range -> Name -> Name
forall t. SetRange t => Range -> t -> t
setRange Range
r Name
n) (Range -> QName -> QName
forall t. SetRange t => Range -> t -> t
setRange Range
r QName
x)

instance SetRange TopLevelModuleName where
  setRange :: Range -> TopLevelModuleName -> TopLevelModuleName
setRange Range
r (TopLevelModuleName Range
_ [RawName]
x) = Range -> [RawName] -> TopLevelModuleName
TopLevelModuleName Range
r [RawName]
x

instance KillRange QName where
  killRange :: QName -> QName
killRange (QName Name
x) = Name -> QName
QName (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ Name -> Name
forall a. KillRange a => KillRangeT a
killRange Name
x
  killRange (Qual Name
n QName
x) = Name -> Name
forall a. KillRange a => KillRangeT a
killRange Name
n Name -> QName -> QName
`Qual` QName -> QName
forall a. KillRange a => KillRangeT a
killRange QName
x

instance KillRange Name where
  killRange :: Name -> Name
killRange (Name Range
r NameInScope
nis [NamePart]
ps)  = Range -> NameInScope -> [NamePart] -> Name
Name (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) NameInScope
nis [NamePart]
ps
  killRange (NoName Range
r NameId
i)     = Range -> NameId -> Name
NoName (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) NameId
i

instance KillRange TopLevelModuleName where
  killRange :: TopLevelModuleName -> TopLevelModuleName
killRange (TopLevelModuleName Range
_ [RawName]
x) = Range -> [RawName] -> TopLevelModuleName
TopLevelModuleName Range
forall a. Range' a
noRange [RawName]
x

------------------------------------------------------------------------
-- * NFData instances
------------------------------------------------------------------------

-- | Ranges are not forced.

instance NFData NameInScope where
  rnf :: NameInScope -> ()
rnf NameInScope
InScope    = ()
  rnf NameInScope
NotInScope = ()

instance NFData Name where
  rnf :: Name -> ()
rnf (Name Range
_ NameInScope
nis [NamePart]
ns) = NameInScope -> ()
forall a. NFData a => a -> ()
rnf NameInScope
nis () -> () -> ()
`seq` [NamePart] -> ()
forall a. NFData a => a -> ()
rnf [NamePart]
ns
  rnf (NoName Range
_ NameId
n)  = NameId -> ()
forall a. NFData a => a -> ()
rnf NameId
n

instance NFData NamePart where
  rnf :: NamePart -> ()
rnf NamePart
Hole   = ()
  rnf (Id RawName
s) = RawName -> ()
forall a. NFData a => a -> ()
rnf RawName
s

instance NFData QName where
  rnf :: QName -> ()
rnf (Qual Name
a QName
b) = Name -> ()
forall a. NFData a => a -> ()
rnf Name
a () -> () -> ()
`seq` QName -> ()
forall a. NFData a => a -> ()
rnf QName
b
  rnf (QName Name
a)  = Name -> ()
forall a. NFData a => a -> ()
rnf Name
a