{-| 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.Concrete.Glyph
import Agda.Syntax.Position

import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.List  (last1)
import Agda.Utils.List1 (List1, pattern (:|), (<|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Pretty
import Agda.Utils.Singleton
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 -> NameParts
nameNameParts :: NameParts
    }
  | 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

type NameParts = List1 NamePart

-- | 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 = \case
  Name Range
_ NameInScope
_ (NamePart
x :| NamePart
x' : [NamePart]
xs) -> NamePart
x NamePart -> NamePart -> Bool
forall a. Eq a => a -> a -> Bool
== NamePart
Hole Bool -> Bool -> Bool
|| NamePart -> [NamePart] -> NamePart
forall a. a -> [a] -> a
last1 NamePart
x' [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 -> NameParts
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
_ NameParts
xs    == :: Name -> Name -> Bool
== Name Range
_ NameInScope
_ NameParts
ys    = NameParts
xs NameParts -> NameParts -> Bool
forall a. Eq a => a -> a -> Bool
== NameParts
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
_ NameParts
xs)  (Name Range
_ NameInScope
_ NameParts
ys)      = NameParts -> NameParts -> Ordering
forall a. Ord a => a -> a -> Ordering
compare NameParts
xs NameParts
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 -> List1 RawName
moduleNameParts :: List1 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, (forall x. TopLevelModuleName -> Rep TopLevelModuleName x)
-> (forall x. Rep TopLevelModuleName x -> TopLevelModuleName)
-> Generic TopLevelModuleName
forall x. Rep TopLevelModuleName x -> TopLevelModuleName
forall x. TopLevelModuleName -> Rep TopLevelModuleName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TopLevelModuleName x -> TopLevelModuleName
$cfrom :: forall x. TopLevelModuleName -> Rep TopLevelModuleName x
Generic)

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

------------------------------------------------------------------------
-- * Constructing simple 'Name's.
------------------------------------------------------------------------

-- | Create an ordinary 'InScope' name.
simpleName :: RawName -> Name
simpleName :: RawName -> Name
simpleName = Range -> NameInScope -> NameParts -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope (NameParts -> Name) -> (RawName -> NameParts) -> RawName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamePart -> NameParts
forall el coll. Singleton el coll => el -> coll
singleton (NamePart -> NameParts)
-> (RawName -> NamePart) -> RawName -> NameParts
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawName -> NamePart
Id

-- | Create a binary operator name in scope.
simpleBinaryOperator :: RawName -> Name
simpleBinaryOperator :: RawName -> Name
simpleBinaryOperator RawName
s = Range -> NameInScope -> NameParts -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope (NameParts -> Name) -> NameParts -> Name
forall a b. (a -> b) -> a -> b
$ NamePart
Hole NamePart -> [NamePart] -> NameParts
forall a. a -> [a] -> NonEmpty a
:| RawName -> NamePart
Id RawName
s NamePart -> [NamePart] -> [NamePart]
forall a. a -> [a] -> [a]
: NamePart
Hole NamePart -> [NamePart] -> [NamePart]
forall a. a -> [a] -> [a]
: []

-- | Create an ordinary 'InScope' name containing a single 'Hole'.
simpleHole :: Name
simpleHole :: Name
simpleHole = Range -> NameInScope -> NameParts -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope (NameParts -> Name) -> NameParts -> Name
forall a b. (a -> b) -> a -> b
$ NamePart -> NameParts
forall el coll. Singleton el coll => el -> coll
singleton NamePart
Hole

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

-- | Don't use on 'NoName{}'.
lensNameParts :: Lens' NameParts Name
lensNameParts :: (NameParts -> f NameParts) -> Name -> f Name
lensNameParts NameParts -> f NameParts
f = \case
  n :: Name
n@Name{} -> NameParts -> f NameParts
f (Name -> NameParts
nameNameParts Name
n) f NameParts -> (NameParts -> Name) -> f Name
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ NameParts
ps -> Name
n { nameNameParts :: NameParts
nameNameParts = NameParts
ps }
  NoName{} -> f Name
forall a. HasCallStack => a
__IMPOSSIBLE__

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

nameParts :: Name -> NameParts
nameParts :: Name -> NameParts
nameParts (Name Range
_ NameInScope
_ NameParts
ps)    = NameParts
ps
nameParts (NoName Range
_ NameId
_)     = NamePart -> NameParts
forall el coll. Singleton el coll => el -> coll
singleton (NamePart -> NameParts) -> NamePart -> NameParts
forall a b. (a -> b) -> a -> b
$ RawName -> NamePart
Id RawName
"_" -- To not return an empty list

