module Dhall.LSP.Backend.Typing (annotateLet, exprAt, srcAt, typeAt) where

import Dhall.Context   (Context, empty, insert)
import Dhall.Core
    ( Binding (..)
    , Expr (..)
    , FunctionBinding (..)
    , Var (..)
    , normalize
    , shift
    , subExpressions
    , subst
    )
import Dhall.Parser    (Src (..))
import Dhall.TypeCheck (TypeError (..), typeWithA)

import Control.Applicative ((<|>))
import Control.Lens        (toListOf)
import Data.Bifunctor      (first)
import Data.Void           (Void, absurd)

import Dhall.LSP.Backend.Dhall       (WellTyped, fromWellTyped)
import Dhall.LSP.Backend.Diagnostics (Position, Range (..), rangeFromDhall)
import Dhall.LSP.Backend.Parsing
    ( getForallIdentifier
    , getLamIdentifier
    , getLetAnnot
    , getLetIdentifier
    , getLetInner
    )

-- | 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.
typeAt :: Position -> WellTyped -> Either String (Maybe Src, Expr Src Void)
typeAt :: Position -> WellTyped -> Either String (Maybe Src, Expr Src Void)
typeAt Position
pos WellTyped
expr = do
  Expr Src Void
expr' <- case Expr Src Void -> Maybe (Expr Src Void)
forall a. Expr Src a -> Maybe (Expr Src a)
splitMultiLetSrc (WellTyped -> Expr Src Void
fromWellTyped WellTyped
expr) of
             Just Expr Src Void
e -> Expr Src Void -> Either String (Expr Src Void)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr Src Void
e
             Maybe (Expr Src Void)
Nothing -> String -> Either String (Expr Src Void)
forall a b. a -> Either a b
Left String
"The impossible happened: failed to split let\
                              \ blocks when preprocessing for typeAt'."
  (Maybe Src
mSrc, Expr Src Void
typ) <- (TypeError Src Void -> String)
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
-> Either String (Maybe Src, Expr Src Void)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TypeError Src Void -> String
forall a. Show a => a -> String
show (Either (TypeError Src Void) (Maybe Src, Expr Src Void)
 -> Either String (Maybe Src, Expr Src Void))
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
-> Either String (Maybe Src, Expr Src Void)
forall a b. (a -> b) -> a -> b
$ Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
typeAt' Position
pos Context (Expr Src Void)
forall a. Context a
empty Expr Src Void
expr'
  case Maybe Src
mSrc of
    Just Src
src -> (Maybe Src, Expr Src Void)
-> Either String (Maybe Src, Expr Src Void)
forall (m :: * -> *) a. Monad m => a -> m a
return (Src -> Maybe Src
forall a. a -> Maybe a
Just Src
src, Expr Src Void -> Expr Src Void
forall a s t. Eq a => Expr s a -> Expr t a
normalize Expr Src Void
typ)
    Maybe Src
Nothing -> (Maybe Src, Expr Src Void)
-> Either String (Maybe Src, Expr Src Void)
forall (m :: * -> *) a. Monad m => a -> m a
return (Position -> Expr Src Void -> Maybe Src
forall a. Position -> Expr Src a -> Maybe Src
srcAt Position
pos Expr Src Void
expr', Expr Src Void -> Expr Src Void
forall a s t. Eq a => Expr s a -> Expr t a
normalize Expr Src Void
typ)

typeAt' :: Position -> Context (Expr Src Void) -> Expr Src Void -> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
-- the user hovered over the bound name in a let expression
typeAt' :: Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
typeAt' Position
pos Context (Expr Src Void)
ctx (Note Src
src (Let (Binding { value :: forall s a. Binding s a -> Expr s a
value = Expr Src Void
a }) Expr Src Void
_)) | Position
pos Position -> Src -> Bool
`inside` Src -> Src
getLetIdentifier Src
src = do
  Expr Src Void
typ <- 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)
ctx Expr Src Void
a
  (Maybe Src, Expr Src Void)
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
forall (m :: * -> *) a. Monad m => a -> m a
return (Src -> Maybe Src
forall a. a -> Maybe a
Just (Src -> Maybe Src) -> Src -> Maybe Src
forall a b. (a -> b) -> a -> b
$ Src -> Src
getLetIdentifier Src
src, Expr Src Void
typ)

