{-|
Module      : Idris.REPL.Browse
Description : Browse the current namespace.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# 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)

-- | Find the sub-namespaces of a given namespace. The components
-- should be in display order rather than the order that they are in
-- inside of NS constructors.
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

-- | Find the user-accessible names that occur directly within a given
-- namespace. The components should be in display order rather than
-- the order that they are in inside of NS constructors.
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