Implement type checking for With op

5 files changed, 57 insertions, 41 deletions

diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs
index 2ccc17d..af6f706 100644
--- a/dhall/src/operations/typecheck.rs
+++ b/dhall/src/operations/typecheck.rs
@@ -503,7 +503,56 @@ pub fn typecheck_operation(
 
             selection_val
         }
-        Completion(..) | With(..) => {
+        With(record, labels, expr) => {
+            use crate::syntax::Label;
+            use std::iter::{once, FromIterator};
+
+            let record_entries = |nk: &NirKind| {
+                match nk {
+                    NirKind::RecordType(kts) => Ok(kts.clone()),
+                    _ => mk_span_err(span.clone(), "WithMustBeRecord"), // TODO better error
+                }
+            };
+
+            let mut current_nk: Option<NirKind> =
+                Some(record.ty().kind().clone());
+            let mut visited: Vec<(&Label, HashMap<Label, Nir>)> = Vec::new();
+            let mut to_create = Vec::new();
+
+            for label in labels {
+                match current_nk {
+                    None => to_create.push(label),
+                    Some(nk) => {
+                        let kts = record_entries(&nk)?;
+
+                        current_nk =
+                            kts.get(label).map(|nir| nir.kind().clone());
+                        visited.push((label, kts));
+                    }
+                }
+            }
+
+            // Create Nir for record type bottom up
+            let mut nir = expr.ty().as_nir().clone();
+
+            while let Some(label) = to_create.pop() {
+                let rec = RecordType(FromIterator::from_iter(once((
+                    label.clone(),
+                    nir,
+                ))));
+                nir = Nir::from_kind(rec);
+            }
+
+            // Update visited records
+            while let Some((label, mut kts)) = visited.pop() {
+                kts.insert(label.clone(), nir);
+                let rec = RecordType(kts);
+                nir = Nir::from_kind(rec);
+            }
+
+            nir.to_type(Const::Type)
+        }
+        Completion(..) => {
             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 572df25..dc1951e 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -2,7 +2,6 @@ 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;
 
@@ -13,8 +12,8 @@ use crate::operations::{BinOp, OpKind};
 use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type};
 use crate::syntax;
 use crate::syntax::{
-    Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget,
-    Label, Span, UnspannedExpr, URL,
+    Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget, Span,
+    UnspannedExpr, URL,
 };
 use crate::{Parsed, Resolved, Typed};
 
@@ -267,30 +266,6 @@ fn resolve_one_import(
     Ok(Typed { hir, ty })
 }
 
-/// 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() {
@@ -316,9 +291,6 @@ 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/tests/spec.rs b/dhall/tests/spec.rs
index 36cbd81..c93be7e 100644
--- a/dhall/tests/spec.rs
+++ b/dhall/tests/spec.rs
@@ -544,12 +544,7 @@ fn define_features() -> Vec<TestFeature> {
             variant: SpecTestKind::TypeInferenceSuccess,
             // TODO: this fails because of caching shenanigans
             // too_slow_path: Rc::new(|path: &str| path == "prelude"),
-            exclude_path: Rc::new(|path: &str| {
-                false
-                    || path == "prelude"
-                    // With builtin not implemented yet
-                    || path == "unit/WithCreateIntermediateRecords"
-            }),
+            exclude_path: Rc::new(|path: &str| path == "prelude"),
             ..default_feature.clone()
         },
         TestFeature {
diff --git a/dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt b/dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt
index c34175f..c2af394 100644
--- a/dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt
+++ b/dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt
@@ -1,7 +1,7 @@
-Type error: error: MustCombineRecord
+Type error: error: WithMustBeRecord
  --> <current file>:1:1
   |
 ...
 6 | { a = 1 } with a.b = 2
-  | ^^^^^^^^^^^^^^^^^^^^^^ MustCombineRecord
+  | ^^^^^^^^^^^^^^^^^^^^^^ WithMustBeRecord
   |
diff --git a/dhall/tests/type-inference/failure/unit/WithNotRecord.txt b/dhall/tests/type-inference/failure/unit/WithNotRecord.txt
index 8574e48..cd76485 100644
--- a/dhall/tests/type-inference/failure/unit/WithNotRecord.txt
+++ b/dhall/tests/type-inference/failure/unit/WithNotRecord.txt
@@ -1,6 +1,6 @@
-Type error: error: MustCombineRecord
+Type error: error: WithMustBeRecord
  --> <current file>:1:1
   |
 1 | 5 with a = 10
-  | ^^^^^^^^^^^^^ MustCombineRecord
+  | ^^^^^^^^^^^^^ WithMustBeRecord
   |