From 8a5bfaa3b9d1c697d9703f984f3fd866a06c21c0 Mon Sep 17 00:00:00 2001 From: Gabriel Gonzalez Date: Tue, 13 Nov 2018 08:01:59 -0800 Subject: [PATCH] Add support for multi-`let` (#675) ... as standardized in: https://github.com/dhall-lang/dhall-lang/pull/266 This also adds `dhall lint` support for consolidating nested `let` expressions --- dhall-json/src/Dhall/JSON.hs | 15 ++- .../deep-nested-large-record/Main.hs | 17 ++- dhall/src/Dhall/Binary.hs | 60 ++++++--- dhall/src/Dhall/Core.hs | 124 ++++++++++++++---- dhall/src/Dhall/Diff.hs | 19 +-- dhall/src/Dhall/Import.hs | 5 +- dhall/src/Dhall/Lint.hs | 28 +++- dhall/src/Dhall/Parser/Expression.hs | 30 +++-- dhall/src/Dhall/Pretty/Internal.hs | 49 +++---- dhall/src/Dhall/Repl.hs | 3 +- dhall/src/Dhall/TypeCheck.hs | 13 +- dhall/tests/QuickCheck.hs | 17 ++- dhall/tests/format/importLinesA.dhall | 10 +- dhall/tests/format/importLinesB.dhall | 12 +- dhall/tests/format/sha256PrintingB.dhall | 4 +- 15 files changed, 278 insertions(+), 128 deletions(-) diff --git a/dhall-json/src/Dhall/JSON.hs b/dhall-json/src/Dhall/JSON.hs index cc5c487ea..aa3dddd1f 100644 --- a/dhall-json/src/Dhall/JSON.hs +++ b/dhall-json/src/Dhall/JSON.hs @@ -386,12 +386,17 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Dhall.Core.normalize e0) a' = loop a b' = loop b - Dhall.Core.Let a b c d -> - Dhall.Core.Let a b' c' d' + Dhall.Core.Let as b -> + Dhall.Core.Let as' b' where - b' = fmap loop b - c' = loop c - d' = loop d + f (Dhall.Core.Binding x y z) = Dhall.Core.Binding x y' z' + where + y' = fmap loop y + z' = loop z + + as' = fmap f as + + b' = loop b Dhall.Core.Annot a b -> Dhall.Core.Annot a' b' diff --git a/dhall/benchmark/deep-nested-large-record/Main.hs b/dhall/benchmark/deep-nested-large-record/Main.hs index 7a986eafd..7e1b9fbd3 100644 --- a/dhall/benchmark/deep-nested-large-record/Main.hs +++ b/dhall/benchmark/deep-nested-large-record/Main.hs @@ -25,7 +25,7 @@ issue412 :: Core.Expr s TypeCheck.X -> Criterion.Benchmarkable issue412 prelude = Criterion.whnf TypeCheck.typeOf expr where expr - = Core.Let "prelude" Nothing prelude + = Core.Let (pure (Core.Binding "prelude" Nothing prelude)) $ Core.ListLit Nothing $ Seq.replicate 5 $ Core.Var (Core.V "prelude" 0) `Core.Field` "types" `Core.Field` "Little" `Core.Field` "Foo" @@ -33,12 +33,15 @@ issue412 prelude = Criterion.whnf TypeCheck.typeOf expr unionPerformance :: Core.Expr s TypeCheck.X -> Criterion.Benchmarkable unionPerformance prelude = Criterion.whnf TypeCheck.typeOf expr where - expr = - Core.Let "x" Nothing - (Core.Let "big" Nothing (prelude `Core.Field` "types" `Core.Field` "Big") - (Core.Prefer "big" "big") - ) - "x" + innerBinding = + Core.Binding "big" Nothing + (prelude `Core.Field` "types" `Core.Field` "Big") + + outerBinding = + Core.Binding "x" Nothing + (Core.Let (pure innerBinding) (Core.Prefer "big" "big")) + + expr = Core.Let (pure outerBinding) "x" main :: IO () main = do diff --git a/dhall/src/Dhall/Binary.hs b/dhall/src/Dhall/Binary.hs index aaaf2c1a6..0034fe1c6 100644 --- a/dhall/src/Dhall/Binary.hs +++ b/dhall/src/Dhall/Binary.hs @@ -24,7 +24,8 @@ import Codec.CBOR.Term (Term(..)) import Control.Applicative (empty) import Control.Exception (Exception) import Dhall.Core - ( Chunks(..) + ( Binding(..) + , Chunks(..) , Const(..) , Directory(..) , Expr(..) @@ -38,12 +39,13 @@ import Dhall.Core , URL(..) , Var(..) ) +import Data.Foldable (toList) +import Data.List.NonEmpty (NonEmpty(..)) import Data.Monoid ((<>)) import Data.Text (Text) import Options.Applicative (Parser) import Prelude hiding (exponent) -import qualified Data.Foldable import qualified Data.Scientific import qualified Data.Sequence import qualified Data.Text @@ -352,17 +354,21 @@ encode (TextLit (Chunks xys₀ z₀)) = z₁ = TString z₀ encode (Embed x) = importToTerm x -encode (Let x Nothing a₀ b₀) = - TList [ TInt 25, TString x, a₁, b₁ ] +encode (Let as₀ b₀) = + TList ([ TInt 25 ] ++ as₁ ++ [ b₁ ]) where - a₁ = encode a₀ + as₁ = do + Binding x mA₀ a₀ <- toList as₀ + + let mA₁ = case mA₀ of + Nothing -> TNull + Just _A₀ -> encode _A₀ + + let a₁ = encode a₀ + + [ TString x, mA₁, a₁ ] + b₁ = encode b₀ -encode (Let x (Just _A₀) a₀ b₀) = - TList [ TInt 25, TString x, _A₁, a₁, b₁ ] - where - a₁ = encode a₀ - _A₁ = encode _A₀ - b₁ = encode b₀ encode (Annot t₀ _T₀) = TList [ TInt 26, t₁, _T₁ ] where @@ -722,15 +728,29 @@ decode (TList (TInt 24 : TInt n : xs)) = do let importHashed = ImportHashed {..} let importMode = Code return (Embed (Import {..})) -decode (TList [ TInt 25, TString x, a₁, b₁ ]) = do - a₀ <- decode a₁ - b₀ <- decode b₁ - return (Let x Nothing a₀ b₀) -decode (TList [ TInt 25, TString x, _A₁, a₁, b₁ ]) = do - _A₀ <- decode _A₁ - a₀ <- decode a₁ - b₀ <- decode b₁ - return (Let x (Just _A₀) a₀ b₀) +decode (TList (TInt 25 : xs)) = do + let process (TString x : _A₁ : a₁ : ls₁) = do + mA₀ <- case _A₁ of + TNull -> return Nothing + _ -> fmap Just (decode _A₁) + + a₀ <- decode a₁ + + let binding = Binding x mA₀ a₀ + + case ls₁ of + [ b₁ ] -> do + b₀ <- decode b₁ + + return (Let (binding :| []) b₀) + _ -> do + Let (l₀ :| ls₀) b₀ <- process ls₁ + + return (Let (binding :| (l₀ : ls₀)) b₀) + process _ = do + empty + + process xs decode (TList [ TInt 26, t₁, _T₁ ]) = do t₀ <- decode t₁ _T₀ <- decode _T₁ diff --git a/dhall/src/Dhall/Core.hs b/dhall/src/Dhall/Core.hs index 2f3737ac3..f286f23f5 100644 --- a/dhall/src/Dhall/Core.hs +++ b/dhall/src/Dhall/Core.hs @@ -29,6 +29,7 @@ module Dhall.Core ( , Path , Scheme(..) , Var(..) + , Binding(..) , Chunks(..) , Expr(..) @@ -69,6 +70,7 @@ import Data.Data (Data) import Data.Foldable import Data.Functor.Identity (Identity(..)) import Data.HashSet (HashSet) +import Data.List.NonEmpty (NonEmpty(..)) import Data.String (IsString(..)) import Data.Scientific (Scientific) import Data.Semigroup (Semigroup(..)) @@ -333,9 +335,9 @@ data Expr s a | Pi Text (Expr s a) (Expr s a) -- | > App f a ~ f a | App (Expr s a) (Expr s a) - -- | > Let x Nothing r e ~ let x = r in e - -- > Let x (Just t) r e ~ let x : t = r in e - | Let Text (Maybe (Expr s a)) (Expr s a) (Expr s a) + -- | > Let [Binding x Nothing r] e ~ let x = r in e + -- > Let [Binding x (Just t) r] e ~ let x : t = r in e + | Let (NonEmpty (Binding s a)) (Expr s a) -- | > Annot x t ~ x : t | Annot (Expr s a) (Expr s a) -- | > Bool ~ Bool @@ -469,7 +471,7 @@ instance Functor (Expr s) where fmap f (Lam v e1 e2) = Lam v (fmap f e1) (fmap f e2) fmap f (Pi v e1 e2) = Pi v (fmap f e1) (fmap f e2) fmap f (App e1 e2) = App (fmap f e1) (fmap f e2) - fmap f (Let v maybeE e1 e2) = Let v (fmap (fmap f) maybeE) (fmap f e1) (fmap f e2) + fmap f (Let as b) = Let (fmap (fmap f) as) (fmap f b) fmap f (Annot e1 e2) = Annot (fmap f e1) (fmap f e2) fmap _ Bool = Bool fmap _ (BoolLit b) = BoolLit b @@ -544,7 +546,9 @@ instance Monad (Expr s) where Lam a b c >>= k = Lam a (b >>= k) (c >>= k) Pi a b c >>= k = Pi a (b >>= k) (c >>= k) App a b >>= k = App (a >>= k) (b >>= k) - Let a b c d >>= k = Let a (fmap (>>= k) b) (c >>= k) (d >>= k) + Let as b >>= k = Let (fmap f as) (b >>= k) + where + f (Binding c d e) = Binding c (fmap (>>= k) d) (e >>= k) Annot a b >>= k = Annot (a >>= k) (b >>= k) Bool >>= _ = Bool BoolLit a >>= _ = BoolLit a @@ -611,7 +615,7 @@ instance Bifunctor Expr where first k (Lam a b c ) = Lam a (first k b) (first k c) first k (Pi a b c ) = Pi a (first k b) (first k c) first k (App a b ) = App (first k a) (first k b) - first k (Let a b c d ) = Let a (fmap (first k) b) (first k c) (first k d) + first k (Let as b ) = Let (fmap (first k) as) (first k b) first k (Annot a b ) = Annot (first k a) (first k b) first _ Bool = Bool first _ (BoolLit a ) = BoolLit a @@ -677,6 +681,17 @@ instance Bifunctor Expr where instance IsString (Expr s a) where fromString str = Var (fromString str) +data Binding s a = Binding + { variable :: Text + , annotation :: Maybe (Expr s a) + , value :: Expr s a + } deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Data) + +instance Bifunctor Binding where + first k (Binding a b c) = Binding a (fmap (first k) b) (first k c) + + second = fmap + -- | The body of an interpolated @Text@ literal data Chunks s a = Chunks [(Text, Expr s a)] Text deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Data) @@ -794,14 +809,24 @@ shift d v (App f a) = App f' a' where f' = shift d v f a' = shift d v a -shift d (V x n) (Let f mt r e) = Let f mt' r' e' +shift d (V x₀ n₀) (Let (Binding x₁ mA₀ a₀ :| []) b₀) = + Let (Binding x₁ mA₁ a₁ :| []) b₁ where - e' = shift d (V x n') e - where - n' = if x == f then n + 1 else n + n₁ = if x₀ == x₁ then n₀ + 1 else n₀ + + mA₁ = fmap (shift d (V x₀ n₀)) mA₀ + a₁ = shift d (V x₀ n₀) a₀ + + b₁ = shift d (V x₀ n₁) b₀ +shift d (V x₀ n₀) (Let (Binding x₁ mA₀ a₀ :| (l₀ : ls₀)) b₀) = + Let (Binding x₁ mA₁ a₁ :| (l₁ : ls₁)) b₁ + where + n₁ = if x₀ == x₁ then n₀ + 1 else n₀ + + mA₁ = fmap (shift d (V x₀ n₀)) mA₀ + a₁ = shift d (V x₀ n₀) a₀ - mt' = fmap (shift d (V x n)) mt - r' = shift d (V x n) r + Let (l₁ :| ls₁) b₁ = shift d (V x₀ n₁) (Let (l₀ :| ls₀) b₀) shift d v (Annot a b) = Annot a' b' where a' = shift d v a @@ -959,14 +984,28 @@ subst v e (App f a) = App f' a' f' = subst v e f a' = subst v e a subst v e (Var v') = if v == v' then e else Var v' -subst (V x n) e (Let f mt r b) = Let f mt' r' b' +subst (V x₀ n₀) e₀ (Let (Binding x₁ mA₀ a₀ :| []) b₀) = + Let (Binding x₁ mA₁ a₁ :| []) b₁ where - b' = subst (V x n') (shift 1 (V f 0) e) b - where - n' = if x == f then n + 1 else n + n₁ = if x₀ == x₁ then n₀ + 1 else n₀ + + e₁ = shift 1 (V x₁ 0) e₀ + + mA₁ = fmap (subst (V x₀ n₀) e₀) mA₀ + a₁ = subst (V x₀ n₀) e₀ a₀ + + b₁ = subst (V x₀ n₁) e₁ b₀ +subst (V x₀ n₀) e₀ (Let (Binding x₁ mA₀ a₀ :| (l₀ : ls₀)) b₀) = + Let (Binding x₁ mA₁ a₁ :| (l₁ : ls₁)) b₁ + where + n₁ = if x₀ == x₁ then n₀ + 1 else n₀ + + e₁ = shift 1 (V x₁ 0) e₀ - mt' = fmap (subst (V x n) e) mt - r' = subst (V x n) e r + mA₁ = fmap (subst (V x₀ n₀) e₀) mA₀ + a₁ = subst (V x₀ n₀) e₀ a₀ + + Let (l₁ :| ls₁) b₁ = subst (V x₀ n₁) e₁ (Let (l₀ :| ls₀) b₀) subst x e (Annot a b) = Annot a' b' where a' = subst x e a @@ -1145,14 +1184,22 @@ alphaNormalize (App f₀ a₀) = f₁ = alphaNormalize f₀ a₁ = alphaNormalize a₀ -alphaNormalize (Let "_" mA₀ a₀ b₀) = - Let "_" mA₁ a₁ b₁ +alphaNormalize (Let (Binding "_" mA₀ a₀ :| []) b₀) = + Let (Binding "_" mA₁ a₁ :| []) b₁ where mA₁ = fmap alphaNormalize mA₀ a₁ = alphaNormalize a₀ + b₁ = alphaNormalize b₀ -alphaNormalize (Let x mA₀ a₀ b₀) = - Let "_" mA₁ a₁ b₄ +alphaNormalize (Let (Binding "_" mA₀ a₀ :| (l₀ : ls₀)) b₀) = + Let (Binding "_" mA₁ a₁ :| (l₁ : ls₁)) b₁ + where + mA₁ = fmap alphaNormalize mA₀ + a₁ = alphaNormalize a₀ + + Let (l₁ :| ls₁) b₁ = alphaNormalize (Let (l₀ :| ls₀) b₀) +alphaNormalize (Let (Binding x mA₀ a₀ :| []) b₀) = + Let (Binding "_" mA₁ a₁ :| []) b₄ where mA₁ = fmap alphaNormalize mA₀ a₁ = alphaNormalize a₀ @@ -1161,6 +1208,17 @@ alphaNormalize (Let x mA₀ a₀ b₀) = b₂ = subst (V x 0) (Var (V "_" 0)) b₁ b₃ = shift (-1) (V x 0) b₂ b₄ = alphaNormalize b₃ +alphaNormalize (Let (Binding x mA₀ a₀ :| (l₀ : ls₀)) b₀) = + Let (Binding "_" mA₁ a₁ :| (l₁ : ls₁)) b₄ + where + mA₁ = fmap alphaNormalize mA₀ + a₁ = alphaNormalize a₀ + + b₁ = shift 1 (V "_" 0) b₀ + b₂ = subst (V x 0) (Var (V "_" 0)) b₁ + b₃ = shift (-1) (V x 0) b₂ + + Let (l₁ :| ls₁) b₄ = alphaNormalize (Let (l₀ :| ls₀) b₃) alphaNormalize (Annot t₀ _T₀) = Annot t₁ _T₁ where @@ -1420,7 +1478,9 @@ denote (Var a ) = Var a denote (Lam a b c ) = Lam a (denote b) (denote c) denote (Pi a b c ) = Pi a (denote b) (denote c) denote (App a b ) = App (denote a) (denote b) -denote (Let a b c d ) = Let a (fmap denote b) (denote c) (denote d) +denote (Let as b ) = Let (fmap f as) (denote b) + where + f (Binding c d e) = Binding c (fmap denote d) (denote e) denote (Annot a b ) = Annot (denote a) (denote b) denote Bool = Bool denote (BoolLit a ) = BoolLit a @@ -1640,11 +1700,15 @@ normalizeWithM ctx e0 = loop (denote e0) case res of Nothing -> pure (App f' a') Just app' -> loop app' - Let f _ r b -> loop b'' + Let (Binding x _ a₀ :| ls₀) b₀ -> loop b₂ where - r' = shift 1 (V f 0) r - b' = subst (V f 0) r' b - b'' = shift (-1) (V f 0) b' + rest = case ls₀ of + [] -> b₀ + l₁ : ls₁ -> Let (l₁ :| ls₁) b₀ + + a₁ = shift 1 (V x 0) a₀ + b₁ = subst (V x 0) a₁ rest + b₂ = shift (-1) (V x 0) b₁ Annot x _ -> loop x Bool -> pure Bool BoolLit b -> pure (BoolLit b) @@ -1946,7 +2010,7 @@ isNormalized e0 = loop (denote e0) App (App (App (App (App OptionalFold _) (App None _)) _) _) _ -> False _ -> True - Let _ _ _ _ -> False + Let _ _ -> False Annot _ _ -> False Bool -> True BoolLit _ -> True @@ -2200,7 +2264,9 @@ subExpressions _ (Var v) = pure (Var v) subExpressions f (Lam a b c) = Lam a <$> f b <*> f c subExpressions f (Pi a b c) = Pi a <$> f b <*> f c subExpressions f (App a b) = App <$> f a <*> f b -subExpressions f (Let a b c d) = Let a <$> traverse f b <*> f c <*> f d +subExpressions f (Let as b) = Let <$> traverse g as <*> f b + where + g (Binding c d e) = Binding c <$> traverse f d <*> f e subExpressions f (Annot a b) = Annot <$> f a <*> f b subExpressions _ Bool = pure Bool subExpressions _ (BoolLit b) = pure (BoolLit b) diff --git a/dhall/src/Dhall/Diff.hs b/dhall/src/Dhall/Diff.hs index 71185b935..ee88f80c9 100644 --- a/dhall/src/Dhall/Diff.hs +++ b/dhall/src/Dhall/Diff.hs @@ -25,7 +25,7 @@ import Data.Sequence (Seq) import Data.String (IsString(..)) import Data.Text (Text) import Data.Text.Prettyprint.Doc (Doc, Pretty) -import Dhall.Core (Chunks (..), Const(..), Expr(..), Var(..)) +import Dhall.Core (Binding(..), Chunks (..), Const(..), Expr(..), Var(..)) import Dhall.Map (Map) import Dhall.Set (Set) import Dhall.Pretty.Internal (Ann) @@ -701,20 +701,21 @@ diffExpression l@(BoolIf {}) r = mismatch l r diffExpression l r@(BoolIf {}) = mismatch l r -diffExpression l@(Let {}) r@(Let {}) = - enclosed' " " (keyword "in" <> " ") (docs l r) +diffExpression (Let asL bL ) (Let asR bR) = + enclosed' "" (keyword "in" <> " ") + (Data.List.NonEmpty.zipWith docA asL asR <> pure docB) where - docs (Let aL bL cL dL) (Let aR bR cR dR) = - Data.List.NonEmpty.cons (align doc) (docs dL dR) + docA (Binding cL dL eL) (Binding cR dR eR) = align doc where doc = keyword "let" <> " " - <> format " " (diffLabel aL aR) - <> format " " (diffMaybe (colon <> " ") diffExpression bL bR) + <> format " " (diffLabel cL cR) + <> format " " (diffMaybe (colon <> " ") diffExpression dL dR) <> equals <> " " - <> diffExpression cL cR - docs aL aR = pure (diffExpression aL aR) + <> diffExpression eL eR + + docB = diffExpression bL bR diffExpression l@(Let {}) r = mismatch l r diffExpression l r@(Let {}) = diff --git a/dhall/src/Dhall/Import.hs b/dhall/src/Dhall/Import.hs index 6bcce23f1..c920902cd 100644 --- a/dhall/src/Dhall/Import.hs +++ b/dhall/src/Dhall/Import.hs @@ -148,6 +148,7 @@ import System.FilePath (()) import Dhall.Binary (StandardVersion(..)) import Dhall.Core ( Expr(..) + , Binding(..) , Chunks(..) , Directory(..) , File(..) @@ -801,7 +802,9 @@ loadWith expr₀ = case expr₀ of Lam a b c -> Lam <$> pure a <*> loadWith b <*> loadWith c Pi a b c -> Pi <$> pure a <*> loadWith b <*> loadWith c App a b -> App <$> loadWith a <*> loadWith b - Let a b c d -> Let <$> pure a <*> mapM loadWith b <*> loadWith c <*> loadWith d + Let as b -> Let <$> traverse f as <*> loadWith b + where + f (Binding c d e) = Binding c <$> traverse loadWith d <*> loadWith e Annot a b -> Annot <$> loadWith a <*> loadWith b Bool -> pure Bool BoolLit a -> pure (BoolLit a) diff --git a/dhall/src/Dhall/Lint.hs b/dhall/src/Dhall/Lint.hs index c95542378..6d8bec24b 100644 --- a/dhall/src/Dhall/Lint.hs +++ b/dhall/src/Dhall/Lint.hs @@ -5,7 +5,9 @@ module Dhall.Lint lint ) where -import Dhall.Core (Chunks(..), Expr(..), Import, Var(..)) +import Dhall.Core (Binding(..), Chunks(..), Expr(..), Import, Var(..)) +import Data.Semigroup ((<>)) +import Data.List.NonEmpty (NonEmpty(..)) import Dhall.TypeCheck (X(..)) import qualified Dhall.Core @@ -15,6 +17,7 @@ import qualified Dhall.Core Currently this: * removes unused @let@ bindings + * consolidates nested @let@ bindings to use a multiple-@let@ binding * switches legacy @List@-like @Optional@ literals to use @Some@ / @None@ instead -} lint :: Expr s Import -> Expr t Import @@ -36,15 +39,32 @@ lint expression = loop (Dhall.Core.denote expression) where a' = loop a b' = loop b - loop (Let a b c d) + + -- Consolidate nested `let` expresssions + loop (Let a (Let b c)) = loop (Let (a <> b) c) + + -- Remove unused bindings + loop (Let (Binding a b c :| []) d) | not (V a 0 `Dhall.Core.freeIn` d') = d' | otherwise = - Let a b' c' d' + Let (Binding a b' c' :| []) d' + where + b' = fmap loop b + c' = loop c + + d' = loop d + loop (Let (Binding a b c :| (l : ls)) d) + | not (V a 0 `Dhall.Core.freeIn` d') = + Let (l' :| ls') d' + | otherwise = + Let (Binding a b' c' :| (l' : ls')) d' where b' = fmap loop b c' = loop c - d' = loop d + + Let (l' :| ls') d' = loop (Let (l :| ls) d) + loop (Annot a b) = Annot a' b' where diff --git a/dhall/src/Dhall/Parser/Expression.hs b/dhall/src/Dhall/Parser/Expression.hs index 31b6bbc2b..861320b6e 100644 --- a/dhall/src/Dhall/Parser/Expression.hs +++ b/dhall/src/Dhall/Parser/Expression.hs @@ -20,6 +20,7 @@ import qualified Crypto.Hash import qualified Data.ByteArray.Encoding import qualified Data.ByteString import qualified Data.Char +import qualified Data.List.NonEmpty import qualified Data.Sequence import qualified Data.Text import qualified Data.Text.Encoding @@ -82,16 +83,27 @@ completeExpression embedded = completeExpression_ return (BoolIf a b c) alternative2 = do - _let - a <- label - b <- optional (do - _colon - expression ) - _equal - c <- expression + let binding = do + _let + + c <- label + d <- optional (do + _colon + expression ) + + _equal + + e <- expression + + return (Binding c d e) + + as <- Data.List.NonEmpty.some1 binding + _in - d <- expression - return (Let a b c d) + + b <- expression + + return (Let as b) alternative3 = do _forall diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs index e586ea401..851d60393 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -387,50 +387,51 @@ prettyCharacterSet characterSet = prettyExpression ] docsShort (Note _ c) = docsShort c docsShort c = [ prettyExpression c ] - prettyExpression a0@(Let _ _ _ _) = - enclose' "" " " (space <> keyword "in" <> space) (Pretty.hardline <> keyword "in" <> " ") - (fmap duplicate (docs a0)) + prettyExpression (Let as b) = + enclose' "" "" space Pretty.hardline + (fmap duplicate (fmap docA (toList as)) ++ [ docB ]) where - docs (Let a Nothing c d) = - Pretty.group (Pretty.flatAlt long short) : docs d + docA (Binding c Nothing e) = + Pretty.group (Pretty.flatAlt long short) where long = keyword "let" <> space <> Pretty.align - ( prettyLabel a + ( prettyLabel c <> space <> equals <> Pretty.hardline <> " " - <> prettyExpression c + <> prettyExpression e ) short = keyword "let" <> space - <> prettyLabel a + <> prettyLabel c <> (space <> equals <> space) - <> prettyExpression c - docs (Let a (Just b) c d) = - Pretty.group (Pretty.flatAlt long short) : docs d + <> prettyExpression e + docA (Binding c (Just d) e) = + Pretty.group (Pretty.flatAlt long short) where long = keyword "let" <> space <> Pretty.align - ( prettyLabel a + ( prettyLabel c <> Pretty.hardline <> colon <> space - <> prettyExpression b + <> prettyExpression d <> Pretty.hardline <> equals <> space - <> prettyExpression c + <> prettyExpression e ) short = keyword "let" <> space - <> prettyLabel a + <> prettyLabel c <> space <> colon <> space - <> prettyExpression b + <> prettyExpression d <> space <> equals <> space - <> prettyExpression c - docs (Note _ d) = - docs d - docs d = - [ prettyExpression d ] + <> prettyExpression e + + docB = + ( keyword "in" <> " " <> prettyExpression b + , keyword "in" <> " " <> prettyExpression b + ) prettyExpression a0@(Pi _ _ _) = arrows characterSet (fmap duplicate (docs a0)) where @@ -810,15 +811,15 @@ prettyCharacterSet characterSet = prettyExpression short = lparen <> prettyExpression a <> rparen prettyKeyValue :: Pretty a => Doc Ann -> (Text, Expr s a) -> (Doc Ann, Doc Ann) - prettyKeyValue separator (key, value) = - ( prettyLabel key <> " " <> separator <> " " <> prettyExpression value + prettyKeyValue separator (key, val) = + ( prettyLabel key <> " " <> separator <> " " <> prettyExpression val , prettyLabel key <> " " <> separator <> long ) where - long = Pretty.hardline <> " " <> prettyExpression value + long = Pretty.hardline <> " " <> prettyExpression val prettyRecord :: Pretty a => Map Text (Expr s a) -> Doc Ann prettyRecord = diff --git a/dhall/src/Dhall/Repl.hs b/dhall/src/Dhall/Repl.hs index 98478141f..971d8bc4e 100644 --- a/dhall/src/Dhall/Repl.hs +++ b/dhall/src/Dhall/Repl.hs @@ -26,6 +26,7 @@ import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty ( renderIO import qualified Dhall import qualified Dhall.Binary import qualified Dhall.Context +import qualified Dhall.Core import qualified Dhall.Core as Dhall ( Var(V), Expr, normalize ) import qualified Dhall.Pretty import qualified Dhall.Core as Expr ( Expr(..) ) @@ -159,7 +160,7 @@ normalize e = do ( Dhall.normalize ( foldl' ( \a (k, Binding { bindingType, bindingExpr }) -> - Expr.Let k ( Just bindingType ) bindingExpr a + Expr.Let (pure (Dhall.Core.Binding k (Just bindingType) bindingExpr)) a ) e ( Dhall.Context.toList ( envToContext env ) ) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 83adea09d..7d3174b62 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -24,6 +24,7 @@ module Dhall.TypeCheck ( import Control.Exception (Exception) import Data.Data (Data(..)) import Data.Foldable (forM_, toList) +import Data.List.NonEmpty (NonEmpty(..)) import Data.Sequence (Seq, ViewL(..)) import Data.Semigroup (Semigroup(..)) import Data.Set (Set) @@ -31,7 +32,7 @@ import Data.Text (Text) import Data.Text.Prettyprint.Doc (Doc, Pretty(..)) import Data.Traversable (forM) import Data.Typeable (Typeable) -import Dhall.Core (Const(..), Chunks(..), Expr(..), Var(..)) +import Dhall.Core (Binding(..), Const(..), Chunks(..), Expr(..), Var(..)) import Dhall.Context (Context) import Dhall.Pretty (Ann, layoutOpts) @@ -147,7 +148,7 @@ typeWithA tpa = loop let nf_A = Dhall.Core.normalize _A let nf_A' = Dhall.Core.normalize _A' Left (TypeError ctx e (TypeMismatch f nf_A a nf_A')) - loop ctx e@(Let x mA a0 b0) = do + loop ctx e@(Let (Binding x mA a0 :| ls) b0) = do _A1 <- loop ctx a0 case mA of Just _A0 -> do @@ -164,6 +165,10 @@ typeWithA tpa = loop let a1 = Dhall.Core.normalize a0 let a2 = Dhall.Core.shift 1 (V x 0) a1 + let rest = case ls of + [] -> b0 + l' : ls' -> Let (l' :| ls') b0 + -- The catch-all branch directly implements the Dhall -- specification as written; it is necessary to substitute in -- types in order to get 'dependent let' behaviour and to @@ -176,13 +181,13 @@ typeWithA tpa = loop case Dhall.Core.normalize t of Const Type -> do let ctx' = fmap (Dhall.Core.shift 1 (V x 0)) (Dhall.Context.insert x (Dhall.Core.normalize _A1) ctx) - _B0 <- loop ctx' b0 + _B0 <- loop ctx' rest let _B1 = Dhall.Core.subst (V x 0) a2 _B0 let _B2 = Dhall.Core.shift (-1) (V x 0) _B1 return _B2 _ -> do - let b1 = Dhall.Core.subst (V x 0) a2 b0 + let b1 = Dhall.Core.subst (V x 0) a2 rest let b2 = Dhall.Core.shift (-1) (V x 0) b1 loop ctx b2 diff --git a/dhall/tests/QuickCheck.hs b/dhall/tests/QuickCheck.hs index 533d608f9..0c76a1a72 100644 --- a/dhall/tests/QuickCheck.hs +++ b/dhall/tests/QuickCheck.hs @@ -8,9 +8,11 @@ module QuickCheck where import Codec.Serialise (DeserialiseFailure(..)) import Control.Monad (guard) +import Data.List.NonEmpty (NonEmpty(..)) import Dhall.Map (Map) import Dhall.Core - ( Chunks(..) + ( Binding(..) + , Chunks(..) , Const(..) , Directory(..) , Expr(..) @@ -126,6 +128,11 @@ instance (Ord k, Arbitrary k, Arbitrary v) => Arbitrary (Map k v) where . shrink . Dhall.Map.toList +instance (Arbitrary s, Arbitrary a) => Arbitrary (Binding s a) where + arbitrary = lift3 Binding + + shrink = genericShrink + instance (Arbitrary s, Arbitrary a) => Arbitrary (Chunks s a) where arbitrary = do n <- Test.QuickCheck.choose (0, 2) @@ -164,7 +171,13 @@ instance (Arbitrary s, Arbitrary a) => Arbitrary (Expr s a) where , ( 1, Test.QuickCheck.oneof [ lift2 (Lam "_"), lift3 Lam ]) , ( 1, Test.QuickCheck.oneof [ lift2 (Pi "_"), lift3 Pi ]) , ( 1, lift2 App) - , ( 1, Test.QuickCheck.oneof [ lift3 (Let "_"), lift4 Let ]) + , let letExpression = do + n <- Test.QuickCheck.choose (0, 2) + binding <- arbitrary + bindings <- Test.QuickCheck.vectorOf n arbitrary + body <- arbitrary + return (Let (binding :| bindings) body) + in ( 1, Test.QuickCheck.oneof [ letExpression ]) , ( 1, lift2 Annot) , ( 7, lift0 Bool) , ( 7, lift1 BoolLit) diff --git a/dhall/tests/format/importLinesA.dhall b/dhall/tests/format/importLinesA.dhall index 572cfc69e..c132412a7 100644 --- a/dhall/tests/format/importLinesA.dhall +++ b/dhall/tests/format/importLinesA.dhall @@ -1,7 +1,7 @@ let _ = ./emptyRecordA.dhall -in let _ = ./emptyRecordA.dhall -in let _ = ./emptyRecordA.dhall -in let _ = ./emptyRecordA.dhall -in let _ = ./emptyRecordA.dhall -in let _ = ./emptyRecordA.dhall +let _ = ./emptyRecordA.dhall +let _ = ./emptyRecordA.dhall +let _ = ./emptyRecordA.dhall +let _ = ./emptyRecordA.dhall +let _ = ./emptyRecordA.dhall in 123 diff --git a/dhall/tests/format/importLinesB.dhall b/dhall/tests/format/importLinesB.dhall index e9a493581..5780ce31f 100644 --- a/dhall/tests/format/importLinesB.dhall +++ b/dhall/tests/format/importLinesB.dhall @@ -1,13 +1,13 @@ - let _ = ./emptyRecordA.dhall +let _ = ./emptyRecordA.dhall -in let _ = ./emptyRecordA.dhall +let _ = ./emptyRecordA.dhall -in let _ = ./emptyRecordA.dhall +let _ = ./emptyRecordA.dhall -in let _ = ./emptyRecordA.dhall +let _ = ./emptyRecordA.dhall -in let _ = ./emptyRecordA.dhall +let _ = ./emptyRecordA.dhall -in let _ = ./emptyRecordA.dhall +let _ = ./emptyRecordA.dhall in 123 \ No newline at end of file diff --git a/dhall/tests/format/sha256PrintingB.dhall b/dhall/tests/format/sha256PrintingB.dhall index e67308661..898485433 100644 --- a/dhall/tests/format/sha256PrintingB.dhall +++ b/dhall/tests/format/sha256PrintingB.dhall @@ -1,4 +1,4 @@ - let replicate = - https://raw.githubusercontent.com/dhall-lang/Prelude/c79c2bc3c46f129cc5b6d594ce298a381bcae92c/List/replicate sha256:b0e3ec1797b32c80c0bcb7e8254b08c7e9e35e75e6b410c7ac21477ab90167ad +let replicate = + https://raw.githubusercontent.com/dhall-lang/Prelude/c79c2bc3c46f129cc5b6d594ce298a381bcae92c/List/replicate sha256:b0e3ec1797b32c80c0bcb7e8254b08c7e9e35e75e6b410c7ac21477ab90167ad in replicate 5 \ No newline at end of file