    module Agda.Interaction.SearchAbout (findMentions) where

    import Control.Monad

    import qualified Data.Map as Map
    import qualified Data.Set as Set
    import Data.List (isInfixOf)
    import Data.Either (partitionEithers)
    import Data.Foldable (toList)

    import Agda.Syntax.Position (Range)
    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Scope.Monad
    import Agda.TypeChecking.Monad.Signature
    import Agda.TypeChecking.Monad.Env
    import Agda.Syntax.Internal.Names (namesIn)
    import Agda.Interaction.Base (Rewrite)
    import Agda.Interaction.BasicOps (normalForm, parseName)

    import qualified Agda.Syntax.Concrete as C
    import qualified Agda.Syntax.Internal as I

    import Agda.Utils.List   ( initLast1  )
    import Agda.Utils.Pretty ( prettyShow )

    findMentions :: Rewrite -> Range -> String -> ScopeM [(C.Name, I.Type)]
    findMentions :: Rewrite -> Range -> String -> ScopeM [(Name, Type)]
    findMentions Rewrite
    norm Range
    rg String
    nm = do
      -- We start by dealing with the user's input

      -- The users passes in `nm`, a list of identifiers and strings
      -- to match against definitions in scope. `findMentions` will
      -- select all of the definitions such that:
      -- - all of the specified identifiers appear in their type
      --   (which has been normalised according to `norm`)
      -- - all of the specified strings are substrings of their name

      -- We separate the strings from the names by a rough analysis
      -- and then parse and resolve the names in the current scope
      let ([String]
    userSubStrings, [String]
    nms) = [Either String String] -> ([String], [String])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers ([Either String String] -> ([String], [String]))
    -> [Either String String] -> ([String], [String])
    forall a b. (a -> b) -> a -> b
    $ String -> Either String String
    isString (String -> Either String String)
    -> [String] -> [Either String String]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> [String]
    words String
    nm
      [ResolvedName]
    rnms <- (String -> TCMT IO ResolvedName)
    -> [String] -> TCMT IO [ResolvedName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (QName -> TCMT IO ResolvedName
    resolveName (QName -> TCMT IO ResolvedName)
    -> (String -> TCMT IO QName) -> String -> TCMT IO ResolvedName
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Range -> String -> TCMT IO QName
    parseName Range
    rg) [String]
    nms
      let userIdentifiers :: [[QName]]
    userIdentifiers = (ResolvedName -> [QName]) -> [ResolvedName] -> [[QName]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((AbstractName -> QName) -> [AbstractName] -> [QName]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap AbstractName -> QName
    anameName ([AbstractName] -> [QName])
    -> (ResolvedName -> [AbstractName]) -> ResolvedName -> [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ResolvedName -> [AbstractName]
    anames) [ResolvedName]
    rnms

      -- We then collect all the things in scope, by name.
      -- Issue #2381: We explicitly filter out pattern synonyms because they
      -- don't have a type. Looking it up makes Agda panic!
      NamesInScope
    snms <- (Scope -> NamesInScope) -> TCMT IO Scope -> TCMT IO NamesInScope
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (NameSpace -> NamesInScope
    nsNames (NameSpace -> NamesInScope)
    -> (Scope -> NameSpace) -> Scope -> NamesInScope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Scope -> NameSpace
    allThingsInScope) (TCMT IO Scope -> TCMT IO NamesInScope)
    -> TCMT IO Scope -> TCMT IO NamesInScope
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> TCMT IO Scope
    getNamedScope (ModuleName -> TCMT IO Scope)
    -> TCMT IO ModuleName -> TCMT IO Scope
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO ModuleName
    forall (m :: * -> *). MonadTCEnv m => m ModuleName
    currentModule
      let namesInScope :: [(Name, AbstractName)]
    namesInScope = ((Name, AbstractName) -> Bool)
    -> [(Name, AbstractName)] -> [(Name, AbstractName)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((KindOfName
    PatternSynName KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    /=) (KindOfName -> Bool)
    -> ((Name, AbstractName) -> KindOfName)
    -> (Name, AbstractName)
    -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbstractName -> KindOfName
    anameKind (AbstractName -> KindOfName)
    -> ((Name, AbstractName) -> AbstractName)
    -> (Name, AbstractName)
    -> KindOfName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, AbstractName) -> AbstractName
    forall a b. (a, b) -> b
    snd)
                       ([(Name, AbstractName)] -> [(Name, AbstractName)])
    -> [(Name, AbstractName)] -> [(Name, AbstractName)]
    forall a b. (a -> b) -> a -> b
    $ ((Name, [AbstractName]) -> [(Name, AbstractName)])
    -> [(Name, [AbstractName])] -> [(Name, AbstractName)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ((Name -> [AbstractName] -> [(Name, AbstractName)])
    -> (Name, [AbstractName]) -> [(Name, AbstractName)]
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ((Name -> [AbstractName] -> [(Name, AbstractName)])
     -> (Name, [AbstractName]) -> [(Name, AbstractName)])
    -> (Name -> [AbstractName] -> [(Name, AbstractName)])
    -> (Name, [AbstractName])
    -> [(Name, AbstractName)]
    forall a b. (a -> b) -> a -> b
    $ (AbstractName -> (Name, AbstractName))
    -> [AbstractName] -> [(Name, AbstractName)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((AbstractName -> (Name, AbstractName))
     -> [AbstractName] -> [(Name, AbstractName)])
    -> (Name -> AbstractName -> (Name, AbstractName))
    -> Name
    -> [AbstractName]
    -> [(Name, AbstractName)]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (,)) ([(Name, [AbstractName])] -> [(Name, AbstractName)])
    -> [(Name, [AbstractName])] -> [(Name, AbstractName)]
    forall a b. (a -> b) -> a -> b
    $ NamesInScope -> [(Name, [AbstractName])]
    forall k a. Map k a -> [(k, a)]
    Map.toList NamesInScope
    snms

      -- Once we have the user-provided names and the names of all the
      -- thing in scope we can start the search: for each name in scope,
      -- we grab its type, normalise it according to `norm` and collect
      -- the identifiers in it. We then check whether it meets the user's
      -- criteria.
      [[(Name, Type)]]
    ress <- [(Name, AbstractName)]
    -> ((Name, AbstractName) -> ScopeM [(Name, Type)])
    -> TCMT IO [[(Name, Type)]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [(Name, AbstractName)]
    namesInScope (((Name, AbstractName) -> ScopeM [(Name, Type)])
     -> TCMT IO [[(Name, Type)]])
    -> ((Name, AbstractName) -> ScopeM [(Name, Type)])
    -> TCMT IO [[(Name, Type)]]
    forall a b. (a -> b) -> a -> b
    $ \ (Name
    x, AbstractName
    n) -> do
        Type
    t <- Rewrite -> Type -> TCM Type
    forall t.
    (Reduce t, Simplify t, Instantiate t, Normalise t) =>
    Rewrite -> t -> TCM t
    normalForm Rewrite
    norm (Type -> TCM Type) -> TCM Type -> TCM Type
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> TCM Type
    forall (m :: * -> *).
    (HasConstInfo m, ReadTCState m) =>
    QName -> m Type
    typeOfConst (AbstractName -> QName
    anameName AbstractName
    n)
        [(Name, Type)] -> ScopeM [(Name, Type)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Name, Type)] -> ScopeM [(Name, Type)])
    -> [(Name, Type)] -> ScopeM [(Name, Type)]
    forall a b. (a -> b) -> a -> b
    $ do
          Bool -> [()]
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> [()]) -> Bool -> [()]
    forall a b. (a -> b) -> a -> b
    $ (String -> Bool) -> [String] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isInfixOf` Name -> String
    forall a. Pretty a => a -> String
    prettyShow Name
    x) [String]
    userSubStrings
          Bool -> [()]
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> [()]) -> Bool -> [()]
    forall a b. (a -> b) -> a -> b
    $ ([QName] -> Bool) -> [[QName]] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all ((QName -> Bool) -> [QName] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (QName -> Set QName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Type -> Set QName
    forall a m. (NamesIn a, Collection QName m) => a -> m
    namesIn Type
    t)) [[QName]]
    userIdentifiers
          (Name, Type) -> [(Name, Type)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name
    x, Type
    t)
      [(Name, Type)] -> ScopeM [(Name, Type)]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([(Name, Type)] -> ScopeM [(Name, Type)])
    -> [(Name, Type)] -> ScopeM [(Name, Type)]
    forall a b. (a -> b) -> a -> b
    $ [[(Name, Type)]] -> [(Name, Type)]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[(Name, Type)]]
    ress

      where
        isString :: String -> Either String String
        isString :: String -> Either String String
    isString (Char
    '"' : Char
    c : String
    cs)
          | (String
    str, Char
    '"') <- Char -> String -> (String, Char)
    forall a. a -> [a] -> ([a], a)
    initLast1 Char
    c String
    cs
          = String -> Either String String
    forall a b. a -> Either a b
    Left (String -> Either String String) -> String -> Either String String
    forall a b. (a -> b) -> a -> b
    $ (Char -> Bool) -> String -> String
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Char
    '"') String
    str
        isString String
    str
          = String -> Either String String
    forall a b. b -> Either a b
    Right String
    str

        anames :: ResolvedName -> [AbstractName]
    anames (DefinedName Access
    _ AbstractName
    an Suffix
    _)   = [AbstractName
    an]
        anames (FieldName     List1 AbstractName
    ans)    = List1 AbstractName -> [AbstractName]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList List1 AbstractName
    ans
        anames (ConstructorName Set Induction
    _ List1 AbstractName
    ans)= List1 AbstractName -> [AbstractName]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList List1 AbstractName
    ans
        anames ResolvedName
    _                      = []