From 5c342a5688fe7a4bb337ce0622968226d524022e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 15:32:27 +0000
Subject: Resolve by ref instead of by mut

---
 dhall/src/syntax/ast/expr.rs    |  53 +------------
 dhall/src/syntax/ast/visitor.rs | 166 ----------------------------------------
 2 files changed, 4 insertions(+), 215 deletions(-)

(limited to 'dhall/src/syntax')

diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index b493fdb..420df5b 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,5 +1,5 @@
 use crate::syntax::map::{DupTreeMap, DupTreeSet};
-use crate::syntax::visitor::{self, ExprKindMutVisitor, ExprKindVisitor};
+use crate::syntax::visitor::{self, ExprKindVisitor};
 use crate::syntax::*;
 
 pub type Integer = isize;
@@ -208,13 +208,6 @@ impl<SE, E> ExprKind<SE, E> {
         self.traverse_ref_maybe_binder(|_, e| visit_subexpr(e))
     }
 
-    fn traverse_mut<'a, Err>(
-        &'a mut self,
-        visit_subexpr: impl FnMut(&'a mut SE) -> Result<(), Err>,
-    ) -> Result<(), Err> {
-        visitor::TraverseMutVisitor { visit_subexpr }.visit(self)
-    }
-
     pub fn map_ref_maybe_binder<'a, SE2>(
         &'a self,
         mut map: impl FnMut(Option<&'a Label>, &'a SE) -> SE2,
@@ -248,16 +241,15 @@ impl<SE, E> ExprKind<SE, E> {
     {
         self.map_ref_maybe_binder(|_, e| map_subexpr(e))
     }
-
-    pub fn map_mut<'a>(&'a mut self, mut map_subexpr: impl FnMut(&'a mut SE)) {
-        trivial_result(self.traverse_mut(|x| Ok(map_subexpr(x))))
-    }
 }
 
 impl<E> Expr<E> {
     pub fn as_ref(&self) -> &UnspannedExpr<E> {
         &self.kind
     }
+    pub fn kind(&self) -> &UnspannedExpr<E> {
+        &self.kind
+    }
     pub fn span(&self) -> Span {
         self.span.clone()
     }
@@ -281,43 +273,6 @@ impl<E> Expr<E> {
             span,
         }
     }
-
-    pub fn traverse_resolve_mut<Err, F1>(
-        &mut self,
-        f: &mut F1,
-    ) -> Result<(), Err>
-    where
-        E: Clone,
-        F1: FnMut(Import<Expr<E>>) -> Result<E, Err>,
-    {
-        match self.kind.as_mut() {
-            ExprKind::BinOp(BinOp::ImportAlt, l, r) => {
-                let garbage_expr = ExprKind::BoolLit(false);
-                let new_self = if l.traverse_resolve_mut(f).is_ok() {
-                    l
-                } else {
-                    r.traverse_resolve_mut(f)?;
-                    r
-                };
-                *self.kind =
-                    std::mem::replace(new_self.kind.as_mut(), garbage_expr);
-            }
-            _ => {
-                self.kind.traverse_mut(|e| e.traverse_resolve_mut(f))?;
-                if let ExprKind::Import(import) = self.kind.as_mut() {
-                    let garbage_import = Import {
-                        mode: ImportMode::Code,
-                        location: ImportLocation::Missing,
-                        hash: None,
-                    };
-                    // Move out of &mut import
-                    let import = std::mem::replace(import, garbage_import);
-                    *self.kind = ExprKind::Embed(f(import)?);
-                }
-            }
-        }
-        Ok(())
-    }
 }
 
 pub fn trivial_result<T>(x: Result<T, !>) -> T {
diff --git a/dhall/src/syntax/ast/visitor.rs b/dhall/src/syntax/ast/visitor.rs
index 6a1ce7d..c09b8d4 100644
--- a/dhall/src/syntax/ast/visitor.rs
+++ b/dhall/src/syntax/ast/visitor.rs
@@ -32,29 +32,6 @@ pub trait ExprKindVisitor<'a, SE1, SE2, E1, E2>: Sized {
     }
 }
 
-/// Like `ExprKindVisitor`, but by mutable reference
-pub trait ExprKindMutVisitor<'a, SE, E>: Sized {
-    type Error;
-
-    fn visit_subexpr(&mut self, subexpr: &'a mut SE)
-        -> Result<(), Self::Error>;
-    fn visit_embed(self, _embed: &'a mut E) -> Result<(), Self::Error> {
-        Ok(())
-    }
-
-    fn visit_subexpr_under_binder(
-        mut self,
-        _label: &'a mut Label,
-        subexpr: &'a mut SE,
-    ) -> Result<(), Self::Error> {
-        self.visit_subexpr(subexpr)
-    }
-
-    fn visit(self, input: &'a mut ExprKind<SE, E>) -> Result<(), Self::Error> {
-        visit_mut(self, input)
-    }
-}
-
 fn visit_ref<'a, V, SE1, SE2, E1, E2>(
     mut v: V,
     input: &'a ExprKind<SE1, E1>,
@@ -174,128 +151,6 @@ where
     })
 }
 
-fn visit_mut<'a, V, SE, E>(
-    mut v: V,
-    input: &'a mut ExprKind<SE, E>,
-) -> Result<(), V::Error>
-where
-    V: ExprKindMutVisitor<'a, SE, E>,
-{
-    fn vec<'a, V, SE, E>(v: &mut V, x: &'a mut Vec<SE>) -> Result<(), V::Error>
-    where
-        V: ExprKindMutVisitor<'a, SE, E>,
-    {
-        for x in x {
-            v.visit_subexpr(x)?;
-        }
-        Ok(())
-    }
-    fn opt<'a, V, SE, E>(
-        v: &mut V,
-        x: &'a mut Option<SE>,
-    ) -> Result<(), V::Error>
-    where
-        V: ExprKindMutVisitor<'a, SE, E>,
-    {
-        if let Some(x) = x {
-            v.visit_subexpr(x)?;
-        }
-        Ok(())
-    }
-    fn dupmap<'a, V, SE, E>(
-        mut v: V,
-        x: impl IntoIterator<Item = (&'a Label, &'a mut SE)>,
-    ) -> Result<(), V::Error>
-    where
-        SE: 'a,
-        V: ExprKindMutVisitor<'a, SE, E>,
-    {
-        for (_, x) in x {
-            v.visit_subexpr(x)?;
-        }
-        Ok(())
-    }
-    fn optdupmap<'a, V, SE, E>(
-        mut v: V,
-        x: impl IntoIterator<Item = (&'a Label, &'a mut Option<SE>)>,
-    ) -> Result<(), V::Error>
-    where
-        SE: 'a,
-        V: ExprKindMutVisitor<'a, SE, E>,
-    {
-        for (_, x) in x {
-            opt(&mut v, x)?;
-        }
-        Ok(())
-    }
-
-    use crate::syntax::ExprKind::*;
-    match input {
-        Var(_) | Const(_) | Builtin(_) | BoolLit(_) | NaturalLit(_)
-        | IntegerLit(_) | DoubleLit(_) => {}
-        Lam(l, t, e) => {
-            v.visit_subexpr(t)?;
-            v.visit_subexpr_under_binder(l, e)?;
-        }
-        Pi(l, t, e) => {
-            v.visit_subexpr(t)?;
-            v.visit_subexpr_under_binder(l, e)?;
-        }
-        Let(l, t, a, e) => {
-            opt(&mut v, t)?;
-            v.visit_subexpr(a)?;
-            v.visit_subexpr_under_binder(l, e)?;
-        }
-        App(f, a) => {
-            v.visit_subexpr(f)?;
-            v.visit_subexpr(a)?;
-        }
-        Annot(x, t) => {
-            v.visit_subexpr(x)?;
-            v.visit_subexpr(t)?;
-        }
-        TextLit(t) => t.traverse_mut(|e| v.visit_subexpr(e))?,
-        BinOp(_, x, y) => {
-            v.visit_subexpr(x)?;
-            v.visit_subexpr(y)?;
-        }
-        BoolIf(b, t, f) => {
-            v.visit_subexpr(b)?;
-            v.visit_subexpr(t)?;
-            v.visit_subexpr(f)?;
-        }
-        EmptyListLit(t) => v.visit_subexpr(t)?,
-        NEListLit(es) => vec(&mut v, es)?,
-        SomeLit(e) => v.visit_subexpr(e)?,
-        RecordType(kts) => dupmap(v, kts)?,
-        RecordLit(kvs) => dupmap(v, kvs)?,
-        UnionType(kts) => optdupmap(v, kts)?,
-        Merge(x, y, t) => {
-            v.visit_subexpr(x)?;
-            v.visit_subexpr(y)?;
-            opt(&mut v, t)?;
-        }
-        ToMap(x, t) => {
-            v.visit_subexpr(x)?;
-            opt(&mut v, t)?;
-        }
-        Field(e, _) => v.visit_subexpr(e)?,
-        Projection(e, _) => v.visit_subexpr(e)?,
-        ProjectionByExpr(e, x) => {
-            v.visit_subexpr(e)?;
-            v.visit_subexpr(x)?;
-        }
-        Completion(x, y) => {
-            v.visit_subexpr(x)?;
-            v.visit_subexpr(y)?;
-        }
-        Assert(e) => v.visit_subexpr(e)?,
-        Import(i) => i.traverse_mut(|e| v.visit_subexpr(e))?,
-        Embed(a) => v.visit_embed(a)?,
-    }
-    Ok(())
-}
-
 pub struct TraverseRefMaybeBinderVisitor<F>(pub F);
 
 impl<'a, SE, E, SE2, Err, F> ExprKindVisitor<'a, SE, SE2, E, E>
@@ -321,24 +176,3 @@ where
         Ok(embed.clone())
     }
 }
