module Dhall.LSP.Backend.Completion where

import Data.List                     (foldl')
import Data.Text                     (Text)
import Data.Void                     (Void, absurd)
import Dhall.Context                 (Context, empty, insert, toList)
import Dhall.LSP.Backend.Diagnostics (Position, positionToOffset)
import Dhall.LSP.Backend.Parsing     (holeExpr)
import Dhall.Parser                  (Src, exprFromText)
import Dhall.TypeCheck               (typeOf, typeWithA)
import System.Directory              (doesDirectoryExist, listDirectory)
import System.Environment            (getEnvironment)
import System.FilePath               (takeDirectory, (</>))
import System.Timeout                (timeout)

import Dhall.Core
    ( Binding (..)
    , Expr (..)
    , FunctionBinding (..)
    , RecordField (..)
    , Var (..)
    , normalize
    , pretty
    , reservedIdentifiers
    , shift
    , subst
    )

import qualified Data.HashSet as HashSet
import qualified Data.Text    as Text
import qualified Dhall.Map
import qualified Dhall.Pretty

-- | Given the cursor position construct the corresponding 'completion query'
-- consisting of the leadup, i.e. text leading up to the word prefix that is to
-- be completed, as well as the prefix that is to be completed.
completionQueryAt :: Text -> Position -> (Text, Text)
completionQueryAt :: Text -> Position -> (Text, Text)
completionQueryAt Text
text Position
pos = (Text
completionLeadup, Text
completionPrefix)
 where
  off :: Int
off = Text -> Position -> Int
positionToOffset Text
text Position
pos
  text' :: Text
text' = Int -> Text -> Text
Text.take Int
off Text
text
  breakEnd :: (Char -> Bool) -> Text -> (Text, Text)
  breakEnd :: (Char -> Bool) -> Text -> (Text, Text)
breakEnd Char -> Bool
p =
    (\(Text
l,Text
r) -> (Text -> Text
Text.reverse Text
l, Text -> Text
Text.reverse Text
r)) ((Text, Text) -> (Text, Text))
-> (Text -> (Text, Text)) -> Text -> (Text, Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> Text -> (Text, Text)
Text.break Char -> Bool
p (Text -> (Text, Text)) -> (Text -> Text) -> Text -> (Text, Text)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
Text.reverse
  (Text
completionPrefix, Text
completionLeadup) =
    (Char -> Bool) -> Text -> (Text, Text)
breakEnd (Char -> [Char] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Char]
" \t\n[(,=+*&|}#?>" :: String)) Text
text'

-- | A completion result, optionally annotated with type information.
data Completion =
  Completion {
    Completion -> Text
completeText :: Text,
    Completion -> Maybe (Expr Src Void)
completeType :: Maybe (Expr Src Void) }

-- | Complete file names.
completeLocalImport :: FilePath -> FilePath -> IO [Completion]
completeLocalImport :: [Char] -> [Char] -> IO [Completion]
completeLocalImport [Char]
relativeTo [Char]
prefix = do
  let dir :: [Char]
dir = [Char] -> [Char]
takeDirectory [Char]
relativeTo [Char] -> [Char] -> [Char]
</> [Char] -> [Char]
takeDirectory [Char]
prefix
  Bool
exists <- [Char] -> IO Bool
doesDirectoryExist [Char]
dir
  if Bool -> Bool
not Bool
exists
  then [Completion] -> IO [Completion]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  else do
    let second :: Int
second = Int
10 Int -> Int -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
6 :: Int)
    Maybe [[Char]]
mFiles <- Int -> IO [[Char]] -> IO (Maybe [[Char]])
forall a. Int -> IO a -> IO (Maybe a)
timeout Int
second ([Char] -> IO [[Char]]
listDirectory [Char]
dir)  -- 1s timeout
    case Maybe [[Char]]
mFiles of
      Just [[Char]]
files -> [Completion] -> IO [Completion]
forall (m :: * -> *) a. Monad m => a -> m a
return (([Char] -> Completion) -> [[Char]] -> [Completion]
forall a b. (a -> b) -> [a] -> [b]
map (\[Char]
file -> Text -> Maybe (Expr Src Void) -> Completion
Completion ([Char] -> Text
Text.pack [Char]
file) Maybe (Expr Src Void)
forall a. Maybe a
Nothing) [[Char]]
files)
      Maybe [[Char]]