-- "..." in a lambda expression
typeAt' Position
pos Context (Expr Src Void)
_ctx (Note Src
src (Lam Maybe CharacterSet
_ FunctionBinding { functionBindingAnnotation :: forall s a. FunctionBinding s a -> Expr s a
functionBindingAnnotation = Expr Src Void
_A} Expr Src Void
_))
  | Just Src
src' <- Src -> Maybe Src
getLamIdentifier Src
src
  , Position
pos Position -> Src -> Bool
`inside` Src
src' =
  (Maybe Src, Expr Src Void)
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
forall (m :: * -> *) a. Monad m => a -> m a
return (Src -> Maybe Src
forall a. a -> Maybe a
Just Src
src', Expr Src Void
_A)

-- "..." in a forall expression
typeAt' Position
pos Context (Expr Src Void)
_ctx (Note Src
src (Pi Maybe CharacterSet
_ Text
_ Expr Src Void
_A Expr Src Void
_)) | Just Src
src' <- Src -> Maybe Src
getForallIdentifier Src
src
                                        , Position
pos Position -> Src -> Bool
`inside` Src
src' =
  (Maybe Src, Expr Src Void)
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
forall (m :: * -> *) a. Monad m => a -> m a
return (Src -> Maybe Src
forall a. a -> Maybe a
Just Src
src', Expr Src Void
_A)

typeAt' Position
pos Context (Expr Src Void)
ctx (Let (Binding { variable :: forall s a. Binding s a -> Text
variable = Text
x, value :: forall s a. Binding s a -> Expr s a
value = Expr Src Void
a }) e :: Expr Src Void
e@(Note Src
src Expr Src Void
_)) | Position
pos Position -> Src -> Bool
`inside` Src
src = do
  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)
ctx Expr Src Void
a
  let a' :: Expr s Void
a' = Int -> Var -> Expr s Void -> Expr s 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 s Void
forall a s t. Eq a => Expr s a -> Expr t a
normalize Expr Src Void
a)
  Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
typeAt' Position
pos Context (Expr Src Void)
ctx (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) (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 s. Expr s Void
a' Expr Src Void
e))

typeAt' Position
pos Context (Expr Src Void)
ctx (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} b :: Expr Src Void
b@(Note Src
src Expr Src Void
_))
  | Position
pos Position -> Src -> Bool
`inside` Src
src = do
      let _A' :: Expr t Void
_A' = Expr Src Void -> Expr t Void
forall a s t. Eq a => Expr s a -> Expr t a
Dhall.Core.normalize Expr Src Void
_A
          ctx' :: Context (Expr Src Void)
ctx' = (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
fmap (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)) (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. Expr s Void
_A' Context (Expr Src Void)
ctx)
      Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
typeAt' Position
pos Context (Expr Src Void)
ctx' Expr Src Void
b

typeAt' Position
pos Context (Expr Src Void)
ctx (Pi Maybe CharacterSet
_ Text
x Expr Src Void
_A  _B :: Expr Src Void
_B@(Note Src
src Expr Src Void
_)) | Position
pos Position -> Src -> Bool
`inside` Src
src = do
  let _A' :: Expr t Void
_A' = Expr Src Void -> Expr t Void
forall a s t. Eq a => Expr s a -> Expr t a
Dhall.Core.normalize Expr Src Void
_A
      ctx' :: Context (Expr Src Void)
ctx' = (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
fmap (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)) (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. Expr s Void
_A' Context (Expr Src Void)
ctx)
  Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
typeAt' Position
pos Context (Expr Src Void)
ctx' Expr Src Void
_B

-- peel off a single Note constructor
typeAt' Position
pos Context (Expr Src Void)
ctx (Note Src
_ Expr Src Void
expr) = Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
typeAt' Position
pos Context (Expr Src Void)
ctx Expr Src Void
expr

-- catch-all
typeAt' Position
pos Context (Expr Src Void)
ctx Expr Src Void
expr = do
  let subExprs :: [Expr Src Void]
subExprs = Getting (Endo [Expr Src Void]) (Expr Src Void) (Expr Src Void)
-> Expr Src Void -> [Expr Src Void]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [Expr Src Void]) (Expr Src Void) (Expr Src Void)
forall (f :: * -> *) s a.
Applicative f =>
(Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
subExpressions Expr Src Void
expr
  case [ (Src
src, Expr Src Void
e) | (Note Src
src Expr Src Void
e) <- [Expr Src Void]
subExprs, Position
pos Position -> Src -> Bool
`inside` Src
src ] of
    [] -> do Expr Src Void
typ <- 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)
ctx Expr Src Void
expr  -- return type of whole subexpression
             (Maybe Src, Expr Src Void)
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Src
forall a. Maybe a
Nothing, Expr Src Void
typ)
    ((Src
src, Expr Src Void
e):[(Src, Expr Src Void)]
_) -> Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either (TypeError Src Void) (Maybe Src, Expr Src Void)
typeAt' Position
pos Context (Expr Src Void)
ctx (Src -> Expr Src Void -> Expr Src Void
forall s a. s -> Expr s a -> Expr s a
Note Src
src Expr Src Void
e)  -- continue with leaf-expression


