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

import Prelude hiding ((!!))

import Control.DeepSeq

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

import GHC.Generics (Generic)

import Agda.Syntax.Common
import Agda.Syntax.Concrete.Glyph
import Agda.Syntax.Position

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

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 String
x :| []}) = String -> Bool
forall a. Underscore a => a -> Bool
isUnderscore String
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 (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
$cfrom :: forall x. NamePart -> Rep NamePart x
from :: forall x. NamePart -> Rep NamePart x
$cto :: forall x. Rep NamePart x -> NamePart
to :: forall x. Rep NamePart x -> NamePart
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 String
s1 == Id String
s2 = String
s1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
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 String
s1) (Id String
s2) = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare String
s1 String
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 (QName -> QName -> Bool
(QName -> QName -> Bool) -> (QName -> QName -> Bool) -> Eq QName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QName -> QName -> Bool
== :: QName -> QName -> Bool
$c/= :: QName -> QName -> Bool
/= :: 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
$ccompare :: QName -> QName -> Ordering
compare :: QName -> QName -> Ordering
$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
>= :: QName -> QName -> Bool
$cmax :: QName -> QName -> QName
max :: QName -> QName -> QName
$cmin :: QName -> QName -> QName
min :: QName -> QName -> 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

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

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

-- | Create a binary operator name in scope.
simpleBinaryOperator :: RawName -> Name
simpleBinaryOperator :: String -> Name
simpleBinaryOperator String
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
:| String -> NamePart
Id String
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 :: Lens' NameParts 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 -> String
nameToRawName = Name -> String
forall a. Pretty a => a -> String
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
$ String -> NamePart
Id String
"_" -- To not return an empty list

nameStringParts :: Name -> [RawName]
nameStringParts :: Name -> [String]
nameStringParts Name
n = [ String
s | Id String
s <- NameParts -> [Item NameParts]
forall l. IsList l => l -> [Item l]
List1.toList (NameParts -> [Item NameParts]) -> NameParts -> [Item NameParts]
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 :: String -> NameParts
stringNameParts String
""  = NamePart -> NameParts
forall el coll. Singleton el coll => el -> coll
singleton (NamePart -> NameParts) -> NamePart -> NameParts
forall a b. (a -> b) -> a -> b
$ String -> NamePart
Id String
"_"  -- NoName
stringNameParts String
"_" = NamePart -> NameParts
forall el coll. Singleton el coll => el -> coll
singleton (NamePart -> NameParts) -> NamePart -> NameParts
forall a b. (a -> b) -> a -> b
$ String -> NamePart
Id String
"_"  -- NoName
stringNameParts String
s = NameParts -> [NamePart] -> NameParts
forall a. List1 a -> [a] -> List1 a
List1.fromListSafe NameParts
forall a. HasCallStack => a
__IMPOSSIBLE__ ([NamePart] -> NameParts) -> [NamePart] -> NameParts
forall a b. (a -> b) -> a -> b
$ String -> [NamePart]
loop String
s
  where
  loop :: String -> [NamePart]
loop String
""                              = []
  loop (Char
'_':String
s)                         = NamePart
Hole NamePart -> [NamePart] -> [NamePart]
forall a. a -> [a] -> [a]
: String -> [NamePart]
loop String
s
  loop String
s | (String
x, String
s') <- (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_') String
s = String -> NamePart
Id (String -> String
stringToRawName String
x) NamePart -> [NamePart] -> [NamePart]
forall a. a -> [a] -> [a]
: String -> [NamePart]
loop String
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 a. [a] -> 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
$c== :: NameInScope -> NameInScope -> Bool
== :: NameInScope -> NameInScope -> Bool
$c/= :: NameInScope -> NameInScope -> Bool
/= :: NameInScope -> NameInScope -> Bool
Eq, Int -> NameInScope -> String -> String
[NameInScope] -> String -> String
NameInScope -> String
(Int -> NameInScope -> String -> String)
-> (NameInScope -> String)
-> ([NameInScope] -> String -> String)
-> Show NameInScope
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> NameInScope -> String -> String
showsPrec :: Int -> NameInScope -> String -> String
$cshow :: NameInScope -> String
show :: NameInScope -> String
$cshowList :: [NameInScope] -> String -> String
showList :: [NameInScope] -> String -> String
Show)

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
^. (NameInScope -> f NameInScope) -> a -> f a
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 (NameInScope -> f NameInScope) -> a -> f a
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 :: Lens' NameInScope NameInScope
lensInScope = (NameInScope -> f NameInScope) -> NameInScope -> f NameInScope
forall a. a -> a
id

instance LensInScope Name where
  lensInScope :: Lens' NameInScope 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 a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NameInScope -> f NameInScope
f NameInScope
InScope

instance LensInScope QName where
  lensInScope :: Lens' NameInScope 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
Lens' NameInScope Name
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
Lens' NameInScope Name
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 -> String -> String
nextRawName FreshNameMode
freshNameMode String
s = String -> Suffix -> String
addSuffix String
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
  (String
root, Maybe Suffix
suffix) = String -> (String, Maybe Suffix)
suffixView String
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' String Name -> LensMap String 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)
-> ((String -> f String) -> NameParts -> f NameParts)
-> (String -> f String)
-> Name
-> f Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> f String) -> NameParts -> f NameParts
Lens' String NameParts
lastIdPart) (FreshNameMode -> String -> String
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 :: Lens' String NameParts
lastIdPart String -> f String
f = NameParts -> f NameParts
loop
  where
  loop :: NameParts -> f NameParts
loop = \case
    Id String
s :| []     -> String -> f String
f String
s f String -> (String -> NameParts) -> f NameParts
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ String
s -> String -> NamePart
Id String
s NamePart -> [NamePart] -> NameParts
forall a. a -> [a] -> NonEmpty a
:| []
    Id String
s :| [NamePart
Hole] -> String -> f String
f String
s f String -> (String -> NameParts) -> f NameParts
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ String
s -> String -> NamePart
Id String
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 :: Lens' (Maybe Suffix) 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 ((String -> f String) -> NameParts -> f NameParts
Lens' String NameParts
lastIdPart String -> f String
idSuf) Name
n
    where
    idSuf :: String -> f String
