From d5bdd48d4c34b4e213e3e2431936c160e4320a80 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 23 Aug 2019 18:53:46 +0200
Subject: Clarify which syntax elements are completely handled in the tck phase

---
 dhall/src/phase/normalize.rs | 40 ++++++++++++++++++----------------------
 dhall/src/phase/typecheck.rs |  9 ++++++---
 2 files changed, 24 insertions(+), 25 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 28dc0f6..c8f5bc2 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -578,39 +578,41 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
             Ret::ValueF(RecordLit(kvs))
         }
 
-        (RecursiveRecordTypeMerge, _, _) => {
+        (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => {
             unreachable!("This case should have been handled in typecheck")
         }
 
-        (Equivalence, _, _) => {
-            Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone()))
-        }
-
         _ => return None,
     })
 }
 
 pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
     use ValueF::{
-        AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
-        NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
-        TextLit, UnionConstructor, UnionLit, UnionType,
+        AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
+        NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
+        UnionConstructor, UnionLit, UnionType,
     };
 
     let ret = match expr {
         ExprF::Import(_) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
-        ExprF::Embed(_) => unreachable!(),
-        ExprF::Var(_) => unreachable!(),
-        ExprF::Annot(x, _) => Ret::Value(x),
+        // Those cases have already been completely handled in the typechecking phase (using
+        // `RetWhole`), so they won't appear here.
+        ExprF::Lam(_, _, _)
+        | ExprF::Pi(_, _, _)
+        | ExprF::Let(_, _, _, _)
+        | ExprF::Embed(_)
+        | ExprF::Const(_)
+        | ExprF::Builtin(_)
+        | ExprF::Var(_)
+        | ExprF::Annot(_, _)
+        | ExprF::RecordType(_)
+        | ExprF::UnionType(_) => {
+            unreachable!("This case should have been handled in typecheck")
+        }
         ExprF::Assert(_) => Ret::Expr(expr),
-        ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)),
-        ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)),
-        ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)),
         ExprF::App(v, a) => Ret::Value(v.app(a)),
-        ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
-        ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
         ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
         ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)),
         ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)),
@@ -635,12 +637,6 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
         ExprF::RecordLit(kvs) => {
             Ret::ValueF(RecordLit(kvs.into_iter().collect()))
         }
-        ExprF::RecordType(kts) => {
-            Ret::ValueF(RecordType(kts.into_iter().collect()))
-        }
-        ExprF::UnionType(kts) => {
-            Ret::ValueF(UnionType(kts.into_iter().collect()))
-        }
         ExprF::TextLit(elts) => {
             use InterpolatedTextContents::Expr;
             let elts: Vec<_> = squash_textlit(elts.into_iter());
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 363d733..0268b80 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -291,7 +291,7 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
 pub(crate) fn builtin_to_value(b: Builtin) -> Value {
     let ctx = TypecheckContext::new();
     Value::from_valuef_and_type(
-        ValueF::PartialExpr(ExprF::Builtin(b)),
+        ValueF::from_builtin(b),
         type_with(&ctx, rc(type_of_builtin(b))).unwrap(),
     )
 }
@@ -399,7 +399,7 @@ fn type_last_layer(
             if &x.get_type()? != t {
                 return mkerr(AnnotMismatch(x.clone(), t.clone()));
             }
-            RetTypeOnly(x.get_type()?)
+            RetWhole(x.clone())
         }
         Assert(t) => {
             match &*t.as_whnf() {
@@ -649,7 +649,10 @@ fn type_last_layer(
                 return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
             }
 
-            RetTypeOnly(Value::from_const(Type))
+            RetWhole(Value::from_valuef_and_type(
+                ValueF::Equivalence(l.clone(), r.clone()),
+                Value::from_const(Type),
+            ))
         }
         BinOp(o, l, r) => {
             let t = builtin_to_value(match o {
-- 
cgit v1.2.3