From 7e523ae1903ae2d8bca8b3a8352167d7bac5b2b5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 14 Sep 2020 23:09:22 +0100
Subject: spec: Enable `with` optimizations

---
 CHANGELOG.md                                       |  1 +
 dhall-lang                                         |  2 +-
 dhall/src/operations/kind.rs                       |  3 ++
 dhall/src/operations/normalization.rs              |  2 +-
 dhall/src/operations/typecheck.rs                  |  2 +-
 dhall/src/semantics/resolve/resolve.rs             | 32 ++++++++++++++++++++--
 dhall/src/syntax/ast/span.rs                       |  1 -
 dhall/src/syntax/binary/decode.rs                  | 21 ++++++++++++++
 dhall/src/syntax/binary/encode.rs                  |  4 +++
 dhall/src/syntax/text/parser.rs                    | 26 ++++--------------
 dhall/src/syntax/text/printer.rs                   |  4 +++
 dhall/tests/parser/success/unit/WithB.txt          |  2 +-
 dhall/tests/parser/success/unit/WithMultipleB.txt  |  2 +-
 .../tests/parser/success/unit/WithPrecedence1B.txt |  2 +-
 .../tests/parser/success/unit/WithPrecedence2B.txt |  2 +-
 .../tests/parser/success/unit/WithPrecedence3B.txt |  2 +-
 .../failure/unit/WithInvalidOverrideA.txt          |  6 ++++
 17 files changed, 82 insertions(+), 32 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9449d4b..ac51508 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,7 @@
 
 #### [Unreleased]
 
+- BREAKING CHANGE: Enable `with` optimizations
 - Support Dhall v17.1.0
 
 #### [0.6.0] - 2020-08-05
diff --git a/dhall-lang b/dhall-lang
index 2cb2e18..b046b84 160000
--- a/dhall-lang
+++ b/dhall-lang
@@ -1 +1 @@
-Subproject commit 2cb2e1804aa5ba8379137df1fc1fd1e9afb17ec7
+Subproject commit b046b849350cdfcdb90af48c3f88d31a40154159
diff --git a/dhall/src/operations/kind.rs b/dhall/src/operations/kind.rs
index 0ee9671..2b035ef 100644
--- a/dhall/src/operations/kind.rs
+++ b/dhall/src/operations/kind.rs
@@ -55,6 +55,8 @@ pub enum OpKind<SubExpr> {
     ProjectionByExpr(SubExpr, SubExpr),
     ///  `x::y`
     Completion(SubExpr, SubExpr),
+    ///  `x with a.b.c = y`
+    With(SubExpr, Vec<Label>, SubExpr),
 }
 
 impl<SE> OpKind<SE> {
@@ -85,6 +87,7 @@ impl<SE> OpKind<SE> {
             Projection(e, ls) => Projection(expr!(e), ls.clone()),
             ProjectionByExpr(e, x) => ProjectionByExpr(expr!(e), expr!(x)),
             Completion(e, x) => Completion(expr!(e), expr!(x)),
+            With(x, ls, y) => With(expr!(x), ls.clone(), expr!(y)),
         })
     }
 
diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs
index 86fed13..b930f93 100644
--- a/dhall/src/operations/normalization.rs
+++ b/dhall/src/operations/normalization.rs
@@ -299,7 +299,7 @@ pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
             )),
             _ => nothing_to_do(),
         },
-        Completion(..) => {
+        Completion(..) | With(..) => {
             unreachable!("This case should have been handled in resolution")
         }
     }
diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs
index 314c587..2ccc17d 100644
--- a/dhall/src/operations/typecheck.rs
+++ b/dhall/src/operations/typecheck.rs
@@ -503,7 +503,7 @@ pub fn typecheck_operation(
 
             selection_val
         }
-        Completion(..) => {
+        Completion(..) | With(..) => {
             unreachable!("This case should have been handled in resolution")
         }
     })
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index 114bd9b..036e9a0 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -2,6 +2,7 @@ use itertools::Itertools;
 use std::borrow::Cow;
 use std::collections::BTreeMap;
 use std::env;
+use std::iter::once;
 use std::path::PathBuf;
 use url::Url;
 
@@ -12,8 +13,8 @@ use crate::operations::{BinOp, OpKind};
 use crate::semantics::{mkerr, Cache, Hir, HirKind, ImportEnv, NameEnv, Type};
 use crate::syntax;
 use crate::syntax::{
-    Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget, Span,
-    UnspannedExpr, URL,
+    Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget,
+    Label, Span, UnspannedExpr, URL,
 };
 use crate::{Parsed, Resolved};
 
