summaryrefslogtreecommitdiff
path: root/dhall/src/core/value.rs
diff options
context:
space:
mode:
authorNadrieril2019-08-13 20:54:15 +0200
committerNadrieril2019-08-13 20:54:15 +0200
commit77af0bbc171618f48531cc6b1d77e18089928885 (patch)
tree8bac17d4b3f1f1adf5f823708d322876eef6cfee /dhall/src/core/value.rs
parent5895c3aa6552f75d7e5202be561f9734fe8945e7 (diff)
Stop tracking the absence of Embed values at the type level
Diffstat (limited to '')
-rw-r--r--dhall/src/core/value.rs10
1 files changed, 5 insertions, 5 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 8486d6e..88d7a20 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -2,7 +2,7 @@ use std::collections::HashMap;
use dhall_syntax::{
rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
- NaiveDouble, Natural, X,
+ NaiveDouble, Natural,
};
use crate::core::thunk::{Thunk, TypedThunk};
@@ -10,7 +10,7 @@ use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
use crate::phase::normalize::{
apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr,
};
-use crate::phase::Typed;
+use crate::phase::{Normalized, Typed};
/// A semantic value. The invariants ensure this value represents a Weak-Head
/// Normal Form (WHNF). This means that this first constructor is the first constructor of the
@@ -59,7 +59,7 @@ pub enum Value {
TextLit(Vec<InterpolatedTextContents<Thunk>>),
Equivalence(TypedThunk, TypedThunk),
// Invariant: this must not contain a value captured by one of the variants above.
- PartialExpr(ExprF<Thunk, X>),
+ PartialExpr(ExprF<Thunk, Normalized>),
}
impl Value {
@@ -475,7 +475,7 @@ impl Shift for Value {
e.traverse_ref_with_special_handling_of_binders(
|v| Ok(v.shift(delta, var)?),
|x, v| Ok(v.shift(delta, &var.under_binder(x))?),
- |x| Ok(X::clone(x)),
+ |x| Ok(Normalized::clone(x)),
)?,
),
})
@@ -500,7 +500,7 @@ impl Subst<Typed> for Value {
&val.under_binder(x),
)
},
- X::clone,
+ Normalized::clone,
))
}
// Retry normalizing since substituting may allow progress