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