-- | Find the smallest Note-wrapped expression at the given position.
exprAt :: Position -> Expr Src a -> Maybe (Expr Src a)
exprAt :: Position -> Expr Src a -> Maybe (Expr Src a)
exprAt Position
pos Expr Src a
e = do Expr Src a
e' <- Expr Src a -> Maybe (Expr Src a)
forall a. Expr Src a -> Maybe (Expr Src a)
splitMultiLetSrc Expr Src a
e
                  Position -> Expr Src a -> Maybe (Expr Src a)
forall a. Position -> Expr Src a -> Maybe (Expr Src a)
exprAt' Position
pos Expr Src a
e'

exprAt' :: Position -> Expr Src a -> Maybe (Expr Src a)
exprAt' :: Position -> Expr Src a -> Maybe (Expr Src a)
exprAt' Position
pos e :: Expr Src a
e@(Note Src
_ Expr Src a
expr) = Position -> Expr Src a -> Maybe (Expr Src a)
forall a. Position -> Expr Src a -> Maybe (Expr Src a)
exprAt Position
pos Expr Src a
expr Maybe (Expr Src a) -> Maybe (Expr Src a) -> Maybe (Expr Src a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Expr Src a -> Maybe (Expr Src a)
forall a. a -> Maybe a
Just Expr Src a
e
exprAt' Position
pos Expr Src a
expr =
  let subExprs :: [Expr Src a]
subExprs = Getting (Endo [Expr Src a]) (Expr Src a) (Expr Src a)
-> Expr Src a -> [Expr Src a]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [Expr Src a]) (Expr Src a) (Expr Src a)
forall (f :: * -> *) s a.
Applicative f =>
(Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
subExpressions Expr Src a
expr
  in case [ (Src
src, Expr Src a
e) | (Note Src
src Expr Src a
e) <- [Expr Src a]
subExprs, Position
pos Position -> Src -> Bool
`inside` Src
src ] of
    [] -> Maybe (Expr Src a)
forall a. Maybe a
Nothing
    ((Src
src,Expr Src a
e) : [(Src, Expr Src a)]
_) -> Position -> Expr Src a -> Maybe (Expr Src a)
forall a. Position -> Expr Src a -> Maybe (Expr Src a)
exprAt' Position
pos Expr Src a
e Maybe (Expr Src a) -> Maybe (Expr Src a) -> Maybe (Expr Src a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Expr Src a -> Maybe (Expr Src a)
forall a. a -> Maybe a
Just (Src -> Expr Src a -> Expr Src a
forall s a. s -> Expr s a -> Expr s a
Note Src
src Expr Src a
e)


-- | Find the smallest Src annotation containing the given position.
srcAt :: Position -> Expr Src a -> Maybe Src
srcAt :: Position -> Expr Src a -> Maybe Src
srcAt Position
pos Expr Src a
expr = do Note Src
src Expr Src a
_ <- Position -> Expr Src a -> Maybe (Expr Src a)
forall a. Position -> Expr Src a -> Maybe (Expr Src a)
exprAt Position
pos Expr Src a
expr
                    Src -> Maybe Src
forall (m :: * -> *) a. Monad m => a -> m a
return Src
src


-- | Given a well-typed expression and a position find the let binder at that
--   position (if there is one) and return the type annotation to be inserted
--   (potentially replacing the existing one). If something goes wrong returns a
--   textual error message.
annotateLet :: Position -> WellTyped -> Either String (Src, Expr Src Void)
annotateLet :: Position -> WellTyped -> Either String (Src, Expr Src Void)
annotateLet Position
pos WellTyped
expr = do
  Expr Src Void
expr' <- case Expr Src Void -> Maybe (Expr Src Void)
forall a. Expr Src a -> Maybe (Expr Src a)
splitMultiLetSrc (WellTyped -> Expr Src Void
fromWellTyped WellTyped
expr) of
             Just Expr Src Void
e -> Expr Src Void -> Either String (Expr Src Void)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr Src Void
e
             Maybe (Expr Src Void)
Nothing -> String -> Either String (Expr Src Void)
forall a b. a -> Either a b
Left String
"The impossible happened: failed to split let\
                              \ blocks when preprocessing for annotateLet'."
  Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either String (Src, Expr Src Void)
annotateLet' Position
pos Context (Expr Src Void)
forall a. Context a
empty Expr Src Void
expr'


annotateLet' :: Position -> Context (Expr Src Void) -> Expr Src Void
             -> Either String (Src, Expr Src Void)
-- the input only contains singleton lets
annotateLet' :: Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either String (Src, Expr Src Void)
annotateLet' Position
pos Context (Expr Src Void)
ctx (Note Src
src e :: Expr Src Void
e@(Let (Binding { value :: forall s a. Binding s a -> Expr s a
value = Expr Src Void
a }) Expr Src Void
_))
  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Src -> Bool) -> [Src] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Position
pos Position -> Src -> Bool
`inside`) [ Src
src' | Note Src
src' Expr Src Void
_ <- Getting (Endo [Expr Src Void]) (Expr Src Void) (Expr Src Void)
-> Expr Src Void -> [Expr Src Void]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [Expr Src Void]) (Expr Src Void) (Expr Src Void)
forall (f :: * -> *) s a.
Applicative f =>
(Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
subExpressions Expr Src Void
e ]
  = do Expr Src Void
