diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/core.rs | 44 | ||||
| -rw-r--r-- | src/typecheck.rs | 8 |
2 files changed, 24 insertions, 28 deletions
diff --git a/src/core.rs b/src/core.rs index 8b0156c..51f1ef2 100644 --- a/src/core.rs +++ b/src/core.rs @@ -362,7 +362,7 @@ fn add_ui(u: usize, i: isize) -> usize { /// descend into a lambda or let expression that binds a variable of the same /// name in order to avoid shifting the bound variables by mistake. /// -pub fn shift<'i, S, T, A>(d: isize, v: V, e: Expr<'i, S, A>) -> Expr<'i, T, A> +pub fn shift<'i, S, T, A>(d: isize, v: V, e: &Expr<'i, S, A>) -> Expr<'i, T, A> where S: ::std::fmt::Debug, T: ::std::fmt::Debug, A: ::std::fmt::Debug, @@ -370,28 +370,24 @@ pub fn shift<'i, S, T, A>(d: isize, v: V, e: Expr<'i, S, A>) -> Expr<'i, T, A> use Expr::*; let V(x, n) = v; match e { - Const(a) => Const(a), - Var(V(x2, n2)) => { + &Const(a) => Const(a), + &Var(V(x2, n2)) => { let n3 = if x == x2 && n <= n2 { add_ui(n2, d) } else { n2 }; Var(V(x2, n3)) } - Lam(x2, tA, b) => { + &Lam(x2, ref tA, ref b) => { let n2 = if x == x2 { n + 1 } else { n }; - let tA2 = shift(d, V(x, n ), *tA); - let b2 = shift(d, V(x, n2), *b); + let tA2 = shift(d, V(x, n ), tA); + let b2 = shift(d, V(x, n2), b); Lam(x2, bx(tA2), bx(b2)) } - Pi(x2, tA, tB) => { + &Pi(x2, ref tA, ref tB) => { let n2 = if x == x2 { n + 1 } else { n }; - let tA2 = shift(d, V(x, n ), *tA); - let tB2 = shift(d, V(x, n2), *tB); + let tA2 = shift(d, V(x, n ), tA); + let tB2 = shift(d, V(x, n2), tB); pi(x2, tA2, tB2) } - App(f, a) => { - let f2 = shift(d, v, *f); - let a2 = shift(d, v, *a); - App(bx(f2), bx(a2)) - } + &App(ref f, ref a) => app(shift(d, v, f), shift(d, v, a)), /* shift d (V x n) (Let f mt r e) = Let f mt' r' e' where @@ -406,8 +402,8 @@ shift d v (Annot a b) = Annot a' b' a' = shift d v a b' = shift d v b */ - BoolLit(a) => BoolLit(a), - BoolAnd(a, b) => BoolAnd(bx(shift(d, v, *a)), bx(shift(d, v, *b))), + &BoolLit(a) => BoolLit(a), + &BoolAnd(ref a, ref b) => BoolAnd(bx(shift(d, v, a)), bx(shift(d, v, b))), /* shift d v (BoolOr a b) = BoolOr a' b' where @@ -500,8 +496,8 @@ shift d v (Note _ b) = b' -- and `shift` does nothing to a closed expression shift _ _ (Embed p) = Embed p */ - BuiltinType(t) => BuiltinType(t), - BuiltinValue(v) => BuiltinValue(v), + &BuiltinType(t) => BuiltinType(t), + &BuiltinValue(v) => BuiltinValue(v), e => panic!("Unimplemented shift case: {:?}", (d, v, e)), } } @@ -524,14 +520,14 @@ pub fn subst<'i, S, T, A>(v: V<'i>, a: Expr<'i, S, A>, b: Expr<'i, T, A>) -> Exp (_, Const(a)) => Const(a), (e, Lam(y, tA, b)) => { let n2 = if x == y { n + 1 } else { n }; - let tA2 = subst(V(x, n), e.clone(), *tA); - let b2 = subst(V(x, n2), shift(1, V(y, 0), e), *b); + let b2 = subst(V(x, n2), shift(1, V(y, 0), &e), *b); + let tA2 = subst(V(x, n), e, *tA); Lam(y, bx(tA2), bx(b2)) } (e, Pi(y, tA, tB)) => { let n2 = if x == y { n + 1 } else { n }; - let tA2 = subst(V(x, n), e.clone(), *tA); - let tB2 = subst(V(x, n2), shift(1, V(y, 0), e), *tB); + let tB2 = subst(V(x, n2), shift(1, V(y, 0), &e), *tB); + let tA2 = subst(V(x, n), e, *tA); pi(y, tA2, tB2) } (e, App(f, a)) => { @@ -583,9 +579,9 @@ pub fn normalize<S, T, A>(e: Expr<S, A>) -> Expr<T, A> App(f, a) => match normalize::<S, T, A>(*f) { Lam(x, _A, b) => { // Beta reduce let vx0 = V(x, 0); - let a2 = shift::<S, S, A>( 1, vx0, *a); + let a2 = shift::<S, S, A>( 1, vx0, &a); let b2 = subst::<S, T, A>(vx0, a2, *b); - let b3 = shift::<S, T, A>(-1, vx0, b2); + let b3 = shift::<S, T, A>(-1, vx0, &b2); normalize(b3) } f2 => match (f2, normalize::<S, T, A>(*a)) { diff --git a/src/typecheck.rs b/src/typecheck.rs index 3bd80ae..aedce38 100644 --- a/src/typecheck.rs +++ b/src/typecheck.rs @@ -122,7 +122,7 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>, .ok_or_else(|| TypeError::new(ctx, &e, UnboundVariable)) } &Lam(ref x, ref tA, ref b) => { - let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e.clone())); + let ctx2 = ctx.insert(x, (**tA).clone()).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)?; @@ -136,7 +136,7 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>, _ => return Err(TypeError::new(ctx, e, InvalidInputType((**tA).clone()))), }; - let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e.clone())); + let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e)); let tB = normalize(type_with(&ctx2, tB)?); let kB = match tB { Const(k) => k, @@ -157,9 +157,9 @@ pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>, let tA2 = type_with(ctx, a)?; if prop_equal(&tA, &tA2) { let vx0 = V(x, 0); - let a2 = shift::<S, S, X>( 1, vx0, (**a).clone()); + let a2 = shift::<S, S, X>( 1, vx0, a); let tB2 = subst(vx0, a2, (*tB).clone()); - let tB3 = shift::<S, S, X>(-1, vx0, tB2); + let tB3 = shift::<S, S, X>(-1, vx0, &tB2); Ok(tB3) } else { let nf_A = normalize(*tA); |