diff options
Diffstat (limited to 'dhall')
| -rw-r--r-- | dhall/src/normalize.rs | 10 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 6 |
2 files changed, 8 insertions, 8 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index d3766d5..4f07d9a 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -26,9 +26,9 @@ where match e { // Matches that don't normalize everything right away Let(f, _, r, b) => { - let r2 = shift::<Label, _, S, _>(1, V(f.clone(), 0), r); - let b2 = subst::<Label, _, S, _>(V(f.clone(), 0), &r2, b); - let b3 = shift::<Label, _, T, _>(-1, V(f.clone(), 0), &b2); + let r2 = shift::<Label, _, S, _>(1, &V(f.clone(), 0), r); + let b2 = subst::<Label, _, S, _>(&V(f.clone(), 0), &r2, b); + let b3 = shift::<Label, _, T, _>(-1, &V(f.clone(), 0), &b2); normalize(&b3) } BoolIf(b, t, f) => match normalize(b) { @@ -41,7 +41,7 @@ where App(f, a) => match normalize::<Label, S, T, A>(f) { Lam(x, _A, b) => { // Beta reduce - let vx0 = V(x, 0); + let vx0 = &V(x, 0); let a2 = shift::<Label, S, S, A>(1, vx0, a); let b2 = subst::<Label, S, T, A>(vx0, &a2, &b); let b3 = shift::<Label, S, T, A>(-1, vx0, &b2); @@ -92,7 +92,7 @@ where // TODO: restore when handling variables generically fixed // (App(box Builtin(ListBuild), a0), k) => { // let k = bx(k); - // let a1 = bx(shift(1, V("a", 0), &a0)); + // let a1 = bx(shift(1, &V("a", 0), &a0)); // normalize(&dhall!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0))) // } (App(box App(box App(box App(box Builtin(ListFold), _), box ListLit(_, xs)), _), cons), nil) => { diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index c2a2ca3..b7fead3 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -198,7 +198,7 @@ where Lam(x, ref tA, ref b) => { let ctx2 = ctx .insert(x, (**tA).clone()) - .map(|e| core::shift(1, V(x, 0), e)); + .map(|e| core::shift(1, &V(x, 0), e)); let tB = type_with(&ctx2, b)?; let p = Pi(x, tA.clone(), bx(tB)); let _ = type_with(ctx, &p)?; @@ -220,7 +220,7 @@ where let ctx2 = ctx .insert(x, (**tA).clone()) - .map(|e| core::shift(1, V(x, 0), e)); + .map(|e| core::shift(1, &V(x, 0), e)); let tB = normalize(&type_with(&ctx2, tB)?); let kB = match tB { Const(k) => k, @@ -252,7 +252,7 @@ where }; let tA2 = type_with(ctx, a)?; if prop_equal(&tA, &tA2) { - let vx0 = V(x, 0); + let vx0 = &V(x, 0); let a2 = shift::<&str, S, S, X>(1, vx0, a); let tB2 = subst(vx0, &a2, &tB); let tB3 = shift::<&str, S, S, X>(-1, vx0, &tB2); |