-
-pub struct TraverseMutVisitor<F1> {
-    pub visit_subexpr: F1,
-}
-
-impl<'a, SE, E, Err, F1> ExprKindMutVisitor<'a, SE, E>
-    for TraverseMutVisitor<F1>
-where
-    SE: 'a,
-    E: 'a,
-    F1: FnMut(&'a mut SE) -> Result<(), Err>,
-{
-    type Error = Err;
-
-    fn visit_subexpr(
-        &mut self,
-        subexpr: &'a mut SE,
-    ) -> Result<(), Self::Error> {
-        (self.visit_subexpr)(subexpr)
-    }
-}
-- 
cgit v1.3.1


From 5a2538d174fd36a8ed7f4fa344b9583fc48bd977 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 11 Feb 2020 13:12:13 +0000
Subject: Remove the Embed variant from ExprKind

---
 dhall/src/lib.rs                     |  8 ++---
 dhall/src/semantics/builtins.rs      |  2 +-
 dhall/src/semantics/hir.rs           |  8 ++---
 dhall/src/semantics/nze/normalize.rs |  6 ++--
 dhall/src/semantics/nze/value.rs     | 16 ++++------
 dhall/src/semantics/resolve.rs       |  4 +--
 dhall/src/semantics/tck/tyexpr.rs    |  3 +-
 dhall/src/semantics/tck/typecheck.rs |  7 ++---
 dhall/src/syntax/ast/expr.rs         | 58 ++++++++++++------------------------
 dhall/src/syntax/ast/visitor.rs      | 30 ++++++++-----------
 dhall/src/syntax/binary/decode.rs    |  2 +-
 dhall/src/syntax/binary/encode.rs    | 44 ++++++++++-----------------
 dhall/src/syntax/text/parser.rs      | 10 ++-----
 dhall/src/syntax/text/printer.rs     | 17 +++++------
 serde_dhall/src/serde.rs             |  2 +-
 15 files changed, 80 insertions(+), 137 deletions(-)

(limited to 'dhall/src/syntax')

diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 2d261f9..2f0ed4b 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -28,10 +28,10 @@ use crate::semantics::{
 use crate::syntax::binary;
 use crate::syntax::{Builtin, Expr};
 
-pub type ParsedExpr = Expr<Normalized>;
-pub type DecodedExpr = Expr<Normalized>;
-pub type ResolvedExpr = Expr<Normalized>;
-pub type NormalizedExpr = Expr<Normalized>;
+pub type ParsedExpr = Expr;
+pub type DecodedExpr = Expr;
+pub type ResolvedExpr = Expr;
+pub type NormalizedExpr = Expr;
 
 #[derive(Debug, Clone)]
 pub struct Parsed(ParsedExpr, ImportRoot);
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index d9a3599..cbb5a6e 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -55,7 +55,7 @@ impl BuiltinClosure<Value> {
     }
 }
 
-pub(crate) fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
+pub(crate) fn rc(x: UnspannedExpr) -> Expr {
     Expr::new(x, Span::Artificial)
 }
 
diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index b45851f..288031c 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -1,7 +1,7 @@
 #![allow(dead_code)]
 use crate::semantics::{NameEnv, NzEnv, TyEnv, Value};
-use crate::syntax::{ExprKind, Span, V};
-use crate::{Expr, Normalized, NormalizedExpr, ToExprOptions};
+use crate::syntax::{Expr, ExprKind, Span, V};
+use crate::{NormalizedExpr, ToExprOptions};
 
 /// Stores an alpha-normalized variable.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@@ -13,8 +13,8 @@ pub struct AlphaVar {
 pub(crate) enum HirKind {
     /// A resolved variable (i.e. a DeBruijn index)
     Var(AlphaVar),
-    // Forbidden ExprKind variants: Var, Import, Embed
-    Expr(ExprKind<Hir, Normalized>),
+    // Forbidden ExprKind variants: Var, Import
+    Expr(ExprKind<Hir>),
 }
 
 // An expression with resolved variables and imports.
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index d12146a..03b91a5 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -6,7 +6,6 @@ use crate::semantics::{
     Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind,
 };
 use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
-use crate::Normalized;
 
 pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind {
     match f.kind() {
@@ -90,7 +89,7 @@ enum Ret<'a> {
     ValueKind(ValueKind),
     Value(Value),
     ValueRef(&'a Value),
-    Expr(ExprKind<Value, Normalized>),
+    Expr(ExprKind<Value>),
 }
 
 fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
@@ -215,7 +214,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
 }
 
 pub(crate) fn normalize_one_layer(
-    expr: ExprKind<Value, Normalized>,
+    expr: ExprKind<Value>,
     env: &NzEnv,
 ) -> ValueKind {
     use ValueKind::{
@@ -233,7 +232,6 @@ pub(crate) fn normalize_one_layer(
         ExprKind::Lam(..)
         | ExprKind::Pi(..)
         | ExprKind::Let(..)
-        | ExprKind::Embed(_)
         | ExprKind::Var(_) => {
             unreachable!("This case should have been handled in typecheck")
         }
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index a60be9d..0df3c74 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -12,7 +12,7 @@ use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
     NaiveDouble, Natural, Span,
 };
-use crate::{Normalized, NormalizedExpr, ToExprOptions};
+use crate::{NormalizedExpr, ToExprOptions};
 
 /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
 /// automatically. Uses a Rc<RefCell> to share computation.
@@ -34,10 +34,7 @@ pub(crate) enum Thunk {
     /// A completely unnormalized expression.
     Thunk { env: NzEnv, body: Hir },
     /// A partially normalized expression that may need to go through `normalize_one_layer`.
-    PartialExpr {
-        env: NzEnv,
-        expr: ExprKind<Value, Normalized>,
-    },
+    PartialExpr { env: NzEnv, expr: ExprKind<Value> },
 }
 
 /// An unevaluated subexpression that takes an argument.
@@ -96,7 +93,7 @@ pub(crate) enum ValueKind {
     TextLit(TextLit),
     Equivalence(Value, Value),
     /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
-    PartialExpr(ExprKind<Value, Normalized>),
+    PartialExpr(ExprKind<Value>),
 }
 
 impl Value {
@@ -106,7 +103,7 @@ impl Value {
         ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value()
     }
     /// Construct a Value from a partially normalized expression that's not in WHNF.
-    pub(crate) fn from_partial_expr(e: ExprKind<Value, Normalized>) -> Value {
+    pub(crate) fn from_partial_expr(e: ExprKind<Value>) -> Value {
         // TODO: env
         let env = NzEnv::new();
         ValueInternal::from_thunk(
@@ -389,10 +386,7 @@ impl Thunk {
     fn new(env: NzEnv, body: Hir) -> Self {
         Thunk::Thunk { env, body }
     }
-    fn from_partial_expr(
-        env: NzEnv,
-        expr: ExprKind<Value, Normalized>,
-    ) -> Self {
+    fn from_partial_expr(env: NzEnv, expr: ExprKind<Value>) -> Self {
         Thunk::PartialExpr { env, expr }
     }
     fn eval(self) -> ValueKind {
diff --git a/dhall/src/semantics/resolve.rs b/dhall/src/semantics/resolve.rs
index 80e5132..fac88d2 100644
--- a/dhall/src/semantics/resolve.rs
+++ b/dhall/src/semantics/resolve.rs
@@ -6,7 +6,7 @@ use crate::error::{Error, ImportError};
 use crate::semantics::{mkerr, Hir, HirKind, NameEnv};
 use crate::syntax;
 use crate::syntax::{BinOp, Expr, ExprKind, FilePath, ImportLocation, URL};
-use crate::{Normalized, Parsed, ParsedExpr, Resolved};
+use crate::{Parsed, ParsedExpr, Resolved};
 
 type Import = syntax::Import<Hir>;
 
@@ -102,7 +102,7 @@ fn load_import(env: &mut ResolveEnv, f: &Path) -> Result<Hir, Error> {
 /// found imports to the provided function.
 fn traverse_resolve_expr(
     name_env: &mut NameEnv,
-    expr: &Expr<Normalized>,
+    expr: &Expr,
     f: &mut impl FnMut(Import) -> Result<Hir, Error>,
 ) -> Result<Hir, Error> {
     let kind = match expr.kind() {
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index a1666a4..d46ab87 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,7 +1,6 @@
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::{AlphaVar, Hir, HirKind, NzEnv, Value};
 use crate::syntax::{ExprKind, Span};
-use crate::Normalized;
 use crate::{NormalizedExpr, ToExprOptions};
 
 pub(crate) type Type = Value;
@@ -10,7 +9,7 @@ pub(crate) type Type = Value;
 pub(crate) enum TyExprKind {
     Var(AlphaVar),
     // Forbidden ExprKind variants: Var, Import, Embed
-    Expr(ExprKind<TyExpr, Normalized>),
+    Expr(ExprKind<TyExpr>),
 }
 
 // An expression with inferred types at every node and resolved variables.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 4e45637..f9ff3d3 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -11,7 +11,6 @@ use crate::semantics::{
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Span,
 };
-use crate::Normalized;
 
 fn type_of_recordtype<'a>(
     span: Span,
@@ -51,7 +50,7 @@ pub fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
 /// layer.
 fn type_one_layer(
     env: &TyEnv,
-    ekind: ExprKind<TyExpr, Normalized>,
+    ekind: ExprKind<TyExpr>,
     span: Span,
 ) -> Result<TyExpr, TypeError> {
     let span_err = |msg: &str| {
@@ -66,9 +65,7 @@ fn type_one_layer(
         ExprKind::Import(..) => unreachable!(
             "There should remain no imports in a resolved expression"
         ),
-        ExprKind::Var(..)
-        | ExprKind::Const(Const::Sort)
-        | ExprKind::Embed(..) => unreachable!(), // Handled in type_with
+        ExprKind::Var(..) | ExprKind::Const(Const::Sort) => unreachable!(), // Handled in type_with
 
         ExprKind::Lam(binder, annot, body) => {
             let body_ty = body.get_type()?;
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 420df5b..722630f 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -96,19 +96,19 @@ pub enum Builtin {
 
 // Each node carries an annotation.
 #[derive(Debug, Clone)]
-pub struct Expr<Embed> {
-    kind: Box<ExprKind<Expr<Embed>, Embed>>,
+pub struct Expr {
+    kind: Box<ExprKind<Expr>>,
     span: Span,
 }
 
-pub type UnspannedExpr<Embed> = ExprKind<Expr<Embed>, Embed>;
+pub type UnspannedExpr = ExprKind<Expr>;
 
 /// Syntax tree for expressions
 // Having the recursion out of the enum definition enables writing
 // much more generic code and improves pattern-matching behind
 // smart pointers.
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
-pub enum ExprKind<SubExpr, Embed> {
+pub enum ExprKind<SubExpr> {
     Const(Const),
     ///  `x`
     ///  `x@n`
@@ -169,18 +169,13 @@ pub enum ExprKind<SubExpr, Embed> {
     Completion(SubExpr, SubExpr),
     /// `./some/path`
     Import(Import<SubExpr>),
-    /// Embeds the result of resolving an import
-    Embed(Embed),
 }
 
-impl<SE, E> ExprKind<SE, E> {
+impl<SE> ExprKind<SE> {
     pub fn traverse_ref_maybe_binder<'a, SE2, Err>(
         &'a self,
         visit: impl FnMut(Option<&'a Label>, &'a SE) -> Result<SE2, Err>,
-    ) -> Result<ExprKind<SE2, E>, Err>
-    where
-        E: Clone,
-    {
+    ) -> Result<ExprKind<SE2>, Err> {
         visitor::TraverseRefMaybeBinderVisitor(visit).visit(self)
     }
 
@@ -188,10 +183,7 @@ impl<SE, E> ExprKind<SE, E> {
         &'a self,
         mut visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
         mut visit_under_binder: impl FnMut(&'a Label, &'a SE) -> Result<SE2, Err>,
-    ) -> Result<ExprKind<SE2, E>, Err>
-    where
-        E: Clone,
-    {
+    ) -> Result<ExprKind<SE2>, Err> {
         self.traverse_ref_maybe_binder(|l, x| match l {
             None => visit_subexpr(x),
             Some(l) => visit_under_binder(l, x),
@@ -201,20 +193,14 @@ impl<SE, E> ExprKind<SE, E> {
     pub(crate) fn traverse_ref<'a, SE2, Err>(
         &'a self,
         mut visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>,
-    ) -> Result<ExprKind<SE2, E>, Err>
-    where
-        E: Clone,
-    {
+    ) -> Result<ExprKind<SE2>, Err> {
         self.traverse_ref_maybe_binder(|_, e| visit_subexpr(e))
     }
 
     pub fn map_ref_maybe_binder<'a, SE2>(
         &'a self,
         mut map: impl FnMut(Option<&'a Label>, &'a SE) -> SE2,
-    ) -> ExprKind<SE2, E>
-    where
-        E: Clone,
-    {
+    ) -> ExprKind<SE2> {
         trivial_result(self.traverse_ref_maybe_binder(|l, x| Ok(map(l, x))))
     }
 
@@ -222,10 +208,7 @@ impl<SE, E> ExprKind<SE, E> {
         &'a self,
         mut map_subexpr: impl FnMut(&'a SE) -> SE2,
         mut map_under_binder: impl FnMut(&'a Label, &'a SE) -> SE2,
-    ) -> ExprKind<SE2, E>
-    where
-        E: Clone,
-    {
+    ) -> ExprKind<SE2> {
         self.map_ref_maybe_binder(|l, x| match l {
             None => map_subexpr(x),
             Some(l) => map_under_binder(l, x),
@@ -235,33 +218,30 @@ impl<SE, E> ExprKind<SE, E> {
     pub fn map_ref<'a, SE2>(
         &'a self,
         mut map_subexpr: impl FnMut(&'a SE) -> SE2,
-    ) -> ExprKind<SE2, E>
-    where
-        E: Clone,
-    {
+    ) -> ExprKind<SE2> {
         self.map_ref_maybe_binder(|_, e| map_subexpr(e))
     }
 }
 
-impl<E> Expr<E> {
-    pub fn as_ref(&self) -> &UnspannedExpr<E> {
+impl Expr {
+    pub fn as_ref(&self) -> &UnspannedExpr {
         &self.kind
     }
-    pub fn kind(&self) -> &UnspannedExpr<E> {
+    pub fn kind(&self) -> &UnspannedExpr {
         &self.kind
     }
     pub fn span(&self) -> Span {
         self.span.clone()
     }
 
-    pub fn new(kind: UnspannedExpr<E>, span: Span) -> Self {
+    pub fn new(kind: UnspannedExpr, span: Span) -> Self {
         Expr {
             kind: Box::new(kind),
             span,
         }
     }
 
-    pub fn rewrap<E2>(&self, kind: UnspannedExpr<E2>) -> Expr<E2> {
+    pub fn rewrap(&self, kind: UnspannedExpr) -> Expr {
         Expr {
             kind: Box::new(kind),
             span: self.span.clone(),
@@ -317,15 +297,15 @@ impl From<Label> for V {
     }
 }
 
-impl<Embed: PartialEq> std::cmp::PartialEq for Expr<Embed> {
+impl std::cmp::PartialEq for Expr {
     fn eq(&self, other: &Self) -> bool {
         self.kind == other.kind
     }
 }
 
-impl<Embed: Eq> std::cmp::Eq for Expr<Embed> {}
+impl std::cmp::Eq for Expr {}
 
-impl<Embed: std::hash::Hash> std::hash::Hash for Expr<Embed> {
+impl std::hash::Hash for Expr {
     fn hash<H>(&self, state: &mut H)
     where
         H: std::hash::Hasher,
diff --git a/dhall/src/syntax/ast/visitor.rs b/dhall/src/syntax/ast/visitor.rs
index c09b8d4..fc90efd 100644
--- a/dhall/src/syntax/ast/visitor.rs
+++ b/dhall/src/syntax/ast/visitor.rs
@@ -10,11 +10,10 @@ use crate::syntax::*;
 /// preventing exactly this ! So we have to be more clever. The visitor pattern allows us to have
 /// only one mutable thing the whole time: the visitor itself. The visitor can then carry around
 /// multiple closures or just one, and Rust is ok with either. See for example TraverseRefVisitor.
-pub trait ExprKindVisitor<'a, SE1, SE2, E1, E2>: Sized {
+pub trait ExprKindVisitor<'a, SE1, SE2>: Sized {
     type Error;
 
     fn visit_subexpr(&mut self, subexpr: &'a SE1) -> Result<SE2, Self::Error>;
-    fn visit_embed(self, embed: &'a E1) -> Result<E2, Self::Error>;
 
     fn visit_subexpr_under_binder(
         mut self,
@@ -26,18 +25,18 @@ pub trait ExprKindVisitor<'a, SE1, SE2, E1, E2>: Sized {
 
     fn visit(
         self,
-        input: &'a ExprKind<SE1, E1>,
-    ) -> Result<ExprKind<SE2, E2>, Self::Error> {
+        input: &'a ExprKind<SE1>,
+    ) -> Result<ExprKind<SE2>, Self::Error> {
         visit_ref(self, input)
     }
 }
 
-fn visit_ref<'a, V, SE1, SE2, E1, E2>(
+fn visit_ref<'a, V, SE1, SE2>(
     mut v: V,
-    input: &'a ExprKind<SE1, E1>,
-) -> Result<ExprKind<SE2, E2>, V::Error>
+    input: &'a ExprKind<SE1>,
+) -> Result<ExprKind<SE2>, V::Error>
 where
-    V: ExprKindVisitor<'a, SE1, SE2, E1, E2>,
+    V: ExprKindVisitor<'a, SE1, SE2>,
 {
     fn vec<'a, T, U, Err, F: FnMut(&'a T) -> Result<U, Err>>(
         x: &'a [T],
@@ -54,27 +53,27 @@ where
             None => None,
         })
     }
-    fn dupmap<'a, V, SE1, SE2, E1, E2, T>(
+    fn dupmap<'a, V, SE1, SE2, T>(
         x: impl IntoIterator<Item = (&'a Label, &'a SE1)>,
         mut v: V,
     ) -> Result<T, V::Error>
     where
         SE1: 'a,
         T: FromIterator<(Label, SE2)>,
-        V: ExprKindVisitor<'a, SE1, SE2, E1, E2>,
+        V: ExprKindVisitor<'a, SE1, SE2>,
     {
         x.into_iter()
             .map(|(k, x)| Ok((k.clone(), v.visit_subexpr(x)?)))
             .collect()
     }
-    fn optdupmap<'a, V, SE1, SE2, E1, E2, T>(
+    fn optdupmap<'a, V, SE1, SE2, T>(
         x: impl IntoIterator<Item = (&'a Label, &'a Option<SE1>)>,
         mut v: V,
     ) -> Result<T, V::Error>
     where
         SE1: 'a,
         T: FromIterator<(Label, Option<SE2>)>,
-        V: ExprKindVisitor<'a, SE1, SE2, E1, E2>,
+        V: ExprKindVisitor<'a, SE1, SE2>,
     {
         x.into_iter()
             .map(|(k, x)| {
@@ -147,17 +146,15 @@ where
         }
         Assert(e) => Assert(v.visit_subexpr(e)?),
         Import(i) => Import(i.traverse_ref(|e| v.visit_subexpr(e))?),
-        Embed(a) => Embed(v.visit_embed(a)?),
     })
 }
 
 pub struct TraverseRefMaybeBinderVisitor<F>(pub F);
 
-impl<'a, SE, E, SE2, Err, F> ExprKindVisitor<'a, SE, SE2, E, E>
+impl<'a, SE, SE2, Err, F> ExprKindVisitor<'a, SE, SE2>
     for TraverseRefMaybeBinderVisitor<F>
 where
     SE: 'a,
-    E: 'a + Clone,
     F: FnMut(Option<&'a Label>, &'a SE) -> Result<SE2, Err>,
 {
     type Error = Err;
@@ -172,7 +169,4 @@ where
     ) -> Result<SE2, Self::Error> {
         (self.0)(Some(label), subexpr)
     }
-    fn visit_embed(self, embed: &'a E) -> Result<E, Self::Error> {
-        Ok(embed.clone())
-    }
 }
diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs
index 52b699c..6fbcc10 100644
--- a/dhall/src/syntax/binary/decode.rs
+++ b/dhall/src/syntax/binary/decode.rs
@@ -19,7 +19,7 @@ pub(crate) fn decode(data: &[u8]) -> Result<DecodedExpr, DecodeError> {
 }
 
 // Should probably rename this
-fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
+fn rc(x: UnspannedExpr) -> Expr {
     Expr::new(x, Span::Decoded)
 }
 
diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs
index 5e79f2d..686f737 100644
--- a/dhall/src/syntax/binary/encode.rs
+++ b/dhall/src/syntax/binary/encode.rs
@@ -9,17 +9,16 @@ use crate::syntax::{
     Label, Scheme, V,
 };
 
-/// Warning: will fail if `expr` contains an `Embed` node.
-pub(crate) fn encode<E>(expr: &Expr<E>) -> Result<Vec<u8>, EncodeError> {
+pub(crate) fn encode(expr: &Expr) -> Result<Vec<u8>, EncodeError> {
     serde_cbor::ser::to_vec(&Serialize::Expr(expr))
         .map_err(|e| EncodeError::CBORError(e))
 }
 
-enum Serialize<'a, E> {
-    Expr(&'a Expr<E>),
+enum Serialize<'a> {
+    Expr(&'a Expr),
     CBOR(cbor::Value),
-    RecordMap(&'a DupTreeMap<Label, Expr<E>>),
-    UnionMap(&'a DupTreeMap<Label, Option<Expr<E>>>),
+    RecordMap(&'a DupTreeMap<Label, Expr>),
+    UnionMap(&'a DupTreeMap<Label, Option<Expr>>),
 }
 
 macro_rules! count {
@@ -39,7 +38,7 @@ macro_rules! ser_seq {
     }};
 }
 
-fn serialize_subexpr<S, E>(ser: S, e: &Expr<E>) -> Result<S::Ok, S::Error>
+fn serialize_subexpr<S>(ser: S, e: &Expr) -> Result<S::Ok, S::Error>
 where
     S: serde::ser::Serializer,
 {
@@ -49,11 +48,11 @@ where
     use syntax::ExprKind::*;
 
     use self::Serialize::{RecordMap, UnionMap};
-    fn expr<E>(x: &Expr<E>) -> self::Serialize<'_, E> {
+    fn expr(x: &Expr) -> self::Serialize<'_> {
         self::Serialize::Expr(x)
     }
     let cbor =
-        |v: cbor::Value| -> self::Serialize<'_, E> { self::Serialize::CBOR(v) };
+        |v: cbor::Value| -> self::Serialize<'_> { self::Serialize::CBOR(v) };
     let tag = |x: u64| cbor(U64(x));
     let null = || cbor(cbor::Value::Null);
     let label = |l: &Label| cbor(cbor::Value::String(l.into()));
@@ -166,16 +165,10 @@ where
         }
         Completion(x, y) => ser_seq!(ser; tag(3), tag(13), expr(x), expr(y)),
         Import(import) => serialize_import(ser, import),
-        Embed(_) => unimplemented!(
-            "An expression with resolved imports cannot be binary-encoded"
-        ),
     }
 }
 
-fn serialize_import<S, E>(
-    ser: S,
-    import: &Import<Expr<E>>,
-) -> Result<S::Ok, S::Error>
+fn serialize_import<S>(ser: S, import: &Import<Expr>) -> Result<S::Ok, S::Error>
 where
     S: serde::ser::Serializer,
 {
@@ -256,7 +249,7 @@ where
     ser_seq.end()
 }
 
-impl<'a, E> serde::ser::Serialize for Serialize<'a, E> {
+impl<'a> serde::ser::Serialize for Serialize<'a> {
     fn serialize<S>(&self, ser: S) -> Result<S::Ok, S::Error>
     where
         S: serde::ser::Serializer,
@@ -282,10 +275,8 @@ impl<'a, E> serde::ser::Serialize for Serialize<'a, E> {
     }
 }
 
-fn collect_nested_applications<'a, E>(
-    e: &'a Expr<E>,
-) -> (&'a Expr<E>, Vec<&'a Expr<E>>) {
-    fn go<'a, E>(e: &'a Expr<E>, vec: &mut Vec<&'a Expr<E>>) -> &'a Expr<E> {
+fn collect_nested_applications<'a>(e: &'a Expr) -> (&'a Expr, Vec<&'a Expr>) {
+    fn go<'a>(e: &'a Expr, vec: &mut Vec<&'a Expr>) -> &'a Expr {
         match e.as_ref() {
             ExprKind::App(f, a) => {
                 vec.push(a);
@@ -299,15 +290,10 @@ fn collect_nested_applications<'a, E>(
     (e, vec)
 }
 
-type LetBinding<'a, E> = (&'a Label, &'a Option<Expr<E>>, &'a Expr<E>);
+type LetBinding<'a> = (&'a Label, &'a Option<Expr>, &'a Expr);
 
-fn collect_nested_lets<'a, E>(
-    e: &'a Expr<E>,
-) -> (&'a Expr<E>, Vec<LetBinding<'a, E>>) {
-    fn go<'a, E>(
-        e: &'a Expr<E>,
-        vec: &mut Vec<LetBinding<'a, E>>,
-    ) -> &'a Expr<E> {
+fn collect_nested_lets<'a>(e: &'a Expr) -> (&'a Expr, Vec<LetBinding<'a>>) {
+    fn go<'a>(e: &'a Expr, vec: &mut Vec<LetBinding<'a>>) -> &'a Expr {
         match e.as_ref() {
             ExprKind::Let(l, t, v, e) => {
                 vec.push((l, t, v));
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index 8d571c0..0ff1363 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -5,23 +5,19 @@ use std::rc::Rc;
 
 use pest_consume::{match_nodes, Parser};
 
-use crate::syntax;
 use crate::syntax::map::{DupTreeMap, DupTreeSet};
 use crate::syntax::ExprKind::*;
 use crate::syntax::{
-    Double, FilePath, FilePrefix, Hash, ImportLocation, ImportMode, Integer,
-    InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, Natural,
-    Scheme, Span, URL, V,
+    Double, Expr, FilePath, FilePrefix, Hash, ImportLocation, ImportMode,
+    Integer, InterpolatedText, InterpolatedTextContents, Label, NaiveDouble,
+    Natural, Scheme, Span, UnspannedExpr, URL, V,
 };
-use crate::Normalized;
 
 // This file consumes the parse tree generated by pest and turns it into
 // our own AST. All those custom macros should eventually moved into
 // their own crate because they are quite general and useful. For now they
 // are here and hopefully you can figure out how they work.
 
-type Expr = syntax::Expr<Normalized>;
-type UnspannedExpr = syntax::UnspannedExpr<Normalized>;
 type ParsedText = InterpolatedText<Expr>;
 type ParsedTextContents = InterpolatedTextContents<Expr>;
 type ParseInput<'input> = pest_consume::Node<'input, Rule, Rc<str>>;
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index 06dd70f..d1c9588 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -19,17 +19,17 @@ enum PrintPhase {
 // Wraps an Expr with a phase, so that phase selection can be done separate from the actual
 // printing.
 #[derive(Clone)]
-struct PhasedExpr<'a, E>(&'a Expr<E>, PrintPhase);
+struct PhasedExpr<'a>(&'a Expr, PrintPhase);
 
-impl<'a, E: Display + Clone> PhasedExpr<'a, E> {
-    fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, E> {
+impl<'a> PhasedExpr<'a> {
+    fn phase(self, phase: PrintPhase) -> PhasedExpr<'a> {
         PhasedExpr(self.0, phase)
     }
 }
 
-impl<E: Display + Clone> UnspannedExpr<E> {
+impl UnspannedExpr {
     // Annotate subexpressions with the appropriate phase, defaulting to Base
-    fn annotate_with_phases<'a>(&'a self) -> ExprKind<PhasedExpr<'a, E>, E> {
+    fn annotate_with_phases<'a>(&'a self) -> ExprKind<PhasedExpr<'a>> {
         use crate::syntax::ExprKind::*;
         use PrintPhase::*;
         let with_base = self.map_ref(|e| PhasedExpr(e, Base));
@@ -134,7 +134,7 @@ where
 }
 
 /// Generic instance that delegates to subexpressions
-impl<SE: Display + Clone, E: Display> Display for ExprKind<SE, E> {
+impl<SE: Display + Clone> Display for ExprKind<SE> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         use crate::syntax::ExprKind::*;
         match self {
@@ -232,19 +232,18 @@ impl<SE: Display + Clone, E: Display> Display for ExprKind<SE, E> {
                 write!(f, "{}::{}", a, b)?;
             }
             Import(a) => a.fmt(f)?,
-            Embed(a) => a.fmt(f)?,
         }
         Ok(())
     }
 }
 
-impl<E: Display + Clone> Display for Expr<E> {
+impl Display for Expr {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.as_ref().fmt_phase(f, PrintPhase::Base)
     }
 }
 
-impl<'a, E: Display + Clone> Display for PhasedExpr<'a, E> {
+impl<'a> Display for PhasedExpr<'a> {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
         self.0.as_ref().fmt_phase(f, self.1)
     }
diff --git a/serde_dhall/src/serde.rs b/serde_dhall/src/serde.rs
index 3e78987..92a0015 100644
--- a/serde_dhall/src/serde.rs
+++ b/serde_dhall/src/serde.rs
@@ -115,7 +115,7 @@ impl<'de: 'a, 'a> serde::Deserializer<'de> for Deserializer<'a> {
             | Assert(..) | Builtin(..) | BinOp(..) | BoolIf(..)
             | RecordType(..) | UnionType(..) | Merge(..) | ToMap(..)
             | Projection(..) | ProjectionByExpr(..) | Completion(..)
-            | Import(..) | Embed(..) => not_serde_compatible(),
+            | Import(..) => not_serde_compatible(),
         }
     }
 
-- 
cgit v1.3.1


From cab75190e86e8fd4ccc209499c0e7f300a669022 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 11 Feb 2020 13:33:17 +0000
Subject: Simplify ExprKind visitor

---
 dhall/src/syntax/ast/expr.rs    |   4 +-
 dhall/src/syntax/ast/visitor.rs | 220 +++++++++++++++-------------------------
 2 files changed, 84 insertions(+), 140 deletions(-)

(limited to 'dhall/src/syntax')

diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 722630f..512010a 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,5 +1,5 @@
 use crate::syntax::map::{DupTreeMap, DupTreeSet};
-use crate::syntax::visitor::{self, ExprKindVisitor};
+use crate::syntax::visitor;
 use crate::syntax::*;
 
 pub type Integer = isize;
@@ -176,7 +176,7 @@ impl<SE> ExprKind<SE> {
         &'a self,
         visit: impl FnMut(Option<&'a Label>, &'a SE) -> Result<SE2, Err>,
     ) -> Result<ExprKind<SE2>, Err> {
-        visitor::TraverseRefMaybeBinderVisitor(visit).visit(self)
+        visitor::visit_ref(self, visit)
     }
 
     pub fn traverse_ref_with_special_handling_of_binders<'a, SE2, Err>(
diff --git a/dhall/src/syntax/ast/visitor.rs b/dhall/src/syntax/ast/visitor.rs
index fc90efd..39959ac 100644
--- a/dhall/src/syntax/ast/visitor.rs
+++ b/dhall/src/syntax/ast/visitor.rs
@@ -2,171 +2,115 @@ use std::iter::FromIterator;
 
 use crate::syntax::*;
 
-/// A visitor trait that can be used to traverse `ExprKind`s. We need this pattern so that Rust lets
-/// us have as much mutability as we can.
-/// For example, `traverse_ref_with_special_handling_of_binders` cannot be made using only
-/// `traverse_ref`, because `traverse_ref` takes a `FnMut` so we would need to pass multiple
-/// mutable reverences to this argument to `traverse_ref`. But Rust's ownership system is all about
-/// preventing exactly this ! So we have to be more clever. The visitor pattern allows us to have
-/// only one mutable thing the whole time: the visitor itself. The visitor can then carry around
-/// multiple closures or just one, and Rust is ok with either. See for example TraverseRefVisitor.
-pub trait ExprKindVisitor<'a, SE1, SE2>: Sized {
-    type Error;
+fn vec<'a, T, U, Err>(
+    x: &'a [T],
+    f: impl FnMut(&'a T) -> Result<U, Err>,
+) -> Result<Vec<U>, Err> {
+    x.iter().map(f).collect()
+}
 
-    fn visit_subexpr(&mut self, subexpr: &'a SE1) -> Result<SE2, Self::Error>;
+fn opt<'a, T, U, Err>(
+    x: &'a Option<T>,
+    f: impl FnOnce(&'a T) -> Result<U, Err>,
+) -> Result<Option<U>, Err> {
+    Ok(match x {
+        Some(x) => Some(f(x)?),
+        None => None,
+    })
+}
 
-    fn visit_subexpr_under_binder(
-        mut self,
-        _label: &'a Label,
-        subexpr: &'a SE1,
-    ) -> Result<SE2, Self::Error> {
-        self.visit_subexpr(subexpr)
-    }
+fn dupmap<'a, SE1, SE2, T, Err>(
+    x: impl IntoIterator<Item = (&'a Label, &'a SE1)>,
+    mut f: impl FnMut(&'a SE1) -> Result<SE2, Err>,
+) -> Result<T, Err>
+where
+    SE1: 'a,
+    T: FromIterator<(Label, SE2)>,
+{
+    x.into_iter().map(|(k, x)| Ok((k.clone(), f(x)?))).collect()
+}
 
-    fn visit(
-        self,
-        input: &'a ExprKind<SE1>,
-    ) -> Result<ExprKind<SE2>, Self::Error> {
-        visit_ref(self, input)
-    }
+fn optdupmap<'a, SE1, SE2, T, Err>(
+    x: impl IntoIterator<Item = (&'a Label, &'a Option<SE1>)>,
+    mut f: impl FnMut(&'a SE1) -> Result<SE2, Err>,
+) -> Result<T, Err>
+where
+    SE1: 'a,
+    T: FromIterator<(Label, Option<SE2>)>,
+{
+    x.into_iter()
+        .map(|(k, x)| {
+            Ok((
+                k.clone(),
+                match x {
+                    Some(x) => Some(f(x)?),
+                    None => None,
+                },
+            ))
+        })
+        .collect()
 }
 
-fn visit_ref<'a, V, SE1, SE2>(
-    mut v: V,
+pub(crate) fn visit_ref<'a, F, SE1, SE2, Err>(
     input: &'a ExprKind<SE1>,
-) -> Result<ExprKind<SE2>, V::Error>
+    mut f: F,
+) -> Result<ExprKind<SE2>, Err>
 where
-    V: ExprKindVisitor<'a, SE1, SE2>,
+    F: FnMut(Option<&'a Label>, &'a SE1) -> Result<SE2, Err>,
 {
-    fn vec<'a, T, U, Err, F: FnMut(&'a T) -> Result<U, Err>>(
-        x: &'a [T],
-        f: F,
-    ) -> Result<Vec<U>, Err> {
-        x.iter().map(f).collect()
-    }
-    fn opt<'a, T, U, Err, F: FnOnce(&'a T) -> Result<U, Err>>(
-        x: &'a Option<T>,
-        f: F,
-    ) -> Result<Option<U>, Err> {
-        Ok(match x {
-            Some(x) => Some(f(x)?),
-            None => None,
-        })
-    }
-    fn dupmap<'a, V, SE1, SE2, T>(
-        x: impl IntoIterator<Item = (&'a Label, &'a SE1)>,
-        mut v: V,
-    ) -> Result<T, V::Error>
-    where
-        SE1: 'a,
-        T: FromIterator<(Label, SE2)>,
-        V: ExprKindVisitor<'a, SE1, SE2>,
-    {
-        x.into_iter()
-            .map(|(k, x)| Ok((k.clone(), v.visit_subexpr(x)?)))
-            .collect()
-    }
-    fn optdupmap<'a, V, SE1, SE2, T>(
-        x: impl IntoIterator<Item = (&'a Label, &'a Option<SE1>)>,
-        mut v: V,
-    ) -> Result<T, V::Error>
-    where
-        SE1: 'a,
-        T: FromIterator<(Label, Option<SE2>)>,
-        V: ExprKindVisitor<'a, SE1, SE2>,
-    {
-        x.into_iter()
-            .map(|(k, x)| {
-                Ok((
-                    k.clone(),
-                    match x {
-                        Some(x) => Some(v.visit_subexpr(x)?),
-                        None => None,
-                    },
-                ))
-            })
-            .collect()
+    // Can't use closures because of borrowing rules
+    macro_rules! expr {
+        ($e:expr) => {
+            f(None, $e)
+        };
+        ($l:expr, $e:expr) => {
+            f(Some($l), $e)
+        };
     }
 
     use crate::syntax::ExprKind::*;
     Ok(match input {
         Var(v) => Var(v.clone()),
         Lam(l, t, e) => {
-            let t = v.visit_subexpr(t)?;
-            let e = v.visit_subexpr_under_binder(l, e)?;
+            let t = expr!(t)?;
+            let e = expr!(l, e)?;
             Lam(l.clone(), t, e)
         }
         Pi(l, t, e) => {
-            let t = v.visit_subexpr(t)?;
-            let e = v.visit_subexpr_under_binder(l, e)?;
+            let t = expr!(t)?;
+            let e = expr!(l, e)?;
             Pi(l.clone(), t, e)
         }
         Let(l, t, a, e) => {
-            let t = opt(t, &mut |e| v.visit_subexpr(e))?;
-            let a = v.visit_subexpr(a)?;
-            let e = v.visit_subexpr_under_binder(l, e)?;
+            let t = opt(t, &mut |e| expr!(e))?;
+            let a = expr!(a)?;
+            let e = expr!(l, e)?;
             Let(l.clone(), t, a, e)
         }
-        App(f, a) => App(v.visit_subexpr(f)?, v.visit_subexpr(a)?),
-        Annot(x, t) => Annot(v.visit_subexpr(x)?, v.visit_subexpr(t)?),
+        App(f, a) => App(expr!(f)?, expr!(a)?),
+        Annot(x, t) => Annot(expr!(x)?, expr!(t)?),
         Const(k) => Const(*k),
         Builtin(v) => Builtin(*v),
         BoolLit(b) => BoolLit(*b),
         NaturalLit(n) => NaturalLit(*n),
         IntegerLit(n) => IntegerLit(*n),
         DoubleLit(n) => DoubleLit(*n),
-        TextLit(t) => TextLit(t.traverse_ref(|e| v.visit_subexpr(e))?),
-        BinOp(o, x, y) => BinOp(*o, v.visit_subexpr(x)?, v.visit_subexpr(y)?),
-        BoolIf(b, t, f) => BoolIf(
-            v.visit_subexpr(b)?,
-            v.visit_subexpr(t)?,
-            v.visit_subexpr(f)?,
-        ),
-        EmptyListLit(t) => EmptyListLit(v.visit_subexpr(t)?),
-        NEListLit(es) => NEListLit(vec(es, |e| v.visit_subexpr(e))?),
-        SomeLit(e) => SomeLit(v.visit_subexpr(e)?),
-        RecordType(kts) => RecordType(dupmap(kts, v)?),
-        RecordLit(kvs) => RecordLit(dupmap(kvs, v)?),
-        UnionType(kts) => UnionType(optdupmap(kts, v)?),
-        Merge(x, y, t) => Merge(
-            v.visit_subexpr(x)?,
-            v.visit_subexpr(y)?,
-            opt(t, |e| v.visit_subexpr(e))?,
-        ),
-        ToMap(x, t) => {
-            ToMap(v.visit_subexpr(x)?, opt(t, |e| v.visit_subexpr(e))?)
-        }
-        Field(e, l) => Field(v.visit_subexpr(e)?, l.clone()),
-        Projection(e, ls) => Projection(v.visit_subexpr(e)?, ls.clone()),
-        ProjectionByExpr(e, x) => {
-            ProjectionByExpr(v.visit_subexpr(e)?, v.visit_subexpr(x)?)
-        }
-        Completion(e, x) => {
-            Completion(v.visit_subexpr(e)?, v.visit_subexpr(x)?)
-        }
-        Assert(e) => Assert(v.visit_subexpr(e)?),
-        Import(i) => Import(i.traverse_ref(|e| v.visit_subexpr(e))?),
+        TextLit(t) => TextLit(t.traverse_ref(|e| expr!(e))?),
+        BinOp(o, x, y) => BinOp(*o, expr!(x)?, expr!(y)?),
+        BoolIf(b, t, f) => BoolIf(expr!(b)?, expr!(t)?, expr!(f)?),
+        EmptyListLit(t) => EmptyListLit(expr!(t)?),
+        NEListLit(es) => NEListLit(vec(es, |e| expr!(e))?),
+        SomeLit(e) => SomeLit(expr!(e)?),
+        RecordType(kts) => RecordType(dupmap(kts, |e| expr!(e))?),
+        RecordLit(kvs) => RecordLit(dupmap(kvs, |e| expr!(e))?),
+        UnionType(kts) => UnionType(optdupmap(kts, |e| expr!(e))?),
+        Merge(x, y, t) => Merge(expr!(x)?, expr!(y)?, opt(t, |e| expr!(e))?),
+        ToMap(x, t) => ToMap(expr!(x)?, opt(t, |e| expr!(e))?),
+        Field(e, l) => Field(expr!(e)?, l.clone()),
+        Projection(e, ls) => Projection(expr!(e)?, ls.clone()),
+        ProjectionByExpr(e, x) => ProjectionByExpr(expr!(e)?, expr!(x)?),
+        Completion(e, x) => Completion(expr!(e)?, expr!(x)?),
+        Assert(e) => Assert(expr!(e)?),
+        Import(i) => Import(i.traverse_ref(|e| expr!(e))?),
     })
 }
-
-pub struct TraverseRefMaybeBinderVisitor<F>(pub F);
-
-impl<'a, SE, SE2, Err, F> ExprKindVisitor<'a, SE, SE2>
-    for TraverseRefMaybeBinderVisitor<F>
-where
-    SE: 'a,
-    F: FnMut(Option<&'a Label>, &'a SE) -> Result<SE2, Err>,
-{
-    type Error = Err;
-
-    fn visit_subexpr(&mut self, subexpr: &'a SE) -> Result<SE2, Self::Error> {
-        (self.0)(None, subexpr)
-    }
-    fn visit_subexpr_under_binder(
-        mut self,
-        label: &'a Label,
-        subexpr: &'a SE,
-    ) -> Result<SE2, Self::Error> {
-        (self.0)(Some(label), subexpr)
-    }
-}
-- 
cgit v1.3.1


From 40bee3cdcb9ac0c76996feeceb6ca160a6bd8b42 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 11 Feb 2020 19:04:44 +0000
Subject: Introduce LitKind to factor out common enum nodes

---
 dhall/src/semantics/builtins.rs      | 119 ++++++++++++++++++-----------------
 dhall/src/semantics/nze/normalize.rs |  86 +++++++++++++------------
 dhall/src/semantics/nze/value.rs     |  21 ++-----
 dhall/src/semantics/tck/typecheck.rs |  16 +++--
 dhall/src/syntax/ast/expr.rs         |  22 ++++---
 dhall/src/syntax/ast/visitor.rs      |   5 +-
 dhall/src/syntax/binary/decode.rs    |  18 +++---
 dhall/src/syntax/binary/encode.rs    |   9 +--
 dhall/src/syntax/text/parser.rs      |  11 ++--
 dhall/src/syntax/text/printer.rs     |  30 ++++++---
 serde_dhall/src/serde.rs             |  11 ++--
 11 files changed, 185 insertions(+), 163 deletions(-)

(limited to 'dhall/src/syntax')

diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index cbb5a6e..752b25c 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -5,7 +5,8 @@ use crate::syntax::map::DupTreeMap;
 use crate::syntax::Const::Type;
 use crate::syntax::{
     BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText,
-    InterpolatedTextContents, Label, NaiveDouble, Span, UnspannedExpr, V,
+    InterpolatedTextContents, Label, LitKind, NaiveDouble, Span, UnspannedExpr,
+    V,
 };
 use crate::Normalized;
 use std::collections::HashMap;
@@ -240,7 +241,7 @@ macro_rules! make_closure {
         rc(ExprKind::BinOp(
             BinOp::NaturalPlus,
             make_closure!($($v)*),
-            rc(ExprKind::NaturalLit(1))
+            rc(ExprKind::Lit(LitKind::Natural(1)))
         ))
     };
     ([ $($head:tt)* ] # $($tail:tt)*) => {{
@@ -256,7 +257,7 @@ macro_rules! make_closure {
 
 #[allow(clippy::cognitive_complexity)]
 fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
-    use Builtin::*;
+    use LitKind::{Bool, Double, Integer, Natural};
     use ValueKind::*;
 
     // Small helper enum
@@ -272,38 +273,40 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
     };
 
     let ret = match (b, args.as_slice()) {
-        (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
-        (NaturalIsZero, [n]) => match &*n.kind() {
-            NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)),
+        (Builtin::OptionalNone, [t]) => {
+            Ret::ValueKind(EmptyOptionalLit(t.clone()))
+        }
+        (Builtin::NaturalIsZero, [n]) => match &*n.kind() {
+            Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n == 0))),
             _ => Ret::DoneAsIs,
         },
-        (NaturalEven, [n]) => match &*n.kind() {
-            NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)),
+        (Builtin::NaturalEven, [n]) => match &*n.kind() {
+            Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n % 2 == 0))),
             _ => Ret::DoneAsIs,
         },
-        (NaturalOdd, [n]) => match &*n.kind() {
-            NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)),
+        (Builtin::NaturalOdd, [n]) => match &*n.kind() {
+            Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n % 2 != 0))),
             _ => Ret::DoneAsIs,
         },
-        (NaturalToInteger, [n]) => match &*n.kind() {
-            NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)),
+        (Builtin::NaturalToInteger, [n]) => match &*n.kind() {
+            Lit(Natural(n)) => Ret::ValueKind(Lit(Integer(*n as isize))),
             _ => Ret::DoneAsIs,
         },
-        (NaturalShow, [n]) => match &*n.kind() {
-            NaturalLit(n) => Ret::Value(Value::from_text(n)),
+        (Builtin::NaturalShow, [n]) => match &*n.kind() {
+            Lit(Natural(n)) => Ret::Value(Value::from_text(n)),
             _ => Ret::DoneAsIs,
         },
-        (NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
-            (NaturalLit(a), NaturalLit(b)) => {
-                Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 }))
+        (Builtin::NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
+            (Lit(Natural(a)), Lit(Natural(b))) => {
+                Ret::ValueKind(Lit(Natural(if b > a { b - a } else { 0 })))
             }
-            (NaturalLit(0), _) => Ret::Value(b.clone()),
-            (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
-            _ if a == b => Ret::ValueKind(NaturalLit(0)),
+            (Lit(Natural(0)), _) => Ret::Value(b.clone()),
+            (_, Lit(Natural(0))) => Ret::ValueKind(Lit(Natural(0))),
+            _ if a == b => Ret::ValueKind(Lit(Natural(0))),
             _ => Ret::DoneAsIs,
         },
-        (IntegerShow, [n]) => match &*n.kind() {
-            IntegerLit(n) => {
+        (Builtin::IntegerShow, [n]) => match &*n.kind() {
+            Lit(Integer(n)) => {
                 let s = if *n < 0 {
                     n.to_string()
                 } else {
@@ -313,27 +316,27 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
             }
             _ => Ret::DoneAsIs,
         },
-        (IntegerToDouble, [n]) => match &*n.kind() {
-            IntegerLit(n) => {
-                Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64)))
+        (Builtin::IntegerToDouble, [n]) => match &*n.kind() {
+            Lit(Integer(n)) => {
+                Ret::ValueKind(Lit(Double(NaiveDouble::from(*n as f64))))
             }
             _ => Ret::DoneAsIs,
         },
-        (IntegerNegate, [n]) => match &*n.kind() {
-            IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)),
+        (Builtin::IntegerNegate, [n]) => match &*n.kind() {
+            Lit(Integer(n)) => Ret::ValueKind(Lit(Integer(-n))),
             _ => Ret::DoneAsIs,
         },
-        (IntegerClamp, [n]) => match &*n.kind() {
-            IntegerLit(n) => {
-                Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0)))
+        (Builtin::IntegerClamp, [n]) => match &*n.kind() {
+            Lit(Integer(n)) => {
+                Ret::ValueKind(Lit(Natural((*n).try_into().unwrap_or(0))))
             }
             _ => Ret::DoneAsIs,
         },
-        (DoubleShow, [n]) => match &*n.kind() {
-            DoubleLit(n) => Ret::Value(Value::from_text(n)),
+        (Builtin::DoubleShow, [n]) => match &*n.kind() {
+            Lit(Double(n)) => Ret::Value(Value::from_text(n)),
             _ => Ret::DoneAsIs,
         },
-        (TextShow, [v]) => match &*v.kind() {
+        (Builtin::TextShow, [v]) => match &*v.kind() {
             TextLit(tlit) => {
                 if let Some(s) = tlit.as_text() {
                     // Printing InterpolatedText takes care of all the escaping
@@ -347,38 +350,41 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
             }
             _ => Ret::DoneAsIs,
         },
-        (ListLength, [_, l]) => match &*l.kind() {
-            EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)),
-            NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())),
+        (Builtin::ListLength, [_, l]) => match &*l.kind() {
+            EmptyListLit(_) => Ret::ValueKind(Lit(Natural(0))),
+            NEListLit(xs) => Ret::ValueKind(Lit(Natural(xs.len()))),
             _ => Ret::DoneAsIs,
         },
-        (ListHead, [_, l]) => match &*l.kind() {
+        (Builtin::ListHead, [_, l]) => match &*l.kind() {
             EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
             NEListLit(xs) => {
                 Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
             }
             _ => Ret::DoneAsIs,
         },
-        (ListLast, [_, l]) => match &*l.kind() {
+        (Builtin::ListLast, [_, l]) => match &*l.kind() {
             EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
             NEListLit(xs) => Ret::ValueKind(NEOptionalLit(
                 xs.iter().rev().next().unwrap().clone(),
             )),
             _ => Ret::DoneAsIs,
         },
-        (ListReverse, [_, l]) => match &*l.kind() {
+        (Builtin::ListReverse, [_, l]) => match &*l.kind() {
             EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())),
             NEListLit(xs) => {
                 Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect()))
             }
             _ => Ret::DoneAsIs,
         },
-        (ListIndexed, [t, l]) => {
+        (Builtin::ListIndexed, [t, l]) => {
             match l.kind() {
                 EmptyListLit(_) | NEListLit(_) => {
                     // Construct the returned record type: { index: Natural, value: t }
                     let mut kts = HashMap::new();
-                    kts.insert("index".into(), Value::from_builtin(Natural));
+                    kts.insert(
+                        "index".into(),
+                        Value::from_builtin(Builtin::Natural),
+                    );
                     kts.insert("value".into(), t.clone());
                     let t = Value::from_kind(RecordType(kts));
 
@@ -392,7 +398,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
                                     let mut kvs = HashMap::new();
                                     kvs.insert(
                                         "index".into(),
-                                        Value::from_kind(NaturalLit(i)),
+                                        Value::from_kind(Lit(Natural(i))),
                                     );
                                     kvs.insert("value".into(), e.clone());
                                     Value::from_kind(RecordLit(kvs))
@@ -406,8 +412,8 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
                 _ => Ret::DoneAsIs,
             }
         }
-        (ListBuild, [t, f]) => {
-            let list_t = Value::from_builtin(List).app(t.clone());
+        (Builtin::ListBuild, [t, f]) => {
+            let list_t = Value::from_builtin(Builtin::List).app(t.clone());
             Ret::Value(
                 f.app(list_t.clone())
                     .app(
@@ -422,7 +428,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
                     .app(EmptyListLit(t.clone()).into_value()),
             )
         }
-        (ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
+        (Builtin::ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
             EmptyListLit(_) => Ret::Value(nil.clone()),
             NEListLit(xs) => {
                 let mut v = nil.clone();
@@ -433,8 +439,9 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
             }
             _ => Ret::DoneAsIs,
         },
-        (OptionalBuild, [t, f]) => {
-            let optional_t = Value::from_builtin(Optional).app(t.clone());
+        (Builtin::OptionalBuild, [t, f]) => {
+            let optional_t =
+                Value::from_builtin(Builtin::Optional).app(t.clone());
             Ret::Value(
                 f.app(optional_t.clone())
                     .app(
@@ -448,25 +455,25 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
                     .app(EmptyOptionalLit(t.clone()).into_value()),
             )
         }
-        (OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
+        (Builtin::OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
             EmptyOptionalLit(_) => Ret::Value(nothing.clone()),
             NEOptionalLit(x) => Ret::Value(just.app(x.clone())),
             _ => Ret::DoneAsIs,
         },
-        (NaturalBuild, [f]) => Ret::Value(
-            f.app(Value::from_builtin(Natural))
+        (Builtin::NaturalBuild, [f]) => Ret::Value(
+            f.app(Value::from_builtin(Builtin::Natural))
                 .app(make_closure(make_closure!(
                     λ(x : Natural) ->
                     1 + var(x)
                 )))
-                .app(NaturalLit(0).into_value()),
+                .app(Lit(Natural(0)).into_value()),
         ),
 
-        (NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
-            NaturalLit(0) => Ret::Value(zero.clone()),
-            NaturalLit(n) => {
-                let fold = Value::from_builtin(NaturalFold)
-                    .app(NaturalLit(n - 1).into_value())
+        (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
+            Lit(Natural(0)) => Ret::Value(zero.clone()),
+            Lit(Natural(n)) => {
+                let fold = Value::from_builtin(Builtin::NaturalFold)
+                    .app(Lit(Natural(n - 1)).into_value())
                     .app(t.clone())
                     .app(succ.clone())
                     .app(zero.clone());
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 03b91a5..4111190 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -5,7 +5,9 @@ use crate::semantics::NzEnv;
 use crate::semantics::{
     Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind,
 };
-use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
+use crate::syntax::{
+    BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind,
+};
 
 pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind {
     match f.kind() {
@@ -98,40 +100,44 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
         NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
         RightBiasedRecordMerge, TextAppend,
     };
-    use ValueKind::{
-        BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
-    };
+    use LitKind::{Bool, Natural};
+    use ValueKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType};
+
     Some(match (o, x.kind(), y.kind()) {
-        (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
-        (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
-        (BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)),
-        (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(BoolLit(false)),
+        (BoolAnd, Lit(Bool(true)), _) => Ret::ValueRef(y),
+        (BoolAnd, _, Lit(Bool(true))) => Ret::ValueRef(x),
+        (BoolAnd, Lit(Bool(false)), _) => Ret::ValueKind(Lit(Bool(false))),
+        (BoolAnd, _, Lit(Bool(false))) => Ret::ValueKind(Lit(Bool(false))),
         (BoolAnd, _, _) if x == y => Ret::ValueRef(x),
-        (BoolOr, BoolLit(true), _) => Ret::ValueKind(BoolLit(true)),
-        (BoolOr, _, BoolLit(true)) => Ret::ValueKind(BoolLit(true)),
-        (BoolOr, BoolLit(false), _) => Ret::ValueRef(y),
-        (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x),
+        (BoolOr, Lit(Bool(true)), _) => Ret::ValueKind(Lit(Bool(true))),
+        (BoolOr, _, Lit(Bool(true))) => Ret::ValueKind(Lit(Bool(true))),
+        (BoolOr, Lit(Bool(false)), _) => Ret::ValueRef(y),
+        (BoolOr, _, Lit(Bool(false))) => Ret::ValueRef(x),
         (BoolOr, _, _) if x == y => Ret::ValueRef(x),
-        (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y),
-        (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x),
-        (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x == y)),
-        (BoolEQ, _, _) if x == y => Ret::ValueKind(BoolLit(true)),
-        (BoolNE, BoolLit(false), _) => Ret::ValueRef(y),
-        (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x),
-        (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)),
-        (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)),
+        (BoolEQ, Lit(Bool(true)), _) => Ret::ValueRef(y),
+        (BoolEQ, _, Lit(Bool(true))) => Ret::ValueRef(x),
+        (BoolEQ, Lit(Bool(x)), Lit(Bool(y))) => {
+            Ret::ValueKind(Lit(Bool(x == y)))
+        }
+        (BoolEQ, _, _) if x == y => Ret::ValueKind(Lit(Bool(true))),
+        (BoolNE, Lit(Bool(false)), _) => Ret::ValueRef(y),
+        (BoolNE, _, Lit(Bool(false))) => Ret::ValueRef(x),
+        (BoolNE, Lit(Bool(x)), Lit(Bool(y))) => {
+            Ret::ValueKind(Lit(Bool(x != y)))
+        }
+        (BoolNE, _, _) if x == y => Ret::ValueKind(Lit(Bool(false))),
 
-        (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
-        (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
-        (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
-            Ret::ValueKind(NaturalLit(x + y))
-        }
-        (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)),
-        (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
-        (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
-        (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
-        (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
-            Ret::ValueKind(NaturalLit(x * y))
+        (NaturalPlus, Lit(Natural(0)), _) => Ret::ValueRef(y),
+        (NaturalPlus, _, Lit(Natural(0))) => Ret::ValueRef(x),
+        (NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => {
+            Ret::ValueKind(Lit(Natural(x + y)))
+        }
+        (NaturalTimes, Lit(Natural(0)), _) => Ret::ValueKind(Lit(Natural(0))),
+        (NaturalTimes, _, Lit(Natural(0))) => Ret::ValueKind(Lit(Natural(0))),
+        (NaturalTimes, Lit(Natural(1)), _) => Ret::ValueRef(y),
+        (NaturalTimes, _, Lit(Natural(1))) => Ret::ValueRef(x),
+        (NaturalTimes, Lit(Natural(x)), Lit(Natural(y))) => {
+            Ret::ValueKind(Lit(Natural(x * y)))
         }
 
         (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
@@ -217,10 +223,11 @@ pub(crate) fn normalize_one_layer(
     expr: ExprKind<Value>,
     env: &NzEnv,
 ) -> ValueKind {
+    use LitKind::Bool;
     use ValueKind::{
-        BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit,
-        NEListLit, NEOptionalLit, NaturalLit, PartialExpr, RecordLit,
-        RecordType, UnionConstructor, UnionLit, UnionType,
+        EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit,
+        PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
+        UnionType,
     };
 
     let ret = match expr {
@@ -240,10 +247,7 @@ pub(crate) fn normalize_one_layer(
         ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)),
         ExprKind::Assert(_) => Ret::Expr(expr),
         ExprKind::App(v, a) => Ret::Value(v.app(a)),
-        ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)),
-        ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)),
-        ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)),
-        ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
+        ExprKind::Lit(l) => Ret::ValueKind(Lit(l.clone())),
         ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
         ExprKind::EmptyListLit(t) => {
             let arg = match t.kind() {
@@ -279,12 +283,12 @@ pub(crate) fn normalize_one_layer(
         }
         ExprKind::BoolIf(ref b, ref e1, ref e2) => {
             match b.kind() {
-                BoolLit(true) => Ret::ValueRef(e1),
-                BoolLit(false) => Ret::ValueRef(e2),
+                Lit(Bool(true)) => Ret::ValueRef(e1),
+                Lit(Bool(false)) => Ret::ValueRef(e2),
                 _ => {
                     match (e1.kind(), e2.kind()) {
                         // Simplify `if b then True else False`
-                        (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
+                        (Lit(Bool(true)), Lit(Bool(false))) => Ret::ValueRef(b),
                         _ if e1 == e2 => Ret::ValueRef(e1),
                         _ => Ret::Expr(expr),
                     }
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 0df3c74..2ae6852 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -9,8 +9,8 @@ use crate::semantics::{
     TyExpr, VarEnv,
 };
 use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
-    NaiveDouble, Natural, Span,
+    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
+    Span,
 };
 use crate::{NormalizedExpr, ToExprOptions};
 
@@ -76,10 +76,7 @@ pub(crate) enum ValueKind {
 
     Var(NzVar),
     Const(Const),
-    BoolLit(bool),
-    NaturalLit(Natural),
-    IntegerLit(Integer),
-    DoubleLit(NaiveDouble),
+    Lit(LitKind),
     EmptyOptionalLit(Value),
     NEOptionalLit(Value),
     // EmptyListLit(t) means `[] : List t`, not `[] : t`
@@ -205,10 +202,7 @@ impl Value {
                     closure.to_hir(venv),
                 ),
                 ValueKind::Const(c) => ExprKind::Const(*c),
-                ValueKind::BoolLit(b) => ExprKind::BoolLit(*b),
-                ValueKind::NaturalLit(n) => ExprKind::NaturalLit(*n),
-                ValueKind::IntegerLit(n) => ExprKind::IntegerLit(*n),
-                ValueKind::DoubleLit(n) => ExprKind::DoubleLit(*n),
+                ValueKind::Lit(l) => ExprKind::Lit(l.clone()),
                 ValueKind::EmptyOptionalLit(n) => ExprKind::App(
                     Value::from_builtin(Builtin::OptionalNone).to_hir(venv),
                     n.to_hir(venv),
@@ -317,12 +311,7 @@ impl ValueKind {
 
     pub(crate) fn normalize(&self) {
         match self {
-            ValueKind::Var(..)
-            | ValueKind::Const(_)
-            | ValueKind::BoolLit(_)
-            | ValueKind::NaturalLit(_)
-            | ValueKind::IntegerLit(_)
-            | ValueKind::DoubleLit(_) => {}
+            ValueKind::Var(..) | ValueKind::Const(_) | ValueKind::Lit(_) => {}
 
             ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
                 tth.normalize();
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index f9ff3d3..c52cfda 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -9,7 +9,7 @@ use crate::semantics::{
     TyExpr, TyExprKind, Type, Value, ValueKind,
 };
 use crate::syntax::{
-    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Span,
+    BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
 };
 
 fn type_of_recordtype<'a>(
@@ -115,10 +115,16 @@ fn type_one_layer(
             let t_tyexpr = typecheck(&t_hir)?;
             t_tyexpr.eval(env)
         }
-        ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool),
-        ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural),
-        ExprKind::IntegerLit(_) => Value::from_builtin(Builtin::Integer),
-        ExprKind::DoubleLit(_) => Value::from_builtin(Builtin::Double),
+        ExprKind::Lit(LitKind::Bool(_)) => Value::from_builtin(Builtin::Bool),
+        ExprKind::Lit(LitKind::Natural(_)) => {
+            Value::from_builtin(Builtin::Natural)
+        }
+        ExprKind::Lit(LitKind::Integer(_)) => {
+            Value::from_builtin(Builtin::Integer)
+        }
+        ExprKind::Lit(LitKind::Double(_)) => {
+            Value::from_builtin(Builtin::Double)
+        }
         ExprKind::TextLit(interpolated) => {
             let text_type = Value::from_builtin(Builtin::Text);
             for contents in interpolated.iter() {
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 512010a..18ec9fd 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -103,6 +103,19 @@ pub struct Expr {
 
 pub type UnspannedExpr = ExprKind<Expr>;
 
+/// Simple literals
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub enum LitKind {
+    ///  `True`
+    Bool(bool),
+    ///  `1`
+    Natural(Natural),
+    ///  `+2`
+    Integer(Integer),
+    ///  `3.24`
+    Double(Double),
+}
+
 /// Syntax tree for expressions
 // Having the recursion out of the enum definition enables writing
 // much more generic code and improves pattern-matching behind
@@ -110,6 +123,7 @@ pub type UnspannedExpr = ExprKind<Expr>;
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum ExprKind<SubExpr> {
     Const(Const),
+    Lit(LitKind),
     ///  `x`
     ///  `x@n`
     Var(V),
@@ -131,16 +145,8 @@ pub enum ExprKind<SubExpr> {
     Builtin(Builtin),
     // Binary operations
     BinOp(BinOp, SubExpr, SubExpr),
-    ///  `True`
-    BoolLit(bool),
     ///  `if x then y else z`
     BoolIf(SubExpr, SubExpr, SubExpr),
-    ///  `1`
-    NaturalLit(Natural),
-    ///  `+2`
-    IntegerLit(Integer),
-    ///  `3.24`
-    DoubleLit(Double),
     ///  `"Some ${interpolated} text"`
     TextLit(InterpolatedText<SubExpr>),
     ///  `[] : t`
diff --git a/dhall/src/syntax/ast/visitor.rs b/dhall/src/syntax/ast/visitor.rs
index 39959ac..c361bc1 100644
--- a/dhall/src/syntax/ast/visitor.rs
+++ b/dhall/src/syntax/ast/visitor.rs
@@ -91,10 +91,7 @@ where
         Annot(x, t) => Annot(expr!(x)?, expr!(t)?),
         Const(k) => Const(*k),
         Builtin(v) => Builtin(*v),
-        BoolLit(b) => BoolLit(*b),
-        NaturalLit(n) => NaturalLit(*n),
-        IntegerLit(n) => IntegerLit(*n),
-        DoubleLit(n) => DoubleLit(*n),
+        Lit(l) => Lit(l.clone()),
         TextLit(t) => TextLit(t.traverse_ref(|e| expr!(e))?),
         BinOp(o, x, y) => BinOp(*o, expr!(x)?, expr!(y)?),
         BoolIf(b, t, f) => BoolIf(expr!(b)?, expr!(t)?, expr!(f)?),
diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs
index 6fbcc10..2e50d61 100644
--- a/dhall/src/syntax/binary/decode.rs
+++ b/dhall/src/syntax/binary/decode.rs
@@ -6,8 +6,8 @@ use crate::error::DecodeError;
 use crate::syntax;
 use crate::syntax::{
     Expr, ExprKind, FilePath, FilePrefix, Hash, ImportLocation, ImportMode,
-    Integer, InterpolatedText, Label, Natural, Scheme, Span, UnspannedExpr,
-    URL, V,
+    Integer, InterpolatedText, Label, LitKind, Natural, Scheme, Span,
+    UnspannedExpr, URL, V,
 };
 use crate::DecodedExpr;
 
@@ -31,8 +31,8 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
         String(s) => match Builtin::parse(s) {
             Some(b) => ExprKind::Builtin(b),
             None => match s.as_str() {
-                "True" => BoolLit(true),
-                "False" => BoolLit(false),
+                "True" => Lit(LitKind::Bool(true)),
+                "False" => Lit(LitKind::Bool(false)),
                 "Type" => Const(Const::Type),
                 "Kind" => Const(Const::Kind),
                 "Sort" => Const(Const::Sort),
@@ -40,8 +40,8 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
             },
         },
         U64(n) => Var(V(Label::from("_"), *n as usize)),
-        F64(x) => DoubleLit((*x).into()),
-        Bool(b) => BoolLit(*b),
+        F64(x) => Lit(LitKind::Double((*x).into())),
+        Bool(b) => Lit(LitKind::Bool(*b)),
         Array(vec) => match vec.as_slice() {
             [String(l), U64(n)] => {
                 if l.as_str() == "_" {
@@ -216,9 +216,9 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
                 let z = cbor_value_to_dhall(&z)?;
                 BoolIf(x, y, z)
             }
-            [U64(15), U64(x)] => NaturalLit(*x as Natural),
-            [U64(16), U64(x)] => IntegerLit(*x as Integer),
-            [U64(16), I64(x)] => IntegerLit(*x as Integer),
+            [U64(15), U64(x)] => Lit(LitKind::Natural(*x as Natural)),
+            [U64(16), U64(x)] => Lit(LitKind::Integer(*x as Integer)),
+            [U64(16), I64(x)] => Lit(LitKind::Integer(*x as Integer)),
             [U64(18), String(first), rest @ ..] => {
                 TextLit(InterpolatedText::from((
                     first.clone(),
diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs
index 686f737..291ac4a 100644
--- a/dhall/src/syntax/binary/encode.rs
+++ b/dhall/src/syntax/binary/encode.rs
@@ -46,6 +46,7 @@ where
     use std::iter::once;
     use syntax::Builtin;
     use syntax::ExprKind::*;
+    use syntax::LitKind::*;
 
     use self::Serialize::{RecordMap, UnionMap};
     fn expr(x: &Expr) -> self::Serialize<'_> {
@@ -60,10 +61,10 @@ where
     match e.as_ref() {
         Const(c) => ser.serialize_str(&c.to_string()),
         Builtin(b) => ser.serialize_str(&b.to_string()),
-        BoolLit(b) => ser.serialize_bool(*b),
-        NaturalLit(n) => ser_seq!(ser; tag(15), U64(*n as u64)),
-        IntegerLit(n) => ser_seq!(ser; tag(16), I64(*n as i64)),
-        DoubleLit(n) => {
+        Lit(Bool(b)) => ser.serialize_bool(*b),
+        Lit(Natural(n)) => ser_seq!(ser; tag(15), U64(*n as u64)),
+        Lit(Integer(n)) => ser_seq!(ser; tag(16), I64(*n as i64)),
+        Lit(Double(n)) => {
             let n: f64 = (*n).into();
             ser.serialize_f64(n)
         }
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index 0ff1363..f3ebd2b 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -7,6 +7,7 @@ use pest_consume::{match_nodes, Parser};
 
 use crate::syntax::map::{DupTreeMap, DupTreeSet};
 use crate::syntax::ExprKind::*;
+use crate::syntax::LitKind::*;
 use crate::syntax::{
     Double, Expr, FilePath, FilePrefix, Hash, ImportLocation, ImportMode,
     Integer, InterpolatedText, InterpolatedTextContents, Label, NaiveDouble,
@@ -344,8 +345,8 @@ impl DhallParser {
         let e = match crate::syntax::Builtin::parse(s) {
             Some(b) => Builtin(b),
             None => match s {
-                "True" => BoolLit(true),
-                "False" => BoolLit(false),
+                "True" => Lit(Bool(true)),
+                "False" => Lit(Bool(false)),
                 "Type" => Const(crate::syntax::Const::Type),
                 "Kind" => Const(crate::syntax::Const::Kind),
                 "Sort" => Const(crate::syntax::Const::Sort),
@@ -833,9 +834,9 @@ impl DhallParser {
     #[alias(expression, shortcut = true)]
     fn primitive_expression(input: ParseInput) -> ParseResult<Expr> {
         Ok(match_nodes!(input.children();
-            [double_literal(n)] => spanned(input, DoubleLit(n)),
-            [natural_literal(n)] => spanned(input, NaturalLit(n)),
-            [integer_literal(n)] => spanned(input, IntegerLit(n)),
+            [double_literal(n)] => spanned(input, Lit(Double(n))),
+            [natural_literal(n)] => spanned(input, Lit(Natural(n))),
+            [integer_literal(n)] => spanned(input, Lit(Integer(n))),
             [double_quote_literal(s)] => spanned(input, TextLit(s)),
             [single_quote_literal(s)] => spanned(input, TextLit(s)),
             [record_type_or_literal(e)] => spanned(input, e),
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index d1c9588..8891d41 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -196,15 +196,7 @@ impl<SE: Display + Clone> Display for ExprKind<SE> {
             Var(a) => a.fmt(f)?,
             Const(k) => k.fmt(f)?,
             Builtin(v) => v.fmt(f)?,
-            BoolLit(true) => f.write_str("True")?,
-            BoolLit(false) => f.write_str("False")?,
-            NaturalLit(a) => a.fmt(f)?,
-            IntegerLit(a) if *a >= 0 => {
-                f.write_str("+")?;
-                a.fmt(f)?;
-            }
-            IntegerLit(a) => a.fmt(f)?,
-            DoubleLit(a) => a.fmt(f)?,
+            Lit(a) => a.fmt(f)?,
             TextLit(a) => a.fmt(f)?,
             RecordType(a) if a.is_empty() => f.write_str("{}")?,
             RecordType(a) => fmt_list("{ ", ", ", " }", a, f, |(k, t), f| {
@@ -239,7 +231,25 @@ impl<SE: Display + Clone> Display for ExprKind<SE> {
 
 impl Display for Expr {
     fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
-        self.as_ref().fmt_phase(f, PrintPhase::Base)
+        self.kind().fmt_phase(f, PrintPhase::Base)
+    }
+}
+
+impl Display for LitKind {
+    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+        use LitKind::*;
+        match self {
+            Bool(true) => f.write_str("True")?,
+            Bool(false) => f.write_str("False")?,
+            Natural(a) => a.fmt(f)?,
+            Integer(a) if *a >= 0 => {
+                f.write_str("+")?;
+                a.fmt(f)?;
+            }
+            Integer(a) => a.fmt(f)?,
+            Double(a) => a.fmt(f)?,
+        }
+        Ok(())
     }
 }
 
diff --git a/serde_dhall/src/serde.rs b/serde_dhall/src/serde.rs
index 92a0015..160392d 100644
--- a/serde_dhall/src/serde.rs
+++ b/serde_dhall/src/serde.rs
@@ -4,7 +4,7 @@ use serde::de::value::{
     MapAccessDeserializer, MapDeserializer, SeqDeserializer,
 };
 
-use dhall::syntax::ExprKind;
+use dhall::syntax::{ExprKind, LitKind};
 use dhall::NormalizedExpr;
 
 use crate::de::{Deserialize, Error, Result};
@@ -39,6 +39,7 @@ impl<'de: 'a, 'a> serde::Deserializer<'de> for Deserializer<'a> {
     {
         use std::convert::TryInto;
         use ExprKind::*;
+        use LitKind::*;
         let expr = self.0.as_ref();
         let not_serde_compatible = || {
             Err(Error::Deserialize(format!(
@@ -48,8 +49,8 @@ impl<'de: 'a, 'a> serde::Deserializer<'de> for Deserializer<'a> {
         };
 
         match expr.as_ref() {
-            BoolLit(x) => visitor.visit_bool(*x),
-            NaturalLit(x) => {
+            Lit(Bool(x)) => visitor.visit_bool(*x),
+            Lit(Natural(x)) => {
                 if let Ok(x64) = (*x).try_into() {
                     visitor.visit_u64(x64)
                 } else if let Ok(x32) = (*x).try_into() {
@@ -58,7 +59,7 @@ impl<'de: 'a, 'a> serde::Deserializer<'de> for Deserializer<'a> {
                     unimplemented!()
                 }
             }
-            IntegerLit(x) => {
+            Lit(Integer(x)) => {
                 if let Ok(x64) = (*x).try_into() {
                     visitor.visit_i64(x64)
                 } else if let Ok(x32) = (*x).try_into() {
@@ -67,7 +68,7 @@ impl<'de: 'a, 'a> serde::Deserializer<'de> for Deserializer<'a> {
                     unimplemented!()
                 }
             }
-            DoubleLit(x) => visitor.visit_f64((*x).into()),
+            Lit(Double(x)) => visitor.visit_f64((*x).into()),
             TextLit(x) => {
                 // Normal form ensures that the tail is empty.
                 assert!(x.tail().is_empty());
-- 
cgit v1.3.1


From 130de8cea49c848a06174c61c747d9414a5c71b7 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 16 Feb 2020 19:06:23 +0000
Subject: Start requiring Universe to build a Type

---
 dhall/src/semantics/nze/normalize.rs               |   2 +-
 dhall/src/semantics/tck/tyexpr.rs                  | 117 +++++++--
 dhall/src/semantics/tck/typecheck.rs               | 263 +++++++++------------
 dhall/src/syntax/ast/expr.rs                       |   7 +
 .../failure/unit/FunctionArgumentTypeNotAType.txt  |   4 +-
 .../unit/FunctionTypeArgumentTypeNotAType.txt      |   4 +-
 tests_buffer                                       |   1 +
 7 files changed, 218 insertions(+), 180 deletions(-)

(limited to 'dhall/src/syntax')

diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 0e09511..c2d2dc2 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -471,7 +471,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
                 closure: Closure::new(env, body.clone()),
             }
         }
-        HirKind::Expr(ExprKind::Let(_, None, val, body)) => {
+        HirKind::Expr(ExprKind::Let(_, _, val, body)) => {
             let val = val.eval(env);
             body.eval(env.insert_value(val, ())).kind().clone()
         }
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 4999899..3c47a81 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,8 +1,12 @@
-use crate::error::TypeError;
-use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value, ValueKind, VarEnv};
+use crate::error::{ErrorBuilder, TypeError};
+use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv};
 use crate::syntax::{Builtin, Const, Span};
 use crate::{NormalizedExpr, ToExprOptions};
 
+/// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
+#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
+pub(crate) struct Universe(u8);
+
 /// An expression representing a type
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) struct Type {
@@ -16,12 +20,64 @@ pub(crate) struct TyExpr {
     ty: Type,
 }
 
+impl Universe {
+    pub fn from_const(c: Const) -> Self {
+        Universe(match c {
+            Const::Type => 0,
+            Const::Kind => 1,
+            Const::Sort => 2,
+        })
+    }
+    pub fn as_const(self) -> Option<Const> {
+        match self.0 {
+            0 => Some(Const::Type),
+            1 => Some(Const::Kind),
+            2 => Some(Const::Sort),
+            _ => None,
+        }
+    }
+    pub fn next(self) -> Self {
+        Universe(self.0 + 1)
+    }
+    pub fn previous(self) -> Option<Self> {
+        if self.0 == 0 {
+            None
+        } else {
+            Some(Universe(self.0 - 1))
+        }
+    }
+}
+
 impl Type {
+    pub fn new(val: Value, _u: Universe) -> Self {
+        Type { val }
+    }
     pub fn from_const(c: Const) -> Self {
-        Value::from_const(c).into()
+        Self::new(Value::from_const(c), c.to_universe().next())
     }
     pub fn from_builtin(b: Builtin) -> Self {
-        Value::from_builtin(b).into()
+        use Builtin::*;
+        match b {
+            Bool | Natural | Integer | Double | Text => {}
+            _ => unreachable!("this builtin is not a type: {}", b),
+        }
+
+        Self::new(Value::from_builtin(b), Universe::from_const(Const::Type))
+    }
+
+    /// Get the type of this type
+    // TODO: avoid recomputing so much
+    pub fn ty(&self, env: &TyEnv) -> Result<Option<Const>, TypeError> {
+        Ok(self.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const())
+    }
+    /// Get the type of this type
+    // TODO: avoid recomputing so much
+    pub fn ty_univ(&self, env: &TyEnv) -> Result<Universe, TypeError> {
+        Ok(match self.ty(env)? {
+            Some(c) => c.to_universe(),
+            // TODO: hack, might explode
+            None => Const::Sort.to_universe().next(),
+        })
     }
 
     pub fn to_value(&self) -> Value {
@@ -49,9 +105,9 @@ impl Type {
 }
 
 impl TyExpr {
-    pub fn new(kind: HirKind, ty: Type, span: Span) -> Self {
+    pub fn from_hir(hir: &Hir, ty: Type) -> Self {
         TyExpr {
-            hir: Hir::new(kind, span),
+            hir: hir.clone(),
             ty,
         }
     }
@@ -62,16 +118,6 @@ impl TyExpr {
     pub fn ty(&self) -> &Type {
         &self.ty
     }
-    /// Get the kind (the type of the type) of this value
-    // TODO: avoid recomputing so much
-    pub fn get_kind(&self, env: &TyEnv) -> Result<Option<Const>, TypeError> {
-        Ok(self
-            .ty()
-            .to_hir(env.as_varenv())
-            .typecheck(env)?
-            .ty()
-            .as_const())
-    }
 
     pub fn to_hir(&self) -> Hir {
         self.as_hir().clone()
@@ -79,18 +125,51 @@ impl TyExpr {
     pub fn as_hir(&self) -> &Hir {
         &self.hir
     }
-    /// Converts a value back to the corresponding AST expression.
+    /// Converts a closed expression back to the corresponding AST expression.
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         self.as_hir().to_expr(opts)
     }
+    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+        self.as_hir().to_expr_tyenv(env)
+    }
 
     /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
     pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
         self.as_hir().eval(env.into())
     }
+    pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
+        if self.ty().as_const().is_none() {
+            return mkerr(
+                ErrorBuilder::new(format!(
+                    "Expected a type, found: `{}`",
+                    self.to_expr_tyenv(env),
+                ))
+                .span_err(
+                    self.span(),
+                    format!(
+                        "this has type: `{}`",
+                        self.ty().to_expr_tyenv(env)
+                    ),
+                )
+                .help(format!(
+                    "An expression in type position must have type `Type`, \
+                     `Kind` or `Sort`",
+                ))
+                .format(),
+            );
+        }
+        Ok(())
+    }
     /// Evaluate to a Type.
-    pub fn eval_to_type(&self, env: impl Into<NzEnv>) -> Type {
-        self.eval(env).into()
+    pub fn eval_to_type(&self, env: &TyEnv) -> Result<Type, TypeError> {
+        self.ensure_is_type(env)?;
+        Ok(Type::new(
+            self.eval(env),
+            self.ty()
+                .as_const()
+                .expect("case handled in ensure_is_type")
+                .to_universe(),
+        ))
     }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index dd996ae..1281045 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -15,8 +15,8 @@ use crate::syntax::{
 fn check_rectymerge(
     span: &Span,
     env: &TyEnv,
-    x: Type,
-    y: Type,
+    x: Value,
+    y: Value,
 ) -> Result<(), TypeError> {
     let kts_x = match x.kind() {
         ValueKind::RecordType(kts) => kts,
@@ -39,7 +39,7 @@ fn check_rectymerge(
     for (k, tx) in kts_x {
         if let Some(ty) = kts_y.get(k) {
             // TODO: store Type in RecordType ?
-            check_rectymerge(span, env, tx.clone().into(), ty.clone().into())?;
+            check_rectymerge(span, env, tx.clone(), ty.clone())?;
         }
     }
     Ok(())
@@ -70,9 +70,8 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
 fn type_one_layer(
     env: &TyEnv,
     ekind: ExprKind<TyExpr>,
-    annot: Option<Type>,
     span: Span,
-) -> Result<TyExpr, TypeError> {
+) -> Result<Type, TypeError> {
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
 
     let ty = match &ekind {
@@ -81,84 +80,19 @@ fn type_one_layer(
         }
         ExprKind::Var(..)
         | ExprKind::Const(Const::Sort)
+        | ExprKind::Lam(..)
+        | ExprKind::Pi(..)
+        | ExprKind::Let(..)
         | ExprKind::Annot(..) => {
             unreachable!("This case should have been handled in type_with")
         }
 
-        ExprKind::Lam(binder, annot, body) => {
-            if annot.ty().as_const().is_none() {
-                return mkerr(
-                    ErrorBuilder::new(format!(
-                        "Invalid input type: `{}`",
-                        annot.ty().to_expr_tyenv(env),
-                    ))
-                    .span_err(
-                        annot.span(),
-                        format!(
-                            "this has type: `{}`",
-                            annot.ty().to_expr_tyenv(env)
-                        ),
-                    )
-                    .help(format!(
-                        "The input type of a function must have type `Type`, \
-                         `Kind` or `Sort`",
-                    ))
-                    .format(),
-                );
-            }
-            let body_env = env.insert_type(&binder, annot.eval_to_type(env));
-            if body.get_kind(&body_env)?.is_none() {
-                return span_err("Invalid output type");
-            }
-            Hir::new(
-                HirKind::Expr(ExprKind::Pi(
-                    binder.clone(),
-                    annot.to_hir(),
-                    body.ty().to_hir(body_env.as_varenv()),
-                )),
-                span.clone(),
-            )
-            .eval_to_type(env)
-        }
-        ExprKind::Pi(_, annot, body) => {
-            let ks = match annot.ty().as_const() {
-                Some(k) => k,
-                _ => {
-                    return mkerr(
-                        ErrorBuilder::new(format!(
-                            "Invalid input type: `{}`",
-                            annot.ty().to_expr_tyenv(env),
-                        ))
-                        .span_err(
-                            annot.span(),
-                            format!(
-                                "this has type: `{}`",
-                                annot.ty().to_expr_tyenv(env)
-                            ),
-                        )
-                        .help(format!(
-                            "The input type of a function must have type \
-                             `Type`, `Kind` or `Sort`",
-                        ))
-                        .format(),
-                    );
-                }
-            };
-            let kt = match body.ty().as_const() {
-                Some(k) => k,
-                _ => return span_err("Invalid output type"),
-            };
-
-            Type::from_const(function_check(ks, kt))
-        }
-        ExprKind::Let(_, _, _, body) => body.ty().clone(),
-
         ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
         ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
         ExprKind::Builtin(b) => {
             let t_hir = type_of_builtin(*b);
             let t_tyexpr = typecheck(&t_hir)?;
-            t_tyexpr.eval_to_type(env)
+            t_tyexpr.eval_to_type(env)?
         }
         ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
         ExprKind::Lit(LitKind::Natural(_)) => {
@@ -183,7 +117,7 @@ fn type_one_layer(
             text_type
         }
         ExprKind::EmptyListLit(t) => {
-            let t = t.eval_to_type(env);
+            let t = t.eval_to_type(env)?;
             match t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
@@ -202,7 +136,7 @@ fn type_one_layer(
                     return span_err("InvalidListElement");
                 }
             }
-            if x.get_kind(env)? != Some(Const::Type) {
+            if x.ty().ty(env)? != Some(Const::Type) {
                 return span_err("InvalidListType");
             }
 
@@ -210,7 +144,7 @@ fn type_one_layer(
             Value::from_builtin(Builtin::List).app(t).to_type()
         }
         ExprKind::SomeLit(x) => {
-            if x.get_kind(env)? != Some(Const::Type) {
+            if x.ty().ty(env)? != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
@@ -230,7 +164,7 @@ fn type_one_layer(
                 };
 
                 // Check that the fields have a valid kind
-                match v.get_kind(env)? {
+                match v.ty().ty(env)? {
                     Some(_) => {}
                     None => return span_err("InvalidFieldType"),
                 }
@@ -297,7 +231,7 @@ fn type_one_layer(
                 },
                 // TODO: branch here only when scrut.ty() is a Const
                 _ => {
-                    let scrut_nf = scrut.eval_to_type(env);
+                    let scrut_nf = scrut.eval(env);
                     match scrut_nf.kind() {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
@@ -305,13 +239,11 @@ fn type_one_layer(
                                 Value::from_kind(ValueKind::PiClosure {
                                     binder: Binder::new(x.clone()),
                                     annot: ty.clone(),
-                                    closure: Closure::new_constant(
-                                        scrut_nf.into_value(),
-                                    ),
+                                    closure: Closure::new_constant(scrut_nf),
                                 })
                                 .to_type()
                             }
-                            Some(None) => scrut_nf,
+                            Some(None) => scrut_nf.to_type(),
                             None => return span_err("MissingUnionField"),
                         },
                         _ => return span_err("NotARecord"),
@@ -320,7 +252,7 @@ fn type_one_layer(
             }
         }
         ExprKind::Assert(t) => {
-            let t = t.eval_to_type(env);
+            let t = t.eval_to_type(env)?;
             match t.kind() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => {
@@ -382,7 +314,7 @@ fn type_one_layer(
             if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
                 return span_err("InvalidPredicate");
             }
-            if y.get_kind(env)? != Some(Const::Type) {
+            if y.ty().ty(env)? != Some(Const::Type) {
                 return span_err("IfBranchMustBeTerm");
             }
             if y.ty() != z.ty() {
@@ -415,25 +347,22 @@ fn type_one_layer(
             Value::from_kind(ValueKind::RecordType(kts)).to_type()
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
-            check_rectymerge(&span, env, x.ty().clone(), y.ty().clone())?;
+            check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?;
 
-            Hir::new(
+            let hir = Hir::new(
                 HirKind::Expr(ExprKind::BinOp(
                     BinOp::RecursiveRecordTypeMerge,
                     x.ty().to_hir(env.as_varenv()),
                     y.ty().to_hir(env.as_varenv()),
                 )),
                 span.clone(),
-            )
-            .eval_to_type(env)
+            );
+            let x_u = x.ty().ty_univ(env)?;
+            let y_u = y.ty().ty_univ(env)?;
+            Type::new(hir.eval(env), max(x_u, y_u))
         }
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
-            check_rectymerge(
-                &span,
-                env,
-                x.eval_to_type(env),
-                y.eval_to_type(env),
-            )?;
+            check_rectymerge(&span, env, x.eval(env), y.eval(env))?;
 
             // A RecordType's type is always a const
             let xk = x.ty().as_const().unwrap();
@@ -459,7 +388,7 @@ fn type_one_layer(
             if l.ty() != r.ty() {
                 return span_err("EquivalenceTypeMismatch");
             }
-            if l.get_kind(env)? != Some(Const::Type) {
+            if l.ty().ty(env)? != Some(Const::Type) {
                 return span_err("EquivalenceArgumentsMustBeTerms");
             }
 
@@ -614,7 +543,10 @@ fn type_one_layer(
                 }
             }
 
-            let type_annot = type_annot.as_ref().map(|t| t.eval_to_type(env));
+            let type_annot = type_annot
+                .as_ref()
+                .map(|t| t.eval_to_type(env))
+                .transpose()?;
             match (inferred_type, type_annot) {
                 (Some(t1), Some(t2)) => {
                     if t1 != t2 {
@@ -628,7 +560,7 @@ fn type_one_layer(
             }
         }
         ExprKind::ToMap(record, annot) => {
-            if record.get_kind(env)? != Some(Const::Type) {
+            if record.ty().ty(env)? != Some(Const::Type) {
                 return span_err("`toMap` only accepts records of type `Type`");
             }
             let record_t = record.ty();
@@ -648,7 +580,7 @@ fn type_one_layer(
                          annotation",
                     );
                 };
-                let annot_val = annot.eval_to_type(env);
+                let annot_val = annot.eval_to_type(env)?;
 
                 let err_msg = "The type of `toMap x` must be of the form \
                                `List { mapKey : Text, mapValue : T }`";
@@ -693,7 +625,7 @@ fn type_one_layer(
                     .app(Value::from_kind(ValueKind::RecordType(kts)))
                     .to_type();
                 if let Some(annot) = annot {
-                    let annot_val = annot.eval_to_type(env);
+                    let annot_val = annot.eval_to_type(env)?;
                     if output_type != annot_val {
                         return span_err("Annotation mismatch");
                     }
@@ -733,7 +665,7 @@ fn type_one_layer(
                 _ => return span_err("ProjectionMustBeRecord"),
             };
 
-            let selection_val = selection.eval_to_type(env);
+            let selection_val = selection.eval_to_type(env)?;
             let sel_kts = match selection_val.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionByExprTakesRecordType"),
@@ -754,22 +686,7 @@ fn type_one_layer(
         }
     };
 
-    if let Some(annot) = annot {
-        if ty != annot {
-            return span_err(&format!(
-                "annot mismatch: {} != {}",
-                ty.to_expr_tyenv(env),
-                annot.to_expr_tyenv(env)
-            ));
-        }
-    }
-
-    // TODO: avoid retraversing
-    Ok(TyExpr::new(
-        HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())),
-        ty,
-        span,
-    ))
+    Ok(ty)
 }
 
 /// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation
@@ -779,59 +696,93 @@ pub(crate) fn type_with(
     hir: &Hir,
     annot: Option<Type>,
 ) -> Result<TyExpr, TypeError> {
-    match hir.kind() {
-        HirKind::Var(var) => {
-            Ok(TyExpr::new(HirKind::Var(*var), env.lookup(var), hir.span()))
-        }
+    let tyexpr = match hir.kind() {
+        HirKind::Var(var) => TyExpr::from_hir(hir, env.lookup(var)),
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
         HirKind::Expr(ExprKind::Const(Const::Sort)) => {
-            mk_span_err(hir.span(), "Sort does not have a type")
+            return mk_span_err(hir.span(), "Sort does not have a type")
         }
         HirKind::Expr(ExprKind::Annot(x, t)) => {
             let t = match t.kind() {
                 HirKind::Expr(ExprKind::Const(Const::Sort)) => {
                     Type::from_const(Const::Sort)
                 }
-                _ => type_with(env, t, None)?.eval_to_type(env),
+                _ => type_with(env, t, None)?.eval_to_type(env)?,
             };
-            type_with(env, x, Some(t))
+            type_with(env, x, Some(t))?
         }
-        HirKind::Expr(ekind) => {
-            let ekind = match ekind {
-                ExprKind::Lam(binder, annot, body) => {
-                    let annot = type_with(env, annot, None)?;
-                    let annot_nf = annot.eval_to_type(env);
-                    let body_env = env.insert_type(binder, annot_nf);
-                    let body = type_with(&body_env, body, None)?;
-                    ExprKind::Lam(binder.clone(), annot, body)
-                }
-                ExprKind::Pi(binder, annot, body) => {
-                    let annot = type_with(env, annot, None)?;
-                    let annot_val = annot.eval_to_type(env);
-                    let body_env = env.insert_type(binder, annot_val);
-                    let body = type_with(&body_env, body, None)?;
-                    ExprKind::Pi(binder.clone(), annot, body)
-                }
-                ExprKind::Let(binder, annot, val, body) => {
-                    let val_annot = if let Some(t) = annot {
-                        Some(type_with(env, t, None)?.eval_to_type(env))
-                    } else {
-                        None
-                    };
-                    let val = type_with(env, &val, val_annot)?;
-                    let val_nf = val.eval(env);
-                    let body_env =
-                        env.insert_value(&binder, val_nf, val.ty().clone());
-                    let body = type_with(&body_env, body, None)?;
-                    ExprKind::Let(binder.clone(), None, val, body)
-                }
-                _ => ekind.traverse_ref(|e| type_with(env, e, None))?,
+
+        HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+            let annot = type_with(env, annot, None)?;
+            let annot_nf = annot.eval_to_type(env)?;
+            let body_env = env.insert_type(binder, annot_nf);
+            let body = type_with(&body_env, body, None)?;
+
+            let u_annot = annot.ty().as_const().unwrap();
+            let u_body = match body.ty().ty(&body_env)? {
+                Some(k) => k,
+                _ => return mk_span_err(hir.span(), "Invalid output type"),
             };
-            type_one_layer(env, ekind, annot, hir.span())
+            let u = function_check(u_annot, u_body).to_universe();
+            let ty_hir = Hir::new(
+                HirKind::Expr(ExprKind::Pi(
+                    binder.clone(),
+                    annot.to_hir(),
+                    body.ty().to_hir(body_env.as_varenv()),
+                )),
+                hir.span(),
+            );
+            let ty = Type::new(ty_hir.eval(env), u);
+
+            TyExpr::from_hir(hir, ty)
+        }
+        HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+            let annot = type_with(env, annot, None)?;
+            let annot_val = annot.eval_to_type(env)?;
+            let body_env = env.insert_type(binder, annot_val);
+            let body = type_with(&body_env, body, None)?;
+            body.ensure_is_type(env)?;
+
+            let ks = annot.ty().as_const().unwrap();
+            let kt = body.ty().as_const().unwrap();
+            let ty = Type::from_const(function_check(ks, kt));
+            TyExpr::from_hir(hir, ty)
+        }
+        HirKind::Expr(ExprKind::Let(binder, annot, val, body)) => {
+            let val_annot = annot
+                .as_ref()
+                .map(|t| Ok(type_with(env, t, None)?.eval_to_type(env)?))
+                .transpose()?;
+            let val = type_with(env, &val, val_annot)?;
+            let val_nf = val.eval(env);
+            let body_env = env.insert_value(&binder, val_nf, val.ty().clone());
+            let body = type_with(&body_env, body, None)?;
+            let ty = body.ty().clone();
+            TyExpr::from_hir(hir, ty)
+        }
+        HirKind::Expr(ekind) => {
+            let ekind = ekind.traverse_ref(|e| type_with(env, e, None))?;
+            let ty = type_one_layer(env, ekind, hir.span())?;
+            TyExpr::from_hir(hir, ty)
+        }
+    };
+
+    if let Some(annot) = annot {
+        if *tyexpr.ty() != annot {
+            return mk_span_err(
+                hir.span(),
+                &format!(
+                    "annot mismatch: {} != {}",
+                    tyexpr.ty().to_expr_tyenv(env),
+                    annot.to_expr_tyenv(env)
+                ),
+            );
         }
     }
+
+    Ok(tyexpr)
 }
 
 /// Typecheck an expression and return the expression annotated with types if type-checking
@@ -842,6 +793,6 @@ pub(crate) fn typecheck(hir: &Hir) -> Result<TyExpr, TypeError> {
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
 pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<TyExpr, TypeError> {
-    let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new());
+    let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?;
     type_with(&TyEnv::new(), hir, Some(ty))
 }
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 18ec9fd..a479b53 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,3 +1,4 @@
+use crate::semantics::Universe;
 use crate::syntax::map::{DupTreeMap, DupTreeSet};
 use crate::syntax::visitor;
 use crate::syntax::*;
@@ -18,6 +19,12 @@ pub enum Const {
     Sort,
 }
 
+impl Const {
+    pub(crate) fn to_universe(self) -> Universe {
+        Universe::from_const(self)
+    }
+}
+
 /// Bound variable
 ///
 /// The `Label` field is the variable's name (i.e. \"`x`\").
diff --git a/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
index e84eb15..ca5bbcd 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionArgumentTypeNotAType.txt
@@ -1,7 +1,7 @@
-Type error: error: Invalid input type: `Natural`
+Type error: error: Expected a type, found: `1`
  --> <current file>:1:6
   |
 1 | λ(_ : 1) → _
   |       ^ this has type: `Natural`
   |
-  = help: The input type of a function must have type `Type`, `Kind` or `Sort`
+  = help: An expression in type position must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
index 4aa0f4f..168ebb9 100644
--- a/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
+++ b/dhall/tests/type-inference/failure/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -1,7 +1,7 @@
-Type error: error: Invalid input type: `Natural`
+Type error: error: Expected a type, found: `2`
  --> <current file>:1:0
   |
 1 | 2 → _
   | ^ this has type: `Natural`
   |
-  = help: The input type of a function must have type `Type`, `Kind` or `Sort`
+  = help: An expression in type position must have type `Type`, `Kind` or `Sort`
diff --git a/tests_buffer b/tests_buffer
index e8eb3d7..1c814ff 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -52,6 +52,7 @@ success/
             (λ(T : Type) → let x = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T
 failure/
     \(_: Bool) -> assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)
+    unit/FunctionTypeOutputTypeNotAType Bool -> 1
     merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
     merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
     merge { x = True, y = 1 } < x | y >.x
-- 
cgit v1.3.1


From 73571249f9bcf8efe84708a4a9f8665af62e44f0 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 17 Feb 2020 18:09:34 +0000
Subject: Remove some unused code

---
 dhall/src/syntax/ast/import.rs | 24 ------------------------
 1 file changed, 24 deletions(-)

(limited to 'dhall/src/syntax')

diff --git a/dhall/src/syntax/ast/import.rs b/dhall/src/syntax/ast/import.rs
index da3e99b..7bde6e0 100644
--- a/dhall/src/syntax/ast/import.rs
+++ b/dhall/src/syntax/ast/import.rs
@@ -75,15 +75,6 @@ impl<SE> URL<SE> {
             headers,
         })
     }
-    pub fn traverse_mut<'a, Err>(
-        &'a mut self,
-        f: impl FnOnce(&'a mut SE) -> Result<(), Err>,
-    ) -> Result<(), Err> {
-        if let Some(header) = &mut self.headers {
-            f(header)?;
-        }
-        Ok(())
-    }
 }
 
 impl<SE> ImportLocation<SE> {
@@ -99,15 +90,6 @@ impl<SE> ImportLocation<SE> {
             Missing => Missing,
         })
     }
-    pub fn traverse_mut<'a, Err>(
-        &'a mut self,
-        f: impl FnOnce(&'a mut SE) -> Result<(), Err>,
-    ) -> Result<(), Err> {
-        if let ImportLocation::Remote(url) = self {
-            url.traverse_mut(f)?;
-        }
-        Ok(())
-    }
 }
 
 impl<SE> Import<SE> {
@@ -121,10 +103,4 @@ impl<SE> Import<SE> {
             hash: self.hash.clone(),
         })
     }
-    pub fn traverse_mut<'a, Err>(
-        &'a mut self,
-        f: impl FnOnce(&'a mut SE) -> Result<(), Err>,
-    ) -> Result<(), Err> {
-        self.location.traverse_mut(f)
-    }
 }
-- 
cgit v1.3.1