From f2917ee07b8fbbe6a411dd057a0191b1e8ba5680 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 27 Apr 2019 19:21:22 +0200
Subject: Replace TypeInternal::UnionType with WHNF::UnionType

---
 dhall/src/typecheck.rs | 46 +++++++++++++++++++++++-----------------------
 1 file changed, 23 insertions(+), 23 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 9e985e4..d3213b1 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -162,7 +162,6 @@ impl TypeThunk {
 pub(crate) enum TypeInternal<'a> {
     Const(Const),
     Pi(Const, Label, Box<Type<'static>>, Box<Type<'static>>),
-    UnionType(Const, BTreeMap<Label, Option<Type<'static>>>),
     ListType(Box<Type<'static>>),
     OptionalType(Box<Type<'static>>),
     /// The type of `Sort`
@@ -194,13 +193,6 @@ impl<'a> TypeInternal<'a> {
                 Some(const_to_type(c)),
                 PhantomData,
             ),
-            TypeInternal::UnionType(c, kts) => Normalized(
-                rc(ExprF::UnionType(kts).traverse_ref_simple(|e| {
-                    Ok(e.clone().into_normalized()?.into_expr())
-                })?),
-                Some(const_to_type(c)),
-                PhantomData,
-            ),
             TypeInternal::ListType(t) => Normalized(
                 rc(ExprF::App(
                     rc(ExprF::Builtin(Builtin::List)),
@@ -239,14 +231,6 @@ impl<'a> TypeInternal<'a> {
                 Box::new(t.shift(delta, var)),
                 Box::new(e.shift(delta, &var.shift0(1, x))),
             ),
-            UnionType(c, kts) => UnionType(
-                *c,
-                kts.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.as_ref().map(|v| v.shift(delta, var)))
-                    })
-                    .collect(),
-            ),
             ListType(t) => ListType(Box::new(t.shift(delta, var))),
             OptionalType(t) => OptionalType(Box::new(t.shift(delta, var))),
             Const(c) => Const(*c),
@@ -695,10 +679,26 @@ impl TypeIntermediate {
                 // An empty union type has type Type;
                 // an union type with only unary variants also has type Type
                 let k = k.unwrap_or(dhall_core::Const::Type);
-                Ok(TypedOrType::Type(Type(TypeInternal::UnionType(
-                    k,
-                    kts.clone(),
-                ))))
+
+                let pnormalized = PartiallyNormalized(
+                    WHNF::UnionType(
+                        kts.iter()
+                            .map(|(k, t)| {
+                                (
+                                    k.clone(),
+                                    t.as_ref().map(|t| {
+                                        TypeThunk::from_type(t.clone())
+                                    }),
+                                )
+                            })
+                            .collect(),
+                    ),
+                    Some(const_to_type(k)),
+                    PhantomData,
+                );
+                Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
+                    pnormalized,
+                )))))
             }
             TypeIntermediate::ListType(ctx, t) => {
                 ensure_simple_type!(
@@ -1028,15 +1028,15 @@ fn type_last_layer(
             },
             _ => {
                 let r = r.normalize_to_type()?;
-                match r.internal() {
-                    TypeInternal::UnionType(_, kts) => match kts.get(&x) {
+                match r.internal_whnf() {
+                    Some(WHNF::UnionType(kts)) => match kts.get(&x) {
                         // Constructor has type T -> < x: T, ... >
                         // TODO: use "_" instead of x (i.e. compare types using equivalence in tests)
                         Some(Some(t)) => Ok(RetType(
                             TypeIntermediate::Pi(
                                 ctx.clone(),
                                 x.clone(),
-                                t.clone(),
+                                t.clone().normalize_to_type(ctx)?,
                                 r,
                             )
                             .typecheck()?
-- 
cgit v1.2.3