summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
authorNadrieril2020-01-30 18:04:16 +0000
committerNadrieril2020-01-30 18:04:16 +0000
commit7062de011eab7954f4bcf78fa1cf970ba91d6a5a (patch)
treef587d2d468d467bd5759ae4e2b8b69f9edc827fc /dhall/src
parent8ff022fa2cec34bc1d46ac3655d0c3d228ef893c (diff)
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.
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/semantics/nze/mod.rs1
-rw-r--r--dhall/src/semantics/nze/value.rs228
-rw-r--r--dhall/src/semantics/nze/visitor.rs167
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))
- }
-}