nameStringParts :: Name -> [RawName]
nameStringParts :: Name -> [RawName]
nameStringParts Name
n = [ RawName
s | Id RawName
s <- NameParts -> [NamePart]
forall a. NonEmpty a -> [a]
List1.toList (NameParts -> [NamePart]) -> NameParts -> [NamePart]
forall a b. (a -> b) -> a -> b
$ Name -> NameParts
nameParts Name
n ]

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

stringNameParts :: String -> NameParts
stringNameParts :: RawName -> NameParts
stringNameParts RawName
""  = NamePart -> NameParts
forall el coll. Singleton el coll => el -> coll
singleton (NamePart -> NameParts) -> NamePart -> NameParts
forall a b. (a -> b) -> a -> b
$ RawName -> NamePart
Id RawName
"_"  -- NoName
stringNameParts RawName
"_" = NamePart -> NameParts
forall el coll. Singleton el coll => el -> coll
singleton (NamePart -> NameParts) -> NamePart -> NameParts
forall a b. (a -> b) -> a -> b
$ RawName -> NamePart
Id RawName
"_"  -- NoName
stringNameParts RawName
s = [NamePart] -> NameParts
forall a. [a] -> NonEmpty a
List1.fromList ([NamePart] -> NameParts) -> [NamePart] -> NameParts
forall a b. (a -> b) -> a -> b
$ 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 NameParts where
  numHoles :: NameParts -> Int
numHoles = [NamePart] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([NamePart] -> Int)
-> (NameParts -> [NamePart]) -> NameParts -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NamePart -> Bool) -> NameParts -> [NamePart]
forall a. (a -> Bool) -> NonEmpty a -> [a]
List1.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 -> NameParts
nameNameParts = NameParts
parts }) = NameParts -> Int
forall a. NumHoles a => a -> Int
numHoles NameParts
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?
--   Needs at least 2 'NamePart's.
isOperator :: Name -> Bool
isOperator :: Name -> Bool
isOperator = \case
  Name Range
_ NameInScope
_ (NamePart
_ :| NamePart
_ : [NamePart]
_) -> Bool
True
  Name
_ -> Bool
False

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 (NameParts -> NamePart
forall a. NonEmpty a -> a
List1.head NameParts
xs)) Bool -> Bool -> Bool
&&      NamePart -> Bool
isHole (NameParts -> NamePart
forall a. NonEmpty a -> a
List1.last NameParts
xs)  where xs :: NameParts
xs = Name -> NameParts
nameParts Name
x
isPostfix :: Name -> Bool
isPostfix Name
x =      NamePart -> Bool
isHole (NameParts -> NamePart
forall a. NonEmpty a -> a
List1.head NameParts
xs)  Bool -> Bool -> Bool
&& Bool -> Bool
not (NamePart -> Bool
isHole (NameParts -> NamePart
forall a. NonEmpty a -> a
List1.last NameParts
xs)) where xs :: NameParts
xs = Name -> NameParts
nameParts Name
x
isInfix :: Name -> Bool
isInfix   Name
x =      NamePart -> Bool
isHole (NameParts -> NamePart
forall a. NonEmpty a -> a
List1.head NameParts
xs)  Bool -> Bool -> Bool
&&      NamePart -> Bool
isHole (NameParts -> NamePart
forall a. NonEmpty a -> a
List1.last NameParts
xs)  where xs :: NameParts
xs = Name -> NameParts
nameParts Name
x
isNonfix :: Name -> Bool
isNonfix  Name
x = Bool -> Bool
not (NamePart -> Bool
isHole (NameParts -> NamePart
forall a. NonEmpty a -> a
List1.head NameParts
xs)) Bool -> Bool -> Bool
&& Bool -> Bool
not (NamePart -> Bool
isHole (NameParts -> NamePart
forall a. NonEmpty a -> a
List1.last NameParts
xs)) where xs :: NameParts
xs = Name -> NameParts
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
n Name -> f NameInScope -> f Name
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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
------------------------------------------------------------------------

