dhall-lsp-server: Type on hover (#1008)

* Type on Hover 1/2: Backend

Adds a function typeAt that, given an annotated expression and a text
position finds the type of the subexpression at that position.

* Type on Hover 2/2: Frontend

Exposes the new type-on-hover functionality as part of the hover
handler.

* Simplify explainDiagnosis

As suggested by @Gabriel439

* Simplify `inside`

Adressing @Gabriel439's comment.

* Simplify typeAt' by assuming well-typedness

* Simply srcAt

Use choice operator `<|>` instead of case distinction

dhall-lsp-server/dhall-lsp-server.cabal

@@ -25,6 +25,7 @@ library
       Dhall.LSP.Backend.Formatting
       Dhall.LSP.Backend.Linting
       Dhall.LSP.Backend.ToJSON
+      Dhall.LSP.Backend.Typing
       Dhall.LSP.Handlers
       Dhall.LSP.Handlers.Command
       Dhall.LSP.Handlers.Diagnostics

dhall-lsp-server/src/Dhall/LSP/Backend/Dhall.hs

@@ -1,6 +1,7 @@
 module Dhall.LSP.Backend.Dhall where
 
-import Dhall.Parser (Src(..))
+import Dhall.Import (loadWith, emptyStatus)
+import Dhall.Parser (Src, exprFromText)
 import Dhall.TypeCheck (X)
 import Dhall.Core (Expr)
 import Dhall
@@ -10,6 +11,7 @@ import Data.Text (Text)
 import System.FilePath (splitFileName)
 import Lens.Family (set)
 import Control.Exception (handle, SomeException)
+import Control.Monad.Trans.State.Strict (evalStateT)
 
 runDhall :: FilePath -> Text -> IO (Expr Src X)
 runDhall path = inputExprWithSettings dhallparams
@@ -21,3 +23,12 @@ runDhall path = inputExprWithSettings dhallparams
 runDhallSafe :: FilePath -> Text -> IO (Maybe (Expr Src X))
 runDhallSafe path text = handle (\(_ :: SomeException) -> return Nothing)
                                 (Just <$> runDhall path text)
+
+loadDhallExprSafe :: FilePath -> Text -> IO (Maybe (Expr Src X))
+loadDhallExprSafe filePath txt =
+  case exprFromText filePath txt of
+    Right expr ->
+      let (dir, _) = splitFileName filePath
+      in handle (\(_ :: SomeException) -> return Nothing)
+                (Just <$> evalStateT (loadWith expr) (emptyStatus dir))
+    Left _ -> return Nothing

dhall-lsp-server/src/Dhall/LSP/Backend/Diagnostics.hs

@@ -4,11 +4,15 @@ module Dhall.LSP.Backend.Diagnostics
   ( DhallException
   , checkDhall
   , diagnose
-  , explain
-  , rangeFromDhall
-  , Position
-  , Range(..)
   , Diagnosis(..)
+  , explain
+  , offsetToPosition
+  , Position
+  , positionFromMegaparsec
+  , positionToOffset
+  , Range(..)
+  , rangeFromDhall
+  , sanitiseRange
   )
 where
 

dhall-lsp-server/src/Dhall/LSP/Backend/Typing.hs

@@ -0,0 +1,75 @@
+module Dhall.LSP.Backend.Typing (typeAt, srcAt) where
+
+import Dhall.Context (Context, insert, empty)
+import Dhall.Core (Expr(..), Binding(..), subExpressions, normalize, shift, Var(..))
+import Dhall.TypeCheck (typeWithA, X(..), TypeError(..))
+import Dhall.Parser (Src(..))
+
+import Data.List.NonEmpty (NonEmpty (..))
+import Control.Lens (toListOf)
+import qualified Data.Text as Text
+import Control.Applicative ((<|>))
+
+import Dhall.LSP.Backend.Diagnostics (Position, positionFromMegaparsec, offsetToPosition)
+
+-- | Find the type of the subexpression at the given position. Assumes that the
+--   input expression is well-typed.
+typeAt :: Position -> Expr Src X -> Maybe (Expr Src X)
+typeAt pos expr = case typeAt' pos empty expr of
+  Right typ -> Just typ
+  _        -> Nothing
+
+typeAt' :: Position -> Context (Expr Src X) -> Expr Src X -> Either (TypeError Src X) (Expr Src X)
+-- unfold lets to make things simpler
+-- need to match on outer Note to recover the range
+typeAt' pos ctx (Note src (Let (b :| (b' : bs)) e)) =
+  typeAt' pos ctx (Note src (Let (b :| []) (Note src (Let (b' :| bs) e))))
+
+-- only handle singleton lets explicitly
+typeAt' pos ctx (Let (Binding x _ a :| []) (Note src e)) | pos `inside` src = do
+  _A <- typeWithA absurd ctx a
+  let ctx' = fmap (shift 1 (V x 0)) (insert x _A ctx)
+  typeAt' pos ctx' e
+
+typeAt' pos ctx (Lam x _A (Note src b)) | 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  (Note src _B)) | 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
+
+-- need to catch Notes since the catch-all would remove two layers at once
+typeAt' pos ctx (Note _ expr) = typeAt' pos ctx expr
+
+-- catch-all
+typeAt' pos ctx expr = do
+  let subExprs = toListOf subExpressions expr
+  case [ e | (Note src e) <- subExprs, pos `inside` src ] of
+    [] -> typeWithA absurd ctx expr  -- return type of whole subexpression
+    (t:_) -> typeAt' pos ctx t  -- continue with leaf-expression
+
+
+-- | Find the smallest Src annotation containing the given position.
+srcAt :: Position -> Expr Src X -> Maybe Src
+srcAt pos (Note src expr) = srcAt pos expr <|> Just src
+srcAt pos expr =
+  let subExprs = toListOf subExpressions expr
+  in case [ (src, e) | (Note src e) <- subExprs, pos `inside` src ] of
+    [] -> Nothing
+    ((src, e) : _) -> srcAt pos e <|> Just src
+
+
+-- Check if range lies completely inside a given subexpression.
+-- This version takes trailing whitespace into account
+-- (c.f. `sanitiseRange` from Backend.Diangostics).
+inside :: Position -> Src -> Bool
+inside pos (Src left _right txt) =
+  let (x1,y1) = positionFromMegaparsec left
+      txt' = Text.stripEnd txt
+      (dx2,dy2) = (offsetToPosition txt . Text.length) txt'
+      (x2,y2) | dx2 == 0 = (x1, y1 + dy2)
+              | otherwise = (x1 + dx2, dy2)
+  in (x1,y1) <= pos && pos < (x2,y2)