_A <- (TypeError Src Void -> String)
-> Either (TypeError Src Void) (Expr Src Void)
-> Either String (Expr Src Void)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TypeError Src Void -> String
forall a. Show a => a -> String
show (Either (TypeError Src Void) (Expr Src Void)
 -> Either String (Expr Src Void))
-> Either (TypeError Src Void) (Expr Src Void)
-> Either String (Expr Src Void)
forall a b. (a -> b) -> a -> b
$ 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)
ctx Expr Src Void
a
       Src
srcAnnot <- case Src -> Maybe Src
getLetAnnot Src
src of
                     Just Src
x -> Src -> Either String Src
forall (m :: * -> *) a. Monad m => a -> m a
return Src
x
                     Maybe Src
Nothing -> String -> Either String Src
forall a b. a -> Either a b
Left String
"The impossible happened: failed\
                                     \ to re-parse a Let expression."
       (Src, Expr Src Void) -> Either String (Src, Expr Src Void)
forall (m :: * -> *) a. Monad m => a -> m a
return (Src
srcAnnot, Expr Src Void -> Expr Src Void
forall a s t. Eq a => Expr s a -> Expr t a
normalize Expr Src Void
_A)

-- binders, see typeAt'
annotateLet' Position
pos Context (Expr Src Void)
ctx (Let (Binding { variable :: forall s a. Binding s a -> Text
variable = Text
x, value :: forall s a. Binding s a -> Expr s a
value = Expr Src Void
a }) e :: Expr Src Void
e@(Note Src
src Expr Src Void
_)) | Position
pos Position -> Src -> Bool
`inside` Src
src = do
  Expr Src Void
_ <- (TypeError Src Void -> String)
-> Either (TypeError Src Void) (Expr Src Void)
-> Either String (Expr Src Void)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first TypeError Src Void -> String
forall a. Show a => a -> String
show (Either (TypeError Src Void) (Expr Src Void)
 -> Either String (Expr Src Void))
-> Either (TypeError Src Void) (Expr Src Void)
-> Either String (Expr Src Void)
forall a b. (a -> b) -> a -> b
$ 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)
ctx Expr Src Void
a
  let a' :: Expr s Void
a' = Int -> Var -> Expr s Void -> Expr s 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 s Void
forall a s t. Eq a => Expr s a -> Expr t a
normalize Expr Src Void
a)
  Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either String (Src, Expr Src Void)
annotateLet' Position
pos Context (Expr Src Void)
ctx (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) (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 s. Expr s Void
a' Expr Src Void
e))

annotateLet' Position
pos Context (Expr Src Void)
ctx (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 } b :: Expr Src Void
b@(Note Src
src Expr Src Void
_)) | Position
pos Position -> Src -> Bool
`inside` Src
src = do
  let _A' :: Expr t Void
_A' = Expr Src Void -> Expr t Void
forall a s t. Eq a => Expr s a -> Expr t a
Dhall.Core.normalize Expr Src Void
_A
      ctx' :: Context (Expr Src Void)
