Treat multi-lets as syntactic sugar

Closes #1185.

This mostly reverts "Add support for multi-`let` (#675)" /
8a5bfaa.

dhall-json/src/Dhall/JSON.hs

@@ -649,17 +649,12 @@ convertToHomogeneousMaps (Conversion {..}) e0 = loop (Core.normalize e0)
             a' = loop a
             b' = loop b
 
-        Core.Let as b ->
-            Core.Let as' b'
+        Core.Let a b c d ->
+            Core.Let a b' c' d'
           where
-            f (Core.Binding x y z) = Core.Binding x y' z'
-              where
-                y' = fmap loop y
-                z' =      loop z
-
-            as' = fmap f as
-
-            b' = loop b
+            b' = fmap loop b
+            c' =      loop c
+            d' =      loop d
 
         Core.Annot a b ->
             Core.Annot a' b'

dhall-nix/src/Dhall/Nix.hs

@@ -93,7 +93,6 @@ module Dhall.Nix (
 import Control.Exception (Exception)
 import Data.Foldable (toList)
 import Data.Fix (Fix(..))
-import Data.Traversable (for)
 import Data.Typeable (Typeable)
 import Data.Void (absurd)
 import Dhall.Core (Chunks(..), Const(..), Expr(..), Var(..))
@@ -230,12 +229,11 @@ dhallToNix e = loop (Dhall.Core.normalize e)
         a' <- loop a
         b' <- loop b
         return (Fix (NBinary NApp a' b'))
-    loop (Let as b) = do
-        as' <- for as $ \a -> do
-          val <- loop $ Dhall.Core.value a
-          pure $ NamedVar [StaticKey $ Dhall.Core.variable a] val Nix.nullPos
+    loop (Let x _mA a b) = do
+        val <- loop a
+        let var = NamedVar [StaticKey $ x] val Nix.nullPos
         b' <- loop b
-        return (Fix (NLet (toList as') b'))
+        return (Fix (NLet [var] b'))
     loop (Annot a _) = loop a
     loop Bool = return (Fix (NSet []))
     loop (BoolLit b) = return (Fix (NConstant (NBool b)))

dhall/benchmark/deep-nested-large-record/Main.hs

@@ -25,23 +25,20 @@ issue412 :: Core.Expr s TypeCheck.X -> Gauge.Benchmarkable
 issue412 prelude = Gauge.whnf TypeCheck.typeOf expr
   where
     expr
-      = Core.Let (pure (Core.Binding "prelude" Nothing prelude))
+      = Core.Let "prelude" Nothing prelude
       $ Core.ListLit Nothing
       $ Seq.replicate 5
       $ Core.Var (Core.V "prelude" 0) `Core.Field` "types" `Core.Field` "Little" `Core.Field` "Foo"
 
 unionPerformance :: Core.Expr s TypeCheck.X -> Gauge.Benchmarkable
 unionPerformance prelude = Gauge.whnf TypeCheck.typeOf expr
   where
-    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"
+    expr =
+        Core.Let "x" Nothing
+            (Core.Let "big" Nothing (prelude `Core.Field` "types" `Core.Field` "Big")
+                (Core.Prefer "big" "big")
+            )
+            "x"
 
 main :: IO ()
 main = do

dhall/src/Dhall/Binary.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts   #-}
 {-# LANGUAGE FlexibleInstances  #-}
 {-# LANGUAGE RecordWildCards    #-}
 {-# LANGUAGE OverloadedStrings  #-}
@@ -38,16 +39,14 @@ import Dhall.Core
     , ImportHashed(..)
     , ImportMode(..)
     , ImportType(..)
+    , MultiLet(..)
     , Scheme(..)
     , URL(..)
     , Var(..)
     )
 
 import Data.Foldable (toList)
-import Data.List.NonEmpty (NonEmpty(..))
-import Data.Monoid ((<>))
 import Data.Text (Text)
-import Prelude hiding (exponent)
 import GHC.Float (double2Float, float2Double)
 
 import qualified Crypto.Hash
@@ -371,21 +370,18 @@ instance ToTerm a => ToTerm (Expr Void a) where
         t₁ = encode t₀
     encode (Embed x) =
         encode x
-    encode (Let as₀ b₀) =
-        TList ([ TInt 25 ] ++ as₁ ++ [ b₁ ])
-      where
-        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₀ mA₀ a₀ b₀) =
+        TList (TInt 25 : foldMap encodeBinding bs ++ [encode e])
+      where
+        MultiLet bs e = Dhall.Core.toMultiLet x₀ mA₀ a₀ b₀
+
+        encodeBinding (Binding x mA a) =
+            [ TString x
+            , case mA of
+                  Nothing -> TNull
+                  Just _A -> encode _A
+            , encode a
+            ]
     encode (Annot t₀ _T₀) =
         TList [ TInt 26, t₁, _T₁ ]
       where
@@ -724,20 +720,13 @@ instance FromTerm a => FromTerm (Expr s a) where
 
                 a₀  <- decode a₁
 
-                let binding = Binding x mA₀ a₀
-
-                case ls₁ of
-                    [ b₁ ] -> do
-                        b₀ <- decode b₁
+                b₀ <- case ls₁ of
+                    [ b₁ ] -> decode b₁
+                    _      -> process ls₁
 
-                        return (Let (binding :| []) b₀)
-                    _ -> do
-                        Let (l₀ :| ls₀) b₀ <- process ls₁
-
-                        return (Let (binding :| (l₀ : ls₀)) b₀)
+                return (Let x mA₀ a₀ b₀)
             process _ = do
                 empty
-
         process xs
     decode (TList [ TInt 26, t₁, _T₁ ]) = do
         t₀  <- decode t₁

dhall/src/Dhall/Core.hs

@@ -4,6 +4,7 @@
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric      #-}
 {-# LANGUAGE DeriveTraversable  #-}
+{-# LANGUAGE LambdaCase         #-}
 {-# LANGUAGE OverloadedStrings  #-}
 {-# LANGUAGE RankNTypes         #-}
 {-# LANGUAGE RecordWildCards    #-}
@@ -64,6 +65,8 @@ module Dhall.Core (
     , escapeText
     , pathCharacter
     , throws
+    , MultiLet(..)
+    , toMultiLet
     ) where
 
 #if MIN_VERSION_base(4,8,0)
@@ -103,6 +106,7 @@ import qualified Crypto.Hash
 import qualified Data.Char
 import {-# SOURCE #-} qualified Dhall.Eval
 import qualified Data.HashSet
+import qualified Data.List.NonEmpty
 import qualified Data.Sequence
 import qualified Data.Text
 import qualified Data.Text.Prettyprint.Doc  as Pretty
@@ -369,9 +373,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 [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)
+    -- | > 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)
     -- | > Annot x t                                ~  x : t
     | Annot (Expr s a) (Expr s a)
     -- | > Bool                                     ~  Bool
@@ -528,7 +532,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 as b) = Let (fmap (fmap f) as) (fmap f b)
+  fmap f (Let v maybeE e1 e2) = Let v (fmap (fmap f) maybeE) (fmap f e1) (fmap f e2)
   fmap f (Annot e1 e2) = Annot (fmap f e1) (fmap f e2)
   fmap _ Bool = Bool
   fmap _ (BoolLit b) = BoolLit b
@@ -605,9 +609,7 @@ 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 as b             >>= k = Let (fmap f as) (b >>= k)
-      where
-        f (Binding c d e) = Binding c (fmap (>>= k) d) (e >>= k)
+    Let a b c d          >>= k = Let a (fmap (>>= k) b) (c >>= k) (d >>= k)
     Annot a b            >>= k = Annot (a >>= k) (b >>= k)
     Bool                 >>= _ = Bool
     BoolLit a            >>= _ = BoolLit a
@@ -676,7 +678,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 as b            ) = Let (fmap (first k) as) (first k b)
+    first k (Let a b c d         ) = Let a (fmap (first k) b) (first k c) (first k d)
     first k (Annot a b           ) = Annot (first k a) (first k b)
     first _  Bool                  = Bool
     first _ (BoolLit a           ) = BoolLit a
@@ -876,25 +878,14 @@ 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 (Binding x₁ mA₀ a₀ :| []) b₀) =
-    Let (Binding x₁ mA₁ a₁ :| []) 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₀
-
-    b₁  =       shift d (V x₀ n₁)   b₀
-shift d (V x₀ n₀) (Let (Binding x₁ mA₀ a₀ :| (l₀ : ls₀)) b₀) =
-    case shift d (V x₀ n₁) (Let (l₀ :| ls₀) b₀) of
-        Let (l₁ :| ls₁) b₁ -> Let (Binding x₁ mA₁ a₁ :| (l₁ : ls₁)) b₁
-        e                  -> Let (Binding x₁ mA₁ a₁ :|       []  ) e
+shift d (V x n) (Let f mt r e) = Let f mt' r' e'
   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₀
+    e' = shift d (V x n') e
+      where
+        n' = if x == f then n + 1 else n
 
+    mt' = fmap (shift d (V x n)) mt
+    r'  =       shift d (V x n)  r
 shift d v (Annot a b) = Annot a' b'
   where
     a' = shift d v a
@@ -1055,29 +1046,14 @@ 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 (Binding x₁ mA₀ a₀ :| []) b₀) =
-    Let (Binding x₁ mA₁ a₁ :| []) b₁
+subst (V x n) e (Let f mt r b) = Let f mt' r' b'
   where
-    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₀) =
-    case subst (V x₀ n₁) e₁ (Let (l₀ :| ls₀) b₀) of
-        Let (l₁ :| ls₁) b₁ -> Let (Binding x₁ mA₁ a₁ :| (l₁ : ls₁)) b₁
-        e                  -> Let (Binding x₁ mA₁ a₁ :|       []  ) e
-  where
-    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') (shift 1 (V f 0) e) b
+      where
+        n' = if x == f then n + 1 else n
 
+    mt' = fmap (subst (V x n) e) mt
+    r'  =       subst (V x n) e  r
 subst x e (Annot a b) = Annot a' b'
   where
     a' = subst x e a
@@ -1276,9 +1252,7 @@ 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 as b            ) = Let (fmap f as) (denote b)
-  where
-    f (Binding c d e) = Binding c (fmap denote d) (denote e)
+denote (Let a b c d         ) = Let a (fmap denote b) (denote c) (denote d)
 denote (Annot a b           ) = Annot (denote a) (denote b)
 denote  Bool                  = Bool
 denote (BoolLit a           ) = BoolLit a
@@ -1545,18 +1519,11 @@ normalizeWithM ctx e0 = loop (denote e0)
                         case res2 of
                             Nothing -> pure (App f' a')
                             Just app' -> loop app'
-    Let (Binding x _ a₀ :| ls₀) b₀ -> do
-        a₁ <- loop a₀
-
-        rest <- case ls₀ of
-                []       -> loop b₀
-                l₁ : ls₁ -> loop (Let (l₁ :| ls₁) b₀)
-
-        let a₂ = shift 1 (V x 0) a₁
-        let b₁ = subst (V x 0) a₂ rest
-        let b₂ = shift (-1) (V x 0) b₁
-
-        loop b₂
+    Let f _ r 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'
     Annot x _ -> loop x
     Bool -> pure Bool
     BoolLit b -> pure (BoolLit b)
@@ -1920,7 +1887,7 @@ isNormalized e0 = loop (denote e0)
           App TextShow (TextLit (Chunks [] _)) ->
               False
           _ -> True
-      Let _ _ -> False
+      Let _ _ _ _ -> False
       Annot _ _ -> False
       Bool -> True
       BoolLit _ -> True
@@ -2160,9 +2127,7 @@ 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 as b) = Let <$> traverse g as <*> f b
-  where
-    g (Binding c d e) = Binding c <$> traverse f d <*> f e
+subExpressions f (Let a b c d) = Let a <$> traverse f b <*> f c <*> f d
 subExpressions f (Annot a b) = Annot <$> f a <*> f b
 subExpressions _ Bool = pure Bool
 subExpressions _ (BoolLit b) = pure (BoolLit b)
@@ -2272,3 +2237,16 @@ prettyURIComponent text
 throws :: (Exception e, MonadIO io) => Either e a -> io a
 throws (Left  e) = liftIO (Control.Exception.throwIO e)
 throws (Right r) = return r
+
+data MultiLet s a = MultiLet (NonEmpty (Binding s a)) (Expr s a)
+
+{-| In the resulting @'MultiLet' bs e@, @e@ is guaranteed not to be a 'Let'.
+-}
+toMultiLet :: Text -> Maybe (Expr s a) -> Expr s a -> Expr s a -> MultiLet s a
+toMultiLet x0 mA0 a0 = \case
+    Let x1 mA1 a1 b1 ->
+        let MultiLet bs e = toMultiLet x1 mA1 a1 b1
+        in MultiLet (Data.List.NonEmpty.cons binding bs) e
+    e -> MultiLet (binding :| []) e
+  where
+    binding = Binding x0 mA0 a0