{-# 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 = 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 [] [a]
xs = [a]
xs
isAproposAll (Text
what:[Text]
more) [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
> Int
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
. HasCallStack => Text -> Text -> [Text]
Text -> Text -> [Text]
T.splitOn (String -> Text
T.pack String
" ") (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 IState
ist 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 (\(Name, Docstring DocTerm)
x (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 [] [(a, a)]
xs = [(a, a)]
xs
isAproposAll (Text
what:[Text]
more) [(a, a)]
xs = ((a, a) -> Bool) -> [(a, a)] -> [(a, a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(a
n,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
> Int
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
. HasCallStack => Text -> Text -> [Text]
Text -> Text -> [Text]
T.splitOn (String -> Text
T.pack String
" ") (Text -> [Text]) -> Text -> [Text]
forall a b. (a -> b) -> a -> b
$ Text
what
unModName :: (Name, b) -> (String, b)
unModName (NS Name
_ [Text]
ns, 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] -> [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 (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) = 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 Text
str 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 String
"()" = 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 String
"," = 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 String
"=" = 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 String
"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 String
"**" = Bool
True
isApropos Text
_ Name
_ = Bool
False
instance Apropos Def where
isApropos :: Text -> Def -> Bool
isApropos Text
str (Function Type
ty Type
tm) = Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos Text
str (TyDecl NameType
_ Type
ty) = Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos Text
str (Operator Type
ty Int
_ [Value] -> Maybe Value
_) = Text -> Type -> Bool
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
_) = 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 Text
str (Lam RigCount
_ Type
ty) = Text
str Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack String
"\\" Bool -> Bool -> Bool
|| Text -> Type -> 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 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack String
"->" Bool -> Bool -> Bool
|| Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos Text
str (Let RigCount
_ Type
ty Type
val) = Text
str Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack String
"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 Text
str (NLet Type
ty Type
val) = Text
str Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
T.pack String
"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 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) = 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 Text
str (P (TCon Int
_ Int
_) Name
n 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 Text
str (P (DCon Int
_ Int
_ Bool
_) Name
n 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 Text
str (P NameType
Bound Name
_ Type
ty) = Text -> Type -> Bool
forall a. Apropos a => Text -> a -> Bool
isApropos Text
str Type
ty
isApropos Text
str (Bind Name
n Binder Type
b 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 Text
str (App AppStatus Name
_ Type
t1 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 Text
str (Constant Const
const) = Text -> Const -> Bool
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 (Const -> String
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 = 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 Text
str (a
x, 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 Text
str (Just a
x) = Text -> a -> Bool
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 = (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