ctx' = (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
fmap (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)) (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. Expr s Void
_A' Context (Expr Src Void)
ctx)
  Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either String (Src, Expr Src Void)
annotateLet' Position
pos Context (Expr Src Void)
ctx' Expr Src Void
b

annotateLet' Position
pos Context (Expr Src Void)
ctx (Pi Maybe CharacterSet
_ Text
x Expr Src Void
_A _B :: Expr Src Void
_B@(Note Src
src Expr Src Void
_)) | Position
pos Position -> Src -> Bool
`inside` Src
src = do
  let _A' :: Expr t Void
_A' = Expr Src Void -> Expr t Void
forall a s t. Eq a => Expr s a -> Expr t a
Dhall.Core.normalize Expr Src Void
_A
      ctx' :: Context (Expr Src Void)
ctx' = (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
fmap (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)) (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. Expr s Void
_A' Context (Expr Src Void)
ctx)
  Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either String (Src, Expr Src Void)
annotateLet' Position
pos Context (Expr Src Void)
ctx' Expr Src Void
_B

-- we need to unfold Notes to make progress
annotateLet' Position
pos Context (Expr Src Void)
ctx (Note Src
_ Expr Src Void
expr) =
  Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either String (Src, Expr Src Void)
annotateLet' Position
pos Context (Expr Src Void)
ctx Expr Src Void
expr

-- catch-all
annotateLet' Position
pos Context (Expr Src Void)
ctx Expr Src Void
expr = do
  let subExprs :: [Expr Src Void]
subExprs = Getting (Endo [Expr Src Void]) (Expr Src Void) (Expr Src Void)
-> Expr Src Void -> [Expr Src Void]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [Expr Src Void]) (Expr Src Void) (Expr Src Void)
forall (f :: * -> *) s a.
Applicative f =>
(Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
subExpressions Expr Src Void
expr
  case [ Src -> Expr Src Void -> Expr Src Void
forall s a. s -> Expr s a -> Expr s a
Note Src
src Expr Src Void
e | (Note Src
src Expr Src Void
e) <- [Expr Src Void]
subExprs, Position
pos Position -> Src -> Bool
`inside` Src
src ] of
    [Expr Src Void
e] -> Position
-> Context (Expr Src Void)
-> Expr Src Void
-> Either String (Src, Expr Src Void)
annotateLet' Position
pos Context (Expr Src Void)
ctx Expr Src Void
e
    [Expr Src Void]
_ -> String -> Either String (Src, Expr Src Void)
forall a b. a -> Either a b
Left String
"You weren't pointing at a let binder!"

-- Make sure all lets in a multilet are annotated with their source information
splitMultiLetSrc :: Expr Src a -> Maybe (Expr Src a)
splitMultiLetSrc :: Expr Src a -> Maybe (Expr Src a)
splitMultiLetSrc (Note Src
src (Let Binding Src a
b (Let Binding Src a
b' Expr Src a
e))) = do
  Src
src' <- Src -> Maybe Src
getLetInner Src
src
  Expr Src a -> Maybe (Expr Src a)
forall a. Expr Src a -> Maybe (Expr Src a)
splitMultiLetSrc (Src -> Expr Src a -> Expr Src a
forall s a. s -> Expr s a -> Expr s a
Note Src
src (Binding Src a -> Expr Src a -> Expr Src a
forall s a. Binding s a -> Expr s a -> Expr s a
Let Binding Src a
b (Src -> Expr Src a -> Expr Src a
forall s a. s -> Expr s a -> Expr s a
Note Src
src' (Binding Src a -> Expr Src a -> Expr Src a
forall s a. Binding s a -> Expr s a -> Expr s a
Let Binding Src a
b' Expr Src a
e))))
splitMultiLetSrc Expr Src a
expr = (Expr Src a -> Maybe (Expr Src a))
-> Expr Src a -> Maybe (Expr Src a)
forall (f :: * -> *) s a.
Applicative f =>
(Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
subExpressions Expr Src a -> Maybe (Expr Src a)
forall a. Expr Src a -> Maybe (Expr Src a)
splitMultiLetSrc Expr Src a
expr

-- 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 :: Position -> Src -> Bool
inside Position
pos Src
src = Position
left Position -> Position -> Bool
forall a. Ord a => a -> a -> Bool
<= Position
pos Bool -> Bool -> Bool
&& Position
pos Position -> Position -> Bool
forall a. Ord a => a -> a -> Bool
< Position
right
  where Range Position
left Position
right = Src -> Range
rangeFromDhall Src
src