From de7664d9dda95dd16742bc30e16a967c43d687ee Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 5 Feb 2020 18:10:41 +0000
Subject: Typecheck record completion

---
 dhall/src/semantics/tck/typecheck.rs | 76 ++++++++++++++++++++++++------------
 1 file changed, 51 insertions(+), 25 deletions(-)

(limited to 'dhall/src/semantics/tck/typecheck.rs')

diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index e3ae129..6817712 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -51,9 +51,9 @@ fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
 /// layer.
 fn type_one_layer(
     env: &TyEnv,
-    kind: &ExprKind<TyExpr, Normalized>,
+    ekind: ExprKind<TyExpr, Normalized>,
     span: Span,
-) -> Result<Type, TypeError> {
+) -> Result<TyExpr, TypeError> {
     let span_err = |msg: &str| {
         mkerr(
             ErrorBuilder::new(msg.to_string())
@@ -62,7 +62,7 @@ fn type_one_layer(
         )
     };
 
-    Ok(match kind {
+    let ty = match &ekind {
         ExprKind::Import(..) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
@@ -74,13 +74,8 @@ fn type_one_layer(
             let body_ty = body.get_type()?;
             let body_ty = body_ty.to_tyexpr(env.as_varenv().insert());
             let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
-            let pi_ty = type_one_layer(env, &pi_ekind, Span::Artificial)?;
-            let ty = TyExpr::new(
-                TyExprKind::Expr(pi_ekind),
-                Some(pi_ty),
-                Span::Artificial,
-            );
-            ty.eval(env.as_nzenv())
+            type_one_layer(env, pi_ekind, Span::Artificial)?
+                .eval(env.as_nzenv())
         }
         ExprKind::Pi(_, annot, body) => {
             let ks = match annot.get_type()?.as_const() {
@@ -187,7 +182,7 @@ fn type_one_layer(
             }
 
             let ty = type_of_recordtype(
-                span,
+                span.clone(),
                 kts.iter()
                     .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
             )?;
@@ -206,7 +201,10 @@ fn type_one_layer(
                 };
             }
 
-            type_of_recordtype(span, kts.iter().map(|(_, t)| Cow::Borrowed(t)))?
+            type_of_recordtype(
+                span.clone(),
+                kts.iter().map(|(_, t)| Cow::Borrowed(t)),
+            )?
         }
         ExprKind::UnionType(kts) => {
             use std::collections::hash_map::Entry;
@@ -389,7 +387,7 @@ fn type_one_layer(
 
             // Construct the final record type
             let ty = type_of_recordtype(
-                span,
+                span.clone(),
                 kts.iter()
                     .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
             )?;
@@ -401,9 +399,7 @@ fn type_one_layer(
                 x.get_type()?.to_tyexpr(env.as_varenv()),
                 y.get_type()?.to_tyexpr(env.as_varenv()),
             );
-            let ty = type_one_layer(env, &ekind, Span::Artificial)?;
-            TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
-                .eval(env.as_nzenv())
+            type_one_layer(env, ekind, Span::Artificial)?.eval(env.as_nzenv())
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
             let x_val = x.eval(env.as_nzenv());
@@ -420,7 +416,7 @@ fn type_one_layer(
                 if let Some(ty) = kts_y.get(k) {
                     type_one_layer(
                         env,
-                        &ExprKind::BinOp(
+                        ExprKind::BinOp(
                             BinOp::RecursiveRecordTypeMerge,
                             tx.to_tyexpr(env.as_varenv()),
                             ty.to_tyexpr(env.as_varenv()),
@@ -547,9 +543,14 @@ fn type_one_layer(
                                 );
                             }
 
-                            closure.remove_binder().or_else(|()| {
-                                span_err("MergeReturnTypeIsDependent")
-                            })?
+                            match closure.remove_binder() {
+                                Ok(v) => v,
+                                Err(()) => {
+                                    return span_err(
+                                        "MergeReturnTypeIsDependent",
+                                    )
+                                }
+                            }
                         }
                         _ => {
                             return mkerr(
@@ -752,8 +753,35 @@ fn type_one_layer(
 
             selection_val
         }
-        ExprKind::Completion(_, _) => unimplemented!("record completion"),
-    })
+        ExprKind::Completion(ty, compl) => {
+            let ty_field_default = type_one_layer(
+                env,
+                ExprKind::Field(ty.clone(), "default".into()),
+                span.clone(),
+            )?;
+            let ty_field_type = type_one_layer(
+                env,
+                ExprKind::Field(ty.clone(), "Type".into()),
+                span.clone(),
+            )?;
+            let merge = type_one_layer(
+                env,
+                ExprKind::BinOp(
+                    BinOp::RightBiasedRecordMerge,
+                    ty_field_default,
+                    compl.clone(),
+                ),
+                span.clone(),
+            )?;
+            return type_one_layer(
+                env,
+                ExprKind::Annot(merge, ty_field_type),
+                span.clone(),
+            );
+        }
+    };
+
+    Ok(TyExpr::new(TyExprKind::Expr(ekind), Some(ty), span))
 }
 
 /// `type_with` typechecks an expressio in the provided environment.
@@ -809,9 +837,7 @@ pub(crate) fn type_with(
                 }
                 _ => ekind.traverse_ref(|e| type_with(env, e))?,
             };
-
-            let ty = type_one_layer(env, &ekind, expr.span())?;
-            (TyExprKind::Expr(ekind), Some(ty))
+            return type_one_layer(env, ekind, expr.span());
         }
     };
 
-- 
cgit v1.2.3