module Dhall.LSP.Backend.Typing (annotateLet, exprAt, srcAt, typeAt) where
import Dhall.Context (Context, insert, empty)
import Dhall.Core (Binding(..), Expr(..), subExpressions, normalize, shift, subst, Var(..), pretty)
import Dhall.TypeCheck (typeWithA, X, TypeError(..))
import Dhall.Parser (Src(..))
import Data.Monoid ((<>))
import Control.Lens (toListOf)
import Data.Text (Text)
import Control.Applicative ((<|>))
import Data.Bifunctor (first)
import Data.Void (absurd)
import Dhall.LSP.Backend.Parsing (getLetAnnot, getLetIdentifier,
getLamIdentifier, getForallIdentifier)
import Dhall.LSP.Backend.Diagnostics (Position, Range(..), rangeFromDhall)
import Dhall.LSP.Backend.Dhall (WellTyped, fromWellTyped)
typeAt :: Position -> WellTyped -> Either String (Maybe Src, Expr Src X)
typeAt pos expr = do
let expr' = fromWellTyped expr
(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 { value = a }) _)) | pos `inside` getLetIdentifier src = do
typ <- typeWithA absurd ctx a
return (Just $ getLetIdentifier src, typ)
typeAt' pos _ctx (Note src (Lam _ _A _)) | Just src' <- getLamIdentifier src
, pos `inside` src' =
return (Just src', _A)
typeAt' pos _ctx (Note src (Pi _ _A _)) | Just src' <- getForallIdentifier src
, pos `inside` src' =
return (Just src', _A)
typeAt' pos ctx (Let (Binding { variable = x, value = a }) e@(Note src _)) | pos `inside` src = do
_ <- typeWithA absurd ctx a
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@(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
annotateLet' pos empty (fromWellTyped expr)
annotateLet' :: Position -> Context (Expr Src X) -> Expr Src X -> Either String (Src, Text)
annotateLet' pos ctx (Note src e@(Let (Binding { value = 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, ": " <> pretty (normalize _A) <> " ")
annotateLet' pos ctx (Let (Binding { variable = x, value = a }) e@(Note src _)) | pos `inside` src = do
_ <- first show $ typeWithA absurd ctx a
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!"
inside :: Position -> Src -> Bool
inside pos src = left <= pos && pos < right
where Range left right = rangeFromDhall src