summaryrefslogtreecommitdiff
path: root/dhall/src/core
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/core')
-rw-r--r--dhall/src/core/thunk.rs10
-rw-r--r--dhall/src/core/value.rs14
2 files changed, 10 insertions, 14 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index c18014e..7c5c537 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -2,7 +2,7 @@ use std::borrow::Cow;
use std::cell::{Ref, RefCell};
use std::rc::Rc;
-use dhall_syntax::{Const, ExprF, X};
+use dhall_syntax::{Const, ExprF};
use crate::core::context::{NormalizationContext, TypecheckContext};
use crate::core::value::Value;
@@ -12,7 +12,7 @@ use crate::phase::normalize::{
apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr,
};
use crate::phase::typecheck::type_of_const;
-use crate::phase::{NormalizedSubExpr, Type, Typed};
+use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed};
#[derive(Debug, Clone, Copy)]
enum Marker {
@@ -30,7 +30,7 @@ enum ThunkInternal {
/// Partially normalized value whose subexpressions have been thunked (this is returned from
/// typechecking). Note that this is different from `Value::PartialExpr` because there is no
/// requirement of WHNF here.
- PartialExpr(ExprF<Thunk, X>),
+ PartialExpr(ExprF<Thunk, Normalized>),
/// Partially normalized value.
/// Invariant: if the marker is `NF`, the value must be fully normalized
Value(Marker, Value),
@@ -123,7 +123,7 @@ impl Thunk {
ThunkInternal::Value(WHNF, v).into_thunk()
}
- pub fn from_partial_expr(e: ExprF<Thunk, X>) -> Thunk {
+ pub fn from_partial_expr(e: ExprF<Thunk, Normalized>) -> Thunk {
ThunkInternal::PartialExpr(e).into_thunk()
}
@@ -309,7 +309,6 @@ impl Shift for ThunkInternal {
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)),
)?,
),
ThunkInternal::Value(m, v) => {
@@ -356,7 +355,6 @@ impl Subst<Typed> for ThunkInternal {
&val.under_binder(x),
)
},
- X::clone,
),
),
ThunkInternal::Value(_, v) => {
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 8486d6e..20a6021 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 {
@@ -243,7 +243,7 @@ impl Value {
y.normalize_to_expr_maybe_alpha(alpha),
)),
Value::PartialExpr(e) => {
- rc(e.map_ref_simple(|v| v.normalize_to_expr_maybe_alpha(alpha)))
+ rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha)))
}
}
}
@@ -333,8 +333,8 @@ impl Value {
y.normalize_mut();
}
Value::PartialExpr(e) => {
- // TODO: need map_mut_simple
- e.map_ref_simple(|v| {
+ // TODO: need map_mut
+ e.map_ref(|v| {
v.normalize_nf();
});
}
@@ -475,7 +475,6 @@ 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)),
)?,
),
})
@@ -500,7 +499,6 @@ impl Subst<Typed> for Value {
&val.under_binder(x),
)
},
- X::clone,
))
}
// Retry normalizing since substituting may allow progress