Implement with without syntactic sugar

dhall/src/Dhall/Diff.hs

@@ -1032,8 +1032,29 @@ diffApplicationExpression l r =
     diffWithExpression l r
 
 diffWithExpression :: (Eq a, Pretty a) => Expr Void a -> Expr Void a -> Diff
-diffWithExpression l@With{} r@With{} =
-    diffWithExpression (Syntax.desugarWith l) (Syntax.desugarWith r)
+diffWithExpression (With eL ksL vL) (With eR ksR vR) =
+    align
+        (    format " " (diffImportExpression eL eR)
+        <>  "with "
+        <>  align
+            (   format " " (diffPath ksL ksR)
+            <>  "= "
+            <>  diffOperatorExpression vL vR
+            )
+        )
+  where
+    diffPath (kL :| []) (kR :| []) =
+        diffLabel kL kR
+    diffPath (kL₀ :| kL₁ : ksL') (kR₀ :| kR₁ : ksR') =
+            format "" (diffLabel kL₀ kR₀)
+        <>  dot
+        <>  diffPath (kL₁ :| ksL') (kR₁ :| ksR')
+    diffPath (kL :| []) (kR₀ :| kR₁ : ksR') =
+            format "" (diffLabel kL kR₀)
+        <>  plus (foldMap (\k -> dot <> token (Internal.prettyLabel k)) (kR₁ :| ksR'))
+    diffPath (kL₀ :| kL₁ : ksL') (kR :| []) =
+            format "" (diffLabel kL₀ kR)
+        <>  minus (foldMap (\k -> dot <> token (Internal.prettyLabel k)) (kL₁ :| ksL'))
 diffWithExpression l r@With{} =
     mismatch l r
 diffWithExpression l@With{} r =

dhall/src/Dhall/Eval.hs

@@ -50,14 +50,15 @@ module Dhall.Eval (
   , textShow
   ) where
 
-import Data.Foldable (foldr', toList)
-import Data.Sequence (Seq, ViewL (..), ViewR (..))
-import Data.Text     (Text)
-import Data.Void     (Void)
-import Dhall.Map     (Map)
-import Dhall.Set     (Set)
-import GHC.Natural   (Natural)
-import Prelude       hiding (succ)
+import Data.Foldable      (foldr', toList)
+import Data.List.NonEmpty (NonEmpty(..))
+import Data.Sequence      (Seq, ViewL (..), ViewR (..))
+import Data.Text          (Text)
+import Data.Void          (Void)
+import Dhall.Map          (Map)
+import Dhall.Set          (Set)
+import GHC.Natural        (Natural)
+import Prelude            hiding (succ)
 
 import Dhall.Syntax
     ( Binding (..)
@@ -219,6 +220,7 @@ data Val a
     | VProject !(Val a) !(Either (Set Text) (Val a))
     | VAssert !(Val a)
     | VEquivalent !(Val a) !(Val a)
+    | VWith !(Val a) (NonEmpty Text) !(Val a)
     | VEmbed a
 
 -- | For use with "Text.Show.Functions".
@@ -383,6 +385,18 @@ vProjectByFields env t ks =
             t' ->
                 VProject t' (Left ks)
 
+vWith :: Val a -> NonEmpty Text -> Val a -> Val a
+vWith (VRecordLit kvs) (k  :| []     ) v = VRecordLit (Map.insert k  v  kvs)
+vWith (VRecordLit kvs) (k₀ :| k₁ : ks) v = VRecordLit (Map.insert k₀ e₂ kvs)
+  where
+    e₁ =
+        case Map.lookup k₀ kvs of
+            Nothing  -> VRecordLit mempty
+            Just e₁' -> e₁'
+
+    e₂ = vWith e₁ (k₁ :| ks) v
+vWith e₀ ks v₀ = VWith e₀ ks v₀
+
 eval :: forall a. Eq a => Environment a -> Expr Void a -> Val a
 eval !env t0 =
     case t0 of
@@ -725,8 +739,8 @@ eval !env t0 =
             VAssert (eval env t)
         Equivalent t u ->
             VEquivalent (eval env t) (eval env u)
-        e@With{} ->
-            eval env (Syntax.desugarWith e)
+        With e₀ ks v ->
+            vWith (eval env e₀) ks (eval env v)
         Note _ e ->
             eval env e
         ImportAlt t _ ->
@@ -1118,6 +1132,8 @@ quote !env !t0 =
             Assert (quote env t)
         VEquivalent t u ->
             Equivalent (quote env t) (quote env u)
+        VWith e ks v ->
+            With (quote env e) ks (quote env v)
         VInject m k Nothing ->
             Field (Union (fmap (fmap (quote env)) m)) $ Syntax.makeFieldSelection k
         VInject m k (Just t) ->

dhall/src/Dhall/Normalize.hs

@@ -23,6 +23,7 @@ module Dhall.Normalize (
 import Control.Applicative   (empty)
 import Data.Foldable
 import Data.Functor.Identity (Identity (..))
+import Data.List.NonEmpty    (NonEmpty(..))
 import Data.Sequence         (ViewL (..), ViewR (..))
 import Data.Traversable
 import Instances.TH.Lift     ()
@@ -613,8 +614,26 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0)
         r' <- loop r
 
         pure (Equivalent l' r')
-    With e' k v ->
-        loop (Syntax.desugarWith (With e' k v))
+    With e ks v -> do
+        e' <- loop e
+        v' <- loop v
+
+        case e' of
+            RecordLit kvs ->
+                case ks of
+                    k :| [] ->
+                        return (RecordLit (Dhall.Map.insert k (Syntax.makeRecordField v') kvs))
+                    k₀ :| k₁ : ks' -> do
+                        let e₁ =
+                                case Dhall.Map.lookup k₀ kvs of
+                                    Nothing -> RecordLit mempty
+                                    Just r  -> Syntax.recordFieldValue r
+
+                        e₂ <- loop (With e₁ (k₁ :| ks') v')
+
+                        return (RecordLit (Dhall.Map.insert k₀ (Syntax.makeRecordField e₂) kvs))
+            _ ->
+                return (With e' ks v')
     Note _ e' -> loop e'
     ImportAlt l _r -> loop l
     Embed a -> pure (Embed a)

dhall/src/Dhall/TypeCheck.hs

@@ -1251,8 +1251,27 @@ infer typer = loop
 
             return (VConst Type)
 
-        e@With{} ->
-            loop ctx (Syntax.desugarWith e)
+        With e ks v -> do
+            tE' <- loop ctx e
+
+            kTs' <- case tE' of
+                VRecord kTs' -> return kTs'
+                _            -> die (NotWithARecord e (quote names tE'))
+
+            case ks of
+                k :| [] -> do
+                    tV' <- loop ctx v
+
+                    return (VRecord (Dhall.Map.insert k tV' kTs'))
+                k₀ :| k₁ : ks' -> do
+                    let e₁ =
+                            if Dhall.Map.member k₀ kTs'
+                                then Field e (Syntax.makeFieldSelection k₀)
+                                else RecordLit mempty
+
+                    tV' <- loop ctx (With e₁ (k₁ :| ks') v)
+
+                    return (VRecord (Dhall.Map.insert k₀ tV' kTs'))
 
         Note s e ->
             case loop ctx e of
@@ -1343,6 +1362,7 @@ data TypeMessage s a
     | NotAnEquivalence (Expr s a)
     | IncomparableExpression (Expr s a)
     | EquivalenceTypeMismatch (Expr s a) (Expr s a) (Expr s a) (Expr s a)
+    | NotWithARecord (Expr s a) (Expr s a)
     | CantAnd (Expr s a) (Expr s a)
     | CantOr (Expr s a) (Expr s a)
     | CantEQ (Expr s a) (Expr s a)
@@ -4238,6 +4258,45 @@ prettyTypeMessage (EquivalenceTypeMismatch l _L r _R) = ErrorMessages {..}
         \                                                                                \n\
         \" <> insert _R <> "\n"
 
+prettyTypeMessage (NotWithARecord expr0 expr1) = ErrorMessages {..}
+  where
+    short = "❰with❱ only works on records"
+
+    long =
+        "Explanation: You can use ❰with❱ to update a record, like this:                  \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌─────────────────────────┐                                                 \n\
+        \    │  { a = 5 } with b = 10  │  This is valid because ❰{ a = 5}❱ is a record   \n\
+        \    └────────────────────────┘                                                  \n\
+        \                                                                                \n\
+        \    ┌──────────────────────────────────────────┐                                \n\
+        \    │  λ(r : { a : Natural }) → r with b = 10  │  This is also valid because    \n\
+        \    └──────────────────────────────────────────┘  ❰r❱ is a record               \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \... but you cannot use ❰with❱ to update an expression that is not a record.  For\n\
+        \example, the following expression is " <> _NOT <> " valid:                      \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \    ┌───────────────┐                                                           \n\
+        \    │ 1 with b = 10 │  Invalid: ❰1❱ is not a record                             \n\
+        \    └───────────────┘                                                           \n\
+        \                                                                                \n\
+        \                                                                                \n\
+        \You tried to update the following expressions:                                  \n\
+        \                                                                                \n\
+        \" <> txt0 <> "\n\
+        \                                                                                \n\
+        \... which has type\n\
+        \                                                                                \n\
+        \" <> txt1 <> "\n\
+        \                                                                                \n\
+        \... which is not a record type\n"
+      where
+        txt0 = insert expr0
+        txt1 = insert expr1
+
 prettyTypeMessage (CantAnd expr0 expr1) =
         buildBooleanOperator "&&" expr0 expr1
 
@@ -4649,6 +4708,8 @@ messageExpressions f m = case m of
         IncomparableExpression <$> f a
     EquivalenceTypeMismatch a b c d ->
         EquivalenceTypeMismatch <$> f a <*> f b <*> f c <*> f d
+    NotWithARecord a b ->
+        NotWithARecord <$> f a <*> f b
     CantAnd a b ->
         CantAnd <$> f a <*> f b
     CantOr a b ->

dhall/tests/diff/with.txt

@@ -0,0 +1,5 @@
+  λ(… : { …
+        })
+→ … with …+ .c.d
+         = - 2
+           + 3

dhall/tests/diff/withA.dhall

@@ -0,0 +1 @@
+λ(r : { a : Natural }) → r with b = 2

dhall/tests/diff/withB.dhall

@@ -0,0 +1 @@
+λ(r : { a : Natural }) → r with b.c.d = 3