Thread Typed through type_with

3 files changed, 67 insertions, 66 deletions

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index ae52e4d..cc7f064 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -1,5 +1,4 @@
 use crate::imports::ImportRoot;
-use crate::typecheck::TypeError;
 use dhall_core::*;
 
 #[derive(Debug, Clone, Eq)]
@@ -9,10 +8,11 @@ pub struct Parsed(pub(crate) SubExpr<X, Import>, pub(crate) ImportRoot);
 pub struct Resolved(pub(crate) SubExpr<X, X>);
 
 #[derive(Debug, Clone)]
-pub struct Typed(pub(crate) SubExpr<X, X>, Type);
+pub struct Typed(pub(crate) SubExpr<X, X>, pub(crate) Type);
 
-#[derive(Debug, Clone)]
-pub struct Type(pub(crate) Box<Normalized>);
+// #[derive(Debug, Clone)]
+// pub struct Type(pub(crate) Box<Normalized>);
+pub type Type = SubExpr<X, X>;
 
 #[derive(Debug, Clone)]
 pub struct Normalized(pub(crate) SubExpr<X, X>);
@@ -28,24 +28,8 @@ impl std::fmt::Display for Parsed {
     }
 }
 
-impl Resolved {
-    pub fn typecheck(self) -> Result<Typed, TypeError<X>> {
-        let typ = Type(Box::new(Normalized(crate::typecheck::type_of(
-            self.0.clone(),
-        )?)));
-        Ok(Typed(self.0, typ))
-    }
-}
-impl Typed {
-    pub fn normalize(self) -> Normalized {
-        Normalized(crate::normalize::normalize(self.0))
-    }
-    pub fn get_type(&self) -> &Type {
-        &self.1
-    }
-}
-impl Type {
-    pub fn as_expr(&self) -> &Normalized {
-        &*self.0
-    }
-}
+// impl Type {
+//     pub fn as_expr(&self) -> &Normalized {
+//         &*self.0
+//     }
+// }
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 24a8601..8ed2136 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -1,8 +1,18 @@
 #![allow(non_snake_case)]
+use crate::expr::*;
 use dhall_core::*;
 use dhall_generator::dhall_expr;
 use std::fmt;
 
+impl Typed {
+    pub fn normalize(self) -> Normalized {
+        Normalized(normalize(self.0))
+    }
+    pub fn get_type(&self) -> &Type {
+        &self.1
+    }
+}
+
 fn apply_builtin<S, A>(b: Builtin, args: &Vec<Expr<S, A>>) -> WhatNext<S, A>
 where
     S: fmt::Debug + Clone,
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index e63b032..f5dbbbf 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -2,6 +2,7 @@
 use std::collections::HashSet;
 use std::fmt;
 
+use crate::expr::*;
 use crate::normalize::normalize;
 use dhall_core;
 use dhall_core::context::Context;
@@ -10,6 +11,17 @@ use dhall_generator as dhall;
 
 use self::TypeMessage::*;
 
+impl Resolved {
+    pub fn typecheck(self) -> Result<Typed, TypeError<X>> {
+        // let typ = Type(Box::new(Normalized(crate::typecheck::type_of(
+        //     self.0.clone(),
+        // )?)));
+        // Ok(Typed(self.0, typ))
+        let typ = crate::typecheck::type_of(self.0.clone())?;
+        Ok(Typed(self.0, typ))
+    }
+}
+
 fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
     use dhall_core::Const::*;
     use dhall_core::ExprF::*;
@@ -199,13 +211,10 @@ where
 ///
 /// `type_with` normalizes the type since while type-checking. It expects the
 /// context to contain only normalized expressions.
