module Dhall.LSP.Backend.Completion where
import Data.List (foldl')
import Data.Text (Text)
import Data.Void (Void, absurd)
import Dhall.Context (Context, insert)
import Dhall.Context (empty, toList)
import Dhall.LSP.Backend.Diagnostics (Position, positionToOffset)
import Dhall.LSP.Backend.Parsing (holeExpr)
import Dhall.Parser (Src, exprFromText)
import Dhall.TypeCheck (typeWithA, typeOf)
import System.Directory (doesDirectoryExist, listDirectory)
import System.Environment (getEnvironment)
import System.FilePath (takeDirectory, (</>))
import System.Timeout (timeout)
import Dhall.Core
( Binding(..)
, Expr(..)
, Var(..)
, normalize
, shift
, subst
, pretty
, reservedIdentifiers
)
import qualified Data.HashSet as HashSet
import qualified Data.Text as Text
import qualified Dhall.Map
import qualified Dhall.Pretty
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 Void) }
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 toCompletion (variable, _) = Completion escapedVariable Nothing
where
escapedVariable =
Dhall.Pretty.escapeEnvironmentVariable (Text.pack variable)
return (map toCompletion environment)
data CompletionContext =
CompletionContext {
context :: Context (Expr Src Void),
values :: Context (Expr Src Void) }
buildCompletionContext :: Expr Src Void -> CompletionContext
buildCompletionContext = buildCompletionContext' empty empty
buildCompletionContext' :: Context (Expr Src Void) -> Context (Expr Src Void)
-> Expr Src Void -> 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 Void)] -> [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 Void -> [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 (Dhall.Pretty.escapeLabel True k) (Just _A)
constructor (k, Just v) =
Completion (Dhall.Pretty.escapeLabel True k) (Just (Pi k v _A))
in map constructor (Dhall.Map.toList m)
completeUnion _ _ = []
completeRecord (Record m) = map toCompletion (Dhall.Map.toList m)
where
toCompletion (name, typ) =
Completion (Dhall.Pretty.escapeLabel True name) (Just typ)
completeRecord _ = []