{-# LANGUAGE FlexibleInstances #-}
module Idris.Apropos (apropos, aproposModules) where
import Idris.AbsSyntax
import Idris.Core.Evaluate (Def(..), ctxtAlist)
import Idris.Core.TT (Binder(..), Const(..), Name(..), NameType(..), TT(..),
toAlist)
import Idris.Docstrings (DocTerm, Docstring, containsText)
import Data.List (intersperse, nub, nubBy)
import qualified Data.Text as T
apropos :: IState -> T.Text -> [Name]
apropos :: IState -> Text -> [Name]
apropos ist :: IState
ist what :: Text
what = let defs :: [(Name, Def)]
defs = Context -> [(Name, Def)]
ctxtAlist (IState -> Context
tt_ctxt IState
ist)
docs :: [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
docs = Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
forall a. Ctxt a -> [(Name, a)]
toAlist (IState -> Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
idris_docstrings IState
ist)
in [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub (((Name, Def) -> Name) -> [(Name, Def)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Def) -> Name
forall a b. (a, b) -> a
fst ([Text] -> [(Name, Def)] -> [(Name, Def)]
forall a. Apropos a => [Text] -> [a] -> [a]
isAproposAll [Text]
parts [(Name, Def)]
defs) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
((Name, (Docstring DocTerm, [(Name, Docstring DocTerm)])) -> Name)
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Docstring DocTerm, [(Name, Docstring DocTerm)])) -> Name
forall a b. (a, b) -> a
fst ([Text]
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
-> [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
forall a. Apropos a => [Text] -> [a] -> [a]
isAproposAll [Text]
parts [(Name, (Docstring DocTerm, [(Name, Docstring DocTerm)]))]
docs))
where isAproposAll :: [Text] -> [a] -> [a]
isAproposAll [] xs :: [a]
xs = [a]
xs
isAproposAll (what :: Text
what:more :: [Text]
more) xs :: [a]
xs = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Text -> a -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
what)
([Text] -> [a] -> [a]
isAproposAll [Text]
more [a]
xs)
parts :: [Text]
parts = (Text -> Bool) -> [Text] -> [Text]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0) (Int -> Bool) -> (Text -> Int) -> Text -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Int
T.length) ([Text] -> [Text]) -> (Text -> [Text]) -> Text -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> [Text]
T.splitOn (String -> Text
T.pack " ") (Text -> [Text]) -> Text -> [Text]
forall a b. (a -> b) -> a -> b
$ Text
what
aproposModules :: IState -> T.Text -> [(String, Docstring DocTerm)]
aproposModules :: IState -> Text -> [(String, Docstring DocTerm)]
aproposModules ist :: IState
ist what :: Text
what = let mods :: [(Name, Docstring DocTerm)]
mods = Ctxt (Docstring DocTerm) -> [(Name, Docstring DocTerm)]
forall a. Ctxt a -> [(Name, a)]
toAlist (IState -> Ctxt (Docstring DocTerm)
idris_moduledocs IState
ist)
found :: [(Name, Docstring DocTerm)]
found = ((Name, Docstring DocTerm) -> (Name, Docstring DocTerm) -> Bool)
-> [(Name, Docstring DocTerm)] -> [(Name, Docstring DocTerm)]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (\x :: (Name, Docstring DocTerm)
x y :: (Name, Docstring DocTerm)
y -> (Name, Docstring DocTerm) -> Name
forall a b. (a, b) -> a
fst (Name, Docstring DocTerm)
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== (Name, Docstring DocTerm) -> Name
forall a b. (a, b) -> a
fst (Name, Docstring DocTerm)
y)
([Text]
-> [(Name, Docstring DocTerm)] -> [(Name, Docstring DocTerm)]
forall a a.
(Apropos a, Apropos a) =>
[Text] -> [(a, a)] -> [(a, a)]
isAproposAll [Text]
parts [(Name, Docstring DocTerm)]
mods)
in ((Name, Docstring DocTerm) -> (String, Docstring DocTerm))
-> [(Name, Docstring DocTerm)] -> [(String, Docstring DocTerm)]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Docstring DocTerm) -> (String, Docstring DocTerm)
forall b. (Name, b) -> (String, b)
unModName [(Name, Docstring DocTerm)]
found
where isAproposAll :: [Text] -> [(a, a)] -> [(a, a)]
isAproposAll [] xs :: [(a, a)]
xs = [(a, a)]
xs
isAproposAll (what :: Text
what:more :: [Text]
more) xs :: [(a, a)]
xs = ((a, a) -> Bool) -> [(a, a)] -> [(a, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(n :: a
n,d :: a
d) -> Text -> a -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
what a
n Bool -> Bool -> Bool
|| Text -> a -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
what a
d)
([Text] -> [(a, a)] -> [(a, a)]
isAproposAll [Text]
more [(a, a)]
xs)
parts :: [Text]
parts = (Text -> Bool) -> [Text] -> [Text]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0) (Int -> Bool) -> (Text -> Int) -> Text -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Int
T.length) ([Text] -> [Text]) -> (Text -> [Text]) -> Text -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> [Text]
T.splitOn (String -> Text
T.pack " ") (Text -> [Text]) -> Text -> [Text]
forall a b. (a -> b) -> a -> b
$ Text
what
unModName :: (Name, b) -> (String, b)
unModName (NS _ ns :: [Text]
ns, d :: b
d) = (([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> ([Text] -> [String]) -> [Text] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse "." ([String] -> [String])
-> ([Text] -> [String]) -> [Text] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack ([Text] -> [String]) -> ([Text] -> [Text]) -> [Text] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> [Text]
forall a. [a] -> [a]
reverse) [Text]
ns, b
d)
unModName (n :: Name
n, d :: b
d) = ("<<MODULE>>", b
d)
textIn :: T.Text -> T.Text -> Bool
textIn :: Text -> Text -> Bool
textIn a :: Text
a b :: Text
b = Text -> Text -> Bool
T.isInfixOf (Text -> Text
T.toLower Text
a) (Text -> Text
T.toLower Text
b)
class Apropos a where
isApropos :: T.Text -> a -> Bool
instance Apropos Name where
isApropos :: Text -> Name -> Bool
isApropos str :: Text
str (UN n :: Text
n) = Text -> Text -> Bool
textIn Text
str Text
n
isApropos str :: Text
str (NS n' :: Name
n' ns :: [Text]
ns) = Text -> Name -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Name
n' Bool -> Bool -> Bool
|| (Text -> Bool) -> [Text] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Text -> Text -> Bool
textIn Text
str) [Text]
ns
isApropos str :: Text
str n :: Name
n | (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
unitTy Bool -> Bool -> Bool
|| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
unitCon) Bool -> Bool -> Bool
&& Text
str Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack "()" = Bool
True
| (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pairTy Bool -> Bool -> Bool
|| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pairCon) Bool -> Bool -> Bool
&& Text
str Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack "," = Bool
True
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
eqTy Bool -> Bool -> Bool
&& Text
str Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack "=" = Bool
True
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
eqCon Bool -> Bool -> Bool
&& (Text -> Text
T.toLower Text
str) Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack "Refl" = Bool
True
| (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
sigmaTy Bool -> Bool -> Bool
|| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
sigmaCon) Bool -> Bool -> Bool
&& Text
str Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack "**" = Bool
True
isApropos _ _ = Bool
False
instance Apropos Def where
isApropos :: Text -> Def -> Bool
isApropos str :: Text
str (Function ty :: Type
ty tm :: Type
tm) = Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos str :: Text
str (TyDecl _ ty :: Type
ty) = Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos str :: Text
str (Operator ty :: Type
ty _ _) = Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos str :: Text
str (CaseOp _ ty :: Type
ty ty' :: [(Type, Bool)]
ty' _ _ _) = Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
instance Apropos (Binder (TT Name)) where
isApropos :: Text -> Binder Type -> Bool
isApropos str :: Text
str (Lam _ ty :: Type
ty) = Text
str Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack "\\" Bool -> Bool -> Bool
|| Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos str :: Text
str (Pi _ _ ty :: Type
ty _) = Text
str Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack "->" Bool -> Bool -> Bool
|| Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos str :: Text
str (Let _ ty :: Type
ty val :: Type
val) = Text
str Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack "let" Bool -> Bool -> Bool
|| Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty Bool -> Bool -> Bool
|| Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
val
isApropos str :: Text
str (NLet ty :: Type
ty val :: Type
val) = Text
str Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack "let" Bool -> Bool -> Bool
|| Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty Bool -> Bool -> Bool
|| Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
val
isApropos str :: Text
str _ = Bool
False
instance Apropos (TT Name) where
isApropos :: Text -> Type -> Bool
isApropos str :: Text
str (P Ref n :: Name
n ty :: Type
ty) = Text -> Name -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Name
n Bool -> Bool -> Bool
|| Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos str :: Text
str (P (TCon _ _) n :: Name
n ty :: Type
ty) = Text -> Name -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Name
n Bool -> Bool -> Bool
|| Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos str :: Text
str (P (DCon _ _ _) n :: Name
n ty :: Type
ty) = Text -> Name -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Name
n Bool -> Bool -> Bool
|| Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos str :: Text
str (P Bound _ ty :: Type
ty) = Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos str :: Text
str (Bind n :: Name
n b :: Binder Type
b tm :: Type
tm) = Text -> Binder Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Binder Type
b Bool -> Bool -> Bool
|| Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
tm
isApropos str :: Text
str (App _ t1 :: Type
t1 t2 :: Type
t2) = Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
t1 Bool -> Bool -> Bool
|| Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
t2
isApropos str :: Text
str (Constant const :: Const
const) = Text -> Const -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Const
const
isApropos str :: Text
str _ = Bool
False
instance Apropos Const where
isApropos :: Text -> Const -> Bool
isApropos str :: Text
str c :: Const
c = Text -> Text -> Bool
textIn Text
str (String -> Text
T.pack (Const -> String
forall a. Show a => a -> String
show Const
c))
instance Apropos (Docstring a) where
isApropos :: Text -> Docstring a -> Bool
isApropos str :: Text
str d :: Docstring a
d = Text -> Docstring a -> Bool
forall a. Text -> Docstring a -> Bool
containsText Text
str Docstring a
d
instance (Apropos a, Apropos b) => Apropos (a, b) where
isApropos :: Text -> (a, b) -> Bool
isApropos str :: Text
str (x :: a
x, y :: b
y) = Text -> a -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str a
x Bool -> Bool -> Bool
|| Text -> b -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str b
y
instance (Apropos a) => Apropos (Maybe a) where
isApropos :: Text -> Maybe a -> Bool
isApropos str :: Text
str (Just x :: a
x) = Text -> a -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str a
x
isApropos _ Nothing = Bool
False
instance (Apropos a) => Apropos [a] where
isApropos :: Text -> [a] -> Bool
isApropos str :: Text
str xs :: [a]
xs = (a -> Bool) -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Text -> a -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str) [a]
xs