summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/semantics/core/value.rs165
-rw-r--r--dhall/src/semantics/core/var.rs144
-rw-r--r--dhall/src/syntax/ast/expr.rs3
3 files changed, 39 insertions, 273 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index b4e4e61..28f8e37 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -381,21 +381,30 @@ impl ValueKind<Value> {
}
impl<V> ValueKind<V> {
+ pub(crate) 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 FnMut(&'a Binder, &'a V) -> Result<V2, E>,
+ ) -> Result<ValueKind<V2>, E> {
+ use crate::semantics::visitor;
+ use visitor::ValueKindVisitor;
+ visitor::TraverseRefWithBindersVisitor {
+ visit_val,
+ visit_under_binder,
+ }
+ .visit(self)
+ }
+
pub(crate) 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 FnMut(&'a Binder, &'a V) -> V2,
) -> ValueKind<V2> {
- use crate::semantics::visitor;
use crate::syntax::trivial_result;
- use visitor::ValueKindVisitor;
- trivial_result(
- visitor::TraverseRefWithBindersVisitor {
- visit_val: |x| Ok(map_val(x)),
- visit_under_binder: |l, x| Ok(map_under_binder(l, x)),
- }
- .visit(self),
- )
+ trivial_result(self.traverse_ref_with_special_handling_of_binders(
+ |x| Ok(map_val(x)),
+ |l, x| Ok(map_under_binder(l, x)),
+ ))
}
#[allow(dead_code)]
@@ -411,7 +420,9 @@ impl<V> ValueKind<V> {
impl Shift for Value {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(Value(self.0.shift(delta, var)?))
+ Some(Value(Rc::new(RefCell::new(
+ self.0.borrow().shift(delta, var)?,
+ ))))
}
}
@@ -420,7 +431,10 @@ impl Shift for ValueInternal {
Some(ValueInternal {
form: self.form,
kind: self.kind.shift(delta, var)?,
- ty: self.ty.shift(delta, var)?,
+ ty: match &self.ty {
+ None => None,
+ Some(ty) => Some(ty.shift(delta, var)?),
+ },
span: self.span.clone(),
})
}
@@ -429,64 +443,11 @@ impl Shift for ValueInternal {
impl Shift for ValueKind<Value> {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(match self {
- ValueKind::Lam(x, t, e) => ValueKind::Lam(
- x.clone(),
- t.shift(delta, var)?,
- e.shift(delta, &var.under_binder(x))?,
- ),
- ValueKind::AppliedBuiltin(b, args) => {
- ValueKind::AppliedBuiltin(*b, args.shift(delta, var)?)
- }
- ValueKind::Pi(x, t, e) => ValueKind::Pi(
- x.clone(),
- t.shift(delta, var)?,
- e.shift(delta, &var.under_binder(x))?,
- ),
ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?),
- ValueKind::Const(c) => ValueKind::Const(*c),
- ValueKind::BoolLit(b) => ValueKind::BoolLit(*b),
- ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n),
- ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n),
- ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n),
- ValueKind::EmptyOptionalLit(tth) => {
- ValueKind::EmptyOptionalLit(tth.shift(delta, var)?)
- }
- ValueKind::NEOptionalLit(th) => {
- ValueKind::NEOptionalLit(th.shift(delta, var)?)
- }
- ValueKind::EmptyListLit(tth) => {
- ValueKind::EmptyListLit(tth.shift(delta, var)?)
- }
- ValueKind::NEListLit(elts) => {
- ValueKind::NEListLit(elts.shift(delta, var)?)
- }
- ValueKind::RecordLit(kvs) => {
- ValueKind::RecordLit(kvs.shift(delta, var)?)
- }
- ValueKind::RecordType(kvs) => {
- ValueKind::RecordType(kvs.shift(delta, var)?)
- }
- ValueKind::UnionType(kts) => {
- ValueKind::UnionType(kts.shift(delta, var)?)
- }
- ValueKind::UnionConstructor(x, kts) => {
- ValueKind::UnionConstructor(x.clone(), kts.shift(delta, var)?)
- }
- ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit(
- x.clone(),
- v.shift(delta, var)?,
- kts.shift(delta, var)?,
- ),
- ValueKind::TextLit(elts) => {
- ValueKind::TextLit(elts.shift(delta, var)?)
- }
- ValueKind::Equivalence(x, y) => ValueKind::Equivalence(
- x.shift(delta, var)?,
- y.shift(delta, var)?,
- ),
- ValueKind::PartialExpr(e) => {
- ValueKind::PartialExpr(e.shift(delta, var)?)
- }
+ _ => self.traverse_ref_with_special_handling_of_binders(
+ |x| Ok(x.shift(delta, var)?),
+ |b, x| Ok(x.shift(delta, &var.under_binder(b))?),
+ )?,
})
}
}
@@ -502,7 +463,9 @@ impl Subst<Value> for Value {
}
val.clone()
}
- _ => Value(self.0.subst_shift(var, val)),
+ _ => Value(Rc::new(RefCell::new(
+ self.0.borrow().subst_shift(var, val),
+ ))),
}
}
}
@@ -513,7 +476,7 @@ impl Subst<Value> for ValueInternal {
// The resulting value may not stay in wnhf after substitution
form: Unevaled,
kind: self.kind.subst_shift(var, val),
- ty: self.ty.subst_shift(var, val),
+ ty: self.ty.as_ref().map(|x| x.subst_shift(var, val)),
span: self.span.clone(),
}
}
@@ -522,65 +485,13 @@ impl Subst<Value> for ValueInternal {
impl Subst<Value> for ValueKind<Value> {
fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
match self {
- ValueKind::AppliedBuiltin(b, args) => {
- ValueKind::AppliedBuiltin(*b, args.subst_shift(var, val))
- }
- ValueKind::PartialExpr(e) => {
- ValueKind::PartialExpr(e.subst_shift(var, val))
- }
- ValueKind::TextLit(elts) => {
- ValueKind::TextLit(elts.subst_shift(var, val))
- }
- ValueKind::Lam(x, t, e) => ValueKind::Lam(
- x.clone(),
- t.subst_shift(var, val),
- e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
- ),
- ValueKind::Pi(x, t, e) => ValueKind::Pi(
- x.clone(),
- t.subst_shift(var, val),
- e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
- ),
ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(),
ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()),
- ValueKind::Const(c) => ValueKind::Const(*c),
- ValueKind::BoolLit(b) => ValueKind::BoolLit(*b),
- ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n),
- ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n),
- ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n),
- ValueKind::EmptyOptionalLit(tth) => {
- ValueKind::EmptyOptionalLit(tth.subst_shift(var, val))
- }
- ValueKind::NEOptionalLit(th) => {
- ValueKind::NEOptionalLit(th.subst_shift(var, val))
- }
- ValueKind::EmptyListLit(tth) => {
- ValueKind::EmptyListLit(tth.subst_shift(var, val))
- }
- ValueKind::NEListLit(elts) => {
- ValueKind::NEListLit(elts.subst_shift(var, val))
- }
- ValueKind::RecordLit(kvs) => {
- ValueKind::RecordLit(kvs.subst_shift(var, val))
- }
- ValueKind::RecordType(kvs) => {
- ValueKind::RecordType(kvs.subst_shift(var, val))
- }
- ValueKind::UnionType(kts) => {
- ValueKind::UnionType(kts.subst_shift(var, val))
- }
- ValueKind::UnionConstructor(x, kts) => ValueKind::UnionConstructor(
- x.clone(),
- kts.subst_shift(var, val),
- ),
- ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit(
- x.clone(),
- v.subst_shift(var, val),
- kts.subst_shift(var, val),
- ),
- ValueKind::Equivalence(x, y) => ValueKind::Equivalence(
- x.subst_shift(var, val),
- y.subst_shift(var, val),
+ _ => self.map_ref_with_special_handling_of_binders(
+ |x| x.subst_shift(var, val),
+ |b, x| {
+ x.subst_shift(&var.under_binder(b), &val.under_binder(b))
+ },
),
}
}
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 99d3125..c21e53e 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,6 +1,6 @@
use std::collections::HashMap;
-use crate::syntax::{ExprKind, InterpolatedTextContents, Label, V};
+use crate::syntax::{Label, V};
/// Stores a pair of variables: a normal one and one
/// that corresponds to the alpha-normalized version of the first one.
@@ -143,145 +143,3 @@ impl From<Binder> for Label {
x.name
}
}
-impl Shift for () {
- fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option<Self> {
- Some(())
- }
-}
-
-impl<A: Shift, B: Shift> Shift for (A, B) {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some((self.0.shift(delta, var)?, self.1.shift(delta, var)?))
- }
-}
-
-impl<T: Shift> Shift for Option<T> {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(match self {
- None => None,
- Some(x) => Some(x.shift(delta, var)?),
- })
- }
-}
-
-impl<T: Shift> Shift for Box<T> {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(Box::new(self.as_ref().shift(delta, var)?))
- }
-}
-
-impl<T: Shift> Shift for std::rc::Rc<T> {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(std::rc::Rc::new(self.as_ref().shift(delta, var)?))
- }
-}
-
-impl<T: Shift> Shift for std::cell::RefCell<T> {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(std::cell::RefCell::new(self.borrow().shift(delta, var)?))
- }
-}
-
-impl<T: Shift, E: Clone> Shift for ExprKind<T, E> {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(self.traverse_ref_with_special_handling_of_binders(
- |v| Ok(v.shift(delta, var)?),
- |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
- )?)
- }
-}
-
-impl<T: Shift> Shift for Vec<T> {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(
- self.iter()
- .map(|v| Ok(v.shift(delta, var)?))
- .collect::<Result<_, _>>()?,
- )
- }
-}
-
-impl<K, T: Shift> Shift for HashMap<K, T>
-where
- K: Clone + std::hash::Hash + Eq,
-{
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(
- self.iter()
- .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?)))
- .collect::<Result<_, _>>()?,
- )
- }
-}
-
-impl<T: Shift> Shift for InterpolatedTextContents<T> {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(self.traverse_ref(|x| Ok(x.shift(delta, var)?))?)
- }
-}
-
-impl<S> Subst<S> for () {
- fn subst_shift(&self, _var: &AlphaVar, _val: &S) -> Self {}
-}
-
-impl<S, A: Subst<S>, B: Subst<S>> Subst<S> for (A, B) {
- fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
- (self.0.subst_shift(var, val), self.1.subst_shift(var, val))
- }
-}
-
-impl<S, T: Subst<S>> Subst<S> for Option<T> {
- fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
- self.as_ref().map(|x| x.subst_shift(var, val))
- }
-}
-
-impl<S, T: Subst<S>> Subst<S> for Box<T> {
- fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
- Box::new(self.as_ref().subst_shift(var, val))
- }
-}
-
-impl<S, T: Subst<S>> Subst<S> for std::rc::Rc<T> {
- fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
- std::rc::Rc::new(self.as_ref().subst_shift(var, val))
- }
-}
-
-impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> {
- fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
- std::cell::RefCell::new(self.borrow().subst_shift(var, val))
- }
-}
-
-impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprKind<T, E> {
- fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
- self.map_ref_with_special_handling_of_binders(
- |v| v.subst_shift(var, val),
- |x, v| v.subst_shift(&var.under_binder(x), &val.under_binder(x)),
- )
- }
-}
-
-impl<S, T: Subst<S>> Subst<S> for Vec<T> {
- fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
- self.iter().map(|v| v.subst_shift(var, val)).collect()
- }
-}
-
-impl<S, T: Subst<S>> Subst<S> for InterpolatedTextContents<T> {
- fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
- self.map_ref(|x| x.subst_shift(var, val))
- }
-}
-
-impl<S, K, T: Subst<S>> Subst<S> for HashMap<K, T>
-where
- K: Clone + std::hash::Hash + Eq,
-{
- fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
- self.iter()
- .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
- .collect()
- }
-}
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 0ac31a5..04b5adc 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -174,9 +174,6 @@ pub enum ExprKind<SubExpr, Embed> {
}
impl<Label> V<Label> {
- pub(crate) fn name(&self) -> &Label {
- &self.0
- }
pub(crate) fn idx(&self) -> usize {
self.1
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 18:35:01 +0000