-- | Method by which to generate fresh unshadowed names.
data FreshNameMode
  = UnicodeSubscript
  -- ^ Append an integer Unicode subscript: x, x₁, x₂, …
  | AsciiCounter
  -- ^ Append an integer ASCII counter: x, x1, x2, …

  -- Note that @Agda.Utils.Suffix@ supports an additional style, @Prime@, but
  -- we currently only encounter it when extending an existing name of that
  -- format, (x', x'', …), not for an initially-generated permutation. There's
  -- no reason we couldn't, except that we currently choose between
  -- subscript/counter styles based on the --no-unicode mode rather than any
  -- finer-grained option.
  --   | PrimeTickCount
  --   ^ Append an ASCII prime/apostrophe: x, x', x'', …

nextRawName :: FreshNameMode -> RawName -> RawName
nextRawName :: FreshNameMode -> ShowS
nextRawName FreshNameMode
freshNameMode RawName
s = RawName -> Suffix -> RawName
addSuffix RawName
root (Suffix -> (Suffix -> Suffix) -> Maybe Suffix -> Suffix
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Suffix
initialSuffix Suffix -> Suffix
nextSuffix Maybe Suffix
suffix)
  where
  (RawName
root, Maybe Suffix
suffix) = RawName -> (RawName, Maybe Suffix)
suffixView RawName
s
  initialSuffix :: Suffix
initialSuffix = case FreshNameMode
freshNameMode of
    FreshNameMode
UnicodeSubscript -> Integer -> Suffix
Subscript Integer
1
    FreshNameMode
AsciiCounter -> Integer -> Suffix
Index Integer
1

-- | Get the next version of the concrete name. For instance,
--   @nextName "x" = "x₁"@.  The name must not be a 'NoName'.
nextName :: FreshNameMode -> Name -> Name
nextName :: FreshNameMode -> Name -> Name
nextName FreshNameMode
freshNameMode x :: Name
x@Name{} = Name -> Name
forall a. LensInScope a => a -> a
setNotInScope (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ Lens' RawName Name -> LensMap RawName Name
forall i o. Lens' i o -> LensMap i o
over ((NameParts -> f NameParts) -> Name -> f Name
Lens' NameParts Name
lensNameParts ((NameParts -> f NameParts) -> Name -> f Name)
-> ((RawName -> f RawName) -> NameParts -> f NameParts)
-> (RawName -> f RawName)
-> Name
-> f Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RawName -> f RawName) -> NameParts -> f NameParts
Lens' RawName NameParts
lastIdPart) (FreshNameMode -> ShowS
nextRawName FreshNameMode
freshNameMode) Name
x
nextName             FreshNameMode
_ NoName{} = Name
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Zoom on the last non-hole in a name.
lastIdPart :: Lens' RawName NameParts
lastIdPart :: (RawName -> f RawName) -> NameParts -> f NameParts
lastIdPart RawName -> f RawName
f = NameParts -> f NameParts
loop
  where
  loop :: NameParts -> f NameParts
loop = \case
    Id RawName
s :| []     -> RawName -> f RawName
f RawName
s f RawName -> (RawName -> NameParts) -> f NameParts
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ RawName
s -> RawName -> NamePart
Id RawName
s NamePart -> [NamePart] -> NameParts
forall a. a -> [a] -> NonEmpty a
:| []
    Id RawName
s :| [NamePart
Hole] -> RawName -> f RawName
f RawName
s f RawName -> (RawName -> NameParts) -> f NameParts
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ RawName
s -> RawName -> NamePart
Id RawName
s NamePart -> [NamePart] -> NameParts
forall a. a -> [a] -> NonEmpty a
:| [NamePart
Hole]
    NamePart
p1 :| NamePart
p2 : [NamePart]
ps  -> (NamePart
p1 NamePart -> NameParts -> NameParts
forall a. a -> NonEmpty a -> NonEmpty a
<|) (NameParts -> NameParts) -> f NameParts -> f NameParts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameParts -> f NameParts
loop (NamePart
p2 NamePart -> [NamePart] -> NameParts
forall a. a -> [a] -> NonEmpty a
:| [NamePart]
ps)
    NamePart
Hole :| []     -> f NameParts
forall a. HasCallStack => a
__IMPOSSIBLE__

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

-- | Lens for accessing and modifying the suffix of a name.
--   The suffix of a @NoName@ is always @Nothing@, and should not be
--   changed.
nameSuffix :: Lens' (Maybe Suffix) Name
nameSuffix :: (Maybe Suffix -> f (Maybe Suffix)) -> Name -> f Name
nameSuffix (Maybe Suffix -> f (Maybe Suffix)
f :: Maybe Suffix -> f (Maybe Suffix)) = \case

  n :: Name
n@NoName{} -> Maybe Suffix -> f (Maybe Suffix)
f Maybe Suffix
forall a. Maybe a
Nothing f (Maybe Suffix) -> (Maybe Suffix -> Name) -> f Name
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
    Maybe Suffix
Nothing -> Name
n
    Just {} -> Name
forall a. HasCallStack => a
__IMPOSSIBLE__

  n :: Name
n@Name{} -> (NameParts -> f NameParts) -> Name -> f Name
Lens' NameParts Name
lensNameParts ((RawName -> f RawName) -> NameParts -> f NameParts
Lens' RawName NameParts
lastIdPart RawName -> f RawName
idSuf) Name
n
    where
    idSuf :: RawName -> f RawName
idSuf RawName
s =
      let (RawName
root, Maybe Suffix
suffix) = RawName -> (RawName, Maybe Suffix)
suffixView RawName
s
      in RawName -> (Suffix -> RawName) -> Maybe Suffix -> RawName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe RawName
root (RawName -> Suffix -> RawName
addSuffix RawName
root) (Maybe Suffix -> RawName) -> f (Maybe Suffix) -> f RawName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe Suffix -> f (Maybe Suffix)
f Maybe Suffix
suffix)

