{-# 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 [String]
ns = do let revNS :: [String]
revNS = forall a. [a] -> [a]
reverse [String]
ns
[(Name, Def)]
allNames <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Context -> [(Name, Def)]
ctxtAlist Idris Context
getContext
forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$
[ forall a. [a] -> [a]
reverse [String]
space | [String]
space <- forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Name -> Maybe [String]
getNS forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Name, Def)]
allNames
, [String]
revNS forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` [String]
space
, [String]
revNS forall a. Eq a => a -> a -> Bool
/= [String]
space ]
where getNS :: Name -> Maybe [String]
getNS (NS Name
_ [Text]
namespace) = forall a. a -> Maybe a
Just (forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack [Text]
namespace)
getNS Name
_ = forall a. Maybe a
Nothing
namesInNS :: [String] -> Idris [Name]
namesInNS :: [String] -> Idris [Name]
namesInNS [String]
ns = do let revNS :: [String]
revNS = forall a. [a] -> [a]
reverse [String]
ns
[(Name, Def)]
allNames <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Context -> [(Name, Def)]
ctxtAlist Idris Context
getContext
let namesInSpace :: [Name]
namesInSpace = [ Name
n | (Name
n, [String]
space) <- forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Name -> Maybe (Name, [String])
getNS forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Name, Def)]
allNames
, [String]
revNS forall a. Eq a => a -> a -> Bool
== [String]
space ]
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 Text
n') [Text]
namespace) = forall a. a -> Maybe a
Just (Name
n, (forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack [Text]
namespace))
getNS Name
_ = forall a. Maybe a
Nothing
accessible :: Name -> StateT IState (ExceptT Err IO) Bool
accessible Name
n = do Context
ctxt <- Idris Context
getContext
case Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n Bool
False Context
ctxt of
Just (Def
_, Accessibility
Hidden ) -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just (Def
_, Accessibility
Private ) -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Maybe (Def, Accessibility)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True