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
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'
data Completion =
Completion {
Completion -> Text
completeText :: Text,
Completion -> Maybe (Expr Src Void)
completeType :: Maybe (Expr Src Void) }
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)
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 []
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)
data CompletionContext =
CompletionContext {
CompletionContext -> Context (Expr Src Void)
context :: Context (Expr Src Void),
CompletionContext -> Context (Expr Src Void)
values :: Context (Expr Src Void) }
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)
| 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'
| 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
| 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
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
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
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
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 =
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
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
_ = []
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
_ = []