Add support for with keyword

standard/dhall.abnf

@@ -382,6 +382,7 @@ keyword =
     / Infinity / NaN
     / merge / Some / toMap
     / forall
+    / with
 
 builtin =
       Natural-fold
@@ -806,7 +807,10 @@ combine-types-expression = times-expression         *(whsp combine-types whsp ti
 times-expression         = equal-expression         *(whsp "*" whsp equal-expression)
 equal-expression         = not-equal-expression     *(whsp "==" whsp not-equal-expression)
 not-equal-expression     = equivalent-expression    *(whsp "!=" whsp equivalent-expression)
-equivalent-expression    = application-expression   *(whsp equivalent whsp application-expression)
+equivalent-expression    = with-expression          *(whsp equivalent whsp with-expression)
+
+with-expression =
+    application-expression *(whsp1 "with" whsp1 any-label-or-some *(whsp "." whsp any-label-or-some) whsp "=" whsp application-expression)
 
 ; Import expressions need to be separated by some whitespace, otherwise there
 ; would be ambiguity: `./ab` could be interpreted as "import the file `./ab`",

standard/record.md

@@ -30,6 +30,31 @@ The above expression first desugars to:
 { x = { y = a, z = b } }
 ```
 
+Additionally, the language supports *record-like* syntax for updating a record
+using the `with` keyword, like this:
+
+```dhall
+record with x.y.z = a
+```
+
+... which desugars to:
+
+```dhall
+let _ = record in _ // { x =
+    let _ = _.x    in _ // { y =
+        let _ = _.y    in _ // { z =
+            a
+        }
+    }
+}
+```
+
+... which is easier to understand as the following equivalent expression:
+
+```dhall
+record // { x = record.x // { y = record.x.y // { z = a } } }
+```
+
 ## Dotted syntax
 
 Dhall records permit dot-separated field labels to specify nested records, like
@@ -158,3 +183,54 @@ associativity.  For example, the following expression:
     left-associative, but they are included for clarity
 -}
 ```
