module Dhall.LSP.Backend.Typing (annotateLet, exprAt, srcAt, typeAt) where
import Dhall.Context (Context, insert, empty)
import Dhall.Core (Expr(..), Binding(..), Const(..), subExpressions, normalize, shift, subst, Var(..))
import Dhall.TypeCheck (typeWithA, X(..), TypeError(..))
import Dhall.Parser (Src(..))
import Data.List.NonEmpty (NonEmpty (..))
import Data.Monoid ((<>))
import Control.Lens (toListOf)
import Data.Text (Text)
import Control.Applicative ((<|>))
import Data.Bifunctor (first)
import Dhall.LSP.Backend.Parsing (getLetInner, getLetAnnot, getLetIdentifier,
getLamIdentifier, getForallIdentifier)
import Dhall.LSP.Backend.Diagnostics (Position, Range(..), rangeFromDhall)
import Dhall.LSP.Backend.Dhall (WellTyped, fromWellTyped)
import qualified Data.Text.Prettyprint.Doc as Pretty
import qualified Data.Text.Prettyprint.Doc.Render.Text as Pretty
import Dhall.Pretty (CharacterSet(..), prettyCharacterSet)
typeAt :: Position -> WellTyped -> Either String (Maybe Src, Expr Src X)
typeAt pos expr = do
expr' <- case splitLets (fromWellTyped expr) of
Just e -> return e
Nothing -> Left "The impossible happened: failed to split let\
\ blocks when preprocessing for typeAt'."
(mSrc, typ) <- first show $ typeAt' pos empty expr'
case mSrc of
Just src -> return (Just src, normalize typ)
Nothing -> return (srcAt pos expr', normalize typ)
typeAt' :: Position -> Context (Expr Src X) -> Expr Src X -> Either (TypeError Src X) (Maybe Src, Expr Src X)
typeAt' pos ctx (Note src (Let (Binding _ _ a :| []) _)) | pos `inside` getLetIdentifier src = do
typ <- typeWithA absurd ctx a
return (Just $ getLetIdentifier src, typ)
typeAt' pos _ctx (Note src (Lam _ _A _)) | pos `inside` getLamIdentifier src =
return (Just $ getLamIdentifier src, _A)
typeAt' pos _ctx (Note src (Pi _ _A _)) | pos `inside` getForallIdentifier src =
return (Just $ getForallIdentifier src, _A)
typeAt' pos ctx (Let (Binding x _ a :| []) e@(Note src _)) | pos `inside` src = do
_A <- typeWithA absurd ctx a
t <- fmap normalize (typeWithA absurd ctx _A)
case t of
Const Type -> do
let ctx' = fmap (shift 1 (V x 0)) (insert x (normalize _A) ctx)
(mSrc, _B) <- typeAt' pos ctx' e
return (mSrc, shift (-1) (V x 0) _B)
_ -> do
let a' = shift 1 (V x 0) (normalize a)
typeAt' pos ctx (shift (-1) (V x 0) (subst (V x 0) a' e))
typeAt' pos ctx (Lam x _A b@(Note src _)) | pos `inside` src = do
let _A' = Dhall.Core.normalize _A
ctx' = fmap (shift 1 (V x 0)) (insert x _A' ctx)
typeAt' pos ctx' b
typeAt' pos ctx (Pi x _A _B@(Note src _)) | pos `inside` src = do
let _A' = Dhall.Core.normalize _A
ctx' = fmap (shift 1 (V x 0)) (insert x _A' ctx)
typeAt' pos ctx' _B
typeAt' pos ctx (Note _ expr) = typeAt' pos ctx expr
typeAt' pos ctx expr = do
let subExprs = toListOf subExpressions expr
case [ (src, e) | (Note src e) <- subExprs, pos `inside` src ] of
[] -> do typ <- typeWithA absurd ctx expr
return (Nothing, typ)
((src, e):_) -> typeAt' pos ctx (Note src e)
exprAt :: Position -> Expr Src a -> Maybe (Expr Src a)
exprAt pos e = do e' <- splitLets e
exprAt' pos e'
exprAt' :: Position -> Expr Src a -> Maybe (Expr Src a)
exprAt' pos e@(Note _ expr) = exprAt pos expr <|> Just e
exprAt' pos expr =
let subExprs = toListOf subExpressions expr
in case [ (src, e) | (Note src e) <- subExprs, pos `inside` src ] of
[] -> Nothing
((src,e) : _) -> exprAt' pos e <|> Just (Note src e)
srcAt :: Position -> Expr Src a -> Maybe Src
srcAt pos expr = do Note src _ <- exprAt pos expr
return src
annotateLet :: Position -> WellTyped -> Either String (Src, Text)
annotateLet pos expr = do
expr' <- case splitLets (fromWellTyped expr) of
Just e -> return e
Nothing -> Left "The impossible happened: failed to split let\
\ blocks when preprocessing for annotateLet'."
annotateLet' pos empty expr'
annotateLet' :: Position -> Context (Expr Src X) -> Expr Src X -> Either String (Src, Text)
annotateLet' pos ctx (Note src e@(Let (Binding _ _ a :| []) _))
| not $ any (pos `inside`) [ src' | Note src' _ <- toListOf subExpressions e ]
= do _A <- first show $ typeWithA absurd ctx a
srcAnnot <- case getLetAnnot src of
Just x -> return x
Nothing -> Left "The impossible happened: failed\
\ to re-parse a Let expression."
return (srcAnnot, ": " <> printExpr (normalize _A) <> " ")
annotateLet' pos ctx (Let (Binding x _ a :| []) e@(Note src _)) | pos `inside` src = do
_A <- first show $ typeWithA absurd ctx a
t <- first show $ fmap normalize (typeWithA absurd ctx _A)
case t of
Const Type -> do
let ctx' = fmap (shift 1 (V x 0)) (insert x (normalize _A) ctx)
annotateLet' pos ctx' e
_ -> do
let a' = shift 1 (V x 0) (normalize a)
annotateLet' pos ctx (shift (-1) (V x 0) (subst (V x 0) a' e))
annotateLet' pos ctx (Lam x _A b@(Note src _)) | pos `inside` src = do
let _A' = Dhall.Core.normalize _A
ctx' = fmap (shift 1 (V x 0)) (insert x _A' ctx)
annotateLet' pos ctx' b
annotateLet' pos ctx (Pi x _A _B@(Note src _)) | pos `inside` src = do
let _A' = Dhall.Core.normalize _A
ctx' = fmap (shift 1 (V x 0)) (insert x _A' ctx)
annotateLet' pos ctx' _B
annotateLet' pos ctx (Note _ expr) = do
annotateLet' pos ctx expr
annotateLet' pos ctx expr = do
let subExprs = toListOf subExpressions expr
case [ Note src e | (Note src e) <- subExprs, pos `inside` src ] of
(e:[]) -> annotateLet' pos ctx e
_ -> Left "You weren't pointing at a let binder!"
printExpr :: Pretty.Pretty b => Expr a b -> Text
printExpr expr = Pretty.renderStrict $ Pretty.layoutCompact (Pretty.unAnnotate (prettyCharacterSet Unicode expr))
splitLets :: Expr Src a -> Maybe (Expr Src a)
splitLets (Note src (Let (b :| (b' : bs)) e)) = do
src' <- getLetInner src
splitLets (Note src (Let (b :| []) (Note src' (Let (b' :| bs) e))))
splitLets expr = subExpressions splitLets expr
inside :: Position -> Src -> Bool
inside pos src = left <= pos && pos < right
where Range left right = rangeFromDhall src