Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(parsing): preserve whitespaces on Lam #1980

Merged
merged 5 commits into from
Aug 7, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 8 additions & 8 deletions dhall-json/src/Dhall/JSON.hs
Original file line number Diff line number Diff line change
Expand Up @@ -500,8 +500,8 @@ dhallToJSON e0 = loop (Core.alphaNormalize (Core.normalize e0))
return (Aeson.toJSON (Dhall.Map.toMap a'))
Core.App (Core.Field (Core.Union _) _) b -> loop b
Core.Field (Core.Union _) k -> return (Aeson.toJSON k)
Core.Lam _ (Core.Const Core.Type)
(Core.Lam _
Core.Lam (Core.functionBindingAnnotation -> Core.Const Core.Type)
(Core.Lam (Core.functionBindingAnnotation ->
(Core.Record
[ ("array" , Core.recordFieldValue -> Core.Pi _ (Core.App Core.List (V 0)) (V 1))
, ("bool" , Core.recordFieldValue -> Core.Pi _ Core.Bool (V 1))
Expand All @@ -513,7 +513,7 @@ dhallToJSON e0 = loop (Core.alphaNormalize (Core.normalize e0))
, ("mapValue", Core.recordFieldValue -> V 0)])) (V 1))
, ("string", Core.recordFieldValue -> Core.Pi _ Core.Text (V 1))
]
)
))
value
) -> do
let outer (Core.Field (V 0) "null") = return Aeson.Null
Expand Down Expand Up @@ -542,8 +542,8 @@ dhallToJSON e0 = loop (Core.alphaNormalize (Core.normalize e0))
outer _ = Left (Unsupported e)

outer value
Core.Lam _ (Core.Const Core.Type)
(Core.Lam _
Core.Lam (Core.functionBindingAnnotation -> Core.Const Core.Type)
(Core.Lam (Core.functionBindingAnnotation ->
(Core.Record
[ ("array" , Core.recordFieldValue -> Core.Pi _ (Core.App Core.List (V 0)) (V 1))
, ("bool" , Core.recordFieldValue -> Core.Pi _ Core.Bool (V 1))
Expand All @@ -557,7 +557,7 @@ dhallToJSON e0 = loop (Core.alphaNormalize (Core.normalize e0))
])) (V 1))
, ("string", Core.recordFieldValue -> Core.Pi _ Core.Text (V 1))
]
)
))
value
) -> do
let outer (Core.Field (V 0) "null") =
Expand Down Expand Up @@ -728,8 +728,8 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Core.normalize e0)
case we do *not* want to perform this rewrite since it will
interfere with decoding the value.
-}
Core.Lam a b c ->
Core.Lam a b c
Core.Lam a b ->
Core.Lam a b

Core.Pi a b c ->
Core.Pi a b' c'
Expand Down
12 changes: 6 additions & 6 deletions dhall-json/src/Dhall/JSONToDhall.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1007,8 +1007,8 @@ dhallFromJSON (Conversion {..}) expressionType =
D.Field "json" "null"

let result =
D.Lam "JSON" (D.Const D.Type)
(D.Lam "json"
D.Lam (D.makeFunctionBinding "JSON" (D.Const D.Type))
(D.Lam (D.makeFunctionBinding "json"
(D.Record
[ ("array" , D.makeRecordField $ D.Pi "_" (D.App D.List "JSON") "JSON")
, ("bool" , D.makeRecordField $ D.Pi "_" D.Bool "JSON")
Expand All @@ -1021,7 +1021,7 @@ dhallFromJSON (Conversion {..}) expressionType =
])) "JSON")
, ("string", D.makeRecordField $ D.Pi "_" D.Text "JSON")
]
)
))
(outer value)
)

Expand Down Expand Up @@ -1097,8 +1097,8 @@ dhallFromJSON (Conversion {..}) expressionType =
D.Field "json" "null"

let result =
D.Lam "JSON" (D.Const D.Type)
(D.Lam "json"
D.Lam (D.makeFunctionBinding "JSON" (D.Const D.Type))
(D.Lam (D.makeFunctionBinding "json"
(D.Record
[ ("array" , D.makeRecordField $ D.Pi "_" (D.App D.List "JSON") "JSON")
, ("bool" , D.makeRecordField $ D.Pi "_" D.Bool "JSON")
Expand All @@ -1111,7 +1111,7 @@ dhallFromJSON (Conversion {..}) expressionType =
, ("mapValue", D.makeRecordField "JSON")])) "JSON")
, ("string", D.makeRecordField $ D.Pi "_" D.Text "JSON")
]
)
))
(outer value)
)