dhall-lsp-server/src/Dhall/LSP/Handlers/Diagnostics.hs

@@ -1,7 +1,7 @@
 {-| This module contains everything related to how the LSP server handles
     diagnostic messages. -}
 module Dhall.LSP.Handlers.Diagnostics
-  ( diagnosticsHandler
+  ( diagnosticsHandler, explainDiagnosis
   )
 where
 
@@ -16,6 +16,8 @@ import           Dhall.LSP.Backend.Diagnostics
 import           Dhall.LSP.Backend.Linting
 import           Dhall.LSP.Util (readUri)
 
+import           Data.List                      ( find )
+import           Data.Maybe                     ( mapMaybe )
 
 -- | Called by @didOpenTextDocumentNotificationHandler@ and
 --   @didSaveTextDocumentNotificationHandler@.
@@ -61,6 +63,17 @@ suggestionToDiagnostic Suggestion {..} = J.Diagnostic {..}
     _message = suggestion
     _relatedInformation = Nothing
 
+explainDiagnosis :: FilePath -> Text -> Position -> IO (Maybe Diagnosis)
+explainDiagnosis path txt pos = do
+  errors <- checkDhall path txt
+  let explanations = mapMaybe (explain txt) errors
+  return $ find (isHovered pos) explanations
+
+isHovered :: Position -> Diagnosis -> Bool
+isHovered _ (Diagnosis _ Nothing _) = False
+isHovered pos (Diagnosis _ (Just (Range left right)) _) =
+  left <= pos && pos <= right
+
 -- | Compute the list of possible improvements, as would be carried out by
 --   @Dhall.Lint@.
 linterDiagnostics :: Text -> [J.Diagnostic]

dhall-lsp-server/src/Dhall/LSP/Handlers/Hover.hs

@@ -7,39 +7,58 @@ import qualified Language.Haskell.LSP.Utility as LSP
 import qualified Language.Haskell.LSP.Types as J
 import qualified Language.Haskell.LSP.Types.Lens as J
 
+import Dhall.Core (pretty)
+
+import Dhall.LSP.Backend.Dhall
 import Dhall.LSP.Backend.Diagnostics
+import Dhall.LSP.Handlers.Diagnostics (explainDiagnosis)
+import Dhall.LSP.Backend.Typing
 import Dhall.LSP.Util (readUri)
 
 import Control.Lens ((^.))
 import qualified Network.URI.Encode as URI
 import qualified Data.Text as Text
-import Data.Maybe (mapMaybe)
 
 -- | This is a prototype implementation. We should avoid recomputing the
 -- diagnostics each time.
 hoverHandler :: LSP.LspFuncs () -> J.HoverRequest -> IO ()
 hoverHandler lsp request = do
   LSP.logs "LSP Handler: processing HoverRequest"
-  let
-    uri = request ^. J.params . J.textDocument . J.uri
-    (J.Position line col) = request ^. (J.params . J.position)
-    fileName = case J.uriToFilePath uri of
-      Nothing -> fail "Failed to parse URI in ReqHover."
-      Just path -> path
+  let uri = request ^. J.params . J.textDocument . J.uri
+      (J.Position line col) = request ^. (J.params . J.position)
+      pos = (line, col)
+      fileName = case J.uriToFilePath uri of
+        Nothing -> fail "Failed to parse URI in ReqHover."
+        Just path -> path
   txt <- readUri lsp uri
-  errors <- checkDhall fileName txt
-  let
-    explanations = mapMaybe (explain txt) errors
-    isHovered :: Diagnosis -> Bool
-    isHovered (Diagnosis _ Nothing _) = False
-    isHovered (Diagnosis _ (Just (Range left right)) _) =
-      left <= (line, col) && (line, col) <= right
-    hover = case filter isHovered explanations of
-      [] -> Nothing
-      (diag : _) -> hoverFromDiagnosis diag
-  LSP.sendFunc lsp $ LSP.RspHover $ LSP.makeResponseMessage request hover
+  -- Explain takes priority
+  mexplain <- explainDiagnosis fileName txt (line, col)
+  case mexplain of
+    Just explanation -> LSP.sendFunc lsp
+                         $ LSP.RspHover
+                         $ LSP.makeResponseMessage
+                           request (hoverFromDiagnosis explanation)
+    Nothing -> do  -- infer type
+      mexpr <- loadDhallExprSafe fileName txt
+      case mexpr of
+        Nothing -> LSP.sendFunc lsp $ LSP.RspHover
+                                    $ LSP.makeResponseMessage request Nothing
+        Just expr ->
+          case typeAt pos expr of
+            Just typ ->
+              let _range = fmap (rangeToJSON . sanitiseRange txt . rangeFromDhall)
+                                (srcAt pos expr)
+                  _contents = J.List [J.PlainString (pretty typ)]
+                  hover = J.Hover{..}
+              in LSP.sendFunc lsp $ LSP.RspHover
+                                  $ LSP.makeResponseMessage request (Just hover)
+            Nothing -> LSP.sendFunc lsp $ LSP.RspHover
+                                        $ LSP.makeResponseMessage request Nothing
 
 
+rangeToJSON :: Range -> J.Range
+rangeToJSON (Range (x1,y1) (x2,y2)) = J.Range (J.Position x1 y1) (J.Position x2 y2)
+
 hoverFromDiagnosis :: Diagnosis -> Maybe J.Hover
 hoverFromDiagnosis (Diagnosis _ Nothing _) = Nothing
 hoverFromDiagnosis (Diagnosis _ (Just (Range left right)) diagnosis) = Just