Nothing -> [Completion] -> IO [Completion]
forall (m :: * -> *) a. Monad m => a -> m a
return []

-- | Complete environment variables.
completeEnvironmentImport :: IO [Completion]
completeEnvironmentImport :: IO [Completion]
completeEnvironmentImport = do
  [([Char], [Char])]
environment <- IO [([Char], [Char])]
getEnvironment

  let toCompletion :: ([Char], b) -> Completion
toCompletion ([Char]
variable, b
_) = Text -> Maybe (Expr Src Void) -> Completion
Completion Text
escapedVariable Maybe (Expr Src Void)
forall a. Maybe a
Nothing
       where
          escapedVariable :: Text
escapedVariable =
              Text -> Text
Dhall.Pretty.escapeEnvironmentVariable ([Char] -> Text
Text.pack [Char]
variable)

  [Completion] -> IO [Completion]
forall (m :: * -> *) a. Monad m => a -> m a
return ((([Char], [Char]) -> Completion)
-> [([Char], [Char])] -> [Completion]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], [Char]) -> Completion
forall b. ([Char], b) -> Completion
toCompletion [([Char], [Char])]
environment)

-- | A completion context, consisting of the (approximated) type-checking
-- context. We need to substitute 'dependent lets' later so we keep their values
-- around.
data CompletionContext =
  CompletionContext {
    CompletionContext -> Context (Expr Src Void)
context :: Context (Expr Src Void),
    -- values to be substituted for 'dependent let' behaviour
    CompletionContext -> Context (Expr Src Void)
values :: Context (Expr Src Void) }

-- | Given a 'binders expression' (with arbitrarily many 'holes') construct the
-- corresponding completion context.
buildCompletionContext :: Expr Src Void -> CompletionContext
buildCompletionContext :: Expr Src Void -> CompletionContext
buildCompletionContext = Context (Expr Src Void)
-> Context (Expr Src Void) -> Expr Src Void -> CompletionContext
buildCompletionContext' Context (Expr Src Void)
forall a. Context a
empty Context (Expr Src Void)
forall a. Context a
empty

buildCompletionContext' :: Context (Expr Src Void) -> Context (Expr Src Void)
  -> Expr Src Void -> CompletionContext
buildCompletionContext' :: Context (Expr Src Void)
-> Context (Expr Src Void) -> Expr Src Void -> CompletionContext
buildCompletionContext' Context (Expr Src Void)
context Context (Expr Src Void)
values (Let (Binding { variable :: forall s a. Binding s a -> Text
variable = Text
x, annotation :: forall s a. Binding s a -> Maybe (Maybe s, Expr s a)
annotation = Maybe (Maybe Src, Expr Src Void)
mA, value :: forall s a. Binding s a -> Expr s a
value = Expr Src Void
a }) Expr Src Void
e)
  -- We prefer the actual value over the annotated type in order to get
  -- 'dependent let' behaviour whenever possible.
  | Right Expr Src Void
_A <- Typer Void
-> Context (Expr Src Void)
-> Expr Src Void
-> Either (TypeError Src Void) (Expr Src Void)
forall a s.
(Eq a, Pretty a) =>
Typer a
-> Context (Expr s a)
-> Expr s a
-> Either (TypeError s a) (Expr s a)
typeWithA forall a. Void -> a
Typer Void
absurd Context (Expr Src Void)
context Expr Src Void
a =
    let _A' :: Expr t Void
_A' = Expr Src Void -> Expr t Void
forall a s t. Eq a => Expr s a -> Expr t a
normalize Expr Src Void
_A

        a' :: Expr t Void
a' = Expr Src Void -> Expr t Void
forall a s t. Eq a => Expr s a -> Expr t a
normalize Expr Src Void
a
        e' :: Expr Src Void
e' = Var -> Expr Src Void -> Expr Src Void -> Expr Src Void
forall s a. Var -> Expr s a -> Expr s a -> Expr s a
subst (Text -> Int -> Var
V Text
x Int
0) Expr Src Void
forall t. Expr t Void
a' Expr Src Void
e

        context' :: Context (Expr Src Void)
