From 6987b275e4bf5f545d823d186ce08a2fe9a3eb44 Mon Sep 17 00:00:00 2001
From: Basile Henry
Date: Sun, 1 Nov 2020 22:46:35 +0100
Subject: Implement type checking for With op

---
 dhall/tests/spec.rs                                              | 7 +------
 dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt | 4 ++--
 dhall/tests/type-inference/failure/unit/WithNotRecord.txt        | 4 ++--
 3 files changed, 5 insertions(+), 10 deletions(-)

(limited to 'dhall/tests')

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
   |
-- 
cgit v1.3.1


From 7066e625fc945e66d8af91c633e762fe5f7b17f5 Mon Sep 17 00:00:00 2001
From: Basile Henry
Date: Sun, 1 Nov 2020 23:33:38 +0100
Subject: Handle partially abstract with

---
 dhall/src/operations/normalization.rs | 37 +++++++++++++++++++++++++++--------
 dhall/tests/spec.rs                   |  4 ----
 2 files changed, 29 insertions(+), 12 deletions(-)

(limited to 'dhall/tests')

diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs
index 908ed93..f147f85 100644
--- a/dhall/src/operations/normalization.rs
+++ b/dhall/src/operations/normalization.rs
@@ -306,16 +306,24 @@ pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
             let mut visited: Vec<(&Label, HashMap<Label, Nir>)> = Vec::new();
             let mut to_create = Vec::new();
 
+            // To be used when an abstract entry is reached
+            let mut abstract_nir = None;
+
             for label in labels {
                 match current_nk {
-                    None => to_create.push(label),
+                    None => to_create.push(label.clone()),
                     Some(nk) => match nk {
                         RecordLit(kvs) => {
                             current_nk =
                                 kvs.get(label).map(|nir| nir.kind().clone());
                             visited.push((label, kvs));
                         }
-                        _ => return nothing_to_do(),
+                        // Handle partially abstract case
+                        nir => {
+                            abstract_nir = Some(Nir::from_kind(nir));
+                            to_create.push(label.clone());
+                            current_nk = None;
+                        }
                     },
                 }
             }
@@ -323,12 +331,25 @@ pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
             // Create Nir for record bottom up
             let mut nir = expr.clone();
 
-            while let Some(label) = to_create.pop() {
-                let rec = RecordLit(FromIterator::from_iter(once((
-                    label.clone(),
-                    nir,
-                ))));
-                nir = Nir::from_kind(rec);
+            match abstract_nir {
+                // No abstract nir, creating singleton records
+                None => {
+                    while let Some(label) = to_create.pop() {
+                        let rec = RecordLit(FromIterator::from_iter(once((
+                            label.clone(),
+                            nir,
+                        ))));
+                        nir = Nir::from_kind(rec);
+                    }
+                }
+                // Abstract nir, creating with op
+                Some(abstract_nir) => {
+                    nir = Nir::from_kind(Op(OpKind::With(
+                        abstract_nir,
+                        to_create,
+                        nir,
+                    )));
+                }
             }
 
             // Update visited records
diff --git a/dhall/tests/spec.rs b/dhall/tests/spec.rs
index c93be7e..357181a 100644
--- a/dhall/tests/spec.rs
+++ b/dhall/tests/spec.rs
@@ -521,10 +521,6 @@ fn define_features() -> Vec<TestFeature> {
                     || path == "simple/integerToDouble"
                     // TODO: fix Double/show
                     || path == "prelude/JSON/number/1"
-                    // With builtin not implemented yet
-                    || path == "unit/WithCreateIntermediateRecords"
-                    || path == "unit/WithDesugar"
-                    || path == "unit/WithPartiallyAbstract"
             }),
             ..default_feature.clone()
         },
-- 
cgit v1.3.1