{-# 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 = [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 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
[[String]] -> Idris [[String]]
forall a. a -> StateT IState (ExceptT Err IO) a
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 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
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
[(Name, Def)]
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]
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 ]
(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 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 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 (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