context' = Int -> Var -> Expr Src Void -> Expr Src Void
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
1 (Text -> Int -> Var
V Text
x Int
0) (Expr Src Void -> Expr Src Void)
-> Context (Expr Src Void) -> Context (Expr Src Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text
-> Expr Src Void
-> Context (Expr Src Void)
-> Context (Expr Src Void)
forall a. Text -> a -> Context a -> Context a
insert Text
x Expr Src Void
forall t. Expr t Void
_A' Context (Expr Src Void)
context
        values' :: Context (Expr Src Void)
values' = Int -> Var -> Expr Src Void -> Expr Src Void
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
1 (Text -> Int -> Var
V Text
x Int
0) (Expr Src Void -> Expr Src Void)
-> Context (Expr Src Void) -> Context (Expr Src Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text
-> Expr Src Void
-> Context (Expr Src Void)
-> Context (Expr Src Void)
forall a. Text -> a -> Context a -> Context a
insert Text
x Expr Src Void
forall t. Expr t Void
a' Context (Expr Src Void)
values

    in Context (Expr Src Void)
-> Context (Expr Src Void) -> Expr Src Void -> CompletionContext
buildCompletionContext' Context (Expr Src Void)
context' Context (Expr Src Void)
values' Expr Src Void
e'

  -- fall back to annotated type if body doesn't type check; bind to `holeExpr`
  | Just (Maybe Src
_, Expr Src Void
_A) <- Maybe (Maybe Src, Expr Src Void)
mA
  , Right Expr Src Void
_ <- Typer Void
-> Context (Expr Src Void)
-> Expr Src Void
-> Either (TypeError Src Void) (Expr Src Void)
forall a s.
(Eq a, Pretty a) =>
Typer a
-> Context (Expr s a)
-> Expr s a
-> Either (TypeError s a) (Expr s a)
typeWithA forall a. Void -> a
Typer Void
absurd Context (Expr Src Void)
context Expr Src Void
_A =
    let _A' :: Expr t Void
_A' = Expr Src Void -> Expr t Void
forall a s t. Eq a => Expr s a -> Expr t a
normalize Expr Src Void
_A

        context' :: Context (Expr Src Void)
context' = Int -> Var -> Expr Src Void -> Expr Src Void
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
1 (Text -> Int -> Var
V Text
x Int
0) (Expr Src Void -> Expr Src Void)
-> Context (Expr Src Void) -> Context (Expr Src Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text
-> Expr Src Void
-> Context (Expr Src Void)
-> Context (Expr Src Void)
forall a. Text -> a -> Context a -> Context a
insert Text
x Expr Src Void
forall t. Expr t Void
_A' Context (Expr Src Void)
context
        values' :: Context (Expr Src Void)
values' = Int -> Var -> Expr Src Void -> Expr Src Void
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
1 (Text -> Int -> Var
V Text
x Int
0) (Expr Src Void -> Expr Src Void)
-> Context (Expr Src Void) -> Context (Expr Src Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text
-> Expr Src Void
-> Context (Expr Src Void)
-> Context (Expr Src Void)
forall a. Text -> a -> Context a -> Context a
insert Text
x Expr Src Void
forall s a. Expr s a
holeExpr Context (Expr Src Void)
values

    in Context (Expr Src Void)
-> Context (Expr Src Void) -> Expr Src Void -> CompletionContext
buildCompletionContext' Context (Expr Src Void)
context' Context (Expr Src Void)
values' Expr Src Void
e

  -- if nothing works, only remember the name (but bind to `holeExpr`)
  | Bool
otherwise =
    let context' :: Context (Expr Src Void)
context' = Int -> Var -> Expr Src Void -> Expr Src Void
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
1 (Text -> Int -> Var
V Text
x Int
0) (Expr Src Void -> Expr Src Void)
-> Context (Expr Src Void) -> Context (Expr Src Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text
-> Expr Src Void
-> Context (Expr Src Void)
-> Context (Expr Src Void)
forall a. Text -> a -> Context a -> Context a
insert Text
x Expr Src Void
forall s a. Expr s a
holeExpr Context (Expr Src Void)
context
        values' :: Context (Expr Src Void)
values' = Int -> Var -> Expr Src Void -> Expr Src Void
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
1 (Text -> Int -> Var
V Text
x Int
0) (Expr Src Void -> Expr Src Void)
-> Context (Expr Src Void) -> Context (Expr Src Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text
-> Expr Src Void
-> Context (Expr Src Void)
-> Context (Expr Src Void)
forall a. Text -> a -> Context a -> Context a
insert Text
x Expr Src Void
forall s a. Expr s a
holeExpr Context (Expr Src Void)
values

    in Context (Expr Src Void)
-> Context (Expr Src Void) -> Expr Src Void -> CompletionContext
buildCompletionContext' Context (Expr Src Void)
context' Context (Expr Src Void)
values' Expr Src Void
e

buildCompletionContext' Context (Expr Src Void)
context Context (Expr Src Void)
values (Lam Maybe CharacterSet
_ (FunctionBinding { functionBindingVariable :: forall s a. FunctionBinding s a -> Text
functionBindingVariable = Text
x, functionBindingAnnotation :: forall s a. FunctionBinding s a -> Expr s a
functionBindingAnnotation = Expr Src Void
_A}) Expr Src Void
b) =
  let _A' :: Expr t Void
_A' | Right Expr Src Void
_ <- Typer Void
-> Context (Expr Src Void)
-> Expr Src Void
-> Either (TypeError Src Void) (Expr Src Void)
forall a s.
(Eq a, Pretty a) =>
Typer a
-> Context (Expr s a)
-> Expr s a
-> Either (TypeError s a) (Expr s a)
typeWithA forall a. Void -> a
Typer Void
absurd Context (Expr Src Void)
context Expr Src Void
_A = Expr Src Void -> Expr t Void
forall a s t. Eq a => Expr s a -> Expr t a
normalize Expr Src Void
_A
          | Bool
otherwise = Expr t Void
forall s a. Expr s a
holeExpr

      context' :: Context (Expr Src Void)
context' = Int -> Var -> Expr Src Void -> Expr Src Void
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
1 (Text -> Int -> Var
V Text
x Int
0) (Expr Src Void -> Expr Src Void)
-> Context (Expr Src Void) -> Context (Expr Src Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text
-> Expr Src Void
-> Context (Expr Src Void)
-> Context (Expr Src Void)
forall a. Text -> a -> Context a -> Context a
insert Text
x Expr Src Void
forall t. Expr t Void
_A' Context (Expr Src Void)
context
      values' :: Context (Expr Src Void)
values' = Int -> Var -> Expr Src Void -> Expr Src Void
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
1 (Text -> Int -> Var
V Text
x Int
0) (Expr Src Void -> Expr Src Void)
-> Context (Expr Src Void) -> Context (Expr Src Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text
-> Expr Src Void
-> Context (Expr Src Void)
-> Context (Expr Src Void)
forall a. Text -> a -> Context a -> Context a
insert Text
x Expr Src Void
forall s a. Expr s a
holeExpr Context (Expr Src Void)
values

    in Context (Expr Src Void)
-> Context (Expr Src Void) -> Expr Src Void -> CompletionContext
buildCompletionContext' Context (Expr Src Void)
context' Context (Expr Src Void)
values' Expr Src Void
b

buildCompletionContext' Context (Expr Src Void)
context Context (Expr Src Void)
values (Pi Maybe CharacterSet
_ Text
x Expr Src Void
_A Expr Src Void
b) =
  let _A' :: Expr t Void
_A' | Right Expr Src Void
_ <- Typer Void
-> Context (Expr Src Void)
-> Expr Src Void
-> Either (TypeError Src Void) (Expr Src Void)
forall a s.
(Eq a, Pretty a) =>
Typer a
-> Context (Expr s a)
-> Expr s a
-> Either (TypeError s a) (Expr s a)
typeWithA forall a. Void -> a
Typer Void
absurd Context (Expr Src Void)
context Expr Src Void
_A = Expr Src Void -> Expr t Void
forall a s t. Eq a => Expr s a -> Expr t a
normalize Expr Src Void
_A
          | Bool
otherwise = Expr t Void
forall s a. Expr s a
holeExpr

      context' :: Context (Expr Src Void)
context' = Int -> Var -> Expr Src Void -> Expr Src Void
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
1 (Text -> Int -> Var
V Text
x Int
0) (Expr Src Void -> Expr Src Void)
-> Context (Expr Src Void) -> Context (Expr Src Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text
-> Expr Src Void
-> Context (Expr Src Void)
-> Context (Expr Src Void)
forall a. Text -> a -> Context a -> Context a
insert Text
x Expr Src Void
forall t. Expr t Void
_A' Context (Expr Src Void)
context
      values' :: Context (Expr Src Void)
values' = Int -> Var -> Expr Src Void -> Expr Src Void
forall s a. Int -> Var -> Expr s a -> Expr s a
shift Int
1 (Text -> Int -> Var
V Text
x Int
0) (Expr Src Void -> Expr Src Void)
-> Context (Expr Src Void) -> Context (Expr Src Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text
-> Expr Src Void
-> Context (Expr Src Void)
-> Context (Expr Src Void)
forall a. Text -> a -> Context a -> Context a
insert Text
x Expr Src Void
forall s a. Expr s a
holeExpr Context (Expr Src Void)
values

    in Context (Expr Src Void)
-> Context (Expr Src Void) -> Expr Src Void -> CompletionContext
buildCompletionContext' Context (Expr Src Void)
context' Context (Expr Src Void)
values' Expr Src Void
b

-- catch-all
buildCompletionContext' Context (Expr Src Void)
context Context (Expr Src Void)
values Expr Src Void
_ = Context (Expr Src Void)
-> Context (Expr Src Void) -> CompletionContext
CompletionContext Context (Expr Src Void)
context Context (Expr Src Void)
values

-- Helper. Given `Dhall.Context.toList ctx` construct the corresponding variable
-- names.
contextToVariables :: [(Text, Expr Src Void)] -> [Var]
contextToVariables :: [(Text, Expr Src Void)] -> [Var]
contextToVariables  [] = []
contextToVariables ((Text
name, Expr Src Void
_) : [(Text, Expr Src Void)]
rest) =
  Text -> Int -> Var
V Text
name Int
0 Var -> [Var] -> [Var]
forall a. a -> [a] -> [a]
: (Var -> Var) -> [Var] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Text -> Var -> Var
inc Text
name) ([(Text, Expr Src Void)] -> [Var]
contextToVariables [(Text, Expr Src Void)]
rest)
 where inc :: Text -> Var -> Var
inc Text
x (V Text
y Int
i) | Text
x Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
y = Text -> Int -> Var
V Text
x (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                     | Bool
otherwise = Text -> Int -> Var
V Text
y Int
i

-- | Complete identifiers from the given completion context.
completeFromContext :: CompletionContext -> [Completion]
completeFromContext :: CompletionContext -> [Completion]
completeFromContext (CompletionContext Context (Expr Src Void)
context Context (Expr Src Void)
_) =
  let context' :: [(Text, Expr Src Void)]
context' = Context (Expr Src Void) -> [(Text, Expr Src Void)]
forall a. Context a -> [(Text, a)]
toList Context (Expr Src Void)
context
      completeReserved :: Text -> Completion
completeReserved Text
keyword
        | Right Expr Src Import
expr <- [Char] -> Text -> Either ParseError (Expr Src Import)
exprFromText [Char]
"" Text
keyword
        , Right Expr Src Void
typ <- Expr Src Void -> Either (TypeError Src Void) (Expr Src Void)
forall s. Expr s Void -> Either (TypeError s Void) (Expr s Void)
typeOf (do Import
_ <- Expr Src Import
expr; Expr Src Void
forall s a. Expr s a
holeExpr) =
          Text -> Maybe (Expr Src Void) -> Completion
Completion Text
keyword (Expr Src Void -> Maybe (Expr Src Void)
forall a. a -> Maybe a
Just Expr Src Void
typ)
        | Bool
otherwise = Text -> Maybe (Expr Src Void) -> Completion
Completion Text
keyword Maybe (Expr Src Void)
forall a. Maybe a
Nothing
      reserved :: [Completion]
reserved = (Text -> Completion) -> [Text] -> [Completion]
forall a b. (a -> b) -> [a] -> [b]
map Text -> Completion
completeReserved ([Text] -> [Completion]) -> [Text] -> [Completion]
forall a b. (a -> b) -> a -> b
$ HashSet Text -> [Text]
forall a. HashSet a -> [a]
HashSet.toList HashSet Text
reservedIdentifiers
  in [ Text -> Maybe (Expr Src Void) -> Completion
Completion (Var -> Text
forall a. Pretty a => a -> Text
pretty Var
var) (if Expr Src Void
typ Expr Src Void -> Expr Src Void -> Bool
forall a. Eq a => a -> a -> Bool
== Expr Src Void
forall s a. Expr s a
holeExpr then Maybe (Expr Src Void)
forall a. Maybe a
Nothing else Expr Src Void -> Maybe (Expr Src Void)
forall a. a -> Maybe a
Just Expr Src Void
typ)
     | (Var
var, (Text
_, Expr Src Void
typ)) <- [Var] -> [(Text, Expr Src Void)] -> [(Var, (Text, Expr Src Void))]
forall a b. [a] -> [b] -> [(a, b)]
zip ([(Text, Expr Src Void)] -> [Var]
contextToVariables [(Text, Expr Src Void)]
context') [(Text, Expr Src Void)]
context' ]
     [Completion] -> [Completion] -> [Completion]
forall a. [a] -> [a] -> [a]
++ [Completion]
reserved

-- | Complete union constructors and record projections.
completeProjections :: CompletionContext -> Expr Src Void -> [Completion]
completeProjections :: CompletionContext -> Expr Src Void -> [Completion]
completeProjections (CompletionContext Context (Expr Src Void)
context Context (Expr Src Void)
values) Expr Src Void
expr =
  -- substitute 'dependent lets', necessary for completion of unions
  let values' :: [(Text, Expr Src Void)]
values' = Context (Expr Src Void) -> [(Text, Expr Src Void)]
forall a. Context a -> [(Text, a)]
toList Context (Expr Src Void)
values
      subs :: [(Var, Expr Src Void)]
subs = ((Var, Expr Src Void) -> Bool)
-> [(Var, Expr Src Void)] -> [(Var, Expr Src Void)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Expr Src Void -> Expr Src Void -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr Src Void
forall s a. Expr s a
holeExpr) (Expr Src Void -> Bool)
-> ((Var, Expr Src Void) -> Expr Src Void)
-> (Var, Expr Src Void)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Expr Src Void) -> Expr Src Void
forall a b. (a, b) -> b
snd) ([(Var, Expr Src Void)] -> [(Var, Expr Src Void)])
-> [(Var, Expr Src Void)] -> [(Var, Expr Src Void)]
forall a b. (a -> b) -> a -> b
$ [Var] -> [Expr Src Void] -> [(Var, Expr Src Void)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([(Text, Expr Src Void)] -> [Var]
contextToVariables [(Text, Expr Src Void)]
values') (((Text, Expr Src Void) -> Expr Src Void)
-> [(Text, Expr Src Void)] -> [Expr Src Void]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Expr Src Void) -> Expr Src Void
forall a b. (a, b) -> b
snd [(Text, Expr Src Void)]
values')
      expr' :: Expr Src Void
expr' = (Expr Src Void -> (Var, Expr Src Void) -> Expr Src Void)
-> Expr Src Void -> [(Var, Expr Src Void)] -> Expr Src Void
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Expr Src Void
e (Var
x,Expr Src Void
val) -> Var -> Expr Src Void -> Expr Src Void -> Expr Src Void
forall s a. Var -> Expr s a -> Expr s a -> Expr s a
subst Var
x Expr Src Void
val Expr Src Void
e) Expr Src Void
expr [(Var, Expr Src Void)]
subs

  in case Typer Void
-> Context (Expr Src Void)
-> Expr Src Void
-> Either (TypeError Src Void) (Expr Src Void)
forall a s.
(Eq a, Pretty a) =>
Typer a
-> Context (Expr s a)
-> Expr s a
-> Either (TypeError s a) (Expr s a)
typeWithA forall a. Void -> a
Typer Void
absurd Context (Expr Src Void)
context Expr Src Void
expr' of
      Left TypeError Src Void
_ -> []
      Right Expr Src Void
_A ->
        let expr'' :: Expr t Void
expr'' = Expr Src Void -> Expr t Void
forall a s t. Eq a => Expr s a -> Expr t a
normalize Expr Src Void
expr'
        in Expr Src Void -> Expr Src Void -> [Completion]
completeUnion Expr Src Void
forall t. Expr t Void
expr'' Expr Src Void
forall t. Expr t Void
expr'' [Completion] -> [Completion] -> [Completion]
forall a. [a] -> [a] -> [a]
++ Expr Src Void -> [Completion]
completeRecord (Expr Src Void -> Expr Src Void
forall a s t. Eq a => Expr s a -> Expr t a
normalize Expr Src Void
_A)

 where
  -- complete a union constructor by inspecting the union value
  completeUnion :: Expr Src Void -> Expr Src Void -> [Completion]
completeUnion Expr Src Void
_A (Union Map Text (Maybe (Expr Src Void))
m) =
    let constructor :: (Text, Maybe (Expr Src Void)) -> Completion
constructor (Text
k, Maybe (Expr Src Void)
Nothing) =
            Text -> Maybe (Expr Src Void) -> Completion
Completion (Bool -> Text -> Text
Dhall.Pretty.escapeLabel Bool
True Text
k) (Expr Src Void -> Maybe (Expr Src Void)
forall a. a -> Maybe a
Just Expr Src Void
_A)
        constructor (Text
k, Just Expr Src Void
v) =
            Text -> Maybe (Expr Src Void) -> Completion
Completion (Bool -> Text -> Text
Dhall.Pretty.escapeLabel Bool
True Text
k) (Expr Src Void -> Maybe (Expr Src Void)
forall a. a -> Maybe a
Just (Maybe CharacterSet
-> Text -> Expr Src Void -> Expr Src Void -> Expr Src Void
forall s a.
Maybe CharacterSet -> Text -> Expr s a -> Expr s a -> Expr s a
Pi Maybe CharacterSet
forall a. Monoid a => a
mempty Text
k Expr Src Void
v Expr Src Void
_A))
     in ((Text, Maybe (Expr Src Void)) -> Completion)
-> [(Text, Maybe (Expr Src Void))] -> [Completion]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Maybe (Expr Src Void)) -> Completion
constructor (Map Text (Maybe (Expr Src Void)) -> [(Text, Maybe (Expr Src Void))]
forall k v. Ord k => Map k v -> [(k, v)]
Dhall.Map.toList Map Text (Maybe (Expr Src Void))
m)
  completeUnion Expr Src Void
_ Expr Src Void
_ = []


  -- complete a record projection by inspecting the record type
  completeRecord :: Expr Src Void -> [Completion]
completeRecord (Record Map Text (RecordField Src Void)
m) = ((Text, Expr Src Void) -> Completion)
-> [(Text, Expr Src Void)] -> [Completion]
forall a b. (a -> b) -> [a] -> [b]
map (Text, Expr Src Void) -> Completion
toCompletion (Map Text (Expr Src Void) -> [(Text, Expr Src Void)]
forall k v. Ord k => Map k v -> [(k, v)]
Dhall.Map.toList (Map Text (Expr Src Void) -> [(Text, Expr Src Void)])
-> Map Text (Expr Src Void) -> [(Text, Expr Src Void)]
forall a b. (a -> b) -> a -> b
$ RecordField Src Void -> Expr Src Void
forall s a. RecordField s a -> Expr s a
recordFieldValue (RecordField Src Void -> Expr Src Void)
-> Map Text (RecordField Src Void) -> Map Text (Expr Src Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Text (RecordField Src Void)
m)
    where
      toCompletion :: (Text, Expr Src Void) -> Completion
toCompletion (Text
name, Expr Src Void
typ) =
          Text -> Maybe (Expr Src Void) -> Completion
Completion (Bool -> Text -> Text
Dhall.Pretty.escapeLabel Bool
True Text
name) (Expr Src Void -> Maybe (Expr Src Void)
forall a. a -> Maybe a
Just Expr Src Void
typ)
  completeRecord Expr Src Void
_ = []