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.BasicOps (normalForm, Rewrite, parseName)
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Internal as I
import Agda.Utils.Pretty ( prettyShow )
findMentions :: Rewrite -> Range -> String -> ScopeM [(C.Name, I.Type)]
findMentions norm rg nm = do
let (userSubStrings, nms) = partitionEithers $ isString <$> words nm
rnms <- mapM (parseName rg >=> resolveName) nms
let userIdentifiers = fmap (fmap anameName . anames) rnms
snms <- fmap (nsNames . allThingsInScope) $ currentModule >>= getNamedScope
let namesInScope = filter ((PatternSynName /=) . anameKind . snd)
$ concatMap (uncurry $ map . (,)) $ Map.toList snms
ress <- forM namesInScope $ \ (x, n) -> do
t <- normalForm norm =<< typeOfConst (anameName n)
let namesInT = Set.toList $ namesIn t
let defName = prettyShow x
return $ do
guard $ all (`isInfixOf` defName) userSubStrings
guard $ all (any (`elem` namesInT)) userIdentifiers
return (x, t)
return $ concat ress
where
isString str
| not (null str)
&& head str == '"'
&& last str == '"' = Left $ filter (/= '"') str
| otherwise = Right str
anames (DefinedName _ an) = [an]
anames (FieldName ans) = toList ans
anames (ConstructorName ans) = toList ans
anames _ = []