module Idris.REPL.Browse (namespacesInNS, namesInNS) where
import Control.Monad (filterM)
import Data.List (isSuffixOf, nub)
import Data.Maybe (mapMaybe)
import qualified Data.Text as T (unpack)
import Idris.Core.Evaluate (ctxtAlist, Accessibility(Private, Hidden), lookupDefAccExact)
import Idris.Core.TT (Name(..))
import Idris.AbsSyntaxTree (Idris)
import Idris.AbsSyntax (getContext)
namespacesInNS :: [String] -> Idris [[String]]
namespacesInNS ns = do let revNS = reverse ns
allNames <- fmap ctxtAlist getContext
return . nub $
[ reverse space | space <- mapMaybe (getNS . fst) allNames
, revNS `isSuffixOf` space
, revNS /= space ]
where getNS (NS _ namespace) = Just (map T.unpack namespace)
getNS _ = Nothing
namesInNS :: [String] -> Idris [Name]
namesInNS ns = do let revNS = reverse ns
allNames <- fmap ctxtAlist getContext
let namesInSpace = [ n | (n, space) <- mapMaybe (getNS . fst) allNames
, revNS == space ]
filterM accessible namesInSpace
where getNS n@(NS (UN n') namespace) = Just (n, (map T.unpack namespace))
getNS _ = Nothing
accessible n = do ctxt <- getContext
case lookupDefAccExact n False ctxt of
Just (_, Hidden ) -> return False
Just (_, Private ) -> return False
_ -> return True