summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-03-08 18:47:25 +0100
committerNadrieril2019-03-08 18:47:25 +0100
commit0916eafc12b0ccbbf5b524a273903a0a84f30e74 (patch)
treebb00b7028835c54db4787e326abed74678ce3884 /dhall
parent74719869dc8aae53bf9521de55188c08f4ebaf11 (diff)
Make labels non-Copy
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/normalize.rs10
-rw-r--r--dhall/src/typecheck.rs6
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);