Remove Value visitor

It's mostly useful when we can change types, but it's also too
constraining if we can, because then we can't enforce complex invariants
like the one for TextLit.

3 files changed, 87 insertions, 309 deletions

diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs
index e3b37cd..3d9c5eb 100644
--- a/dhall/src/semantics/nze/mod.rs
+++ b/dhall/src/semantics/nze/mod.rs
@@ -2,7 +2,6 @@ pub mod env;
 pub mod normalize;
 pub mod value;
 pub mod var;
-pub mod visitor;
 pub(crate) use env::*;
 pub(crate) use normalize::*;
 pub(crate) use value::*;
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 0a9de6a..6ab6fe3 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -3,7 +3,6 @@ use std::collections::HashMap;
 use std::rc::Rc;
 
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::nze::visitor;
 use crate::semantics::Binder;
 use crate::semantics::{apply_any, normalize_tyexpr_whnf, normalize_whnf};
 use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
@@ -276,62 +275,96 @@ impl Value {
     }
 
     pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+        let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
+            ExprKind::UnionType(
+                kts.iter()
+                    .map(|(k, v)| {
+                        (k.clone(), v.as_ref().map(|v| v.to_tyexpr(venv)))
+                    })
+                    .collect(),
+            )
+        };
+
         let tye = match &*self.kind() {
             ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
-            ValueKind::LamClosure {
-                binder,
-                annot,
-                closure,
-            } => TyExprKind::Expr(ExprKind::Lam(
-                binder.to_label(),
-                annot.to_tyexpr(venv),
-                closure.to_tyexpr(venv),
-            )),
-            ValueKind::PiClosure {
-                binder,
-                annot,
-                closure,
-            } => TyExprKind::Expr(ExprKind::Pi(
-                binder.to_label(),
-                annot.to_tyexpr(venv),
-                closure.to_tyexpr(venv),
-            )),
             ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv),