-- | Split a name into a base name plus a suffix.
nameSuffixView :: Name -> (Maybe Suffix, Name)
nameSuffixView :: Name -> (Maybe Suffix, Name)
nameSuffixView = (Maybe Suffix -> (Maybe Suffix, Maybe Suffix))
-> Name -> (Maybe Suffix, Name)
Lens' (Maybe Suffix) Name
nameSuffix (,Maybe Suffix
forall a. Maybe a
Nothing)

-- | Replaces the suffix of a name. Unless the suffix is @Nothing@,
--   the name should not be @NoName@.
setNameSuffix :: Maybe Suffix -> Name -> Name
setNameSuffix :: Maybe Suffix -> Name -> Name
setNameSuffix = Lens' (Maybe Suffix) Name -> Maybe Suffix -> Name -> Name
forall i o. Lens' i o -> LensSet i o
set Lens' (Maybe Suffix) Name
nameSuffix

-- | Get a raw version of the name with all suffixes removed. For
--   instance, @nameRoot "x₁₂₃" = "x"@.
nameRoot :: Name -> RawName
nameRoot :: Name -> RawName
nameRoot Name
x = Name -> RawName
nameToRawName (Name -> RawName) -> Name -> RawName
forall a b. (a -> b) -> a -> b
$ (Maybe Suffix, Name) -> Name
forall a b. (a, b) -> b
snd ((Maybe Suffix, Name) -> Name) -> (Maybe Suffix, Name) -> Name
forall a b. (a -> b) -> a -> b
$ Name -> (Maybe Suffix, Name)
nameSuffixView Name
x

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
------------------------------------------------------------------------

-- | Lens for the unqualified part of a QName
lensQNameName :: Lens' Name QName
lensQNameName :: (Name -> f Name) -> QName -> f QName
lensQNameName Name -> f Name
f (QName Name
n)  = Name -> QName
QName (Name -> QName) -> f Name -> f QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> f Name
f Name
n
lensQNameName Name -> f Name
f (Qual Name
m QName
n) = Name -> QName -> QName
Qual Name
m (QName -> QName) -> f QName -> f QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> f Name) -> QName -> f QName
Lens' Name QName
lensQNameName Name -> f Name
f QName
n

-- | @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 -> List1 Name
qnameParts :: QName -> List1 Name
qnameParts (Qual Name
x QName
q) = Name
x Name -> List1 Name -> List1 Name
forall a. a -> NonEmpty a -> NonEmpty a
<| QName -> List1 Name
qnameParts QName
q
qnameParts (QName Name
x)  = Name -> List1 Name
forall el coll. Singleton el coll => el -> coll
singleton 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 -> List1 RawName -> TopLevelModuleName
TopLevelModuleName (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
q) (List1 RawName -> TopLevelModuleName)
-> List1 RawName -> TopLevelModuleName
forall a b. (a -> b) -> a -> b
$
  (Name -> RawName) -> List1 Name -> List1 RawName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> RawName
