summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/core.rs44
-rw-r--r--src/typecheck.rs8
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);