{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}
module Idris.REPL.Browse (namespacesInNS, namesInNS) where
import Idris.AbsSyntax (getContext)
import Idris.AbsSyntaxTree (Idris)
import Idris.Core.Evaluate (Accessibility(Hidden, Private), ctxtAlist,
lookupDefAccExact)
import Idris.Core.TT (Name(..))
import Control.Monad (filterM)
import Data.List (isSuffixOf, nub)
import Data.Maybe (mapMaybe)
import qualified Data.Text as T (unpack)
namespacesInNS :: [String] -> Idris [[String]]
namespacesInNS :: [String] -> Idris [[String]]
namespacesInNS ns :: [String]
ns = do let revNS :: [String]
revNS = [String] -> [String]
forall a. [a] -> [a]
reverse [String]
ns
[(Name, Def)]
allNames <- (Context -> [(Name, Def)])
-> StateT IState (ExceptT Err IO) Context
-> StateT IState (ExceptT Err IO) [(Name, Def)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Context -> [(Name, Def)]
ctxtAlist StateT IState (ExceptT Err IO) Context
getContext
[[String]] -> Idris [[String]]
forall (m :: * -> *) a. Monad m => a -> m a
return ([[String]] -> Idris [[String]])
-> ([[String]] -> [[String]]) -> [[String]] -> Idris [[String]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[String]] -> [[String]]
forall a. Eq a => [a] -> [a]
nub ([[String]] -> Idris [[String]]) -> [[String]] -> Idris [[String]]
forall a b. (a -> b) -> a -> b
$
[ [String] -> [String]
forall a. [a] -> [a]
reverse [String]
space | [String]
space <- ((Name, Def) -> Maybe [String]) -> [(Name, Def)] -> [[String]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Name -> Maybe [String]
getNS (Name -> Maybe [String])
-> ((Name, Def) -> Name) -> (Name, Def) -> Maybe [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Def) -> Name
forall a b. (a, b) -> a
fst) [(Name, Def)]
allNames
, [String]
revNS [String] -> [String] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` [String]
space
, [String]
revNS [String] -> [String] -> Bool
forall a. Eq a => a -> a -> Bool
/= [String]
space ]
where getNS :: Name -> Maybe [String]
getNS (NS _ namespace :: [Text]
namespace) = [String] -> Maybe [String]
forall a. a -> Maybe a
Just ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack [Text]
namespace)
getNS _ = Maybe [String]
forall a. Maybe a
Nothing
namesInNS :: [String] -> Idris [Name]
namesInNS :: [String] -> Idris [Name]
namesInNS ns :: [String]
ns = do let revNS :: [String]
revNS = [String] -> [String]
forall a. [a] -> [a]
reverse [String]
ns
[(Name, Def)]
allNames <- (Context -> [(Name, Def)])
-> StateT IState (ExceptT Err IO) Context
-> StateT IState (ExceptT Err IO) [(Name, Def)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Context -> [(Name, Def)]
ctxtAlist StateT IState (ExceptT Err IO) Context
getContext
let namesInSpace :: [Name]
namesInSpace = [ Name
n | (n :: Name
n, space :: [String]
space) <- ((Name, Def) -> Maybe (Name, [String]))
-> [(Name, Def)] -> [(Name, [String])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Name -> Maybe (Name, [String])
getNS (Name -> Maybe (Name, [String]))
-> ((Name, Def) -> Name) -> (Name, Def) -> Maybe (Name, [String])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Def) -> Name
forall a b. (a, b) -> a
fst) [(Name, Def)]
allNames
, [String]
revNS [String] -> [String] -> Bool
forall a. Eq a => a -> a -> Bool
== [String]
space ]
(Name -> StateT IState (ExceptT Err IO) Bool)
-> [Name] -> Idris [Name]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM Name -> StateT IState (ExceptT Err IO) Bool
accessible [Name]
namesInSpace
where getNS :: Name -> Maybe (Name, [String])
getNS n :: Name
n@(NS (UN n' :: Text
n') namespace :: [Text]
namespace) = (Name, [String]) -> Maybe (Name, [String])
forall a. a -> Maybe a
Just (Name
n, ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack [Text]
namespace))
getNS _ = Maybe (Name, [String])
forall a. Maybe a
Nothing
accessible :: Name -> StateT IState (ExceptT Err IO) Bool
accessible n :: Name
n = do Context
ctxt <- StateT IState (ExceptT Err IO) Context
getContext
case Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n Bool
False Context
ctxt of
Just (_, Hidden ) -> Bool -> StateT IState (ExceptT Err IO) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just (_, Private ) -> Bool -> StateT IState (ExceptT Err IO) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
_ -> Bool -> StateT IState (ExceptT Err IO) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True