From 728a0e61a91806544de864488d8e52f6c9e4b458 Mon Sep 17 00:00:00 2001 From: German Robayo Date: Thu, 6 Aug 2020 11:14:11 -0400 Subject: [PATCH 1/5] record whitespaces on Lam --- dhall-json/src/Dhall/JSON.hs | 16 ++-- dhall-json/src/Dhall/JSONToDhall.hs | 12 +-- .../src/Dhall/LSP/Backend/Completion.hs | 3 +- .../src/Dhall/LSP/Backend/Parsing.hs | 10 ++- .../src/Dhall/LSP/Backend/Typing.hs | 7 +- dhall-nix/src/Dhall/Nix.hs | 9 +- dhall/src/Dhall.hs | 5 +- dhall/src/Dhall/Binary.hs | 9 +- dhall/src/Dhall/Core.hs | 3 + dhall/src/Dhall/Diff.hs | 5 +- dhall/src/Dhall/Eval.hs | 32 ++++--- dhall/src/Dhall/Import.hs | 2 + dhall/src/Dhall/Normalize.hs | 32 ++++--- dhall/src/Dhall/Parser/Expression.hs | 8 +- dhall/src/Dhall/Pretty/Internal.hs | 5 +- dhall/src/Dhall/Syntax.hs | 85 ++++++++++++++++++- dhall/src/Dhall/TypeCheck.hs | 3 +- dhall/tests/Dhall/Test/QuickCheck.hs | 15 +++- 18 files changed, 191 insertions(+), 70 deletions(-) diff --git a/dhall-json/src/Dhall/JSON.hs b/dhall-json/src/Dhall/JSON.hs index a27de5cb3..7b0990697 100644 --- a/dhall-json/src/Dhall/JSON.hs +++ b/dhall-json/src/Dhall/JSON.hs @@ -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.fbAnnotation -> Core.Const Core.Type) + (Core.Lam (Core.fbAnnotation -> (Core.Record [ ("array" , Core.recordFieldValue -> Core.Pi _ (Core.App Core.List (V 0)) (V 1)) , ("bool" , Core.recordFieldValue -> Core.Pi _ Core.Bool (V 1)) @@ -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 @@ -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.fbAnnotation -> Core.Const Core.Type) + (Core.Lam (Core.fbAnnotation -> (Core.Record [ ("array" , Core.recordFieldValue -> Core.Pi _ (Core.App Core.List (V 0)) (V 1)) , ("bool" , Core.recordFieldValue -> Core.Pi _ Core.Bool (V 1)) @@ -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") = @@ -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' diff --git a/dhall-json/src/Dhall/JSONToDhall.hs b/dhall-json/src/Dhall/JSONToDhall.hs index d8acd9545..21061d18b 100644 --- a/dhall-json/src/Dhall/JSONToDhall.hs +++ b/dhall-json/src/Dhall/JSONToDhall.hs @@ -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") @@ -1021,7 +1021,7 @@ dhallFromJSON (Conversion {..}) expressionType = ])) "JSON") , ("string", D.makeRecordField $ D.Pi "_" D.Text "JSON") ] - ) + )) (outer value) ) @@ -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") @@ -1111,7 +1111,7 @@ dhallFromJSON (Conversion {..}) expressionType = , ("mapValue", D.makeRecordField "JSON")])) "JSON") , ("string", D.makeRecordField $ D.Pi "_" D.Text "JSON") ] - ) + )) (outer value) ) diff --git a/dhall-lsp-server/src/Dhall/LSP/Backend/Completion.hs b/dhall-lsp-server/src/Dhall/LSP/Backend/Completion.hs index 7add114b1..01a17dc43 100644 --- a/dhall-lsp-server/src/Dhall/LSP/Backend/Completion.hs +++ b/dhall-lsp-server/src/Dhall/LSP/Backend/Completion.hs @@ -16,6 +16,7 @@ import System.Timeout (timeout) import Dhall.Core ( Binding (..) , Expr (..) + , FunctionBinding (..) , RecordField (..) , Var (..) , normalize @@ -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 { fbVariable = x, fbAnnotation = _A}) b) = let _A' | Right _ <- typeWithA absurd context _A = normalize _A | otherwise = holeExpr diff --git a/dhall-lsp-server/src/Dhall/LSP/Backend/Parsing.hs b/dhall-lsp-server/src/Dhall/LSP/Backend/Parsing.hs index 23d95ed0a..ef5ffba50 100644 --- a/dhall-lsp-server/src/Dhall/LSP/Backend/Parsing.hs +++ b/dhall-lsp-server/src/Dhall/LSP/Backend/Parsing.hs @@ -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 @@ -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) diff --git a/dhall-lsp-server/src/Dhall/LSP/Backend/Typing.hs b/dhall-lsp-server/src/Dhall/LSP/Backend/Typing.hs index fd78d6ea7..bf691887a 100644 --- a/dhall-lsp-server/src/Dhall/LSP/Backend/Typing.hs +++ b/dhall-lsp-server/src/Dhall/LSP/Backend/Typing.hs @@ -4,6 +4,7 @@ import Dhall.Context (Context, empty, insert) import Dhall.Core ( Binding (..) , Expr (..) + , FunctionBinding (..) , Var (..) , normalize , shift @@ -49,7 +50,7 @@ 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 +typeAt' pos _ctx (Note src (Lam FunctionBinding { fbAnnotation = _A} _)) | Just src' <- getLamIdentifier src , pos `inside` src' = return (Just src', _A) @@ -63,7 +64,7 @@ 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 +typeAt' pos ctx (Lam FunctionBinding { fbVariable = x, fbAnnotation = _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 @@ -136,7 +137,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{ fbVariable = x, fbAnnotation = _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 diff --git a/dhall-nix/src/Dhall/Nix.hs b/dhall-nix/src/Dhall/Nix.hs index c230fe06a..ac6f18747 100644 --- a/dhall-nix/src/Dhall/Nix.hs +++ b/dhall-nix/src/Dhall/Nix.hs @@ -103,6 +103,7 @@ import Dhall.Core , Chunks (..) , DhallDouble (..) , Expr (..) + , FunctionBinding (..) , MultiLet (..) , PreferAnnotation (..) , Var (..) @@ -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 {fbVariable = x', fbAnnotation = 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) @@ -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 { fbVariable = x, fbAnnotation = 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) @@ -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 { fbVariable = a } c) = do c' <- loop c return (Fix (NAbs (Param a) c')) loop (Pi _ _ _) = return untranslatable diff --git a/dhall/src/Dhall.hs b/dhall/src/Dhall.hs index 9ae2593fc..9f914206c 100644 --- a/dhall/src/Dhall.hs +++ b/dhall/src/Dhall.hs @@ -161,6 +161,7 @@ import Dhall.Syntax ( Chunks (..) , DhallDouble (..) , Expr (..) + , FunctionBinding (..) , RecordField (..) , Var (..) ) @@ -1361,10 +1362,10 @@ 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 { fbVariable = x }) expr) = extract1 (rename x "result" expr) extract0 _ = die - extract1 (Lam y _ expr) = extract2 (rename y "Make" expr) + extract1 (Lam (FunctionBinding { fbVariable = y }) expr) = extract2 (rename y "Make" expr) extract1 _ = die extract2 expr = fmap resultToFix (Dhall.extract (autoWith inputNormalizer) expr) diff --git a/dhall/src/Dhall/Binary.hs b/dhall/src/Dhall/Binary.hs index cb587758d..b61954b10 100644 --- a/dhall/src/Dhall/Binary.hs +++ b/dhall/src/Dhall/Binary.hs @@ -39,6 +39,7 @@ import Dhall.Syntax , Expr (..) , File (..) , FilePrefix (..) + , FunctionBinding (..) , Import (..) , ImportHashed (..) , ImportMode (..) @@ -256,7 +257,7 @@ decodeExpressionInternal decodeEmbed = go b <- go - return (Lam "_" _A b) + return (Lam (Syntax.makeFunctionBinding "_" _A) b) 4 -> do x <- Decoding.decodeString @@ -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) @@ -706,13 +707,13 @@ encodeExpressionInternal encodeEmbed = go where (function, arguments) = unApply a - Lam "_" _A b -> + Lam (FunctionBinding { fbVariable = "_", fbAnnotation = _A }) b -> encodeList3 (Encoding.encodeInt 1) (go _A) (go b) - Lam x _A b -> + Lam (FunctionBinding { fbVariable = x, fbAnnotation = _A }) b -> encodeList4 (Encoding.encodeInt 1) (Encoding.encodeString x) diff --git a/dhall/src/Dhall/Core.hs b/dhall/src/Dhall/Core.hs index dacd79757..bdaef5adc 100644 --- a/dhall/src/Dhall/Core.hs +++ b/dhall/src/Dhall/Core.hs @@ -27,6 +27,8 @@ module Dhall.Core ( , PreferAnnotation(..) , RecordField(..) , makeRecordField + , FunctionBinding(..) + , makeFunctionBinding , Expr(..) -- * Normalization @@ -55,6 +57,7 @@ module Dhall.Core ( , chunkExprs , bindingExprs , recordFieldExprs + , functionBindingExprs -- * Let-blocks , multiLet diff --git a/dhall/src/Dhall/Diff.hs b/dhall/src/Dhall/Diff.hs index ceec2f6de..7f8949bb1 100644 --- a/dhall/src/Dhall/Diff.hs +++ b/dhall/src/Dhall/Diff.hs @@ -32,6 +32,7 @@ import Dhall.Syntax , Const (..) , DhallDouble (..) , Expr (..) + , FunctionBinding (..) , RecordField (..) , Var (..) ) @@ -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 { fbVariable = aL, fbAnnotation = bL }) cL) + (Lam (FunctionBinding { fbVariable = aR, fbAnnotation = bR }) cR) = Data.List.NonEmpty.cons (align doc) (docs cL cR) where doc = lambda diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs index 7d4559929..1831d15c2 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -50,14 +50,14 @@ 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 (..) @@ -65,6 +65,7 @@ import Dhall.Syntax , Const (..) , DhallDouble (..) , Expr (..) + , FunctionBinding (..) , PreferAnnotation (..) , RecordField (..) , Var (..) @@ -389,7 +390,7 @@ eval !env t0 = VConst k Var v -> vVar env v - Lam x a t -> + Lam (FunctionBinding { fbVariable = x, fbAnnotation = a }) t -> VLam (eval env a) (Closure x env t) Pi x a b -> VPi (eval env a) (Closure x env b) @@ -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) @@ -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 -> diff --git a/dhall/src/Dhall/Import.hs b/dhall/src/Dhall/Import.hs index d145ecd40..2eab2cea8 100644 --- a/dhall/src/Dhall/Import.hs +++ b/dhall/src/Dhall/Import.hs @@ -173,6 +173,7 @@ import Dhall.Syntax , RecordField (..) , URL (..) , bindingExprs + , functionBindingExprs , recordFieldExprs ) @@ -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 diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs index b76264dc3..a953519ea 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -1,6 +1,7 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ViewPatterns #-} module Dhall.Normalize ( alphaNormalize @@ -31,6 +32,7 @@ import Dhall.Syntax , Chunks (..) , DhallDouble (..) , Expr (..) + , FunctionBinding (..) , PreferAnnotation (..) , RecordField (..) , Var (..) @@ -120,7 +122,8 @@ shift :: Int -> Var -> Expr s a -> Expr s a shift d (V x n) (Var (V x' n')) = Var (V x' n'') where n'' = if x == x' && n <= n' then n' + d else n' -shift d (V x n) (Lam x' _A b) = Lam x' _A' b' +shift d (V x n) (Lam (FunctionBinding src0 x' src1 src2 _A) b) = + Lam (FunctionBinding src0 x' src1 src2 _A') b' where _A' = shift d (V x n ) _A b' = shift d (V x n') b @@ -149,7 +152,8 @@ shift d v expression = Lens.over Syntax.subExpressions (shift d v) expression -} subst :: Var -> Expr s a -> Expr s a -> Expr s a subst _ _ (Const a) = Const a -subst (V x n) e (Lam y _A b) = Lam y _A' b' +subst (V x n) e (Lam (FunctionBinding src0 y src1 src2 _A) b) = + Lam (FunctionBinding src0 y src1 src2 _A') b' where _A' = subst (V x n ) e _A b' = subst (V x n') (shift 1 (V y 0) e) b @@ -196,8 +200,9 @@ boundedType _ = False {-| α-normalize an expression by renaming all bound variables to @\"_\"@ and using De Bruijn indices to distinguish them ->>> alphaNormalize (Lam "a" (Const Type) (Lam "b" (Const Type) (Lam "x" "a" (Lam "y" "b" "x")))) -Lam "_" (Const Type) (Lam "_" (Const Type) (Lam "_" (Var (V "_" 1)) (Lam "_" (Var (V "_" 1)) (Var (V "_" 1))))) +>>> mfb = Syntax.makeFunctionBinding +>>> alphaNormalize (Lam (mfb "a" (Const Type)) (Lam (mfb "b" (Const Type)) (Lam (mfb "x" "a") (Lam (mfb "y" "b") "x")))) +Lam (FunctionBinding {fbSrc0 = Nothing, fbVariable = "_", fbSrc1 = Nothing, fbSrc2 = Nothing, fbAnnotation = Const Type}) (Lam (FunctionBinding {fbSrc0 = Nothing, fbVariable = "_", fbSrc1 = Nothing, fbSrc2 = Nothing, fbAnnotation = Const Type}) (Lam (FunctionBinding {fbSrc0 = Nothing, fbVariable = "_", fbSrc1 = Nothing, fbSrc2 = Nothing, fbAnnotation = Var (V "_" 1)}) (Lam (FunctionBinding {fbSrc0 = Nothing, fbVariable = "_", fbSrc1 = Nothing, fbSrc2 = Nothing, fbAnnotation = Var (V "_" 1)}) (Var (V "_" 1))))) α-normalization does not affect free variables: @@ -256,7 +261,8 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) loop e = case e of Const k -> pure (Const k) Var v -> pure (Var v) - Lam x _A b -> Lam x <$> _A' <*> b' + Lam (FunctionBinding { fbVariable = x, fbAnnotation = _A }) b -> + Lam <$> (Syntax.makeFunctionBinding x <$> _A') <*> b' where _A' = loop _A b' = loop b @@ -272,7 +278,7 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) f' <- loop f a' <- loop a case f' of - Lam x _A b₀ -> do + Lam (FunctionBinding _ x _ _ _A) b₀ -> do let a₂ = shift 1 (V x 0) a' let b₁ = subst (V x 0) a₂ b₀ @@ -299,7 +305,7 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) lazyLoop !n = App succ' (lazyLoop (n - 1)) App NaturalBuild g -> loop (App (App (App g Natural) succ) zero) where - succ = Lam "n" Natural (NaturalPlus "n" (NaturalLit 1)) + succ = Lam (Syntax.makeFunctionBinding "n" Natural) (NaturalPlus "n" (NaturalLit 1)) zero = NaturalLit 0 App NaturalIsZero (NaturalLit n) -> pure (BoolLit (n == 0)) @@ -341,9 +347,9 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) list = App List _A₀ cons = - Lam "a" _A₀ - (Lam "as" - (App List _A₁) + Lam (Syntax.makeFunctionBinding "a" _A₀) + (Lam + (Syntax.makeFunctionBinding "as" (App List _A₁)) (ListAppend (ListLit Nothing (pure "a")) "as") ) @@ -732,10 +738,10 @@ isNormalized e0 = loop (Syntax.denote e0) loop e = case e of Const _ -> True Var _ -> True - Lam _ a b -> loop a && loop b + Lam (Syntax.fbAnnotation -> a) b -> loop a && loop b Pi _ a b -> loop a && loop b App f a -> loop f && loop a && case App f a of - App (Lam _ _ _) _ -> False + App (Lam _ _) _ -> False App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False App NaturalBuild _ -> False App NaturalIsZero (NaturalLit _) -> False @@ -916,7 +922,7 @@ isNormalized e0 = loop (Syntax.denote e0) True >>> "x" `freeIn` "y" False ->>> "x" `freeIn` Lam "x" (Const Type) "x" +>>> "x" `freeIn` Lam (mfb "x" (Const Type)) "x" False -} freeIn :: Eq a => Var -> Expr s a -> Bool diff --git a/dhall/src/Dhall/Parser/Expression.hs b/dhall/src/Dhall/Parser/Expression.hs index 9edcbedd1..96d426c32 100644 --- a/dhall/src/Dhall/Parser/Expression.hs +++ b/dhall/src/Dhall/Parser/Expression.hs @@ -137,11 +137,11 @@ parsers embedded = Parsers {..} _lambda whitespace _openParens - whitespace + src0 <- src whitespace a <- label - whitespace + src1 <- src whitespace _colon - nonemptyWhitespace + src2 <- src nonemptyWhitespace b <- expression whitespace _closeParens @@ -149,7 +149,7 @@ parsers embedded = Parsers {..} _arrow whitespace c <- expression - return (Lam a b c) + return (Lam (FunctionBinding (Just src0) a (Just src1) (Just src2) b) c) alternative1 = do try (_if *> nonemptyWhitespace) diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs index e27698e6b..9ba2b3e92 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -533,10 +533,11 @@ prettyCharacterSet :: Pretty a => CharacterSet -> Expr Src a -> Doc Ann prettyCharacterSet characterSet expression = Pretty.group (prettyExpression expression) where - prettyExpression a0@(Lam _ _ _) = + prettyExpression a0@(Lam _ _) = arrows characterSet (docs a0) where - docs (Lam a b c) = Pretty.group (Pretty.flatAlt long short) : docs c + docs (Lam (FunctionBinding { fbVariable = a, fbAnnotation = b }) c) = + Pretty.group (Pretty.flatAlt long short) : docs c where long = (lambda characterSet <> space) <> Pretty.align diff --git a/dhall/src/Dhall/Syntax.hs b/dhall/src/Dhall/Syntax.hs index 2f6360caf..415a56cd5 100644 --- a/dhall/src/Dhall/Syntax.hs +++ b/dhall/src/Dhall/Syntax.hs @@ -6,6 +6,7 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE StandaloneDeriving #-} @@ -29,6 +30,8 @@ module Dhall.Syntax ( , Expr(..) , RecordField(..) , makeRecordField + , FunctionBinding(..) + , makeFunctionBinding -- ** 'Let'-blocks , MultiLet(..) @@ -41,6 +44,7 @@ module Dhall.Syntax ( , chunkExprs , bindingExprs , recordFieldExprs + , functionBindingExprs -- ** Handling 'Note's , denote @@ -314,6 +318,43 @@ instance Bifunctor RecordField where RecordField (k <$> s0) (first k value) second = fmap +{-| Record the label of a function or a function-type expression + +For example, + +> λ({- A -} a {- B -} : {- C -} T) -> e + +will be instantiated as follows: +* @fbSrc0@ corresponds to the @A@ comment +* @fbVariable@ is @a@ +* @fbSrc1@ corresponds to the @B@ comment +* @fbSrc2@ corresponds to the @C@ comment +* @fbAnnotation@ is @T@ +-} +data FunctionBinding s a = FunctionBinding + { fbSrc0 :: Maybe s + , fbVariable :: Text + , fbSrc1 :: Maybe s + , fbSrc2 :: Maybe s + , fbAnnotation :: Expr s a + } deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable) + +makeFunctionBinding :: Text -> Expr s a -> FunctionBinding s a +makeFunctionBinding l t = FunctionBinding Nothing l Nothing Nothing t + +-- pattern Lam :: Text -> Expr s a -> Expr s a -> Expr s a +-- pattern Lam l t e <- Lam (FunctionBinding _ l _ _ t) e +-- where +-- Lam l t e = Lam (FunctionBinding Nothing l Nothing Nothing t) e + +-- {-# COMPLETE Lam #-} + +instance Bifunctor FunctionBinding where + first k (FunctionBinding src0 label src1 src2 type_) = + FunctionBinding (k <$> src0) label (k <$> src1) (k <$> src2) (first k type_) + + second = fmap + {-| Syntax tree for expressions The @s@ type parameter is used to track the presence or absence of `Src` @@ -334,8 +375,8 @@ data Expr s a -- | > Var (V x 0) ~ x -- > Var (V x n) ~ x@n | Var Var - -- | > Lam x A b ~ λ(x : A) -> b - | Lam Text (Expr s a) (Expr s a) + -- | > Lam (FunctionBinding _ "x" _ _ A) b ~ λ(x : A) -> b + | Lam (FunctionBinding s a) (Expr s a) -- | > Pi "_" A B ~ A -> B -- > Pi x A B ~ ∀(x : A) -> B | Pi Text (Expr s a) (Expr s a) @@ -520,6 +561,19 @@ data Expr s a -- NB: If you add a constructor to Expr, please also update the Arbitrary -- instance in Dhall.Test.QuickCheck. +-- {-# COMPLETE Lam, Var, Pi, App, Let, Annot, Bool, BoolLit, BoolAnd, +-- BoolOr, BoolEQ, BoolNE, BoolIf, Natural, NaturalLit, NaturalFold, +-- NaturalBuild, NaturalIsZero, NaturalEven, NaturalOdd, +-- NaturalToInteger, NaturalShow, NaturalSubtract, NaturalPlus, +-- NaturalTimes, Integer, IntegerLit, IntegerClamp, IntegerNegate, +-- IntegerShow, IntegerToDouble, Double, DoubleLit, DoubleShow, Text, +-- TextLit, TextAppend, TextShow, List, ListLit, ListAppend, +-- ListBuild, ListFold, ListLength, ListHead, ListLast, ListIndexed, +-- ListReverse, Optional, Some, None, Record, RecordLit, Union, +-- Combine, CombineTypes, Prefer, RecordCompletion, Merge, ToMap, +-- Field, Project, Assert, Equivalent, With, Note, ImportAlt, Embed +-- #-} + -- | This instance encodes what the Dhall standard calls an \"exact match\" -- between two expressions. -- @@ -543,6 +597,7 @@ instance Functor (Expr s) where fmap f (Note s e1) = Note s (fmap f e1) fmap f (Record a) = Record $ fmap f <$> a fmap f (RecordLit a) = RecordLit $ fmap f <$> a + fmap f (Lam fb e) = Lam (f <$> fb) (f <$> e) fmap f expression = Lens.over unsafeSubExpressions (fmap f) expression {-# INLINABLE fmap #-} @@ -560,6 +615,7 @@ instance Monad (Expr s) where Note a b -> Note a (b >>= k) Record a -> Record $ bindRecordKeyValues <$> a RecordLit a -> RecordLit $ bindRecordKeyValues <$> a + Lam a b -> Lam (adaptFunctionBinding a) (b >>= k) _ -> Lens.over unsafeSubExpressions (>>= k) expression where bindRecordKeyValues (RecordField s0 e) = RecordField s0 (e >>= k) @@ -567,6 +623,9 @@ instance Monad (Expr s) where adaptBinding (Binding src0 c src1 d src2 e) = Binding src0 c src1 (fmap adaptBindingAnnotation d) src2 (e >>= k) + adaptFunctionBinding (FunctionBinding src0 label src1 src2 type_) = + FunctionBinding src0 label src1 src2 (type_ >>= k) + adaptBindingAnnotation (src3, f) = (src3, f >>= k) instance Bifunctor Expr where @@ -575,6 +634,7 @@ instance Bifunctor Expr where first k (Let a b ) = Let (first k a) (first k b) first k (Record a ) = Record $ first k <$> a first k (RecordLit a) = RecordLit $ first k <$> a + first k (Lam a b ) = Lam (first k a) (first k b) first k expression = Lens.over unsafeSubExpressions (first k) expression second = fmap @@ -644,6 +704,7 @@ subExpressions f (Note a b) = Note a <$> f b subExpressions f (Let a b) = Let <$> bindingExprs f a <*> f b subExpressions f (Record a) = Record <$> traverse (recordFieldExprs f) a subExpressions f (RecordLit a) = RecordLit <$> traverse (recordFieldExprs f) a +subExpressions f (Lam fb e) = Lam <$> functionBindingExprs f fb <*> f e subExpressions f expression = unsafeSubExpressions f expression {-# INLINABLE subExpressions #-} @@ -658,7 +719,6 @@ unsafeSubExpressions :: Applicative f => (Expr s a -> f (Expr t b)) -> Expr s a -> f (Expr t b) unsafeSubExpressions _ (Const c) = pure (Const c) unsafeSubExpressions _ (Var v) = pure (Var v) -unsafeSubExpressions f (Lam a b c) = Lam a <$> f b <*> f c unsafeSubExpressions f (Pi a b c) = Pi a <$> f b <*> f c unsafeSubExpressions f (App a b) = App <$> f a <*> f b unsafeSubExpressions f (Annot a b) = Annot <$> f a <*> f b @@ -731,6 +791,7 @@ unsafeSubExpressions _ (Note {}) = unhandledConstructor "Note" unsafeSubExpressions _ (Embed {}) = unhandledConstructor "Embed" unsafeSubExpressions _ (Record {}) = unhandledConstructor "Record" unsafeSubExpressions _ (RecordLit {}) = unhandledConstructor "RecordLit" +unsafeSubExpressions _ (Lam {}) = unhandledConstructor "Lam" {-# INLINABLE unsafeSubExpressions #-} unhandledConstructor :: Text -> a @@ -768,6 +829,20 @@ recordFieldExprs f (RecordField s0 e) = <$> pure s0 <*> f e +{-| Traverse over the immediate 'Expr' children in a 'FunctionBinding'. +-} +functionBindingExprs + :: Applicative f + => (Expr s a -> f (Expr s b)) + -> FunctionBinding s a -> f (FunctionBinding s b) +functionBindingExprs f (FunctionBinding s0 label s1 s2 type_) = + FunctionBinding + <$> pure s0 + <*> pure label + <*> pure s1 + <*> pure s2 + <*> f type_ + -- | A traversal over the immediate sub-expressions in 'Chunks'. chunkExprs :: Applicative f @@ -990,6 +1065,7 @@ denote = \case Combine _ b c -> Combine Nothing (denote b) (denote c) Record a -> Record $ denoteRecordField <$> a RecordLit a -> RecordLit $ denoteRecordField <$> a + Lam a b -> Lam (denoteFunctionBinding a) (denote b) expression -> Lens.over unsafeSubExpressions denote expression where denoteRecordField (RecordField _ e) = RecordField Nothing (denote e) @@ -998,6 +1074,9 @@ denote = \case denoteBindingAnnotation (_, f) = (Nothing, denote f) + denoteFunctionBinding (FunctionBinding _ l _ _ t) = + FunctionBinding Nothing l Nothing Nothing (denote t) + -- | The \"opposite\" of `denote`, like @first absurd@ but faster renote :: Expr Void a -> Expr s a renote = unsafeCoerce diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index a375d07c3..d5199e49e 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -56,6 +56,7 @@ import Dhall.Syntax , Chunks (..) , Const (..) , Expr (..) + , FunctionBinding (..) , PreferAnnotation (..) , RecordField (..) , Var (..) @@ -227,7 +228,7 @@ infer typer = loop go types n0 - Lam x _A b -> do + Lam (FunctionBinding { fbVariable = x, fbAnnotation = _A}) b -> do tA' <- loop ctx _A case tA' of diff --git a/dhall/tests/Dhall/Test/QuickCheck.hs b/dhall/tests/Dhall/Test/QuickCheck.hs index 2e5aa4b46..6bc12c125 100644 --- a/dhall/tests/Dhall/Test/QuickCheck.hs +++ b/dhall/tests/Dhall/Test/QuickCheck.hs @@ -39,6 +39,7 @@ import Dhall.Core , Expr (..) , File (..) , FilePrefix (..) + , FunctionBinding (..) , Import (..) , ImportHashed (..) , ImportMode (..) @@ -60,7 +61,7 @@ import Dhall.Set (Set) import Dhall.Src (Src (..)) import Dhall.Test.Format (format) import Dhall.TypeCheck (TypeError, Typer) -import Generic.Random ((:+) (..), W, Weights, (%), ConstrGen(..)) +import Generic.Random ((:+) (..), ConstrGen (..), W, Weights, (%)) import Test.QuickCheck ( Arbitrary (..) , Gen @@ -282,6 +283,14 @@ instance (Arbitrary s, Arbitrary a) => Arbitrary (RecordField s a) where shrink = genericShrink +instance (Arbitrary s, Arbitrary a) => Arbitrary (FunctionBinding s a) where + arbitrary = do + l <- label + type_ <- arbitrary + return $ FunctionBinding Nothing l Nothing Nothing type_ + + shrink = genericShrink + instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where arbitrary = Test.QuickCheck.suchThat @@ -292,7 +301,7 @@ instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where standardizedExpression where customGens - :: ConstrGen "Lam" 0 Text + :: ConstrGen "Lam" 0 (FunctionBinding s a) :+ ConstrGen "Pi" 0 Text :+ ConstrGen "Field" 1 Text :+ ConstrGen "Project" 1 (Either (Set Text) (Expr s a)) @@ -300,7 +309,7 @@ instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where :+ Gen Text -- Generates all Text fields in Expr :+ () customGens = - ConstrGen label + ConstrGen arbitrary :+ ConstrGen label :+ ConstrGen label :+ ConstrGen projection From 3dd92d171a1382e081e8a6b75c408464b27e5262 Mon Sep 17 00:00:00 2001 From: German Robayo Date: Thu, 6 Aug 2020 11:15:53 -0400 Subject: [PATCH 2/5] remove COMPLETE pragma list --- dhall/src/Dhall/Syntax.hs | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/dhall/src/Dhall/Syntax.hs b/dhall/src/Dhall/Syntax.hs index 415a56cd5..ca0a9f8f4 100644 --- a/dhall/src/Dhall/Syntax.hs +++ b/dhall/src/Dhall/Syntax.hs @@ -561,19 +561,6 @@ data Expr s a -- NB: If you add a constructor to Expr, please also update the Arbitrary -- instance in Dhall.Test.QuickCheck. --- {-# COMPLETE Lam, Var, Pi, App, Let, Annot, Bool, BoolLit, BoolAnd, --- BoolOr, BoolEQ, BoolNE, BoolIf, Natural, NaturalLit, NaturalFold, --- NaturalBuild, NaturalIsZero, NaturalEven, NaturalOdd, --- NaturalToInteger, NaturalShow, NaturalSubtract, NaturalPlus, --- NaturalTimes, Integer, IntegerLit, IntegerClamp, IntegerNegate, --- IntegerShow, IntegerToDouble, Double, DoubleLit, DoubleShow, Text, --- TextLit, TextAppend, TextShow, List, ListLit, ListAppend, --- ListBuild, ListFold, ListLength, ListHead, ListLast, ListIndexed, --- ListReverse, Optional, Some, None, Record, RecordLit, Union, --- Combine, CombineTypes, Prefer, RecordCompletion, Merge, ToMap, --- Field, Project, Assert, Equivalent, With, Note, ImportAlt, Embed --- #-} - -- | This instance encodes what the Dhall standard calls an \"exact match\" -- between two expressions. -- From c567df7e00f329974cfb446aa0d1a2ddcb1ca945 Mon Sep 17 00:00:00 2001 From: German Robayo Date: Thu, 6 Aug 2020 12:09:43 -0400 Subject: [PATCH 3/5] add haddocks for makeFunctionBinding --- dhall/src/Dhall/Syntax.hs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/dhall/src/Dhall/Syntax.hs b/dhall/src/Dhall/Syntax.hs index ca0a9f8f4..5d01b3652 100644 --- a/dhall/src/Dhall/Syntax.hs +++ b/dhall/src/Dhall/Syntax.hs @@ -339,16 +339,10 @@ data FunctionBinding s a = FunctionBinding , fbAnnotation :: Expr s a } deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable) +-- | Smart constructor for 'FunctionBinding' with no src information makeFunctionBinding :: Text -> Expr s a -> FunctionBinding s a makeFunctionBinding l t = FunctionBinding Nothing l Nothing Nothing t --- pattern Lam :: Text -> Expr s a -> Expr s a -> Expr s a --- pattern Lam l t e <- Lam (FunctionBinding _ l _ _ t) e --- where --- Lam l t e = Lam (FunctionBinding Nothing l Nothing Nothing t) e - --- {-# COMPLETE Lam #-} - instance Bifunctor FunctionBinding where first k (FunctionBinding src0 label src1 src2 type_) = FunctionBinding (k <$> src0) label (k <$> src1) (k <$> src2) (first k type_) From ede1fc8109c2e1c6908a953e12ee9d35aff90b5a Mon Sep 17 00:00:00 2001 From: German Robayo Date: Fri, 7 Aug 2020 11:09:00 -0400 Subject: [PATCH 4/5] use full `functionBinding` prefix for FunctionBinding attributes --- dhall-json/src/Dhall/JSON.hs | 8 ++++---- .../src/Dhall/LSP/Backend/Completion.hs | 2 +- .../src/Dhall/LSP/Backend/Typing.hs | 16 ++++++++------- dhall-nix/src/Dhall/Nix.hs | 6 +++--- dhall/src/Dhall.hs | 6 ++++-- dhall/src/Dhall/Binary.hs | 4 ++-- dhall/src/Dhall/Diff.hs | 4 ++-- dhall/src/Dhall/Eval.hs | 2 +- dhall/src/Dhall/Normalize.hs | 6 +++--- dhall/src/Dhall/Pretty/Internal.hs | 2 +- dhall/src/Dhall/Syntax.hs | 20 +++++++++---------- dhall/src/Dhall/TypeCheck.hs | 2 +- 12 files changed, 41 insertions(+), 37 deletions(-) diff --git a/dhall-json/src/Dhall/JSON.hs b/dhall-json/src/Dhall/JSON.hs index 7b0990697..ac6454066 100644 --- a/dhall-json/src/Dhall/JSON.hs +++ b/dhall-json/src/Dhall/JSON.hs @@ -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.fbAnnotation -> Core.Const Core.Type) - (Core.Lam (Core.fbAnnotation -> + 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)) @@ -542,8 +542,8 @@ dhallToJSON e0 = loop (Core.alphaNormalize (Core.normalize e0)) outer _ = Left (Unsupported e) outer value - Core.Lam (Core.fbAnnotation -> Core.Const Core.Type) - (Core.Lam (Core.fbAnnotation -> + 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)) diff --git a/dhall-lsp-server/src/Dhall/LSP/Backend/Completion.hs b/dhall-lsp-server/src/Dhall/LSP/Backend/Completion.hs index 01a17dc43..d1b1f6c02 100644 --- a/dhall-lsp-server/src/Dhall/LSP/Backend/Completion.hs +++ b/dhall-lsp-server/src/Dhall/LSP/Backend/Completion.hs @@ -124,7 +124,7 @@ buildCompletionContext' context values (Let (Binding { variable = x, annotation in buildCompletionContext' context' values' e -buildCompletionContext' context values (Lam (FunctionBinding { fbVariable = x, fbAnnotation = _A}) b) = +buildCompletionContext' context values (Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A}) b) = let _A' | Right _ <- typeWithA absurd context _A = normalize _A | otherwise = holeExpr diff --git a/dhall-lsp-server/src/Dhall/LSP/Backend/Typing.hs b/dhall-lsp-server/src/Dhall/LSP/Backend/Typing.hs index bf691887a..a47025e0b 100644 --- a/dhall-lsp-server/src/Dhall/LSP/Backend/Typing.hs +++ b/dhall-lsp-server/src/Dhall/LSP/Backend/Typing.hs @@ -50,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 FunctionBinding { fbAnnotation = _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 @@ -64,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 FunctionBinding { fbVariable = x, fbAnnotation = _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 @@ -137,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 FunctionBinding{ fbVariable = x, fbAnnotation = _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 diff --git a/dhall-nix/src/Dhall/Nix.hs b/dhall-nix/src/Dhall/Nix.hs index ac6f18747..f8826d42d 100644 --- a/dhall-nix/src/Dhall/Nix.hs +++ b/dhall-nix/src/Dhall/Nix.hs @@ -237,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 FunctionBinding {fbVariable = x', fbAnnotation = 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) @@ -272,7 +272,7 @@ dhallToNix e = x' = x <> Data.Text.pack (show n) renameShadowed :: Expr s Void -> Maybe (Expr s Void) - renameShadowed (Lam FunctionBinding { fbVariable = x, fbAnnotation = a} b) = do + renameShadowed (Lam FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = a} b) = do (x', b') <- rename (x, b) return (Lam (Dhall.Core.makeFunctionBinding x' a) b') @@ -294,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 FunctionBinding { fbVariable = a } c) = do + loop (Lam FunctionBinding { functionBindingVariable = a } c) = do c' <- loop c return (Fix (NAbs (Param a) c')) loop (Pi _ _ _) = return untranslatable diff --git a/dhall/src/Dhall.hs b/dhall/src/Dhall.hs index 9f914206c..cce65360f 100644 --- a/dhall/src/Dhall.hs +++ b/dhall/src/Dhall.hs @@ -1362,10 +1362,12 @@ instance (Functor f, FromDhall (f (Result f))) => FromDhall (Fix f) where where die = typeError expected expr0 - extract0 (Lam (FunctionBinding { fbVariable = x }) expr) = extract1 (rename x "result" expr) + extract0 (Lam (FunctionBinding { functionBindingVariable = x }) expr) = + extract1 (rename x "result" expr) extract0 _ = die - extract1 (Lam (FunctionBinding { fbVariable = 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) diff --git a/dhall/src/Dhall/Binary.hs b/dhall/src/Dhall/Binary.hs index b61954b10..00fccee83 100644 --- a/dhall/src/Dhall/Binary.hs +++ b/dhall/src/Dhall/Binary.hs @@ -707,13 +707,13 @@ encodeExpressionInternal encodeEmbed = go where (function, arguments) = unApply a - Lam (FunctionBinding { fbVariable = "_", fbAnnotation = _A }) b -> + Lam (FunctionBinding { functionBindingVariable = "_", functionBindingAnnotation = _A }) b -> encodeList3 (Encoding.encodeInt 1) (go _A) (go b) - Lam (FunctionBinding { fbVariable = x, fbAnnotation = _A }) b -> + Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A }) b -> encodeList4 (Encoding.encodeInt 1) (Encoding.encodeString x) diff --git a/dhall/src/Dhall/Diff.hs b/dhall/src/Dhall/Diff.hs index 7f8949bb1..f9985cd89 100644 --- a/dhall/src/Dhall/Diff.hs +++ b/dhall/src/Dhall/Diff.hs @@ -647,8 +647,8 @@ diff l@(Lam {}) r@(Lam {}) = enclosed' " " (rarrow <> " ") (docs l r) where docs - (Lam (FunctionBinding { fbVariable = aL, fbAnnotation = bL }) cL) - (Lam (FunctionBinding { fbVariable = aR, fbAnnotation = bR }) cR) = + (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 diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs index 1831d15c2..edb3f8d25 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -390,7 +390,7 @@ eval !env t0 = VConst k Var v -> vVar env v - Lam (FunctionBinding { fbVariable = x, fbAnnotation = 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) diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs index a953519ea..c7ee8e1e2 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -202,7 +202,7 @@ boundedType _ = False >>> mfb = Syntax.makeFunctionBinding >>> alphaNormalize (Lam (mfb "a" (Const Type)) (Lam (mfb "b" (Const Type)) (Lam (mfb "x" "a") (Lam (mfb "y" "b") "x")))) -Lam (FunctionBinding {fbSrc0 = Nothing, fbVariable = "_", fbSrc1 = Nothing, fbSrc2 = Nothing, fbAnnotation = Const Type}) (Lam (FunctionBinding {fbSrc0 = Nothing, fbVariable = "_", fbSrc1 = Nothing, fbSrc2 = Nothing, fbAnnotation = Const Type}) (Lam (FunctionBinding {fbSrc0 = Nothing, fbVariable = "_", fbSrc1 = Nothing, fbSrc2 = Nothing, fbAnnotation = Var (V "_" 1)}) (Lam (FunctionBinding {fbSrc0 = Nothing, fbVariable = "_", fbSrc1 = Nothing, fbSrc2 = Nothing, fbAnnotation = Var (V "_" 1)}) (Var (V "_" 1))))) +Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Const Type}) (Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Lam (FunctionBinding {functionBindingSrc0 = Nothing, functionBindingVariable = "_", functionBindingSrc1 = Nothing, functionBindingSrc2 = Nothing, functionBindingAnnotation = Var (V "_" 1)}) (Var (V "_" 1))))) α-normalization does not affect free variables: @@ -261,7 +261,7 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) loop e = case e of Const k -> pure (Const k) Var v -> pure (Var v) - Lam (FunctionBinding { fbVariable = x, fbAnnotation = _A }) b -> + Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A }) b -> Lam <$> (Syntax.makeFunctionBinding x <$> _A') <*> b' where _A' = loop _A @@ -738,7 +738,7 @@ isNormalized e0 = loop (Syntax.denote e0) loop e = case e of Const _ -> True Var _ -> True - Lam (Syntax.fbAnnotation -> a) b -> loop a && loop b + Lam (Syntax.functionBindingAnnotation -> a) b -> loop a && loop b Pi _ a b -> loop a && loop b App f a -> loop f && loop a && case App f a of App (Lam _ _) _ -> False diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs index 9ba2b3e92..89b3f6adc 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -536,7 +536,7 @@ prettyCharacterSet characterSet expression = prettyExpression a0@(Lam _ _) = arrows characterSet (docs a0) where - docs (Lam (FunctionBinding { fbVariable = a, fbAnnotation = b }) c) = + docs (Lam (FunctionBinding { functionBindingVariable = a, functionBindingAnnotation = b }) c) = Pretty.group (Pretty.flatAlt long short) : docs c where long = (lambda characterSet <> space) diff --git a/dhall/src/Dhall/Syntax.hs b/dhall/src/Dhall/Syntax.hs index 5d01b3652..fe62bae31 100644 --- a/dhall/src/Dhall/Syntax.hs +++ b/dhall/src/Dhall/Syntax.hs @@ -325,18 +325,18 @@ For example, > λ({- A -} a {- B -} : {- C -} T) -> e will be instantiated as follows: -* @fbSrc0@ corresponds to the @A@ comment -* @fbVariable@ is @a@ -* @fbSrc1@ corresponds to the @B@ comment -* @fbSrc2@ corresponds to the @C@ comment -* @fbAnnotation@ is @T@ +* @functionBindingSrc0@ corresponds to the @A@ comment +* @functionBindingVariable@ is @a@ +* @functionBindingSrc1@ corresponds to the @B@ comment +* @functionBindingSrc2@ corresponds to the @C@ comment +* @functionBindingAnnotation@ is @T@ -} data FunctionBinding s a = FunctionBinding - { fbSrc0 :: Maybe s - , fbVariable :: Text - , fbSrc1 :: Maybe s - , fbSrc2 :: Maybe s - , fbAnnotation :: Expr s a + { functionBindingSrc0 :: Maybe s + , functionBindingVariable :: Text + , functionBindingSrc1 :: Maybe s + , functionBindingSrc2 :: Maybe s + , functionBindingAnnotation :: Expr s a } deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable) -- | Smart constructor for 'FunctionBinding' with no src information diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index d5199e49e..f66e74c2a 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -228,7 +228,7 @@ infer typer = loop go types n0 - Lam (FunctionBinding { fbVariable = x, fbAnnotation = _A}) b -> do + Lam (FunctionBinding { functionBindingVariable = x, functionBindingAnnotation = _A}) b -> do tA' <- loop ctx _A case tA' of From 9f5682828c3c8732b61e3b5fe9f336eddd4a891a Mon Sep 17 00:00:00 2001 From: German Robayo Date: Fri, 7 Aug 2020 11:09:41 -0400 Subject: [PATCH 5/5] use Syntax.makeFunctionBinding instead of mfb in `freeIn` haddock --- dhall/src/Dhall/Normalize.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs index c7ee8e1e2..3e5b7cb4e 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -922,7 +922,7 @@ isNormalized e0 = loop (Syntax.denote e0) True >>> "x" `freeIn` "y" False ->>> "x" `freeIn` Lam (mfb "x" (Const Type)) "x" +>>> "x" `freeIn` Lam (Syntax.makeFunctionBinding "x" (Const Type)) "x" False -} freeIn :: Eq a => Var -> Expr s a -> Bool