summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/normalize.rs36
1 files changed, 17 insertions, 19 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index b5971cb..2fa3bc5 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -371,7 +371,7 @@ pub(crate) type NF = X;
#[derive(Debug, Clone)]
pub(crate) enum Value<Form> {
/// Closures
- Lam(Label, Thunk<Form>, (NormalizationContext, InputSubExpr)),
+ Lam(Label, Thunk<Form>, Thunk<Form>),
AppliedBuiltin(Builtin, Vec<Value<Form>>),
/// `λ(x: a) -> Some x`
OptionalSomeClosure(TypeThunk<Form>),
@@ -405,14 +405,11 @@ impl Value<NF> {
/// Convert the value back to a (normalized) syntactic expression
pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
match self {
- Value::Lam(x, t, (ctx, e)) => {
- let ctx2 = ctx.skip(&x);
- rc(ExprF::Lam(
- x.clone(),
- t.to_nf().normalize_to_expr(),
- normalize_whnf(ctx2, e).normalize_to_expr(),
- ))
- }
+ Value::Lam(x, t, e) => rc(ExprF::Lam(
+ x.clone(),
+ t.to_nf().normalize_to_expr(),
+ e.to_nf().normalize_to_expr(),
+ )),
Value::AppliedBuiltin(b, args) => {
let mut e = rc(ExprF::Builtin(b));
for v in args {
@@ -535,8 +532,8 @@ impl Value<WHNF> {
pub(crate) fn normalize(&self) -> Value<NF> {
match self {
- Value::Lam(x, t, (ctx, e)) => {
- Value::Lam(x.clone(), t.normalize(), (ctx.clone(), e.clone()))
+ Value::Lam(x, t, e) => {
+ Value::Lam(x.clone(), t.normalize(), e.normalize())
}
Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
*b,
@@ -618,9 +615,10 @@ impl Value<WHNF> {
/// Apply to a value
pub(crate) fn app(self, val: Value<WHNF>) -> Value<WHNF> {
match (self, val) {
- (Value::Lam(x, _, (ctx, e)), val) => {
- let ctx2 = ctx.insert(&x, val);
- normalize_whnf(ctx2, e)
+ (Value::Lam(x, _, e), val) => {
+ let val =
+ PartiallyNormalized(val, None, std::marker::PhantomData);
+ e.subst_shift(&V(x, 0), &val).normalize_whnf()
}
(Value::AppliedBuiltin(b, mut args), val) => {
args.push(val);
@@ -675,9 +673,9 @@ impl Value<WHNF> {
Value::NEOptionalLit(th) => {
th.shift(delta, var);
}
- Value::Lam(x, t, (_, e)) => {
+ Value::Lam(x, t, e) => {
t.shift(delta, var);
- shift_mut(delta, &var.shift0(1, x), e);
+ e.shift(delta, &var.shift0(1, x));
}
Value::AppliedBuiltin(_, args) => {
for x in args.iter_mut() {
@@ -739,10 +737,10 @@ impl Value<WHNF> {
val: &PartiallyNormalized<'static>,
) -> Self {
match self {
- Value::Lam(x, t, (ctx, e)) => Value::Lam(
+ Value::Lam(x, t, e) => Value::Lam(
x.clone(),
t.subst_shift(var, val),
- (ctx.subst_shift(var, val), e.clone()),
+ e.subst_shift(&var.shift0(1, x), val),
),
Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin(
*b,
@@ -981,7 +979,7 @@ fn normalize_whnf(
ExprF::Lam(x, t, e) => Value::Lam(
x.clone(),
Thunk::new(ctx.clone(), t.clone()),
- (ctx, e.clone()),
+ Thunk::new(ctx.skip(x), e.clone()),
),
ExprF::Builtin(b) => Value::from_builtin(*b),
ExprF::Const(c) => Value::Const(*c),