+
+## `with` keyword
+
+You can use the `with` keyword for ergonomic updates to deeply-nested records,
+like this:
+
+```dhall
+let record = { a.b = { c = 1, d = True } }
+
+in  record with a.b.d = False with a.b.e = 2.0
+```
+
+... which evaluates to:
+
+```dhall
+{ a.b = { c = 1, d = False, e = 2.0 } }
+```
+
+This desugaring uses the following judgment that translates the `with` keyword to
+the `//` operator:
+
+    desugar-with(e₀ with ks = v) = e₁
+
+... where:
+
+* `e₀` (an input) is an expression representing a record to update
+* `ks` (an input) is one or more dot-separated record labels representing the
+  record path to the value to insert
+* `v`  (an input) is the value to insert
+* `e₁` (the output) is the desugared expression
+
+A `with` expression with multiple dotted labels is equivalent to chained uses of
+the `//` operator:
+
+
+    desugar-with(let _ = e₀ in _ // { k₀ = _.k₀ with k₁.ks… = v₀ }) = e₁
+    ─────────────────────────────────────────  ; Inductive case for more than one
+    desugar-with(e₀ with k₀.k₁.ks… = v₀) = e₁  ; label
+
+
+... and if there is only one update with one label then the `with` keyword is a
+synonym for the `//` operator:
+
+
+    desugar-with(e₀ // { k = v }) = e₁
+    ──────────────────────────────────  ; Base case for exactly one
+    desugar-with(e₀ with k = v) = e₁    ; label
+
+
+For all other cases, `desugar-with` descends into sub-expressions and ignores
+anything that is not a `with` expression.

tests/normalization/success/WithRecordValueA.dhall

@@ -0,0 +1,12 @@
+{-  This test illustrates that `with a = { c = 2 }` is not the same thing as
+    `with a.c = 2`:
+
+    * `with a = { c = 2 }` overrides the entire value of the field `a` with a new
+      record containing only `c = 2`
+
+    * `with a.c = 2` extends or updates the record stored underneath `a` to
+      set the field `c` to `2`.
+
+    Compare this to the `WithNested` test, which contains the `a.c = 2` case
+-}
+{ a.b = 1 } with a = { c = 2 }

tests/normalization/success/WithRecordValueB.dhall

@@ -0,0 +1 @@
+{ a = { c = 2 } }

tests/normalization/success/unit/TextShowInterpolatedA.dhall

@@ -1 +1 @@
-λ(with : Text) → Text/show "text ${with} interpolation"
+λ(containing : Text) → Text/show "text ${containing} interpolation"

tests/normalization/success/unit/TextShowInterpolatedB.dhall

@@ -1 +1 @@
-λ(with : Text) → Text/show "text ${with} interpolation"
+λ(containing: Text) → Text/show "text ${containing} interpolation"

tests/normalization/success/unit/WithA.dhall

@@ -0,0 +1 @@
+{ a = 1 } with b = 2

tests/normalization/success/unit/WithB.dhall

@@ -0,0 +1 @@
+{ a = 1, b = 2 }

tests/normalization/success/unit/WithChainedA.dhall

@@ -0,0 +1,4 @@
+{-  This test verifies that an implementation correctly handles chained
+    `with` expressions
+-}
+{ a = 1 } with b = 2 with c = 3

tests/normalization/success/unit/WithChainedB.dhall

@@ -0,0 +1 @@
+{ a = 1, b = 2, c = 3 }

tests/normalization/success/unit/WithNestedA.dhall

@@ -0,0 +1,12 @@
+{-  This test verifies that an implementation handles `with` expressions that
+    update nested labels correctly
+
+    A common mistake an implementation might make is to produce the following
+    result:
+
+        { a.c = 2 }
+
+    ... due to the nested update clobbering the inner record.  A compliant
+    implementation extends inner records.
+-}
+{ a.b = 1 } with a.c = 2

tests/normalization/success/unit/WithNestedB.dhall

@@ -0,0 +1 @@
+{ a = { b = 1, c = 2 } }

tests/normalization/success/unit/WithPriorityA.dhall

@@ -0,0 +1,6 @@
+{-  This test ensures that updates are ordered and latter updates take priority
+    when the same field is updated more than one time
+
+    In this example, the `a` field is updated twice, and the latter update wins
+-}
+{ a = 1 } with a = 2 with a = 3

tests/normalization/success/unit/WithPriorityB.dhall

@@ -0,0 +1 @@
+{ a = 3 }

tests/parser/success/unit/WithA.dhall

@@ -0,0 +1,6 @@
+{-  The purpose of this test is to verify that an implementation correctly
+    desugars the base case of a non-nested update.  Specifically, an
+    implementation should not use an intermediate `let` when desugaring this
+    base case.
+-}
+{ a = 1 } with a = 2

tests/parser/success/unit/WithB.dhallb

@@ -0,0 +1 @@
+�	��aa�
��aa�

tests/parser/success/unit/WithB.diag

@@ -0,0 +1 @@
+[3, 9, [8, {"a": [15, 1]}], [8, {"a": [15, 2]}]]

tests/parser/success/unit/WithMultipleA.dhall

@@ -0,0 +1,8 @@
+{- This test ensures that `with` is purely syntactic sugar, meaning that it is
+   desugared before encoding and therefore is encoded as the desugared expression
+   in the CBOR encoding.
+
+   This test also ensures that implementations desugar the code exactly as
+   specified (e.g. using an intermediate `let` binding)
+-}
+{ a.b = 1, c.d = 2 } with a.b = 3 with c.e = 4

tests/parser/success/unit/WithMultipleB.diag

@@ -0,0 +1 @@
+[25, "_", null, [25, "_", null, [8, {"a": [8, {"b": [15, 1]}], "c": [8, {"d": [15, 2]}]}], [3, 9, 0, [8, {"a": [3, 9, [9, 0, "a"], [8, {"b": [15, 3]}]]}]]], [3, 9, 0, [8, {"c": [3, 9, [9, 0, "c"], [8, {"e": [15, 4]}]]}]]]

tests/parser/success/unit/WithPrecedenceA.dhall

@@ -0,0 +1,13 @@
+{-  The purpose of this test is to illustrate that function application has
+    higher precedence than `with` so that chained with expressions parse
+    correctly
+
+    The following expression should parse as:
+
+        ({ a = Some 1 } with a = Some 2) with a = Some 3
+
+    ... and not parse as:
+
+        { a = Some 1 } with a = (Some 2 with a = Some 3)
+-}
+{ a = Some 1 } with a = Some 2 with a = Some 3

tests/parser/success/unit/WithPrecedenceB.dhallb

@@ -0,0 +1 @@
+�	�	��aa���
��aa�����aa���

tests/parser/success/unit/WithPrecedenceB.diag

@@ -0,0 +1 @@
+[3, 9, [3, 9, [8, {"a": [5, null, [15, 1]]}], [8, {"a": [5, null, [15, 2]]}]], [8, {"a": [5, null, [15, 3]]}]]

tests/type-inference/failure/unit/WithInvalidOverrideA.dhall

@@ -0,0 +1,6 @@
+{-  The `with` keyword cannot "descend" past a field that is not a record
+
+    In the following example, the `a` field is not a record, therefore there is
+    no possibility of adding or overriding `a` with an inner `b` field
+-}
+{ a = 1 } with a.b = 2

tests/type-inference/success/unit/WithNewFieldA.dhall

@@ -0,0 +1,4 @@
+{- This test illustrates how the `with` keyword is permitted to extend a record
+   with new fields
+-}
+{ a = 1 } with b = 2

tests/type-inference/success/unit/WithNewFieldB.dhall

@@ -0,0 +1 @@
+{ a : Natural, b : Natural }

tests/type-inference/success/unit/WithNewTypeA.dhall

@@ -0,0 +1,4 @@
+{- This test illustrates that the `with` keyword is permitted to override
+   existing fields with a value of a new type (just like the `//` operator)
+-}
+{ a = 1 } with a = True

tests/type-inference/success/unit/WithNewTypeB.dhall

@@ -0,0 +1 @@
+{ a : Bool }