Expand Down
3 changes: 2 additions & 1 deletion dhall-lsp-server/src/Dhall/LSP/Backend/Completion.hs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ import System.Timeout (timeout)
import Dhall.Core
( Binding (..)
, Expr (..)
, FunctionBinding (..)
, RecordField (..)
, Var (..)
, normalize
Expand Down Expand Up @@ -123,7 +124,7 @@ buildCompletionContext' context values (Let (Binding { variable = x, annotation

in buildCompletionContext' context' values' e

buildCompletionContext' context values (Lam x _A b) =
buildCompletionContext' context values (Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A}) b) =
let _A' | Right _ <- typeWithA absurd context _A = normalize _A
| otherwise = holeExpr

Expand Down
10 changes: 8 additions & 2 deletions dhall-lsp-server/src/Dhall/LSP/Backend/Parsing.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,13 @@ where

import Control.Applicative (optional, (<|>))
import Data.Text (Text)
import Dhall.Core (Binding (..), Expr (..), Import, Var (..))
import Dhall.Core
( Binding (..)
, Expr (..)
, Import
, Var (..)
, makeFunctionBinding
)
import Dhall.Parser
import Dhall.Parser.Expression
( getSourcePos
Expand Down Expand Up @@ -308,4 +314,4 @@ binderExprFromText txt =
<|> (do skipManyTill anySingle _arrow; return holeExpr)
whitespace
inner <- parseBinderExpr
return (Lam name typ inner)
return (Lam (makeFunctionBinding name typ) inner)
17 changes: 10 additions & 7 deletions dhall-lsp-server/src/Dhall/LSP/Backend/Typing.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ import Dhall.Context (Context, empty, insert)
import Dhall.Core
( Binding (..)
, Expr (..)
, FunctionBinding (..)
, Var (..)
, normalize
, shift
Expand Down Expand Up @@ -49,8 +50,9 @@ typeAt' pos ctx (Note src (Let (Binding { value = a }) _)) | pos `inside` getLet
return (Just $ getLetIdentifier src, typ)

-- "..." in a lambda expression
typeAt' pos _ctx (Note src (Lam _ _A _)) | Just src' <- getLamIdentifier src
, pos `inside` src' =
typeAt' pos _ctx (Note src (Lam FunctionBinding { functionBindingAnnotation = _A} _))
| Just src' <- getLamIdentifier src
, pos `inside` src' =
return (Just src', _A)

-- "..." in a forall expression
Expand All @@ -63,10 +65,11 @@ typeAt' pos ctx (Let (Binding { variable = x, value = a }) e@(Note src _)) | pos
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 (Lam FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _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
Expand Down Expand Up @@ -136,7 +139,7 @@ annotateLet' pos ctx (Let (Binding { variable = x, value = a }) e@(Note src _))
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
annotateLet' pos ctx (Lam FunctionBinding{ functionBindingVariable = x, functionBindingAnnotation = _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
Expand Down
9 changes: 5 additions & 4 deletions dhall-nix/src/Dhall/Nix.hs
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,7 @@ import Dhall.Core
, Chunks (..)
, DhallDouble (..)
, Expr (..)
, FunctionBinding (..)
, MultiLet (..)
, PreferAnnotation (..)
, Var (..)
Expand Down Expand Up @@ -236,7 +237,7 @@ dhallToNix e =
-- If any other number, then rename the variable to include the maximum
-- depth.
maximumDepth :: Var -> Expr s Void -> Maybe Int
maximumDepth v@(V x n) (Lam x' a b)
maximumDepth v@(V x n) (Lam FunctionBinding {functionBindingVariable = x', functionBindingAnnotation = a} b)
| x == x' =
max (maximumDepth v a) (fmap (+ 1) (maximumDepth (V x (n + 1)) b))
maximumDepth v@(V x n) (Pi x' a b)
Expand Down Expand Up @@ -271,10 +272,10 @@ dhallToNix e =
x' = x <> Data.Text.pack (show n)

renameShadowed :: Expr s Void -> Maybe (Expr s Void)
renameShadowed (Lam x a b) = do
renameShadowed (Lam FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = a} b) = do
(x', b') <- rename (x, b)

return (Lam x' a b')
return (Lam (Dhall.Core.makeFunctionBinding x' a) b')
renameShadowed (Pi x a b) = do
(x', b') <- rename (x, b)

Expand All @@ -293,7 +294,7 @@ dhallToNix e =
loop (Const _) = return untranslatable
loop (Var (V a 0)) = return (Fix (NSym a))
loop (Var a ) = Left (CannotReferenceShadowedVariable a)
loop (Lam a _ c) = do
loop (Lam FunctionBinding { functionBindingVariable = a } c) = do
c' <- loop c
return (Fix (NAbs (Param a) c'))
loop (Pi _ _ _) = return untranslatable
Expand Down
7 changes: 5 additions & 2 deletions dhall/src/Dhall.hs
Original file line number Diff line number Diff line change
Expand Up @@ -161,6 +161,7 @@ import Dhall.Syntax
( Chunks (..)
, DhallDouble (..)
, Expr (..)
, FunctionBinding (..)
, RecordField (..)
, Var (..)
)
Expand Down Expand Up @@ -1361,10 +1362,12 @@ instance (Functor f, FromDhall (f (Result f))) => FromDhall (Fix f) where
where
die = typeError expected expr0

extract0 (Lam x _ expr) = extract1 (rename x "result" expr)
extract0 (Lam (FunctionBinding { functionBindingVariable = x }) expr) =
extract1 (rename x "result" expr)
extract0 _ = die

extract1 (Lam y _ expr) = extract2 (rename y "Make" expr)
extract1 (Lam (FunctionBinding { functionBindingVariable = y }) expr) =
extract2 (rename y "Make" expr)
extract1 _ = die

extract2 expr = fmap resultToFix (Dhall.extract (autoWith inputNormalizer) expr)
Expand Down
9 changes: 5 additions & 4 deletions dhall/src/Dhall/Binary.hs
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ import Dhall.Syntax
, Expr (..)
, File (..)
, FilePrefix (..)
, FunctionBinding (..)
, Import (..)
, ImportHashed (..)
, ImportMode (..)
Expand Down Expand Up @@ -256,7 +257,7 @@ decodeExpressionInternal decodeEmbed = go

b <- go

return (Lam "_" _A b)
return (Lam (Syntax.makeFunctionBinding "_" _A) b)

4 -> do
x <- Decoding.decodeString
Expand All @@ -269,7 +270,7 @@ decodeExpressionInternal decodeEmbed = go

b <- go

return (Lam x _A b)
return (Lam (Syntax.makeFunctionBinding x _A) b)

_ ->
die ("Incorrect number of tokens used to encode a λ expression: " <> show len)
Expand Down Expand Up @@ -706,13 +707,13 @@ encodeExpressionInternal encodeEmbed = go
where
(function, arguments) = unApply a

Lam "_" _A b ->
Lam (FunctionBinding { functionBindingVariable = "_", functionBindingAnnotation = _A }) b ->
encodeList3
(Encoding.encodeInt 1)
(go _A)
(go b)

Lam x _A b ->
Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A }) b ->
encodeList4
(Encoding.encodeInt 1)
(Encoding.encodeString x)
Expand Down
3 changes: 3 additions & 0 deletions dhall/src/Dhall/Core.hs
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,8 @@ module Dhall.Core (
, PreferAnnotation(..)
, RecordField(..)
, makeRecordField
, FunctionBinding(..)
, makeFunctionBinding
, Expr(..)

-- * Normalization
Expand Down Expand Up @@ -55,6 +57,7 @@ module Dhall.Core (
, chunkExprs
, bindingExprs
, recordFieldExprs
, functionBindingExprs

-- * Let-blocks
, multiLet
Expand Down
5 changes: 4 additions & 1 deletion dhall/src/Dhall/Diff.hs
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ import Dhall.Syntax
, Const (..)
, DhallDouble (..)
, Expr (..)
, FunctionBinding (..)
, RecordField (..)
, Var (..)
)
Expand Down Expand Up @@ -645,7 +646,9 @@ diff :: (Eq a, Pretty a) => Expr Void a -> Expr Void a -> Diff
diff l@(Lam {}) r@(Lam {}) =
enclosed' " " (rarrow <> " ") (docs l r)
where
docs (Lam aL bL cL) (Lam aR bR cR) =
docs
(Lam (FunctionBinding { functionBindingVariable = aL, functionBindingAnnotation = bL }) cL)
(Lam (FunctionBinding { functionBindingVariable = aR, functionBindingAnnotation = bR }) cR) =
Data.List.NonEmpty.cons (align doc) (docs cL cR)
where
doc = lambda
Expand Down
32 changes: 19 additions & 13 deletions dhall/src/Dhall/Eval.hs
Original file line number Diff line number Diff line change
Expand Up @@ -50,21 +50,22 @@ module Dhall.Eval (
, textShow
) where

import Data.Foldable (foldr', toList)
import Data.Sequence (Seq, ViewL (..), ViewR (..))
import Data.Text (Text)
import Data.Void (Void)
import Dhall.Map (Map)
import Dhall.Set (Set)
import GHC.Natural (Natural)
import Prelude hiding (succ)
import Data.Foldable (foldr', toList)
import Data.Sequence (Seq, ViewL (..), ViewR (..))
import Data.Text (Text)
import Data.Void (Void)
import Dhall.Map (Map)
import Dhall.Set (Set)
import GHC.Natural (Natural)
import Prelude hiding (succ)

import Dhall.Syntax
( Binding (..)
, Chunks (..)
, Const (..)
, DhallDouble (..)
, Expr (..)
, FunctionBinding (..)
, PreferAnnotation (..)
, RecordField (..)
, Var (..)
Expand Down Expand Up @@ -389,7 +390,7 @@ eval !env t0 =
VConst k
Var v ->
vVar env v
Lam x a t ->
Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = a }) t ->
VLam (eval env a) (Closure x env t)
Pi x a b ->
VPi (eval env a) (Closure x env b)
Expand Down Expand Up @@ -984,10 +985,15 @@ quote !env !t0 =
VApp t u ->
quote env t `qApp` u
VLam a (freshClosure -> (x, v, t)) ->
Lam x (quote env a) (quoteBind x (instantiate t v))
Lam
(Syntax.makeFunctionBinding x (quote env a))
(quoteBind x (instantiate t v))
VHLam i t ->
case i of
Typed (fresh -> (x, v)) a -> Lam x (quote env a) (quoteBind x (t v))
Typed (fresh -> (x, v)) a ->
Lam
(Syntax.makeFunctionBinding x (quote env a))
(quoteBind x (t v))
Prim -> quote env (t VPrimVar)
NaturalSubtractZero -> App NaturalSubtract (NaturalLit 0)

Expand Down Expand Up @@ -1165,8 +1171,8 @@ alphaNormalize = goEnv EmptyNames
Const k
Var (V x i) ->
goVar e0 x i
Lam x t u ->
Lam "_" (go t) (goBind x u)
Lam (FunctionBinding src0 x src1 src2 t) u ->
Lam (FunctionBinding src0 "_" src1 src2 (go t)) (goBind x u)
Pi x a b ->
Pi "_" (go a) (goBind x b)
App t u ->
Expand Down
2 changes: 2 additions & 0 deletions dhall/src/Dhall/Import.hs
Original file line number Diff line number Diff line change
Expand Up @@ -173,6 +173,7 @@ import Dhall.Syntax
, RecordField (..)
, URL (..)
, bindingExprs
, functionBindingExprs
, recordFieldExprs
)

Expand Down Expand Up @@ -1074,6 +1075,7 @@ loadWith expr₀ = case expr₀ of
Let a b -> Let <$> bindingExprs loadWith a <*> loadWith b
Record m -> Record <$> traverse (recordFieldExprs loadWith) m
RecordLit m -> RecordLit <$> traverse (recordFieldExprs loadWith) m
Lam a b -> Lam <$> functionBindingExprs loadWith a <*> loadWith b
expression -> Syntax.unsafeSubExpressions loadWith expression

-- | Resolve all imports within an expression
Expand Down
Loading