module Dhall.LSP.Backend.Completion where
import Data.Text (Text)
import Data.Void (absurd)
import Dhall.LSP.Backend.Diagnostics (Position, positionToOffset)
import System.Directory (doesDirectoryExist, listDirectory)
import System.FilePath (takeDirectory, (</>))
import System.Environment (getEnvironment)
import System.Timeout (timeout)
import Dhall.Context (empty, toList)
import qualified Data.Text as Text
import Dhall.Context (Context, insert)
import Dhall.Core (Binding(..), Expr(..), Var(..), normalize, shift, subst, pretty, reservedIdentifiers)
import Dhall.TypeCheck (X, typeWithA, typeOf)
import Dhall.Parser (Src, exprFromText)
import qualified Dhall.Map
import qualified Data.HashSet as HashSet
import Dhall.LSP.Backend.Parsing (holeExpr)
completionQueryAt :: Text -> Position -> (Text, Text)
completionQueryAt text pos = (completionLeadup, completionPrefix)
where
off = positionToOffset text pos
text' = Text.take off text
breakEnd :: (Char -> Bool) -> Text -> (Text, Text)
breakEnd p =
(\(l,r) -> (Text.reverse l, Text.reverse r)) . Text.break p . Text.reverse
(completionPrefix, completionLeadup) =
breakEnd (`elem` (" \t\n[(,=+*&|}#?>" :: [Char])) text'
data Completion =
Completion {
completeText :: Text,
completeType :: Maybe (Expr Src X) }
completeLocalImport :: FilePath -> FilePath -> IO [Completion]
completeLocalImport relativeTo prefix = do
let dir = takeDirectory relativeTo </> takeDirectory prefix
exists <- doesDirectoryExist dir
if not exists
then return []
else do
let second = 10 ^ (6 :: Int)
mFiles <- timeout second (listDirectory dir)
case mFiles of
Just files -> return (map (\file -> Completion (Text.pack file) Nothing) files)
Nothing -> return []
completeEnvironmentImport :: IO [Completion]
completeEnvironmentImport = do
environment <- getEnvironment
let environmentImports = map (Text.pack . fst) environment
return $ map (\env -> Completion env Nothing) environmentImports
data CompletionContext =
CompletionContext {
context :: Context (Expr Src X),
values :: Context (Expr Src X) }
buildCompletionContext :: Expr Src X -> CompletionContext
buildCompletionContext = buildCompletionContext' empty empty
buildCompletionContext' :: Context (Expr Src X) -> Context (Expr Src X)
-> Expr Src X -> CompletionContext
buildCompletionContext' context values (Let (Binding { variable = x, annotation = mA, value = a }) e)
| Right _A <- typeWithA absurd context a =
let _A' = normalize _A
a' = normalize a
e' = subst (V x 0) a' e
context' = fmap (shift 1 (V x 0)) $ insert x _A' context
values' = fmap (shift 1 (V x 0)) $ insert x a' values
in buildCompletionContext' context' values' e'
| Just (_, _A) <- mA
, Right _ <- typeWithA absurd context _A =
let _A' = normalize _A
context' = fmap (shift 1 (V x 0)) $ insert x _A' context
values' = fmap (shift 1 (V x 0)) $ insert x holeExpr values
in buildCompletionContext' context' values' e
| otherwise =
let context' = fmap (shift 1 (V x 0)) $ insert x holeExpr context
values' = fmap (shift 1 (V x 0)) $ insert x holeExpr values
in buildCompletionContext' context' values' e
buildCompletionContext' context values (Lam x _A b) =
let _A' | Right _ <- typeWithA absurd context _A = normalize _A
| otherwise = holeExpr
context' = fmap (shift 1 (V x 0)) $ insert x _A' context
values' = fmap (shift 1 (V x 0)) $ insert x holeExpr values
in buildCompletionContext' context' values' b
buildCompletionContext' context values (Pi x _A b) =
let _A' | Right _ <- typeWithA absurd context _A = normalize _A
| otherwise = holeExpr
context' = fmap (shift 1 (V x 0)) $ insert x _A' context
values' = fmap (shift 1 (V x 0)) $ insert x holeExpr values
in buildCompletionContext' context' values' b
buildCompletionContext' context values _ = CompletionContext context values
contextToVariables :: [(Text, Expr Src X)] -> [Var]
contextToVariables [] = []
contextToVariables ((name, _) : rest) =
V name 0 : map (inc name) (contextToVariables rest)
where inc x (V y i) | x == y = V x (i + 1)
| otherwise = V y i
completeFromContext :: CompletionContext -> [Completion]
completeFromContext (CompletionContext context _) =
let context' = toList context
completeReserved keyword
| Right expr <- exprFromText "" keyword
, Right typ <- typeOf (do _ <- expr; holeExpr) =
Completion keyword (Just typ)
| otherwise = Completion keyword Nothing
reserved = map completeReserved $ HashSet.toList reservedIdentifiers
in [ Completion (pretty var) (if typ == holeExpr then Nothing else Just typ)
| (var, (_, typ)) <- zip (contextToVariables context') context' ]
++ reserved
completeProjections :: CompletionContext -> Expr Src X -> [Completion]
completeProjections (CompletionContext context values) expr =
let values' = toList values
subs = filter ((/= holeExpr) . snd) $ zip (contextToVariables values') (map snd values')
expr' = foldl (\e (x,val) -> subst x val e) expr subs
in case typeWithA absurd context expr' of
Left _ -> []
Right _A ->
let expr'' = normalize expr'
in completeUnion expr'' expr'' ++ completeRecord (normalize _A)
where
completeUnion _A (Union m) =
let constructor (k, Nothing) = Completion k (Just _A)
constructor (k, Just v) = Completion k (Just (Pi k v _A))
in map constructor (Dhall.Map.toList m)
completeUnion _ _ = []
completeRecord (Record m) =
map (\(name, typ) -> Completion name (Just typ)) (Dhall.Map.toList m)
completeRecord _ = []