spec: Enable `with` optimizations

3 files changed, 5 insertions, 2 deletions

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")
         }
     })