@@ -276,6 +277,30 @@ fn resolve_one_import(
     })
 }
 
+/// Desugar a `with` expression.
+fn desugar_with(x: Expr, path: &[Label], y: Expr, span: Span) -> Expr {
+    use crate::operations::BinOp::RightBiasedRecordMerge;
+    use ExprKind::{Op, RecordLit};
+    use OpKind::{BinOp, Field};
+    let expr = |k| Expr::new(k, span.clone());
+    match path {
+        [] => y,
+        [l, rest @ ..] => {
+            let res = desugar_with(
+                expr(Op(Field(x.clone(), l.clone()))),
+                rest,
+                y,
+                span.clone(),
+            );
+            expr(Op(BinOp(
+                RightBiasedRecordMerge,
+                x,
+                expr(RecordLit(once((l.clone(), res)).collect())),
+            )))
+        }
+    }
+}
+
 /// Desugar the first level of the expression.
 fn desugar(expr: &Expr) -> Cow<'_, Expr> {
     match expr.kind() {
@@ -301,6 +326,9 @@ fn desugar(expr: &Expr) -> Cow<'_, Expr> {
                 expr.span(),
             ))
         }
+        ExprKind::Op(OpKind::With(x, path, y)) => {
+            Cow::Owned(desugar_with(x.clone(), path, y.clone(), expr.span()))
+        }
         _ => Cow::Borrowed(expr),
     }
 }
diff --git a/dhall/src/syntax/ast/span.rs b/dhall/src/syntax/ast/span.rs
index ab3279b..b0c7b5a 100644
--- a/dhall/src/syntax/ast/span.rs
+++ b/dhall/src/syntax/ast/span.rs
@@ -21,7 +21,6 @@ pub enum Span {
     /// Desugarings
     DuplicateRecordFieldsSugar,
     DottedFieldSugar,
-    WithSugar,
     RecordPunSugar,
     /// For expressions obtained from decoding binary
     Decoded,
diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs
index 195bd0a..d360949 100644
--- a/dhall/src/syntax/binary/decode.rs
+++ b/dhall/src/syntax/binary/decode.rs
@@ -434,6 +434,27 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
                 let x = cbor_value_to_dhall(&x)?;
                 EmptyListLit(x)
             }