-            ValueKind::UnionConstructor(l, kts, t) => {
-                TyExprKind::Expr(ExprKind::Field(
-                    TyExpr::new(
-                        TyExprKind::Expr(ExprKind::UnionType(
-                            kts.into_iter()
-                                .map(|(k, v)| {
-                                    (
-                                        k.clone(),
-                                        v.as_ref().map(|v| v.to_tyexpr(venv)),
-                                    )
-                                })
-                                .collect(),
+            ValueKind::Thunk(th) => return th.to_tyexpr(venv),
+            self_kind => TyExprKind::Expr(match self_kind {
+                ValueKind::Var(..)
+                | ValueKind::AppliedBuiltin(..)
+                | ValueKind::Thunk(..) => unreachable!(),
+                ValueKind::LamClosure {
+                    binder,
+                    annot,
+                    closure,
+                } => ExprKind::Lam(
+                    binder.to_label(),
+                    annot.to_tyexpr(venv),
+                    closure.to_tyexpr(venv),
+                ),
+                ValueKind::PiClosure {
+                    binder,
+                    annot,
+                    closure,
+                } => ExprKind::Pi(
+                    binder.to_label(),
+                    annot.to_tyexpr(venv),
+                    closure.to_tyexpr(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::EmptyOptionalLit(n) => ExprKind::App(
+                    Value::from_builtin(Builtin::OptionalNone).to_tyexpr(venv),
+                    n.to_tyexpr(venv),
+                ),
+                ValueKind::NEOptionalLit(n) => {
+                    ExprKind::SomeLit(n.to_tyexpr(venv))
+                }
+                ValueKind::EmptyListLit(n) => {
+                    ExprKind::EmptyListLit(TyExpr::new(
+                        TyExprKind::Expr(ExprKind::App(
+                            Value::from_builtin(Builtin::List).to_tyexpr(venv),
+                            n.to_tyexpr(venv),
                         )),
+                        Some(Value::from_const(Const::Type)),
+                        Span::Artificial,
+                    ))
+                }
+                ValueKind::NEListLit(elts) => ExprKind::NEListLit(
+                    elts.iter().map(|v| v.to_tyexpr(venv)).collect(),
+                ),
+                ValueKind::TextLit(elts) => ExprKind::TextLit(
+                    elts.iter()
+                        .map(|t| t.map_ref(|v| v.to_tyexpr(venv)))
+                        .collect(),
+                ),
+                ValueKind::RecordLit(kvs) => ExprKind::RecordLit(
+                    kvs.iter()
+                        .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
+                        .collect(),
+                ),
+                ValueKind::RecordType(kts) => ExprKind::RecordType(
+                    kts.iter()
+                        .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
+                        .collect(),
+                ),
+                ValueKind::UnionType(kts) => map_uniontype(kts),
+                ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
+                    TyExpr::new(
+                        TyExprKind::Expr(map_uniontype(kts)),
                         Some(t.clone()),
                         Span::Artificial,
                     ),
                     l.clone(),
-                ))
-            }
-            ValueKind::UnionLit(l, v, kts, uniont, ctort) => {
-                TyExprKind::Expr(ExprKind::App(
+                ),
+                ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App(
                     TyExpr::new(
                         TyExprKind::Expr(ExprKind::Field(
                             TyExpr::new(
-                                TyExprKind::Expr(ExprKind::UnionType(
-                                    kts.into_iter()
-                                        .map(|(k, v)| {
-                                            (
-                                                k.clone(),
-                                                v.as_ref()
-                                                    .map(|v| v.to_tyexpr(venv)),
-                                            )
-                                        })
-                                        .collect(),
-                                )),
+                                TyExprKind::Expr(map_uniontype(kts)),
                                 Some(uniont.clone()),
                                 Span::Artificial,
                             ),
@@ -341,61 +374,14 @@ impl Value {
                         Span::Artificial,
                     ),
                     v.to_tyexpr(venv),
-                ))
-            }
-            ValueKind::Thunk(th) => return th.to_tyexpr(venv),
-            self_kind => {
-                let self_kind = self_kind.map_ref(|v| v.to_tyexpr(venv));
-                let expr = match self_kind {
-                    ValueKind::Var(..)
-                    | ValueKind::LamClosure { .. }
-                    | ValueKind::PiClosure { .. }
-                    | ValueKind::AppliedBuiltin(..)
-                    | ValueKind::UnionConstructor(..)
-                    | ValueKind::UnionLit(..)
-                    | ValueKind::Thunk(..) => unreachable!(),
-                    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::EmptyOptionalLit(n) => ExprKind::App(
-                        Value::from_builtin(Builtin::OptionalNone)
-                            .to_tyexpr(venv),
-                        n,
-                    ),
-                    ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n),
-                    ValueKind::EmptyListLit(n) => {
-                        ExprKind::EmptyListLit(TyExpr::new(
-                            TyExprKind::Expr(ExprKind::App(
-                                Value::from_builtin(Builtin::List)
-                                    .to_tyexpr(venv),
-                                n,
-                            )),
-                            Some(Value::from_const(Const::Type)),
-                            Span::Artificial,
-                        ))
-                    }
-                    ValueKind::NEListLit(elts) => ExprKind::NEListLit(elts),
-                    ValueKind::RecordLit(kvs) => {
-                        ExprKind::RecordLit(kvs.into_iter().collect())
-                    }
-                    ValueKind::RecordType(kts) => {
-                        ExprKind::RecordType(kts.into_iter().collect())
-                    }
-                    ValueKind::UnionType(kts) => {
-                        ExprKind::UnionType(kts.into_iter().collect())
-                    }
-                    ValueKind::TextLit(elts) => {
-                        ExprKind::TextLit(elts.into_iter().collect())
-                    }
-                    ValueKind::Equivalence(x, y) => {
-                        ExprKind::BinOp(BinOp::Equivalence, x, y)
-                    }
-                    ValueKind::PartialExpr(e) => e,
-                };
-                TyExprKind::Expr(expr)
-            }
+                ),
+                ValueKind::Equivalence(x, y) => ExprKind::BinOp(
+                    BinOp::Equivalence,
+                    x.to_tyexpr(venv),
+                    y.to_tyexpr(venv),
+                ),
+                ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_tyexpr(venv)),
+            }),
         };
 
         let self_ty = self.as_internal().ty.clone();
@@ -535,46 +521,6 @@ impl ValueKind<Value> {
     }
 }
 
-impl<V> ValueKind<V> {
-    fn traverse_ref_with_special_handling_of_binders<'a, V2, E>(
-        &'a self,
-        visit_val: impl FnMut(&'a V) -> Result<V2, E>,
-        visit_under_binder: impl for<'b> FnMut(
-            &'a Binder,
-            &'b V,
-            &'a V,
-        ) -> Result<V2, E>,
-    ) -> Result<ValueKind<V2>, E> {
-        use visitor::ValueKindVisitor;
-        visitor::TraverseRefWithBindersVisitor {
-            visit_val,
-            visit_under_binder,
-        }
-        .visit(self)
-    }
-
-    fn map_ref_with_special_handling_of_binders<'a, V2>(
-        &'a self,
-        mut map_val: impl FnMut(&'a V) -> V2,
-        mut map_under_binder: impl for<'b> FnMut(&'a Binder, &'b V, &'a V) -> V2,
-    ) -> ValueKind<V2> {
-        use crate::syntax::trivial_result;
-        trivial_result(self.traverse_ref_with_special_handling_of_binders(
-            |x| Ok(map_val(x)),
-            |l, t, x| Ok(map_under_binder(l, t, x)),
-        ))
-    }
-
-    fn map_ref<'a, V2>(
-        &'a self,
-        map_val: impl Fn(&'a V) -> V2,
-    ) -> ValueKind<V2> {
-        self.map_ref_with_special_handling_of_binders(&map_val, |_, _, x| {
-            map_val(x)
-        })
-    }
-}
-
 impl Thunk {
     pub fn new(env: &NzEnv, body: TyExpr) -> Self {
         Thunk {
diff --git a/dhall/src/semantics/nze/visitor.rs b/dhall/src/semantics/nze/visitor.rs
deleted file mode 100644
index d1a85d8..0000000
--- a/dhall/src/semantics/nze/visitor.rs
+++ /dev/null
@@ -1,167 +0,0 @@
-use std::iter::FromIterator;
-
-use crate::semantics::{Binder, BuiltinClosure, ValueKind};
-use crate::syntax::Label;
-
-/// A visitor trait that can be used to traverse `ValueKind`s. We need this pattern so that Rust lets
-/// us have as much mutability as we can. See the equivalent file in `crate::syntax` for more
-/// details.
-pub(crate) trait ValueKindVisitor<'a, V1, V2>: Sized {
-    type Error;
-
-    fn visit_val(&mut self, val: &'a V1) -> Result<V2, Self::Error>;
-    fn visit_binder(
-        mut self,
-        _label: &'a Binder,
-        ty: &'a V1,
-        val: &'a V1,
-    ) -> Result<(V2, V2), Self::Error> {
-        Ok((self.visit_val(ty)?, self.visit_val(val)?))
-    }
-    fn visit_vec(&mut self, x: &'a [V1]) -> Result<Vec<V2>, Self::Error> {
-        x.iter().map(|e| self.visit_val(e)).collect()
-    }
-    fn visit_opt(
-        &mut self,
-        x: &'a Option<V1>,
-    ) -> Result<Option<V2>, Self::Error> {
-        Ok(match x {
-            Some(x) => Some(self.visit_val(x)?),
-            None => None,
-        })
-    }
-    fn visit_map<T>(
-        &mut self,
-        x: impl IntoIterator<Item = (&'a Label, &'a V1)>,
-    ) -> Result<T, Self::Error>
-    where
-        V1: 'a,
-        T: FromIterator<(Label, V2)>,
-    {
-        x.into_iter()
-            .map(|(k, x)| Ok((k.clone(), self.visit_val(x)?)))
-            .collect()
-    }
-    fn visit_optmap<T>(
-        &mut self,
-        x: impl IntoIterator<Item = (&'a Label, &'a Option<V1>)>,
-    ) -> Result<T, Self::Error>
-    where
-        V1: 'a,
-        T: FromIterator<(Label, Option<V2>)>,
-    {
-        x.into_iter()
-            .map(|(k, x)| Ok((k.clone(), self.visit_opt(x)?)))
-            .collect()
-    }
-
-    fn visit(
-        self,
-        input: &'a ValueKind<V1>,
-    ) -> Result<ValueKind<V2>, Self::Error> {
-        visit_ref(self, input)
-    }
-}
-
-fn visit_ref<'a, Visitor, V1, V2>(
-    mut v: Visitor,
-    input: &'a ValueKind<V1>,
-) -> Result<ValueKind<V2>, Visitor::Error>
-where
-    Visitor: ValueKindVisitor<'a, V1, V2>,
-{
-    use ValueKind::*;
-    Ok(match input {
-        LamClosure {
-            binder,
-            annot,
-            closure,
-        } => LamClosure {
-            binder: binder.clone(),
-            annot: v.visit_val(annot)?,
-            closure: closure.clone(),
-        },
-        PiClosure {
-            binder,
-            annot,
-            closure,
-        } => PiClosure {
-            binder: binder.clone(),
-            annot: v.visit_val(annot)?,
-            closure: closure.clone(),
-        },
-        AppliedBuiltin(BuiltinClosure {
-            b,
-            args,
-            types,
-            env,
-        }) => AppliedBuiltin(BuiltinClosure {
-            b: *b,
-            args: v.visit_vec(args)?,
-            types: v.visit_vec(types)?,
-            env: env.clone(),
-        }),
-        Var(v) => Var(*v),
-        Const(k) => Const(*k),
-        BoolLit(b) => BoolLit(*b),
-        NaturalLit(n) => NaturalLit(*n),
-        IntegerLit(n) => IntegerLit(*n),
-        DoubleLit(n) => DoubleLit(*n),
-        EmptyOptionalLit(t) => EmptyOptionalLit(v.visit_val(t)?),
-        NEOptionalLit(x) => NEOptionalLit(v.visit_val(x)?),
-        EmptyListLit(t) => EmptyListLit(v.visit_val(t)?),
-        NEListLit(xs) => NEListLit(v.visit_vec(xs)?),
-        RecordType(kts) => RecordType(v.visit_map(kts)?),
-        RecordLit(kvs) => RecordLit(v.visit_map(kvs)?),
-        UnionType(kts) => UnionType(v.visit_optmap(kts)?),
-        UnionConstructor(l, kts, uniont) => UnionConstructor(
-            l.clone(),
-            v.visit_optmap(kts)?,
-            v.visit_val(uniont)?,
-        ),
-        UnionLit(l, x, kts, uniont, ctort) => UnionLit(
-            l.clone(),
-            v.visit_val(x)?,
-            v.visit_optmap(kts)?,
-            v.visit_val(uniont)?,
-            v.visit_val(ctort)?,
-        ),
-        TextLit(ts) => TextLit(
-            ts.iter()
-                .map(|t| t.traverse_ref(|e| v.visit_val(e)))
-                .collect::<Result<_, _>>()?,
-        ),
-        Equivalence(x, y) => Equivalence(v.visit_val(x)?, v.visit_val(y)?),
-        PartialExpr(e) => PartialExpr(e.traverse_ref(|e| v.visit_val(e))?),
-        Thunk(th) => Thunk(th.clone()),
-    })
-}
-
-pub struct TraverseRefWithBindersVisitor<F1, F2> {
-    pub visit_val: F1,
-    pub visit_under_binder: F2,
-}
-
-impl<'a, V1, V2, Err, F1, F2> ValueKindVisitor<'a, V1, V2>
-    for TraverseRefWithBindersVisitor<F1, F2>
-where
-    V1: 'a,
-    F1: FnMut(&'a V1) -> Result<V2, Err>,
-    F2: for<'b> FnOnce(&'a Binder, &'b V1, &'a V1) -> Result<V2, Err>,
-{
-    type Error = Err;
-
-    fn visit_val(&mut self, val: &'a V1) -> Result<V2, Self::Error> {
-        (self.visit_val)(val)
-    }
-    fn visit_binder<'b>(
-        mut self,
-        label: &'a Binder,
-        ty: &'a V1,
-        val: &'a V1,
-    ) -> Result<(V2, V2), Self::Error> {
-        let val = (self.visit_under_binder)(label, ty, val)?;
-        let ty = (self.visit_val)(ty)?;
-        Ok((ty, val))
-    }
-}