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.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 (resolveName <=< parseName rg) nms
let userIdentifiers = fmap (fmap anameName . anames) rnms
snms <- fmap (nsNames . allThingsInScope) $ getNamedScope =<< currentModule
let namesInScope = filter ((PatternSynName /=) . anameKind . snd)
$ concatMap (uncurry $ map . (,)) $ Map.toList snms
ress <- forM namesInScope $ \ (x, n) -> do
t <- normalForm norm =<< typeOfConst (anameName 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 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 _ = []