Desugar Completion during resolution

5 files changed, 49 insertions, 55 deletions

diff --git a/dhall/build.rs b/dhall/build.rs
index 8deb637..7c62083 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -299,9 +299,6 @@ fn generate_tests() -> std::io::Result<()> {
                     || path == "unit/RecursiveRecordMergeWithinFieldSelection0"
                     || path == "unit/RecursiveRecordMergeWithinFieldSelection2"
                     || path == "unit/RecursiveRecordMergeWithinFieldSelection3"
-                    // TODO: record completion
-                    || path == "simple/completion"
-                    || path == "unit/Completion"
             }),
             input_type: FileType::Text,
             output_type: Some(FileType::Text),
diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index 42f151e..c8258ff 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -14,7 +14,7 @@ pub struct AlphaVar {
 pub(crate) enum HirKind {
     /// A resolved variable (i.e. a DeBruijn index)
     Var(AlphaVar),
-    // Forbidden ExprKind variants: Var, Import
+    // Forbidden ExprKind variants: Var, Import, Completion
     Expr(ExprKind<Hir>),
 }
 
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index c8dd5ae..0e09511 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -231,17 +231,16 @@ pub(crate) fn normalize_one_layer(
     };
 
     let ret = match expr {
-        ExprKind::Import(_) => unreachable!(
-            "There should remain no imports in a resolved expression"
-        ),
-        // Those cases have already been completely handled in the typechecking phase (using
-        // `RetWhole`), so they won't appear here.
-        ExprKind::Lam(..)
-        | ExprKind::Pi(..)
-        | ExprKind::Let(..)
-        | ExprKind::Var(_) => {
-            unreachable!("This case should have been handled in typecheck")
+        ExprKind::Import(..) | ExprKind::Completion(..) => {
+            unreachable!("This case should have been handled in resolution")
         }
+        ExprKind::Var(..)
+        | ExprKind::Lam(..)
+        | ExprKind::Pi(..)
+        | ExprKind::Let(..) => unreachable!(
+            "This case should have been handled in normalize_hir_whnf"
+        ),
+
         ExprKind::Annot(x, _) => Ret::Value(x),
         ExprKind::Const(c) => Ret::Value(Value::from_const(c)),
         ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)),
@@ -391,7 +390,6 @@ pub(crate) fn normalize_one_layer(
         ExprKind::ProjectionByExpr(_, _) => {
             unimplemented!("selection by expression")
         }
-        ExprKind::Completion(_, _) => unimplemented!("record completion"),
 
         ExprKind::Merge(ref handlers, ref variant, _) => {
             match handlers.kind() {
diff --git a/dhall/src/semantics/resolve.rs b/dhall/src/semantics/resolve.rs
index fac88d2..3038597 100644
--- a/dhall/src/semantics/resolve.rs
+++ b/dhall/src/semantics/resolve.rs
@@ -105,9 +105,9 @@ fn traverse_resolve_expr(
     expr: &Expr,
     f: &mut impl FnMut(Import) -> Result<Hir, Error>,
 ) -> Result<Hir, Error> {
-    let kind = match expr.kind() {
+    Ok(match expr.kind() {
         ExprKind::Var(var) => match name_env.unlabel_var(&var) {
-            Some(v) => HirKind::Var(v),
+            Some(v) => Hir::new(HirKind::Var(v), expr.span()),
             None => mkerr(
                 ErrorBuilder::new(format!("unbound variable `{}`", var))
                     .span_err(expr.span(), "not found in this scope")
@@ -115,16 +115,38 @@ fn traverse_resolve_expr(
             )?,
         },
         ExprKind::BinOp(BinOp::ImportAlt, l, r) => {
-            return match traverse_resolve_expr(name_env, l, f) {
-                Ok(l) => Ok(l),
+            match traverse_resolve_expr(name_env, l, f) {
+                Ok(l) => l,
                 Err(_) => {
                     match traverse_resolve_expr(name_env, r, f) {
-                        Ok(r) => Ok(r),
+                        Ok(r) => r,
                         // TODO: keep track of the other error too
-                        Err(e) => Err(e),
+                        Err(e) => return Err(e),
                     }
                 }
-            };
+            }
+        }
+        // Desugar
+        ExprKind::Completion(ty, compl) => {
+            let ty_field_default = Expr::new(
+                ExprKind::Field(ty.clone(), "default".into()),
+                expr.span(),
+            );
+            let merged = Expr::new(
+                ExprKind::BinOp(
+                    BinOp::RightBiasedRecordMerge,
+                    ty_field_default,
+                    compl.clone(),
+                ),
+                expr.span(),
+            );
+            let ty_field_type = Expr::new(
+                ExprKind::Field(ty.clone(), "Type".into()),
+                expr.span(),
+            );
+            let desugared =
+                Expr::new(ExprKind::Annot(merged, ty_field_type), expr.span());
+            traverse_resolve_expr(name_env, &desugared, f)?
         }
         kind => {
             let kind = kind.traverse_ref_maybe_binder(|l, e| {
@@ -137,14 +159,13 @@ fn traverse_resolve_expr(
                 }
                 Ok::<_, Error>(hir)
             })?;
-            match kind {
+            let kind = match kind {
                 ExprKind::Import(import) => f(import)?.kind().clone(),
                 kind => HirKind::Expr(kind),
-            }
+            };
+            Hir::new(kind, expr.span())
         }
-    };
-
-    Ok(Hir::new(kind, expr.span()))
+    })
 }
 
 fn resolve_with_env(
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a8a2d95..36f7173 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -75,12 +75,14 @@ fn type_one_layer(
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
 
     let ty = match &ekind {
-        ExprKind::Import(..) => unreachable!(
-            "There should remain no imports in a resolved expression"
-        ),
+        ExprKind::Import(..) | ExprKind::Completion(..) => {
+            unreachable!("This case should have been handled in resolution")
+        }
         ExprKind::Var(..)
         | ExprKind::Const(Const::Sort)
-        | ExprKind::Annot(..) => unreachable!(), // Handled in type_with
+        | ExprKind::Annot(..) => {
+            unreachable!("This case should have been handled in type_with")
+        }
 
         ExprKind::Lam(binder, annot, body) => {
             if annot.ty().as_const().is_none() {
@@ -739,30 +741,6 @@ fn type_one_layer(
 
             selection_val
         }
-        ExprKind::Completion(ty, compl) => {
-            let ty_field_default = type_one_layer(
-                env,
-                ExprKind::Field(ty.clone(), "default".into()),
-                None,
-                span.clone(),
-            )?;
-            let ty_field_type = type_one_layer(
-                env,
-                ExprKind::Field(ty.clone(), "Type".into()),
-                None,
-                span.clone(),
-            )?;
-            return type_one_layer(
-                env,
-                ExprKind::BinOp(
-                    BinOp::RightBiasedRecordMerge,
-                    ty_field_default,
-                    compl.clone(),
-                ),
-                Some(ty_field_type.eval(env)),
-                span.clone(),
-            );
-        }
     };
 
     if let Some(annot) = annot {