nameToRawName (List1 Name -> List1 RawName) -> List1 Name -> List1 RawName
forall a b. (a -> b) -> a -> b
$ QName -> List1 Name
qnameParts QName
q

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

moduleNameToFileName :: TopLevelModuleName -> String -> FilePath
moduleNameToFileName :: TopLevelModuleName -> ShowS
moduleNameToFileName (TopLevelModuleName Range
_ List1 RawName
ms) RawName
ext =
  [RawName] -> RawName
joinPath (List1 RawName -> [RawName]
forall a. NonEmpty a -> [a]
List1.init List1 RawName
ms) RawName -> ShowS
</> List1 RawName -> RawName
forall a. NonEmpty a -> a
List1.last List1 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
_ List1 RawName
m) =
  RawName -> AbsolutePath
mkAbsolute (RawName -> AbsolutePath) -> RawName -> AbsolutePath
forall a b. (a -> b) -> a -> b
$
    ShowS -> RawName -> [RawName]
forall a. (a -> a) -> a -> [a]
iterate ShowS
takeDirectory (AbsolutePath -> RawName
filePath AbsolutePath
file) [RawName] -> Int -> RawName
forall a. [a] -> Int -> a
!! List1 RawName -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length List1 RawName
m

------------------------------------------------------------------------
-- * 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 -> ModuleNameHash -> NameId
NameId Word64
0 ModuleNameHash
noModuleNameHash)

-- | 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 = \case
    NoName{}              -> Bool
True
    Name Range
_ NameInScope
_ (NamePart
Hole :| []) -> Bool
True
    Name Range
_ NameInScope
_ (Id RawName
x :| []) -> RawName -> Bool
forall a. IsNoName a => a -> Bool
isNoName RawName
x
    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

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

instance Pretty Name where
  pretty :: Name -> Doc
pretty (Name Range
_ NameInScope
_ NameParts
xs)    = NonEmpty Doc -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat (NonEmpty Doc -> Doc) -> NonEmpty Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (NamePart -> Doc) -> NameParts -> NonEmpty Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamePart -> Doc
forall a. Pretty a => a -> Doc
pretty NameParts
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
_ List1 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] -> RawName) -> [RawName] -> RawName
forall a b. (a -> b) -> a -> b
$ List1 RawName -> [RawName]
forall a. NonEmpty a -> [a]
List1.toList List1 RawName
ms

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

instance HasRange Name where
    getRange :: Name -> Range
getRange (Name Range
r NameInScope
_ NameParts
_ps) = Range
r
    getRange (NoName Range
r NameId
_)   = Range
r

instance HasRange QName where
    getRange :: QName -> Range
getRange (QName  Name
x) = Name -> Range
forall a. HasRange a => a -> 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 NameParts
ps) = Range -> NameInScope -> NameParts -> Name
Name Range
r NameInScope
nis NameParts
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 a. SetRange a => Range -> a -> a
setRange Range
r Name
x)
  setRange Range
r (Qual Name
n QName
x) = Name -> QName -> QName
Qual (Range -> Name -> Name
forall a. SetRange a => Range -> a -> a
setRange Range
r Name
n) (Range -> QName -> QName
forall a. SetRange a => Range -> a -> a
setRange Range
r QName
x)

instance SetRange TopLevelModuleName where
  setRange :: Range -> TopLevelModuleName -> TopLevelModuleName
setRange Range
r (TopLevelModuleName Range
_ List1 RawName
x) = Range -> List1 RawName -> TopLevelModuleName
TopLevelModuleName Range
r List1 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 NameParts
ps)  = Range -> NameInScope -> NameParts -> Name
Name (KillRangeT Range
forall a. KillRange a => KillRangeT a
killRange Range
r) NameInScope
nis NameParts
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
_ List1 RawName
x) = Range -> List1 RawName -> TopLevelModuleName
TopLevelModuleName Range
forall a. Range' a
noRange List1 RawName
x

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

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

-- | Ranges are not forced.

instance NFData Name where
  rnf :: Name -> ()
rnf (Name Range
_ NameInScope
nis NameParts
ns) = NameInScope -> ()
forall a. NFData a => a -> ()
rnf NameInScope
nis () -> () -> ()
`seq` NameParts -> ()
forall a. NFData a => a -> ()
rnf NameParts
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

instance NFData TopLevelModuleName