{-# OPTIONS_GHC -Wunused-imports #-}
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 qualified Agda.Utils.List1 as List1
import Agda.Syntax.Common.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
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
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 a. [List1 a] -> [a]
List1.concat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\ (Name
c, NonEmpty AbstractName
as) -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name
c,) NonEmpty AbstractName
as) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList NamesInScope
snms
[[(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 NonEmpty AbstractName
ans) = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty AbstractName
ans
anames (ConstructorName Set Induction
_ NonEmpty AbstractName
ans)= forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty AbstractName
ans
anames ResolvedName
_ = []