{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Interaction.SearchAbout (findMentions) where

import Control.Monad

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

import Agda.Interaction.Base (Rewrite)
import Agda.Interaction.BasicOps (normalForm, parseName)
import Agda.Syntax.Abstract.Name (AbstractName(..), KindOfName (PatternSynName))
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Syntax.Concrete qualified as C
import Agda.Syntax.Internal qualified as I
import Agda.Syntax.Internal.Names (namesIn)
import Agda.Syntax.Position (Range)
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Monad.Signature

import Agda.Utils.List (initLast1)
import Agda.Utils.List1 qualified as List1

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
  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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 = (ResolvedName -> [QName]) -> [ResolvedName] -> [[QName]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((AbstractName -> QName) -> [AbstractName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
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!
  snms <- fmap (nsNames . allThingsInScope) $ getNamedScope =<< currentModule
  let 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
$ [List1 (Name, AbstractName)] -> [(Name, AbstractName)]
forall a. [List1 a] -> [a]
List1.concat ([List1 (Name, AbstractName)] -> [(Name, AbstractName)])
-> [List1 (Name, AbstractName)] -> [(Name, AbstractName)]
forall a b. (a -> b) -> a -> b
$ ((Name, NonEmpty AbstractName) -> List1 (Name, AbstractName))
-> [(Name, NonEmpty AbstractName)] -> [List1 (Name, AbstractName)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
c, NonEmpty AbstractName
as) -> (AbstractName -> (Name, AbstractName))
-> NonEmpty AbstractName -> List1 (Name, AbstractName)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name
c,) NonEmpty AbstractName
as) ([(Name, NonEmpty AbstractName)] -> [List1 (Name, AbstractName)])
-> [(Name, NonEmpty AbstractName)] -> [List1 (Name, AbstractName)]
forall a b. (a -> b) -> a -> b
$ NamesInScope -> [(Name, NonEmpty 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.
  ress <- forM namesInScope $ \ (Name
x, AbstractName
n) -> do
    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)
    return $ do
      guard $ all (`isInfixOf` prettyShow x) userSubStrings
      guard $ all (any (`Set.member` namesIn t)) userIdentifiers
      return (x, t)
  return $ concat 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     NonEmpty AbstractName
ans)    = NonEmpty AbstractName -> [AbstractName]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty AbstractName
ans
    anames (ConstructorName Set1 Induction
_ NonEmpty AbstractName
ans)= NonEmpty AbstractName -> [AbstractName]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty AbstractName
ans
    anames ResolvedName
_                      = []