{-# 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 n :: Name
n = case Name
n of
  Name _ _ (x :: NamePart
x : xs :: [NamePart]
xs@(_:_)) -> 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
  _                       -> 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 x :: RawName
x]}) = RawName -> Bool
forall a. Underscore a => a -> Bool
isUnderscore RawName
x
  isUnderscore _ = 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 _ _ xs :: [NamePart]
xs    == :: Name -> Name -> Bool
== Name _ _ ys :: [NamePart]
ys    = [NamePart]
xs [NamePart] -> [NamePart] -> Bool
forall a. Eq a => a -> a -> Bool
== [NamePart]
ys
    NoName _ i :: NameId
i     == NoName _ j :: NameId
j     = NameId
i NameId -> NameId -> Bool
forall a. Eq a => a -> a -> Bool
== NameId
j
    _              == _              = Bool
False

instance Ord Name where
    compare :: Name -> Name -> Ordering
compare (Name _ _ xs :: [NamePart]
xs)  (Name _ _ ys :: [NamePart]
ys)      = [NamePart] -> [NamePart] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare [NamePart]
xs [NamePart]
ys
    compare (NoName _ i :: NameId
i)   (NoName _ j :: 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
  Hole  == :: NamePart -> NamePart -> Bool
== Hole  = Bool
True
  Id s1 :: RawName
s1 == Id s2 :: RawName
s2 = RawName
s1 RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
== RawName
s2
  _     == _     = Bool
False

instance Ord NamePart where
  compare :: NamePart -> NamePart -> Ordering
compare Hole    Hole    = Ordering
EQ
  compare Hole    (Id {}) = Ordering
LT
  compare (Id {}) Hole    = Ordering
GT
  compare (Id s1 :: RawName
s1) (Id s2 :: 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 x :: 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 _ _ ps :: [NamePart]
ps)    = [NamePart]
ps
nameParts (NoName _ _)     = [RawName -> NamePart
Id "_"] -- To not return an empty list

nameStringParts :: Name -> [RawName]
nameStringParts :: Name -> [RawName]
nameStringParts n :: Name
n = [ RawName
s | Id s :: 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 -> NamePart
Id "_"]   -- NoName
stringNameParts s :: RawName
s = RawName -> [NamePart]
loop RawName
s where
  loop :: RawName -> [NamePart]
loop ""                              = []
  loop ('_':s :: RawName
s)                         = NamePart
Hole NamePart -> [NamePart] -> [NamePart]
forall a. a -> [a] -> [a]
: RawName -> [NamePart]
loop RawName
s
  loop s :: RawName
s | (x :: RawName
x, s' :: 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
== '_') 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{}         = 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 x :: Name
x)  = Name -> Int
forall a. NumHoles a => a -> Int
numHoles Name
x
  numHoles (Qual _ x :: 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 _ _ ps :: [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
> 1

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

isPrefix, isPostfix, isInfix, isNonfix :: Name -> Bool
isPrefix :: Name -> Bool
isPrefix  x :: 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 x :: 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   x :: 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  x :: 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 x :: 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 f :: NameInScope -> f NameInScope
f = \case
    n :: Name
n@Name{ nameInScope :: Name -> NameInScope
nameInScope = NameInScope
nis } -> (\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 f :: NameInScope -> f NameInScope
f = \case
    Qual x :: Name
x xs :: 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 x :: 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 s :: RawName
s = case RawName -> (RawName, Suffix)
suffixView RawName
s of
  (s0 :: RawName
s0, suf :: 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 s :: RawName
s]       = [RawName -> NamePart
Id (RawName -> NamePart) -> RawName -> NamePart
forall a b. (a -> b) -> a -> b
$ ShowS
nextStr RawName
s]
    nextSuf [Id s :: RawName
s, Hole] = [RawName -> NamePart
Id (RawName -> NamePart) -> RawName -> NamePart
forall a b. (a -> b) -> a -> b
$ ShowS
nextStr RawName
s, NamePart
Hole]
    nextSuf (p :: NamePart
p : ps :: [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 taken :: Name -> Bool
taken x :: 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 s :: RawName
s] = [RawName -> NamePart
Id (RawName -> NamePart) -> RawName -> NamePart
forall a b. (a -> b) -> a -> b
$ ShowS
strRoot RawName
s]
    root [Id s :: RawName
s, Hole] = [RawName -> NamePart
Id (RawName -> NamePart) -> RawName -> NamePart
forall a b. (a -> b) -> a -> b
$ ShowS
strRoot RawName
s , NamePart
Hole]
    root (p :: NamePart
p : ps :: [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 m :: Name
m) x :: Name
x     = Name -> QName -> QName
Qual Name
m (Name -> QName
QName Name
x)
qualify (Qual m :: Name
m m' :: QName
m') x :: 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 q :: 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 x :: Name
x)  = Name
x
  unqualify' (Qual _ x :: QName
x) = QName -> Name
unqualify' QName
x

-- | @qnameParts A.B.x = [A, B, x]@
qnameParts :: QName -> [Name]
qnameParts :: QName -> [Name]
qnameParts (Qual x :: Name
x q :: QName
q) = Name
x Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: QName -> [Name]
qnameParts QName
q
qnameParts (QName x :: 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 n :: 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 q :: 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 _ []) ext :: RawName
ext = RawName
forall a. HasCallStack => a
__IMPOSSIBLE__
moduleNameToFileName (TopLevelModuleName _ ms :: [RawName]
ms) ext :: 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 file :: AbsolutePath
file (TopLevelModuleName _ m :: [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
- 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 r :: Range
r = Range -> NameId -> Name
NoName Range
r (Word64 -> Word64 -> NameId
NameId 0 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 _ _)      = Bool
True
  isNoName (Name _ _ [Hole]) = Bool
True   -- TODO: Track down where these come from
  isNoName (Name _ _ [])     = Bool
True
  isNoName (Name _ _ [Id x :: RawName
x]) = RawName -> Bool
forall a. IsNoName a => a -> Bool
isNoName RawName
x
  isNoName _                 = Bool
False

instance IsNoName QName where
  isNoName :: QName -> Bool
isNoName (QName x :: 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 _ _ xs :: [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 _ _)     = "_"

instance Pretty NamePart where
  pretty :: NamePart -> Doc
pretty Hole   = "_"
  pretty (Id s :: 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 m :: Name
m x :: 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
forall a. Semigroup a => a -> a -> a
<> QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x
  pretty (QName x :: Name
x)  = Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x

instance Pretty TopLevelModuleName where
  pretty :: TopLevelModuleName -> Doc
pretty (TopLevelModuleName _ ms :: [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]
ms

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

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

instance HasRange QName where
    getRange :: QName -> Range
getRange (QName  x :: Name
x) = Name -> Range
forall t. HasRange t => t -> Range
getRange Name
x
    getRange (Qual n :: Name
n x :: 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 r :: Range
r (Name _ nis :: NameInScope
nis ps :: [NamePart]
ps) = Range -> NameInScope -> [NamePart] -> Name
Name Range
r NameInScope
nis [NamePart]
ps
  setRange r :: Range
r (NoName _ i :: NameId
i)  = Range -> NameId -> Name
NoName Range
r NameId
i

instance SetRange QName where
  setRange :: Range -> QName -> QName
setRange r :: Range
r (QName x :: Name
x)  = Name -> QName
QName (Range -> Name -> Name
forall t. SetRange t => Range -> t -> t
setRange Range
r Name
x)
  setRange r :: Range
r (Qual n :: Name
n x :: 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 r :: Range
r (TopLevelModuleName _ x :: [RawName]
x) = Range -> [RawName] -> TopLevelModuleName
TopLevelModuleName Range
r [RawName]
x

instance KillRange QName where
  killRange :: QName -> QName
killRange (QName x :: 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 n :: Name
n x :: 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 r :: Range
r nis :: NameInScope
nis ps :: [NamePart]
ps)  = Range -> NameInScope -> [NamePart] -> Name
Name (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) NameInScope
nis [NamePart]
ps
  killRange (NoName r :: Range
r i :: 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 _ x :: [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 InScope    = ()
  rnf NotInScope = ()

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

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

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