Add support for multi-let

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'

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

@@ -25,20 +25,23 @@ 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"
 
 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

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₁

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)