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