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
)
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)
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)
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)
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
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
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
(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)
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)
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
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)
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)
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
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
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!"
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
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