-pub fn type_with<S>(
-    ctx: &Context<Label, SubExpr<S, X>>,
-    e: SubExpr<S, X>,
-) -> Result<SubExpr<S, X>, TypeError<S>>
-where
-    S: ::std::fmt::Debug + Clone,
-{
+pub fn type_with(
+    ctx: &Context<Label, SubExpr<X, X>>,
+    e: SubExpr<X, X>,
+) -> Result<Typed, TypeError<X>> {
     use dhall_core::BinOp::*;
     use dhall_core::Builtin::*;
     use dhall_core::Const::*;
@@ -228,19 +237,19 @@ where
             let ctx2 = ctx
                 .insert(x.clone(), t2.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
-            let tB = type_with(&ctx2, b.clone())?;
-            let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?;
+            let tB = type_with(&ctx2, b.clone())?.1;
+            let _ = type_with(ctx, rc(Pi(x.clone(), t.clone(), tB.clone())))?.1;
             Ok(Pi(x.clone(), t2, tB))
         }
         Pi(x, tA, tB) => {
-            let ttA = type_with(ctx, tA.clone())?;
+            let ttA = type_with(ctx, tA.clone())?.1;
             let tA = normalize(SubExpr::clone(tA));
             let kA = ensure_const(&ttA, InvalidInputType(tA.clone()))?;
 
             let ctx2 = ctx
                 .insert(x.clone(), tA.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
-            let tB = type_with(&ctx2, tB.clone())?;
+            let tB = type_with(&ctx2, tB.clone())?.1;
             let kB = match tB.as_ref() {
                 Const(k) => *k,
                 _ => {
@@ -264,15 +273,15 @@ where
                 SubExpr::clone(r)
             };
 
-            let tR = type_with(ctx, r)?;
-            let ttR = type_with(ctx, tR.clone())?;
+            let tR = type_with(ctx, r)?.1;
+            let ttR = type_with(ctx, tR.clone())?.1;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
             let kR = ensure_const(&ttR, InvalidInputType(tR.clone()))?;
 
             let ctx2 = ctx.insert(f.clone(), tR.clone());
-            let tB = type_with(&ctx2, b.clone())?;
-            let ttB = type_with(ctx, tB.clone())?;
+            let tB = type_with(&ctx2, b.clone())?.1;
+            let ttB = type_with(ctx, tB.clone())?.1;
             // Don't bother to provide a `let`-specific version of this error
             // message because this should never happen anyway
             let kB = ensure_const(&ttB, InvalidOutputType(tB.clone()))?;
@@ -285,7 +294,7 @@ where
         }
         _ => match e
             .as_ref()
-            .traverse_ref_simple(|e| Ok((e, type_with(ctx, e.clone())?)))?
+            .traverse_ref_simple(|e| type_with(ctx, e.clone()))?
         {
             Lam(_, _, _) => unreachable!(),
             Pi(_, _, _) => unreachable!(),
@@ -295,10 +304,10 @@ where
                 Some(e) => Ok(e.unroll()),
                 None => Err(mkerr(UnboundVariable)),
             },
-            App((f, mut tf), args) => {
+            App(Typed(f, mut tf), args) => {
                 let mut iter = args.into_iter();
                 let mut seen_args: Vec<SubExpr<_, _>> = vec![];
-                while let Some((a, ta)) = iter.next() {
+                while let Some(Typed(a, ta)) = iter.next() {
                     seen_args.push(a.clone());
                     let (x, tx, tb) = match tf.as_ref() {
                         Pi(x, tx, tb) => (x, tx, tb),
@@ -321,18 +330,18 @@ where
                 }
                 Ok(tf.unroll())
             }
-            Annot((x, tx), (t, _)) => {
+            Annot(Typed(x, tx), Typed(t, _)) => {
                 let t = normalize(t.clone());
                 ensure_equal(t.as_ref(), tx.as_ref(), mkerr, || {
                     AnnotMismatch(x.clone(), t.clone(), tx.clone())
                 })?;
                 Ok(t.unroll())
             }
-            BoolIf((x, tx), (y, ty), (z, tz)) => {
+            BoolIf(Typed(x, tx), Typed(y, ty), Typed(z, tz)) => {
                 ensure_equal(tx.as_ref(), &Builtin(Bool), mkerr, || {
                     InvalidPredicate(x.clone(), tx.clone())
                 })?;
-                let tty = type_with(ctx, ty.clone())?;
+                let tty = type_with(ctx, ty.clone())?.1;
                 ensure_is_type(
                     tty.clone(),
                     IfBranchMustBeTerm(
@@ -343,7 +352,7 @@ where
                     ),
                 )?;
 
-                let ttz = type_with(ctx, tz.clone())?;
+                let ttz = type_with(ctx, tz.clone())?.1;
                 ensure_is_type(
                     ttz.clone(),
                     IfBranchMustBeTerm(
@@ -364,35 +373,35 @@ where
                 })?;
                 Ok(ty.unroll())
             }
-            EmptyListLit((t, tt)) => {
-                ensure_is_type(tt, InvalidListType(t.clone()))?;
-                let t = normalize(SubExpr::clone(t));
+            EmptyListLit(Typed(t, tt)) => {
+                ensure_is_type(tt.clone(), InvalidListType(t.clone()))?;
+                let t = Typed(t, tt).normalize().0;
                 Ok(dhall::expr!(List t))
             }
             NEListLit(xs) => {
                 let mut iter = xs.into_iter().enumerate();
-                let (_, (_, t)) = iter.next().unwrap();
-                let s = type_with(ctx, t.clone())?;
+                let (_, Typed(_, t)) = iter.next().unwrap();
+                let s = type_with(ctx, t.clone())?.1;
                 ensure_is_type(s, InvalidListType(t.clone()))?;
-                for (i, (y, ty)) in iter {
+                for (i, Typed(y, ty)) in iter {
                     ensure_equal(t.as_ref(), ty.as_ref(), mkerr, || {
                         InvalidListElement(i, t.clone(), y.clone(), ty.clone())
                     })?;
                 }
                 Ok(dhall::expr!(List t))
             }
-            EmptyOptionalLit((t, tt)) => {
+            EmptyOptionalLit(Typed(t, tt)) => {
                 ensure_is_type(tt, InvalidOptionalType(t.clone()))?;
                 let t = normalize(t.clone());
                 Ok(dhall::expr!(Optional t))
             }
-            NEOptionalLit((_, t)) => {
-                let s = type_with(ctx, t.clone())?;
+            NEOptionalLit(Typed(_, t)) => {
+                let s = type_with(ctx, t.clone())?.1;
                 ensure_is_type(s, InvalidOptionalType(t.clone()))?;
                 Ok(dhall::expr!(Optional t))
             }
             RecordType(kts) => {
-                for (k, (t, tt)) in kts {
+                for (k, Typed(t, tt)) in kts {
                     ensure_is_type(tt, InvalidFieldType(k.clone(), t.clone()))?;
                 }
                 Ok(Const(Type))
@@ -400,15 +409,15 @@ where
             RecordLit(kvs) => {
                 let kts = kvs
                     .into_iter()
-                    .map(|(k, (v, t))| {
-                        let s = type_with(ctx, t.clone())?;
+                    .map(|(k, Typed(v, t))| {
+                        let s = type_with(ctx, t.clone())?.1;
                         ensure_is_type(s, InvalidField(k.clone(), v.clone()))?;
                         Ok((k.clone(), t))
                     })
                     .collect::<Result<_, _>>()?;
                 Ok(RecordType(kts))
             }
-            Field((r, tr), x) => match tr.as_ref() {
+            Field(Typed(r, tr), x) => match tr.as_ref() {
                 RecordType(kts) => match kts.get(&x) {
                     Some(e) => Ok(e.unroll()),
                     None => Err(mkerr(MissingField(x.clone(), tr.clone()))),
@@ -422,7 +431,7 @@ where
             DoubleLit(_) => Ok(Builtin(Double)),
             // TODO: check type of interpolations
             TextLit(_) => Ok(Builtin(Text)),
-            BinOp(o, (l, tl), (r, tr)) => {
+            BinOp(o, Typed(l, tl), Typed(r, tr)) => {
                 let t = Builtin(match o {
                     BoolAnd => Bool,
                     BoolOr => Bool,
@@ -448,17 +457,15 @@ where
             _ => panic!("Unimplemented typecheck case: {:?}", e),
         },
     }?;
-    Ok(rc(ret))
+    Ok(Typed(e, rc(ret)))
 }
 
 /// `typeOf` is the same as `type_with` with an empty context, meaning that the
 /// expression must be closed (i.e. no free variables), otherwise type-checking
 /// will fail.
-pub fn type_of<S: ::std::fmt::Debug + Clone>(
-    e: SubExpr<S, X>,
-) -> Result<SubExpr<S, X>, TypeError<S>> {
+pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
     let ctx = Context::new();
-    type_with(&ctx, e) //.map(|e| e.into_owned())
+    type_with(&ctx, e).map(|e| e.1)
 }
 
 /// The specific type error