summaryrefslogtreecommitdiff
path: root/dhall/src/core/value.rs
diff options
context:
space:
mode:
authorNadrieril2019-05-07 18:38:54 +0200
committerNadrieril2019-05-07 18:38:54 +0200
commitb3f00a827bcdd0fe406ccf8913cc5fb7cd6e0f2f (patch)
tree18d8326069fe94bcb03177c3375fcf453a370759 /dhall/src/core/value.rs
parent8cb3046e0920bf24d66c578b1a2b184c741b73fe (diff)
Promote shift and subst_shift to traits
Diffstat (limited to '')
-rw-r--r--dhall/src/core/value.rs10
1 files changed, 7 insertions, 3 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 4c71778..412fe11 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -7,7 +7,7 @@ use dhall_syntax::{
};
use crate::core::thunk::{Thunk, TypeThunk};
-use crate::core::var::{AlphaLabel, AlphaVar};
+use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
use crate::phase::normalize::{
apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr,
};
@@ -316,8 +316,10 @@ impl Value {
pub(crate) fn from_builtin(b: Builtin) -> Value {
Value::AppliedBuiltin(b, vec![])
}
+}
- pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
+impl Shift for Value {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
match self {
Value::Lam(x, t, e) => Value::Lam(
x.clone(),
@@ -413,8 +415,10 @@ impl Value {
}
}
}
+}
- pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<Typed> for Value {
+ fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
// Retry normalizing since substituting may allow progress
Value::AppliedBuiltin(b, args) => apply_builtin(