Mostly revert "Add support for multi-let (#675)"

This reverts commit 8a5bfaa.

dhall/src/Dhall/Binary.hs

@@ -27,8 +27,7 @@ import Control.Applicative (empty, (<|>))
 import Control.Exception (Exception)
 import Data.Void (Void, absurd)
 import Dhall.Core
-    ( Binding(..)
-    , Chunks(..)
+    ( Chunks(..)
     , Const(..)
     , Directory(..)
     , Expr(..)
@@ -44,10 +43,7 @@ import Dhall.Core
     )
 
 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 +367,14 @@ 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₁ ])
+    encode (Let x mA₀ a₀ b₀) =
+        TList [ TInt 25, TString x, mA₁, a₁, b₁ ]
       where
-        as₁ = do
-            Binding x mA₀ a₀ <- toList as₀
-
-            let mA₁ = case mA₀ of
+        a₁  = encode a₀
+        mA₁ = case mA₀ of
                     Nothing  -> TNull
                     Just _A₀ -> encode _A₀
-
-            let a₁ = encode a₀
-
-            [ TString x, mA₁, a₁ ]
-
-        b₁ = encode b₀
+        b₁  = encode b₀
     encode (Annot t₀ _T₀) =
         TList [ TInt 26, t₁, _T₁ ]
       where
@@ -716,29 +705,16 @@ instance FromTerm a => FromTerm (Expr s a) where
 
         return (Assert t₀)
     decode e@(TList (TInt 24 : _)) = fmap Embed (decode e)
-    decode (TList (TInt 25 : xs)) = do
-        let process (TString x : _A₁ : a₁ : ls₁) = do
+    decode (TList [ TInt 25, TString x, _A₁, a₁, b₁ ]) = do
                 mA₀ <- case _A₁ of
                     TNull -> return Nothing
                     _     -> fmap Just (decode _A₁)
 
-                a₀  <- decode a₁
-
-                let binding = Binding x mA₀ a₀
+                a₀ <- decode 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
+                b₀ <- decode b₁
 
-        process xs
+                return (Let x mA₀ a₀ b₀)
     decode (TList [ TInt 26, t₁, _T₁ ]) = do
         t₀  <- decode t₁
         _T₀ <- decode _T₁

dhall/src/Dhall/Core.hs

@@ -30,7 +30,6 @@ module Dhall.Core (
     , URL(..)
     , Scheme(..)
     , Var(..)
-    , Binding(..)
     , Chunks(..)
     , Expr(..)
 
@@ -80,7 +79,6 @@ 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.Semigroup (Semigroup(..))
 import Data.Sequence (Seq, ViewL(..), ViewR(..))
@@ -369,9 +367,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 +526,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 +603,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 +672,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
@@ -744,19 +740,6 @@ 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, Ord, Data, NFData)
-
-instance (Lift s, Lift a, Data s, Data a) => Lift (Binding s a)
-
-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, Ord, Data, NFData)
@@ -876,25 +859,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₁
+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₀
-
-    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
-  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 +1027,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₁
-  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
+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') (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 +1233,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 +1500,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 +1868,7 @@ isNormalized e0 = loop (denote e0)
           App TextShow (TextLit (Chunks [] _)) ->
               False
           _ -> True
-      Let _ _ -> False
+      Let _ _ _ _ -> False
       Annot _ _ -> False
       Bool -> True
       BoolLit _ -> True
@@ -2160,9 +2108,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)

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 (Binding(..), Chunks (..), Const(..), Expr(..), Var(..))
+import Dhall.Core (Chunks (..), Const(..), Expr(..), Var(..))
 import Dhall.Binary (ToTerm)
 import Dhall.Map (Map)
 import Dhall.Set (Set)
@@ -667,21 +667,20 @@ diffExpression l@(BoolIf {}) r =
     mismatch l r
 diffExpression l r@(BoolIf {}) =
     mismatch l r
-diffExpression (Let asL bL ) (Let asR bR) =
-    enclosed' "" (keyword "in" <> "  ")
-        (Data.List.NonEmpty.zipWith docA asL asR <> pure docB)
+diffExpression l@(Let {}) r@(Let {}) =
+    enclosed' "    " (keyword "in" <> "  ") (docs l r)
   where
