From 7062de011eab7954f4bcf78fa1cf970ba91d6a5a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 18:04:16 +0000 Subject: 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. --- dhall/src/semantics/nze/mod.rs | 1 - dhall/src/semantics/nze/value.rs | 228 ++++++++++++++----------------------- dhall/src/semantics/nze/visitor.rs | 167 --------------------------- 3 files changed, 87 insertions(+), 309 deletions(-) delete mode 100644 dhall/src/semantics/nze/visitor.rs (limited to 'dhall/src/semantics') 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>| { + 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 { } } -impl ValueKind { - fn traverse_ref_with_special_handling_of_binders<'a, V2, E>( - &'a self, - visit_val: impl FnMut(&'a V) -> Result, - visit_under_binder: impl for<'b> FnMut( - &'a Binder, - &'b V, - &'a V, - ) -> Result, - ) -> Result, 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 { - 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 { - 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; - 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, Self::Error> { - x.iter().map(|e| self.visit_val(e)).collect() - } - fn visit_opt( - &mut self, - x: &'a Option, - ) -> Result, Self::Error> { - Ok(match x { - Some(x) => Some(self.visit_val(x)?), - None => None, - }) - } - fn visit_map( - &mut self, - x: impl IntoIterator, - ) -> Result - where - V1: 'a, - T: FromIterator<(Label, V2)>, - { - x.into_iter() - .map(|(k, x)| Ok((k.clone(), self.visit_val(x)?))) - .collect() - } - fn visit_optmap( - &mut self, - x: impl IntoIterator)>, - ) -> Result - where - V1: 'a, - T: FromIterator<(Label, Option)>, - { - x.into_iter() - .map(|(k, x)| Ok((k.clone(), self.visit_opt(x)?))) - .collect() - } - - fn visit( - self, - input: &'a ValueKind, - ) -> Result, Self::Error> { - visit_ref(self, input) - } -} - -fn visit_ref<'a, Visitor, V1, V2>( - mut v: Visitor, - input: &'a ValueKind, -) -> Result, 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::>()?, - ), - 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 { - pub visit_val: F1, - pub visit_under_binder: F2, -} - -impl<'a, V1, V2, Err, F1, F2> ValueKindVisitor<'a, V1, V2> - for TraverseRefWithBindersVisitor -where - V1: 'a, - F1: FnMut(&'a V1) -> Result, - F2: for<'b> FnOnce(&'a Binder, &'b V1, &'a V1) -> Result, -{ - type Error = Err; - - fn visit_val(&mut self, val: &'a V1) -> Result { - (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)) - } -} -- cgit v1.2.3