content: {-# OPTIONS_GHC -Wunused-imports #-}
  {-# OPTIONS_GHC -Wunused-matches #-}
  {-# OPTIONS_GHC -Wunused-binds   #-}
  
  {-| 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 (on)
  import qualified Data.Foldable as Fold
  
  import GHC.Generics (Generic)
  
  import Agda.Syntax.Common
  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.Syntax.Common.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.
      { nameRange     :: Range
      , nameInScope   :: NameInScope
      , nameNameParts :: NameParts
      }
    | NoName -- ^ @_@.
      { nameRange     :: Range
      , 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 = \case
    Name _ _ (x :| x' : xs) -> x == Hole || last1 x' xs == Hole
    _ -> False
  
  instance Underscore Name where
    underscore = NoName noRange __IMPOSSIBLE__
    isUnderscore NoName{} = True
    isUnderscore (Name {nameNameParts = Id x :| []}) = isUnderscore x
    isUnderscore _ = 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 Generic
  
  -- | Define equality on @Name@ to ignore range so same names in different
  --   locations are equal.
  --
  --   Is there a reason not to do this? -Jeff
  --
  --   No. But there are tons of reasons to do it. For instance, when using
  --   names as keys in maps you really don't want to have to get the range
  --   right to be able to do a lookup. -Ulf
  
  instance Eq Name where
      Name _ _ xs    == Name _ _ ys    = xs == ys
      NoName _ i     == NoName _ j     = i == j
      _              == _              = False
  
  instance Ord Name where
      compare (Name _ _ xs)  (Name _ _ ys)      = compare xs ys
      compare (NoName _ i)   (NoName _ j)       = compare i j
      compare (NoName {})    (Name {})          = LT
      compare (Name {})      (NoName {})        = GT
  
  instance Eq NamePart where
    Hole  == Hole  = True
    Id s1 == Id s2 = s1 == s2
    _     == _     = False
  
  instance Ord NamePart where
    compare Hole    Hole    = EQ
    compare Hole    (Id {}) = LT
    compare (Id {}) Hole    = GT
    compare (Id s1) (Id s2) = compare s1 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 (Eq, Ord)
  
  instance Underscore QName where
    underscore = QName underscore
    isUnderscore (QName x) = isUnderscore x
    isUnderscore Qual{}    = False
  
  ------------------------------------------------------------------------
  -- * Constructing simple 'Name's.
  ------------------------------------------------------------------------
  
  -- | Create an ordinary 'InScope' name.
  simpleName :: RawName -> Name
  simpleName = Name noRange InScope . singleton . Id
  
  -- | Create a binary operator name in scope.
  simpleBinaryOperator :: RawName -> Name
  simpleBinaryOperator s = Name noRange InScope $ Hole :| Id s : Hole : []
  
  -- | Create an ordinary 'InScope' name containing a single 'Hole'.
  simpleHole :: Name
  simpleHole = Name noRange InScope $ singleton Hole
  
  ------------------------------------------------------------------------
  -- * Operations on 'Name' and 'NamePart'
  ------------------------------------------------------------------------
  
  -- | Don't use on 'NoName{}'.
  lensNameParts :: Lens' Name NameParts
  lensNameParts f = \case
    n@Name{} -> f (nameNameParts n) <&> \ ps -> n { nameNameParts = ps }
    NoName{} -> __IMPOSSIBLE__
  
  nameToRawName :: Name -> RawName
  nameToRawName = prettyShow
  
  nameParts :: Name -> NameParts
  nameParts (Name _ _ ps)    = ps
  nameParts (NoName _ _)     = singleton $ Id "_" -- To not return an empty list
  
  nameStringParts :: Name -> [RawName]
  nameStringParts n = [ s | Id s <- List1.toList $ nameParts n ]
  
  -- | Parse a string to parts of a concrete name.
  --
  --   Note: @stringNameParts "_" == [Id "_"] == nameParts NoName{}@
  
  stringNameParts :: String -> NameParts
  stringNameParts ""  = singleton $ Id "_"  -- NoName
  stringNameParts "_" = singleton $ Id "_"  -- NoName
  stringNameParts s = List1.fromListSafe __IMPOSSIBLE__ $ loop s
    where
    loop ""                              = []
    loop ('_':s)                         = Hole : loop s
    loop s | (x, s') <- break (== '_') s = Id (stringToRawName x) : loop 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 = length . List1.filter (== Hole)
  
  instance NumHoles Name where
    numHoles NoName{}         = 0
    numHoles (Name { nameNameParts = parts }) = numHoles parts
  
  instance NumHoles QName where
    numHoles (QName x)  = numHoles x
    numHoles (Qual _ x) = numHoles x
  
  -- | Is the name an operator?
  --   Needs at least 2 'NamePart's.
  isOperator :: Name -> Bool
  isOperator = \case
    Name _ _ (_ :| _ : _) -> True
    _ -> False
  
  isHole :: NamePart -> Bool
  isHole Hole = True
  isHole _    = False
  
  isPrefix, isPostfix, isInfix, isNonfix :: Name -> Bool
  isPrefix  x = not (isHole (List1.head xs)) &&      isHole (List1.last xs)  where xs = nameParts x
  isPostfix x =      isHole (List1.head xs)  && not (isHole (List1.last xs)) where xs = nameParts x
  isInfix   x =      isHole (List1.head xs)  &&      isHole (List1.last xs)  where xs = nameParts x
  isNonfix  x = not (isHole (List1.head xs)) && not (isHole (List1.last xs)) where xs = nameParts x
  
  
  ------------------------------------------------------------------------
  -- * Keeping track of which names are (not) in scope
  ------------------------------------------------------------------------
  
  data NameInScope = InScope | NotInScope
    deriving (Eq, Show)
  
  class LensInScope a where
    lensInScope :: Lens' a NameInScope
  
    isInScope :: a -> NameInScope
    isInScope x = x ^. lensInScope
  
    mapInScope :: (NameInScope -> NameInScope) -> a -> a
    mapInScope = over lensInScope
  
    setInScope :: a -> a
    setInScope = mapInScope $ const InScope
  
    setNotInScope :: a -> a
    setNotInScope = mapInScope $ const NotInScope
  
  instance LensInScope NameInScope where
    lensInScope = id
  
  instance LensInScope Name where
    lensInScope f = \case
      n@Name{ nameInScope = nis } -> (\nis' -> n { nameInScope = nis' }) <$> f nis
      n@NoName{} -> n <$ f InScope
  
  instance LensInScope QName where
    lensInScope f = \case
      Qual x xs -> (`Qual` xs) <$> lensInScope f x
      QName x   -> QName <$> lensInScope f 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 s = addSuffix root (maybe initialSuffix nextSuffix suffix)
    where
    (root, suffix) = suffixView s
    initialSuffix = case freshNameMode of
      UnicodeSubscript -> Subscript 1
      AsciiCounter -> Index 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 x@Name{} = setNotInScope $ over (lensNameParts . lastIdPart) (nextRawName freshNameMode) x
  nextName             _ NoName{} = __IMPOSSIBLE__
  
  -- | Zoom on the last non-hole in a name.
  lastIdPart :: Lens' NameParts RawName
  lastIdPart f = loop
    where
    loop = \case
      Id s :| []     -> f s <&> \ s -> Id s :| []
      Id s :| [Hole] -> f s <&> \ s -> Id s :| [Hole]
      p1 :| p2 : ps  -> (p1 <|) <$> loop (p2 :| ps)
      Hole :| []     -> __IMPOSSIBLE__
  
  -- | Get the first version of the concrete name that does not satisfy
  --   the given predicate.
  firstNonTakenName :: FreshNameMode -> (Name -> Bool) -> Name -> Name
  firstNonTakenName freshNameMode taken x =
    if taken x
    then firstNonTakenName freshNameMode taken (nextName freshNameMode x)
    else 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' Name (Maybe Suffix)
  nameSuffix (f :: Maybe Suffix -> f (Maybe Suffix)) = \case
  
    n@NoName{} -> f Nothing <&> \case
      Nothing -> n
      Just {} -> __IMPOSSIBLE__
  
    n@Name{} -> lensNameParts (lastIdPart idSuf) n
      where
      idSuf s =
        let (root, suffix) = suffixView s
        in maybe root (addSuffix root) <$> (f suffix)
  
  -- | Split a name into a base name plus a suffix.
  nameSuffixView :: Name -> (Maybe Suffix, Name)
  nameSuffixView = nameSuffix (,Nothing)
  
  -- | Replaces the suffix of a name. Unless the suffix is @Nothing@,
  --   the name should not be @NoName@.
  setNameSuffix :: Maybe Suffix -> Name -> Name
  setNameSuffix = set nameSuffix
  
  -- | Get a raw version of the name with all suffixes removed. For
  --   instance, @nameRoot "x₁₂₃" = "x"@.
  nameRoot :: Name -> RawName
  nameRoot x = nameToRawName $ snd $ nameSuffixView x
  
  sameRoot :: Name -> Name -> Bool
  sameRoot = (==) `on` nameRoot
  
  ------------------------------------------------------------------------
  -- * Operations on qualified names
  ------------------------------------------------------------------------
  
  -- | Lens for the unqualified part of a QName
  lensQNameName :: Lens' QName Name
  lensQNameName f (QName n)  = QName <$> f n
  lensQNameName f (Qual m n) = Qual m <$> lensQNameName f n
  
  -- | @qualify A.B x == A.B.x@
  qualify :: QName -> Name -> QName
  qualify (QName m) x     = Qual m (QName x)
  qualify (Qual m m') x   = Qual m $ qualify m' x
  
  -- | @unqualify A.B.x == x@
  --
  -- The range is preserved.
  unqualify :: QName -> Name
  unqualify q = unqualify' q `withRangeOf` q
    where
    unqualify' (QName x)  = x
    unqualify' (Qual _ x) = unqualify' x
  
  -- | @qnameParts A.B.x = [A, B, x]@
  qnameParts :: QName -> List1 Name
  qnameParts (Qual x q) = x <| qnameParts q
  qnameParts (QName x)  = singleton x
  
  -- | Is the name (un)qualified?
  
  isQualified :: QName -> Bool
  isQualified Qual{}  = True
  isQualified QName{} = False
  
  isUnqualified :: QName -> Maybe Name
  isUnqualified Qual{}    = Nothing
  isUnqualified (QName n) = Just n
  
  ------------------------------------------------------------------------
  -- * No name stuff
  ------------------------------------------------------------------------
  
  -- | @noName_ = 'noName' 'noRange'@
  noName_ :: Name
  noName_ = noName noRange
  
  noName :: Range -> Name
  noName r = NoName r (NameId 0 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 = Fold.all isNoName
  
  instance IsNoName String where
    isNoName = isUnderscore
  
  instance IsNoName ByteString where
    isNoName = isUnderscore
  
  instance IsNoName Name where
    isNoName = \case
      NoName{}              -> True
      Name _ _ (Hole :| []) -> True
      Name _ _ (Id x :| []) -> isNoName x
      _ -> False
  
  instance IsNoName QName where
    isNoName (QName x) = isNoName x
    isNoName Qual{}    = 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 _ _ xs)    = hcat $ fmap pretty xs
    pretty (NoName _ _)     = "_"
  
  instance Pretty NamePart where
    pretty Hole   = "_"
    pretty (Id s) = text $ rawNameToString s
  
  instance Pretty QName where
    pretty (Qual m x)
      | isUnderscore m = pretty x -- don't print anonymous modules
      | otherwise      = pretty m <> "." <> pretty x
    pretty (QName x)  = pretty x
  
  ------------------------------------------------------------------------
  -- * Range instances
  ------------------------------------------------------------------------
  
  instance HasRange Name where
      getRange (Name r _ _ps) = r
      getRange (NoName r _)   = r
  
  instance HasRange QName where
      getRange (QName  x) = getRange x
      getRange (Qual n x) = fuseRange n x
  
  instance SetRange Name where
    setRange r (Name _ nis ps) = Name r nis ps
    setRange r (NoName _ i)  = NoName r i
  
  instance SetRange QName where
    setRange r (QName x)  = QName (setRange r x)
    setRange r (Qual n x) = Qual (setRange r n) (setRange r x)
  
  instance KillRange QName where
    killRange (QName x) = QName $ killRange x
    killRange (Qual n x) = killRange n `Qual` killRange x
  
  instance KillRange Name where
    killRange (Name r nis ps)  = Name (killRange r) nis ps
    killRange (NoName r i)     = NoName (killRange r) i
  
  ------------------------------------------------------------------------
  -- * NFData instances
  ------------------------------------------------------------------------
  
  instance NFData NameInScope where
    rnf InScope    = ()
    rnf NotInScope = ()
  
  -- | Ranges are not forced.
  
  instance NFData Name where
    rnf (Name _ nis ns) = rnf nis `seq` rnf ns
    rnf (NoName _ n)  = rnf n
  
  instance NFData NamePart where
    rnf Hole   = ()
    rnf (Id s) = rnf s
  
  instance NFData QName where
    rnf (Qual a b) = rnf a `seq` rnf b
    rnf (QName a)  = rnf a
  