-    docA (Binding cL dL eL) (Binding cR dR eR) = align doc
+    docs (Let aL bL cL dL) (Let aR bR cR dR) =
+        Data.List.NonEmpty.cons (align doc) (docs dL dR)
       where
         doc =   keyword "let"
             <>  " "
-            <>  format " " (diffLabel cL cR)
-            <>  format " " (diffMaybe (colon <> " ") diffExpression dL dR)
+            <>  format " " (diffLabel aL aR)
+            <>  format " " (diffMaybe (colon <> " ") diffExpression bL bR)
             <>  equals
             <>  " "
-            <>  diffExpression eL eR
-
-    docB = diffExpression bL bR
+            <>  diffExpression cL cR
+    docs aL aR = pure (diffExpression aL aR)
 diffExpression l@(Let {}) r =
     mismatch l r
 diffExpression l r@(Let {}) =

dhall/src/Dhall/Eval.hs

@@ -58,16 +58,14 @@ module Dhall.Eval (
 import Control.Applicative (Applicative(..), (<$>))
 #endif
 
-import Data.Foldable (foldr', foldl', toList)
-import Data.List.NonEmpty (NonEmpty(..), cons)
+import Data.Foldable (foldr', toList)
 import Data.Semigroup (Semigroup(..))
 import Data.Sequence (Seq)
 import Data.Text (Text)
 import Data.Void (Void)
 
 import Dhall.Core (
     Expr(..)
-  , Binding(..)
   , Chunks(..)
   , Const(..)
   , Import
@@ -84,7 +82,6 @@ import Unsafe.Coerce (unsafeCoerce)
 
 import qualified Codec.Serialise     as Serialise
 import qualified Data.Char
-import qualified Data.List.NonEmpty
 import qualified Data.Sequence
 import qualified Data.Text
 import qualified Dhall.Binary
@@ -352,10 +349,8 @@ eval !env t =
     Lam x a t        -> VLam (evalE a) (Cl x env t)
     Pi x a b         -> VPi (evalE a) (Cl x env b)
     App t u          -> vApp (evalE t) (evalE u)
-    Let (b :| bs) t  -> go env (b:bs) where
-                          go !env []     = eval env t
-                          go  env (b:bs) = go (Extend env (variable b)
-                                                          (eval env (value b))) bs
+    Let x _mA a b    -> let !env' = Extend env x (evalE a)
+                        in eval env' b
     Annot t _        -> evalE t
 
     Bool             -> VBool
@@ -927,7 +922,10 @@ alphaNormalize = goEnv NEmpty where
       Pi x a b         -> Pi "_" (go a) (goBind x b)
       App t u          -> App (go t) (go u)
 
-      Let (b :| bs) u  ->
+      Let x mA a b     -> Let "_" (go <$> mA) (go a) (goBind x b)
+
+{-
+      Let (b :| bs) u ->
         let Binding x a t = b
 
             nil = (NBind e x, Binding "_" (goEnv e <$> a) (goEnv e t) :| [])
@@ -938,6 +936,7 @@ alphaNormalize = goEnv NEmpty where
             (e', Data.List.NonEmpty.reverse -> bs') = foldl' snoc nil bs
 
         in Let bs' (goEnv e' u)
+-}
 
       Annot t u        -> Annot (go t) (go u)
       Bool             -> Bool

dhall/src/Dhall/Import.hs

@@ -159,7 +159,6 @@ import System.FilePath ((</>))
 import Dhall.Binary (StandardVersion(..))
 import Dhall.Core
     ( Expr(..)
-    , Binding(..)
     , Chunks(..)
     , Directory(..)
     , File(..)
@@ -906,9 +905,7 @@ 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 as b             -> Let <$> traverse f as <*> loadWith b
-    where
-      f (Binding c d e) = Binding c <$> traverse loadWith d <*> loadWith e
+  Let a b c d          -> Let <$> pure a <*> mapM loadWith b <*> loadWith c <*> loadWith d
   Annot a b            -> Annot <$> loadWith a <*> loadWith b
   Bool                 -> pure Bool
   BoolLit a            -> pure (BoolLit a)