diff options
| -rw-r--r-- | dhall/src/semantics/nze/mod.rs | 1 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/value.rs | 228 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/visitor.rs | 167 |
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)) - } -} |