+            [U64(29), x, labels, y] => {
+                let x = cbor_value_to_dhall(&x)?;
+                let y = cbor_value_to_dhall(&y)?;
+                let labels = match labels {
+                    Array(labels) => labels
+                        .iter()
+                        .map(|s| match s {
+                            String(s) => Ok(Label::from(s.as_str())),
+                            _ => Err(DecodeError::WrongFormatError(
+                                "with".to_owned(),
+                            )),
+                        })
+                        .collect::<Result<_, _>>()?,
+                    _ => {
+                        return Err(DecodeError::WrongFormatError(
+                            "with".to_owned(),
+                        ))
+                    }
+                };
+                Op(With(x, labels, y))
+            }
             _ => {
                 return Err(DecodeError::WrongFormatError(format!(
                     "{:?}",
diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs
index b6bbabe..33c7fa5 100644
--- a/dhall/src/syntax/binary/encode.rs
+++ b/dhall/src/syntax/binary/encode.rs
@@ -171,6 +171,10 @@ where
         Op(Completion(x, y)) => {
             ser_seq!(ser; tag(3), tag(13), expr(x), expr(y))
         }
+        Op(With(x, ls, y)) => {
+            let ls: Vec<_> = ls.iter().map(label).collect();
+            ser_seq!(ser; tag(29), expr(x), ls, expr(y))
+        }
         Import(import) => serialize_import(ser, import),
     }
 }
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index 06c1ac3..377f5e4 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -105,26 +105,6 @@ fn insert_recordlit_entry(map: &mut BTreeMap<Label, Expr>, l: Label, e: Expr) {
     }
 }
 
-fn desugar_with_expr(x: Expr, labels: &[Label], y: Expr) -> Expr {
-    use crate::operations::BinOp::RightBiasedRecordMerge;
-    let expr = |k| Expr::new(k, Span::WithSugar);
-    match labels {
-        [] => y,
-        [l, rest @ ..] => {
-            let res = desugar_with_expr(
-                expr(Op(Field(x.clone(), l.clone()))),
-                rest,
-                y,
-            );
-            expr(Op(BinOp(
-                RightBiasedRecordMerge,
-                x,
-                expr(RecordLit(once((l.clone(), res)).collect())),
-            )))
-        }
-    }
-}
-
 lazy_static::lazy_static! {
     static ref PRECCLIMBER: PrecClimber<Rule> = {
         use Rule::*;
@@ -778,7 +758,11 @@ impl DhallParser {
                 clauses.fold(
                     first,
                     |acc, (labels, e)| {
-                        desugar_with_expr(acc, &labels, e)
+                        spanned_union(
+                            acc.span(),
+                            e.span(),
+                            Op(With(acc, labels, e))
+                        )
                     }
                 )
             },
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index 8815d69..0c2eb2e 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -275,6 +275,10 @@ impl<SE: Display + Clone> Display for OpKind<SE> {
             Completion(a, b) => {
                 write!(f, "{}::{}", a, b)?;
             }
+            With(a, ls, b) => {
+                let ls = ls.iter().join(".");
+                write!(f, "{} with {} = {}", a, ls, b)?;
+            }
         }
         Ok(())
     }
diff --git a/dhall/tests/parser/success/unit/WithB.txt b/dhall/tests/parser/success/unit/WithB.txt
index 74f42a2..555eb50 100644
--- a/dhall/tests/parser/success/unit/WithB.txt
+++ b/dhall/tests/parser/success/unit/WithB.txt
@@ -1 +1 @@
-{ a = 1 } ⫽ { a = 2 }
+{ a = 1 } with a = 2
diff --git a/dhall/tests/parser/success/unit/WithMultipleB.txt b/dhall/tests/parser/success/unit/WithMultipleB.txt
index 76782a5..dbc5bb3 100644
--- a/dhall/tests/parser/success/unit/WithMultipleB.txt
+++ b/dhall/tests/parser/success/unit/WithMultipleB.txt
@@ -1 +1 @@
-{ a = { b = 1 }, c = { d = 2 } } ⫽ { a = { a = { b = 1 }, c = { d = 2 } }.a ⫽ { b = 3 } } ⫽ { c = ({ a = { b = 1 }, c = { d = 2 } } ⫽ { a = { a = { b = 1 }, c = { d = 2 } }.a ⫽ { b = 3 } }).c ⫽ { e = 4 } }
+{ a = { b = 1 }, c = { d = 2 } } with a.b = 3 with c.e = 4
diff --git a/dhall/tests/parser/success/unit/WithPrecedence1B.txt b/dhall/tests/parser/success/unit/WithPrecedence1B.txt
index 5f22335..2509dba 100644
--- a/dhall/tests/parser/success/unit/WithPrecedence1B.txt
+++ b/dhall/tests/parser/success/unit/WithPrecedence1B.txt
@@ -1 +1 @@
-{ a = Some 1 } ⫽ { a = Some 2 } ⫽ { a = Some 3 }
+{ a = Some 1 } with a = Some 2 with a = Some 3
diff --git a/dhall/tests/parser/success/unit/WithPrecedence2B.txt b/dhall/tests/parser/success/unit/WithPrecedence2B.txt
index f945cc9..02df511 100644
--- a/dhall/tests/parser/success/unit/WithPrecedence2B.txt
+++ b/dhall/tests/parser/success/unit/WithPrecedence2B.txt
@@ -1 +1 @@
-{ x = 0 } ⫽ { x = 1 + 1 }
+{ x = 0 } with x = 1 + 1
diff --git a/dhall/tests/parser/success/unit/WithPrecedence3B.txt b/dhall/tests/parser/success/unit/WithPrecedence3B.txt
index a801b24..544b4d1 100644
--- a/dhall/tests/parser/success/unit/WithPrecedence3B.txt
+++ b/dhall/tests/parser/success/unit/WithPrecedence3B.txt
@@ -1 +1 @@
-foo::{ x = 0 } ⫽ { x = 1 }
+foo::{ x = 0 } with x = 1
diff --git a/dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt b/dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt
index de101e0..c34175f 100644
--- a/dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt
+++ b/dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt
@@ -1 +1,7 @@
 Type error: error: MustCombineRecord
+ --> <current file>:1:1
+  |
+...
+6 | { a = 1 } with a.b = 2
+  | ^^^^^^^^^^^^^^^^^^^^^^ MustCombineRecord
+  |
-- 
cgit v1.2.3