From 5465b7e2b8cc286e2e8b87556b3ec6a2476cf0cf Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 2 May 2019 12:54:35 +0200
Subject: Tweaks

---
 dhall/src/normalize.rs          | 84 +++++++++++++++++++----------------------
 dhall/src/traits/static_type.rs |  2 +-
 dhall/src/typecheck.rs          | 68 ++++++++++++++++++---------------
 3 files changed, 78 insertions(+), 76 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index dbb6d95..7a69bea 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -383,8 +383,8 @@ impl Value {
         match self {
             Value::Lam(x, t, e) => rc(ExprF::Lam(
                 x.clone(),
-                t.normalize_nf().normalize_to_expr(),
-                e.normalize_nf().normalize_to_expr(),
+                t.normalize_to_expr(),
+                e.normalize_to_expr(),
             )),
             Value::AppliedBuiltin(b, args) => {
                 let mut e = rc(ExprF::Builtin(*b));
@@ -394,18 +394,18 @@ impl Value {
                 e
             }
             Value::OptionalSomeClosure(n) => {
-                let a = n.normalize_nf().normalize_to_expr();
+                let a = n.normalize_to_expr();
                 dhall::subexpr!(λ(x: a) -> Some x)
             }
             Value::ListConsClosure(n, None) => {
-                let a = n.normalize_nf().normalize_to_expr();
+                let a = n.normalize_to_expr();
                 // Avoid accidental capture of the new `x` variable
                 let a1 = a.shift0(1, &"x".into());
                 dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
             }
             Value::ListConsClosure(n, Some(v)) => {
-                let v = v.normalize_nf().normalize_to_expr();
-                let a = n.normalize_nf().normalize_to_expr();
+                let v = v.normalize_to_expr();
+                let a = n.normalize_to_expr();
                 // Avoid accidental capture of the new `xs` variable
                 let v = v.shift0(1, &"xs".into());
                 dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
@@ -415,8 +415,8 @@ impl Value {
             }
             Value::Pi(x, t, e) => rc(ExprF::Pi(
                 x.clone(),
-                t.normalize_nf().normalize_to_expr(),
-                e.normalize_nf().normalize_to_expr(),
+                t.normalize_to_expr(),
+                e.normalize_to_expr(),
             )),
             Value::Var(v) => rc(ExprF::Var(v.clone())),
             Value::Const(c) => rc(ExprF::Const(*c)),
@@ -425,41 +425,31 @@ impl Value {
             Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
             Value::EmptyOptionalLit(n) => rc(ExprF::App(
                 rc(ExprF::Builtin(Builtin::OptionalNone)),
-                n.normalize_nf().normalize_to_expr(),
+                n.normalize_to_expr(),
             )),
             Value::NEOptionalLit(n) => {
-                rc(ExprF::SomeLit(n.normalize_nf().normalize_to_expr()))
+                rc(ExprF::SomeLit(n.normalize_to_expr()))
             }
             Value::EmptyListLit(n) => {
-                rc(ExprF::EmptyListLit(n.normalize_nf().normalize_to_expr()))
+                rc(ExprF::EmptyListLit(n.normalize_to_expr()))
             }
             Value::NEListLit(elts) => rc(ExprF::NEListLit(
-                elts.into_iter()
-                    .map(|n| n.normalize_nf().normalize_to_expr())
-                    .collect(),
+                elts.into_iter().map(|n| n.normalize_to_expr()).collect(),
             )),
             Value::RecordLit(kvs) => rc(ExprF::RecordLit(
                 kvs.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.normalize_nf().normalize_to_expr())
-                    })
+                    .map(|(k, v)| (k.clone(), v.normalize_to_expr()))
                     .collect(),
             )),
             Value::RecordType(kts) => rc(ExprF::RecordType(
                 kts.iter()
-                    .map(|(k, v)| {
-                        (k.clone(), v.normalize_nf().normalize_to_expr())
-                    })
+                    .map(|(k, v)| (k.clone(), v.normalize_to_expr()))
                     .collect(),
             )),
             Value::UnionType(kts) => rc(ExprF::UnionType(
                 kts.iter()
                     .map(|(k, v)| {
-                        (
-                            k.clone(),
-                            v.as_ref()
-                                .map(|v| v.normalize_nf().normalize_to_expr()),
-                        )
+                        (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
                     })
                     .collect(),
             )),
@@ -467,25 +457,17 @@ impl Value {
                 let kts = kts
                     .iter()
                     .map(|(k, v)| {
-                        (
-                            k.clone(),
-                            v.as_ref()
-                                .map(|v| v.normalize_nf().normalize_to_expr()),
-                        )
+                        (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
                     })
                     .collect();
                 rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
             }
             Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit(
                 l.clone(),
-                v.normalize_nf().normalize_to_expr(),
+                v.normalize_to_expr(),
                 kts.iter()
                     .map(|(k, v)| {
-                        (
-                            k.clone(),
-                            v.as_ref()
-                                .map(|v| v.normalize_nf().normalize_to_expr()),
-                        )
+                        (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
                     })
                     .collect(),
             )),
@@ -961,7 +943,10 @@ impl Value {
 }
 
 mod thunk {
-    use super::{normalize_whnf, InputSubExpr, NormalizationContext, Value};
+    use super::{
+        normalize_whnf, InputSubExpr, NormalizationContext, OutputSubExpr,
+        Value,
+    };
     use crate::expr::Typed;
     use dhall_core::{Label, V};
     use std::cell::{Ref, RefCell};
@@ -1108,6 +1093,10 @@ mod thunk {
             Ref::map(self.0.borrow(), ThunkInternal::as_nf)
         }
 
+        pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+            self.normalize_nf().normalize_to_expr()
+        }
+
         pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
             self.0.borrow().shift(delta, var).into_thunk()
         }
@@ -1148,6 +1137,7 @@ impl TypeThunk {
         TypeThunk::Type(t)
     }
 
+    // Deprecated
     fn normalize(&self) -> TypeThunk {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.normalize()),
@@ -1162,6 +1152,18 @@ impl TypeThunk {
         }
     }
 
+    pub(crate) fn normalize_nf(&self) -> Value {
+        match self {
+            TypeThunk::Thunk(th) => th.normalize_nf().clone(),
+            // TODO: let's hope for the best with the unwrap
+            TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(),
+        }
+    }
+
+    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+        self.normalize_nf().normalize_to_expr()
+    }
+
     fn shift(&self, delta: isize, var: &V<Label>) -> Self {
         match self {
             TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
@@ -1179,14 +1181,6 @@ impl TypeThunk {
             TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
         }
     }
-
-    pub(crate) fn normalize_nf(&self) -> Value {
-        match self {
-            TypeThunk::Thunk(th) => th.normalize_nf().clone(),
-            // TODO: let's hope for the best with the unwrap
-            TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(),
-        }
-    }
 }
 
 /// Reduces the imput expression to Value. See doc on `Value` for details.
diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs
index 225eb32..8b5acbf 100644
--- a/dhall/src/traits/static_type.rs
+++ b/dhall/src/traits/static_type.rs
@@ -33,7 +33,7 @@ pub trait SimpleStaticType {
 }
 
 fn mktype<'a>(x: SubExpr<X, X>) -> SimpleType<'a> {
-    SimpleType(x, std::marker::PhantomData)
+    x.into()
 }
 
 impl<T: SimpleStaticType> StaticType for T {
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index cdc53a3..e8bc26d 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -66,7 +66,7 @@ impl<'a> Normalized<'a> {
             ExprF::Const(c) => Type(TypeInternal::Const(*c)),
             ExprF::Pi(_, _, _) | ExprF::RecordType(_) | ExprF::UnionType(_) => {
                 // TODO: wasteful
-                type_with(ctx, self.0.embed_absurd())?.normalize_to_type()
+                type_with(ctx, self.0.embed_absurd())?.to_type()
             }
             _ => Type(TypeInternal::Typed(Box::new(Typed(
                 Value::Expr(self.0).into_thunk(),
@@ -87,7 +87,7 @@ impl Normalized<'static> {
     }
 }
 impl<'a> Typed<'a> {
-    fn normalize_to_type(&self) -> Type<'a> {
+    fn to_type(&self) -> Type<'a> {
         match &*self.normalize_whnf() {
             Value::Const(c) => Type(TypeInternal::Const(*c)),
             _ => Type(TypeInternal::Typed(Box::new(self.clone()))),
@@ -106,6 +106,9 @@ impl<'a> Type<'a> {
     pub(crate) fn normalize_whnf(&self) -> Result<Value, TypeError> {
         Ok(self.0.normalize_whnf()?)
     }
+    fn as_const(&self) -> Option<Const> {
+        self.0.as_const()
+    }
     fn internal(&self) -> &TypeInternal<'a> {
         &self.0
     }
@@ -192,6 +195,12 @@ impl<'a> TypeInternal<'a> {
             }
         })
     }
+    fn as_const(&self) -> Option<Const> {
+        match self {
+            TypeInternal::Const(c) => Some(*c),
+            _ => None,
+        }
+    }
     fn whnf(&self) -> Option<std::cell::Ref<Value>> {
         match self {
             TypeInternal::Typed(e) => Some(e.normalize_whnf()),
@@ -491,8 +500,8 @@ macro_rules! ensure_equal {
 // Ensure the provided type has type `Type`
 macro_rules! ensure_simple_type {
     ($x:expr, $err:expr $(,)*) => {{
-        match $x.get_type()?.internal() {
-            TypeInternal::Const(dhall_core::Const::Type) => {}
+        match $x.get_type()?.as_const() {
+            Some(dhall_core::Const::Type) => {}
             _ => return Err($err),
         }
     }};
@@ -514,8 +523,8 @@ impl TypeIntermediate {
             TypeIntermediate::Pi(ctx, x, ta, tb) => {
                 let ctx2 = ctx.insert_type(x, ta.clone());
 
-                let kA = match ta.get_type()?.internal() {
-                    TypeInternal::Const(k) => *k,
+                let kA = match ta.get_type()?.as_const() {
+                    Some(k) => k,
                     _ => {
                         return Err(mkerr(
                             ctx,
@@ -524,8 +533,8 @@ impl TypeIntermediate {
                     }
                 };
 
-                let kB = match tb.get_type()?.internal() {
-                    TypeInternal::Const(k) => *k,
+                let kB = match tb.get_type()?.as_const() {
+                    Some(k) => k,
                     _ => {
                         return Err(mkerr(
                             &ctx2,
@@ -570,9 +579,9 @@ impl TypeIntermediate {
                 // Check that all types are the same const
                 let mut k = None;
                 for (x, t) in kts {
-                    match (k, t.get_type()?.internal()) {
-                        (None, TypeInternal::Const(k2)) => k = Some(*k2),
-                        (Some(k1), TypeInternal::Const(k2)) if k1 == *k2 => {}
+                    match (k, t.get_type()?.as_const()) {
+                        (None, Some(k2)) => k = Some(k2),
+                        (Some(k1), Some(k2)) if k1 == k2 => {}
                         _ => {
                             return Err(mkerr(
                                 ctx,
@@ -602,10 +611,9 @@ impl TypeIntermediate {
                 let mut k = None;
                 for (x, t) in kts {
                     if let Some(t) = t {
-                        match (k, t.get_type()?.internal()) {
-                            (None, TypeInternal::Const(k2)) => k = Some(*k2),
-                            (Some(k1), TypeInternal::Const(k2))
-                                if k1 == *k2 => {}
+                        match (k, t.get_type()?.as_const()) {
+                            (None, Some(k2)) => k = Some(k2),
+                            (Some(k1), Some(k2)) if k1 == k2 => {}
                             _ => {
                                 return Err(mkerr(
                                     ctx,
@@ -677,7 +685,7 @@ fn mktype(
     ctx: &TypecheckContext,
     e: SubExpr<X, Normalized<'static>>,
 ) -> Result<Type<'static>, TypeError> {
-    Ok(type_with(ctx, e)?.normalize_to_type())
+    Ok(type_with(ctx, e)?.to_type())
 }
 
 fn builtin_to_type<'a>(b: Builtin) -> Result<Type<'a>, TypeError> {
@@ -713,7 +721,7 @@ fn type_with(
             Ok(RetType(
                 TypeIntermediate::Pi(ctx.clone(), x.clone(), tx, tb)
                     .typecheck()?
-                    .normalize_to_type(),
+                    .to_type(),
             ))
         }
         Pi(x, ta, tb) => {
@@ -813,7 +821,7 @@ fn type_last_layer(
             Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a)))
         }
         Annot(x, t) => {
-            let t = t.normalize_to_type();
+            let t = t.to_type();
             ensure_equal!(
                 &t,
                 x.get_type()?,
@@ -847,11 +855,11 @@ fn type_last_layer(
             Ok(RetType(y.get_type_move()?))
         }
         EmptyListLit(t) => {
-            let t = t.normalize_to_type();
+            let t = t.to_type();
             Ok(RetType(
                 TypeIntermediate::ListType(ctx.clone(), t)
                     .typecheck()?
-                    .normalize_to_type(),
+                    .to_type(),
             ))
         }
         NEListLit(xs) => {
@@ -872,7 +880,7 @@ fn type_last_layer(
             Ok(RetType(
                 TypeIntermediate::ListType(ctx.clone(), t)
                     .typecheck()?
-                    .normalize_to_type(),
+                    .to_type(),
             ))
         }
         SomeLit(x) => {
@@ -880,13 +888,13 @@ fn type_last_layer(
             Ok(RetType(
                 TypeIntermediate::OptionalType(ctx.clone(), t)
                     .typecheck()?
-                    .normalize_to_type(),
+                    .to_type(),
             ))
         }
         RecordType(kts) => {
             let kts: BTreeMap<_, _> = kts
                 .into_iter()
-                .map(|(x, t)| Ok((x, t.normalize_to_type())))
+                .map(|(x, t)| Ok((x, t.to_type())))
                 .collect::<Result<_, _>>()?;
             Ok(RetTyped(
                 TypeIntermediate::RecordType(ctx.clone(), kts).typecheck()?,
@@ -900,7 +908,7 @@ fn type_last_layer(
                         x,
                         match t {
                             None => None,
-                            Some(t) => Some(t.normalize_to_type()),
+                            Some(t) => Some(t.to_type()),
                         },
                     ))
                 })
@@ -917,7 +925,7 @@ fn type_last_layer(
             Ok(RetType(
                 TypeIntermediate::RecordType(ctx.clone(), kts)
                     .typecheck()?
-                    .normalize_to_type(),
+                    .to_type(),
             ))
         }
         UnionLit(x, v, kvs) => {
@@ -925,7 +933,7 @@ fn type_last_layer(
                 .into_iter()
                 .map(|(x, v)| {
                     let t = match v {
-                        Some(x) => Some(x.normalize_to_type()),
+                        Some(x) => Some(x.to_type()),
                         None => None,
                     };
                     Ok((x, t))
@@ -936,7 +944,7 @@ fn type_last_layer(
             Ok(RetType(
                 TypeIntermediate::UnionType(ctx.clone(), kts)
                     .typecheck()?
-                    .normalize_to_type(),
+                    .to_type(),
             ))
         }
         Field(r, x) => {
@@ -953,7 +961,7 @@ fn type_last_layer(
                 },
                 // TODO: branch here only when r.get_type() is a Const
                 _ => {
-                    let r = r.normalize_to_type();
+                    let r = r.to_type();
                     let r_internal = r.internal_whnf();
                     match r_internal.deref() {
                         Some(Value::UnionType(kts)) => match kts.get(&x) {
@@ -970,7 +978,7 @@ fn type_last_layer(
                                         r,
                                     )
                                     .typecheck()?
-                                    .normalize_to_type(),
+                                    .to_type(),
                                 ))
                             },
                             Some(None) => {
@@ -996,7 +1004,7 @@ fn type_last_layer(
                 }
                 // _ => Err(mkerr(NotARecord(
                 //     x,
-                //     r.normalize_to_type()?.into_normalized()?,
+                //     r.to_type()?.into_normalized()?,
                 // ))),
             }
         }
-- 
cgit v1.2.3