idSuf String
s =
      let (String
root, Maybe Suffix
suffix) = String -> (String, Maybe Suffix)
suffixView String
s
      in String -> (Suffix -> String) -> Maybe Suffix -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
root (String -> Suffix -> String
addSuffix String
root) (Maybe Suffix -> String) -> f (Maybe Suffix) -> f String
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 (Maybe Suffix -> f (Maybe Suffix)) -> Name -> f Name
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 -> String
nameRoot Name
x = Name -> String
nameToRawName (Name -> String) -> Name -> String
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 = String -> String -> Bool
forall a. Eq a => a -> a -> Bool
(==) (String -> String -> Bool)
-> (Name -> String) -> Name -> Name -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Name -> String
nameRoot

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

-- | Lens for the unqualified part of a QName
lensQNameName :: Lens' Name QName
lensQNameName :: Lens' Name 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

------------------------------------------------------------------------
-- * 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 :: String -> Bool
isNoName = String -> 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 String
x :| []) -> String -> Bool
forall a. IsNoName a => a -> Bool
isNoName String
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

------------------------------------------------------------------------
-- * 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 a b. (a -> b) -> NonEmpty a -> NonEmpty b
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 String
s) = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> String
rawNameToString String
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

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

------------------------------------------------------------------------
-- * 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 () -> () -> ()
forall a b. a -> b -> b
`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 String
s) = String -> ()
forall a. NFData a => a -> ()
rnf String
s

instance NFData QName where
  rnf :: QName -> ()
rnf (Qual Name
a 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 Name
a)  = Name -> ()
forall a. NFData a => a -> ()
rnf Name
a