From 7983c43210f5fcaa439fa1c6742e72252652e4f4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 6 Apr 2019 20:50:57 +0200
Subject: Thread Typed through type_with

---
 dhall/src/normalize.rs | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'dhall/src/normalize.rs')

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,
-- 
cgit v1.3.1


From c4438eb3d52b1a69c9022b12e8de135b8c9991c9 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 6 Apr 2019 21:54:55 +0200
Subject: Start taking Typed seriously

---
 dhall/src/expr.rs      |   2 +-
 dhall/src/normalize.rs |   5 +-
 dhall/src/typecheck.rs | 239 +++++++++++++++++++++++++++----------------------
 3 files changed, 135 insertions(+), 111 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index cc7f064..831fbc5 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -15,7 +15,7 @@ pub struct Typed(pub(crate) SubExpr<X, X>, pub(crate) Type);
 pub type Type = SubExpr<X, X>;
 
 #[derive(Debug, Clone)]
-pub struct Normalized(pub(crate) SubExpr<X, X>);
+pub struct Normalized(pub(crate) SubExpr<X, X>, pub(crate) Type);
 
 impl PartialEq for Parsed {
     fn eq(&self, other: &Self) -> bool {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 8ed2136..f9633fb 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -6,10 +6,7 @@ use std::fmt;
 
 impl Typed {
     pub fn normalize(self) -> Normalized {
-        Normalized(normalize(self.0))
-    }
-    pub fn get_type(&self) -> &Type {
-        &self.1
+        Normalized(normalize(self.0), self.1)
     }
 }
 
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index f5dbbbf..d62fe5a 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -3,7 +3,6 @@ use std::collections::HashSet;
 use std::fmt;
 
 use crate::expr::*;
-use crate::normalize::normalize;
 use dhall_core;
 use dhall_core::context::Context;
 use dhall_core::*;
@@ -21,6 +20,16 @@ impl Resolved {
         Ok(Typed(self.0, typ))
     }
 }
+impl Typed {
+    pub fn get_type(&self) -> &Type {
+        &self.1
+    }
+}
+impl Normalized {
+    pub fn get_type(&self) -> &Type {
+        &self.1
+    }
+}
 
 fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
     use dhall_core::Const::*;
@@ -231,23 +240,29 @@ pub fn type_with(
             _ => Err(mkerr(msg)),
         };
 
+    enum Ret {
+        ErrRet(TypeError<X>),
+        OkNormalized(Normalized),
+        OkRet(Expr<X, X>),
+    }
+    use Ret::*;
     let ret = match e.as_ref() {
         Lam(x, t, b) => {
-            let t2 = normalize(SubExpr::clone(t));
+            let t2 = type_with(ctx, t.clone())?.normalize();
             let ctx2 = ctx
-                .insert(x.clone(), t2.clone())
+                .insert(x.clone(), t2.0.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             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))
+            OkRet(Pi(x.clone(), t2.0, tB))
         }
         Pi(x, tA, tB) => {
-            let ttA = type_with(ctx, tA.clone())?.1;
-            let tA = normalize(SubExpr::clone(tA));
-            let kA = ensure_const(&ttA, InvalidInputType(tA.clone()))?;
+            let tA = type_with(ctx, tA.clone())?.normalize();
+            let kA =
+                ensure_const(tA.get_type(), InvalidInputType(tA.0.clone()))?;
 
             let ctx2 = ctx
-                .insert(x.clone(), tA.clone())
+                .insert(x.clone(), tA.0.clone())
                 .map(|e| shift(1, &V(x.clone(), 0), e));
             let tB = type_with(&ctx2, tB.clone())?.1;
             let kB = match tB.as_ref() {
@@ -262,8 +277,8 @@ pub fn type_with(
             };
 
             match rule(kA, kB) {
-                Err(()) => Err(mkerr(NoDependentTypes(tA.clone(), tB))),
-                Ok(_) => Ok(Const(kB)),
+                Err(()) => ErrRet(mkerr(NoDependentTypes(tA.0.clone(), tB))),
+                Ok(_) => OkRet(Const(kB)),
             }
         }
         Let(f, mt, r, b) => {
@@ -273,24 +288,33 @@ pub fn type_with(
                 SubExpr::clone(r)
             };
 
-            let tR = type_with(ctx, r)?.1;
-            let ttR = type_with(ctx, tR.clone())?.1;
+            let r = type_with(ctx, r)?;
+            let tr = type_with(ctx, r.get_type().clone())?;
             // 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 kR = ensure_const(
+                tr.get_type(),
+                InvalidInputType(r.get_type().clone()),
+            )?;
 
-            let ctx2 = ctx.insert(f.clone(), tR.clone());
-            let tB = type_with(&ctx2, b.clone())?.1;
-            let ttB = type_with(ctx, tB.clone())?.1;
+            let ctx2 = ctx.insert(f.clone(), r.get_type().clone());
+            let b = type_with(&ctx2, b.clone())?;
+            let tb = type_with(ctx, b.get_type().clone())?;
             // 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()))?;
+            let kB = ensure_const(
+                tb.get_type(),
+                InvalidOutputType(b.get_type().clone()),
+            )?;
 
             if let Err(()) = rule(kR, kB) {
-                return Err(mkerr(NoDependentLet(tR, tB)));
+                return Err(mkerr(NoDependentLet(
+                    r.get_type().clone(),
+                    b.get_type().clone(),
+                )));
             }
 
-            Ok(tB.unroll())
+            OkRet(b.get_type().unroll())
         }
         _ => match e
             .as_ref()
@@ -299,84 +323,85 @@ pub fn type_with(
             Lam(_, _, _) => unreachable!(),
             Pi(_, _, _) => unreachable!(),
             Let(_, _, _, _) => unreachable!(),
-            Const(c) => axiom(c).map(Const),
+            Const(c) => OkRet(Const(axiom(c)?)),
             Var(V(x, n)) => match ctx.lookup(&x, n) {
-                Some(e) => Ok(e.unroll()),
-                None => Err(mkerr(UnboundVariable)),
+                Some(e) => OkRet(e.unroll()),
+                None => ErrRet(mkerr(UnboundVariable)),
             },
-            App(Typed(f, mut tf), args) => {
+            App(f, args) => {
                 let mut iter = args.into_iter();
                 let mut seen_args: Vec<SubExpr<_, _>> = vec![];
+                let mut tf = type_with(ctx, f.get_type().clone())?.normalize();
                 while let Some(Typed(a, ta)) = iter.next() {
                     seen_args.push(a.clone());
-                    let (x, tx, tb) = match tf.as_ref() {
+                    let (x, tx, tb) = match tf.0.as_ref() {
                         Pi(x, tx, tb) => (x, tx, tb),
                         _ => {
                             return Err(mkerr(NotAFunction(
-                                rc(App(f.clone(), seen_args)),
+                                rc(App(f.0.clone(), seen_args)),
                                 tf,
                             )));
                         }
                     };
                     ensure_equal(tx.as_ref(), ta.as_ref(), mkerr, || {
                         TypeMismatch(
-                            rc(App(f.clone(), seen_args.clone())),
+                            rc(App(f.0.clone(), seen_args.clone())),
                             tx.clone(),
                             a.clone(),
                             ta.clone(),
                         )
                     })?;
-                    tf = normalize(subst_shift(&V(x.clone(), 0), &a, &tb));
+                    tf =
+                        type_with(ctx, subst_shift(&V(x.clone(), 0), &a, &tb))?
+                            .normalize();
                 }
-                Ok(tf.unroll())
+                OkNormalized(tf)
             }
-            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())
+            Annot(x, t) => {
+                let t = t.normalize();
+                ensure_equal(
+                    t.0.as_ref(),
+                    x.get_type().as_ref(),
+                    mkerr,
+                    || AnnotMismatch(x.clone(), t.clone()),
+                )?;
+                OkNormalized(t)
             }
-            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())?.1;
+            BoolIf(x, y, z) => {
+                ensure_equal(
+                    x.get_type().as_ref(),
+                    &Builtin(Bool),
+                    mkerr,
+                    || InvalidPredicate(x.clone()),
+                )?;
+                let ty = type_with(ctx, y.get_type().clone())?.normalize();
                 ensure_is_type(
-                    tty.clone(),
-                    IfBranchMustBeTerm(
-                        true,
-                        y.clone(),
-                        ty.clone(),
-                        tty.clone(),
-                    ),
+                    ty.get_type().clone(),
+                    IfBranchMustBeTerm(true, y.clone()),
                 )?;
 
-                let ttz = type_with(ctx, tz.clone())?.1;
+                let tz = type_with(ctx, z.get_type().clone())?.normalize();
                 ensure_is_type(
-                    ttz.clone(),
-                    IfBranchMustBeTerm(
-                        false,
-                        z.clone(),
-                        tz.clone(),
-                        ttz.clone(),
-                    ),
+                    tz.get_type().clone(),
+                    IfBranchMustBeTerm(false, z.clone()),
                 )?;
 
-                ensure_equal(ty.as_ref(), tz.as_ref(), mkerr, || {
-                    IfBranchMismatch(
-                        y.clone(),
-                        z.clone(),
-                        ty.clone(),
-                        tz.clone(),
-                    )
-                })?;
-                Ok(ty.unroll())
+                ensure_equal(
+                    y.get_type().as_ref(),
+                    z.get_type().as_ref(),
+                    mkerr,
+                    || IfBranchMismatch(y.clone(), z.clone()),
+                )?;
+
+                OkNormalized(ty)
             }
-            EmptyListLit(Typed(t, tt)) => {
-                ensure_is_type(tt.clone(), InvalidListType(t.clone()))?;
-                let t = Typed(t, tt).normalize().0;
-                Ok(dhall::expr!(List t))
+            EmptyListLit(t) => {
+                ensure_is_type(
+                    t.get_type().clone(),
+                    InvalidListType(t.0.clone()),
+                )?;
+                let t = t.normalize().0;
+                OkRet(dhall::expr!(List t))
             }
             NEListLit(xs) => {
                 let mut iter = xs.into_iter().enumerate();
@@ -388,23 +413,26 @@ pub fn type_with(
                         InvalidListElement(i, t.clone(), y.clone(), ty.clone())
                     })?;
                 }
-                Ok(dhall::expr!(List t))
+                OkRet(dhall::expr!(List t))
             }
-            EmptyOptionalLit(Typed(t, tt)) => {
-                ensure_is_type(tt, InvalidOptionalType(t.clone()))?;
-                let t = normalize(t.clone());
-                Ok(dhall::expr!(Optional t))
+            EmptyOptionalLit(t) => {
+                ensure_is_type(
+                    t.get_type().clone(),
+                    InvalidOptionalType(t.0.clone()),
+                )?;
+                let t = t.normalize().0;
+                OkRet(dhall::expr!(Optional t))
             }
             NEOptionalLit(Typed(_, t)) => {
                 let s = type_with(ctx, t.clone())?.1;
                 ensure_is_type(s, InvalidOptionalType(t.clone()))?;
-                Ok(dhall::expr!(Optional t))
+                OkRet(dhall::expr!(Optional t))
             }
             RecordType(kts) => {
                 for (k, Typed(t, tt)) in kts {
                     ensure_is_type(tt, InvalidFieldType(k.clone(), t.clone()))?;
                 }
-                Ok(Const(Type))
+                OkRet(Const(Type))
             }
             RecordLit(kvs) => {
                 let kts = kvs
@@ -415,23 +443,23 @@ pub fn type_with(
                         Ok((k.clone(), t))
                     })
                     .collect::<Result<_, _>>()?;
-                Ok(RecordType(kts))
+                OkRet(RecordType(kts))
             }
-            Field(Typed(r, tr), x) => match tr.as_ref() {
+            Field(r, x) => match r.get_type().as_ref() {
                 RecordType(kts) => match kts.get(&x) {
-                    Some(e) => Ok(e.unroll()),
-                    None => Err(mkerr(MissingField(x.clone(), tr.clone()))),
+                    Some(e) => OkRet(e.unroll()),
+                    None => ErrRet(mkerr(MissingField(x.clone(), r.clone()))),
                 },
-                _ => Err(mkerr(NotARecord(x.clone(), r.clone(), tr.clone()))),
+                _ => ErrRet(mkerr(NotARecord(x.clone(), r.clone()))),
             },
-            Builtin(b) => Ok(type_of_builtin(b)),
-            BoolLit(_) => Ok(Builtin(Bool)),
-            NaturalLit(_) => Ok(Builtin(Natural)),
-            IntegerLit(_) => Ok(Builtin(Integer)),
-            DoubleLit(_) => Ok(Builtin(Double)),
+            Builtin(b) => OkRet(type_of_builtin(b)),
+            BoolLit(_) => OkRet(Builtin(Bool)),
+            NaturalLit(_) => OkRet(Builtin(Natural)),
+            IntegerLit(_) => OkRet(Builtin(Integer)),
+            DoubleLit(_) => OkRet(Builtin(Double)),
             // TODO: check type of interpolations
-            TextLit(_) => Ok(Builtin(Text)),
-            BinOp(o, Typed(l, tl), Typed(r, tr)) => {
+            TextLit(_) => OkRet(Builtin(Text)),
+            BinOp(o, l, r) => {
                 let t = Builtin(match o {
                     BoolAnd => Bool,
                     BoolOr => Bool,
@@ -443,21 +471,25 @@ pub fn type_with(
                     _ => panic!("Unimplemented typecheck case: {:?}", e),
                 });
 
-                ensure_equal(tl.as_ref(), &t, mkerr, || {
-                    BinOpTypeMismatch(o, l.clone(), tl.clone())
+                ensure_equal(l.get_type().as_ref(), &t, mkerr, || {
+                    BinOpTypeMismatch(o, l.clone())
                 })?;
 
-                ensure_equal(tr.as_ref(), &t, mkerr, || {
-                    BinOpTypeMismatch(o, r.clone(), tr.clone())
+                ensure_equal(r.get_type().as_ref(), &t, mkerr, || {
+                    BinOpTypeMismatch(o, r.clone())
                 })?;
 
-                Ok(t)
+                OkRet(t)
             }
             Embed(p) => match p {},
             _ => panic!("Unimplemented typecheck case: {:?}", e),
         },
-    }?;
-    Ok(Typed(e, rc(ret)))
+    };
+    match ret {
+        OkRet(ret) => Ok(Typed(e, rc(ret))),
+        OkNormalized(ret) => Ok(Typed(e, ret.0)),
+        ErrRet(e) => Err(e),
+    }
 }
 
 /// `typeOf` is the same as `type_with` with an empty context, meaning that the
@@ -474,23 +506,18 @@ pub enum TypeMessage<S> {
     UnboundVariable,
     InvalidInputType(SubExpr<S, X>),
     InvalidOutputType(SubExpr<S, X>),
-    NotAFunction(SubExpr<S, X>, SubExpr<S, X>),
+    NotAFunction(SubExpr<S, X>, Normalized),
     TypeMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
-    AnnotMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+    AnnotMismatch(Typed, Normalized),
     Untyped,
     InvalidListElement(usize, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
     InvalidListType(SubExpr<S, X>),
     InvalidOptionalElement(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
     InvalidOptionalLiteral(usize),
     InvalidOptionalType(SubExpr<S, X>),
-    InvalidPredicate(SubExpr<S, X>, SubExpr<S, X>),
-    IfBranchMismatch(
-        SubExpr<S, X>,
-        SubExpr<S, X>,
-        SubExpr<S, X>,
-        SubExpr<S, X>,
-    ),
-    IfBranchMustBeTerm(bool, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+    InvalidPredicate(Typed),
+    IfBranchMismatch(Typed, Typed),
+    IfBranchMustBeTerm(bool, Typed),
     InvalidField(Label, SubExpr<S, X>),
     InvalidFieldType(Label, SubExpr<S, X>),
     InvalidAlternative(Label, SubExpr<S, X>),
@@ -505,9 +532,9 @@ pub enum TypeMessage<S> {
     HandlerInputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
     HandlerOutputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
     HandlerNotAFunction(Label, SubExpr<S, X>),
-    NotARecord(Label, SubExpr<S, X>, SubExpr<S, X>),
-    MissingField(Label, SubExpr<S, X>),
-    BinOpTypeMismatch(BinOp, SubExpr<S, X>, SubExpr<S, X>),
+    NotARecord(Label, Typed),
+    MissingField(Label, Typed),
+    BinOpTypeMismatch(BinOp, Typed),
     NoDependentLet(SubExpr<S, X>, SubExpr<S, X>),
     NoDependentTypes(SubExpr<S, X>, SubExpr<S, X>),
 }
-- 
cgit v1.3.1


From 4bebcd96b6e76b9b8ae7877af91d2ae571e617a9 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 7 Apr 2019 16:45:30 +0200
Subject: Restrict public API

Closes #20
---
 dhall/src/expr.rs         | 48 ++++++++++++++++++++++--------------
 dhall/src/imports.rs      | 15 +----------
 dhall/src/lib.rs          | 12 ++++-----
 dhall/src/main.rs         | 20 +++++++--------
 dhall/src/normalize.rs    |  8 ++++--
 dhall/src/typecheck.rs    |  9 ++++---
 dhall/tests/common/mod.rs | 63 +++++++++++++++++++++++++++++++++++------------
 7 files changed, 104 insertions(+), 71 deletions(-)

(limited to 'dhall/src/normalize.rs')

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 555db2f..7baf628 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -1,34 +1,46 @@
 use crate::imports::ImportRoot;
 use dhall_core::*;
 
+macro_rules! derive_other_traits {
+    ($ty:ident) => {
+        impl std::cmp::PartialEq for $ty {
+            fn eq(&self, other: &Self) -> bool {
+                self.0 == other.0
+            }
+        }
+
+        impl std::fmt::Display for $ty {
+            fn fmt(
+                &self,
+                f: &mut std::fmt::Formatter,
+            ) -> Result<(), std::fmt::Error> {
+                self.0.fmt(f)
+            }
+        }
+    };
+}
+
 #[derive(Debug, Clone, Eq)]
 pub struct Parsed(pub(crate) SubExpr<X, Import>, pub(crate) ImportRoot);
+derive_other_traits!(Parsed);
 
-#[derive(Debug, Clone, PartialEq, Eq)]
+#[derive(Debug, Clone, Eq)]
 pub struct Resolved(pub(crate) SubExpr<X, X>);
+derive_other_traits!(Resolved);
 
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, Eq)]
 pub struct Typed(pub(crate) SubExpr<X, X>, pub(crate) Type);
+derive_other_traits!(Typed);
+
+#[derive(Debug, Clone, Eq)]
+pub struct Normalized(pub(crate) SubExpr<X, X>, pub(crate) Type);
+derive_other_traits!(Normalized);
 
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq)]
 pub struct Type(pub(crate) TypeInternal);
 
-#[derive(Debug, Clone)]
+#[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) enum TypeInternal {
     Expr(Box<Normalized>),
     Untyped,
 }
-
-#[derive(Debug, Clone)]
-pub struct Normalized(pub(crate) SubExpr<X, X>, pub(crate) Type);
-
-impl PartialEq for Parsed {
-    fn eq(&self, other: &Self) -> bool {
-        self.0 == other.0
-    }
-}
-impl std::fmt::Display for Parsed {
-    fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
-        self.0.fmt(f)
-    }
-}
diff --git a/dhall/src/imports.rs b/dhall/src/imports.rs
index 5d94b6a..fdde8c3 100644
--- a/dhall/src/imports.rs
+++ b/dhall/src/imports.rs
@@ -44,12 +44,6 @@ impl fmt::Display for ImportError {
     }
 }
 
-// Deprecated
-pub fn panic_imports<S: Clone>(expr: &Expr<S, Import>) -> Expr<S, X> {
-    let no_import = |i: &Import| -> X { panic!("ahhh import: {:?}", i) };
-    expr.map_embed(&no_import)
-}
-
 /// A root from which to resolve relative imports.
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub enum ImportRoot {
@@ -121,7 +115,7 @@ impl Parsed {
     pub fn resolve(self) -> Result<Resolved, ImportError> {
         crate::imports::resolve_expr(self, true)
     }
-    pub fn resolve_no_imports(self) -> Result<Resolved, ImportError> {
+    pub fn skip_resolve(self) -> Result<Resolved, ImportError> {
         crate::imports::resolve_expr(self, false)
     }
 }
@@ -135,10 +129,3 @@ pub fn load_dhall_file(
     let expr = resolve_expr(expr, resolve_imports)?;
     Ok(expr.0.unroll())
 }
-
-// Deprecated
-pub fn load_dhall_file_no_resolve_imports(
-    f: &Path,
-) -> Result<ParsedExpr, ImportError> {
-    Ok(Parsed::load_from_file(f)?.0)
-}
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 28b43ba..f00e5b6 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -7,16 +7,14 @@
     clippy::many_single_char_names
 )]
 
-mod normalize;
-pub use crate::normalize::*;
 mod binary;
-pub mod imports;
-mod traits;
+mod imports;
+mod normalize;
+pub mod traits;
 pub mod typecheck;
-pub use crate::imports::*;
-pub use crate::traits::*;
+pub use crate::imports::{load_dhall_file, ImportError};
+pub use crate::traits::StaticType;
 pub use dhall_generator::expr;
 pub use dhall_generator::subexpr;
 pub use dhall_generator::StaticType;
 pub mod expr;
-pub use crate::expr::*;
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 77f558c..2881d5a 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -2,9 +2,6 @@ use std::error::Error;
 use std::io::{self, Read};
 use term_painter::ToStyle;
 
-use dhall::*;
-use dhall_core::*;
-
 const ERROR_STYLE: term_painter::Color = term_painter::Color::Red;
 const BOLD: term_painter::Attr = term_painter::Attr::Bold;
 
@@ -57,17 +54,19 @@ fn print_error(message: &str, source: &str, start: usize, end: usize) {
 fn main() {
     let mut buffer = String::new();
     io::stdin().read_to_string(&mut buffer).unwrap();
-    let expr = match parse_expr(&buffer) {
-        Ok(e) => e,
+
+    let expr = match dhall::expr::Parsed::load_from_str(&buffer) {
+        Ok(expr) => expr,
         Err(e) => {
             print_error(&format!("Parse error {}", e), &buffer, 0, 0);
             return;
         }
     };
 
-    let expr: SubExpr<_, _> = rc(imports::panic_imports(expr.as_ref()));
+    let expr = expr.resolve().unwrap();
 
-    let type_expr = match typecheck::type_of(expr.clone()) {
+    let expr = match expr.typecheck() {
+        Ok(expr) => expr,
         Err(e) => {
             let explain = ::std::env::args().any(|s| s == "--explain");
             if !explain {
@@ -84,10 +83,9 @@ fn main() {
             // FIXME Print source position
             return;
         }
-        Ok(type_expr) => type_expr,
     };
 
-    println!("{}", type_expr);
-    println!();
-    println!("{}", normalize(expr));
+    let expr = expr.normalize();
+
+    println!("{}", expr);
 }
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index f9633fb..c07d3cb 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -8,6 +8,10 @@ impl Typed {
     pub fn normalize(self) -> Normalized {
         Normalized(normalize(self.0), self.1)
     }
+    /// Pretends this expression is normalized. Use with care.
+    pub fn skip_normalize(self) -> Normalized {
+        Normalized(self.0, self.1)
+    }
 }
 
 fn apply_builtin<S, A>(b: Builtin, args: &Vec<Expr<S, A>>) -> WhatNext<S, A>
@@ -209,7 +213,7 @@ enum WhatNext<'a, S, A> {
     DoneAsIs,
 }
 
-pub fn normalize_ref<S, A>(expr: &Expr<S, A>) -> Expr<S, A>
+fn normalize_ref<S, A>(expr: &Expr<S, A>) -> Expr<S, A>
 where
     S: fmt::Debug + Clone,
     A: fmt::Debug + Clone,
@@ -313,7 +317,7 @@ where
 /// However, `normalize` will not fail if the expression is ill-typed and will
 /// leave ill-typed sub-expressions unevaluated.
 ///
-pub fn normalize<S, A>(e: SubExpr<S, A>) -> SubExpr<S, A>
+fn normalize<S, A>(e: SubExpr<S, A>) -> SubExpr<S, A>
 where
     S: fmt::Debug + Clone,
     A: fmt::Debug + Clone,
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index a0782f8..babfad0 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -11,8 +11,11 @@ use self::TypeMessage::*;
 
 impl Resolved {
     pub fn typecheck(self) -> Result<Typed, TypeError<X>> {
-        let typ = crate::typecheck::type_of_(self.0.clone())?;
-        Ok(typ)
+        type_of_(self.0.clone())
+    }
+    /// Pretends this expression has been typechecked. Use with care.
+    pub fn skip_typecheck(self) -> Typed {
+        Typed(self.0, UNTYPE)
     }
 }
 impl Typed {
@@ -63,7 +66,7 @@ impl Normalized {
 }
 impl Type {
     #[inline(always)]
-    fn as_normalized(&self) -> Result<&Normalized, TypeError<X>> {
+    pub fn as_normalized(&self) -> Result<&Normalized, TypeError<X>> {
         use TypeInternal::*;
         match &self.0 {
             Expr(e) => Ok(e),
diff --git a/dhall/tests/common/mod.rs b/dhall/tests/common/mod.rs
index fc5aa5b..5f16d2c 100644
--- a/dhall/tests/common/mod.rs
+++ b/dhall/tests/common/mod.rs
@@ -44,20 +44,21 @@ pub enum Feature {
     TypeInferenceFailure,
 }
 
+// Deprecated
 fn read_dhall_file<'i>(file_path: &str) -> Result<Expr<X, X>, ImportError> {
-    load_dhall_file(&PathBuf::from(file_path), true)
+    dhall::load_dhall_file(&PathBuf::from(file_path), true)
 }
 
 fn load_from_file_str<'i>(
     file_path: &str,
-) -> Result<dhall::Parsed, ImportError> {
-    Parsed::load_from_file(&PathBuf::from(file_path))
+) -> Result<dhall::expr::Parsed, ImportError> {
+    dhall::expr::Parsed::load_from_file(&PathBuf::from(file_path))
 }
 
 fn load_from_binary_file_str<'i>(
     file_path: &str,
-) -> Result<dhall::Parsed, ImportError> {
-    Parsed::load_from_binary_file(&PathBuf::from(file_path))
+) -> Result<dhall::expr::Parsed, ImportError> {
+    dhall::expr::Parsed::load_from_binary_file(&PathBuf::from(file_path))
 }
 
 pub fn run_test(base_path: &str, feature: Feature) {
@@ -88,7 +89,8 @@ pub fn run_test(base_path: &str, feature: Feature) {
             assert_eq_pretty!(expr, expected);
 
             // Round-trip pretty-printer
-            let expr = Parsed::load_from_str(&expr.to_string()).unwrap();
+            let expr =
+                dhall::expr::Parsed::load_from_str(&expr.to_string()).unwrap();
             assert_eq!(expr, expected);
         }
         ParserFailure => {
@@ -102,15 +104,29 @@ pub fn run_test(base_path: &str, feature: Feature) {
         Normalization => {
             let expr_file_path = base_path.clone() + "A.dhall";
             let expected_file_path = base_path + "B.dhall";
-            let expr = rc(read_dhall_file(&expr_file_path).unwrap());
-            let expected = rc(read_dhall_file(&expected_file_path).unwrap());
+            let expr = load_from_file_str(&expr_file_path)
+                .unwrap()
+                .resolve()
+                .unwrap()
+                .skip_typecheck()
+                .normalize();
+            let expected = load_from_file_str(&expected_file_path)
+                .unwrap()
+                .resolve()
+                .unwrap()
+                .skip_typecheck()
+                .normalize();
 
-            assert_eq_display!(normalize(expr), normalize(expected));
+            assert_eq_display!(expr, expected);
         }
         TypecheckFailure => {
             let file_path = base_path + ".dhall";
-            let expr = rc(read_dhall_file(&file_path).unwrap());
-            typecheck::type_of(expr).unwrap_err();
+            load_from_file_str(&file_path)
+                .unwrap()
+                .skip_resolve()
+                .unwrap()
+                .typecheck()
+                .unwrap_err();
         }
         TypecheckSuccess => {
             // Many tests stack overflow in debug mode
@@ -131,15 +147,30 @@ pub fn run_test(base_path: &str, feature: Feature) {
         }
         TypeInferenceFailure => {
             let file_path = base_path + ".dhall";
-            let expr = rc(read_dhall_file(&file_path).unwrap());
-            typecheck::type_of(expr).unwrap_err();
+            load_from_file_str(&file_path)
+                .unwrap()
+                .skip_resolve()
+                .unwrap()
+                .typecheck()
+                .unwrap_err();
         }
         TypeInferenceSuccess => {
             let expr_file_path = base_path.clone() + "A.dhall";
             let expected_file_path = base_path + "B.dhall";
-            let expr = rc(read_dhall_file(&expr_file_path).unwrap());
-            let expected = rc(read_dhall_file(&expected_file_path).unwrap());
-            assert_eq_display!(typecheck::type_of(expr).unwrap(), expected);
+            let expr = load_from_file_str(&expr_file_path)
+                .unwrap()
+                .skip_resolve()
+                .unwrap()
+                .typecheck()
+                .unwrap();
+            let ty = expr.get_type().as_normalized().unwrap();
+            let expected = load_from_file_str(&expected_file_path)
+                .unwrap()
+                .skip_resolve()
+                .unwrap()
+                .skip_typecheck()
+                .skip_normalize();
+            assert_eq_display!(ty, &expected);
         }
     }
 }
-- 
cgit v1.3.1