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) = forall a b. [Either a b] -> ([a], [b])
partitionEithers forall a b. (a -> b) -> a -> b
$ String -> Either String String
isString forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> [String]
words String
nm
  [ResolvedName]
rnms <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (QName -> TCMT IO ResolvedName
resolveName forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Range -> String -> TCM QName
parseName Range
rg) [String]
nms
  let userIdentifiers :: [[QName]]
userIdentifiers = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AbstractName -> QName
anameName 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 <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (NameSpace -> NamesInScope
nsNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope -> NameSpace
allThingsInScope) forall a b. (a -> b) -> a -> b
$ ModuleName -> TCMT IO Scope
getNamedScope forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
  let namesInScope :: [(Name, AbstractName)]
namesInScope = forall a. (a -> Bool) -> [a] -> [a]
filter ((KindOfName
PatternSynName forall a. Eq a => a -> a -> Bool
/=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> KindOfName
anameKind forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)
                   forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,)) forall a b. (a -> b) -> a -> b
$ 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, AbstractName)]
namesInScope forall a b. (a -> b) -> a -> b
$ \ (Name
x, AbstractName
n) -> do
    Type
t <- forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
normalForm Rewrite
norm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(HasConstInfo m, ReadTCState m) =>
QName -> m Type
typeOfConst (AbstractName -> QName
anameName AbstractName
n)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` forall a. Pretty a => a -> String
prettyShow Name
x) [String]
userSubStrings
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Ord a => a -> Set a -> Bool
`Set.member` forall a m. (NamesIn a, Collection QName m) => a -> m
namesIn Type
t)) [[QName]]
userIdentifiers
      forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x, Type
t)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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
'"') <- forall a. a -> [a] -> ([a], a)
initLast1 Char
c String
cs
      = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Char
'"') String
str
    isString String
str
      = 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)    = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList List1 AbstractName
ans
    anames (ConstructorName Set Induction
_ List1 AbstractName
ans)= forall (t :: * -> *) a. Foldable t => t a -> [a]
toList List1 AbstractName
ans
    anames ResolvedName
_                      = []