Implement more efficient with desugaring (#1993)

… as permitted by dhall-lang/dhall-lang#1052

dhall/src/Dhall/Binary.hs

@@ -31,6 +31,7 @@ import Codec.Serialise      (Serialise (decode, encode))
 import Control.Applicative  (empty, (<|>))
 import Control.Exception    (Exception)
 import Data.ByteString.Lazy (ByteString)
+import Data.Foldable (Foldable)
 import Dhall.Syntax
     ( Binding (..)
     , Chunks (..)
@@ -68,6 +69,8 @@ import qualified Data.ByteArray
 import qualified Data.ByteString
 import qualified Data.ByteString.Lazy
 import qualified Data.ByteString.Short
+import qualified Data.Foldable         as Foldable
+import qualified Data.List.NonEmpty    as NonEmpty
 import qualified Data.Sequence
 import qualified Dhall.Crypto
 import qualified Dhall.Map
@@ -581,6 +584,23 @@ decodeExpressionInternal decodeEmbed = go
 
                                 return (ListLit (Just _T) empty)
 
+                            29 -> do
+                                l <- go
+
+                                n <- Decoding.decodeListLen
+
+                                ks₀ <- replicateDecoder n Decoding.decodeString
+
+                                ks₁ <- case NonEmpty.nonEmpty ks₀ of
+                                    Nothing ->
+                                        die "0 field labels in decoded with expression"
+                                    Just ks₁ ->
+                                        return ks₁
+
+                                r <- go
+
+                                return (With l ks₁ r)
+
                             _ ->
                                 die ("Unexpected tag: " <> show tag)
 
@@ -941,8 +961,12 @@ encodeExpressionInternal encodeEmbed = go
                 (go t)
                 (go _T)
 
-        a@With{} ->
-            go (Syntax.desugarWith a)
+        With l ks r ->
+            encodeList4
+                (Encoding.encodeInt 29)
+                (go l)
+                (encodeList (fmap Encoding.encodeString ks))
+                (go r)
 
         Note _ b ->
             go b
@@ -976,11 +1000,12 @@ encodeList4 :: Encoding -> Encoding -> Encoding -> Encoding -> Encoding
 encodeList4 a b c d = Encoding.encodeListLen 4 <> a <> b <> c <> d
 {-# INLINE encodeList4 #-}
 
-encodeListN :: Int -> [ Encoding ] -> Encoding
-encodeListN len xs = Encoding.encodeListLen (fromIntegral len) <> mconcat xs
+encodeListN :: Foldable f => Int -> f Encoding -> Encoding
+encodeListN len xs =
+    Encoding.encodeListLen (fromIntegral len) <> Foldable.fold xs
 {-# INLINE encodeListN #-}
 
-encodeList :: [ Encoding ] -> Encoding
+encodeList :: Foldable f => f Encoding -> Encoding
 encodeList xs = encodeListN (length xs) xs
 {-# INLINE encodeList #-}
 

dhall/src/Dhall/Normalize.hs

@@ -14,7 +14,7 @@ module Dhall.Normalize (
     , ReifiedNormalizer (..)
     , judgmentallyEqual
     , subst
-    , shift
+    , Syntax.shift
     , isNormalized
     , isNormalizedWith
     , freeIn
@@ -59,95 +59,6 @@ judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
 judgmentallyEqual = Eval.judgmentallyEqual
 {-# INLINE judgmentallyEqual #-}
 
-{-| `shift` is used by both normalization and type-checking to avoid variable
-    capture by shifting variable indices
-
-    For example, suppose that you were to normalize the following expression:
-
-> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x
-
-    If you were to substitute @y@ with @x@ without shifting any variable
-    indices, then you would get the following incorrect result:
-
-> λ(a : Type) → λ(x : a) → λ(x : a) → x  -- Incorrect normalized form
-
-    In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in
-    order to avoid being misinterpreted as the @x@ bound by the innermost
-    lambda.  If we perform that `shift` then we get the correct result:
-
-> λ(a : Type) → λ(x : a) → λ(x : a) → x@1
-
-    As a more worked example, suppose that you were to normalize the following
-    expression:
-
->     λ(a : Type)
-> →   λ(f : a → a → a)
-> →   λ(x : a)
-> →   λ(x : a)
-> →   (λ(x : a) → f x x@1) x@1
-
-    The correct normalized result would be:
-
->     λ(a : Type)
-> →   λ(f : a → a → a)
-> →   λ(x : a)
-> →   λ(x : a)
-> →   f x@1 x
-
-    The above example illustrates how we need to both increase and decrease
-    variable indices as part of substitution:
-
-    * We need to increase the index of the outer @x\@1@ to @x\@2@ before we
-      substitute it into the body of the innermost lambda expression in order
-      to avoid variable capture.  This substitution changes the body of the
-      lambda expression to @(f x\@2 x\@1)@
-
-    * We then remove the innermost lambda and therefore decrease the indices of
-      both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one
-      less @x@ variable is now bound within that scope
-
-    Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to
-    the indices of all variables named @x@ whose indices are greater than
-    @(n + m)@, where @m@ is the number of bound variables of the same name
-    within that scope
-
-    In practice, @d@ is always @1@ or @-1@ because we either:
-
-    * increment variables by @1@ to avoid variable capture during substitution
-    * decrement variables by @1@ when deleting lambdas after substitution
-
-    @n@ starts off at @0@ when substitution begins and increments every time we
-    descend into a lambda or let expression that binds a variable of the same
-    name in order to avoid shifting the bound variables by mistake.
--}
-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 (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
-      where
-        n' = if x == x' then n + 1 else n
-shift d (V x n) (Pi x' _A _B) = Pi x' _A' _B'
-  where
-    _A' = shift d (V x n ) _A
-    _B' = shift d (V x n') _B
-      where
-        n' = if x == x' then n + 1 else n
-shift d (V x n) (Let (Binding src0 f src1 mt src2 r) e) =
-    Let (Binding src0 f src1 mt' src2 r') e'
-  where
-    e' = shift d (V x n') e
-      where
-        n' = if x == f then n + 1 else n
-
-    mt' = fmap (fmap (shift d (V x n))) mt
-    r'  =             shift d (V x n)  r
-shift d v expression = Lens.over Syntax.subExpressions (shift d v) expression
-
 {-| Substitute all occurrences of a variable with an expression
 
 > subst x C B  ~  B[x := C]
@@ -157,19 +68,19 @@ subst _ _ (Const a) = Const a
 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
+    _A' = subst (V x n )                         e  _A
+    b'  = subst (V x n') (Syntax.shift 1 (V y 0) e)  b
     n'  = if x == y then n + 1 else n
 subst (V x n) e (Pi y _A _B) = Pi y _A' _B'
   where
-    _A' = subst (V x n )                  e  _A
-    _B' = subst (V x n') (shift 1 (V y 0) e) _B
+    _A' = subst (V x n )                         e  _A
+    _B' = subst (V x n') (Syntax.shift 1 (V y 0) e) _B
     n'  = if x == y then n + 1 else n
 subst v e (Var v') = if v == v' then e else Var v'
 subst (V x n) e (Let (Binding src0 f src1 mt src2 r) b) =
     Let (Binding src0 f src1 mt' src2 r') b'
   where
-    b' = subst (V x n') (shift 1 (V f 0) e) b
+    b' = subst (V x n') (Syntax.shift 1 (V f 0) e) b
       where
         n' = if x == f then n + 1 else n
 
@@ -282,9 +193,9 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
               case f' of
                 Lam (FunctionBinding _ x _ _ _A) b₀ -> do
 
-                    let a₂ = shift 1 (V x 0) a'
+                    let a₂ = Syntax.shift 1 (V x 0) a'
                     let b₁ = subst (V x 0) a₂ b₀
-                    let b₂ = shift (-1) (V x 0) b₁
+                    let b₂ = Syntax.shift (-1) (V x 0) b₁
 
                     loop b₂
                 _ ->
@@ -344,7 +255,7 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
                         pure (TextLit (Chunks [] (Data.Text.pack (show n))))
                     App (App ListBuild _A₀) g -> loop (App (App (App g list) cons) nil)
                       where
-                        _A₁ = shift 1 "a" _A₀
+                        _A₁ = Syntax.shift 1 "a" _A₀
 
                         list = App List _A₀
 
@@ -413,9 +324,9 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
                             Just app' -> loop app'
     Let (Binding _ f _ _ _ r) b -> loop b''
       where
-        r'  = shift   1  (V f 0) r
+        r'  = Syntax.shift   1  (V f 0) r
         b'  = subst (V f 0) r' b
-        b'' = shift (-1) (V f 0) b'
+        b'' = Syntax.shift (-1) (V f 0) b'
     Annot x _ -> loop x
     Bool -> pure Bool
     BoolLit b -> pure (BoolLit b)

dhall/src/Dhall/Syntax.hs

@@ -80,6 +80,9 @@ module Dhall.Syntax (
 
     -- * Utilities
     , internalError
+    -- `shift` should really be in `Dhall.Normalize`, but it's here to avoid a
+    -- module cycle
+    , shift
     ) where
 
 import Control.DeepSeq            (NFData)
@@ -1305,19 +1308,114 @@ toDoubleQuoted literal =
 
     indent = Data.Text.length longestSharedPrefix
 
+{-| `shift` is used by both normalization and type-checking to avoid variable
+    capture by shifting variable indices
+
+    For example, suppose that you were to normalize the following expression:
+
+> λ(a : Type) → λ(x : a) → (λ(y : a) → λ(x : a) → y) x
+
+    If you were to substitute @y@ with @x@ without shifting any variable
+    indices, then you would get the following incorrect result:
+
+> λ(a : Type) → λ(x : a) → λ(x : a) → x  -- Incorrect normalized form
+
+    In order to substitute @x@ in place of @y@ we need to `shift` @x@ by @1@ in
+    order to avoid being misinterpreted as the @x@ bound by the innermost
+    lambda.  If we perform that `shift` then we get the correct result:
+
+> λ(a : Type) → λ(x : a) → λ(x : a) → x@1
+
+    As a more worked example, suppose that you were to normalize the following
+    expression:
+
+>     λ(a : Type)
+> →   λ(f : a → a → a)
+> →   λ(x : a)
+> →   λ(x : a)
+> →   (λ(x : a) → f x x@1) x@1
+
+    The correct normalized result would be:
+
+>     λ(a : Type)
+> →   λ(f : a → a → a)
+> →   λ(x : a)
+> →   λ(x : a)
+> →   f x@1 x
+
+    The above example illustrates how we need to both increase and decrease
+    variable indices as part of substitution:
+
+    * We need to increase the index of the outer @x\@1@ to @x\@2@ before we
+      substitute it into the body of the innermost lambda expression in order
+      to avoid variable capture.  This substitution changes the body of the
+      lambda expression to @(f x\@2 x\@1)@
+
+    * We then remove the innermost lambda and therefore decrease the indices of
+      both @x@s in @(f x\@2 x\@1)@ to @(f x\@1 x)@ in order to reflect that one
+      less @x@ variable is now bound within that scope
+
+    Formally, @(shift d (V x n) e)@ modifies the expression @e@ by adding @d@ to
+    the indices of all variables named @x@ whose indices are greater than
+    @(n + m)@, where @m@ is the number of bound variables of the same name
+    within that scope
+
+    In practice, @d@ is always @1@ or @-1@ because we either:
+
+    * increment variables by @1@ to avoid variable capture during substitution
+    * decrement variables by @1@ when deleting lambdas after substitution
+
+    @n@ starts off at @0@ when substitution begins and increments every time we
+    descend into a lambda or let expression that binds a variable of the same
+    name in order to avoid shifting the bound variables by mistake.
+-}
+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 (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
+      where
+        n' = if x == x' then n + 1 else n
+shift d (V x n) (Pi x' _A _B) = Pi x' _A' _B'
+  where
+    _A' = shift d (V x n ) _A
+    _B' = shift d (V x n') _B
+      where
+        n' = if x == x' then n + 1 else n
+shift d (V x n) (Let (Binding src0 f src1 mt src2 r) e) =
+    Let (Binding src0 f src1 mt' src2 r') e'
+  where
+    e' = shift d (V x n') e
+      where
+        n' = if x == f then n + 1 else n
+
+    mt' = fmap (fmap (shift d (V x n))) mt
+    r'  =             shift d (V x n)  r
+shift d v expression = Lens.over subExpressions (shift d v) expression
+
 -- | Desugar all @with@ expressions
 desugarWith :: Expr s a -> Expr s a
 desugarWith = Optics.rewriteOf subExpressions rewrite
   where
     rewrite e@(With record (key :| []) value) =
-        Just (Prefer (PreferFromWith e) record (RecordLit [ (key, makeRecordField value) ]))
+        Just
+            (Prefer
+                (PreferFromWith e)
+                record
+                (RecordLit [ (key, makeRecordField value) ])
+            )
     rewrite e@(With record (key0 :| key1 : keys) value) =
         Just
-            (Prefer (PreferFromWith e) record
-                (RecordLit
-                    [ (key0, makeRecordField $
-                        With (Field record (FieldSelection Nothing key0 Nothing)) (key1 :| keys) value)
-                    ]
+            (Let
+                (makeBinding "_" record)
+                (Prefer (PreferFromWith e) "_"
+                    (RecordLit
+                        [ (key0, makeRecordField $ With (Field "_" (FieldSelection Nothing key0 Nothing)) (key1 :| keys) (shift 1 "_" value)) ]
+                    )
                 )
             )
     rewrite _ = Nothing