summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-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))
- }
-}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 22:03:48 +0000