module HERMIT.Shell.Completion (shellComplete) where
import Control.Applicative
import Control.Arrow
import Control.Monad.State
import Data.Dynamic
import Data.List (isPrefixOf, nub)
import Data.Map (keys)
import Data.Maybe (fromMaybe)
import HERMIT.Kure
import HERMIT.External
import qualified HERMIT.GHC as GHC
import HERMIT.Kernel.Scoped
import HERMIT.Monad
import HERMIT.Parser
import HERMIT.Dictionary.Inline
import HERMIT.Dictionary.Navigation
import HERMIT.Dictionary.Reasoning
import HERMIT.Dictionary.Rules
import HERMIT.Shell.Interpreter
import HERMIT.Shell.Types
import System.Console.Haskeline hiding (catch, display)
shellComplete :: (MonadCatch m, MonadIO m, MonadState CommandLineState m) => String -> String -> m [Completion]
shellComplete rPrev so_far = do
let (partial, _) = toUnmatched rPrev
if null partial
then completionsFor so_far [CommandC]
else case parseExprH partial of
Left _ -> return []
Right e -> do
eds <- attemptM $ exprToDyns e
case eds of
Left msg -> liftIO $ putStrLn ("\n" ++ msg) >> return []
Right ds -> do
let ts = [ head args | d <- ds
, let args = fst (splitFunTyArgs (dynTypeRep d))
, not (null args) ]
completionsFor so_far $ filterUnknowns $ map (completionType.show) ts
completionsFor :: (MonadCatch m, MonadIO m, MonadState CommandLineState m)
=> String -> [CompletionType] -> m [Completion]
completionsFor so_far cts = do
qs <- mapM completionQuery cts
(k,(env,sast)) <- gets (cl_kernel &&& cl_kernel_env &&& cl_cursor)
cls <- forM qs $ \ q -> catchM (queryS k q env sast) (\_ -> return [])
return $ map simpleCompletion $ nub $ filter (so_far `isPrefixOf`) $ concat cls
data CompletionType = ConsiderC
| BindingOfC
| BindingGroupOfC
| RhsOfC
| OccurrenceOfC
| InlineC
| InScopeC
| LemmaC
| CommandC
| CoreC
| NothingC
| RuleC
| StashC
| StringC
| UnknownC String
completionType :: String -> CompletionType
completionType s = fromMaybe (UnknownC s) (lookup s m)
where m = [ ("BindingName" , BindingOfC)
, ("Considerable" , ConsiderC)
, ("CoreBox" , CoreC)
, ("HermitName" , NothingC)
, ("IntBox" , NothingC)
, ("LemmaName" , LemmaC)
, ("OccurrenceName", OccurrenceOfC)
, ("RememberedName", StashC)
, ("RewriteCoreBox", CommandC)
, ("RhsOfName" , RhsOfC)
, ("RuleName" , RuleC)
, ("StringBox" , StringC)
]
filterUnknowns :: [CompletionType] -> [CompletionType]
filterUnknowns l = if null l' then l else l'
where l' = filter (\case UnknownC _ -> False ; _ -> True) l
completionQuery :: (MonadIO m, MonadState CommandLineState m) => CompletionType -> m (TransformH CoreTC [String])
completionQuery ConsiderC = return $ pure $ map fst considerables
completionQuery OccurrenceOfC = return $ occurrenceOfTargetsT >>^ GHC.varSetToStrings >>^ map ('\'':)
completionQuery BindingOfC = return $ bindingOfTargetsT >>^ GHC.varSetToStrings >>^ map ('\'':)
completionQuery BindingGroupOfC = return $ bindingGroupOfTargetsT >>^ GHC.varSetToStrings >>^ map ('\'':)
completionQuery RhsOfC = return $ rhsOfTargetsT >>^ GHC.varSetToStrings >>^ map ('\'':)
completionQuery InlineC = return $ promoteT inlineTargetsT >>^ map ('\'':)
completionQuery InScopeC = return $ pure ["'"]
completionQuery LemmaC = return $ liftM (map show . keys) $ getLemmasT
completionQuery NothingC = return $ pure []
completionQuery RuleC = return $ liftM (map (show . fst)) $ getHermitRulesT
completionQuery StashC = return $ liftM (map show . keys) $ constT getStash
completionQuery StringC = return $ pure ["\""]
completionQuery CommandC = gets cl_externals >>= return . pure . map externName
completionQuery CoreC = return $ pure ["[|"]
completionQuery (UnknownC s) = do
liftIO $ putStrLn $ "\nCannot tab complete: unknown argument type: " ++ s
return (pure [])
toUnmatched :: String -> (String, String)
toUnmatched = go 0 ""
where go :: Int -> String -> String -> (String, String)
go n acc s@('(':cs)
| n > 0 = go (n1) ('(':acc) cs
| otherwise = (acc, s)
go n acc (')':cs) = go (n+1) (')':acc) cs
go n acc (c:cs) = go n (c:acc) cs
go _ acc [] = (acc, [])