Skip to content

Commit

Permalink
Improve rendering of types when annotating lets (#1222)
Browse files Browse the repository at this point in the history
Previously the annotated type would have too many line-breaks, e.g. when
the result of annotating
  let id = \(A : Type) -> \(a : A) -> a
was
  let id :   ∀ ( A
  : Type
  )
  → ∀ ( a
  : A
  )
  → A = \(A : Type) -> \(a : A) -> a
while it should be
  let id : ∀(A : Type) → ∀(a : A) → A = \(A : Type) -> \(a : A) -> a
  • Loading branch information
EggBaconAndSpam authored and mergify[bot] committed Aug 8, 2019
1 parent c2cc641 commit 4c1736b
Showing 1 changed file with 2 additions and 10 deletions.
12 changes: 2 additions & 10 deletions dhall-lsp-server/src/Dhall/LSP/Backend/Typing.hs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
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.Core (Expr(..), Binding(..), Const(..), subExpressions, normalize, shift, subst, Var(..), pretty)
import Dhall.TypeCheck (typeWithA, X, TypeError(..))
import Dhall.Parser (Src(..))

Expand All @@ -18,10 +18,6 @@ import Dhall.LSP.Backend.Parsing (getLetInner, getLetAnnot, getLetIdentifier,
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)

-- | Find the type of the subexpression at the given position. Assumes that the
-- input expression is well-typed. Also returns the Src descriptor containing
-- that subexpression if possible.
Expand Down Expand Up @@ -126,7 +122,7 @@ annotateLet' pos ctx (Note src e@(Let (Binding _ _ a :| []) _))
Just x -> return x
Nothing -> Left "The impossible happened: failed\
\ to re-parse a Let expression."
return (srcAnnot, ": " <> printExpr (normalize _A) <> " ")
return (srcAnnot, ": " <> pretty (normalize _A) <> " ")

-- binders, see typeAt'
annotateLet' pos ctx (Let (Binding x _ a :| []) e@(Note src _)) | pos `inside` src = do
Expand Down Expand Up @@ -162,10 +158,6 @@ annotateLet' pos ctx expr = do
_ -> 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))


-- Split all multilets into single lets in an expression
splitLets :: Expr Src a -> Maybe (Expr Src a)
splitLets (Note src (Let (b :| (b' : bs)) e)) = do
Expand Down

0 comments on commit 4c1736b

Please sign in to comment.